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.
Monotone relational simulateQ. A generalization of relTriple_simulateQ_run that
does not require equal per-query outputs. Instead, each per-query coupling must (a) preserve
the state invariant and (b) supply, for the same free-monad continuation applied to the two
(possibly different) coupled outputs, a recoupling of the two continued simulations preserving
the invariant. This is the right shape when the two handlers genuinely diverge on the answer
returned to the caller (e.g. an eager vs. deferred-sampling random-oracle read), so output
equality cannot be maintained and the coupling must be rebuilt across the branch point.
The continuation hypothesis is self-referential by design: discharging it is exactly the construction of the divergent-branch coupling, which is the hard probabilistic content this lemma isolates from the free-monad bookkeeping.
Marginal stochastic dominance from a coupling. If oa and ob are related by a
coupling whose post-relation R carries an event implication P a → Q b, then the marginal
probability of P on the left is at most that of Q on the right. This is the one-sided
(inequality) counterpart of evalDist_map_eq_of_relTriple: where the latter extracts a
distributional equality from output equality, this extracts a probability inequality from an
output implication. The proof reads off both marginals from the single coupling distribution
c and applies pointwise monotonicity of probEvent on c.
Projection: relational simulateQ preserving only output equality.
probEvent monotonicity between two relational simulateQ runs. Simulating the same adversary
oa under two StateT implementations related per query by rState (via
relTriple_simulateQ_run), any event implication that holds along the run postcondition
z₁.1 = z₂.1 ∧ rState z₁.2 z₂.2 transports to Pr[p | run impl₁] ≤ Pr[q | run impl₂]. The
simulateQ form of probEvent_le_of_relTriple; the events range over the full (output, state)
pair, so it covers output events, state events, and their conjunctions over the two
(output, state) spaces (the output type is shared; the state spaces σ₁/σ₂ differ).
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 #
Marginal stochastic dominance through simulateQ (self-referential / Fubini form).
The marginal counterpart of relTriple_simulateQ_run_mono. Where the latter demands a
pointwise per-step coupling whose support respects an output-and-state relation, this lemma
demands only a marginal per-step inequality: at every query and every pair of R-related
states, the one-step run of impl₁ followed by any left tail k₁ has bad-marginal at most
the one-step run of impl₂ followed by any right tail k₂, provided the two tails are
themselves marginally bad-dominated from every pair of R-related successor states.
This is the right shape when the two handlers genuinely diverge on the answer distribution at a
single step (e.g. an eager deterministic ghost read vs. a deferred-sampling read), so no
pointwise coupling can dominate the bad flag at that step, yet the marginal bad mass — the
tsum over the deferred draw, taken before the divergent continuation is applied — is still
ordered (Fubini / tsum-swap). The per-step premise is self-referential by design: discharging
it at the divergent step is exactly the marginal draw-commutation, the hard content this lemma
isolates from the free-monad bookkeeping.
The base hypothesis h_base (R s₁ s₂ → bad₁ s₁ → bad₂ s₂) discharges the pure leaf, where no
further step can repair the bad flag: there the bad marginal is exactly the indicator of the
current state, so R must already carry the bad implication.
Distribution-level stochastic dominance through simulateQ.
The distribution-level sibling of probEvent_marginal_simulateQ_mono. Where the latter carries
a pointwise state relation R : σ₁ → σ₂ → Prop and discharges the per-query step at every pair
of R-related states, this lemma carries a relation Rrun directly on the two run
distributions (the whole OracleComp spec₁ (γ × σ₁) / OracleComp spec₂ (γ × σ₂)
computations), generic over the output type γ. This is the shape needed when the per-step
recoupling is inherently joint-law — e.g. an eager handler that has already committed sampled
keys into its state versus a deferred-sampling handler that only carries a pending count, so that
no pointwise state predicate relates the two successor states yet the two run distributions are
related by a coupling over the deferred draw.
The induction is pure free-monad bookkeeping; the entire probabilistic content is isolated into the two premises:
h_pureseeds the relation at thepureleaves (the run distributions are the two point massespure (a, s₁)/pure (a, s₂));h_bindis the distribution-level bind congruence: given a querytand any two tailsk₁ k₂whose per-output continuations are alreadyRrun-related, the one-step runs followed by those tails are againRrun-related. Dischargingh_bindat a divergent step is the marginal draw-commutation, the hard content this lemma isolates.
Once the relation is established along the whole run, h_bad reads off the ordered bad marginals.
s₁ : σ₁, s₂ : σ₂ are the initial states and hbase : Rrun (pure …) …-free: instead the
seed is supplied through h_pure, applied at the actual reachable leaves during the induction, so
no separate base hypothesis on s₁ s₂ is required beyond what h_pure/h_bind carry.
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].
Exact identical-until-bad with output bad flag: joint heterogeneous variant #
tvDist_simulateQ_le_probEvent_output_bad fixes the inner monad to OracleComp spec
over the same spec as the simulated computation, and projects the conclusion to the
output marginal. The variant here generalizes the inner monad to OracleComp spec' and
keeps the conclusion on the joint output-and-state distribution, which is what a
game with a state-dependent continuation (e.g. a final verification step reading the
run's cache) consumes.
Bad-event equality for exact identical-until-bad, with the inner monad over an
arbitrary uniform spec spec'. Two state-extended implementations that agree on every
non-bad output transition from a non-bad input state (h_agree_good) and are bad-input
monotone (h_mono₁, h_mono₂) flip the output bad flag with exactly the same
probability. This is the equality counterpart of tvDist_simulateQ_run_le_probEvent_output_bad
(which bounds only the TV distance): the bad marginals coincide because the two runs differ
only on the already-bad trajectory, where both flags read true.
"Identical until bad" with an output bad flag, on the joint output-and-state
distribution, with the inner monad over an arbitrary uniform spec spec'.
Two state-extended oracle implementations that agree on non-bad output transitions from
non-bad input states (and are bad-input monotone) produce simulated runs whose joint
output-and-state distributions are within the probability of the flag firing in the run
of impl₁. Unlike tvDist_simulateQ_le_probEvent_output_bad, the conclusion keeps the
final state, so a state-dependent continuation (e.g. verification against the final
cache) can be appended on both sides.
ε-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'.
Query-bounded TV budget without a bad event #
When the two implementations agree exactly off the charged queries and no bad event is
tracked, the selective bound simplifies to a pure per-query budget qS * ε on the joint
output-and-state distribution, with no bad-flag plumbing in the state.
Query-bounded total-variation budget for simulateQ.
If two stateful oracle implementations agree exactly on every query outside a designated
set S, and on S-queries are within total-variation distance ε on the joint
answer-and-state distribution — uniformly in the carried state — then simulating any
computation making at most qS queries to S keeps the joint output-and-state
distributions within qS * ε, from any shared starting state.
This is the bad-event-free counterpart of
tvDist_simulateQ_run_le_queryBound_mul_slack_plus_probEvent_bad: the per-query budgets
telescope across the simulation by the triangle inequality, the hybrid for the i-th
charged query swapping which implementation answers it. Typical use: a signing oracle
whose real and simulated bodies are within ε from every shared random-oracle cache,
with all remaining oracles handled identically on both sides.
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) * β.
Expected-growth resource bound for expectedQuerySlack.
Like expectedQuerySlack_resource_le, but a charged query may grow the resource by more
than one in support, as long as it grows by at most g in expectation under the
handler. Growth queries grow the resource by at most one in support, and free queries
never grow it. The accumulated slack of a computation with at most qS charged and qH
growth queries is then at most qS·ζ + (qS·R s + qS·qH + C(qS,2)·g)·β, the binomial
cross term coming from the expected resource increase of earlier charged queries.
Charged-read / expected-growth resource bound for expectedQuerySlack.
A variant of expectedQuerySlack_expected_resource_le for the situation where the
charged queries never grow the resource (they only read it), while a separate class of
growth queries grows the resource by at most g in expectation (and may grow it by
arbitrarily much in support). Free queries never grow it.
Each charged query pays R s · β at the state s reached when it fires. Since the
charged queries do not grow R, and the growth queries grow it by at most g in
expectation, the resource seen by any charged query is at most R s₀ + qH · g in
expectation, where s₀ is the starting state and qH bounds the growth queries. Folding
the qS charged reads against this expected cap gives accumulated slack at most
qS · (R s₀ + qH · g) · β, with no (qS choose 2) cross-term and no dependence on
the in-support growth of the resource (which expectedQuerySlack_expected_resource_le
would charge through its h_growth/h_charged ≤ R p.1 + g shape).
This is the fold used by the ghost-read collision charge of the Fiat-Shamir-with-aborts
Prog → Trans hop, where the charged queries are the adversary's random-oracle reads (which
only grow the real cache, leaving the ghost cache R untouched) and the growth queries
are the signing queries (which grow the ghost cache by the number of rejected attempts, up
to maxAttempts − 1 in support but at most ∑_{a} p^a ≤ 1/(1−p) in expectation).
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.
Heterogeneous-state bad + slack simulateQ rule #
A fully heterogeneous (σ₁ ≠ σ₂, spec₁ ≠ spec₂) one-directional simulateQ induction
rule carrying both a monotone bad event on side 1 and per-charged-query slack ε.
Unlike the tvDist-based bounds above, this rule does not require the two simulations to
have the same output/state type: the conclusion is a one-directional Pr[= true]
inequality
Pr[= true | run' impl₁] ≤ Pr[= true | run' impl₂] + Pr[bad] + q · ε,
which is exactly the shape consumed by cross-domain crypto reductions that couple a
per-tag random oracle against a per-session one. The accounting term q · ε comes from
the charged-query budget IsQueryBoundP oa charged q.
Heterogeneous-state bad + slack simulateQ rule.
Couples two stateful oracle simulations with different state types σ₁, σ₂ and
different base specs spec₁, spec₂, related by a coupling invariant R. It carries a
monotone bad event bad on side 1 together with per-charged-query slack ε, charged
queries being designated by the predicate charged. If the computation oa makes at most
q charged queries (IsQueryBoundP oa charged q), then
Pr[= true | run' impl₁ oa] ≤ Pr[= true | run' impl₂ oa] + Pr[bad] + q · ε.
The per-query premise hstep is the bind-level coupling step: from R-related, non-bad
states, one query head together with any pair of continuations satisfying a continuation
bound yields the head-bind bound, paying ε for charged queries. This packages exactly
the obligation a concrete cross-domain reduction must discharge for its oracle pair.
Only impl₁ requires bad monotonicity (hmono), since the bound is one-directional and
mentions Pr[bad] only on side 1.
Single-world resource-charged bad accumulator #
A single-world accumulator bounding Pr[flag = true] for a stateful simulation whose
state σ × Bool carries a monotone resource R : σ → ℝ≥0∞ and a never-reset bad flag.
Unlike the identical-until-bad theorems above, which bound only the TV distance between two
worlds and treat Pr[output bad] as an additive remainder term they never bound, this
lemma bounds the bad-flag mass directly, by the resource-weighted query slack
expectedQuerySlack impl charged (fun s => R s · ε).
The per-step hypotheses are:
h_charged_step: at a charged (read) step from a non-bad state, the bad mass after the step-and-continuation is at mostR s · ε(the flip charge) plus the expected continuation bad mass;h_free_step: at a free step, no flip charge is paid.
Folding the resulting expectedQuerySlack against a resource bound (e.g. via
expectedQuerySlack_resource_le / expectedQuerySlack_expected_resource_le) yields a
closed-form bilinear bound.
Single-world resource-charged bad accumulator.
For simulateQ impl oa over a state σ × Bool (resource σ, never-reset bad flag), if
- every charged step pays a flip charge
R s · ε(h_charged_step), routing any further bad mass through its good (non-flagged) output states, while - every free step pays nothing and introduces no bad mass (
h_free_step),
then the probability the flag is set after the whole run from a non-bad state is bounded by
the resource-weighted query slack
expectedQuerySlack impl charged (fun s => R s * ε) oa qS (s, false). This is the
single-world, output-event analogue of
probEvent_fst_simulateQ_run_le_add_bad_add_slack: the inductive structure (good branch
reduced through the head bind by the per-step premise, bad output states discarded since
their slack is 0) is similar, but the conclusion bounds Pr[bad] itself rather than
carrying it as
an additive remainder.
Averaged-state-measure bad accumulator #
The single-world resource accumulator probEvent_bad_simulateQ_run_le_expectedQuerySlack
charges a flip cost R s · ε at a fixed reachable state s. That is exactly the right
shape for a handler that draws the hidden randomness at the read (the lazy /
deferred-sampling handler), where the per-state read charge is genuinely the averaged
guessing mass R s · ε < 1.
It is the wrong shape for an eager handler that commits the hidden draw upstream
(at signing time) and then reads it back deterministically: at a committed state s the
read-hit indicator 1_{mc ∈ slot(s)} is 0 or 1, never ε. The averaging that
produces ε happened earlier, at the commit draw, and cannot be localized to any fixed
read state.
The fix carried here is to average not over a single fixed state but over a state
measure ν : σ × Bool → ℝ≥0∞ — the law of the eager handler's slot under the pending
upstream draws. The averaged bad mass
avgBadM impl ν oa := ∑' p, ν p · Pr[bad | (simulateQ impl oa).run p]
telescopes through the free monad exactly like expectedQuerySlack, but the read step's
charge is now ∑' p, ν p · 1_{mc ∈ slot(p)} = Pr_{p∼ν}[mc ∈ slot(p)], a genuine
probability over the state law. When ν is the pushforward of the upstream commit draws,
this collapses (by Fubini / tsum-swap over the pending draws) to the same mass the lazy
handler charges at the read — probOutput_lazyGhostFire_one is its single-pending base
case. This is the missing-framework analogue of expectedQuerySlack: it carries a
state-law plus an averaged-output invariant rather than a per-state resource charge.
This section builds the reusable telescoping scaffold (avgBadM, its pure/query_bind
unfoldings, and the output-grouped step law avgBadM_query_bind_eq_tsum_output) and isolates
the read-step charge as the standalone Fubini lemma (tsum_tsum_postStepOutM_mul) the
instantiation must match against the lazy run.
Bare-measure averaged bad mass #
The scaffold is stated over a bare measure ν : σ × Bool → ℝ≥0∞ rather than a
probability law: the telescoping identities and the free-monad induction only ever use
ν p as an ℝ≥0∞ weight, and an aborting signing step produces a sub-probability
post-step state law (its total mass drops by the rejection mass), which a PMF-typed
average could not carry.
A caller (e.g. the deferred-sampling charge route) telescopes with
avgBadM_query_bind_eq_tsum_output directly at the sub-probability state laws produced by
the aborting sign step.
Bare-measure averaged bad mass. The per-state bad mass of a run, averaged against an
arbitrary measure ν : σ × Bool → ℝ≥0∞ rather than a probability law. No total-mass
constraint is needed by the telescoping, so the average carries the sub-probability
post-step laws emitted by an aborting step.
Instances For
avgBadM at a Dirac (single-point indicator) measure is the plain per-state bad
probability.
Linearity of avgBadM in the state measure. The averaged bad mass over ν is the
ν-weighted sum of the per-state (Dirac) bad masses.
Pure base case of avgBadM. With no queries, the bad mass is exactly the carried
bad mass of the measure ν — the ν-mass on states with the flag already set.
One-step telescoping of avgBadM (joint-law form). Moves one query off the front
and exposes the post-step joint law, holding for any impl and any measure ν. No
probabilistic content — pure rearrangement.
Post-step joint measure of a query step (bare-measure form). The measure over
(output, post-state) produced by averaging the per-state impl step Pr[= z | (impl t).run p]
against the state measure ν. Stated directly as a tsum since ν need not be a
probability law.
Instances For
Output-grouped telescoping of the bare-measure average. The telescoped one-step
average regroups as a single tsum over the post-step joint measure postStepJointM impl ν t,
weighting each (output, post-state) pair by the Dirac bad mass at the post-state.
Pure tsum-Fubini.
Per-output post-step state measure. Grouping the post-step joint measure
postStepJointM impl ν t by the query output u: the resulting state measure assigns to
each post-state s the joint mass of producing (u, s). The state coordinate of the
output-u slice of the post-step joint measure.
Instances For
Output-grouped one-step telescoping of avgBadM. The telescoped one-step average
regroups as a tsum over the query output u, each weighted by the averaged bad mass of
the continuation cont u run from the per-output post-step state measure
postStepOutM impl ν t u. This is the form the threaded-charge induction consumes: it
applies the inductive hypothesis once per output, at a genuine state measure (not a Dirac),
so the per-target charge of the post-step measure can be bounded as a measure (avoiding the
∑-of-⨆ blow-up of the per-post-state Dirac grouping).
Weighted post-step rearrangement. Summing any post-state functional F against the
post-step measure (over output u and post-state s) equals the ν-average of the per-state
expected value of F after one impl step. The Fubini bridge used to push a per-state charge
bound (e.g. ghost-size or membership-charge growth) through the post-step measure.