Executing the next actual frontend root #
The actual descriptor loads establish the complete root program's ABI. Global remaining-root reservations derive its local arena, rather than supplying another assumed execution contract.
Main results #
execute_next_root: actual loads followed by the complete native traversal, with exact output.
The native composition and resource proofs are original.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.execute_next_root {a : Traversal.Arena} {w U : ℕ} {l : Frontend.Layout} {input : List ℤ} {rs : List (ℕ × ℕ)} {s : ForestCursor} {x : WordRAM.Data 128} (ha : a.Separated) (hw : a.Ready w) (h : ForestCursor.Invariant a w l U rs s x) (hc : (WordRAM.Cond.lt current roots).Holds x) (hn : a.n = l.n + 1) (hU : a.U = 2 * U) (hfront : l.endpoint ≤ a.stack) (hkeys : ∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ List.map WordRAM.Signed.encode input) (hnd : (List.map Prod.fst rs).Nodup) (hcard : rs.length ≤ l.n) (hvalues : ∀ z ∈ input, |z| ≤ ↑U) :
have e := entry l U a.fuel rs s.index;
∃ (out : List (ℕ × ThreeSum.ChanHe.Node)) (y : WordRAM.Data 128),
WordRAM.ExecWithin (w + 2) (loadRoot.seq Traversal.oneRoot) x y (14 + Traversal.rootTime a.fuel a.n a.m a.N) ∧ Traversal.Cursor.Invariant (rootArena a x s.nodes) w
(List.map Prod.snd s.nodes ++ Traversal.Math.Task.output a.m.primesLE a.Λ e.task)
{ pending := [], emitted := out } y ∧ List.map Prod.snd out = List.map Prod.snd s.nodes ++ Traversal.Math.Task.output a.m.primesLE a.Λ e.task ∧ (∀ p < a.stack, y.mem p = x.mem p) ∧ ∀ (i : Fin 128), 109 ≤ ↑i → i ≠ address → y.regs i = x.regs i
Execute the next actual descriptor and its full recursion within that root's own budget.