Lazy/eager transfer

This file is the bridge between the lazy and eager random oracles.

• convert — the operation that fills in undefined RO entries with a fresh uniform function. It's the program-level witness that lazy and eager are interchangeable.

• Convert algebra: how convert interacts with wp, with set/get on disjoint variables, and with random_oracle_init. Includes the claim_* family of foundational lazy/eager equations (lazy_init_convert_eq_random_oracle_init, lazy_query_convert_eq_convert_random_oracle_query, etc.).

• ProgramDenotation.transfer — the lazy/eager transfer relation, transferBy convert (see GaudisCrypt.Logic.TransferBy for the generic calculus). The closure laws (bind, while_loop, reflexivity on RO-disjoint programs) and the commutation/continuation forms are all instances of the generic transferBy_* lemmas; only the base cases (transfer_lazy_init, transfer_lazy_query) are proved here.

• wp/marginal bridges — ProgramDenotation.transfer_value_marginal and the enriched RO-invariant variants (transfer_wp_ro_invariant, transfer_marginal_ro_invariant), instantiating the generic transferBy bridges with convert_mass / RO-invariance.

Convert

noncomputable def convert : GaudisCrypt.ProgramDenotation state Unit

Fill in undefined entries of the random oracle with a fresh uniform function. The bridge between lazy and eager: applied to a lazy state, convert produces the same distribution as an eager state.

Equations

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

theorem convert_inFootprint_ro : convert.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)

convert only reads and writes random_oracle_state (probabilistic footprint form; drives the countability-free transfer-reflexivity).

Convert algebra

theorem convert_mass (σ : state) : convert.wp (fun (x : Unit × state) => 1) σ = 1

convert is a probability measure: its total mass is 1. All pieces (get, uniform, set) preserve mass.

theorem convert_wp_eq (f : GaudisCrypt.ProgramDenotation.Post state Unit) (s : state) : convert.wp f s = ∑ y : input → output, f ((), random_oracle_state.set (fun (x : input) => some ((random_oracle_state.get s x).getD (y x))) s) / ↑(Fintype.card (input → output))

Explicit convert.wp formula derived from the definition.

Foundational lazy/eager equations (the claim_* family)

theorem lazy_init_convert_eq_random_oracle_init : (do lazy_init convert) = random_oracle_init

lazy_init then convert = random_oracle_init. The eager initialisation is exactly the lazy initialisation followed by a fresh uniform sampling that fills the cache.

theorem sum_update_eq_card_mul_sum {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] (i : α) (G : (α → β) → ENNReal) : ∑ v : β, ∑ y : α → β, G (Function.update y i v) = ↑(Fintype.card β) * ∑ z : α → β, G z

Sum-over-Function.update reorganization (would-be-generic). Used by lazy_query_convert_eq_convert_random_oracle_query. Cannot be moved out of this file as-is because the local sorry'd Fintype (a → b) instance in Basic.lean shadows Mathlib's Pi.instFintype, causing type-class instance mismatches at the call site if the lemma is elaborated in a module that doesn't see the local instance. Move once the duplicate Fintype instance is removed.

theorem lazy_query_convert_eq_convert_random_oracle_query (inp : input) : (do let v ← lazy_query inp convert pure v) = do convert random_oracle_query inp

Value-passing lazy/eager bridge for lazy_query: lazy_query followed by convert (passing the value through) equals convert followed by random_oracle_query. This is the workhorse equation; the continuation form lazy_query_convert_cont_eq_convert_random_oracle_query is a corollary.

theorem lazy_query_convert_cont_eq_convert_random_oracle_query {β : Type} (inp : input) (k : output → GaudisCrypt.ProgramDenotation state β) : (do let v ← lazy_query inp convert k v) = convert >>= fun (x : Unit) => random_oracle_query inp >>= k

Continuation-passing variant of lazy_query_convert_eq_convert_random_oracle_query.

theorem if_factor_convert (b : Bool) (X : GaudisCrypt.ProgramDenotation state Unit) : (if b = true then do convert X else convert) = do convert if b = true then X else pure ()

Factor convert out of an if: if the then-branch starts with convert and the else-branch IS convert, we can move convert outside.

theorem convert_random_oracle_init : (do convert random_oracle_init) = random_oracle_init

convert is absorbed by random_oracle_init: a fresh uniform sample overwrites any prior RO content.

theorem convert_bind_random_oracle_init_bind {α : Type} (rest : GaudisCrypt.ProgramDenotation state α) : (do convert random_oracle_init rest) = do random_oracle_init rest

convert is absorbed by any program that starts with random_oracle_init: convert >>= (random_oracle_init >>= rest) = random_oracle_init >>= rest. Used by convert_*_experiment_eager lemmas (where the experiment starts with random_oracle_init) to absorb a preceding convert step.

def ProgramDenotation.transfer {α : Type} (p q : GaudisCrypt.ProgramDenotation state α) : Prop

Lazy/eager transfer relation: p followed by convert produces the same joint α × state distribution as convert followed by q.

Captures "convert slides past p, turning lazy operations into eager ones". The instance of the generic ProgramDenotation.transferBy calculus at c := convert: closed under bind; reflexive on RO-disjoint programs. Together with the base cases lazy_init ↦ random_oracle_init (lazy_init_convert_eq_random_oracle_init) and lazy_query x ↦ random_oracle_query x (lazy_query_convert_eq_convert_random_oracle_query), this lets us transfer any program built from these primitives.

Equations

• ProgramDenotation.transfer p q = convert.transferBy p q

theorem ProgramDenotation.transfer_refl_of_inFootprint_compl {α : Type} {p : GaudisCrypt.ProgramDenotation state α} (hp : p.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) : transfer p p

Reflexivity on RO-disjoint programs — countability-free (subtask 4). The Footprint analogue of transfer_refl_of_inRange_compl: a program whose probabilistic footprint avoids the RO table commutes with convert (via commute_of_disjoint_footprint, no [Countable]), so transfers to itself. The ᶜ-form makes the disjointness le_refl.

theorem ProgramDenotation.transfer_of_inFootprint_disjoint {α : Type} (p : GaudisCrypt.ProgramDenotation state α) {β : Type} (v : GaudisCrypt.Lens β state) [GaudisCrypt.disjoint v random_oracle_state] (hp : p.inFootprint v.footprint) : transfer p p

Any program in v.footprint, for a v disjoint from random_oracle_state, transfers to itself — the countability-free Footprint analogue of transfer_of_inRange_disjoint.

theorem ProgramDenotation.transfer_set_of_disjoint_ro {α : Type} (v : GaudisCrypt.Lens α state) [GaudisCrypt.disjoint v random_oracle_state] (x : α) : transfer (GaudisCrypt.ProgramDenotation.set v x) (GaudisCrypt.ProgramDenotation.set v x)

ProgramDenotation.set v x transfers to itself when v is disjoint from random_oracle_state. Countability-free (subtask 4): via the Footprint transfer-reflexivity.

theorem ProgramDenotation.transfer_get_of_disjoint_ro {α : Type} (v : GaudisCrypt.Lens α state) [GaudisCrypt.disjoint v random_oracle_state] : transfer (GaudisCrypt.ProgramDenotation.get v) (GaudisCrypt.ProgramDenotation.get v)

ProgramDenotation.get v transfers to itself when v is disjoint from random_oracle_state. Countability-free (subtask 4).

theorem convert_commutes_set {α : Type} (v : Variable α) [GaudisCrypt.disjoint v random_oracle_state] (x : α) : (do GaudisCrypt.ProgramDenotation.set v x convert) = do convert GaudisCrypt.ProgramDenotation.set v x

convert commutes with ProgramDenotation.set v x for any v disjoint from random_oracle_state: the bind form of transfer_set_of_disjoint_ro.

theorem convert_commutes_get {α β : Type} (v : Variable α) [GaudisCrypt.disjoint v random_oracle_state] (k : α → GaudisCrypt.ProgramDenotation state β) : (do let y ← GaudisCrypt.ProgramDenotation.get v convert k y) = convert >>= fun (x : Unit) => GaudisCrypt.ProgramDenotation.get v >>= k

convert commutes with ProgramDenotation.get v for any v disjoint from random_oracle_state, in continuation-passing form: the continuation form of transfer_get_of_disjoint_ro.

theorem ProgramDenotation.transfer_uniform {α : Type} [Fintype α] [Nonempty α] : transfer GaudisCrypt.ProgramDenotation.uniform GaudisCrypt.ProgramDenotation.uniform

ProgramDenotation.uniform transfers to itself (it doesn't touch state at all). Countability-free (subtask 4).

theorem ProgramDenotation.transfer_bind {α β : Type} {p q : GaudisCrypt.ProgramDenotation state α} {p' q' : α → GaudisCrypt.ProgramDenotation state β} (h : transfer p q) (h' : ∀ (a : α), transfer (p' a) (q' a)) : transfer (p >>= p') (q >>= q')

Bind closure: transfer chains under >>=.

theorem ProgramDenotation.transfer_pure {α : Type} (a : α) : transfer (pure a) (pure a)

Pure transfers to itself.

theorem ProgramDenotation.transfer_lazy_init : transfer lazy_init random_oracle_init

lazy_init transfers to random_oracle_init: lazy_init; convert equals random_oracle_init (the claim), which absorbs a preceding convert.

theorem ProgramDenotation.transfer_lazy_query (x : input) : transfer (lazy_query x) (random_oracle_query x)

lazy_query x transfers to random_oracle_query x. This is lazy_query_convert_eq_convert_random_oracle_query restated in the transfer language.

theorem ProgramDenotation.transfer_while_loop {cond : GaudisCrypt.ProgramDenotation state Bool} (h_cond : cond.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) {body_lazy body_eager : GaudisCrypt.ProgramDenotation state Unit} (h_body : transfer body_lazy body_eager) : transfer (GaudisCrypt.while_loop cond body_lazy) (GaudisCrypt.while_loop cond body_eager)

Transfer is preserved by while_loop. If the body transfers (lazy to eager) and the condition is RO-disjoint, then the lazy and eager while-loops transfer.

Instance of the generic Kleene closure ProgramDenotation.transferBy_while_loop; the condition's self-transfer comes from its RO-disjointness via the footprint transfer-reflexivity. Any RO-based while-loop construction inherits the lazy = eager equivalence by this closure law plus the base-case body transfer.

theorem ProgramDenotation.transfer_value_marginal {α : Type} {p q : GaudisCrypt.ProgramDenotation state α} (h_transfer : transfer p q) (h_absorb : (do convert q) = q) (σ₀ : state) : (do let aσ ← p σ₀ pure aσ.1) = do let aσ ← q σ₀ pure aσ.1

Value marginal: SubProb-level statement of the transfer. (For the wp-level value-only bridge, use ProgramDenotation.transferBy_wp_value with convert_mass.)

Enriched transfer: RO-invariant projections of state

The basic transfer_wp_value only delivers wp-equality for posts that ignore the state. But convert only writes random_oracle_state — so any projection of state that is invariant under random_oracle_state.set is automatically preserved by convert. This means we can transfer postconditions that depend on (value, RO-invariant state projection).

These enriched lemmas recover the full strength of the wrapper-style oracle_loop_wp_lazy_eq_random_oracle and its marginal/compl/glob companions, without rebuilding the Kleene argument.

theorem convert_wp_state_const_of_ro_invariant (G : state → ENNReal) (hG_inv : ∀ (σ : state) (x : input → Option output), G (random_oracle_state.set x σ) = G σ) (σ : state) : convert.wp (fun (aσ : Unit × state) => G aσ.2) σ = G σ

convert preserves any state projection G : state → ENNReal that is invariant under writes to random_oracle_state. Because convert only samples a fresh RO function and writes it, an RO-invariant G is constant along the convert trajectory, and convert's total mass is 1.

theorem ProgramDenotation.transfer_wp_ro_invariant {α : Type} {p q : GaudisCrypt.ProgramDenotation state α} (h_transfer : transfer p q) (h_absorb : (do convert q) = q) (F : α × state → ENNReal) (hF_inv : ∀ (a : α) (σ : state) (x : input → Option output), F (a, random_oracle_state.set x σ) = F (a, σ)) (σ₀ : state) : p.wp F σ₀ = q.wp F σ₀

Transfer at the wp level for RO-invariant postconditions. Strict strengthening of transfer_wp_value: instead of requiring the post to ignore state entirely, only requires it to be invariant under writes to random_oracle_state.

Captures the wrapper-style oracle_loop_wp_lazy_eq_random_oracle.

theorem ProgramDenotation.transfer_marginal_ro_invariant {α β : Type} {p q : GaudisCrypt.ProgramDenotation state α} (h_transfer : transfer p q) (h_absorb : (do convert q) = q) (h : state → β) (h_inv : ∀ (σ : state) (x : input → Option output), h (random_oracle_state.set x σ) = h σ) (σ₀ : state) : (do let aσ ← p σ₀ pure (aσ.1, h aσ.2)) = do let aσ ← q σ₀ pure (aσ.1, h aσ.2)

Marginal at the (value × RO-invariant projection) level.

Strict strengthening of transfer_value_marginal: instead of projecting to just the value, we additionally include any RO-invariant projection h : state → β. Captures the wrapper-style oracle_loop_marginal_lazy_eq_random_oracle family.