A complete native counting and placement call

This routine actually computes the residues and histogram before extracting a heavy array and placing the corresponding packed column. The histogram is not a premise of the execution contract. It also writes the compact output count to its caller-supplied descriptor cell.

Main definitions

• CountPlace.program: modulus encoding, complete CountCall.program 2, runtime argument delivery, complete Place.program, and the count store.

References

This native composition is original and reuses the existing Chan–He mathematical definitions.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.len : Fin 64

Input length (the selected third argument of the existing counting call).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.src : Fin 64

Signed input base.

@[reducible, inline]

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

Unsigned residue workspace base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.hist : Fin 64

Histogram workspace base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.heavy : Fin 64

Compact heavy output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.packed : Fin 64

Packed node array base.

@[reducible, inline]

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

Positive modulus, decoded unsigned.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.tag : Fin 64

Encoded positive tag.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.column : Fin 64

Packed column.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.distance : Fin 64

Distance between the two stores.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.negative : Fin 64

Zero for X/Y, one for Z.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.descriptor : Fin 64

Cell in which the exact heavy count is stored.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.registers (i : Fin 32) : Fin 64

Fixed embedding of the placement workspace below all caller parameters.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.psrc : Fin 64

Input array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.pkeys : Fin 64

Unsigned residue array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.plen : Fin 64

Input length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.phist : Fin 64

Histogram base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.pheavy : Fin 64

Compact heavy output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.ppacked : Fin 64

Packed node output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.pmodulus : Fin 64

Positive modulus, decoded unsigned.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.ptag : Fin 64

Twice the positive tag added to a light integer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.pcolumn : Fin 64

Column in a four-cell group.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.pdistance : Fin 64

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

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.pnegative : Fin 64

Zero for X/Y, one for Z.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.pcount : Fin 64

Number of heavy integers already written.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.prepare : WordRAM.Code WordRAM.Basis.standard 64

All eleven runtime argument copies are real instructions.

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

Complete fixed native routine: no host histogram, heavy filter or output constructor.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.preserves (i : Fin 64) (hi : 32 ≤ ↑i) (hm : i ≠ CountCall.modulus) (hc : i ≠ CountCall.result 2) : WordRAM.Code.Preserves i program

Only the counting/placement workspace, the encoded modulus, and the discarded collision counter can change. All caller registers at least 46 are included in this frame.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.budget (x : WordRAM.Data 64) (M N U t : ℕ) : ℕ

Polynomial envelope for addresses, counters, encoded magnitudes and every scan intermediate.

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

Exact memory, including actual residue/histogram construction and the descriptor write.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.CountPlace.exec {w M N U t : ℕ} (x : WordRAM.Data 64) (values : ℕ → ℤ) (neg : Bool) (hM : 0 < M) (hmod : GenericRAM.Signed.Fits w ↑M) (hmreg : x.regs modulus = M) (hN : 2 * M ≤ N) (ht : U ≤ t) (htag : x.regs tag = 2 * t) (hneg : x.regs negative = if neg = true then 1 else 0) (hc : x.regs column < 4) (hd : x.regs distance ≤ 4 * M) (hbdd : ∀ i < x.regs len, (values i).natAbs ≤ U) (hsigned : ∀ i < x.regs len, GenericRAM.Signed.Fits w (values i)) (hfit : WordRAM.Fits (w + 2) (budget x M N U t)) (hsh : x.regs src + x.regs len ≤ x.regs heavy) (hhp : x.regs heavy + x.regs len ≤ x.regs packed) (hpk : x.regs packed + 4 * N ≤ x.regs scratch) (hkh : x.regs scratch + x.regs len ≤ x.regs hist) (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 64), WordRAM.ExecWithin (w + 2) program x y (66 * x.regs len + 5 * M + 45) ∧ y.mem = memory x.mem values (x.regs len) M (x.regs heavy) (x.regs packed) (x.regs column) (x.regs distance) t (x.regs scratch) (x.regs hist) (x.regs descriptor) neg ∧ ∀ (i : Fin 64), 32 ≤ ↑i → i ≠ CountCall.modulus → i ≠ CountCall.result 2 → y.regs i = x.regs i

Complete native count/extract/place execution, charging modulus encoding, all subroutine argument/result copies and the final count write. The caller supplies actual signed input words; no histogram or light/heavy-output contract is assumed.