Complete native root evaluation and ordered reporting #
Main results #
PrunedQuery.exec_evaluate: actual root deduplication, all-depth native traversal and ordered reporting, allowing duplicate input queries and arbitrary original memory outside the workspace.
The query function specifies the words of the supplied input list. The machine computes its own
distinct set, every recursive child list and every reported index. All scratch addresses, signed
fits, fresh generations and instruction charges follow from the ordinary numerical premises.
This module is an internal implementation API used to prove the initialized and pointer-based
client interfaces in Pruned.Flat, Pruned.Width and Pruned.Kernel.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_evaluate {w L f a0 b0 q0 o0 Q E A B : ℕ} (a b : MatrixMultiplication.Schonhage.Leaf L → ℤ) (qs : Fin Q → MatrixMultiplication.Schonhage.OutStr L) (x : WordRAM.Data registers) (hregs : KernelRegs L f a0 b0 x) (hQ : x.regs queryCount = Q) (hq0 : x.regs queries = q0) (ho0 : x.regs output = o0) (hE : x.regs epoch = E) (hinput : ∀ (i : Fin Q), x.mem (q0 + ↑i) = ↑(queryIndex (qs i))) (hleft :
∀ (v : MatrixMultiplication.Schonhage.Leaf L), x.mem (a0 + ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (a v)) (hright :
∀ (v : MatrixMultiplication.Schonhage.Leaf L), x.mem (b0 + ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (b v)) (hbeforeA : a0 + 10 ^ L ≤ f) (hbeforeB : b0 + 10 ^ L ≤ f) (hqueryOut : q0 + Q ≤ o0) (houtFrame : o0 + Q ≤ f) (hmarks : ∀ q < 10 ^ L, x.mem (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + q) ≤ E) (ha : ∀ (v : MatrixMultiplication.Schonhage.Leaf L), |a v| ≤ ↑A) (hb : ∀ (v : MatrixMultiplication.Schonhage.Leaf L), |b v| ≤ ↑B) (hw : 0 < w) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (evaluationBudget L f a0 b0 q0 o0 Q E)) :
∃ (y : WordRAM.Data registers),
WordRAM.ExecWithin (w + 2) (rootList.seq (controller.seq report)) x y
(29 * Q + traceWeight (Finset.image qs Finset.univ) + 24) ∧ (∀ (i : Fin Q),
y.mem (o0 + ↑i) = WordRAM.Signed.encode
(MatrixMultiplication.Schonhage.Pruned.result L a b (Finset.image qs Finset.univ) (qs i))) ∧ (∀ (c : ℕ),
¬(o0 ≤ c ∧ c < o0 + Q) → ¬(f ≤ c ∧ c < f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + 10 ^ L) → y.mem c = x.mem c) ∧ y.regs output = o0 ∧ E + 1 ≤ y.regs epoch ∧ y.regs epoch ≤ E + 1 + epochAllowance L ∧ ∀ q < 10 ^ L, y.mem (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + q) ≤ y.regs epoch
Evaluate the actual supplied queries after workspace pointers have been computed. The result uses the existing finite request-set semantics; no initialized directory or traversal certificate is supplied. Only the original source cells and an upper bound on old timestamps are required.