Fixed native controller for one Chan–He recursion tree

The controller pops actual seven-word records, skips zero fuel or empty inputs, computes the modulus, constructs the complete heavy and packed outputs, records the packed pointer, and pushes the three children. Children are pushed third, second, first so the existing native stack visits them in the mathematical preorder. Fresh allocations follow every live node; all earlier arrays, the prime bitmap, stack reservation and output table precede the heap.

This module defines executable code. Its correctness and resource proofs belong to the traversal development; these definitions alone do not certify a native preprocessing bound. The frontend and initialized-input composition remain separate.

Main definitions

• oneRoot: the finite native traversal controller, independent of fuel, input sizes and width.
• visit: complete native modulus and node construction, including output delivery.
• pushChildren: actual reverse-order stack pushes preserving the original three descriptors.

The native code is original and reuses the existing finite Chan–He construction.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.kernel (i : Fin 64) : Fin 128

The complete node kernels occupy registers 0–63.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.limit : Fin 128

The supplied candidate-prime bound.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.digits : Fin 128

The supplied label-bit parameter.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.magnitude : Fin 128

The common input-magnitude bound of the tree.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.groups : Fin 128

The common number of packed four-cell groups.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.bitmap : Fin 128

The prime bitmap, retained below the heap.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.primeCount : Fin 128

The exact number of candidate primes.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.heap : Fin 128

The current fresh allocation base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.outputs : Fin 128

The reserved output-pointer table.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.outputCount : Fin 128

Accumulated output count; this is not reset between roots.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.stackBase : Fin 128

The reserved word-stack base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.stackCapacity : Fin 128

The reserved word-stack capacity, used by the safety specification.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.zero : Fin 128

Controller constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.one : Fin 128

Controller constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.temporary : Fin 128

Controller address temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.selected : Fin 128

The computed unsigned modulus.

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

The three computed heavy lengths.

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

The three computed heavy bases.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.packed : Fin 128

Current packed-array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.endpoint : Fin 128

One-past-end of the current node allocation.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.original (i : Fin 4) : Fin 128

Saved original descriptor words, outside both kernels and the stack dispatcher.

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

Fourteen actual instructions deliver the modulus program's complete caller ABI.

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

Ten actual copies deliver the complete node builder's caller ABI.

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

Read the three actual count cells, record the packed pointer, and advance the fresh heap.

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

Complete actual native calls, with argument preparation, modulus copy and output delivery.

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

Decrease fuel, retain both descriptors needed for restoration, and prepare the third child.

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

Restore the third original descriptor and prepare the second child.

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

Restore the second original descriptor and prepare the first child.

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

Push third, second, first. Every child retains the two other original set descriptors.

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

A popped record either skips exactly the mathematical guard or executes the complete node.

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

The actual pending-word stack, including zero-fuel and empty entries, controls the loop.

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

The complete finite native controller for one supplied root. It appends to the caller's output table, retaining the accumulated count and advancing the fresh allocation base.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.oneRoot_not_readsWidth : ¬oneRoot.ReadsWidth

The same finite controller is used at every admitted word width.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.oneRoot_size : oneRoot.size ≤ 65536

The native controller has a fixed finite instruction list, independent of recursion fuel.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.oneRoot_preserves (i : Fin 128) : 109 ≤ ↑i → WordRAM.Code.Preserves i oneRoot

Registers 109–127 are retained for the outer frontend-forest controller.