OneWayness GameHop: Guess Experiment Framework #
This module provides the abstract guessing-game machinery that abstracts both the win and bad events in the OW chain. Used by both Game 1's bad-event reduction and Game 2's win-event reduction.
Core combinators #
loop_n n body— iteratebodyexactlyntimes.guess_experiment env sample tvar mvar body final n— the abstract guessing experiment. Adversary makesnqueries, then afinalquery; we count whether the matched flag fires.guess_experiment_interim— the same experiment but with a recording list collecting all adv queries (sampling happens FIRST).guess_experiment_collector— equivalent recording form with sampling commuted past the recording loop.
Bounds #
guess_experiment_collector_wp_bound : (collector).wp post σ ≤ (n+1)/|T|— the heart of the bound, viauniform_wp_mem_le.guess_experiment_interim_eq_collector— interim = collector byProgramDenotation.bind_uniform_commapplied 3 times.guess_experiment_interim_wp_bound— composed bound: interim ≤ (n+1)/|T|.
Schema (per-game correspondence) #
guess_experiment_le_interim_assumption— given a per-σ', t correspondence (h_correspondence), bounds guess_experiment by guess_experiment_interim.schema_inner_equation— the per-σ', t equation, proven structurally for any body decomposed asq >>= match_checkandbody_recordingasq >>= record.guess_experiment_le_interim_via_schema— combines the above two: applies to any game whose body fits the schema'sq >>= ...form.
Game 2's body fits directly. Game 1's needs the bridges in Game1.lean to
convert to Game 1' form.
Generic guessing-game combinators #
The framework for cryptographic guess-game reductions. loop_n is a
plain bounded loop; guess_experiment is the unifying "n+1 attempts to
hit a uniform target" game.
A generic "guess the uniform target" experiment.
The key generalization vs prior versions: the body and final
iterations are parameterized by the target t. Each iteration can
use the bound target directly in match-checks (no state extracts
required). This unifies two shapes of match-check that arise in OW:
- Input-side match (Game 1 bad): lazy_query_tracked already
tracks input matches internally via
chal_x_queried_gh; the body doesn't need an explicit match-check (it ignores its target param). - Output-side match (Game 2 win-bound): body explicitly does
if y_val = t then set matched_var trueusing boundy_valandt.
Returns the matched flag's final value (Bool). Cryptographic reductions relate ow_game_*'s win/bad events to the matched flag via specialized bridges.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Collector-game route to the bound. #
ALTERNATIVE architectural approach: introduce a collector version of
guess_experiment that:
- Doesn't sample the target during the loop.
- Records each iteration's "comparison value" into a list.
- Samples target uniformly at the END, then checks if it lies in the recorded list.
The bound on the collector is then a one-line application of "uniform
sample ∈ finite list of length ≤ n+1 has probability ≤ (n+1)/|T|". The
deferred-sampling content becomes a single equivalence proof
guess_experiment ≤ guess_experiment_collector.
Interim form of guess_experiment: same as the collector but with the
target sampled FIRST (like guess_experiment) instead of last.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generic bound: guess_experiment.wp ≤ guess_experiment_interim.wp (with
sample_target = ProgramDenotation.uniform).
The cryptographic content is in h_correspondence: a per-state bound
that the LHS's matched-fire after the loop+final is at most the RHS's
t ∈ qs after recording+final_recording. This bound must be discharged
at each instantiation — the proof here just peels the common env and
uniform t prefix.
Schema's inner per-σ', t equation: the per-σ', t correspondence that
guess_experiment_le_interim_via_schema uses to discharge the
h_correspondence of guess_experiment_le_interim_assumption.
Proved relationally: this is PRHLSchema.schema_inner_equation_prhl
(PlonkLean/PRHL/Clients/SchemaInnerEquation.lean), one synchronized
loop invariant matched₁ = (t ∈ qs₂) in the pRHL calculus. The former
unary proof (~280 lines plus ~700 lines of private support lemmas,
maxHeartbeats 1600000) was removed in favor of it.
Reusable for other game-level proofs (e.g., game_1_correspondence) that
need the inner equation directly without going through the full schema.
Schema-based correspondence: when body and body_recording both
decompose as q >>= ... for some shared "query" subprogram q, with
body's tail being a match-check against t and body_recording's tail
appending to queries_list_var, the per-state correspondence (the
h_correspondence hypothesis of guess_experiment_le_interim_assumption)
is provable structurally via schema_inner_equation.
q_body and q_final are the shared subprograms for the loop and the
final iteration respectively. They may differ (e.g., body does adv query
via oracle_input, final does response check via ow_response).
Interim wp bound: by interim = collector + collector bound. Generic.
Helpers for length-bound proofs #
For a program p that doesn't write to qs_var, the expected list
length at output is bounded by the initial length (up to mass ≤ 1).