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
Lens.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 first answer local r_a.
Equations
Instances For
The second answer local r_b.
Equations
Instances For
The return getter: read back the pair of observed answers (r_a, r_b).
Equations
Instances For
The global variable advG viewed inside the program 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 locals, and the input parameters — is a lens
disjoint from roLift = globalL.chain random_oracle_state (advG by hypothesis instDisj, the
locals/params through the localL/globalL split). So the whole syntactic footprint lands in
(roLift.footprint)ᶜ; reducing through globalL (reduce_le_compl_of_chain) then lands it in
(random_oracle_state.footprint)ᶜ.
The global adversary lens advGL is disjoint from the oracle-table lens roLift.
A lens read's footprint (raw or assign-wrapped) lands in (roLift.footprint)ᶜ.
A raw lens read lands in (roLift.footprint)ᶜ.
A lens write's family footprint lands in (roLift.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.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
bVar viewed inside the program state.
Equations
Instances For
The ¾-biased sample expression (a constant distribution getter).
Equations
Instances For
The fair sample expression (a constant distribution getter).
Equations
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 (trivial) return value of q_syn.
Equations
- GaudisCrypt.Lib.RO.Instantiate.retQ = { get := fun (x : GaudisCrypt.ProgramState) => () }
Instances For
The counterexample program, in syntax — its denotation's state action is exactly the
abelian-footprint kernel qKer on the bVar component.
Equations
- One or more equations did not get rendered due to their size.
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.