FullEager: the lazy = eager theorem, PROM-style

An independent, EasyCrypt-style derivation of the whole-game lazy = eager coupling, after the FullEager subtheory of EasyCrypt's PROM.ec. The headline is a chain of pRHL judgments in the eager calculus (GaudisCrypt.Logic.EagerRhl / EagerProc):

PROM.ec (FullEager)	here
resample (Iter over Unknown)	convert (one uniform function draw)
eager_init, eager_get (eager rnd)	eager_init, eager_query (native)
eager_D (eager proc on abstract D)	eager_D (via the eager_call rule)
D <: FRO_Distinguisher {-FRO}	hdisj : FVP.fvP_proc A ≤ (RO.footprint)ᶜ
RO_LRO : ={glob D} ==> ={res, glob D}	RO_LRO_glob

Dependency policy. The per-operation eager lemmas are proven natively on the concrete RO programs — applied-form computations plus the resampling bijection uniform_bind_update (the eager rnd content). The derivation imports no transfer_* claims and neither of the transfer-side body inductions; the only adversary-crossing step is the calculus rule eager_call (Logic/EagerProc.lean), whose soundness is the once-and-for-all induction — the analogue of EasyCrypt's trusted eager proc. The allowed substrate is the footprint/confinement layer (the module-system analogue of {-FRO}), the applied-form helpers, and the invariant machinery of GlobTransfer.lean (all coupling-native), used for the ={glob A} precondition step exactly where EC's kernel threads ={glob D}.

Applied forms of the RO primitives

theorem GaudisCrypt.Lib.RO.Instantiate.random_oracle_query_apply (inp : input) (σ : state) : random_oracle_query inp σ = pure ((random_oracle_state.get σ inp).getD default, σ)

random_oracle_query applied: a deterministic table read.

theorem GaudisCrypt.Lib.RO.Instantiate.convert_apply (σ : state) : convert σ = do let y ← SubProbability.uniform pure ((), random_oracle_state.set (fun (x : input) => some ((random_oracle_state.get σ x).getD (y x))) σ)

convert applied: one uniform draw filling the table's holes.

theorem GaudisCrypt.Lib.RO.Instantiate.random_oracle_init_apply (σ : state) : random_oracle_init σ = do let h ← SubProbability.uniform pure ((), random_oracle_state.set (fun (x : input) => some (h x)) σ)

random_oracle_init applied: one uniform draw of the full table.

Uniform-sampling algebra (the eager rnd substance)

theorem GaudisCrypt.Lib.RO.Instantiate.uniform_mass {α : Type} [Fintype α] [Nonempty α] : ↑SubProbability.uniform Set.univ = 1

The uniform sub-probability is a probability.

theorem GaudisCrypt.Lib.RO.Instantiate.SubProbability.bind_const {α β : Type} (ν : SubProbability α) (hν : ↑ν Set.univ = 1) (m : SubProbability β) : (do let _ ← ν m) = m

A lossless sampling whose value is ignored collapses.

theorem GaudisCrypt.Lib.RO.Instantiate.uniform_bind_update (inp : input) : (do let v ← SubProbability.uniform let y ← SubProbability.uniform pure (Function.update y inp v)) = SubProbability.uniform

Resampling one coordinate of a uniform function is uniform — the bijection behind EasyCrypt's eager rnd: drawing v uniformly and overwriting a uniformly drawn y at inp is a uniform draw.

Per-operation eager lemmas (PROM's eager_init, eager_get)

theorem GaudisCrypt.Lib.RO.Instantiate.eager_init : convert.eagerR convert (fun (σ₁ σ₂ : state) => σ₁ = σ₂) random_oracle_init lazy_init fun (u v : Unit × state) => u = v

Eager init (native): convert; random_oracle_init ~ lazy_init; convert — both sides are "sample a full fresh table over σ".

theorem GaudisCrypt.Lib.RO.Instantiate.eager_query (x : input) : convert.eagerR convert (fun (σ₁ σ₂ : state) => σ₁ = σ₂) (random_oracle_query x) (lazy_query x) fun (u v : output × state) => u = v

Eager query (native): convert; random_oracle_query x ~ lazy_query x; convert. Cache hit: both sides read the shared cached value around the same fill. Cache miss: the fresh lazy sample and the fill coordinate are exchanged by the resampling bijection (uniform_bind_update).

Kernel instantiation (PROM's eager_D)

theorem GaudisCrypt.Lib.RO.Instantiate.swapLoc_of_loc {holes : HoleSigs} {l : Type} (A : StmtWithHoles holes l) : Loc A → SwapLoc (ProgramDenotation.zoom ProcedureState.globalL convert) A

Loc (the footprint-discharged locality) is swap-locality for the lifted convert block.

theorem GaudisCrypt.Lib.RO.Instantiate.eager_query_spec (args : roSig.ParamType) : convert.eagerR convert (fun (σ₁ σ₂ : state) => σ₁ = σ₂) (procedureDenotation RO_eager_proc args) (procedureDenotation RO_lazy_proc args) fun (u v : roSig.ret × state) => u = v

The oracle's procedure-level eager specification (PROM's eager_get in procedure form): the native eager_query through the denotation bridges — the input to the eager call rule.

theorem GaudisCrypt.Lib.RO.Instantiate.eager_D {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : convert.eagerR convert (fun (σ₁ σ₂ : state) => σ₁ = σ₂) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) args) (procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_lazy) args) fun (u v : sig.ret × state) => u = v

eager_D: the abstract adversary is eager for the resampler, from footprint disjointness alone — one application of the eager_call rule, with the per-hole case discharged by the native eager_query.

theorem GaudisCrypt.Lib.RO.Instantiate.convert_glob_self {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 σ₂) convert convert fun (u v : Unit × state) => (FVP.glob A).get u.2 = (FVP.glob A).get v.2

convert self-couples from ={glob A} states, preserving ={glob A}: the samples couple diagonally and the fills differ only inside the oracle region (native; EC's s ~ s : I ==> I framing condition).

theorem GaudisCrypt.Lib.RO.Instantiate.eager_D_glob {sig : ProcedureSignature} (A : ProcedureWithHoles roHoles sig) (args : sig.ParamType) (hdisj : FVP.fvP_proc A ≤ (Lens.footprint random_oracle_state)ᶜ) : convert.eagerR convert (fun (σ₁ σ₂ : state) => (FVP.glob A).get σ₁ = (FVP.glob A).get σ₂) (do random_oracle_init procedureDenotation (A.instantiate fun {sig : ProcedureSignature} => RO_eager) 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 whole-game invariant eager judgment — EC's eager_D in its native shape ={glob D} ==> ={res, glob D}: the two games swap with the resampler from ={glob A} initial states, with equal results and ={glob A} finals. One eagerR_of_self_right: the equality-level judgment (eagerR_seq eager_init eager_D) glued to the framing self-coupling of the lazy composite (glob_self_coupling_lazy extended by convert_glob_self).

theorem GaudisCrypt.Lib.RO.Instantiate.convert_init_absorb {α : Type} (rest : ProgramDenotation state α) : (do convert random_oracle_init rest) = do random_oracle_init rest

The resampler is swallowed by the eager initialisation (native).

The headline (PROM's RO_LRO)

theorem GaudisCrypt.Lib.RO.Instantiate.RO_LRO_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

RO_LRO with ={glob A}: the whole lazy and eager games couple from ={glob A} initial states with equal results and ={glob A} final states — a chain of pRHL judgments:

1. the whole-game eager judgment: eagerR_seq eager_init eager_D;
2. the leading resampler is swallowed by the eager initialisation (convert_init_absorb);
3. the trailing resampler is absorbed into a coupling over the ={glob A} self-coupling base (prhl2_of_lossless_tail_proj_inv) — the invariant threading EC's kernel performs inside eager proc, cf. the judgment-level form eager_D_glob.

theorem GaudisCrypt.Lib.RO.Instantiate.RO_LRO_win {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 RO_LRO_glob: any event decided by A's output transfers between the lazy and eager games, with ={glob A} throughout.