OneWayness GameHop: Game 1 reduction

This module reduces Game 1's bad event (chal_x_queried_gh = true) to the abstract guess_experiment framework, ultimately bounding it by (q+1)/|input|.

Game 1 variants

• body_game_1, final_game_1 — direct query / response handlers.
• body_recording_game_1, final_recording_game_1 — recording variants that append each query to queries_input.

Correspondence (relational)

game_1_correspondence couples the match-tracking run to the recording run with one pRHL invariant (see InvG1 below); the former Game 1' explicit-match variants and their bridge lemmas are gone.

• game_1_correspondence — Game 1's per-σ', t inequality (LHS ≤ RHS in schema form), proven by chaining: bridges → schema_inner_equation for Game 1' → reverse bridges.
• ow_game_1_tracked_bad_le_guess_input_bound — full bound: Pr[Game 1 bad] ≤ (q+1)/|input|.

Flag-elision (lazy ↔ tracked)

ow_game_1_wp_eq_ow_game_1_tracked_wp_of_flag_ignoring — at flag-ignoring posts, Game 1's lazy oracle and tracked oracle are wp-equivalent. Bridges the OW theorem's "lazy" Game 1 to our "tracked" Game 1.

noncomputable def body_game_1 (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (_x : input) : GaudisCrypt.ProgramDenotation state Unit

Body of guess_experiment_game_1: adv query + lazy_query_tracked (which internally flips chal_x_queried_gh when inp = chal_x). Doesn't use the bound target x.

Equations

• body_game_1 ow_adv _x = do ow_adv let inp ← GaudisCrypt.ProgramDenotation.get oracle_input let y ← lazy_query_tracked inp GaudisCrypt.ProgramDenotation.set oracle_output y

noncomputable def final_game_1 (_x : input) : GaudisCrypt.ProgramDenotation state Unit

Final of guess_experiment_game_1: oracle on response. Doesn't use the bound target.

Equations

• final_game_1 _x = do let resp ← GaudisCrypt.ProgramDenotation.get ow_response let y ← lazy_query_tracked resp GaudisCrypt.ProgramDenotation.set oracle_output y

theorem lazy_query_tracked_inFootprint_queries_input (inp : input) : (lazy_query_tracked inp).inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ

lazy_query_tracked is queries_input-disjoint.

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

Body recording for Game 1 bad: same shape as guess_experiment_game_1.body but appends inp (adv's query) to qs.

Equations

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

noncomputable def final_recording_game_1 : GaudisCrypt.ProgramDenotation state Unit

Final recording for Game 1 bad: the last query attempt records resp.

Equations

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

theorem body_recording_game_1_qs_length_bump (adv : GaudisCrypt.ProgramDenotation state Unit) (h_adv : adv.inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ) (σ : state) : (body_recording_game_1 adv).wp (fun (aσ : Unit × state) => ↑(queries_input.get aσ.2).length) σ ≤ ↑(queries_input.get σ).length + 1

body_recording_game_1 bumps queries_input.length by at most 1 per iteration.

theorem final_recording_game_1_qs_length_bump (σ : state) : final_recording_game_1.wp (fun (aσ : Unit × state) => ↑(queries_input.get aσ.2).length) σ ≤ ↑(queries_input.get σ).length + 1

final_recording_game_1 bumps queries_input.length by at most 1.

The relational correspondence

The match-tracking run (left: body_game_1, whose lazy_query_tracked flips chal_x_queried_gh when the query equals chal_x = t) is coupled to the recording run (right: body_recording_game_1, which appends each query to queries_input) by the invariant InvG1 below: the recording state is the tracking state with the three bookkeeping lenses overwritten; the left flag mirrors membership of the target in the recorded list; the left challenge is pinned to the target. The right flag value m is existential — the right run's lazy_query_tracked junk-flips it against tv = chal_x.get σ', and the ending overwrites it anyway.

This one invariant replaces the entire former Game 1' apparatus (the explicit-match variants, eight bridge lemmas, the queries-input invisibility block, and two maxHeartbeats game-level conversions — see git history).

@[reducible, inline]

abbrev InvG1 (t tv : input) (σ₁ σ₂ : state) : Prop

The Game-1 coupling invariant.

Equations

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

theorem ending_g1_rel (t tv : input) : (GaudisCrypt.ProgramDenotation.get chal_x_queried_gh).rel (do let qs ← GaudisCrypt.ProgramDenotation.get queries_input GaudisCrypt.ProgramDenotation.set chal_x_queried_gh (decide (t ∈ qs)) GaudisCrypt.ProgramDenotation.get chal_x_queried_gh) (InvG1 t tv) fun (u v : Bool × state) => u.1 = v.1

The ending: reading the tracking flag (left) returns the same boolean as the deferred membership test (right).

theorem body_game_1_rel (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_cx : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_qi : ow_adv.inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ) (t tv : input) : (body_game_1 ow_adv t).rel (body_recording_game_1 ow_adv) (InvG1 t tv) fun (u v : Unit × state) => InvG1 t tv u.2 v.2

Loop-body judgment: one tracking step vs one recording step.

theorem game_1_correspondence (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv_chal_x : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_ow_adv_chal_x_qg : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_ow_adv_qi : ow_adv.inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ) (q : ℕ) (σ' : state) (t : input) : (do GaudisCrypt.ProgramDenotation.set ow_challenge_x t GaudisCrypt.ProgramDenotation.set chal_x_queried_gh false GaudisCrypt.loop_n q (body_game_1 ow_adv t) final_game_1 t GaudisCrypt.ProgramDenotation.get chal_x_queried_gh).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ' ≤ (do GaudisCrypt.ProgramDenotation.set queries_input [] GaudisCrypt.loop_n q (body_recording_game_1 ow_adv) final_recording_game_1 let qs ← GaudisCrypt.ProgramDenotation.get queries_input GaudisCrypt.ProgramDenotation.set chal_x_queried_gh (decide (t ∈ qs)) GaudisCrypt.ProgramDenotation.get chal_x_queried_gh).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ'

Game 1 correspondence, relationally: the tracking flag fires iff the target lands in the recorded query list. One synchronized invariant (InvG1) through the loop, the final query, and the ending.

theorem ow_game_1_tracked_bad_le_guess_input_bound (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv_RO : ow_adv.inFootprint (GaudisCrypt.Lens.footprint random_oracle_state)ᶜ) (h_ow_adv_chal_y : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_y)ᶜ) (h_ow_adv_chal_x : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_x)ᶜ) (h_ow_adv_chal_x_queried_gh : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (h_ow_adv_queries : ow_adv.inFootprint (GaudisCrypt.Lens.footprint queries_input)ᶜ) (h_ow_adv_mass_one : ∀ (σ : 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) σ ≤ (↑q + 1) / ↑(Fintype.card input)

Reduction: bad-in-Game-1 ≤ Guess(input, q+1).

Routes via guess_experiment_game_1 → interim → collector → bound.

Flag-elision bridge: untracked Game 1 ↔ tracked Game 1

For postconditions that don't read chal_x_queried_gh, the tracked and untracked variants of Game 1 agree at the wp level.

theorem ow_game_1_wp_eq_ow_game_1_tracked_wp_of_flag_ignoring (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv_flag : ow_adv.inFootprint (GaudisCrypt.Lens.footprint chal_x_queried_gh)ᶜ) (q : ℕ) (F : Bool × state → ENNReal) (h_F : GaudisCrypt.IgnoresLens chal_x_queried_gh F) (σ : state) : (ow_game_1 ow_adv q).wp F σ = (ow_game_1_tracked ow_adv q).wp F σ

Flag elision at the game level: ow_game_1 and ow_game_1_tracked have equal wp's for flag-ignoring postconditions.

Proof via the EquivModuloLens calculus: bind congruence chains compose oracle_loop_n_equiv (loop-level), lazy_query_equiv_lazy_query_tracked (final query), and set_equiv_pure (initial set chal_x_queried_gh false).