Actual native argument delivery in the Chan–He traversal

The current record and persistent parameters are delivered to the existing complete modulus and node programs in registers 0–63. Every copy and histogram-base addition is a native instruction. The record, controller parameters and native word-stack registers survive setup.

Main definitions

• modulusState, nodeState: exact states after the two native argument blocks.

Main results

• prepareModulus_exec: fourteen charged instructions, including all histogram-base additions.
• prepareNode_exec: ten charged native register copies.
• modulusState_preserves, nodeState_preserves: all registers above the kernel survive.

These calling-convention proofs are original.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.modulusState (x : WordRAM.Data 128) : WordRAM.Data 128

The exact state after the fourteen-instruction modulus argument block.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.nodeState (x : WordRAM.Data 128) : WordRAM.Data 128

The exact state after the ten-instruction node argument block.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.recordLayout (x : WordRAM.Data 128) (M : ℕ) : NodePacking.Layout

The existing node layout instantiated by the traversal record and one computed modulus.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.nodeState_layout (x : WordRAM.Data 128) : NodePacking.layout (WordRAM.Data.comap kernel (nodeState x)) = recordLayout x (x.regs selected)

The delivered node ABI has exactly the current record's layout.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.recordLayout_congr (x y : WordRAM.Data 128) (M : ℕ) (h : ∀ (i : Fin 128), 64 ≤ ↑i → i ≠ selected → y.regs i = x.regs i) : recordLayout y M = recordLayout x M

The layout reads only persistent record/controller fields outside the selected-modulus word.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.recordLayout_endpoint (x : WordRAM.Data 128) (M : ℕ) : (recordLayout x M).endpoint = x.regs heap + 3 + 2 * (x.regs (slot 2) + x.regs (slot 4) + x.regs (slot 6)) + 4 * x.regs groups + M

The final endpoint formula expressed entirely in the persistent traversal ABI.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.modulusState_preserves (x : WordRAM.Data 128) (i : Fin 128) (hi : 64 ≤ ↑i) : (modulusState x).regs i = x.regs i

Modulus argument delivery preserves every traversal and stack register.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.nodeState_preserves (x : WordRAM.Data 128) (i : Fin 128) (hi : 64 ≤ ↑i) : (nodeState x).regs i = x.regs i

Node argument delivery preserves every traversal and stack register.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.prepareModulus_exec {w : ℕ} (x : WordRAM.Data 128) (h : WordRAM.Fits w (x.regs heap + x.regs (slot 2) + x.regs (slot 4) + x.regs (slot 6))) : WordRAM.Exec w prepareModulus x (modulusState x) 14

Native modulus argument delivery charges the three histogram-base additions too. A fit for their largest value derives all intermediate address fits.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.prepareNode_exec {w : ℕ} (x : WordRAM.Data 128) : WordRAM.Exec w prepareNode x (nodeState x) 10

Complete node argument delivery is ten native copies; no address arithmetic is hidden.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.callModulus_exec {w : ℕ} (x : WordRAM.Data 128) (values : Fin 3 → ℕ → ℤ) (hm : 2 ≤ x.regs limit) (hmod : GenericRAM.Signed.Fits w ↑(x.regs limit ^ 2)) (hbudget : WordRAM.Fits (w + 2) (Modulus.budget (WordRAM.Data.comap kernel (modulusState x)))) (hcard : x.regs primeCount = (x.regs limit).primesLE.card) (hbefore : x.regs bitmap + x.regs limit < x.regs heap) (hbitmap : ∀ q ≤ x.regs limit, x.mem (x.regs bitmap + q) = if Nat.Prime q then 1 else 0) (hvalues : ∀ (j : Fin 3), ∀ i < x.regs (arrayLength j), GenericRAM.Signed.Fits w (values j i)) (hsrc : ∀ (j : Fin 3), x.regs (arraySource j) + x.regs (arrayLength j) ≤ x.regs heap) (hinput : ∀ (j : Fin 3), ∀ i < x.regs (arrayLength j), x.mem (x.regs (arraySource j) + i) = WordRAM.Signed.encode (values j i)) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (x.regs (arrayLength j)))) : ∃ (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) (prepareModulus.seq (WordRAM.Code.rename kernel Modulus.program)) x y (14 + Modulus.cost (WordRAM.Data.comap kernel (modulusState x))) ∧ (∀ (i : Fin 128), 64 ≤ ↑i → y.regs i = x.regs i) ∧ (∀ a < x.regs heap, y.mem a = x.mem a) ∧ y.regs (kernel Modulus.output) = ThreeSum.ChanHe.modulus (x.regs limit).primesLE (x.regs digits) (Finset.image (values 0) (Finset.range (x.regs (arrayLength 0)))) (Finset.image (values 1) (Finset.range (x.regs (arrayLength 1)))) (Finset.image (values 2) (Finset.range (x.regs (arrayLength 2)))) ∧ 1 ≤ y.regs (kernel Modulus.output) ∧ y.regs (kernel Modulus.output) ≤ x.regs limit ^ 2

Actual argument delivery and complete two-prime computation inside the traversal's fixed register file. The mathematical filters may fail; their default-one selections are still bounded. The bitmap/count are the outputs of the separate native prime-table routine.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.callNode_exec {w : ℕ} (x : WordRAM.Data 128) (values : Fin 3 → ℕ → ℤ) (hM : 0 < x.regs selected) (hN : 2 * x.regs selected ≤ x.regs groups) (hwidth : GenericRAM.Signed.Fits w ↑(NodePacking.layout (WordRAM.Data.comap kernel (nodeState x))).budget) (hsrc : ∀ (j : Fin 3), x.regs (arraySource j) + x.regs (arrayLength j) ≤ x.regs heap) (hbdd : ∀ (j : Fin 3), ∀ i < x.regs (arrayLength j), (values j i).natAbs ≤ x.regs magnitude) (hinput : ∀ (j : Fin 3), ∀ i < x.regs (arrayLength j), x.mem (x.regs (arraySource j) + i) = WordRAM.Signed.encode (values j i)) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (x.regs (arrayLength j)))) : have L := NodePacking.layout (WordRAM.Data.comap kernel (nodeState x)); ∃ (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) (prepareNode.seq (WordRAM.Code.rename kernel NodePacking.program)) x y (10 + 66 * L.total + 15 * L.M + 12 * L.N + 228) ∧ NodePacking.Output L values x.mem y.mem ∧ ∀ (i : Fin 128), 64 ≤ ↑i → y.regs i = x.regs i

Ten actual argument copies followed by the complete native heavy/packed-node program. The existing exact semantic output and the full allocation frame survive register renaming.