Native collision counts for the three Chan–He sets

All three calls are actual native counting programs, with charged argument and result copies. The prime-search control registers and every input cell below the workspace are preserved.

Main definitions

• CountTriple.program: three complete native collision-count calls.

Main results

• CountTriple.exec: exact counts for all three sets and charged total time.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountTriple.program : WordRAM.Code WordRAM.Basis.standard 64

Run one full count call on each of the three arrays.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountTriple.exec {w M : ℕ} (x : WordRAM.Data 64) (values : Fin 3 → ℕ → ℤ) (hM : 0 < M) (hmod : GenericRAM.Signed.Fits w ↑M) (hmodreg : x.regs CountCall.modulus = WordRAM.Signed.encode ↑M) (hfit : ∀ (j : Fin 3), ∀ i < x.regs (CountCall.length j), GenericRAM.Signed.Fits w (values j i)) (hs : ∀ (j : Fin 3), WordRAM.Fits (w + 2) (x.regs (CountCall.source j) + x.regs (CountCall.length j))) (hk : ∀ (j : Fin 3), WordRAM.Fits (w + 2) (x.regs CountCall.scratch + x.regs (CountCall.length j))) (hd : WordRAM.Fits (w + 2) (x.regs CountCall.histogram + M)) (ht : ∀ (j : Fin 3), WordRAM.Fits (w + 2) (x.regs (CountCall.length j) * x.regs (CountCall.length j) + x.regs (CountCall.length j) + 1)) (hsk : ∀ (j : Fin 3), x.regs (CountCall.source j) + x.regs (CountCall.length j) ≤ x.regs CountCall.scratch) (hkd : ∀ (j : Fin 3), x.regs CountCall.scratch + x.regs (CountCall.length j) ≤ x.regs CountCall.histogram) (hinput : ∀ (j : Fin 3), ∀ i < x.regs (CountCall.length j), x.mem (x.regs (CountCall.source j) + i) = WordRAM.Signed.encode (values j i)) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (x.regs (CountCall.length j)))) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin (w + 2) program x y (34 * (x.regs (CountCall.length 0) + x.regs (CountCall.length 1) + x.regs (CountCall.length 2)) + 15 * M + 72) ∧ (∀ (j : Fin 3), y.regs (CountCall.result j) = ThreeSum.ChanHe.coll (Finset.image (values j) (Finset.range (x.regs (CountCall.length j)))) M) ∧ (∀ (i : Fin 64), 28 ≤ ↑i ∧ ↑i < 37 ∨ 40 ≤ ↑i → y.regs i = x.regs i) ∧ ∀ a < x.regs CountCall.scratch, y.mem a = x.mem a

Count collisions in all three injectively enumerated sets in at most 34(n₀+n₁+n₂)+15M+72 instructions, excluding halt. All caller registers except the three results are preserved, as is all memory before the counting workspace.