All-depth execution of the native pruned controller #
Main results #
PrunedQuery.exec_ready: the fixed controller computes the existing pruned recursion, with actual stored child lists, signed values, frames and a bound charged to its mathematical trace.
The induction composes only Code.ExecWithin for the existing standard unsigned machine. Its
continuation form stops the inductive node at the parent return cursor; at the root the proved
zero active flag supplies the ordinary native loop-exit execution.
The stage execution lemmas and node invariants here are internal implementation APIs,
exported for proof composition across modules. Callers use Pruned.Kernel or Pruned.Flat.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_ready {w L f a0 b0 A B : ℕ} (n : ℕ) {d p E : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr n)) (a b : MatrixMultiplication.Schonhage.Leaf n → ℤ) (x : WordRAM.Data registers) (hx : NodeReady L f a0 b0 n d p E S x) (hleft :
∀ (v : MatrixMultiplication.Schonhage.Leaf n),
x.mem (a0 + p + 10 ^ d * ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (a v)) (hright :
∀ (v : MatrixMultiplication.Schonhage.Leaf n),
x.mem (b0 + p + 10 ^ d * ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (b v)) (hbeforeA : a0 + 10 ^ L ≤ f) (hbeforeB : b0 + 10 ^ L ≤ f) (ha : ∀ (v : MatrixMultiplication.Schonhage.Leaf n), |a v| ≤ ↑A) (hb : ∀ (v : MatrixMultiplication.Schonhage.Leaf n), |b v| ≤ ↑B) (hw : 0 < w) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (nodeBudget L f a0 b0 E n)) :
∃ (y : WordRAM.Data registers),
NodeResult L f a0 b0 n d E S a b x y ∧ ∀ (z : WordRAM.Data registers) (U : ℕ),
WordRAM.ExecWithin (w + 2) controller y z U → WordRAM.ExecWithin (w + 2) controller x z (traceWeight S + U)
An arbitrary-depth ready node returns the unchanged finite pruned result. The only width premises concern original pointers, depths, epochs and input magnitudes; all intermediate fits are derived. Every child is generated and executed by the same fixed native controller.