The previous page introduced the leakage record L(q) and the simulator-property claim: two queries with the same L produce byte-identical wire transcripts. This page is about how we believe that claim — three independent layers of evidence, each addressing a different failure mode.

1. EasyCrypt — the simulator-property is mechanically proved

The strongest layer. A formal model of what each backend emits on the wire (Real) is shown to be equivalent to a model that has access only to L(q) (Sim). The theorem statement, in EasyCrypt syntax:

lemma simulator_property_per_query (b0 : backend) (q1 q2 : query) :
  L_eq q1 q2 =>
  equiv [
    Real.query ~ Real.query :
    \={glob Real} /\ b{1} = b0 /\ b{2} = b0
                 /\ q{1} = q1 /\ q{2} = q2
    ==>
    \={res}
  ].

Read aloud: whenever q1, q2 agree on the leakage record, running Real.query on either yields the same result. A multi-query (batched) version extends this to whole sessions, so privacy doesn't drift across sequences of queries either. Both versions are closed; no admit tactics. The lemmas live under proofs/easycrypt/; the central per-query statement is at proofs/easycrypt/Theorem.ec:232, and the multi-query one at :313.

2. Kani — helper-level invariants are exhaustively model-checked

EasyCrypt proves the protocol behaves as specified. Kani addresses a different failure mode: the spec is faithful, but the Rust implementation drifts away from it. The verifier checks helper routines such as plan_index_pbc_rounds, plan_chunk_rounds, pad_chunk_rounds_for_presence, and build_index_alphas_batched inline in each backend. These checks verify the closed invariants (for example, index-group count bounds) and protocol-shape guarantees such as CHUNK round presence. The admitted chunk_max axis is explicitly documented rather than closed.

Kani is a bounded model checker for Rust: it explores the full state space of small functions in seconds. The harnesses live inline in pir-sdk-client/src/dpf.rs::kani_harnesses and the analogous modules in harmony.rs and onion.rs, so they're maintained beside the code they verify.

3. Live integration tests — wire-byte equality is asserted end-to-end

The third layer addresses yet another failure mode: spec faithful, helpers correct, but the assembled client behaves differently in practice (for example, an emergent ordering bug). A test driver runs a found query and a not-found query through the same client against the live PIR deployment, captures the full wire transcript, and asserts byte-equality round by round with assert_profiles_equivalent. One test per backend:

• dpf_found_vs_not_found_have_byte_identical_profiles
• harmony_found_vs_not_found_have_byte_identical_profiles
• onion_found_vs_not_found_have_byte_identical_profiles

A separate cross-language test confirms that the standalone TypeScript client produces byte-equivalent traffic to the Rust reference — so the browser implementation isn't quietly doing something different from the canonical Rust SDK.

These three layers don't add up to a single proof; they cover different ways the claim could be wrong. The next page covers what's not in scope, and what cryptographic results we're relying on without re-proving.