ROM Unpredictability and Collision Win Bounds #
Fresh query uniformity, cache preimage bounds, and the collision-based win probability theorem.
Unpredictability #
HasUnpredictableSample samples β packages "the probability of any specific outcome of
samples : ProbComp α is at most β". It is the abstract handle through which downstream
collision bounds ingest min-entropy of a sample distribution without re-deriving uniform-sample
arithmetic at each call site.
Instances:
HasUnpredictableSample.uniformSample:$ᵗ αis1/|α|-unpredictable.HasUnpredictableSample.mono:β-unpredictability transports up to anyβ' ≥ β.
The TV-distance "programming collision" bound that consumes this typeclass lives downstream in
VCVio/ProgramLogic/Relational/ProgrammingOracle.lean (see programming_collision_bound and
its qP * qH * β repackaging), keeping the relational theorem in the ProgramLogic layer
while the unpredictability primitive stays here in QueryTracking.
Unpredictability #
Fresh query uniformity: querying cachingOracle at an uncached point
yields each value with probability 1/|C|.
WARNING: trivially true. The proof uses only probEvent_le_one; the query bound
hbound and target are completely unused. The conclusion Pr[...] * |C|⁻¹ ≤ |C|⁻¹
holds for any computation regardless of how many queries it makes.
A meaningful unpredictability bound should use hbound to establish that the queried point
is fresh, giving a tight 1/|C| bound on the probability of guessing the ROM output.
Cache preimage bound: if the initial cache contains at most one preimage
of a target value v₀, then the probability that simulateQ cachingOracle oa
creates a fresh cache entry equal to v₀ is at most n / |C|, where n is the
total query bound. Each cache miss is a fresh uniform draw, so a union bound
over the at most n misses gives the result.
This is the reusable ROM lemma for the extractability "fresh target hit" case.
Special case of
probEvent_cache_has_value_le_of_unique_preimage when the initial cache
contains at most one preimage of v₀ because the cache is collision-free.
Special case of
probEvent_cache_has_value_le_of_unique_preimage when the initial cache
contains no preimage of v₀.
Collision-Based Win Bound #
WARNING: vacuously true. The [Unique ι] hypothesis means ι has exactly one element,
but CacheHasCollision (used via probEvent_cacheCollision_le_birthday') requires two distinct
oracle indices t₁ ≠ t₂ : ι, which is impossible when ι is unique. The event
CacheHasCollision z.2 is therefore always false, making the bound trivially 0 ≤ ....
For a useful single-oracle collision bound, state it over LogHasCollision (which checks for
equal outputs on distinct inputs within the same oracle index) rather than CacheHasCollision
(which requires distinct indices).
A probabilistic computation samples : ProbComp α is β-unpredictable if every specific
outcome occurs with probability at most β. This is the standard "min-entropy at level
log₂(1/β)" notion, packaged as a structured proposition so that downstream collision bounds
can ingest it generically.
Equivalent to ∀ x, Pr[= x | samples] ≤ β; the structure shape lets it serve as the canonical
abstract hypothesis for "values drawn from samples are hard to guess".
Instances For
Monotonicity in the bound: a β-unpredictable sample is also β'-unpredictable for any
β' ≥ β.
$ᵗ α is (|α|)⁻¹-unpredictable for any nonempty Fintype.
Sanity check: uniform sampling reproduces the canonical 1/|α| shape #
For a β-unpredictable sampling distribution from a fintype, the per-sample bound
matches (Fintype.card α)⁻¹ exactly when samples = $ᵗ α. This pins the textbook
"uniform draw from α has min-entropy log₂|α|" arithmetic so downstream collision bounds
can substitute β = 1/|α| algebraically.