Phase 4 — Oracle loops parameterised by an adversary

Below, adv and h_adv are parameters (via a variable declaration), not axioms. Every oracle_loop-style definition and adv_conv_eq_conv_adv–oracle_loop_wp_lazy_eq_random_oracle*-style theorem in this section is parameterised over an arbitrary adversary adv : ProgramDenotation state Unit together with its RO-disjointness hypothesis h_adv : adv.inFootprint (random_oracle_state.footprint)ᶜ.

This enables instantiation with wrapped/composed adversaries (CR reductions, hybrid games, etc.) without re-axiomatising or re-deriving the framework.

noncomputable def adv_conv (adv : GaudisCrypt.ProgramDenotation state Unit) : GaudisCrypt.ProgramDenotation state Unit

Equations

• adv_conv adv = do adv convert

noncomputable def conv_adv (adv : GaudisCrypt.ProgramDenotation state Unit) : GaudisCrypt.ProgramDenotation state Unit

Equations

• conv_adv adv = do convert adv

theorem adv_conv_eq_conv_adv (adv : GaudisCrypt.ProgramDenotation state Unit) (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) : adv_conv adv = conv_adv adv

The oracle_loop, loop_body_lazy, and loop_body_eager definitions now live in PlonkLean.RO.OracleLoop alongside oracle_step and oracle_loop_n. The lazy = eager proof for oracle_loop (below) uses them via explicit adv arguments.

theorem ProgramDenotation.transfer_oracle_loop (adv : GaudisCrypt.ProgramDenotation state Unit) (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) : transfer (oracle_loop adv lazy_init lazy_query) (oracle_loop adv random_oracle_init random_oracle_query)

The full oracle_loop transfer: lazy and eager oracle_loops transfer to each other, built via the transfer framework (no Kleene plumbing in this file).

The proof is a ProgramDenotation.transfer_bind chain over the four components of oracle_loop (set want_more, init, while_loop, get adversary_result). The while_loop component is discharged by ProgramDenotation.transfer_while_loop, which contains the Kleene argument in abstract form.

theorem convert_bind_oracle_loop_eager (adv : GaudisCrypt.ProgramDenotation state Unit) : (do convert oracle_loop adv random_oracle_init random_oracle_query) = oracle_loop adv random_oracle_init random_oracle_query

convert is absorbed by the eager oracle_loop. The loop starts with ProgramDenotation.set want_more true >>= random_oracle_init >>= ..., so we push convert past the (RO-disjoint) set want_more true and then absorb it via convert_bind_random_oracle_init_bind.

theorem oracle_loop_lazy_convert_eq_random_oracle_loop (adv : GaudisCrypt.ProgramDenotation state Unit) (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) : (do let b ← oracle_loop adv lazy_init lazy_query convert pure b) = oracle_loop adv random_oracle_init random_oracle_query

The foundational lazy = eager equation for oracle_loop: the lazy loop composed with convert equals the eager loop. Derived from ProgramDenotation.transfer_oracle_loop plus convert-absorption by the eager loop. (This used to be claim_4, proved directly via Kleene in this file; now the Kleene argument lives in ProgramDenotation.transfer_while_loop and this theorem is a corollary.)

theorem oracle_loop_wp_lazy_eq_random_oracle (adv : GaudisCrypt.ProgramDenotation state Unit) (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (F : Bool × state → ENNReal) (hF_inv : ∀ (b : Bool) (σ : state) (x : input → Option output), F (b, random_oracle_state.set x σ) = F (b, σ)) : (oracle_loop adv lazy_init lazy_query).wp F = (oracle_loop adv random_oracle_init random_oracle_query).wp F

wp-level lazy/eager equivalence for oracle_loop: for any postcondition F invariant under writes to random_oracle_state, the wp's of the lazy and eager oracle_loop agree. Specialisation of ProgramDenotation.transfer_wp_ro_invariant to ProgramDenotation.transfer_oracle_loop.

theorem oracle_loop_marginal_lazy_eq_random_oracle (adv : GaudisCrypt.ProgramDenotation state Unit) (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) {β : Type} (h : state → β) (h_inv : ∀ (σ : state) (x : input → Option output), h (random_oracle_state.set x σ) = h σ) (σ₀ : state) : (do let bσ ← oracle_loop adv lazy_init lazy_query σ₀ pure (bσ.1, h bσ.2)) = do let bσ ← oracle_loop adv random_oracle_init random_oracle_query σ₀ pure (bσ.1, h bσ.2)

SubProb-marginal lazy/eager equivalence: for any RO-invariant projection h : state → β, the joint (bit, h σ) distribution agrees under lazy and eager oracle_loop. Specialisation of ProgramDenotation.transfer_marginal_ro_invariant.

theorem oracle_loop_marginal_lazy_eq_random_oracle_compl (adv : GaudisCrypt.ProgramDenotation state Unit) (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (σ₀ : state) : (do let bσ ← oracle_loop adv lazy_init lazy_query σ₀ pure (bσ.1, (GaudisCrypt.Lens.compl random_oracle_state).get bσ.2)) = do let bσ ← oracle_loop adv random_oracle_init random_oracle_query σ₀ pure (bσ.1, (GaudisCrypt.Lens.compl random_oracle_state).get bσ.2)

Form (a) — lens-complement projection. The joint distribution of (adv's bit, the entire non-RO part of state) agrees under lazy and eager. Specialisation via random_oracle_state.compl.get.