Stored partial sums between native child calls

Main definitions

• PrunedQuery.NodeProgress: the actual dispatch cursor, frame, directory and partial values.

Main results

• PrunedQuery.exec_ready_enter: native entry establishes the zero-term invariant.

This is an invariant of the existing finite controller. It contains ordinary register and memory equalities, not assumed executions or resource bounds. The timestamp directory is shared by all nodes, so the parent retains its list but does not retain a stale membership-marker assertion.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeProgress (L f a0 b0 n d p E : ℕ) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (x : WordRAM.Data registers) (k : ℕ) (y : WordRAM.Data registers) : Prop

Progress after k of the ten actual child dispatches. The initial state is kept only to express the concrete spatial frame and preservation of its occupied request list.

• regs : KernelRegs L f a0 b0 y

  The constants and workspace pointers are unchanged.

• level_eq : y.regs level = d

  The cursor is at this internal node.

• mode_eq : y.regs mode = 1

  The next controller step dispatches the stored term.

• active_eq : y.regs active = 1

  A dispatching node is active.

• frame : { base := f + 4 * d, length := 4 }.Realizes y.mem ![S.card, p, 10 ^ d, k]

  The first three frame words survive all child returns.

• requests (i : ℕ) : i < S.card → y.mem (f + 4 * (L + 1) + d * 10 ^ L + i) = x.mem (f + 4 * (L + 1) + d * 10 ^ L + i)

  The parent's requests remain in the actual original row.

• values (q : MatrixMultiplication.Schonhage.OutStr (n + 1)) : q ∈ S → y.mem (f + 4 * (L + 1) + (L + 1) * 10 ^ L + d * 10 ^ L + ↑(queryIndex q)) = WordRAM.Signed.encode (partialValue a b S q k)

  Every requested accumulator holds the completed prefix of terms.

• epoch_le : E ≤ y.regs epoch

  Native scans only increase the generation.

• epoch_upper : y.regs epoch ≤ E + k * (1 + epochAllowance n)

  Each completed term pays for its scan and its possible descendant calls.

• timestamps (q : ℕ) : q < 10 ^ L → y.mem (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + q) ≤ y.regs epoch

  All directory cells admit a further fresh generation.

• footprint : WordRAM.Modifies (nodeWrites L f d) x.mem y.mem

  Only the explicit descendant workspace may have changed.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeProgress.scan_eq {L f a0 b0 n d p E k : ℕ} {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) (hy : NodeProgress L f a0 b0 n d p E S a b x k y) (t : Fin 10) : scanSet true (↑t) (fun (i : ℕ) => y.mem (f + 4 * (L + 1) + d * 10 ^ L + i)) S.card = Finset.image (fun (q : MatrixMultiplication.Schonhage.OutStr n) => ↑(queryIndex q)) (MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits t))

The native scan's quotient image is the existing mathematical child set, even though the shared timestamp directory no longer marks the parent's membership.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeProgress.epoch_child_le {L f a0 b0 n d p E k : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))} {a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ} {x y : WordRAM.Data registers} (hy : NodeProgress L f a0 b0 n d p E S a b x k y) (hk : k < 10) : y.regs epoch + 1 + epochAllowance n ≤ E + epochAllowance (n + 1)

Before a dispatch, the original scalar budget covers the fresh scan and every possible descendant generation for that term.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_ready_enter {w L f a0 b0 n d p E : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (x : WordRAM.Data registers) (hx : NodeReady L f a0 b0 (n + 1) d p E S x) (hfit : WordRAM.Fits w (nodeBudget L f a0 b0 E (n + 1))) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w step x y (7 * S.card + 28) ∧ NodeProgress L f a0 b0 n d p E S a b x 0 y

Entry performs the actual frame loads, clear loop and term store. The same returned state has zero partial sums and the original request list, including when that list is empty.