One-wayness via game hopping

A proof from first principles that for any adversary against a random oracle making at most q queries:

  P[OW experiment wins]  ≤  2 (q + 1) / |output|

Proof structure

                                       ow_game_0_eq_ow_game_1
  ow_experiment  ==  ow_game_0  ==========================>  ow_game_1
                                  (program equality)              ║
                                                                  ║ flag-elision
                                                                  ║ (tracking
                                                                  ║  invisible
                                                                  ║  at flag-
                                                                  ║  ignoring
                                                                  ║  posts)
                                                                  ║
                                                                  ▼
                                                          ow_game_1_tracked
                                                                  ║
                                                                  ║ up-to-bad
                                                                  ║ (Game 1 ─ Game 2
                                                                  ║   identical
                                                                  ║   until adv
                                                                  ║   queries
                                                                  ║   chal_x)
                                                                  ▼
                                                          ow_game_2_tracked
                                                          + bad event
                                            ┌───────────────┴──────────┐
                                            ▼                          ▼
                                     win event in G2              bad event
                                            │                          │
                                            │ Game 2 → guess-          │ Game 1 → guess-
                                            │ experiment_game_2        │ experiment_game_1
                                            │ (matched_chal_y)         │ (chal_x_queried_gh)
                                            ▼                          ▼
                                  ≤ (q+1)/|output|              ≤ (q+1)/|input|
                                                                       │
                                                                       │ |input| ≥ |output|
                                                                       ▼
                                                                ≤ (q+1)/|output|
                                            └──────────────┬───────────┘
                                                           ▼
                                                ≤ 2(q+1)/|output|

Module layout

• Definitions — the three games (ow_game_0, ow_game_1, ow_game_2), their tracked variants, the tracking flag chal_x_queried_gh, the matched flag matched_chal_y, the query-recording lists queries_input/queries_output, all disjointness axioms.
• GuessExperiment — the abstract guessing-game framework (guess_experiment, guess_experiment_interim, schema_inner_equation, guess_experiment_le_interim_via_schema, guess_experiment_interim_wp_bound). Reduces both Game 2 wins and Game 1 bad to a single bound ≤ (q+1)/|T|.
• UpToBad — the identical-until-bad analysis bridging Game 1 to Game 2. Contains RO-invariance machinery, mass-conservation lemmas, and the up_to_bad-style decomposition.
• Game1 — Game 1 specifics: bridges Game 1 to Game 1' (a schema-friendly variant with explicit if inp = t then set chal_x_queried_gh true), game_1_correspondence, and the bad-event bound.
• Game2 — Game 2 specifics: schema decomposition (q_body_game_2, q_final_game_2), win-event bound.

The master theorem

ow_lazy_bound_via_gamehop (this file) chains everything together.

theorem ow_lazy_bound_via_gamehop (ow_adv : GaudisCrypt.ProgramDenotation state Unit) (h_ow_adv : 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_matched_chal_y : ow_adv.inFootprint (GaudisCrypt.Lens.footprint matched_chal_y)ᶜ) (h_ow_adv_queries_output : ow_adv.inFootprint (GaudisCrypt.Lens.footprint queries_output)ᶜ) (h_ow_adv_queries_input : 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_experiment ow_adv q lazy_init lazy_query).wp (fun (bσ : Bool × state) => if bσ.1 = true then 1 else 0) σ ≤ 2 * (↑q + 1) / ↑(Fintype.card output)

The OW lazy bound via the game-hop chain. Matches the existing ow_lazy_bound (in QueryHit.lean), proved via the game-hopping + up-to-bad chain.