Complete native frontend-root loop #
Every iteration loads the next actual descriptor, executes its complete bounded recursion and increments the native index. Remaining-root reservations pay for every later iteration.
Main results #
forest_body_exec: actual root execution preserves the global resource and output invariant.forest_exec: the entire actual outer loop emits exactly the finite frontend forest.
These composition proofs are original and use the existing charged native loop rule.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.forest_body_exec {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) (hf : a.fuel = ThreeSum.ChanHe.fuel l.n) (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) :
∃ (s' : ForestCursor) (y : WordRAM.Data 128),
WordRAM.ExecWithin (w + 2) body x y (Traversal.rootTime a.fuel a.n a.m a.N + 15) ∧ ForestCursor.Invariant a w l U rs s' y ∧ l.count - s'.index < l.count - s.index
An actual root execution leaves enough heap and table capacity for all later roots.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.forest_exec {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) (hn : a.n = l.n + 1) (hU : a.U = 2 * U) (hf : a.fuel = ThreeSum.ChanHe.fuel l.n) (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) :
∃ (s' : ForestCursor) (y : WordRAM.Data 128),
WordRAM.ExecWithin (w + 2) forest x y ((l.count - s.index) * (Traversal.rootTime a.fuel a.n a.m a.N + 17) + 2) ∧ ForestCursor.Invariant a w l U rs s' y ∧ s'.index = l.count ∧ List.map Prod.snd s'.nodes = Traversal.Math.output a.m.primesLE a.Λ (List.map Traversal.Entry.task (entries l U rs))
Execute every native frontend root with exact finite output and all loop control charged.