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 * β).