Relational simulateQ Rules #
This file provides the highest-leverage theorems for game-hopping proofs: relational coupling through oracle simulation, and the "identical until bad" lemma.
Main results #
relTriple_simulateQ_run: If two stateful oracle implementations are related by a state invariant and produce equal outputs, then simulating a computation with either implementation preserves the invariant and output equality.relTriple_simulateQ_run': Projection that only asserts output equality.tvDist_simulateQ_le_probEvent_bad: "Identical until bad" — if two oracle implementations agree whenever a "bad" flag is unset, the TV distance between their simulations is bounded by the probability of bad being set.
Relational simulateQ rules #
Core relational simulateQ theorem with state invariant.
If two oracle implementations produce equal outputs and preserve a state invariant R_state,
then the full simulation also preserves the invariant and output equality.
Projection: relational simulateQ preserving only output equality.
Exact-distribution specialization of relTriple_simulateQ_run'.
If corresponding oracle calls have identical full (output, state) distributions whenever the
states are equal, then the simulated computations have identical output distributions. This
packages the common pattern "prove per-query evalDist equality, then use Eq as the state
invariant" into a single theorem.
WriterT analogue of relTriple_simulateQ_run.
If two writer-transformed oracle implementations produce outputs related by a reflexive-and-closed
relation R_writer on the accumulated logs, then the full simulation preserves output equality
together with the accumulated-log relation.
hR_one witnesses reflexivity at the empty accumulator (the run-start value), and hR_mul
closes R_writer under the monoid multiplication used by WriterT's bind. Together these make
R_writer a monoid congruence on the two writer spaces, which is precisely the structural
requirement for whole-program accumulation.
WriterT analogue of relTriple_simulateQ_run_of_impl_eq_preservesInv.
If two writer-transformed oracle implementations agree pointwise on
.run (i.e. every per-query increment is identical as an OracleComp),
then the whole simulations yield identical (output, accumulator)
distributions.
WriterT handlers are stateless (.run takes no argument), so the
hypothesis is a plain equality rather than an invariant-gated
implication. The postcondition is strict equality on α × ω.
Output-probability projection of
relTriple_simulateQ_run_writerT_of_impl_eq: two WriterT handlers with
pointwise-equal .run yield identical (output, accumulator) probability
distributions.
evalDist equality projection of
relTriple_simulateQ_run_writerT_of_impl_eq.
Projection of relTriple_simulateQ_run_writerT onto the output component.
If two stateful oracle implementations agree on every query while Inv holds, and the
second implementation preserves Inv, then the full simulations have identical (output, state)
distributions from any invariant-satisfying initial state.
Exact-equality specialization of relTriple_simulateQ_run_of_impl_eq_preservesInv.
This weakens the stronger invariant-carrying postcondition to plain equality on (output, state),
which is the shape consumed directly by probability-transport lemmas and theorem-driven
rvcgen steps.
Output-probability projection of
relTriple_simulateQ_run_of_impl_eq_preservesInv.
Query-bounded exact-output transport for simulateQ.
If oa satisfies a structural query bound IsQueryBound budget canQuery cost, the two
implementations agree on every query that the bound permits, and the second implementation
preserves a budget-indexed invariant Inv, then the full simulated computations have identical
output-state probabilities from any initial state satisfying Inv.
Relational transport corollary of OracleComp.run'_simulateQ_eq_of_query_map_eq
(SimSemantics/StateProjection.lean): under the same per-step projection hypothesis, the two
output distributions are related by equality.
"Identical until bad" fundamental lemma #
The fundamental lemma of game playing: if two oracle implementations agree whenever a "bad" flag is unset, then the total variation distance between the two simulations is bounded by the probability that bad gets set.
Both implementations must satisfy a monotonicity condition: once bad s holds, it must
remain true in all reachable successor states. Without this, the theorem is false — an
implementation could enter a bad state (where agreement is not required), diverge, and
then return to a non-bad state, producing different outputs with Pr[bad] = 0.
Monotonicity is needed on both sides because the proof establishes pointwise equality
Pr[= (x,s) | sim₁] = Pr[= (x,s) | sim₂] for all ¬bad s, which requires ruling out
bad-to-non-bad transitions in each implementation independently.
Distributional "identical until bad" #
The _dist variant weakens the agreement hypothesis from definitional equality
(impl₁ t).run s = (impl₂ t).run s) to distributional equality
(∀ p, Pr[= p | (impl₁ t).run s] = Pr[= p | (impl₂ t).run s]).
This is needed when the two implementations differ intensionally but agree on
output probabilities.
Distributional variant of tvDist_simulateQ_le_probEvent_bad:
weakens the agreement hypothesis from definitional equality to distributional equality
(pointwise equal output probabilities).
"Identical until bad" with an output bad flag #
These variants record the bad event in the output state of each oracle step (not the input).
The state has shape σ × Bool with the second component a monotone bad flag, and the two
implementations may disagree on the very step that flips the flag. The standard pointwise
agreement hypothesis of tvDist_simulateQ_le_probEvent_bad{,_dist} is too strong here: at the
firing step, the input is non-bad but the outputs already differ. The output-bad pattern is the
exact shape of QueryImpl.withProgramming (which sets bad := true only on policy-firing
steps) and the programming_collision_bound argument that builds on it.
"Identical until bad" with the bad flag tracked at the output of each oracle step.
TV-distance between two state-extended simulations is bounded by the probability of the flag
firing in the run of impl₁.
Compared to tvDist_simulateQ_le_probEvent_bad{,_dist}, this version weakens the
agreement hypothesis: the two implementations need only agree on non-bad output transitions
from non-bad input states. They may disagree arbitrarily on the very step that flips the flag.
Both implementations must satisfy bad-input monotonicity: once b = true in the input state of
a step, every reachable output also has b = true.
Ergonomic wrapper of tvDist_simulateQ_le_probEvent_output_bad for the very common case
where the underlying oracle implementations live in StateT σ (OracleComp spec) and have been
lifted to StateT (σ × Bool) (OracleComp spec) by attaching a bad flag.
This is the exact shape consumed by the QueryImpl.withProgramming collision-bound argument:
the impls agree on (s, false) input modulo the rare programming-fired step, and the bound
is the probability of any policy hit during the run.
ε-perturbed "identical until bad" with output bad flag #
These lemmas generalize tvDist_simulateQ_le_probEvent_output_bad from EXACT agreement on
the no-bad path to ε-CLOSE agreement: the per-step TV distance between the two oracle
implementations may be at most ε (instead of zero) on the no-bad path. Combined with a
query bound q on the computation, the total bound becomes q*ε + Pr[bad].
The standard "identical until bad" bound (Pr[bad]) is recovered as the special case ε = 0.
Application: HVZK simulation in Fiat-Shamir, where the simulated transcript is only
ε-close to the real transcript per query (not exactly equal), but a "programming
collision" event captures the catastrophic failure mode (collision between programmed hash
entries). The total reduction loss is qS·ε + Pr[collision].
ε-perturbed identical-until-bad: helper lemmas (in dependency order) #
ε-perturbed identical-until-bad with output bad flag.
If two stateful oracle implementations are ε-CLOSE in TV distance per step on the no-bad
path (instead of exactly equal as in tvDist_simulateQ_le_probEvent_output_bad), and the
computation makes at most q queries, then the TV distance between the two simulations
is bounded by q*ε + Pr[bad].
Only impl₁ requires bad-flag monotonicity (since the bound uses Pr[bad | sim₁]); the
"true" branch in the inductive proof exploits monotonicity to push Pr[bad | sim₁] = 1
which dominates the trivial tvDist ≤ 1 bound.
The ε = 0 case recovers the existing identical-until-bad bound (modulo the upgraded
agreement hypothesis from definitional equality to TV-distance equality, which is
equivalent for distributions over the same type).
Selective ε-perturbed identical-until-bad #
A refinement of tvDist_simulateQ_le_qeps_plus_probEvent_output_bad where the per-step ε
bound applies only to a designated subset S of queries (the "costly" or "perturbed"
queries), and the impls are pointwise equal on the complement (the "free" queries). The
bound counts only the charged queries, giving a tight q · ε instead of q_total · ε.
This is essential for cryptographic reductions where, e.g., signing-oracle queries are
ε-close to a simulator (HVZK guarantee) but uniform / RO queries are exactly equal (both
sides forward through the same RO cache). Direct application of the uniform-ε lemma would
give (qS + qH) · ε, but for tight bounds we want q · ε.
Selective ε-perturbed identical-until-bad with output bad flag.
Like tvDist_simulateQ_le_qeps_plus_probEvent_output_bad, but the per-step ε bound
applies only to queries t satisfying a designated predicate S (the "costly" queries),
and the impls are pointwise equal on ¬ S (the "free" queries). The bound counts only
the charged queries (via IsQueryBoundP oa S qS), giving the tight q · ε instead of the
trivial q_total · ε from the uniform-ε lemma.
The intended use is for cryptographic reductions: e.g., for Fiat-Shamir signing-oracle
swaps, the "costly" queries are signing queries (HVZK gives per-query ε bound) and the
"free" queries are the underlying spec queries (uniform sampling and RO caching, where
both sides forward through the same baseSim).
Selective ε-perturbed identical-until-bad with output bad flag.
Like tvDist_simulateQ_run_le_queryBound_mul_slack_plus_probEvent_bad, but projected to the
computation output via StateT.run'.
State-dep ε-perturbed identical-until-bad #
A further refinement of tvDist_simulateQ_le_queryBound_mul_slack_plus_probEvent_bad where the
per-step ε bound is allowed to depend on the input state s : σ to the impl. The
bound on tvDist is then expressed as the expected sum of ε s over the trace of
charged queries fired during the simulation, captured by the recursive function
expectedQuerySlack.
This is essential for cryptographic reductions where the per-step gap depends on a varying
state quantity (e.g., for Fiat-Shamir signing-oracle swaps the gap is
ζ_zk + |s.cache| · β, growing with cache size, with no uniform constant ε).
The constant-ε lemma tvDist_simulateQ_run_le_queryBound_mul_slack_plus_probEvent_bad
is a corollary.
To sidestep summability obligations, expectedQuerySlack is valued in ℝ≥0∞ and the
bridge lemma is stated in ℝ≥0∞ via ENNReal.ofReal (tvDist …).
Per-query_bind step of expectedQuerySlack. Given the impl, the charged-query
predicate S, the per-state query slack ε, the query symbol t, and the IH continuation
k : Range t → ℕ → (σ × Bool) → ℝ≥0∞, returns the expected cost contributed by
performing the query t from state p with budget qS:
- if the bad flag is set in
p, return0(thePr[bad]term swallows the deficit); - if
tis a uncharged query (¬ S t), forward through the impl with budget unchanged; - if
tis a charged query and the budget is exhausted, return0(vacuous viaIsQueryBound); - if
tis a charged query with positive budget, payε p.1immediately, then forward through the impl with budget decremented toqS - 1.
Instances For
Recursive expected accumulated query slack over the charged queries fired during
(simulateQ impl oa).run p. Defined by recursion on oa via OracleComp.construct.
Instances For
Pointwise monotonicity of expectedQuerySlack in ε #
If ε ≤ ε' pointwise (as functions σ → ℝ≥0∞), then
expectedQuerySlack impl S ε oa qS p ≤ expectedQuerySlack impl S ε' oa qS p.
The analogous monotonicity in the continuation k (for
expectedQuerySlackStep) is the step-level lemma, used in the inductive
step of expectedQuerySlack_mono. These lemmas are used to bound a
state-dependent ε by a constant upper bound so the constant-ε bound
expectedQuerySlack_const_le_queryBudget_mul applies.
Invariant support congruence for expectedQuerySlack #
If two per-state query slack functions agree on an invariant and the real handler preserves
that invariant from no-bad states, then expectedQuerySlack is insensitive to their values on
unreachable states.
The input hypothesis is phrased as p.2 = false → Inv p.1 so that bad states remain
vacuous: expectedQuerySlack is definitionally zero once the bad flag is set.
Helper lemma: per-summand IH bound implies the bind-sum bound #
Per-step inductive helpers #
Inductive auxiliary lemma #
Public bridge lemmas #
State-dep ε-perturbed identical-until-bad with output bad flag (joint state).
Like tvDist_simulateQ_run_le_queryBound_mul_slack_plus_probEvent_bad, but the
per-step ε bound is allowed to depend on the input state s : σ to the impl.
The q · ε term is replaced by the expected accumulated query slack over
the trace of charged queries fired during simulation, captured by
expectedQuerySlack.
Statement is in ℝ≥0∞ to sidestep summability obligations on the query-slack trace.
State-dep ε-perturbed identical-until-bad with output bad flag (projected output).
Composing the joint-state lemma with the projection Prod.fst : α × σ × Bool → α, which
can only decrease TV distance (data-processing inequality tvDist_map_le).
Constant-ε corollary (Phase A2 regression) #
Specializing expectedQuerySlack to a constant query-slack function fun _ => ε and using
IsQueryBoundP to bound the number of charged queries, the accumulated slack is dominated by
q · ε. Combined
with the state-dep main lemma this re-derives the selective constant-ε bound
in ENNReal form.
State-dependent resource bound for expectedQuerySlack.
If each charged query pays ζ + R s * β, and the resource R can increase by
at most one on charged or growth queries and never increases otherwise, then a
computation with at most qS charged queries and at most qH growth queries
has accumulated slack at most
qS * ζ + qS * (R s + qS + qH) * β.
Constant-ε version of the bridge as a corollary of the state-dep version.
This is the ENNReal-form analogue of the existing real-valued
tvDist_simulateQ_run_le_queryBound_mul_slack_plus_probEvent_bad. It demonstrates that
the state-dep version subsumes the constant-ε version: instantiate
ε := fun _ => ENNReal.ofReal ε_const and bound expectedQuerySlack by
queryBudget * ENNReal.ofReal ε_const.