ROM Birthday Bound #
Per-pair collision bounds and union bound birthday argument for random oracle collision probability. Covers both log-based and cache-based collision bounds, with per-index corollaries.
Per-Pair Collision Bound (Textbook Step 3) #
For each pair (i,j) of positions in the log with distinct inputs, Pr[outputs equal] ≤ 1/|C|. This is because in the evalDist model, each query returns an independent uniform sample.
ROM uniformity at a log position: For any loggingOracle trace, the
probability that the k-th log entry matches a fixed sigma-typed value ⟨t, v⟩
is at most 1/|Range t|. Each query response is an independent uniform draw.
Proof by structural induction on the computation. For query t >>= mx:
- The log is
[⟨t, u⟩] ++ sub_logwhereuis uniform fromRange t. - For k = 0: the event is
⟨t, u⟩ = entry, bounded byPr[= v | query t] = 1/|Range t|. - For k > 0: the event is
sub_log[k-1]? = entry, bounded by the inductive hypothesis.
Uniformized log entry bound: the probability that position k of a loggingOracle
trace equals a fixed sigma-typed entry is at most 1/|Range default|, assuming |Range default|
is minimal across all oracle indices.
This is a corollary of probEvent_log_entry_eq_le (which gives 1/|Range entry.1|) combined
with the hrange monotonicity hypothesis.
Probability that the k-th log entry's output is HEq to a fixed value u₀ : spec.Range t₀.
Unlike probEvent_log_entry_eq_le which matches the full sigma entry, this only constrains
the output component. The bound uses hrange to get 1/|Range default|.
Proof by structural induction on the computation, same shape as probEvent_log_entry_eq_le.
Per-pair collision bound: For any two positions in a loggingOracle trace
with distinct inputs, the probability that their outputs are HEq-equal is ≤ 1/|C|.
This is the core ROM property: distinct oracle inputs yield independent uniform outputs.
In the evalDist model, each query call returns a fresh uniform sample.
The proof is by structural induction on the computation. For query t >>= mx:
- If both positions ≥ 1: they refer to sub-log positions, and the IH applies directly.
- If one position is 0: the collision involves the fresh response
ufromquery tand a sub-log entry. ByprobEvent_log_output_heq_le, sub-log position k matching any fixed entry has prob ≤ 1/|Range default|.
The hrange hypothesis ensures that |Range default| is minimal across all oracle
indices, so the per-entry bound 1/|Range s| ≤ 1/|Range default| holds uniformly.
Union Bound Birthday (Textbook Steps 4-5) #
Collision = ∃ pair with collision. Union bound over C(n,2) pairs gives n²/(2|C|).
Birthday bound for loggingOracle (total query bound):
The probability of a collision in the query log is ≤ n²/(2|C|).
Proof: express collision as ∃ pair (i,j), then union bound using
probEvent_pair_collision_le for each pair.
Tight birthday bound for cachingOracle (total query bound):
The probability of a collision in the cache is ≤ n*(n-1)/(2|C|).
Loose birthday bound for cachingOracle (total query bound):
The probability of a collision in the cache is ≤ n²/(2|C|).
Derived from the tight bound n*(n-1)/(2|C|) since n*(n-1) ≤ n².
Per-Index Bound Versions #
Birthday bound for cachingOracle with per-index query bound.
WARNING: vacuously true. The [Unique ι] hypothesis means ι has exactly one element,
but CacheHasCollision requires two distinct oracle indices t₁ ≠ t₂ : ι, which is impossible.
The event CacheHasCollision z.2 is therefore always false, making the bound trivially 0 ≤ ....
The non-vacuous birthday bound is probEvent_cacheCollision_le_birthday_total_tight.