OneWayness GameHop: Up-to-Bad Hop (Game 1 → Game 2), relationally

This module bounds the difference between ow_game_1_tracked and ow_game_2_tracked by the bad event (the adversary queried chal_x). The two games differ only in whether the random oracle is pre-programmed at chal_x (Game 1 does, Game 2 doesn't).

One pRHL judgment delivers everything (ow_game_tracked_relE): G1 ~ G2 : Eq ⇒ PostG where PostG says the bad flags agree and, on good runs, the results agree and the states differ only by the pre-programmed RO entry. The coupling invariant carried through the adversary loop is

InvUB x y σ₁ σ₂ := flag σ₁ = flag σ₂
                 ∧ (flag σ₁ = false → chal_x σ₂ = x ∧ σ₁ = insRO x y σ₂)

The per-query coupling lqt_relE is proved by exhibiting one coupling per cache branch (relE.of_coupling); the after-bad phase is the rectangular rule rel.of_unary, whose side conditions are the flag-monotonicity and mass-1 facts.

Main results (all corollaries of the judgment)

• ow_game_1_tracked_eq_ow_game_2_tracked_until_bad — agree-until-bad (via relE.wp_eq).
• ow_game_1_tracked_bad_eq_ow_game_2_tracked_bad — bad events agree (via relE.bad_eq; the former unary proof needed a 138-line mass-conservation/cancellation chain).
• ow_game_1_tracked_le_ow_game_2_tracked_plus_bad — the hop bound (via relE.up_to_bad).

Hypothesis note: the single-judgment route needs the adversary's mass-1 hypothesis for all three results (the rectangular phase needs the right side to be lossless). The OW master theorem assumes it anyway.

The former ~790-line unary development (per-step RO-invariance machinery, flag-true-zero family, mass block, hand-rolled identical-until-bad induction) was replaced by this relational proof; see git history.

Tracking is invisible to flag-ignoring posts (kept: used by Game1)

theorem lazy_query_tracked_eq_lazy_query_wp {α : Type} (k : output → GaudisCrypt.ProgramDenotation state α) (h_k_inFootprint : ∀ (y : output), (k y).inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (F : α × state → ENNReal) (h_F_inv : GaudisCrypt.IgnoresLens chal_x_queried_gh F) (inp : input) (σ : state) : (lazy_query_tracked inp >>= k).wp F σ = (lazy_query inp >>= k).wp F σ

One lazy_query_tracked is wp-equivalent to one lazy_query for any flag-ignoring continuation whose post is also flag-ignoring.

The RO[chal_x] insertion point

insert_at_chal_x is the state-indexed form of the pre-programming write (position read from the state); the relational development below uses the fixed-position form insRO and relates the two where needed.

noncomputable def insert_at_chal_x (y_chal : output) (σ : state) : state

Shorthand: the state with RO[chal_x] forcibly set to some y_chal.

Equations

• insert_at_chal_x y_chal σ = random_oracle_state.set (fun (k : input) => if k = ow_challenge_x.get σ then some y_chal else random_oracle_state.get σ k) σ

The shift function and the coupling invariant

noncomputable def insRO (x : input) (y : output) (σ : state) : state

Overwrite the RO entry at the (fixed) position x with some y. This is insert_at_chal_x with the position decoupled from the state.

Equations

• insRO x y σ = random_oracle_state.set (fun (k : input) => if k = x then some y else random_oracle_state.get σ k) σ

theorem get_insRO {γ : Type} (L : GaudisCrypt.Lens γ state) [GaudisCrypt.disjoint random_oracle_state L] (x : input) (y : output) (σ : state) : L.get (insRO x y σ) = L.get σ

Reading any RO-disjoint lens through insRO is invisible.

def InvUB (x : input) (y : output) (σ₁ σ₂ : state) : Prop

The coupling invariant between the Game-1 run (left) and the Game-2 run (right): flags agree; on good runs the left state is the right state with RO[x ↦ y] overwritten and the right challenge is x.

Equations

• InvUB x y σ₁ σ₂ = (chal_x_queried_gh.get σ₁ = chal_x_queried_gh.get σ₂ ∧ (chal_x_queried_gh.get σ₁ = false → ow_challenge_x.get σ₂ = x ∧ σ₁ = insRO x y σ₂))

theorem invUB_of_good {x : input} {y : output} {σ₁ σ₂ : state} (_hf : chal_x_queried_gh.get σ₂ = false) (hcx : ow_challenge_x.get σ₂ = x) (hσ : σ₁ = insRO x y σ₂) : InvUB x y σ₁ σ₂

theorem invUB_of_bad {x : input} {y : output} {σ₁ σ₂ : state} (h₁ : chal_x_queried_gh.get σ₁ = true) (h₂ : chal_x_queried_gh.get σ₂ = true) : InvUB x y σ₁ σ₂

theorem invUB_cases {x : input} {y : output} {σ₁ σ₂ : state} (h : InvUB x y σ₁ σ₂) : GoodPre✝ x y σ₁ σ₂ ∨ chal_x_queried_gh.get σ₁ = true ∧ chal_x_queried_gh.get σ₂ = true

Closed wp forms (the wp-tactic analogue)

theorem wp_lq_hit (inp : input) {σ : state} {v : output} (h : random_oracle_state.get σ inp = some v) (F : output × state → ENNReal) : (lazy_query inp).wp F σ = F (v, σ)

theorem wp_lq_miss (inp : input) {σ : state} (h : random_oracle_state.get σ inp = none) (F : output × state → ENNReal) : (lazy_query inp).wp F σ = ∑ v : output, F (v, random_oracle_state.set (fun (k : input) => if k = inp then some v else random_oracle_state.get σ k) σ) / ↑(Fintype.card output)

theorem wp_lqt (inp : input) (F : output × state → ENNReal) (σ : state) : (lazy_query_tracked inp).wp F σ = (lazy_query inp).wp (fun (yσ : output × state) => if inp = ow_challenge_x.get yσ.2 then F (yσ.1, chal_x_queried_gh.set true yσ.2) else F yσ) σ

Decompose lazy_query_tracked.wp into a lazy_query.wp with the flag-branching folded into the post.

theorem wp_set_seq_state {γ α : Type} (L : GaudisCrypt.Lens γ state) (v : γ) (P : GaudisCrypt.ProgramDenotation state α) (F : α × state → ENNReal) (σ : state) : (do GaudisCrypt.ProgramDenotation.set L v P).wp F σ = P.wp F (L.set v σ)

theorem wp_uniform_seq_state {α β : Type} [Fintype α] [Nonempty α] (k : α → GaudisCrypt.ProgramDenotation state β) (F : β × state → ENNReal) (σ : state) : (GaudisCrypt.ProgramDenotation.uniform >>= k).wp F σ = ∑ v : α, (k v).wp F σ / ↑(Fintype.card α)

The per-query coupling (the heart of the hop)

lazy_query_tracked inp relates to itself across insRO x y:

• inp ≠ x: both sides read the same cache entry — hit-hit returns the same value, miss-miss couples the fresh sample identically and the new entry commutes with the x-overwrite. Good post, equal values.
• inp = x: the left side hits the pre-programmed entry while the right side does whatever its cache says — but both set the flag. Bad post.

Proved by exhibiting one coupling per branch (relE.of_coupling), so both judgment directions come from a single case analysis.

Bad-phase unary side conditions (flag monotonicity and mass)

theorem lqt_flag_zero {inp : input} {F : output × state → ENNReal} (hF : ∀ (u : output × state), chal_x_queried_gh.get u.2 = true → F u = 0) {σ : state} (h : chal_x_queried_gh.get σ = true) : (lazy_query_tracked inp).wp F σ = 0

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

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

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

Indicator complement trick: full mass + zero on the complement gives mass 1 on the event.

theorem body_flag_zero (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) {F : Unit × state → ENNReal} (hF : ∀ (u : Unit × state), chal_x_queried_gh.get u.2 = true → F u = 0) {σ : state} (h : chal_x_queried_gh.get σ = true) : (oracle_step ow_adv lazy_query_tracked).wp F σ = 0

theorem wp_post_congr {α : Type} (p : GaudisCrypt.ProgramDenotation state α) {F G : α × state → ENNReal} (h : ∀ (u : α × state), F u = G u) (σ : state) : p.wp F σ = p.wp G σ

Pointwise post congruence for wp.

theorem body_mass (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_mass : ∀ (σ : state), ow_adv.wp (fun (x : Unit × state) => 1) σ = 1) (σ : state) : (oracle_step ow_adv lazy_query_tracked).wp (fun (x : Unit × state) => 1) σ = 1

noncomputable def finalSeg (y_v : output) : GaudisCrypt.ProgramDenotation state Bool

The verification segment shared by both games (parameterized by the challenge output y_v it compares against).

Equations

• finalSeg y_v = do let resp ← GaudisCrypt.ProgramDenotation.get ow_response let y_check ← lazy_query_tracked resp pure (decide (y_check = y_v))

The rectangular (after-bad) judgments

theorem body_bad_relE (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_mass : ∀ (σ : state), ow_adv.wp (fun (x : Unit × state) => 1) σ = 1) (x : input) (y : output) : (oracle_step ow_adv lazy_query_tracked).relE (oracle_step ow_adv lazy_query_tracked) (fun (σ₁ σ₂ : state) => chal_x_queried_gh.get σ₁ = true ∧ chal_x_queried_gh.get σ₂ = true) fun (u v : Unit × state) => InvUB x y u.2 v.2

The good-phase judgments

theorem body_good_relE (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (x : input) (y : output) : (oracle_step ow_adv lazy_query_tracked).relE (oracle_step ow_adv lazy_query_tracked) (GoodPre✝ x y) fun (u v : Unit × state) => InvUB x y u.2 v.2

theorem body_relE (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_cx : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_mass : ∀ (σ : state), ow_adv.wp (fun (x : Unit × state) => 1) σ = 1) (x : input) (y : output) : (oracle_step ow_adv lazy_query_tracked).relE (oracle_step ow_adv lazy_query_tracked) (InvUB x y) fun (u v : Unit × state) => InvUB x y u.2 v.2

The full loop-body judgment: Inv is preserved by one oracle step.

The game-level judgment

theorem ow_game_tracked_relE (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_cx : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_mass : ∀ (σ : state), ow_adv.wp (fun (x : Unit × state) => 1) σ = 1) (q : ℕ) : (ow_game_1_tracked ow_adv q).relE (ow_game_2_tracked ow_adv q) Eq fun (u v : Bool × state) => chal_x_queried_gh.get u.2 = chal_x_queried_gh.get v.2 ∧ (chal_x_queried_gh.get u.2 = false → u.1 = v.1 ∧ ∃ (y' : output), u.2 = insert_at_chal_x y' v.2)

The game-level judgment: tracked Game 1 and tracked Game 2 are related at "flags agree, and on good runs the results agree and the states differ only by the pre-programmed RO entry". All three up-to-bad theorems are corollaries.

The three theorems of the unary development, as corollaries

theorem ow_game_1_tracked_bad_eq_ow_game_2_tracked_bad (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_cx : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_mass : ∀ (σ : state), ow_adv.wp (fun (x : Unit × state) => 1) σ = 1) (q : ℕ) (σ : state) : (ow_game_1_tracked ow_adv q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then 1 else 0) σ = (ow_game_2_tracked ow_adv q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then 1 else 0) σ

Bad-event probability equality (the unary original needed a 138-line mass-conservation + ENNReal-cancellation chain).

theorem ow_game_1_tracked_le_ow_game_2_tracked_plus_bad (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_RO : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_cx : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_mass : ∀ (σ : state), ow_adv.wp (fun (x : Unit × state) => 1) σ = 1) (q : ℕ) (G : Bool × state → ENNReal) (h_G_RO_inv : ∀ (bσ : Bool × state) (y : output), G (bσ.1, insert_at_chal_x y bσ.2) = G bσ) (σ : state) : (ow_game_1_tracked ow_adv q).wp G σ ≤ (ow_game_2_tracked ow_adv q).wp G σ + (ow_game_1_tracked ow_adv q).wp (fun (bσ : Bool × state) => if chal_x_queried_gh.get bσ.2 = true then G bσ else 0) σ

The up-to-bad hop bound: Pr[G1 : G] ≤ Pr[G2 : G] + Pr[G1 : bad ∧ G].