Charged native execution of the Chan–He traversal controller #
The zero-fuel case executes setup, a complete record push, a complete record pop, both loop tests, and the skip branch. It preserves the accumulated output count, heap and memory outside the reserved stack. It does not silently replace a negative 3SUM instance by an empty output.
Main results #
oneRoot_zero: exact 173-instruction execution of the complete controller at zero fuel.
The controller composition proofs are original. General supplied-root traversal correctness is
proved in TraversalRoot.root_exec; complete initialized-input preprocessing is composed in
PreprocessingInput.runs_input.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.oneRoot_zero {w capacity : ℕ} (x : WordRAM.Data 128) (hx : WordRAM.Data.Bounded w x) (h2 : WordRAM.Fits w 2) (hcap : WordRAM.Fits w (x.regs stackBase + capacity)) (hcapacity : 7 ≤ capacity) (hf : x.regs (slot 0) = 0) :
∃ (y : WordRAM.Data 128),
WordRAM.Exec w oneRoot x y 173 ∧ WordRAM.Stack.Rep w (x.regs stackBase) capacity [] (WordRAM.Data.comap registers y) ∧ (∀ (i : Fin 7), y.regs (slot i) = x.regs (slot i)) ∧ y.regs outputCount = x.regs outputCount ∧ y.regs heap = x.regs heap ∧ WordRAM.Modifies (WordRAM.Stack.footprint (x.regs stackBase) capacity) x.mem y.mem
Even zero fuel executes all native setup and stack work. No node is emitted, and the root record is recovered exactly. Existing output arrays and all non-stack memory are preserved.