TV-distance bound for withProgramming vs withCaching #
The headline theorem tvDist_simulateQ_withCaching_withProgramming_le_probEvent_bad bounds
the total variation distance between the output distribution of withCaching and the output
distribution of withProgramming policy by the probability that the bad flag of
withProgramming policy ever fires (i.e., the adversary queries a point on which policy is
defined).
The proof factors through the auxiliary withCachingTrackingPolicy (defined alongside
withProgramming in OracleComp/QueryTracking/ProgrammingOracle.lean):
- On every step from non-bad input
(cache, false), the head distributions ofwithProgramming policyandwithCachingTrackingPolicy policyagree on non-bad outputs. On policy-firing steps, both implementations produce only bad outputs (with possibly different(value, cache)components). This is the exact shape consumed byOracleComp.ProgramLogic.Relational.identical_until_bad_with_flag. withCachingTrackingPolicy_run'_eqprojectswithCachingTrackingPolicytowithCachingon the output marginal, eliminating the auxiliary impl from the user-facing statement.
The bound applies to any underlying so : QueryImpl spec (OracleComp spec), with the policy
acting on inputs of spec.
Programming collision bound #
Built directly on top of the headline TV-distance bound, programming_collision_bound is the
"collision-event" repackaging used by Fiat-Shamir-style identical-until-bad reductions: given
any upper bound B on probEventBadOfWithProgramming so policy oa, the TV-distance between
the unprogrammed and programmed runs is at most B.toReal. The convenience wrapper
programming_collision_bound_qP_qH_β specializes B to the textbook qP * qH * β shape so
callers only need to discharge a union-bound hypothesis. Both live in this Relational
namespace because they are TV-distance statements; the underlying withProgramming /
withCaching definitions and the HasUnpredictableSample typeclass remain in
QueryTracking/.
Per-step distributional agreement on non-bad outputs #
TV-distance bound #
TV-distance between the output marginal of so.withCaching and the output marginal of
so.withProgramming policy is bounded by the probability that the bad flag of
withProgramming policy fires (i.e., the adversary queries a programmed point) during the run.
This is the user-facing "identical until bad" bound: programming a random oracle is indistinguishable from the unprogrammed oracle until the adversary queries a programmed point. The bound is one-sided in the natural way for "ratchet" arguments: it controls the answer distribution under the unprogrammed oracle by the bad-event probability under the programmed oracle.
Programming collision bound #
The bad-event probability of withProgramming policy on input oa, started from an empty
cache and bad := false. The bad flag flips on the first cache-miss whose query input lies in
the policy's support; this abbreviation isolates that probability so downstream union-bound
arguments can name it.
Instances For
Programming collision bound.
The TV-distance between running oa under pure caching and under a policy-programming
oracle is bounded by any upper bound B on the bad-event probability of
withProgramming policy (provided B < ∞).
This is the user-facing wrapper around
tvDist_simulateQ_withCaching_withProgramming_le_probEvent_bad: the heavy lifting (the
identical-until-bad bridge between withCaching and withProgramming) is the headline
theorem of this file; here we just expose it under the canonical "collision" name and combine
it with a user-supplied bad-event bound hBad.
The canonical qP * qH * β Fiat-Shamir slack is recovered by instantiating
B := (qP : ℝ≥0∞) * qH * β (see programming_collision_bound_qP_qH_β) and discharging hBad
via a union bound over the at most qP programmed points (each contributing at most qH * β
by per-step unpredictability of the queried inputs). For Schnorr with spec.Domain = M × Commit,
β = 1/|G|, qP = qS, and effective qH = qS + qH, this matches collisionSlack qS qH G.
The per-point union bound itself depends on the structure of oa's queries (specifically, an
unpredictability hypothesis on each query's input distribution); it is discharged in the
caller's setting. See Examples/CommitmentScheme/ and CryptoFoundations/FiatShamir/Sigma/
for FS-flavored applications.
Convenience repackaging of programming_collision_bound: when the user has a bad-event
bound of the canonical qP * qH * β shape, we get the canonical FS slack as the TV-distance
bound. The caller need only discharge hBad (typically by a union bound over at most qP
programmed points, each hit with probability ≤ qH * β).
Heterogeneous inner monad: ProbComp-valued random-oracle bridge #
The bridges above fix the inner monad of the wrapped oracle to OracleComp spec (the same
spec as the simulated computation). The lazy random oracle OracleSpec.randomOracle is instead
uniformSampleImpl.withCaching, whose base implementation uniformSampleImpl lives in
ProbComp = OracleComp unifSpec — a different spec from the surface program. The bridge below
re-establishes the identical-until-bad TV-distance bound when the base implementation so is
valued in OracleComp spec' for an arbitrary uniform spec' (taking spec' = unifSpec recovers
the random-oracle case). It is driven by the heterogeneous engine
tvDist_simulateQ_run_le_probEvent_output_bad and the heterogeneous projection
withCachingTrackingPolicy_run'_eq'.
These lemmas are the random-oracle-state-threading component of the GPV hash-and-sign EUF-CMA
reduction (VCVio/CryptoFoundations/GPVHashAndSign.lean): they let one replace the unprogrammed
lazy random oracle by a programmed one up to the salt/programming bad event.
Joint (state-included) identical-until-bad TV-distance bound between withProgramming policy
and its tracking partner withCachingTrackingPolicy policy, with the base implementation valued
in OracleComp spec'. The conclusion keeps the final (cache, bad) state, so a state-dependent
continuation (e.g. GPV verify reading the run's cache) can be appended on both sides.
Heterogeneous identical-until-bad bridge (output marginal).
The TV-distance between the output marginal of so.withCaching and the output marginal of
so.withProgramming policy is bounded by the probability that the bad flag of
withProgramming policy fires during the run, for any base implementation so valued in
OracleComp spec' with spec' uniform.
This is the spec'-generalization of
tvDist_simulateQ_withCaching_withProgramming_le_probEvent_bad; specializing so to
uniformSampleImpl (so spec' = unifSpec) gives the lazy-random-oracle bridge
tvDist_simulateQ_randomOracle_withProgramming_le_probEvent_bad.
Lazy random-oracle state-threading bridge #
The specialization of the heterogeneous bridge to the lazy random oracle
OracleSpec.randomOracle = uniformSampleImpl.withCaching. This is the reusable state-threading
infrastructure consumed by the GPV hash-and-sign EUF-CMA reduction: it replaces the unprogrammed
lazy random oracle by a policy-programmed one, up to the programming bad event.
Random-oracle state-threading bridge.
For a lazy random oracle over a spec with sampleable ranges, the TV-distance between the output
marginal of the unprogrammed run (simulateQ spec.randomOracle oa, started from cache) and the
programmed run (simulateQ (uniformSampleImpl.withProgramming policy) oa, started from
(cache, false)) is bounded by the probability that the programming bad flag fires.
This instantiates tvDist_simulateQ_withCaching_withProgramming_le_probEvent_bad' at
so := uniformSampleImpl (so the inner monad is ProbComp = OracleComp unifSpec), using
OracleSpec.randomOracle = uniformSampleImpl.withCaching definitionally.