Worked example: the glob endpoint on a concrete adversary #
This file is a concrete, worked example of the EasyCrypt-style relational lazy ≈ eager
endpoint GaudisCrypt.Lib.RO.Instantiate.prhl_instantiate_of_glob
(ROCouplingEquiv.lean).
We build a concrete adversary procedure A_ex that genuinely uses all three kinds of
memory the framework distinguishes:
- a global program variable
advG : Variable Nat(read and written), - a local variable (of type
Nat, read and written), and - the oracle holes —
A_exqueries the oracle at each of its two inputsa,band stores the two answers in twooutputlocalsr_a,r_b, which it then returns.
The whole point of the endpoint is that the adversary's only assumption is a checkable
footprint-disjointness fact FVP.fvP_proc A ≤ (random_oracle_state.footprint)ᶜ — "A never
touches the oracle table". We discharge that disjointness completely (no sorry, no new
axiom), which is the substance of the example: everything A touches (advG, its locals,
the hole plumbing) is provably disjoint from the random oracle.
The per-query lazy ≈ eager coupling h is left as a hypothesis, exactly as in the endpoint's
own statement — it is the framework's separate obligation, not proved standalone here.
What the example concludes: a correct collision transfer #
The invariant P_ex is the genuine lazy ≈ eager relation between the eager state g₁ (full,
pre-sampled random function) and the lazy state g₂ (partial, filled on demand): they agree
outside the oracle, the eager table is total, and the lazy table is a subset of the eager one.
This is what makes the per-query coupling h a real, satisfiable obligation.
The collision is stated on A_ex's output — its two observed answers — and transferred by the
coupling's result-equality: A_ex found a collision (two distinct queried inputs with equal
answers) against the eager (real) oracle iff it did against the lazy one.
⚠ Why not a table-level Collides(g₁) ↔ Collides(g₂) invariant? Because it is false: the
eager table is a total function input → output, which collides by construction (pigeonhole) while
the partial lazy table usually does not. An h forcing Collides(eager) ↔ Collides(lazy) would be
unsatisfiable, making the whole theorem vacuous. Putting the collision on the output and using the
real invariant fixes this.
Generic footprint helpers (chain footprints and their globalL-reduction) #
A chained lens's footprint is bounded by the outer lift of the inner footprint. Each
generator (L.chain v).liftSubProbability κ equals L.liftSubProbability (v.liftSubProbability κ) (Lens.liftSubProbability_chain), a member of the lifted image.
Lens.reduceFootprint L of a chained lens's footprint is bounded by the inner lens's footprint.
Combine chain_footprint_le_lift with Lens.reduceFootprint's exact-left-inverse property
(FVP.Lens.reduceFootprint_extend). Needs [Nonempty c] for the extend/reduce round trip.
The L-reduction of a footprint disjoint from L.chain v is disjoint from v (the honest
converse of reduce_chain_le_compl). Each reduced generator reduceSubProbability L (k, i, o)
commutes with every generator v.liftSubProbability g of v.footprint: the two Fubini
identities (Lens.reduceSubProbability_mul_left/_right) turn the goal into commutation of
L.liftSubProbability (v.liftSubProbability g) (= the L.chain v generator, by
Lens.liftSubProbability_chain) with k, which
hdisj : R ≤ ((L.chain v).footprint)ᶜ supplies.
Two lenses chained through a common outer lens are disjoint when their inner lenses are.
The two chained overwrites both go through L; commutation reduces to
inA.set _ (inB.set _ ·) = inB.set _ (inA.set _ ·) on the L-content, i.e. the inner
disjoint inA inB.
A lens chained through L is disjoint from one chained through a disjoint outer lens M.
Each chained overwrite preserves the other outer lens's get, so the two commute.
Reading through a lens (post-composed with any k) has footprint bounded by the lens. Such
a getter factors as ProgramDenotation.get l >>= (pure ∘ k), so footprint_bind_le bounds it
by (get l).footprint ⊔ ⊥ ≤ l.footprint. Handles both a raw lens read and the wrapped getter
that StmtWithHoles.assign builds.
The concrete example #
The procedure state of the example.
Equations
Instances For
The first answer local r_a (.intoVars at the second-then-first component of
Nat × (output × output)).
Equations
Instances For
The second answer local r_b (.intoVars at the second-then-second component).
Equations
Instances For
The second input parameter b (.intoParams, Lens.snd).
Instances For
The return getter: read back the pair of observed answers (r_a, r_b).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The global variable advG viewed inside the procedure state.
Equations
Instances For
The example adversary body. It exercises global + local + oracle memory:
copy the global into itself (touches advG), query the oracle at parameter a storing the
answer in local r_a (first oracle hole), query at b storing in r_b (second oracle hole),
then read the global into the Nat scratch local (touches both a local and advG).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The example adversary procedure: bodyEx returning the observed answer pair (r_a, r_b).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The genuine lazy ≈ eager invariant. P_ex g₁ g₂ relates the eager state g₁ (whose
oracle table is the full pre-sampled random function) to the lazy state g₂ (whose oracle
table is partial, filled on demand):
- they agree outside the oracle (
random_oracle_state.compl); - the eager table is total (every input has a defined answer — it was pre-sampled); and
- the lazy table is a subset of the eager one (every cached lazy answer matches eager).
Conjuncts 2–3 are exactly the honest coupling of the eager and lazy oracles: after any query the
eager side already knows the answer and the lazy side agrees wherever it has committed. This is
what makes the per-query hypothesis h (relating random_oracle_query inp to lazy_query inp)
a real, satisfiable obligation.
Why a table-level collision invariant would be wrong (the old, vacuous version): the eager
table is a total function input → output and hence collides by construction whenever
card input > card output (pigeonhole), while the partial lazy table usually does not — so
Collides(eager) ↔ Collides(lazy) is false and any h forcing it is unsatisfiable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Discharging FVP.fvP_proc A_ex ≤ (random_oracle_state.footprint)ᶜ #
Everything A_ex touches — the global advG, the two locals, and the input parameter — is a lens
disjoint from roLift stateEx = globalL.chain random_oracle_state (advG by hypothesis
instDisj, the locals/param through the localL/globalL split). So the whole syntactic
footprint lands in ((roLift stateEx).footprint)ᶜ; reducing through globalL
(reduce_le_compl_of_chain) then lands it in (random_oracle_state.footprint)ᶜ.
A lens read's footprint (raw or assign-wrapped) lands in ((roLift stateEx).footprint)ᶜ.
A lens write's family footprint lands in ((roLift stateEx).footprint)ᶜ.
The body's syntactic footprint is disjoint from the oracle table. Two oracle holes just add one
more set/get sup summand of the same shape as the single-hole case.
The return getter retExG (reading the two answer locals r_a, r_b) has footprint in
((roLift stateEx).footprint)ᶜ. It factors as get raLocalL >>= get rbLocalL >>= pure ∘ pair,
so footprint_bind_le bounds it by raLocalL.footprint ⊔ rbLocalL.footprint ⊔ ⊥, both disjoint
from the oracle.
The example's footprint disjointness from the random oracle — fully discharged.
The example invariant's endpoint premises #
hrefine is the first conjunct of P_ex. hstable keeps the outside-oracle agreement from its
own hypothesis and transports the eager-total/lazy⊆eager conjuncts along the table equalities.
P_ex forces agreement on the non-oracle globals — the first conjunct of P_ex.
P_ex is determined by the oracle table: overwriting the non-oracle globals on both sides while
keeping each side's table preserves the outside agreement (hc), the eager-total conjunct and
the lazy ⊆ eager conjunct (both transported along the table equalities ho₁/ho₂, since the
oracle tables themselves are unchanged).
The worked instantiation of prhl_instantiate_of_glob. For the concrete adversary A_ex
(global advG, a Nat local, two output locals for the two oracle answers, two oracle holes)
and the genuine lazy ≈ eager invariant P_ex, the eager and lazy instantiations couple under
P_ex, given only the per-query lazy ≈ eager coupling h. Every structural hypothesis of the
endpoint — footprint disjointness (hdisj_ex) and the two P-side conditions (hrefine_ex,
hstable_ex) — is discharged; h is a hypothesis, as in the endpoint's own statement, and is
now a real obligation because P_ex is satisfiable (see P_ex).
Collision transfer, read off the coupling's result-equality. Running A_ex on inputs
(a, b) returns the pair of oracle answers A_ex observed for a and b. liftPost P_ex
gives equal results on the two marginals (u.1 = v.1), so the output-collision event
"A_ex queried two distinct inputs and got equal answers" — a ≠ b ∧ u.1.1 = u.1.2 — holds
against the eager (real) oracle exactly when it holds against the lazy one.
Unlike a table-level Collides ↔ Collides, this is a true statement: it lives entirely on
A_ex's output, which the coupling equates, and never inspects the (differently-shaped)
eager/lazy tables. It is the abstract output_win_transfer specialized to A_ex with the
win predicate Win (r : output × output) := a ≠ b ∧ r.1 = r.2.
End-to-end collision transfer for the worked adversary — no coupling hypothesis.
The per-query h of glob_example_collision_transfer is pointwise unsatisfiable for the
genuine eager/lazy pair (a fixed eager entry cannot couple with a fresh lazy sample), so this
is the honest form: at the whole-game level, with the initialisations included,
random_oracle_init supplies the eager table's randomness and theorem 1 (the
convert-sliding engine behind output_win_transfer_games) discharges everything. The only
remaining hypothesis is the structural footprint disjointness hdisj_ex. The collision event
on A_ex's output transfers between the lazy and eager (real) games unconditionally.
Second worked example: the counterexample program q, in syntax #
CounterExamples/IndistinguishableVsGlob.lean shows that the minimal semantic footprint of the
"asymmetric lazy flip" q separates observational indistinguishability from the touched getter.
Here the same program is written syntactically (q_syn — if b then b ←$ ¾-bias else b ←$ fair), and for the region the syntax assigns it — FVP.fvP_proc q_syn — the two notions
provably agree (qsyn_indistinguishable_iff_touched_getter_eq), via the pointwise sandwich:
the region is bounded by bVar's lens region (standard upper-bound assembly) and contains
bVar's conditional-abort tests (a reduced read-slice of the if-condition).
The (trivial) signature of the syntactic q program: no parameters, Unit result.
Instances For
The (trivial) local state of q_syn.
bVar viewed inside the (locals-free) procedure state.
Equations
Instances For
The ¾-biased sample expression (a constant distribution getter).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The fair sample expression (a constant distribution getter).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The body of the syntactic q: if b then b ←$ ¾-bias else b ←$ fair.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The counterexample program, in syntax — its denotation's state action is exactly the
abelian-footprint kernel qKer on the bVar component.
Equations
- GaudisCrypt.Lib.RO.Instantiate.q_syn bVar = { locals := [], body := GaudisCrypt.Lib.RO.Instantiate.bodyQ bVar, return_val := GaudisCrypt.Lib.RO.Instantiate.retQ }
Instances For
(ii) of the sandwich: the syntactic region of q_syn is bounded by bVar's lens region —
every leaf reads/writes bVar (through globalL) or a constant, and the globalL-reduction
of the chained region lands in bVar.footprint.
(i) of the sandwich: bVar's conditional-abort tests live in q_syn's syntactic region.
The x₀-slice of the if-condition read is the chained test (bPS bVar).testKer x₀;
feeding the globalL-reduction a point input on the (trivial) locals and a constant-accept
weight reduces it to the state-level test bVar.testKer x₀, which is therefore a generator
of Lens.reduceFootprint globalL (fvP_stmt bodyQ) ≤ FVP.fvP_proc q_syn.
For the region syntax assigns to the counterexample program, the notions agree:
observational indistinguishability through FVP.fvP_proc q_syn is touched-getter equality.
Instance of the pointwise sandwich — contrast with the minimal semantic footprint of the
same program, where the two notions provably differ
(CounterExamples.exists_indistinguishable_touched_getter_ne).
The concrete form: q_syn's tests see exactly the variable bVar.
glob q_syn = b (EasyCrypt's glob Q = {b}), stated with the touched getter: the
touched getter of the region syntax assigns to q_syn induces the same equivalence on
states as reading the variable bVar — kernel equality of the two getters, which is the
only identification ={glob ·}-style reasoning ever consumes (their codomains differ, so
literal equality is ill-typed). Proved observationally: both sides are the
indistinguishability relation of the region.