Callable native pruned-query kernel #
Main results #
PrunedQuery.exec_kernel: compute powers/layout, deduplicate supplied queries, execute the complete pruned traversal and report answers using ordinary caller pointers and a fresh epoch.
Input arrays contain canonical Signed.encode words. Query codes, pointers, depth and count are
raw unsigned words. The caller supplies only the source arrays/list and old timestamp bound;
all frames, child lists and decisions are computed by the fixed code. The returned directory
bound permits reuse across tiles without a free dense-directory initialization per call.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_kernel {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) (hL : x.regs inputDepth = L) (hA : x.regs arrayA = a0) (hB : x.regs arrayB = b0) (hQ : x.regs queryCount = Q) (hq0 : x.regs queries = q0) (ho0 : x.regs output = o0) (hf : x.regs scratch = f) (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) (kernelBudget L f a0 b0 q0 o0 Q E)) :
∃ (y : WordRAM.Data registers),
WordRAM.ExecWithin (w + 2) kernel x y (4 * L + 29 * Q + traceWeight (Finset.image qs Finset.univ) + 41) ∧ (∀ (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
The actual pointer-argument kernel, with computed powers and workspace partition, preserves all memory outside its output and explicit scratch intervals. No initialized frame/list or child execution premise is used. The original input magnitude envelope derives every signed fit.