Concrete worklist invariant for the native Chan–He traversal

The invariant connects the reserved native stack, existing finite recursion, retained arrays, output-pointer table and fresh heap. Remaining work pays for both future output cells and future allocations. In particular, allocation bounds decrease with the mathematical work measure rather than granting an unbounded heap to each kernel call.

Main definitions

• Arena: fixed caller parameters and disjoint stack/table/heap reservations.
• Cursor: represented pending entries and the already emitted native pointers and nodes.
• Cursor.Invariant: readback, frames, exact remaining output and concrete space reservations.

These proof invariants are original and do not add a machine model or operational oracle.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Arena : Type

Fixed parameters and concrete memory reservations of a complete native root traversal.

• n : ℕ

  Maximum column cardinality.

• m : ℕ

  Candidate-prime bound.

• Λ : ℕ

  Label-bit parameter.

• U : ℕ

  Node input magnitude.

• N : ℕ

  Common number of four-cell packed groups.

• fuel : ℕ

  Root recursion fuel.

• primes : ℕ

  Prime bitmap base.

• stack : ℕ

  Reserved native word-stack base.

• capacity : ℕ

  Reserved native word-stack capacity.

• table : ℕ

  Unsigned output-pointer table base.

• outputCapacity : ℕ

  Reserved output-pointer table capacity.

• floor : ℕ

  First address permitted for allocated heavy and packed arrays.

• ceiling : ℕ

  Final upper bound on the fresh heap pointer.

• retained : ℕ → ℕ

  Protected original memory below the stack, including the complete frontend forest.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Arena.Controls (a : Arena) (x : WordRAM.Data 128) : Prop

Persistent caller registers, including actual zero and one used by native branches.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Arena.Controls.congr {a : Arena} {x y : WordRAM.Data 128} (h : a.Controls x) (hp : ∀ (i : Fin 128), ↑i ∈ [71, 72, 73, 74, 75, 76, 78, 80, 81, 82, 83] → y.regs i = x.regs i) : a.Controls y

Exact register preservation transfers all persistent caller parameters. The heap and accumulated count are deliberately absent from this fixed register set.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Arena.Separated (a : Arena) : Prop

Concrete non-overlap and capacity obligations for the reserved native layout.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Arena.Ready (a : Arena) (w : ℕ) : Prop

A single signed envelope covers both actual native kernels at every worklist transition.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Arena.Bitmap (a : Arena) (mem : ℕ → ℕ) : Prop

The actual native bitmap is retained below the reserved stack.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Cursor : Type

Proof state of the actual stack loop; no part of this structure is evaluated by the program.

• pending : List Entry

  Top-first pending entries.

• emitted : List (ℕ × ThreeSum.ChanHe.Node)

  Packed base pointers and their existing mathematical nodes in emitted order.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Cursor.work (s : Cursor) : ℕ

Remaining transitions include empty entries and zero-fuel leaves.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Cursor.Invariant (a : Arena) (w : ℕ) (target : List ThreeSum.ChanHe.Node) (s : Cursor) (x : WordRAM.Data 128) : Prop

Full readback and allocation invariant at the actual native loop header.

• bounded : WordRAM.Data.Bounded (w + 2) x

  All actual native words fit.

• controls : a.Controls x

  Persistent caller parameters have not changed.

• bitmap : a.Bitmap x.mem

  The actual bitmap still represents all candidate primes.

• stack : WordRAM.Stack.Rep (w + 2) a.stack a.capacity (List.flatMap Entry.words s.pending) (WordRAM.Data.comap registers x)

  The actual word stack represents exactly the pending entries.

• depth : Math.Bounded a.fuel (List.map Entry.task s.pending)

  The existing finite depth invariant bounds pending entries.

• valid (e : Entry) : e ∈ s.pending → e.Valid a.n a.U

  Every pending entry retains its duplicate-free existing admissibility promise.

• stored (e : Entry) : e ∈ s.pending → e.Stored x.mem

  Every pending array has exact signed-encoded native readback.

• around (e : Entry) : e ∈ s.pending → e.Around a.stack (a.floor - a.stack)

  Pending arrays avoid the entire reserved stack and output-table gap.

• ends (e : Entry) : e ∈ s.pending → ∀ (j : Fin 3), e.source j + (e.data j).length ≤ x.regs heap

  Every pending array lies below the current fresh allocation.

• floor : a.floor ≤ x.regs heap

  The fresh heap never enters the reserved table or stack.

• heapBudget : x.regs heap + s.work * allocationSize a.n a.m a.N ≤ a.ceiling

  Remaining work reserves enough space for every later allocation.

• count : x.regs outputCount = s.emitted.length

  The accumulated native count equals the actual emitted sequence length.

• tableBudget : s.emitted.length + s.work ≤ a.outputCapacity

  Remaining work reserves enough output-table cells.

• output : StoredNodes a.U a.N a.table s.emitted x.mem

  Every emitted pointer and every packed cell has exact existing-node readback.

• outputBounds (i : Fin s.emitted.length) : a.floor ≤ s.emitted[↑i].1 ∧ s.emitted[↑i].1 + 4 * a.N ≤ x.regs heap

  Retained packed arrays lie above the reserved output table and below the fresh heap.

• exactOutput : List.map Prod.snd s.emitted ++ Math.output a.m.primesLE a.Λ (List.map Entry.task s.pending) = target

  The emitted prefix followed by the exact pending recursion is the target sequence.

• protectedMemory (p : ℕ) : p < a.stack → x.mem p = a.retained p

  Every original cell below the reserved stack remains available to subsequent roots.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Cursor.Invariant.nonempty {a : Arena} {w : ℕ} {target : List ThreeSum.ChanHe.Node} {s : Cursor} {x : WordRAM.Data 128} (h : Invariant a w target s x) (hc : (WordRAM.Cond.lt zero (registers WordRAM.Stack.len)).Holds x) : s.pending ≠ []

A live loop has at least one pending entry, since each entry occupies seven actual words.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Cursor.Invariant.finished {a : Arena} {w : ℕ} {target : List ThreeSum.ChanHe.Node} {s : Cursor} {x : WordRAM.Data 128} (h : Invariant a w target s x) (hc : ¬(WordRAM.Cond.lt zero (registers WordRAM.Stack.len)).Holds x) : s.pending = [] ∧ List.map Prod.snd s.emitted = target

A finished actual loop has emitted the complete target, with every array already read back.