The verification covers wire shape — the lengths, the round counts, the item vectors. It does not cover cryptographic indistinguishability of the bytes inside each fixed-length envelope. That's a different kind of claim, and it's outside the verification effort by design.

Mechanized vs cited-by-hypothesis

The simulator-property theorem is a statement about lengths and structure. It says: at every wire round, the request and response sizes, and the labelled item vectors, are determined by L(q). Whether the bytes inside those fixed-length buffers are indistinguishable is a separate question — it depends on the security of the underlying cryptographic primitives.

DPF keys, FHE ciphertexts, and PRP outputs are treated as ideal-primitive uniform randomness in the EasyCrypt model. That hypothesis is cited from the underlying primitives' papers:

• DPF security from the libdpf construction's reduction to a length-doubling PRG.
• OnionPIR semantic security from BFV's IND-CPA argument, as instantiated in the OnionPIRv2-fork crate.
• HarmonyPIR PRP indistinguishability from the Hoang–Morris–Rogaway / FastPRP papers (FastPRP is the active backend in this build).

Closing this gap formally — re-proving the cryptographic primitives from scratch in EasyCrypt — would be a multi-year research project per primitive. The verification effort deliberately did not pursue it. The site's section on each backend (DPF, OnionPIR, HarmonyPIR) cites the underlying papers for the cryptographic claims.

What the claim means for users

For BitcoinPIR's actual threat model — "the server should not learn which scripthash you queried, nor whether it was found, nor the cuckoo position it matched at" plus a deliberate leak of approximate per-query UTXO count — the verification is as tight as a non-research-project codebase can reasonably get.

Stated precisely: every wire-observable axis is either structurally constant, explicitly admitted in L, or outside scope. An adversary who records a session of BitcoinPIR queries cannot use the wire shape to fingerprint the wallet's behavior, even with adversarially chosen scripthash patterns. Side channels that PIR doesn't address — timing, network metadata, the observation that you're using a wallet at all — are listed in section 12.