ROM Unpredictability and Collision Win Bounds #
Fresh query uniformity, cache preimage bounds, and the collision-based win probability theorem.
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).