Native stack calls for Chan–He traversal records

Traversal keeps a seven-word record in registers 64–70 and the existing bounded stack in registers 96–104. Registers below 64 remain available to the complete modulus and node programs. Each record contains fuel followed by three base/length pairs. The stack stores words, so a record is pushed in reverse order and popped in forward order.

The dispatcher, representation and memory frame are reused from Cslib.WordRAM.Stack. Argument delivery and result copies here are actual native instructions and are charged.

Main definitions

• slot: the seven persistent traversal-record registers.
• registers: the existing nine-register stack dispatcher inside the 128-register controller.
• pushSlot: native argument delivery followed by the complete bounded-stack dispatcher.
• popSlot: native dispatch and result delivery to one traversal-record register.

Main results

• pushSlot_exec: a nine-instruction push, with the exact stack, memory and register frames.
• popSlot_exec: a fourteen-instruction nonempty pop with the same exact frames.
• pushFrame_exec, popFrame_exec: complete seven-word record transfers in 64 and 99 instructions.

The native controller and its composition proofs are original.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.slot (i : Fin 7) : Fin 128

Fuel and the three base/length pairs, retained across both 64-register native kernels.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.arraySource (j : Fin 3) : Fin 128

Pointer word of the selected pending set.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.arrayLength (j : Fin 3) : Fin 128

Length word of the selected pending set.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.registers (i : Fin 9) : Fin 128

The existing stack's workspace lies above every 64-register node-kernel register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Outside (i : Fin 128) : Prop

Caller-owned registers outside the stack dispatcher.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.pushSlot (i : Fin 7) : WordRAM.Code WordRAM.Basis.standard 128

Deliver the push tag and actual record word, then execute the existing stack program.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.pushSlot_exec {w base capacity : ℕ} (i : Fin 7) (x : WordRAM.Data 128) (vs : List ℕ) (h2 : WordRAM.Fits w 2) (hcap : WordRAM.Fits w (base + capacity)) (hr : WordRAM.Stack.Rep w base capacity vs (WordRAM.Data.comap registers x)) (hw : WordRAM.Fits w (x.regs (slot i))) (hv : vs.length < capacity) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w (pushSlot i) x y 9 ∧ WordRAM.Stack.Rep w base capacity (x.regs (slot i) :: vs) (WordRAM.Data.comap registers y) ∧ WordRAM.Modifies (WordRAM.Stack.footprint base capacity) x.mem y.mem ∧ ∀ (j : Fin 128), Outside j → y.regs j = x.regs j

Each native push includes both argument instructions, not a host-level stack operation. Every register outside 96–104 and every memory cell outside the reserved stack is preserved.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.pushFrame : WordRAM.Code WordRAM.Basis.standard 128

Push all seven words in reverse order, so the next seven pops recover the record in order. The trailing self-copy gives the fixed empty suffix an ordinary native instruction.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.pushFrame_exec {w base capacity : ℕ} (x : WordRAM.Data 128) (vs : List ℕ) (h2 : WordRAM.Fits w 2) (hcap : WordRAM.Fits w (base + capacity)) (hr : WordRAM.Stack.Rep w base capacity vs (WordRAM.Data.comap registers x)) (hw : ∀ (i : Fin 7), WordRAM.Fits w (x.regs (slot i))) (hv : 7 + vs.length ≤ capacity) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w pushFrame x y 64 ∧ WordRAM.Stack.Rep w base capacity ([x.regs (slot 0), x.regs (slot 1), x.regs (slot 2), x.regs (slot 3), x.regs (slot 4), x.regs (slot 5), x.regs (slot 6)] ++ vs) (WordRAM.Data.comap registers y) ∧ WordRAM.Modifies (WordRAM.Stack.footprint base capacity) x.mem y.mem ∧ ∀ (j : Fin 128), Outside j → y.regs j = x.regs j

The complete native frame push charges all seven dispatches and argument delivery. There is no host-level record write, and the exact seven-word sequence is at the stack top.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.popSlot (i : Fin 7) : WordRAM.Code WordRAM.Basis.standard 128

Deliver the pop tag, execute the complete dispatcher, and copy its answer to the record.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.popSlot_exec {w base capacity : ℕ} (i : Fin 7) (x : WordRAM.Data 128) (v : ℕ) (vs : List ℕ) (h2 : WordRAM.Fits w 2) (hcap : WordRAM.Fits w (base + capacity)) (hr : WordRAM.Stack.Rep w base capacity (v :: vs) (WordRAM.Data.comap registers x)) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w (popSlot i) x y 14 ∧ WordRAM.Stack.Rep w base capacity vs (WordRAM.Data.comap registers y) ∧ y.regs (slot i) = v ∧ WordRAM.Modifies (WordRAM.Stack.footprint base capacity) x.mem y.mem ∧ ∀ (j : Fin 128), Outside j → j ≠ slot i → y.regs j = x.regs j

A nonempty native pop includes both argument instructions and the actual result copy. Only the selected record register, stack workspace and reserved stack memory may change.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.popFrame : WordRAM.Code WordRAM.Basis.standard 128

Pop all seven words into the record, in forward order, using the native dispatcher.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.popFrame_exec {w base capacity : ℕ} (x : WordRAM.Data 128) (vs : List ℕ) (a : Fin 7 → ℕ) (h2 : WordRAM.Fits w 2) (hcap : WordRAM.Fits w (base + capacity)) (hr : WordRAM.Stack.Rep w base capacity ([a 0, a 1, a 2, a 3, a 4, a 5, a 6] ++ vs) (WordRAM.Data.comap registers x)) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w popFrame x y 99 ∧ WordRAM.Stack.Rep w base capacity vs (WordRAM.Data.comap registers y) ∧ (∀ (i : Fin 7), y.regs (slot i) = a i) ∧ WordRAM.Modifies (WordRAM.Stack.footprint base capacity) x.mem y.mem ∧ ∀ (j : Fin 128), Outside j → ↑j < 64 ∨ 71 ≤ ↑j → y.regs j = x.regs j

The complete record pop charges every argument, dispatch and result-copy instruction. The seven restored words have their original order; other caller registers are preserved.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.not_readsWidth : ¬pushFrame.ReadsWidth ∧ ¬popFrame.ReadsWidth

Record transfers do not inspect the physical word width.