RO coupling equivalence (subtask-3, theorem 2)

Lazy ≈ eager random oracle as a relational statement (ProgramDenotation.prhl2, i.e. a coupling): for a syntactic adversary A, instantiating A against the eager oracle and against the lazy oracle yields couplable executions preserving any state invariant P. The companion TransferInstantiate proves the distributional version (theorem 1) via transfer; this file is the coupling version.

The development has three layers:

• Lifting (liftRel/liftRelPost/GetOK/LocP): lift the state invariant P to procedure states (P on globals, equal locals) and state the per-statement honest-locality predicate.
• The coupling (body_prhl2_gen → ro_hhole_prhl → prhl_wrapper): the body induction in prhl2, the RO-hole coupling, and the procedure wrapper, assembled into the main theorem.
• Confinement endpoints (FootprintCompat → confinedP_locP → prhl_instantiate_of_fvP): discharge LocP from the adversary's footprint lying in a FootprintCompat region (lens-free). The EasyCrypt-style entry point is prhl_instantiate_of_glob, whose adversary hypothesis is just footprint disjointness from the oracle (FVP.fvP_proc A ≤ (random_oracle_state.footprint)ᶜ).

def GaudisCrypt.Lib.RO.Instantiate.liftPost {α : Type} (P : state → state → Prop) : α × state → α × state → Prop

Lift a state relation P to a post-relation on (result, state) pairs: require equal results and P on the states.

Equations

• GaudisCrypt.Lib.RO.Instantiate.liftPost P u v = (u.1 = v.1 ∧ P u.2 v.2)

Theorem 2 scaffolding: relational invariant preservation

Subtask-3 theorem 2 is the coupling/prhl2 analogue of theorem 1. We lift the state invariant P to procedure states (P on globals, equal locals), give an honest locality predicate LocP (each of the adversary's own operations preserves the invariant relationally — its guards return equal booleans and its updates preserve the relation), and prove the body induction body_prhl2_gen in prhl2 (the richer relational calculus).

def GaudisCrypt.Lib.RO.Instantiate.liftRel {l : Type} (P : state → state → Prop) : ProcedureState l → ProcedureState l → Prop

Lift P (on the global RO state) to a relation on procedure states: P on the globals, identical locals (the adversary's local computation is the same on the eager and lazy sides).

Equations

• GaudisCrypt.Lib.RO.Instantiate.liftRel P ps₁ ps₂ = (P ps₁.global ps₂.global ∧ ps₁.locals = ps₂.locals)

def GaudisCrypt.Lib.RO.Instantiate.liftRelPost {l α : Type} (P : state → state → Prop) : α × ProcedureState l → α × ProcedureState l → Prop

Post-relation on (result, procedure state): equal results, liftRel P on states.

Equations

• GaudisCrypt.Lib.RO.Instantiate.liftRelPost P u v = (u.1 = v.1 ∧ GaudisCrypt.Lib.RO.Instantiate.liftRel P u.2 v.2)

def GaudisCrypt.Lib.RO.Instantiate.GetOK {γ l : Type} (P : state → state → Prop) (g : Getter γ (ProcedureState l)) : Prop

Read coupling: a getter returns equal values and preserves liftRel P. Used both for Bool guards (if/while) and the oracle's params getter.

Equations

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

def GaudisCrypt.Lib.RO.Instantiate.LocP {holes : HoleSigs} {l : Type} (P : state → state → Prop) : StmtWithHoles holes l → Prop

Honest locality for theorem 2: every operation of A outside the oracle preserves the invariant relationally (self-couples under liftRel P). The oracle hole is exempt (handled by the per-query hypothesis).

Equations

• One or more equations did not get rendered due to their size.
• GaudisCrypt.Lib.RO.Instantiate.LocP P GaudisCrypt.StmtWithHoles.skip = True
• GaudisCrypt.Lib.RO.Instantiate.LocP P (s1.seq s2) = (GaudisCrypt.Lib.RO.Instantiate.LocP P s1 ∧ GaudisCrypt.Lib.RO.Instantiate.LocP P s2)
• GaudisCrypt.Lib.RO.Instantiate.LocP P (GaudisCrypt.StmtWithHoles.while c t) = (GaudisCrypt.Lib.RO.Instantiate.GetOK P c ∧ GaudisCrypt.Lib.RO.Instantiate.LocP P t)

def GaudisCrypt.Lib.RO.Instantiate.FootprintCompat {l : Type} (P : state → state → Prop) (R : Footprint (ProcedureState l)) : Prop

Footprint-level compatibility with liftRel P (lens-free). A region R is P-compatible when every program confined to R self-couples under liftRel P. This is exactly what confinedP_locP consumes — it never inspects a lens, only inFootprint R. Discharged for the oracle-complement region by footprintCompat_of_glob (the glob/HasReset route).

Equations

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

Layer 2 — the coupling

theorem GaudisCrypt.Lib.RO.Instantiate.body_prhl2_gen {P : state → state → Prop} {holes : HoleSigs} {l : Type} (A : StmtWithHoles holes l) (eagerInst lazyInst : holes.Instantiation) : LocP P A → (∀ {sig : ProcedureSignature} (n : HoleIndex holes sig) (x : Setter sig.ret (ProcedureState l)) (p : Getter sig.ParamType (ProcedureState l)), GetOK P p → (∀ (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 (eagerInst n) p)) (programDenotation (StmtWithHoles.call x (lazyInst n) p)) (liftRelPost P)) → ProgramDenotation.prhl2 (liftRel P) (programDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst)) (programDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst)) (liftRelPost P)

Body induction: an arbitrary adversary body A preserves the lifted invariant relationally, given LocP and a per-hole coupling hhole (the oracle preserves the invariant). Threads the prhl2 composition rules (bind/cond/while_loop) over the statement structure.

theorem GaudisCrypt.Lib.RO.Instantiate.prhl2_zoom {P : state → state → Prop} (l : Type) {γ : Type} {c d : ProgramDenotation state γ} {B : γ × state → γ × state → Prop} (hcd : ProgramDenotation.prhl2 P c d B) : ProgramDenotation.prhl2 (liftRel P) (ProgramDenotation.zoom ProcedureState.globalL c) (ProgramDenotation.zoom ProcedureState.globalL d) fun (u v : γ × ProcedureState l) => B (u.1, u.2.global) (v.1, v.2.global) ∧ u.2.locals = v.2.locals

Coupling lift through zoom globalL (the prhl2 analogue of transferBy_zoom): a state-level coupling of c, d under P lifts to a ProcedureState coupling of their zooms under liftRel P, threading the (equal) locals. Used to lift the per-query hypothesis h to the oracle hole.

theorem GaudisCrypt.Lib.RO.Instantiate.ro_hhole_prhl {P : state → state → Prop} {l : Type} (h : ∀ (inp : input), ProgramDenotation.prhl2 P (random_oracle_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_eager n) p)) (programDenotation (StmtWithHoles.call x (RO_lazy n) p)) (liftRelPost P)

RO hole coupling: the eager/lazy oracle calls couple under liftRel P, given the surrounding read/write are liftRel-preserving. The query couples via prhl2_zoom of the per-query hypothesis h (with the bridges identifying the procedures with the semantic queries). This is body_prhl2_gen's hhole for the RO instantiation.

theorem GaudisCrypt.Lib.RO.Instantiate.prhl_instantiate_body {P : state → state → Prop} {l : Type} (h : ∀ (inp : input), ProgramDenotation.prhl2 P (random_oracle_query inp) (lazy_query inp) (liftPost P)) (A : StmtWithHoles roHoles l) (hloc : LocP P A) : ProgramDenotation.prhl2 (liftRel P) (programDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager)) (programDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy)) (liftRelPost P)

Body-level theorem 2 — fully assembled: an arbitrary Local adversary body preserves the invariant relationally, with the RO oracle. Combines body_prhl2_gen with the RO hole coupling ro_hhole_prhl.

theorem GaudisCrypt.Lib.RO.Instantiate.prhl_wrapper_gen {P : state → state → Prop} {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (hbody : ProgramDenotation.prhl2 (liftRel P) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => eagerInst)) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => lazyInst)) (liftRelPost P)) (hret : ∀ (ps₁ ps₂ : ProcedureState (sig.LocalVariableState A.locals)), liftRel P ps₁ ps₂ → A.return_val.get ps₁ = A.return_val.get ps₂) : ProgramDenotation.prhl2 P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst) args) (liftPost P)

Oracle-agnostic procedure wrapper for prhl2 (the generalization of prhl_wrapper): a body-level prhl2 coupling of A's body under two arbitrary hole-instantiations eagerInst/lazyInst lifts to a state-level prhl2 coupling of the whole procedure, given the return value is determined by the invariant. The proof never inspects the instantiations (only uses them via A.instantiate/procedureDenotation), so RO_eager/RO_lazy were incidental.

theorem GaudisCrypt.Lib.RO.Instantiate.prhl_wrapper {P : state → state → Prop} {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hbody : ProgramDenotation.prhl2 (liftRel P) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => RO_eager)) (programDenotation (A.body.instantiate fun {sig : ProcedureSignature} => RO_lazy)) (liftRelPost P)) (hret : ∀ (ps₁ ps₂ : ProcedureState (sig.LocalVariableState A.locals)), liftRel P ps₁ ps₂ → A.return_val.get ps₁ = A.return_val.get ps₂) : ProgramDenotation.prhl2 P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) (liftPost P)

Procedure wrapper for prhl2 (isolated, analogue of transfer_wrapper): a body-level prhl2 coupling lifts to a state-level prhl2 coupling of the whole procedure, given the return value is determined by the invariant. The RO instantiation of the oracle-agnostic prhl_wrapper_gen.

Layer 3 — confinement endpoints (discharge LocP from a footprint)

theorem GaudisCrypt.Lib.RO.Instantiate.inFootprint_preserves_touched {s a : Type} {R S : Footprint s} {p : ProgramDenotation s a} (hp : p.inFootprint R) (hSc : S ≤ Rᶜ) {σ : s} (hS : S.HasReset σ) : (p σ).satisfies fun (xs : a × s) => S.touched_getter.get xs.2 = S.touched_getter.get σ

Confinement preserves a disjoint footprint's content (the lens-free frame linchpin). A program confined to R leaves unchanged the content (S.touched_getter) of any resettable footprint S disjoint from R (S ≤ Rᶜ). Idempotent-fixpoint argument (no orbit collapse): S.HasReset's overwrite is an Rᶜ-update fixing σ that collapses S.touched_getter to σ's value, so by inFootprint_subprob p σ is a fixpoint of pushing it. For S = roLift.footprint (a lens), Lens.footprint_hasReset discharges S.HasReset, so the frame needs only footprint disjointness S ≤ Rᶜ.

theorem GaudisCrypt.Lib.RO.Instantiate.FootprintCompat.mono {P : state → state → Prop} {l : Type} {R R' : Footprint (ProcedureState l)} (h : FootprintCompat P R) (hle : R' ≤ R) : FootprintCompat P R'

FootprintCompat is antitone: a smaller footprint is still P-compatible. Lets us prove compatibility once for a large "nice" region (e.g. Oᶜ, the oracle-complement) and transport it down to any confined adversary fvP_proc A ≤ Oᶜ (disjoint from the oracle).

theorem GaudisCrypt.Lib.RO.Instantiate.footprintCompat_of_glob {P : state → state → Prop} {l : Type} {R O : Footprint (ProcedureState l)} (hOc : O ≤ Rᶜ) (hO : ∀ (σ : ProcedureState l), O.HasReset σ) (hrefine : ∀ (a b : ProcedureState l), liftRel P a b → R.touched_getter.get a = R.touched_getter.get b) (hstable : ∀ (a b u v : ProcedureState l), liftRel P a b → R.touched_getter.get u = R.touched_getter.get v → O.touched_getter.get u = O.touched_getter.get a → O.touched_getter.get v = O.touched_getter.get b → liftRel P u v) : FootprintCompat P R

Glob-based FootprintCompat (lens-free, Q-free, disjointness form). Reduce FootprintCompat P R to two intrinsic properties of liftRel P over the split into the touched content R.touched_getter and a resettable oracle region O disjoint from R (O ≤ Rᶜ, O.HasReset):

• hrefine — liftRel P refines ={glob A}: the touched content R.touched_getter is equal.
• hstable — liftRel P is frame-stable on the oracle: it depends only on O's content, so overwriting the touched content on both sides (keeping O.touched_getter fixed) preserves it.

Each confined program self-couples via prhl2_glob (touched stays equal) and inFootprint_preserves_touched (the oracle content stays fixed, from O.HasReset + O ≤ Rᶜ), then hstable rebuilds liftRel P. No Lens, no orbit collapse, no frame predicate.

theorem GaudisCrypt.Lib.RO.Instantiate.confinedP_locP {P : state → state → Prop} {holes : HoleSigs} {l : Type} (R : Footprint (ProcedureState l)) (hR : FootprintCompat P R) (hc : ∀ {sig : ProcedureSignature} (a : HoleIndex holes sig), Countable sig.ParamType) (A : StmtWithHoles holes l) : ConfinedP R A → LocP P A

ConfinedP discharges LocP (theorem-2 locality) for any invariant P — the Footprint analogue of confined_locP.

theorem GaudisCrypt.Lib.RO.Instantiate.reads_equal_of_footprintCompat {P : state → state → Prop} {l γ : Type} {R : Footprint (ProcedureState l)} (hR : FootprintCompat P R) {g : Getter γ (ProcedureState l)} (hg : (ProgramDenotation.get g).inFootprint R) {ps₁ ps₂ : ProcedureState l} (hpre : liftRel P ps₁ ps₂) : g.get ps₁ = g.get ps₂

A getter confined to a FootprintCompat region reads equal values from liftRel P-related states — the return-value condition prhl_wrapper needs, now derived from the footprint bound rather than assumed. A deterministic get/get self-coupling has both marginals point masses, so its (a.e.) post x.1.1 = x.2.1 pins the two reads together. Replaces the standalone hret.

theorem GaudisCrypt.Lib.RO.Instantiate.instantiate_of_fvP_gen {P : state → state → Prop} {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (hcompat : FootprintCompat P (fvP_proc A)) (hc : ∀ {sig' : ProcedureSignature} (a : HoleIndex holes sig'), Countable sig'.ParamType) (hhole : ∀ {sig' : ProcedureSignature} (n : HoleIndex holes sig') (x : Setter sig'.ret (ProcedureState (sig.LocalVariableState A.locals))) (p : Getter sig'.ParamType (ProcedureState (sig.LocalVariableState A.locals))), GetOK P p → (∀ (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 (eagerInst n) p)) (programDenotation (StmtWithHoles.call x (lazyInst n) p)) (liftRelPost P)) : ProgramDenotation.prhl2 P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst) args) (liftPost P)

Oracle-agnostic footprint endpoint (the generalization of prhl_instantiate_of_fvP). Relational (coupling) A[eager] ≈ A[lazy] for an invariant P under two arbitrary hole-instantiations eagerInst/lazyInst, given (1) A's own footprint fvP_proc A is P-compatible (FootprintCompat P (fvP_proc A)) and (2) a per-hole coupling hhole (the oracle call preserves the invariant). Nothing about the specific oracle enters: this inlines the fvP → ConfinedP → LocP → coupling → prhl2 chain with RO_eager/RO_lazy replaced by the given instantiations and ro_hhole_prhl replaced by hhole.

theorem GaudisCrypt.Lib.RO.Instantiate.instantiate_of_glob_gen {P : state → state → Prop} {holes : HoleSigs} {sig : ProcedureSignature} (eagerInst lazyInst : holes.Instantiation) (A : ProcedureWithHoles holes sig) (args : sig.ParamType) (O : Footprint (ProcedureState (sig.LocalVariableState A.locals))) (hO : ∀ (σ : ProcedureState (sig.LocalVariableState A.locals)), O.HasReset σ) (hdisj : fvP_proc A ≤ Oᶜ) (hrefine : ∀ (a b : ProcedureState (sig.LocalVariableState A.locals)), liftRel P a b → Oᶜ.touched_getter.get a = Oᶜ.touched_getter.get b) (hstable : ∀ (a b u v : ProcedureState (sig.LocalVariableState A.locals)), liftRel P a b → Oᶜ.touched_getter.get u = Oᶜ.touched_getter.get v → O.touched_getter.get u = O.touched_getter.get a → O.touched_getter.get v = O.touched_getter.get b → liftRel P u v) (hc : ∀ {sig' : ProcedureSignature} (a : HoleIndex holes sig'), Countable sig'.ParamType) (hhole : ∀ {sig' : ProcedureSignature} (n : HoleIndex holes sig') (x : Setter sig'.ret (ProcedureState (sig.LocalVariableState A.locals))) (p : Getter sig'.ParamType (ProcedureState (sig.LocalVariableState A.locals))), GetOK P p → (∀ (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 (eagerInst n) p)) (programDenotation (StmtWithHoles.call x (lazyInst n) p)) (liftRelPost P)) : ProgramDenotation.prhl2 P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => eagerInst) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => lazyInst) args) (liftPost P)

Oracle-agnostic glob endpoint — the oracle-agnostic core of prhl_instantiate_of_glob. Relational (coupling) A[eager] ≈ A[lazy] for an invariant P under two arbitrary hole-instantiations eagerInst/lazyInst, from a footprint-disjointness hypothesis against an arbitrary resettable oracle region O (hdisj : fvP_proc A ≤ Oᶜ) plus the glob-split conditions (hrefine/hstable) on liftRel P over the split into the outside-O content (Oᶜ.touched_getter) and O's content (O.touched_getter), a countability plumbing hc, and a per-hole coupling hhole.

Instantiate with (RO_eager, RO_lazy, roLift.footprint, ro_hhole_prhl h) for the random oracle (this is exactly how prhl_instantiate_of_glob is derived). A random-permutation oracle would be another instantiation: it supplies its own two hole-instantiations, its permutation-table region as O, and its collision-avoiding per-hole coupling as hhole. The middle (footprintCompat_of_glob + FootprintCompat.mono + wrapper + body induction) is oracle-agnostic and lives here; the caller supplies only the oracle-specific ingredients.

theorem GaudisCrypt.Lib.RO.Instantiate.prhl_instantiate_of_fvP {P : state → state → Prop} {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hcompat : FootprintCompat P (fvP_proc A)) (h : ∀ (inp : input), ProgramDenotation.prhl2 P (random_oracle_query inp) (lazy_query inp) (liftPost P)) : ProgramDenotation.prhl2 P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) (liftPost P)

Theorem 2 — the entry point. Relational (coupling) lazy ≈ eager equivalence for an invariant P, for any adversary whose own footprint fvP_proc A (body + return) is P-compatible (FootprintCompat P (fvP_proc A)). This is the weakest such hypothesis — only A's actual footprint need be compatible, not a larger region — and it subsumes the explicit RO-disjointness premise (for the canonical RO-agreement P, FootprintCompat P (fvP_proc A) is "A is disjoint from the random oracle"). Lens-free, R-free; the RO instantiation of the oracle-agnostic instantiate_of_fvP_gen.

theorem GaudisCrypt.Lib.RO.Instantiate.roLift_get_global {l : Type} (x : ProcedureState l) : (roLift l).get x = random_oracle_state.get x.global

The oracle content of a procedure state is the oracle table of its global: roLift reads through globalL into random_oracle_state.

theorem GaudisCrypt.Lib.RO.Instantiate.roLift_compl_get_iff {l : Type} (x y : ProcedureState l) : (roLift l).compl.get x = (roLift l).compl.get y ↔ x.locals = y.locals ∧ (Lens.compl random_oracle_state).get x.global = (Lens.compl random_oracle_state).get y.global

The oracle-complement of a procedure state splits into locals + non-oracle global. Two states have equal outside-oracle content ((roLift l).compl.get) iff their locals agree and their globals agree away from the oracle (random_oracle_state.compl.get). This is what lets the endpoint phrase its premises purely on the global invariant P (on state), with the locals handled structurally by the framework.

theorem GaudisCrypt.Lib.RO.Instantiate.prhl_instantiate_of_glob {P : state → state → Prop} {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) (hrefine : ∀ (g₁ g₂ : state), P g₁ g₂ → (Lens.compl random_oracle_state).get g₁ = (Lens.compl random_oracle_state).get g₂) (hstable : ∀ (g₁ g₂ g₁' g₂' : state), P g₁ g₂ → (Lens.compl random_oracle_state).get g₁' = (Lens.compl random_oracle_state).get g₂' → random_oracle_state.get g₁' = random_oracle_state.get g₁ → random_oracle_state.get g₂' = random_oracle_state.get g₂ → P g₁' g₂') (h : ∀ (inp : input), ProgramDenotation.prhl2 P (random_oracle_query inp) (lazy_query inp) (liftPost P)) : ProgramDenotation.prhl2 P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) (liftPost P)

Theorem 2 via glob (the EasyCrypt-style endpoint, disjointness form, global invariant). Relational lazy ≈ eager for any adversary A whose footprint is disjoint from the random oracle (hdisj : fvP_proc A ≤ (roLift _).footprintᶜ), from two conditions on the global invariant P (on state) — no locals, phrased entirely via random_oracle_state:

• hrefine — P forces agreement on the non-oracle globals (random_oracle_state.compl), and
• hstable — P is determined by the oracle table (random_oracle_state): overwriting the non-oracle globals on both sides (keeping each side's table) preserves it.

Locals never appear: liftRel's locals-equality is carried structurally by prhl2_glob (A runs identically), which is also why locals must not enter a condition that has to survive descent into call' (a callee's locals differ). Internally footprintCompat_of_glob runs at R = (roLift _).footprintᶜ (resettability discharged by Lens.footprint_hasReset); the global P-conditions are lifted to procedure states via roLift_compl_get_iff/roLift_get_global and FootprintCompat.mono transports the result down to fvP_proc A via hdisj.

theorem GaudisCrypt.Lib.RO.Instantiate.output_win_transfer {P : state → state → Prop} {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (Win : sig.ret → Prop) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) (hrefine : ∀ (g₁ g₂ : state), P g₁ g₂ → (Lens.compl random_oracle_state).get g₁ = (Lens.compl random_oracle_state).get g₂) (hstable : ∀ (g₁ g₂ g₁' g₂' : state), P g₁ g₂ → (Lens.compl random_oracle_state).get g₁' = (Lens.compl random_oracle_state).get g₂' → random_oracle_state.get g₁' = random_oracle_state.get g₁ → random_oracle_state.get g₂' = random_oracle_state.get g₂ → P g₁' g₂') (h : ∀ (inp : input), ProgramDenotation.prhl2 P (random_oracle_query inp) (lazy_query inp) (liftPost P)) : ProgramDenotation.prhl2 P (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) fun (u v : sig.ret × state) => Win u.1 ↔ Win v.1

Output-decided game transfer for an abstract adversary (the collision-resistance shape). For any adversary A disjoint from the oracle and any predicate Win on its result, the eager and lazy instantiations couple so the win event coincides: A wins against the eager (real) oracle iff against the lazy one. Immediate from prhl_instantiate_of_glob, which equates the two results (u.1 = v.1) — so any event decided by A's output transfers, regardless of the full oracle table. Collision resistance is the instance where Win r reads "r is a collision A produced" (e.g. two distinct queried inputs whose observed answers are equal).