The birthday accumulation bound (generic)

A reusable "balls into bins" accumulation lemma for the bounded loop combinator loop_n, independent of any random-oracle structure. Given a loop body that

• bumps a collision potential coll : s → ENNReal by at most size σ / N per iteration, and
• bumps a size potential size : s → ℕ by at most 1 per iteration,

the n-fold loop bumps coll by at most the triangular sum n (2·size + n − 1) / 2N — and starting from size = 0 this is the birthday bound n(n−1)/2N.

This is the abstract core shared by collision-resistance and the PRP/PRF switching lemma; each supplies the two per-step facts (e.g. "a lazy query collides with probability ≤ RO_size/N" and "the cache grows by ≤ 1") and instantiates loop_n_birthday_bound.

theorem loop_n_birthday_bound {s : Type} (body : GaudisCrypt.ProgramDenotation s Unit) (coll : s → ENNReal) (size : s → ℕ) (N : ENNReal) (hN_pos : N ≠ 0) (hN_top : N ≠ ⊤) (h_coll : ∀ (σ : s), body.wp (fun (yσ : Unit × s) => coll yσ.2) σ ≤ coll σ + ↑(size σ) / N) (h_size : ∀ (σ : s), body.wp (fun (yσ : Unit × s) => ↑(size yσ.2)) σ ≤ ↑(size σ) + 1) (k : ℕ) (σ : s) : (GaudisCrypt.loop_n k body).wp (fun (yσ : Unit × s) => coll yσ.2) σ ≤ coll σ + ↑k * (2 * ↑(size σ) + ↑k - 1) / (2 * N)

The birthday accumulation bound. If body bumps coll by at most size/N and size by at most 1 per iteration, then loop_n k body bumps coll by at most k(2·size + k − 1)/2N.