Composing every computed native preprocessing root #
Starting from the complete frontend's actual output, the native program computes its shared prime table and reservations, then executes every actual descriptor and recursion tree.
Main results #
afterFrontend_exec: the complete native suffix has exact finite node output and charged cost.
The native composition proofs are original. No runtime algorithm or fit advice is supplied.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.afterFrontend_exec {κ w : ℕ} (input : List ℤ) (rs : List (ℕ × ℕ)) (x : WordRAM.Data 128) (hw : width κ input.length ≤ w + 2) (hx : WordRAM.Data.Bounded (w + 2) x) (hvalues : ∀ z ∈ input, |z| ≤ ↑((input.length + 2) ^ κ)) (hfront : Frontend.Output (Frontend.layout κ input.length) ((input.length + 2) ^ κ) rs x.mem) (hparams : Parameters.Output input.length ((input.length + 2) ^ κ) (WordRAM.Data.comap Frontend.parameterRegisters x)) (hbase : x.regs Frontend.descriptorBase = (Frontend.layout κ input.length).descriptors) (hcount : x.regs Frontend.descriptorCount = (Frontend.layout κ input.length).count) (hend : x.regs Frontend.heapEnd = (Frontend.layout κ input.length).endpoint) (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 ≤ input.length) :
have n := input.length;
have U := (n + 2) ^ κ;
have m := ThreeSum.ChanHe.mPar n (2 * U);
have F := ThreeSum.ChanHe.fuel n;
have l := Frontend.layout κ n;
∃ (out : List (ℕ × ThreeSum.ChanHe.Node)) (y : WordRAM.Data 128),
WordRAM.ExecWithin (w + 2) afterFrontend x y
((m + 1) * (7 * m + 15) + 8 + 4 * F + 45 + l.count * (Traversal.rootTime F (n + 1) m (2 * m ^ 2) + 17)) ∧ List.map Prod.snd out = Traversal.Math.output m.primesLE l.digits (List.map Traversal.Entry.task (entries l U rs)) ∧ Traversal.StoredNodes (2 * U) (2 * m ^ 2) (arena κ n x.mem).table out y.mem ∧ y.regs Traversal.outputCount = out.length ∧ y.regs Traversal.outputs = (arena κ n x.mem).table ∧ y.regs packedLength = 8 * m ^ 2
The complete actual suffix consumes only computed frontend output and a global width.