Transfer instantiate (theorem 1) #
Lazy/eager distribution equivalence (ProgramDenotation.transfer) for a syntactic adversary:
the
transferBy calculus, Stable/Loc, the body/wrapper lemmas, and the single confinement entry
point ProgramDenotation.transfer_instantiate_of_fvP.
The generic transferBy calculus #
ProgramDenotation.transfer is transferBy convert. We need the same relation
at the ProcedureState level (with convertL), so we use the generic calculus
ProgramDenotation.transferBy from GaudisCrypt.Logic.TransferBy — monad-law
combinators, the Kleene while_loop closure, and the zoom lifting lemma
(convertL = zoom globalL convert, and zoom is a monad morphism, so any
state-level transfer lifts to a zoomed ProcedureState one).
Honest locality + the body induction #
fv_proc is sorry in FV.lean, and a computed footprint for an opaque
getter/setter is genuinely undefinable. The honest, usable locality condition
is semantic: each of the adversary's own operations commutes with convert
(i.e. transfers to itself). Loc A collects exactly these per-leaf facts. The
oracle hole is exempt — it is handled by the hhole hypothesis (later
discharged by the per-query transfer lemma).
p commutes with convertL ("transfers to itself").
Equations
Instances For
Locality: every operation of A outside the oracle interface is Stable.
For a hole, this is the surrounding read (get p) and write (set x) — the
oracle query itself is not required stable (it transfers, lazy↦eager).
Equations
- One or more equations did not get rendered due to their size.
- GaudisCrypt.Lib.RO.Instantiate.Loc GaudisCrypt.StmtWithHoles.skip = True
- GaudisCrypt.Lib.RO.Instantiate.Loc (GaudisCrypt.StmtWithHoles.sample x_1 e) = GaudisCrypt.Lib.RO.Instantiate.Stable (GaudisCrypt.programDenotation (GaudisCrypt.StmtWithHoles.sample x_1 e))
- GaudisCrypt.Lib.RO.Instantiate.Loc (s1.seq s2) = (GaudisCrypt.Lib.RO.Instantiate.Loc s1 ∧ GaudisCrypt.Lib.RO.Instantiate.Loc s2)
- GaudisCrypt.Lib.RO.Instantiate.Loc (GaudisCrypt.StmtWithHoles.while c t) = (GaudisCrypt.Lib.RO.Instantiate.Stable (GaudisCrypt.ProgramDenotation.get c) ∧ GaudisCrypt.Lib.RO.Instantiate.Loc t)
Instances For
The former hard lemma (now proved): transferBy convertL is closed under
while_loop. Instantiates the generic Kleene closure
ProgramDenotation.transferBy_while_loop with c := convertL; the
condition's self-transfer is literally Stable c.
Body induction: an arbitrary syntactic adversary A transfers from its
lazy to its eager instantiation, given locality (Loc) of its own operations
and a per-hole transfer hypothesis (hhole). Generic over the holes so the
induction goes through; specialized to the RO hole below.
Discharge of the oracle hypothesis for RO: the lazy and eager oracle
calls transfer, given the surrounding read/write are stable. This is the
concrete hhole for body_transfer_gen with RO_lazy/RO_eager: the
query itself transfers by ProgramDenotation.transfer_lazy_query (lifted via
transferBy_zoom), and the bridges identify the procedures with the
semantic queries.
Body-level RO transfer — fully assembled (only transferL_while_loop
remains, via body_transfer_gen). For any syntactic adversary body A
that is Local (touches the RO table only through the oracle hole), the
lazy and eager instantiations transfer at the ProcedureState level.
convertL slides in: convert before the wrapper = convertL before the
body, inside the wrapper. Structural (no return-value hypothesis).
ProgramDenotation.get rv reads rv and threads the state through unchanged.
From hret: reading rv commutes with convertL (clean convertL-form).
key: reading rv is invariant under convert changing the table (the global
component of rv_convertL_stable).
convert slides out: convert after the wrapper = convertL after the
body, inside the wrapper. Consumes hret (the return value is RO-disjoint,
so reading it commutes with convert changing the table) via rv_convert_invariant.
Procedure wrapper: a body-level transferBy convertL lifts to a
state-level ProgramDenotation.transfer of the whole procedure denotation, provided
the return value is RO-disjoint. Assembled from procedureDenotation_eq_procWrap,
procWrap_convert_out (uses hret), hbody, and procWrap_convertL_in.
Stable from probabilistic footprint disjointness. A program confined (in the
inFootprint sense) to the complement of the RO table commutes with convertL, i.e. is
Stable. The Footprint analogue of stable_of_inRange_compl; the ᶜ-form makes the
commute_of_disjoint_footprint disjointness hypothesis le_refl, so no complement_range analog
is needed.
Stable from confinement to a footprint disjoint from the RO (probabilistic). The
Footprint analogue of stable_of_confined_lens. No complement_range needed — the
ᶜ-form bound hdisj feeds inFootprint_mono directly.
ConfinedP discharges Loc (theorem-1 locality), leaf by leaf — reusing the existing
Loc→theorems chain. The Footprint analogue of confined_loc.
Theorem 1, end-to-end from footprint disjointness. Lazy/eager indistinguishability for any
adversary whose full footprint fvP_proc A (body + return) is disjoint from the random-oracle
state — fvP_proc A ≤ (roLift _).footprintᶜ — derived from that single bound, with no
per-leaf confinement to check by hand (lens-free, R-free). Inlines the whole
fvP → ConfinedP → Loc → transfer chain — the sole entry point.
Whole-game form: initialisations included, coupling output #
The per-query eager/lazy coupling is pointwise unsatisfiable (a fixed eager table entry cannot
couple with a fresh lazy sample), so theorem 2's h cannot be discharged for the genuine RO pair.
The true lazy = eager statement lives at the whole-game level, where random_oracle_init
supplies the eager table's randomness — and that is exactly theorem 1. The results below convert
theorem 1 into the coupling format (prhl2 with a result-decided post), giving the h-free
end-to-end transfer.
convert is lossless (measure form of convert_mass): from any state its run has total
mass 1.
convert's support only performs a random_oracle_state write: any state projection g
invariant under RO writes is preserved along convert's run. Via the explicit
convert_wp_eq formula — no support analysis of the monadic plumbing needed.
Writes to the RO table do not move glob A, for any A whose footprint avoids the
oracle: under hdisj the write random_oracle_state.set Z is a (fvP_proc A)ᶜ-orbit
step, and the touched getter is constant on (fvP_proc A)ᶜ-orbits.
Theorem 1 at whole-game level: with the initialisations included, the lazy game followed
by a result-preserving convert equals the eager game. Unlike the per-query coupling,
this is unconditionally true from footprint disjointness — the eager table's randomness is
supplied by random_oracle_init = lazy_init; convert.
Game-level output-decided transfer, semantic disjointness form — see
output_win_transfer_games for the user-facing (syntactic-FVP) statement.
Game-level output-decided transfer — the h-free counterpart of output_win_transfer,
for any adversary whose variables avoid the oracle (FVP.fvP_proc A ≤ oracleᶜ, the same
EasyCrypt-style hypothesis as prhl_instantiate_of_glob) and any predicate Win on its
result: the whole games (initialisation included) couple with Win u.1 ↔ Win v.1.
Collision resistance is the instance where Win r reads "r is a collision A
produced". Everything is discharged by theorem 1 (convert-sliding), which owns the eager
table's initialisation randomness — no per-query coupling hypothesis remains.
={glob A} in the postcondition #
glob A := (FVP.fvP_proc A).touched_getter (EasyCrypt's glob A). The whole-game coupling
not only decides the result: the coupled final states also agree on everything A may
touch. The two legs differ by the trailing convert only, convert writes the RO table
only, and — under the footprint disjointness — RO writes are (fvP_proc A)ᶜ-orbit steps,
invisible to glob A.
Whole-game transfer with ={glob A} in the postcondition: from equal initial states,
the lazy and eager games couple with equal results and (glob A)-equal final states.
The glob-enriched form of the coupling behind output_win_transfer_games.
output_win_transfer_games, strengthened with ={glob A}: the games couple with
Win-agreement on the results and (glob A)-equal final states.