OneWayness GameHop: Game 2 reduction

This module reduces Game 2's win event to the abstract guess_experiment framework, ultimately bounding it by (q+1)/|output|.

Game 2 components

• body_game_2, final_game_2 — direct query / response handlers (with explicit if y_val = y then set matched_chal_y true).
• env_game_2 — the prefix that samples y and tracks the matched flag.
• body_recording_game_2, final_recording_game_2 — recording variants that append each response to queries_output.
• q_body_game_2, q_final_game_2 — shared query subprograms; body_game_2 = q_body_game_2 >>= match_check_y and body_recording_game_2 = q_body_game_2 >>= record_to_qs. This decomposition fits the schema directly (no bridges needed).
• guess_experiment_game_2 — Game 2 as a guess_experiment instance.

Bridges and bound

• ow_game_2_tracked_wins_le_guess_experiment_game_2_matched — Game 2's win event ≤ guess_experiment_game_2 matched event.
• ow_game_2_tracked_bad_eq_guess_experiment_game_1 — Game 2's BAD event equals guess_experiment_game_1's matched event (used in UpToBad).
• ow_game_2_tracked_wins_le_guess_output_bound — full bound: Pr[Game 2 wins] ≤ (q+1)/|output|, by chaining the above into guess_experiment_le_interim_via_schema and guess_experiment_interim_wp_bound.

Length-bound helpers

ProgramDenotation.wp_qs_length_preserved_of_inFootprint, loop_n_wp_linear_bound, body_recording_game_2_qs_length_bump, etc. — used to discharge h_qs_length_le (the |queries| ≤ q+1 hypothesis of guess_experiment_interim_wp_bound).

The relational bridge: Game 2 wins ≤ guess-experiment matched

The two programs share their entire probabilistic structure (same prefix, same adversary loop, same final query); the guess experiment additionally maintains the write-only matched_chal_y flag. The coupling invariant is

InvM σ₁ σ₂ := ∃ b, σ₂ = matched_chal_y.set b σ₁

("the guess-experiment state is the game state with some matched-flag value on top"), and the final post is win → matched: when the game's verification succeeds (y_check = y), the experiment's final match-check fires. One rel judgment (only the ≤ direction is needed) replaces the former manual seq-descent and its body_v2/loop-conversion machinery.

Collector-based per-game instances and reductions

For each game, define body_recording and final_recording that record guesses into the appropriate queries list, then assume the per-game inequality guess_experiment_game_X ≤ guess_experiment_interim_game_X and the length invariant. This closes the chain via: Game → guess_experiment → guess_experiment_interim → (n+1)/|T|.

Game 2 schema: shared query subprograms for body and body_recording

For the schema-based correspondence, body_game_2 and body_recording_game_2 share a q_body_game_2 subprogram that returns the y_val value. Similarly for final.

theorem ow_game_2_tracked_wins_le_guess_output_bound (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv_matched_chal_y : ow_adv.inFootprint (GaudisCrypt.Lens.footprint matched_chal_y)ᶜ) (h_ow_adv_queries : ow_adv.inFootprint (GaudisCrypt.Lens.footprint queries_output)ᶜ) (h_ow_adv_chal_y : ow_adv.inFootprint (GaudisCrypt.Lens.footprint ow_challenge_y)ᶜ) (q : ℕ) (σ : state) : (ow_game_2_tracked ow_adv q).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ ≤ (↑q + 1) / ↑(Fintype.card output)

Game 2 wins bound: combines the direct bridge with the framework bound. Routes via guess_experiment_game_2 → interim → collector → bound. Uses the schema-based correspondence (no per-game ad-hoc lemma needed).