Native Chan–He collision counting

This fixed native program first decodes signed Euclidean residue keys, then builds a histogram and counts ordered collisions. Register setup between the two loops is charged. For injective input arrays its counter is exactly the existing Chan–He coll.

Main definitions

• Count.program: the composed native residue/histogram program.
• Count.memory: the complete output memory, including the residue scratch array.

Main results

• Count.exec: execution in at most 34n + 5M + 18 native instructions.
• Count.exec_coll: the counter equals the existing mathematical collision count.
• Count.memory_before: cells below the two workspace blocks retain their contents.

References

• T. M. Chan and Q. He, Reducing 3SUM to Convolution-3SUM

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.residuesRegisters (i : Fin 16) : Fin 28

Residue routine registers occupy the first sixteen registers.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.histogramRegisters (i : Fin 11) : Fin 28

Histogram registers occupy registers sixteen through twenty-six.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.src : Fin 28

Encoded integer input base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.scratch : Fin 28

Residue scratch base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.len : Fin 28

Number of input values.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.modulus : Fin 28

Encoded positive modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.dst : Fin 28

Histogram destination base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.total : Fin 28

Output collision count, an ordinary unsigned word.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.hsrc : Fin 28

Histogram input base register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.hdst : Fin 28

Histogram output base register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.hlen : Fin 28

Histogram length register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.hbins : Fin 28

Histogram modulus register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.hone : Fin 28

Histogram constant register, also used to decode the encoded modulus.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.prepare : WordRAM.Code WordRAM.Basis.standard 28

Set up the histogram parameters, explicitly decoding the positive modulus.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.program : WordRAM.Code WordRAM.Basis.standard 28

A single finite native program, independent of input length, modulus and word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.preserves_parameters (i : Fin 28) (hi : 9 ≤ ↑i ∧ ↑i ≤ 12 ∨ i = dst) : WordRAM.Code.Preserves i program

The complete counting program preserves its input base, scratch base, length, encoded modulus and histogram base registers.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.memory (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M scratch dst : ℕ) : ℕ → ℕ

The residue scratch array and the complete histogram, framed by the original memory.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.memory_before (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M scratch dst a : ℕ) (hs : a < scratch) (hd : a < dst) : memory mem values n M scratch dst a = mem a

Neither the residue array nor the histogram modifies an earlier memory cell.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.exec {w M : ℕ} (x : WordRAM.Data 28) (values : ℕ → ℤ) (hM : 0 < M) (hmod : GenericRAM.Signed.Fits w ↑M) (hmodreg : x.regs modulus = WordRAM.Signed.encode ↑M) (hfit : ∀ i < x.regs len, GenericRAM.Signed.Fits w (values i)) (hs : WordRAM.Fits (w + 2) (x.regs src + x.regs len)) (hk : WordRAM.Fits (w + 2) (x.regs scratch + x.regs len)) (hd : WordRAM.Fits (w + 2) (x.regs dst + M)) (ht : WordRAM.Fits (w + 2) (x.regs len * x.regs len + x.regs len + 1)) (hsk : x.regs src + x.regs len ≤ x.regs scratch) (hkd : x.regs scratch + x.regs len ≤ x.regs dst) (hinput : ∀ i < x.regs len, x.mem (x.regs src + i) = WordRAM.Signed.encode (values i)) : ∃ (y : WordRAM.Data 28), WordRAM.ExecWithin (w + 2) program x y (34 * x.regs len + 5 * M + 18) ∧ y.mem = memory x.mem values (x.regs len) M (x.regs scratch) (x.regs dst) ∧ y.regs total = Histogram.pairs (fun (i : ℕ) => (values i % ↑M).toNat) (x.regs len) ∧ ∀ (i : Fin 28), 9 ≤ ↑i ∧ ↑i ≤ 12 ∨ i = dst → y.regs i = x.regs i

Complete native collision counting, including residue computation, clearing the histogram and register setup. Input, scratch and histogram blocks occur in that order and are disjoint. The final halt is excluded. Fit hypotheses are local; a caller must derive them from its input and width contract.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Count.exec_coll {w M : ℕ} (x : WordRAM.Data 28) (values : ℕ → ℤ) (hM : 0 < M) (hmod : GenericRAM.Signed.Fits w ↑M) (hmodreg : x.regs modulus = WordRAM.Signed.encode ↑M) (hfit : ∀ i < x.regs len, GenericRAM.Signed.Fits w (values i)) (hs : WordRAM.Fits (w + 2) (x.regs src + x.regs len)) (hk : WordRAM.Fits (w + 2) (x.regs scratch + x.regs len)) (hd : WordRAM.Fits (w + 2) (x.regs dst + M)) (ht : WordRAM.Fits (w + 2) (x.regs len * x.regs len + x.regs len + 1)) (hsk : x.regs src + x.regs len ≤ x.regs scratch) (hkd : x.regs scratch + x.regs len ≤ x.regs dst) (hinput : ∀ i < x.regs len, x.mem (x.regs src + i) = WordRAM.Signed.encode (values i)) (hinj : Set.InjOn values ↑(Finset.range (x.regs len))) : ∃ (y : WordRAM.Data 28), WordRAM.ExecWithin (w + 2) program x y (34 * x.regs len + 5 * M + 18) ∧ y.mem = memory x.mem values (x.regs len) M (x.regs scratch) (x.regs dst) ∧ y.regs total = ThreeSum.ChanHe.coll (Finset.image values (Finset.range (x.regs len))) M ∧ ∀ (i : Fin 28), 9 ≤ ↑i ∧ ↑i ≤ 12 ∨ i = dst → y.regs i = x.regs i

For an injective integer array, the composed program returns exactly the collision count used by the existing Chan–He prime searches.