Charged calls to Chan–He collision counting

The prime searches keep their parameters outside the counting workspace. Each of the three set arrays has a fixed pair of base/length registers and its own result register. This module charges argument setup and result delivery as well as the complete native counting routine.

Main definitions

• CountCall.program: a counting call on one of the three input arrays.

Main results

• CountCall.exec: exact collision count, memory frame and preserved caller registers.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.registers (i : Fin 28) : Fin 64

Counting workspace in a larger, fixed register file.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.length (j : Fin 3) : Fin 64

Length register for the selected set.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.source (j : Fin 3) : Fin 64

Base register for the selected set.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.scratch : Fin 64

Residue scratch base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.histogram : Fin 64

Histogram base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.modulus : Fin 64

Encoded positive modulus.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.result (j : Fin 3) : Fin 64

Collision-count output register for the selected set.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.countSource : Fin 64

Counting input base register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.countScratch : Fin 64

Counting scratch base register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.countLength : Fin 64

Counting input length register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.countModulus : Fin 64

Counting encoded-modulus register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.countHistogram : Fin 64

Counting histogram base register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.countTotal : Fin 64

Counting result register.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.prepare (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 64

Five runtime register copies deliver the counting arguments.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountCall.program (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 64

A complete native count call, including argument and result copies.

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

A native count call costs 34n+5M+24, including five argument copies and one result copy. The mathematical input is an injective array enumeration, as required by the existing set-based Chan–He collision count. All registers outside the workspace, except its chosen result, survive.