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.

theorem OracleComp.probEvent_log_entry_eq_le {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] [spec.IsUniformSpec] {α : Type} (oa : OracleComp spec α) (k : ℕ) (entry : (t : spec.Domain) × spec.Range t) : (probEvent (simulateQ OracleSpec.loggingOracle oa).run fun (z : α × spec.QueryLog) => z.2[k]? = some entry) ≤ (↑(Fintype.card (spec.Range entry.fst)))⁻¹

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.

theorem OracleComp.probEvent_log_output_heq_le {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] [spec.IsUniformSpec] {α : Type} [Inhabited ι] (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) (oa : OracleComp spec α) (k : ℕ) (entry : (t : spec.Domain) × spec.Range t) : (probEvent (simulateQ OracleSpec.loggingOracle oa).run fun (z : α × spec.QueryLog) => z.2[k]? = some entry) ≤ (↑(Fintype.card (spec.Range default)))⁻¹

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.

theorem OracleComp.probEvent_log_output_match_le {ι : Type} {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} [Inhabited ι] (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) (oa : OracleComp spec α) (k : ℕ) (t₀ : spec.Domain) (u₀ : spec.Range t₀) : (probEvent (simulateQ OracleSpec.loggingOracle oa).run fun (z : α × spec.QueryLog) => ∃ (s : spec.Domain) (v : spec.Range s), z.2[k]? = some ⟨s, v⟩ ∧ u₀ ≍ v) ≤ (↑(Fintype.card (spec.Range default)))⁻¹

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|.

theorem OracleComp.probEvent_pair_collision_le {ι : Type} {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} [Inhabited ι] (oa : OracleComp spec α) (n : ℕ) (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) (i j : Fin n) (hij : i ≠ j) : (probEvent (simulateQ OracleSpec.loggingOracle oa).run fun (z : α × spec.QueryLog) => List.length z.2 > ↑i ∧ List.length z.2 > ↑j ∧ (z.2[i]?.bind fun (ei : (t : spec.Domain) × spec.Range t) => Option.map (fun (ej : (t : spec.Domain) × spec.Range t) => ei.fst ≠ ej.fst ∧ ei.snd ≍ ej.snd) z.2[j]?) = do let a ← some true pure (a = true)) ≤ (↑(Fintype.card (spec.Range default)))⁻¹

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. The hrange hypothesis ensures |Range default| is minimal across all oracle indices, so the bound holds uniformly with |C| = |Range default|.

Union Bound Birthday (Textbook Steps 4-5)

Collision = ∃ pair with collision. Union bound over C(n,2) pairs gives n²/(2|C|).

theorem OracleComp.probEvent_logCollision_le_birthday_total_tight {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] [spec.IsUniformSpec] {α : Type} [Inhabited ι] (oa : OracleComp spec α) (n : ℕ) (hbound : oa.IsTotalQueryBound n) (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) : (probEvent (simulateQ OracleSpec.loggingOracle oa).run fun (z : α × spec.QueryLog) => LogHasCollision z.2) ≤ ↑(n.choose 2) / ↑(Fintype.card (spec.Range default))

Tight birthday bound for loggingOracle (total query bound): The probability of a collision in the query log is ≤ C(n,2)/|C|, where C(n,2) is the exact number of unordered pairs of query positions.

theorem OracleComp.probEvent_logCollision_le_birthday_total {ι : Type} {spec : OracleSpec ι} [spec.DecidableEq] [spec.IsUniformSpec] {α : Type} [Inhabited ι] (oa : OracleComp spec α) (n : ℕ) (hbound : oa.IsTotalQueryBound n) (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) : (probEvent (simulateQ OracleSpec.loggingOracle oa).run fun (z : α × spec.QueryLog) => LogHasCollision z.2) ≤ ↑n ^ 2 / (2 * ↑(Fintype.card (spec.Range default)))

Birthday bound for loggingOracle (total query bound): The probability of a collision in the query log is ≤ n²/(2|C|).

A loose corollary of probEvent_logCollision_le_birthday_total_tight.

theorem OracleComp.probEvent_cacheCollision_le_birthday_total_tight {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} [Inhabited ι] (oa : OracleComp spec α) (n : ℕ) (hbound : oa.IsTotalQueryBound n) (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) : (probEvent ((simulateQ OracleSpec.cachingOracle oa).run ∅) fun (z : α × spec.QueryCache) => CacheHasCollision z.2) ≤ ↑(n * (n - 1)) / (2 * ↑(Fintype.card (spec.Range default)))

Tight birthday bound for cachingOracle (total query bound): The probability of a collision in the cache is ≤ n*(n-1)/(2|C|).

theorem OracleComp.probEvent_cacheCollision_le_birthday_total {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} [Inhabited ι] (oa : OracleComp spec α) (n : ℕ) (hbound : oa.IsTotalQueryBound n) (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) : (probEvent ((simulateQ OracleSpec.cachingOracle oa).run ∅) fun (z : α × spec.QueryCache) => CacheHasCollision z.2) ≤ ↑n ^ 2 / (2 * ↑(Fintype.card (spec.Range default)))

Loose birthday bound for cachingOracle (total query bound): The probability of a collision in the cache is ≤ n²/(2|C|).

A loose corollary of probEvent_cacheCollision_le_birthday_total_tight.

Per-Index Bound Versions

theorem OracleComp.probEvent_cacheCollision_le_birthday {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} {t : ℕ} [Inhabited ι] [Fintype ι] (oa : OracleComp spec α) (hbound : oa.IsPerIndexQueryBound fun (x : ι) => t) (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) : (probEvent ((simulateQ OracleSpec.cachingOracle oa).run ∅) fun (z : α × spec.QueryCache) => CacheHasCollision z.2) ≤ (↑(Fintype.card ι) * ↑t) ^ 2 / (2 * ↑(Fintype.card (spec.Range default)))

Birthday bound for cachingOracle with per-index query bound.

theorem OracleComp.probEvent_cacheCollision_le_birthday' {ι : Type} [DecidableEq ι] {spec : OracleSpec ι} [spec.IsUniformSpec] {α : Type} {t : ℕ} [Inhabited ι] [Unique ι] (oa : OracleComp spec α) (hbound : oa.IsPerIndexQueryBound fun (x : ι) => t) (hrange : ∀ (t : ι), Fintype.card (spec.Range default) ≤ Fintype.card (spec.Range t)) : (probEvent ((simulateQ OracleSpec.cachingOracle oa).run ∅) fun (z : α × spec.QueryCache) => CacheHasCollision z.2) ≤ ↑t ^ 2 / (2 * ↑(Fintype.card (spec.Range default)))

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.