PRP/PRF switching lemma — oracles and the shared bad flag (Phase 1)

Infrastructure for the information-theoretic switching lemma |Pr[A^RF] − Pr[A^RP]| ≤ q(q−1)/2N, set up for the up-to-bad (Fundamental Lemma) argument in the relational calculus.

The two oracles are identical until bad: both draw the same underlying uniform value y on a cache miss and set the shared flag prp_bad to true iff y already occurs in the oracle's image (a collision). On no collision both behave identically (cache y); on a collision RF keeps y (with replacement) while RP resamples a fresh value from the unused outputs (without replacement). Because the flag is set from the same draw against the same image, it agrees on both sides — exactly what relE.up_to_bad needs.

• prp_bad : Variable Bool — the shared "a collision has occurred" flag.
• colliding_outputs h inp — outputs already used by inputs other than inp (the values a fresh draw at inp would collide with). Equal to inducing_set inp σ when h = random_oracle_state.get σ.
• lazy_query_rf / lazy_query_rp — the RF and RP oracles.
• lazy_query_rf_inFootprint / lazy_query_rp_inFootprint — both touch only random_oracle_state and prp_bad.

This is Phase 1 of the plan; the per-query coupling (Phase 2) and the Fundamental-Lemma assembly (Phases 3–4) build on these definitions.

axiom prp_bad : Variable Bool

Shared "a collision has occurred" flag for the switching coupling. Set to true the first time a freshly drawn output already appears in the image; both lazy_query_rf and lazy_query_rp maintain it identically.

axiom disjoint_prp_bad_ro : GaudisCrypt.disjoint prp_bad random_oracle_state

axiom disjoint_prp_bad_oracle_input : GaudisCrypt.disjoint prp_bad oracle_input

axiom disjoint_prp_bad_oracle_output : GaudisCrypt.disjoint prp_bad oracle_output

instance instDisjointForallInputOptionOutputStateBoolRandom_oracle_statePrp_bad : GaudisCrypt.disjoint random_oracle_state prp_bad

Symmetric instances.

instance instDisjointInputStateBoolOracle_inputPrp_bad : GaudisCrypt.disjoint oracle_input prp_bad

instance instDisjointOutputStateBoolOracle_outputPrp_bad : GaudisCrypt.disjoint oracle_output prp_bad

instance instDisjointForallInputOptionOutputStateRandom_oracle_stateOracle_input : GaudisCrypt.disjoint random_oracle_state oracle_input

The symmetric forms of the OracleLoop RO-disjointness axioms, needed to frame the RO read/write inside the oracles against the scratch lenses.

instance instDisjointForallInputOptionOutputStateRandom_oracle_stateOracle_output : GaudisCrypt.disjoint random_oracle_state oracle_output

noncomputable def colliding_outputs (h : input → Option output) (inp : input) : Finset output

Outputs already assigned to some input other than inp — i.e. the values a fresh draw at inp would collide with, and (when inp is uncached) the set RP must avoid to stay injective. Definitionally equal to inducing_set inp σ when h = random_oracle_state.get σ.

Equations

• colliding_outputs h inp = Finset.image (fun (x' : input) => (h x').getD default) ({x' ∈ Finset.univ.erase inp | (h x').isSome = true})

noncomputable def lazy_query_rf (inp : input) : GaudisCrypt.ProgramDenotation state output

RF oracle (instrumented). Acts exactly like lazy_query on the RO state, additionally setting prp_bad := true when the freshly drawn value already occurs in the image (the draw creates a collision). Written with explicit >>= to avoid the do-notation join-point macro on the if.

Equations

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

noncomputable def lazy_query_rp (inp : input) : GaudisCrypt.ProgramDenotation state output

RP oracle (instrumented, resample-on-collision). Draws the same y and sets prp_bad on a collision exactly as lazy_query_rf. On a collision it resamples uniformly from the unused outputs (univ \ colliding_outputs), keeping the oracle injective; if the outputs are exhausted it falls through (the flag is already set, so the returned value is immaterial).

Equations

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

Closed-form weakest preconditions (Phase 2a)

The per-query coupling marginals are computed against these closed forms.

noncomputable def rp_resample_sub (h : input → Option output) (inp : input) (y : output) : GaudisCrypt.SubProbability output

The sub-distribution lazy_query_rp resamples from on a collision: uniform over the unused outputs, or a point mass on y if all outputs are used.

Equations

• rp_resample_sub h inp y = if hne : (Finset.univ \ colliding_outputs h inp).Nonempty then GaudisCrypt.SubProbability.uniformOfFinset (Finset.univ \ colliding_outputs h inp) hne else pure y

theorem lazy_query_rf_wp_hit {inp : input} {σ : state} {x : output} (hc : random_oracle_state.get σ inp = some x) (F : output × state → ENNReal) : (lazy_query_rf inp).wp F σ = F (x, σ)

lazy_query_rf on a cache hit returns the cached value, no state change.

theorem lazy_query_rp_wp_hit {inp : input} {σ : state} {x : output} (hc : random_oracle_state.get σ inp = some x) (G : output × state → ENNReal) : (lazy_query_rp inp).wp G σ = G (x, σ)

lazy_query_rp on a cache hit returns the cached value, no state change.

theorem lazy_query_rf_wp_miss {inp : input} {σ : state} (hc : random_oracle_state.get σ inp = none) (F : output × state → ENNReal) : (lazy_query_rf inp).wp F σ = ∑ y : output, F (y, if y ∈ colliding_outputs (random_oracle_state.get σ) inp then random_oracle_state.set (fun (k : input) => if k = inp then some y else random_oracle_state.get σ k) (prp_bad.set true σ) else random_oracle_state.set (fun (k : input) => if k = inp then some y else random_oracle_state.get σ k) σ) / ↑(Fintype.card output)

lazy_query_rf on a cache miss: uniform over the drawn value y, setting the flag and caching y on a collision (with replacement).

theorem lazy_query_rp_wp_miss {inp : input} {σ : state} (hc : random_oracle_state.get σ inp = none) (G : output × state → ENNReal) : (lazy_query_rp inp).wp G σ = ∑ y : output, (if y ∈ colliding_outputs (random_oracle_state.get σ) inp then (rp_resample_sub (random_oracle_state.get σ) inp y).expected fun (y' : output) => G (y', random_oracle_state.set (fun (k : input) => if k = inp then some y' else random_oracle_state.get σ k) (prp_bad.set true σ)) else G (y, random_oracle_state.set (fun (k : input) => if k = inp then some y else random_oracle_state.get σ k) σ)) / ↑(Fintype.card output)

lazy_query_rp on a cache miss: uniform over the drawn value y; on a collision it sets the flag and resamples a fresh value (without replacement) via rp_resample_sub, otherwise caches y.

theorem lazy_query_rf_inFootprint {α : Type} (L : Variable α) [GaudisCrypt.disjoint random_oracle_state L] [GaudisCrypt.disjoint prp_bad L] (inp : input) : (lazy_query_rf inp).inFootprint (GaudisCrypt.Lens.footprint L)ᶜ

lazy_query_rf touches only random_oracle_state and prp_bad: it lives in the complement of any lens disjoint from both.

theorem lazy_query_rp_inFootprint {α : Type} (L : Variable α) [GaudisCrypt.disjoint random_oracle_state L] [GaudisCrypt.disjoint prp_bad L] (inp : input) : (lazy_query_rp inp).inFootprint (GaudisCrypt.Lens.footprint L)ᶜ

lazy_query_rp touches only random_oracle_state and prp_bad.

The per-query coupling (Phase 2b)

theorem rp_resample_sub_expected_const (h : input → Option output) (inp : input) (y : output) (c : ENNReal) : ((rp_resample_sub h inp y).expected fun (x : output) => c) = c

The resample sub-distribution has mass one, so integrating a constant against it returns the constant.

theorem lazy_query_switch_step (inp : input) : (lazy_query_rf inp).relE (lazy_query_rp inp) (fun (σ₁ σ₂ : state) => σ₁ = σ₂ ∧ prp_bad.get σ₁ = false) fun (u v : output × state) => prp_bad.get u.2 = prp_bad.get v.2 ∧ (prp_bad.get u.2 = false → u = v)

Per-query coupling (the heart of the switching argument). From equal states with the flag clear, lazy_query_rf and lazy_query_rp are coupled so that the flag always agrees, and on no-collision runs the full output-and-state result agrees. The collision branch is coupled by the independent product (both flags are then true, so the post is satisfied regardless).

Unary facts: mass one and flag preservation (Phase 3a)

These feed the flag-set mode of the loop body, where the two games have already diverged and are coupled only through rel.of_unary: each side independently keeps prp_bad = true (with full mass).

theorem prp_bad_get_ro_set (g : input → Option output) (σ : state) : prp_bad.get (random_oracle_state.set g σ) = prp_bad.get σ

Setting random_oracle_state doesn't change the flag.

theorem prp_bad_get_ro_set_true (g : input → Option output) (σ : state) : prp_bad.get (random_oracle_state.set g (prp_bad.set true σ)) = true

After setting the flag then the RO, the flag is true.

theorem lazy_query_rf_mass_one (inp : input) (σ : state) : (lazy_query_rf inp).wp (fun (x : output × state) => 1) σ = 1

lazy_query_rf is lossless.

theorem lazy_query_rp_mass_one (inp : input) (σ : state) : (lazy_query_rp inp).wp (fun (x : output × state) => 1) σ = 1

lazy_query_rp is lossless.

theorem lazy_query_rf_keeps_flag {inp : input} {σ : state} (h : prp_bad.get σ = true) : (lazy_query_rf inp).wp (fun (u : output × state) => if prp_bad.get u.2 = true then 0 else 1) σ = 0

lazy_query_rf keeps prp_bad = true.

theorem lazy_query_rp_keeps_flag {inp : input} {σ : state} (h : prp_bad.get σ = true) : (lazy_query_rp inp).wp (fun (u : output × state) => if prp_bad.get u.2 = true then 1 else 0) σ = 1

lazy_query_rp keeps prp_bad = true (with full mass).

Two-mode relational lifting (Phase 3b)

theorem wp_keeps_flag_zero {α : Type} {prog : GaudisCrypt.ProgramDenotation state α} (hpres : prog.inFootprint (GaudisCrypt.Lens.footprint prp_bad)ᶜ) {σ : state} (h : prp_bad.get σ = true) : prog.wp (fun (u : α × state) => if prp_bad.get u.2 = true then 0 else 1) σ = 0

A program that doesn't touch prp_bad almost surely keeps it true.

theorem flag_one_of_zero {α : Type} {prog : GaudisCrypt.ProgramDenotation state α} {σ : state} (hmass : prog.wp (fun (x : α × state) => 1) σ = 1) (hzero : prog.wp (fun (u : α × state) => if prp_bad.get u.2 = true then 0 else 1) σ = 0) : prog.wp (fun (u : α × state) => if prp_bad.get u.2 = true then 1 else 0) σ = 1

From losslessness and a.s.-flag-preservation, the full-mass flag form.

theorem two_mode_relE {α : Type} {p q : GaudisCrypt.ProgramDenotation state α} {Pre : state → state → Prop} {Post : α × state → α × state → Prop} (h_flageq : ∀ (σ₁ σ₂ : state), Pre σ₁ σ₂ → prp_bad.get σ₁ = prp_bad.get σ₂) (h_sync_fwd : p.rel q (fun (σ₁ σ₂ : state) => Pre σ₁ σ₂ ∧ prp_bad.get σ₁ = false) Post) (h_sync_bwd : q.rel p (fun (σ₂ σ₁ : state) => Pre σ₁ σ₂ ∧ prp_bad.get σ₁ = false) fun (v u : α × state) => Post u v) (h_p0 : ∀ (σ : state), prp_bad.get σ = true → p.wp (fun (u : α × state) => if prp_bad.get u.2 = true then 0 else 1) σ = 0) (h_p1 : ∀ (σ : state), prp_bad.get σ = true → p.wp (fun (u : α × state) => if prp_bad.get u.2 = true then 1 else 0) σ = 1) (h_q0 : ∀ (σ : state), prp_bad.get σ = true → q.wp (fun (u : α × state) => if prp_bad.get u.2 = true then 0 else 1) σ = 0) (h_q1 : ∀ (σ : state), prp_bad.get σ = true → q.wp (fun (u : α × state) => if prp_bad.get u.2 = true then 1 else 0) σ = 1) (h_post_true : ∀ (u v : α × state), prp_bad.get u.2 = true → prp_bad.get v.2 = true → Post u v) : p.relE q Pre Post

Two-mode relational lifting. For two programs over state related by a precondition that (a) forces flag agreement and (b) when the flag is clear forces synchronization (h_sync_*), the judgment lifts to the conditional invariant. The flag-clear mode is given directly; the flag-set mode uses rel.of_unary (each side independently keeps prp_bad set).

theorem lazy_query_rp_keeps_flag_zero {inp : input} {σ : state} (h : prp_bad.get σ = true) : (lazy_query_rp inp).wp (fun (u : output × state) => if prp_bad.get u.2 = true then 0 else 1) σ = 0

lazy_query_rp a.s. keeps prp_bad = true.

theorem lazy_query_rf_keeps_flag_one {inp : input} {σ : state} (h : prp_bad.get σ = true) : (lazy_query_rf inp).wp (fun (u : output × state) => if prp_bad.get u.2 = true then 1 else 0) σ = 1

lazy_query_rf keeps prp_bad = true with full mass.

The loop body preserves the conditional invariant (Phase 3b)

theorem oracle_step_switch_relE (A : GaudisCrypt.ProgramDenotation state Unit) (hA_pres : A.inFootprint (GaudisCrypt.Lens.footprint prp_bad)ᶜ) (hA_mass : ∀ (σ : state), A.wp (fun (x : Unit × state) => 1) σ = 1) : (oracle_step A lazy_query_rf).relE (oracle_step A lazy_query_rp) (fun (σ₁ σ₂ : state) => prp_bad.get σ₁ = prp_bad.get σ₂ ∧ (prp_bad.get σ₁ = false → σ₁ = σ₂)) fun (u v : Unit × state) => prp_bad.get u.2 = prp_bad.get v.2 ∧ (prp_bad.get u.2 = false → u.2 = v.2)

The switching loop body relates RF to RP at the conditional invariant. oracle_step A with the RF oracle relates to the same with the RP oracle: the flag always agrees, and as long as it is clear the states stay equal. Requires A to leave prp_bad untouched and to be lossless.

Loop lifting and the Fundamental Lemma (Phase 3c)

theorem loop_switch_relE (A : GaudisCrypt.ProgramDenotation state Unit) (hA_pres : A.inFootprint (GaudisCrypt.Lens.footprint prp_bad)ᶜ) (hA_mass : ∀ (σ : state), A.wp (fun (x : Unit × state) => 1) σ = 1) (q : ℕ) : (GaudisCrypt.loop_n q (oracle_step A lazy_query_rf)).relE (GaudisCrypt.loop_n q (oracle_step A lazy_query_rp)) (fun (σ₁ σ₂ : state) => prp_bad.get σ₁ = prp_bad.get σ₂ ∧ (prp_bad.get σ₁ = false → σ₁ = σ₂)) fun (u v : Unit × state) => prp_bad.get u.2 = prp_bad.get v.2 ∧ (prp_bad.get u.2 = false → u.2 = v.2)

The whole q-round game relates RF to RP at the conditional invariant.

theorem switch_up_to_bad (A : GaudisCrypt.ProgramDenotation state Unit) (hA_pres : A.inFootprint (GaudisCrypt.Lens.footprint prp_bad)ᶜ) (hA_mass : ∀ (σ : state), A.wp (fun (x : Unit × state) => 1) σ = 1) (q : ℕ) (G : state → ENNReal) (σ : state) : (GaudisCrypt.loop_n q (oracle_step A lazy_query_rf)).wp (fun (u : Unit × state) => G u.2) σ ≤ (GaudisCrypt.loop_n q (oracle_step A lazy_query_rp)).wp (fun (u : Unit × state) => G u.2) σ + (GaudisCrypt.loop_n q (oracle_step A lazy_query_rf)).wp (fun (u : Unit × state) => if prp_bad.get u.2 = true then G u.2 else 0) σ

Switching inequality (Fundamental Lemma). For any state-functional G, the RF game's expectation is at most the RP game's plus the probability that RF triggered a collision (prp_bad). Starting from a common state.

Bounding the bad event (Phase 4)

theorem RO_size_set_upd_fresh {x : input} {σ : state} (hc : random_oracle_state.get σ x = none) (y : output) (τ : state) : RO_size (random_oracle_state.set (fun (k : input) => if k = x then some y else random_oracle_state.get σ k) τ) = RO_size σ + 1

Caching a fresh input grows the RO size by exactly one (independent of any disjoint scratch state in the base).

theorem lazy_query_rf_RO_size_step (x : input) (σ : state) : (lazy_query_rf x).wp (fun (u : output × state) => ↑(RO_size u.2)) σ ≤ ↑(RO_size σ) + 1

One RF query grows the expected RO size by at most one.

theorem lazy_query_rf_bad_step (x : input) (σ : state) : (lazy_query_rf x).wp (fun (u : output × state) => if prp_bad.get u.2 = true then 1 else 0) σ ≤ (if prp_bad.get σ = true then 1 else 0) + ↑(RO_size σ) / ↑(Fintype.card output)

One RF query bumps the bad-flag indicator by at most RO_size σ / N: the flag flips only when the fresh draw lands in the (≤ RO_size)-element collision set.

theorem oracle_step_bump_gen {A : GaudisCrypt.ProgramDenotation state Unit} (oracle : input → GaudisCrypt.ProgramDenotation state output) {f : state → ENNReal} (c : state → ENNReal) (h_adv_f : ∀ (σ : state), A.wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ) (h_adv_c : ∀ (σ : state), A.wp (fun (yσ : Unit × state) => c yσ.2) σ ≤ c σ) (h_set_oo : ∀ (y : output) (σ : state), f (oracle_output.set y σ) = f σ) (h_oracle : ∀ (x : input) (σ : state), (oracle x).wp (fun (yσ : output × state) => f yσ.2) σ ≤ f σ + c σ) (σ : state) : (oracle_step A oracle).wp (fun (yσ : Unit × state) => f yσ.2) σ ≤ f σ + c σ

Generic oracle_step potential bump, parameterized by the oracle (the lazy_query-specific oracle_step_wp_indicator_bump adapted).

theorem oracle_step_rf_size_bump {A : GaudisCrypt.ProgramDenotation state Unit} (hA_ro : A.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (hA_mass : ∀ (σ : state), A.wp (fun (x : Unit × state) => 1) σ = 1) (σ : state) : (oracle_step A lazy_query_rf).wp (fun (u : Unit × state) => ↑(RO_size u.2)) σ ≤ ↑(RO_size σ) + 1

One loop body bumps RO_size by at most one.

theorem oracle_step_rf_bad_bump {A : GaudisCrypt.ProgramDenotation state Unit} (hA_ro : A.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (hA_pres : A.inFootprint (GaudisCrypt.Lens.footprint prp_bad)ᶜ) (σ : state) : (oracle_step A lazy_query_rf).wp (fun (u : Unit × state) => if prp_bad.get u.2 = true then 1 else 0) σ ≤ (if prp_bad.get σ = true then 1 else 0) + ↑(RO_size σ) / ↑(Fintype.card output)

One loop body bumps the bad-flag indicator by at most RO_size σ / N.

The switching lemma (Phase 4)

theorem loop_rf_bad_bound {A : GaudisCrypt.ProgramDenotation state Unit} (hA_ro : A.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (hA_pres : A.inFootprint (GaudisCrypt.Lens.footprint prp_bad)ᶜ) (hA_mass : ∀ (σ : state), A.wp (fun (x : Unit × state) => 1) σ = 1) (q : ℕ) (σ : state) (h_flag : prp_bad.get σ = false) (h_size0 : RO_size σ = 0) : (GaudisCrypt.loop_n q (oracle_step A lazy_query_rf)).wp (fun (u : Unit × state) => if prp_bad.get u.2 = true then 1 else 0) σ ≤ ↑q * (↑q - 1) / (2 * ↑(Fintype.card output))

Bad-event bound. Starting from a clean state (flag clear, empty oracle), the probability that q RF rounds set prp_bad is at most q(q−1)/2N. The bad flag is itself a collision potential, so this is loop_n_birthday_bound applied directly.

theorem switching_lemma {A : GaudisCrypt.ProgramDenotation state Unit} (hA_ro : A.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (hA_pres : A.inFootprint (GaudisCrypt.Lens.footprint prp_bad)ᶜ) (hA_mass : ∀ (σ : state), A.wp (fun (x : Unit × state) => 1) σ = 1) (q : ℕ) (G : state → ENNReal) (hG : ∀ (σ : state), G σ ≤ 1) (σ : state) (h_flag : prp_bad.get σ = false) (h_size0 : RO_size σ = 0) : (GaudisCrypt.loop_n q (oracle_step A lazy_query_rf)).wp (fun (u : Unit × state) => G u.2) σ ≤ (GaudisCrypt.loop_n q (oracle_step A lazy_query_rp)).wp (fun (u : Unit × state) => G u.2) σ + ↑q * (↑q - 1) / (2 * ↑(Fintype.card output))

PRP/PRF switching lemma. For a distinguisher A (touching neither the oracle table nor the internal flag, and lossless) outputting a [0,1]-valued functional G, the RF and RP games differ by at most q(q−1)/2N:

Pr[A^RF : G] ≤ Pr[A^RP : G] + q(q−1)/2N.

Combines the Fundamental Lemma (switch_up_to_bad) with the birthday bound on the bad event (loop_rf_bad_bound).