Exact output memory of complete native Chan–He node construction

Main definitions

• NodePacking.paddingMemory, roundMemory, memory: exact instruction-level write specs.
• NodePacking.node: the existing mathematical node for the three supplied enumerations.

References

These memory composition proofs are original.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.paddingMemory (L : Layout) (mem : ℕ → ℕ) : ℕ → ℕ

Every output cell is initialized, even when the three input arrays are empty.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.roundMemory (L : Layout) (values : Fin 3 → ℕ → ℤ) (j : Fin 3) (mem : ℕ → ℕ) : ℕ → ℕ

Exact complete count/place call for the selected supplied input array.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.memory (L : Layout) (values : Fin 3 → ℕ → ℤ) (mem : ℕ → ℕ) : ℕ → ℕ

Exact memory after padding and all three complete native calls.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.node (L : Layout) (values : Fin 3 → ℕ → ℤ) : ThreeSum.ChanHe.Node

The existing mathematical Chan–He node, with no alternative 3SUM semantics.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.padding_values (L : Layout) : 120 * L.U + 80 = WordRAM.Signed.encode (10 * ↑L.gap) ∧ 16 * L.U + 10 = WordRAM.Signed.encode (ThreeSum.ChanHe.pad L.U + ↑L.gap) ∧ 40 * L.U + 26 = WordRAM.Signed.encode (ThreeSum.ChanHe.pad L.U + 3 * ↑L.gap) ∧ 44 * L.U + 30 = WordRAM.Signed.encode (-ThreeSum.ChanHe.pad L.U + 4 * ↑L.gap)

The native unsigned pattern encodes exactly the signed padding and tags of oneArray.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.paddingMemory_read (L : Layout) (mem : ℕ → ℕ) {u : ℕ} (hu : u < 4 * L.N) : paddingMemory L mem (L.packed + u) = Padding.pattern (120 * L.U + 80) (16 * L.U + 10) (40 * L.U + 26) (44 * L.U + 30) u

Reading initialized packed memory at any fitting index.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.roundMemory_before (L : Layout) (values : Fin 3 → ℕ → ℤ) (j : Fin 3) (mem : ℕ → ℕ) (hM : 0 < L.M) (hN : 2 * L.M ≤ L.N) {a : ℕ} (ha : a < L.descriptor j) : roundMemory L values j mem a = mem a

Later rounds preserve every earlier count/capacity block.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.roundMemory_other (L : Layout) (values : Fin 3 → ℕ → ℤ) (j : Fin 3) (mem : ℕ → ℕ) {u : ℕ} (hu : u < 4 * L.N) (hc : u % 4 ≠ ↑j + 1) : roundMemory L values j mem (L.packed + u) = mem (L.packed + u)

Every complete call preserves every other packed column, including column zero.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.roundMemory_arrXY (L : Layout) (values : Fin 3 → ℕ → ℤ) (j : Fin 3) (mem : ℕ → ℕ) (hj : j ≠ 2) (hM : 0 < L.M) (hinj : Set.InjOn (values j) ↑(Finset.range (L.n j))) {i : ℕ} (hi : i < L.N) (hpad : mem (L.packed + 4 * i + (↑j + 1)) = WordRAM.Signed.encode (ThreeSum.ChanHe.pad L.U + ↑(L.tag j))) : roundMemory L values j mem (L.packed + 4 * i + (↑j + 1)) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrXY (Finset.image (values j) (Finset.range (L.n j))) L.M L.U i + ↑(L.tag j))

The first two complete rounds produce the existing mathematical light array.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.roundMemory_arrZ (L : Layout) (values : Fin 3 → ℕ → ℤ) (mem : ℕ → ℕ) (hM : 0 < L.M) (hinj : Set.InjOn (values 2) ↑(Finset.range (L.n 2))) {i : ℕ} (hi : i < L.N) (hpad : mem (L.packed + 4 * i + 3) = WordRAM.Signed.encode (-ThreeSum.ChanHe.pad L.U + 4 * ↑L.gap)) : roundMemory L values 2 mem (L.packed + 4 * i + 3) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrZ (Finset.image (values 2) (Finset.range (L.n 2))) L.M L.U i + 4 * ↑L.gap)

The third complete round produces the existing duplicated, negated mathematical array.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.memory_cells (L : Layout) (values : Fin 3 → ℕ → ℤ) (mem : ℕ → ℕ) (hM : 0 < L.M) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (L.n j))) {i : ℕ} (hi : i < L.N) : memory L values mem (L.packed + 4 * i) = WordRAM.Signed.encode (10 * ↑L.gap) ∧ memory L values mem (L.packed + 4 * i + 1) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrXY (node L values).S₁ L.M L.U i + ↑L.gap) ∧ memory L values mem (L.packed + 4 * i + 2) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrXY (node L values).S₂ L.M L.U i + 3 * ↑L.gap) ∧ memory L values mem (L.packed + 4 * i + 3) = WordRAM.Signed.encode (ThreeSum.ChanHe.arrZ (node L values).S₃ L.M L.U i + 4 * ↑L.gap)

All four packed columns have exactly the existing node's required values.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.memory_oneArray (L : Layout) (values : Fin 3 → ℕ → ℤ) (mem : ℕ → ℕ) (hM : 0 < L.M) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (L.n j))) {u : ℕ} (hu : u < 4 * L.N) : memory L values mem (L.packed + u) = WordRAM.Signed.encode ((node L values).oneArray L.U u)

Every one of the 4N native output cells equals the existing mathematical Node.oneArray. This includes column-zero sentinels, empty and heavy buckets, and the entire padded tail.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.memory_heavy (L : Layout) (values : Fin 3 → ℕ → ℤ) (mem : ℕ → ℕ) (hM : 0 < L.M) (hN : 2 * L.M ≤ L.N) (j : Fin 3) : memory L values mem (L.descriptor j) = (Place.heavyList (values j) (L.n j) L.M (L.n j)).length ∧ ∀ (k : ℕ) (hk : k < (Place.heavyList (values j) (L.n j) L.M (L.n j)).length), memory L values mem (L.heavy j + k) = WordRAM.Signed.encode (Place.heavyList (values j) (L.n j) L.M (L.n j))[k]

Every count cell and every used heavy cell survives subsequent rounds.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.roundMemory_outside (L : Layout) (values : Fin 3 → ℕ → ℤ) (j : Fin 3) (mem : ℕ → ℕ) (hM : 0 < L.M) (hN : 2 * L.M ≤ L.N) {a : ℕ} (ha : a < L.base ∨ L.endpoint ≤ a) : roundMemory L values j mem a = mem a

Each complete round preserves all memory outside the concrete allocation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.memory_outside (L : Layout) (values : Fin 3 → ℕ → ℤ) (mem : ℕ → ℕ) (hM : 0 < L.M) (hN : 2 * L.M ≤ L.N) {a : ℕ} (ha : a < L.base ∨ L.endpoint ≤ a) : memory L values mem a = mem a

Inputs, caller memory before the allocation, and memory beyond its endpoint are preserved.