Consuming ={glob A}: the whole-game coupling from glob-equal initial states

The produce side (output_glob_transfer_games, TransferInstantiate.lean) starts the lazy and eager games from equal states. This file relaxes the precondition to EasyCrypt's ={glob A} — the initial states need only agree on everything A may touch.

Architecture (chained by prhl2.trans):

G_lazy σ₁  ~[same-program glob rule]~  G_lazy σ₂  ~[produce side, σ₂ = σ₂]~  G_eager σ₂

• PGlob A — the invariant threaded through the body induction: ={glob A} plus equal oracle tables. Glob-equality alone is too weak (the per-query coupling needs equal tables); the tables conjunct is established by lazy_init (lazy_init_coupling_glob) rather than assumed of the initial states.

• glob_self_coupling_lazy — the same-program whole-game rule: from ={glob A}, two runs of the lazy game couple with equal results and ={glob A} finals. Assembled from the init coupling and the oracle-generic body machinery (instantiate_of_fvP_gen at eagerInst := lazyInst := RO_lazy, with the same-side hole wrapper ro_hhole_prhl_lazy).

• output_glob_transfer_games_of_glob — the endpoint: ={glob A} precondition, u.1 = v.1 ∧ ={glob A} postcondition, lazy vs eager.

Both obligations of the original skeleton are discharged, so the endpoint needs only the footprint disjointness hdisj:

• the same-side per-query coupling (lazy_query_self_coupling) — cache hits agree on the shared cached value, cache misses couple the samples diagonally; and

• the glob adversary rule (footprintCompat_PGlob) — every A-confined program self-couples from PGlob-related states, via per-orbit-step map-f couplings (inFootprint_subprob) chained by prhl2.refl/symm/trans (prhl2_self_of_orbit), the reduce/lift bridge (lifted_step_mem_fvP_proc_compl), and per-leg table preservation re-attached through the coupling marginals.

def GaudisCrypt.Lib.RO.Instantiate.PGlob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) : state → state → Prop

The consume-side invariant: agreement on everything A may touch (={glob A}) plus equal oracle tables. The tables conjunct is what makes the per-query self-coupling satisfiable; it is established by the initialisation, not assumed of the initial states.

Equations

• GaudisCrypt.Lib.RO.Instantiate.PGlob A g₁ g₂ = ((GaudisCrypt.FVP.glob A).get g₁ = (GaudisCrypt.FVP.glob A).get g₂ ∧ random_oracle_state.get g₁ = random_oracle_state.get g₂)

The per-query self-coupling

lazy_query applied is a point mass on a cache hit and a uniform sample + table write on a miss. With equal tables the two sides take the same branch: a hit returns the shared cached value; a miss couples the samples diagonally.

theorem GaudisCrypt.Lib.RO.Instantiate.bind_apply {α β : Type} (p : ProgramDenotation state α) (k : α → ProgramDenotation state β) (σ : state) : (p >>= k) σ = do let a ← p σ k a.1 a.2

ProgramDenotation bind, applied: the StateT plumbing, definitionally.

theorem GaudisCrypt.Lib.RO.Instantiate.get_ro_apply (σ : state) : ProgramDenotation.get random_oracle_state σ = pure (random_oracle_state.get σ, σ)

ProgramDenotation.get random_oracle_state, applied: a point mass on the table.

theorem GaudisCrypt.Lib.RO.Instantiate.set_ro_apply (Z : input → Option output) (σ : state) : ProgramDenotation.set random_oracle_state Z σ = pure ((), random_oracle_state.set Z σ)

ProgramDenotation.set random_oracle_state Z, applied: the deterministic write.

theorem GaudisCrypt.Lib.RO.Instantiate.uniform_apply {α : Type} [Fintype α] [Nonempty α] (σ : state) : ProgramDenotation.uniform σ = do let v ← SubProbability.uniform pure (v, σ)

ProgramDenotation.uniform, applied: sample, thread the state (definitional).

theorem GaudisCrypt.Lib.RO.Instantiate.lazy_query_apply_hit (inp : input) {σ : state} {x : output} (h : random_oracle_state.get σ inp = some x) : lazy_query inp σ = pure (x, σ)

lazy_query applied on a cache hit: a point mass, state unchanged.

theorem GaudisCrypt.Lib.RO.Instantiate.lazy_query_apply_miss (inp : input) {σ : state} (h : random_oracle_state.get σ inp = none) : lazy_query inp σ = do let v ← SubProbability.uniform pure (v, random_oracle_state.set (fun (x : input) => if x = inp then some v else random_oracle_state.get σ x) σ)

lazy_query applied on a cache miss: sample uniformly, cache, return.

theorem GaudisCrypt.Lib.RO.Instantiate.lazy_query_self_coupling {P : state → state → Prop} (htab : ∀ (σ₁ σ₂ : state), P σ₁ σ₂ → random_oracle_state.get σ₁ = random_oracle_state.get σ₂) (hset : ∀ (Z : input → Option output) (σ₁ σ₂ : state), P σ₁ σ₂ → P (random_oracle_state.set Z σ₁) (random_oracle_state.set Z σ₂)) (inp : input) : ProgramDenotation.prhl2 P (lazy_query inp) (lazy_query inp) (liftPost P)

Same-side per-query coupling (generic): for any invariant P that implies equal oracle tables and is preserved by equal RO writes, two lazy_querys couple with equal results and P preserved.

theorem GaudisCrypt.Lib.RO.Instantiate.lazy_query_self_coupling_PGlob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) (inp : input) : ProgramDenotation.prhl2 (PGlob A) (lazy_query inp) (lazy_query inp) (liftPost (PGlob A))

The per-query obligation for PGlob A: lazy-vs-lazy queries self-couple — tables are equal by the invariant, glob-agreement survives the write (glob_ro_set_invariant), and the written tables coincide.

theorem GaudisCrypt.Lib.RO.Instantiate.ro_hhole_prhl_lazy {P : state → state → Prop} {l : Type} (h : ∀ (inp : input), ProgramDenotation.prhl2 P (lazy_query inp) (lazy_query inp) (liftPost P)) {sig : ProcedureSignature} (n : HoleIndex roHoles sig) (x : Setter sig.ret (ProcedureState l)) (p : Getter sig.ParamType (ProcedureState l)) (hp : GetOK P p) (hx : ∀ (ret : sig.ret), ProgramDenotation.prhl2 (liftRel P) (ProgramDenotation.set x ret) (ProgramDenotation.set x ret) (liftRelPost P)) : ProgramDenotation.prhl2 (liftRel P) (programDenotation (StmtWithHoles.call x (RO_lazy n) p)) (programDenotation (StmtWithHoles.call x (RO_lazy n) p)) (liftRelPost P)

Same-side analogue of ro_hhole_prhl: the lazy-vs-lazy oracle hole preserves the invariant, given the per-query self-coupling h.

theorem GaudisCrypt.Lib.RO.Instantiate.lazy_init_apply (σ : state) : lazy_init σ = pure ((), random_oracle_state.set (fun (x : input) => none) σ)

lazy_init applied: the deterministic table reset, as a point mass.

theorem GaudisCrypt.Lib.RO.Instantiate.lazy_init_coupling_glob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => (FVP.glob A).get σ₁ = (FVP.glob A).get σ₂) lazy_init lazy_init fun (u v : Unit × state) => PGlob A u.2 v.2

From ={glob A} initial states, the two lazy_inits couple and establish the full invariant: glob-agreement survives the RO write (glob_ro_set_invariant), and both tables are reset to fun _ => none.

The glob adversary rule: FootprintCompat (PGlob A) (fvP_proc A)

An A-confined program self-couples from PGlob-related states. The glob-equality precondition is an orbit fact — the two global states are joined by a zig-zag of (FVP.fvP_proc A)ᶜ-updates (Quotient.exact). Each such update, lifted through globalL (fixing the locals), commutes with everything A may touch as a procedure (lifted_step_mem_fvP_proc_compl, via the reduce/lift algebra), so a confined p maps one leg onto the other pointwise (inFootprint_subprob), giving a per-step coupling; prhl2.refl/symm/trans chain the zig-zag (prhl2_self_of_orbit). The final states remain in a lifted orbit — equal locals and ={glob A} globals (glob_locals_of_lifted_orbit) — while the tables conjunct is re-attached from the per-leg supports (inFootprint_preserves_touched through the coupling marginals).

theorem GaudisCrypt.Lib.RO.Instantiate.prhl2_self_of_orbit {s γ : Type} {F : Footprint s} {p : ProgramDenotation s γ} (hp : p.inFootprint F) (U : Set (Function.End s)) (hU : ∀ f ∈ U, diracKer f ∈ Fᶜ.updates) : ProgramDenotation.prhl2 (Relation.EqvGen fun (a b : s) => ∃ f ∈ U, f a = b) p p fun (u v : γ × s) => u.1 = v.1 ∧ Relation.EqvGen (fun (a b : s) => ∃ f ∈ U, f a = b) u.2 v.2

Self-coupling along an orbit of confined-complement updates. A program confined to F couples with itself across any zig-zag of updates from U ⊆ Fᶜ: each step is mapped through p pointwise (inFootprint_subprob), and prhl2.refl/symm/trans compose the zig-zag. The coupled final states are again U-orbit-related.

def GaudisCrypt.Lib.RO.Instantiate.liftedGlobSteps {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (l : Type) : Set (Function.End (ProcedureState l))

The update set driving the orbit coupling: global (FVP.fvP_proc A)ᶜ-updates lifted through globalL (fixing the locals).

Equations

• One or more equations did not get rendered due to their size.

theorem GaudisCrypt.Lib.RO.Instantiate.lifted_step_mem_fvP_proc_compl {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) {f : Function.End state} (hf : diracKer f ∈ (FVP.fvP_proc A)ᶜ.updates) : diracKer (ProcedureState.globalL.liftFunction f) ∈ (fvP_proc A)ᶜ.updates

The bridge: a global update commuting with everything A may touch globally ((FVP.fvP_proc A)ᶜ), lifted through globalL, commutes with everything A may touch as a procedure ((fvP_proc A)ᶜ). Both fvP_procs decompose (definitionally) into body ⊔ return, with the global one the globalL-reduction of the procedure one; per component the commutation transfers by Footprint.liftSubProbability_comm_reduce_compl.

theorem GaudisCrypt.Lib.RO.Instantiate.lifted_orbit_of_global {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) {l : Type} (loc : l) {g₁ g₂ : state} (h : Relation.EqvGen (fun (a b : state) => ∃ (f : Function.End state), diracKer f ∈ (FVP.fvP_proc A)ᶜ.updates ∧ f a = b) g₁ g₂) : Relation.EqvGen (fun (a b : ProcedureState l) => ∃ fp ∈ liftedGlobSteps A l, fp a = b) { global := g₁, locals := loc } { global := g₂, locals := loc }

Pre-transport: a global (FVP.fvP_proc A)ᶜ-orbit lifts to a liftedGlobSteps orbit of procedure states with any fixed locals.

theorem GaudisCrypt.Lib.RO.Instantiate.glob_locals_of_lifted_orbit {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) {l : Type} {x y : ProcedureState l} (h : Relation.EqvGen (fun (a b : ProcedureState l) => ∃ fp ∈ liftedGlobSteps A l, fp a = b) x y) : (FVP.glob A).get x.global = (FVP.glob A).get y.global ∧ x.locals = y.locals

Post-transport: liftedGlobSteps-orbit-related procedure states have equal locals and ={glob A} globals (each step fixes the locals and is invisible to glob A).

theorem GaudisCrypt.Lib.RO.Instantiate.footprintCompat_PGlob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : FootprintCompat (PGlob A) (fvP_proc A)

The glob adversary rule: every program confined to fvP_proc A self-couples from PGlob A-related states — the last obligation of the consume-side endpoint.

theorem GaudisCrypt.Lib.RO.Instantiate.glob_self_coupling_lazy {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => (FVP.glob A).get σ₁ = (FVP.glob A).get σ₂) (do lazy_init procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) (do lazy_init procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) fun (u v : sig.ret × state) => u.1 = v.1 ∧ (FVP.glob A).get u.2 = (FVP.glob A).get v.2

The same-program whole-game glob rule (lazy side): from ={glob A} initial states, two runs of the lazy game couple with equal results and ={glob A} final states. lazy_init establishes PGlob A; the body preserves it via the oracle-generic machinery at eagerInst := lazyInst := RO_lazy.

theorem GaudisCrypt.Lib.RO.Instantiate.output_glob_transfer_games_of_glob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => (FVP.glob A).get σ₁ = (FVP.glob A).get σ₂) (do lazy_init procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) (do random_oracle_init procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) args) fun (u v : sig.ret × state) => u.1 = v.1 ∧ (FVP.glob A).get u.2 = (FVP.glob A).get v.2

The endpoint — ={glob A} consumed and produced. From initial states that agree on everything A may touch, the lazy and eager whole games couple with equal results and ={glob A} final states. Chains the same-program glob rule (glob_self_coupling_lazy, taking σ₁ to σ₂ on the lazy side) with the produce-side coupling (output_glob_transfer_games, lazy to eager at σ₂) by prhl2.trans.

theorem GaudisCrypt.Lib.RO.Instantiate.output_win_transfer_games_of_glob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (Win : sig.ret → Prop) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : ProgramDenotation.prhl2 (fun (σ₁ σ₂ : state) => (FVP.glob A).get σ₁ = (FVP.glob A).get σ₂) (do lazy_init procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) (do random_oracle_init procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) args) fun (u v : sig.ret × state) => (Win u.1 ↔ Win v.1) ∧ (FVP.glob A).get u.2 = (FVP.glob A).get v.2

Win-form of the endpoint: any event decided by A's output transfers between the lazy and eager games from ={glob A} initial states, with ={glob A} final states.