Native heavy extraction and light placement

The input, unsigned residue array and histogram are supplied by the actual Count.program. One scan copies heavy integers, in input order, to a compact output. Each light integer is tagged and placed directly in the packed node array. The third pass negates its integer and its residue, and writes both copies required by arrZ.

The mathematical comparator is Anthropic's Buckets.lean and NodeArray.lean at formal-math@16a5ce41304fcdaea4e0be7c132e1c361dc26da5. The native code, encoding arithmetic and execution proofs here are original. No Light execution theorem or source-machine simulation is assumed.

Main definitions

• Place.program: a fixed scan with runtime bases, length, modulus, tag and column.
• Place.heavyList: compact heavy elements in input order.
• Place.memory: exact writes of a prefix of the scan, including both third-column copies.

References

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.src : Fin 32

Input array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.keys : Fin 32

Unsigned residue array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.len : Fin 32

Input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.hist : Fin 32

Histogram base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.heavy : Fin 32

Compact heavy output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.packed : Fin 32

Packed node output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.modulus : Fin 32

Positive modulus, decoded unsigned.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.tag : Fin 32

Twice the positive tag added to a light integer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.column : Fin 32

Column in a four-cell group.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.distance : Fin 32

Distance to the second write: zero for X/Y, 4M for Z.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.negative : Fin 32

Zero for X/Y, one for Z.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.idx : Fin 32

Input cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.count : Fin 32

Number of heavy integers already written.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.addr : Fin 32

Temporary address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.key : Fin 32

Current remainder.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.value : Fin 32

Current value and its tagged encoding.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.magnitude : Fin 32

Twice the current magnitude.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.sign : Fin 32

Current input sign.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.one : Fin 32

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.two : Fin 32

Constant two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.four : Fin 32

Constant four.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.zero : Fin 32

Constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.bucketSize : Fin 32

Current histogram count.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.targetKey (M : ℕ) (neg : Bool) (z : ℤ) : ℕ

Negating a Euclidean residue needs only a subtraction and a remainder.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.signedValue (neg : Bool) (z : ℤ) : ℤ

Integer contribution before the positive tag.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.targetKey_eq {M : ℕ} (hM : 0 < M) (neg : Bool) (z : ℤ) : targetKey M neg z = residueKey M (signedValue neg z)

The target index is exactly the residue of the signed contribution.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.heavyList (values : ℕ → ℤ) (n M : ℕ) : ℕ → List ℤ

A prefix of the compact output; membership is tested against the full histogram.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.length_heavyList_le (values : ℕ → ℤ) (n M k : ℕ) : (heavyList values n M k).length ≤ k

A compact prefix has at most as many cells as the corresponding input prefix.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.heavyList_eq_filter (values : ℕ → ℤ) (n M k : ℕ) : heavyList values n M k = List.map values (List.filter (fun (i : ℕ) => decide (1 < Histogram.count (fun (j : ℕ) => residueKey M (values j)) n (residueKey M (values i)))) (List.range k))

The compact array is the input subsequence selected by the histogram test.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.heavyList_toFinset (values : ℕ → ℤ) (n : ℕ) {M : ℕ} (hM : 0 < M) (hinj : Set.InjOn values ↑(Finset.range n)) : (heavyList values n M n).toFinset = ThreeSum.ChanHe.heavy (Finset.image values (Finset.range n)) M

The native compact output has exactly the existing heavy subset as its underlying set.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.write (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t : ℕ) (neg : Bool) (k : ℕ) : ℕ → ℕ

The exact per-input write, either to the next compact heavy cell or to packed light cells.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t : ℕ) (neg : Bool) : ℕ → ℕ → ℕ

All writes of the first k iterations, framed by arbitrary initial memory.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.heavyCode : WordRAM.Code WordRAM.Basis.standard 32

Copy a heavy integer without changing its signed encoding.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.lightCode : WordRAM.Code WordRAM.Basis.standard 32

Tag a light integer using its magnitude and sign, then write its required cells.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.body : WordRAM.Code WordRAM.Basis.standard 32

Every iteration reads the original integer, its unsigned key and its exact bucket size.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.program : WordRAM.Code WordRAM.Basis.standard 32

The same finite code handles every input length, width, modulus and output length.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.preserves_parameters (i : Fin 32) (hi : 9 ≤ ↑i ∧ ↑i ≤ 19) : WordRAM.Code.Preserves i program

All runtime parameters survive the scan.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Place.memory_outside (mem : ℕ → ℕ) (values : ℕ → ℤ) (n M out dst col dist t N : ℕ) (neg : Bool) (hM : 0 < M) (hN : 2 * M ≤ N) (hc : col < 4) (hd : dist ≤ 4 * M) {k : ℕ} (hk : k ≤ n) {a : ℕ} (ha : ¬(out ≤ a ∧ a < out + n)) (hb : ¬(dst ≤ a ∧ a < dst + 4 * N)) : memory mem values n M out dst col dist t neg k a = mem a

A scan can only change its heavy capacity block and its packed output block.