Oracle loops

Scratch state and loop primitives for adversary-driven oracle protocols.

• Scratch state: want_more, oracle_input, oracle_output, adversary_result — the per-step variables shared between the adversary and the loop infrastructure. All disjoint from random_oracle_state.

• The three oracle-loop variants, sharing the same body shape:

  • oracle_step — one iteration.
  • oracle_loop_n — q iterations (static query budget).
  • oracle_loop — unbounded iteration via while_loop and want_more.

• Their transfer / inRange / linear-bound / indicator-step lemmas.

• Key-level RO reasoning for lazy_query inp >>= set oracle_output (the "deferred sampling" combinator).

Scratch state

axiom want_more : Variable Bool

axiom oracle_input : Variable input

axiom oracle_output : Variable output

axiom adversary_result : Variable Bool

noncomputable def skip : GaudisCrypt.ProgramDenotation state Unit

Equations

• skip = pure ()

axiom disjoint_want_more_ro : GaudisCrypt.disjoint want_more random_oracle_state

axiom disjoint_oracle_input_ro : GaudisCrypt.disjoint oracle_input random_oracle_state

axiom disjoint_oracle_output_ro : GaudisCrypt.disjoint oracle_output random_oracle_state

axiom disjoint_adversary_result_ro : GaudisCrypt.disjoint adversary_result random_oracle_state

lazy_query + set oracle_output — the "deferred sampling" combinator

The combined step "query the oracle on inp, store the result in oracle_output" is the unit of work performed in every oracle-loop body. We collect its key-level properties here.

theorem query_set_convert_eq : (do do let inp ← GaudisCrypt.ProgramDenotation.get oracle_input let v ← lazy_query inp GaudisCrypt.ProgramDenotation.set oracle_output v convert) = do convert let inp ← GaudisCrypt.ProgramDenotation.get oracle_input let v ← random_oracle_query inp GaudisCrypt.ProgramDenotation.set oracle_output v

Pushing convert past the let inp ← get oracle_input; let v ← lazy_query inp; set oracle_output v piece.

theorem lazy_query_then_set_oracle_output_inFootprint_compl {γ : Type} (L : GaudisCrypt.Lens γ state) [GaudisCrypt.disjoint random_oracle_state L] [GaudisCrypt.disjoint oracle_output L] (inp : input) : (do let y ← lazy_query inp GaudisCrypt.ProgramDenotation.set oracle_output y).inFootprint L.footprintᶜ

(lazy_query inp >>= set oracle_output) avoids any lens L disjoint from both random_oracle_state and oracle_output (probabilistic footprint form).

theorem lazy_query_set_oracle_output_preserves_RO_at_other_key (inp k : input) (h_neq : inp ≠ k) (σ : state) (F : Unit × state → ENNReal) : (do let y_lq ← lazy_query inp GaudisCrypt.ProgramDenotation.set oracle_output y_lq).wp F σ = (do let y_lq ← lazy_query inp GaudisCrypt.ProgramDenotation.set oracle_output y_lq).wp (fun (aσ_lq : Unit × state) => if random_oracle_state.get aσ_lq.2 k = random_oracle_state.get σ k then F aσ_lq else 0) σ

(lazy_query inp >>= set oracle_output) preserves RO[k] for inp ≠ k. More precisely, the wp can be strengthened with the RO[k]-preserved condition.

theorem RO_setentry_neq_commutes_lazy_query_set_oracle_output (inp x : input) (h_neq : inp ≠ x) (y : output) (σ : state) (F : Unit × state → ENNReal) : (do let y_lq ← lazy_query inp GaudisCrypt.ProgramDenotation.set oracle_output y_lq).wp F (random_oracle_state.set (fun (k : input) => if k = x then some y else random_oracle_state.get σ k) σ) = (do let y_lq ← lazy_query inp GaudisCrypt.ProgramDenotation.set oracle_output y_lq).wp (fun (aσ_lq : Unit × state) => F (aσ_lq.1, random_oracle_state.set (fun (k : input) => if k = x then some y else random_oracle_state.get aσ_lq.2 k) aσ_lq.2)) σ

Fine-grained RO commutativity: a write to RO[x] commutes with (lazy_query inp >>= set oracle_output) when inp ≠ x. Writes to different RO keys commute, and oracle_output is disjoint from RO. Mechanical core of averaged-invariance MISS-case arguments.

Generic adversary + oracle loop primitives

Both cr_loop_body/cr_loop (in CollisionResistance.lean) and ow_loop_body/ow_loop (in OneWayness.lean) use the same shape: "run the adversary, then perform one oracle call on whatever the adversary wrote to oracle_input, storing the result in oracle_output." The shared abstraction lives here. Game-specific files alias these.

noncomputable def oracle_step (adv : GaudisCrypt.ProgramDenotation state Unit) (oracle : input → GaudisCrypt.ProgramDenotation state output) : GaudisCrypt.ProgramDenotation state Unit

One round of an adversary-and-query loop body. Generic over the adversary; parameterised over the oracle so it can be instantiated to lazy_query or random_oracle_query.

Equations

• oracle_step adv oracle = do adv let __do_lift ← GaudisCrypt.ProgramDenotation.get oracle_input let __do_lift ← oracle __do_lift GaudisCrypt.ProgramDenotation.set oracle_output __do_lift

noncomputable def oracle_loop_n (adv : GaudisCrypt.ProgramDenotation state Unit) : ℕ → (input → GaudisCrypt.ProgramDenotation state output) → GaudisCrypt.ProgramDenotation state Unit

Run oracle_step adv oracle for q rounds.

Equations

• oracle_loop_n adv 0 x✝ = pure ()
• oracle_loop_n adv n.succ x✝ = do oracle_step adv x✝ oracle_loop_n adv n x✝

Unbounded oracle_loop

The while_loop variant: the adversary may continue indefinitely, terminating by clearing want_more. Strictly more general than oracle_loop_n (which fixes the query budget upfront). The lazy = eager equivalence is proved in PlonkLean.RO.ROEquiv via the transfer framework's while_loop closure law.

noncomputable def oracle_loop (adv init : GaudisCrypt.ProgramDenotation state Unit) (oracle : input → GaudisCrypt.ProgramDenotation state output) : GaudisCrypt.ProgramDenotation state Bool

Unbounded "adversary + oracle call" loop. The adversary decides via the want_more flag whether to continue or stop. Returns the value of adversary_result.

Equations

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

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

The lazy form of oracle_loop's while-loop body.

Equations

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

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

The eager form of oracle_loop's while-loop body.

Equations

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

theorem ProgramDenotation.transfer_oracle_step_prob {adv : GaudisCrypt.ProgramDenotation state Unit} (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) : transfer (oracle_step adv lazy_query) (oracle_step adv random_oracle_query)

oracle_step adv transfers from lazy to eager, provided adv is RO-disjoint. (Countability-free; the inRange original was retired once all consumers moved to inFootprint.)

theorem ProgramDenotation.transfer_oracle_loop_n_prob {adv : GaudisCrypt.ProgramDenotation state Unit} (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (q : ℕ) : transfer (oracle_loop_n adv q lazy_query) (oracle_loop_n adv q random_oracle_query)

oracle_loop_n adv q transfers from lazy to eager. (Countability-free; the inRange original was retired once all consumers moved to inFootprint.)

theorem oracle_step_inFootprint_compl {γ : Type} (L : GaudisCrypt.Lens γ state) [GaudisCrypt.disjoint random_oracle_state L] [GaudisCrypt.disjoint oracle_input L] [GaudisCrypt.disjoint oracle_output L] {adv : GaudisCrypt.ProgramDenotation state Unit} (h_adv : adv.inFootprint L.footprintᶜ) : (oracle_step adv lazy_query).inFootprint L.footprintᶜ

Generic preservation: oracle_step adv avoids any lens L disjoint from random_oracle_state, oracle_input, and oracle_output, provided the adversary avoids it.

theorem oracle_loop_n_inFootprint_compl {γ : Type} (L : GaudisCrypt.Lens γ state) [GaudisCrypt.disjoint random_oracle_state L] [GaudisCrypt.disjoint oracle_input L] [GaudisCrypt.disjoint oracle_output L] {adv : GaudisCrypt.ProgramDenotation state Unit} (h_adv : adv.inFootprint L.footprintᶜ) (q : ℕ) : (oracle_loop_n adv q lazy_query).inFootprint L.footprintᶜ

Generic preservation lifted to the loop, by induction on q.

theorem oracle_loop_n_wp_linear_bound {adv : GaudisCrypt.ProgramDenotation state Unit} {f : state → ENNReal} {c : ENNReal} (h_body : ∀ (σ : state), (oracle_step adv lazy_query).wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ + c) (q : ℕ) (σ : state) : (oracle_loop_n adv q lazy_query).wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ + ↑q * c

Linear-growth bound for oracle_loop_n. If a single body iteration bumps the wp of f (against the state-projected post) by at most a constant c, then q iterations bump it by at most q * c. Captures the standard "loop accumulation" pattern used for both query-budget bounds (e.g. each query bumps RO size by ≤ 1) and probability bounds (e.g. each query has ≤ 1/N chance of producing a target value).

Generic per-query indicator step

The "one lazy_query bumps a state-indicator f by at most the integrated pointwise badness" pattern. Captures lazy_query_collision_step, lazy_query_RO_size_step (in CollisionResistance.lean) and lazy_query_useful_preimage_step (in OneWayness.lean).

theorem lazy_query_wp_step (f : state → ENNReal) (bad : input → output → state → ENNReal) (h_bound : ∀ (x : input) (σ : state) (y : output), random_oracle_state.get σ x = none → f (random_oracle_state.set (fun (x' : input) => if x' = x then some y else random_oracle_state.get σ x') σ) ≤ f σ + bad x y σ) (x : input) (σ : state) : (lazy_query x).wp (fun (yσ : output × state) => f yσ.2) σ ≤ f σ + (∑ y : output, bad x y σ) / ↑(Fintype.card output)

Per-query indicator step (generic). If on every cache-miss, the new fresh sample y at input x bumps f by at most bad x y σ, then the wp of lazy_query x on the state-marginal of f is at most f σ + (∑ y, bad x y σ) / |output|. Cache-hit case is trivial since lazy_query is pure y_cache there (state unchanged).

theorem oracle_step_wp_indicator_bump {adv : GaudisCrypt.ProgramDenotation state Unit} {f : state → ENNReal} (c : state → ENNReal) (h_adv_preserves_f : ∀ (σ : state), adv.wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ) (h_adv_preserves_c : ∀ (σ : state), adv.wp (fun (yσ : Unit × state) => c yσ.2) σ ≤ c σ) (h_set_oo : ∀ (y : output) (σ : state), f (oracle_output.set y σ) = f σ) (h_lazy_query : ∀ (x : input) (σ : state), (lazy_query x).wp (fun (yσ : output × state) => f yσ.2) σ ≤ f σ + c σ) (σ : state) : (oracle_step adv lazy_query).wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ + c σ

Generic oracle-step indicator bump. One oracle_step adv bumps the state-indicator f by at most c σ, given that: (1) the adversary preserves f (in expectation), (2) the adversary preserves c (in expectation), (3) writes to oracle_output leave f unchanged, (4) one lazy_query bumps f by at most c σ.

Captures the standard "Layer A + adv-preservation" pattern: a single loop body iteration bumps the indicator by the per-query amount, because the adversary alone preserves it. Used by both CR and OW for multiple indicators (collision, RO_size, useful_preimage).

theorem oracle_step_wp_indicator_bump_const {adv : GaudisCrypt.ProgramDenotation state Unit} {f : state → ENNReal} (c : ENNReal) (h_adv_preserves : ∀ (σ : state), adv.wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ) (h_set_oo : ∀ (y : output) (σ : state), f (oracle_output.set y σ) = f σ) (h_lazy_query : ∀ (x : input) (σ : state), (lazy_query x).wp (fun (yσ : output × state) => f yσ.2) σ ≤ f σ + c) (σ : state) : (oracle_step adv lazy_query).wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ + c

Constant-c specialization of oracle_step_wp_indicator_bump. The adversary trivially preserves a constant via ProgramDenotation.wp_const_le.

theorem oracle_loop_n_eq_loop_n (adv : GaudisCrypt.ProgramDenotation state Unit) (oracle : input → GaudisCrypt.ProgramDenotation state output) (q : ℕ) : oracle_loop_n adv q oracle = GaudisCrypt.loop_n q (oracle_step adv oracle)

The static-budget oracle loop is the bounded loop combinator applied to a single oracle step. Lets generic loop_n lemmas apply to oracle_loop_n.