Child entry established by the native dispatch #
Main results #
PrunedQuery.exec_progress_child: an actual nonempty scan and push establishes the next induction assertion, with its computed set and prefix.
The finite nonemptiness test is a proof case split. The machine uses the count it computes by scanning the parent's actual list; that count, its contents and the fresh directory are proved at the same returned state as the execution.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeProgress.child_source {L f a0 b0 n d p E base : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))} {a b c : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ} {x y u : WordRAM.Data registers} (hx : NodeReady L f a0 b0 (n + 1) d p E S x) (k : Fin 10) (hy : NodeProgress L f a0 b0 n d p E S a b x (↑k) y) (hpush : WordRAM.Modifies (childWrites L f d) y.mem u.mem) (hbase : base + 10 ^ L ≤ f) (hc :
∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)),
x.mem (base + p + 10 ^ d * ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (c v)) (v : MatrixMultiplication.Schonhage.Leaf n) :
u.mem (base + (p + ↑k * 10 ^ d) + 10 ^ (d + 1) * ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.sliceAt c (Encoding.termDigits k) v)
A pushed child's strided input cells are the existing sliceAt, rather than a supplied
child array. Both preceding native phases preserve the original source block below f.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_progress_child {w L f a0 b0 n d p E : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (x y : WordRAM.Data registers) (hx : NodeReady L f a0 b0 (n + 1) d p E S x) (k : Fin 10) (hy : NodeProgress L f a0 b0 n d p E S a b x (↑k) y) (hne : (MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits k)).Nonempty) (hfit : WordRAM.Fits w (nodeBudget L f a0 b0 E (n + 1))) :
∃ (z : WordRAM.Data registers),
WordRAM.ExecWithin w step y z (20 * S.card + 42) ∧ NodeReady L f a0 b0 n (d + 1) (p + ↑k * 10 ^ d) (y.regs epoch + 1)
(MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits k)) z ∧ WordRAM.Modifies (childWrites L f d) y.mem z.mem ∧ WordRAM.Fits w (nodeBudget L f a0 b0 (y.regs epoch + 1) n)
The computed child state satisfies the concrete node-entry assertion and has a budget derived from the original parent parameters. No child execution is assumed here.