Shared resources across all native frontend roots

The outer loop reserves heap and pointer cells for every remaining root. A particular root gets only its own remaining allocation, so its execution theorem cannot consume another root's budget.

Main definitions

• rootArena: the existing traversal arena restricted to one root's actual remaining budget.
• ForestCursor, ForestCursor.Invariant: exact root index, output and global resource relation.

Main results

• rootArena_ready: the global signed envelope derives each dynamic root envelope.

These native composition invariants are original; the program remains the existing native code.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.rootArena (a : Traversal.Arena) (x : WordRAM.Data 128) (ns : List (ℕ × ThreeSum.ChanHe.Node)) : Traversal.Arena

Restrict a root call to its own heap and pointer-table allowance. All addresses stay fixed.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.rootArena_ready {a : Traversal.Arena} {w : ℕ} {x : WordRAM.Data 128} {ns : List (ℕ × ThreeSum.ChanHe.Node)} (hw : a.Ready w) (hh : (rootArena a x ns).ceiling ≤ a.ceiling) : (rootArena a x ns).Ready w

Monotonicity of the existing polynomial envelope derives every root's actual local fit.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.ForestCursor : Type

Mathematical proof state of the native outer descriptor loop.

• index : ℕ

  Number of root descriptors already executed.

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

  Actual native pointer and existing-node pairs already emitted.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.ForestCursor.Invariant (a : Traversal.Arena) (w : ℕ) (l : Frontend.Layout) (U : ℕ) (rs : List (ℕ × ℕ)) (s : ForestCursor) (x : WordRAM.Data 128) : Prop

Exact frontend output, native controller registers and all remaining-root reservations.

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

  Every actual word fits.

• controls : a.Controls x

  The traversal constants remain actual registers.

• frontend : Frontend.Output l U rs x.mem

  Every frontend descriptor and compact array is still available.

• descriptors : x.regs Preprocessing.descriptors = l.descriptors

  Actual descriptor base and root count.

• roots : x.regs Preprocessing.roots = l.count
• current : x.regs Preprocessing.current = s.index

  Actual root index and shared fuel.

• levels : x.regs Preprocessing.levels = a.fuel
• stride : x.regs Preprocessing.stride = 6

  Native descriptor stride and outer increment constant.

• one : x.regs Preprocessing.one = 1
• index_le : s.index ≤ l.count

  The actual index never passes the last descriptor.

• bitmap : a.Bitmap x.mem

  Every candidate prime still has its actual bitmap bit.

• floor : a.floor ≤ x.regs Traversal.heap

  The heap avoids all shared reservations.

• heapBudget : x.regs Traversal.heap + (l.count - s.index) * (Traversal.Math.work a.fuel * Traversal.allocationSize a.n a.m a.N) ≤ a.ceiling

  All unprocessed roots retain their complete allocation budgets.

• count : x.regs Traversal.outputCount = s.nodes.length

  The native count agrees with the emitted list.

• tableBudget : s.nodes.length + (l.count - s.index) * Traversal.Math.work a.fuel ≤ a.outputCapacity

  All unprocessed roots retain their complete pointer-table budgets.

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

  Exact native pointer-table and packed-cell readback.

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

  Every earlier packed array is safely below the current fresh allocation.

• exactOutput : List.map Prod.snd s.nodes ++ Traversal.Math.output a.m.primesLE a.Λ (List.map Traversal.Entry.task (List.drop s.index (entries l U rs))) = Traversal.Math.output a.m.primesLE a.Λ (List.map Traversal.Entry.task (entries l U rs))

  The emitted prefix and untouched roots give exactly the original finite forest.

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

  Original memory below the shared stack is retained throughout the forest.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.ForestCursor.Invariant.root_budgets {a : Traversal.Arena} {w U : ℕ} {l : Frontend.Layout} {rs : List (ℕ × ℕ)} {s : ForestCursor} {x : WordRAM.Data 128} (h : Invariant a w l U rs s x) (hc : (WordRAM.Cond.lt Preprocessing.current Preprocessing.roots).Holds x) : (rootArena a x s.nodes).ceiling ≤ a.ceiling ∧ (rootArena a x s.nodes).outputCapacity ≤ a.outputCapacity

A live outer iteration has room for the one root it is about to execute.