Native preparation of the three Chan–He child records

The third child is pushed first. Original descriptors are retained above the stack dispatcher and restored before replacing another column. All descriptor moves and the fuel decrement are native instructions; the same finite code is used at every recursion level.

Main definitions

• thirdState, secondState, firstState: exact states after the native child-argument blocks.
• childWords: the seven actual words of one child record, in its pop order.

Main results

• prepareThird_exec, prepareSecond_exec, prepareFirst_exec: charged native argument blocks.

The native stack controller and proofs are original.

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

Save both descriptors needed for restoration and prepare the third child.

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

Restore the third original column and prepare the second child.

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

Restore the second original column and prepare the first child.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.childWords (x : WordRAM.Data 128) (j : Fin 3) : List ℕ

Exact child-record serialization. Only the selected column is replaced by its heavy output.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.length_childWords (x : WordRAM.Data 128) (j : Fin 3) : (childWords x j).length = 7

Every child occupies exactly one seven-word native record.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.prepareThird_exec {w : ℕ} (x : WordRAM.Data 128) (hx : WordRAM.Data.Bounded w x) (hone : x.regs one = 1) : WordRAM.Exec w prepareThird x (thirdState x) 7

The fuel subtraction and all six descriptor copies cost seven native instructions.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.prepareSecond_exec {w : ℕ} (x : WordRAM.Data 128) : WordRAM.Exec w prepareSecond x (secondState x) 4

Restoring the third column and replacing the second costs four native copies.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.prepareFirst_exec {w : ℕ} (x : WordRAM.Data 128) : WordRAM.Exec w prepareFirst x (firstState x) 4

Restoring the second column and replacing the first costs four native copies.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.pushChildren_preserves (i : Fin 128) : 71 ≤ ↑i ∧ ↑i < 96 ∨ 109 ≤ ↑i → WordRAM.Code.Preserves i pushChildren

Child pushes preserve every persistent controller parameter outside the record and stack.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.pushChildren_exec {w base capacity : ℕ} (x : WordRAM.Data 128) (vs : List ℕ) (hx : WordRAM.Data.Bounded w x) (hone : x.regs one = 1) (h2 : WordRAM.Fits w 2) (hcap : WordRAM.Fits w (base + capacity)) (hr : WordRAM.Stack.Rep w base capacity vs (WordRAM.Data.comap registers x)) (hcapacity : 21 + vs.length ≤ capacity) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w pushChildren x y 207 ∧ WordRAM.Stack.Rep w base capacity (childWords x 0 ++ childWords x 1 ++ childWords x 2 ++ vs) (WordRAM.Data.comap registers y) ∧ WordRAM.Modifies (WordRAM.Stack.footprint base capacity) x.mem y.mem ∧ ∀ (i : Fin 128), 71 ≤ ↑i ∧ ↑i < 96 ∨ 109 ≤ ↑i → y.regs i = x.regs i

All three child records are pushed by native instructions in reverse order. The resulting top-first stack contains first, second, third, followed by the original pending suffix.