Memory and register invariants for actual controller nodes

Main definitions

• PrunedQuery.KernelRegs: the unchanged native parameters and computed workspace pointers.
• PrunedQuery.nodeWrites: the descendant rows that one node may change.

Main results

• PrunedQuery.exec_node_zero: the terminal node case, with the existing mathematical result, concrete frame and timestamp preservation, and charged native continuation.

The invariants describe ordinary register and memory values. They contain no execution, solver, time-bound or all-state-fit field. Execution is proved separately in native semantics.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.KernelRegs (L f a b : ℕ) (x : WordRAM.Data registers) : Prop

Fixed caller parameters and the explicit workspace partition computed by locate. This is a register-value assertion, with no assumed execution or resource guarantee.

• depth_eq : x.regs inputDepth = L

  Original recursion depth.

• span_eq : x.regs span = 10 ^ L

  Actual source-array and row capacity.

• left_eq : x.regs arrayA = a

  Left input-array pointer.

• right_eq : x.regs arrayB = b

  Right input-array pointer.

• frames_eq : x.regs frames = f

  First stored frame.

• lists_eq : x.regs lists = f + 4 * (L + 1)

  First query row, after the four-word frames.

• values_eq : x.regs values = f + 4 * (L + 1) + (L + 1) * 10 ^ L

  First value row, after all query rows.

• stamps_eq : x.regs stamps = f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L

  Shared timestamp directory, after all value rows.

• nil_eq : x.regs nil = 0

  Constant zero.

• one_eq : x.regs one = 1

  Constant one.

• ten_eq : x.regs ten = 10

  Constant ten.

• nine_eq : x.regs nine = 9

  Constant inner-output digit.

• frameWidth_eq : x.regs frameWidth = 4

  Four ordinary words per frame.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nodeWrites (L f d : ℕ) : Finset ℕ

The exact permitted workspace rows for a node at depth d. Its own query row is read-only; descendant query rows, current/descendant value rows, frame suffix and timestamps may change.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.KernelRegs.of_step {w T L f a b : ℕ} {x y : WordRAM.Data registers} (h : KernelRegs L f a b x) (he : WordRAM.ExecWithin w step x y T) : KernelRegs L f a b y

Every branch of the actual controller preserves the fixed caller parameters.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_node_zero {w L f a0 b0 p E : ℕ} {a b : ℤ} (ha : GenericRAM.Signed.Fits w a) (hb : GenericRAM.Signed.Fits w b) (hab : GenericRAM.Signed.Fits w (a * b)) (S : Finset (MatrixMultiplication.Schonhage.OutStr 0)) (x : WordRAM.Data registers) (hregs : KernelRegs L f a0 b0 x) (hd : x.regs level = L) (hm : x.regs mode = 0) (hactive : x.regs active = 1) (hcount : x.mem (f + 4 * L) = S.card) (hpref : x.mem (f + 4 * L + 1) = p) (hleft : x.mem (a0 + p) = WordRAM.Signed.encode a) (hright : x.mem (b0 + p) = WordRAM.Signed.encode b) (hE : x.regs epoch = E) (hmarks : ∀ q < 10 ^ L, x.mem (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + q) ≤ E) (hw : WordRAM.Fits (w + 2) (f + 4 * (L + 1) + (f + 4 * (L + 1)) + (f + 4 * (L + 1) + (L + 1) * 10 ^ L) + (L + 1) * 10 ^ L + L + a0 + p + b0 + p + 12)) : ∃ (y : WordRAM.Data registers), KernelRegs L f a0 b0 y ∧ (y.regs level = if L = 0 then 0 else L - 1) ∧ (y.regs mode = if L = 0 then 0 else 2) ∧ (y.regs active = if L = 0 then 0 else 1) ∧ y.regs epoch = E ∧ (∀ q < 10 ^ L, y.mem (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + q) ≤ E) ∧ (∀ q ∈ S, y.mem (f + 4 * (L + 1) + (L + 1) * 10 ^ L + L * 10 ^ L + ↑(queryIndex q)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.Pruned.result 0 (fun (x : MatrixMultiplication.Schonhage.Leaf 0) => a) (fun (x : MatrixMultiplication.Schonhage.Leaf 0) => b) S q)) ∧ WordRAM.Modifies (nodeWrites L f L) x.mem y.mem ∧ (∀ (i : Fin registers), ¬LeafStepLocal i → y.regs i = x.regs i) ∧ ∀ (z : WordRAM.Data registers) (U : ℕ), WordRAM.ExecWithin (w + 2) controller y z U → WordRAM.ExecWithin (w + 2) controller x z (traceWeight S + U)

The terminal induction case is a proved actual controller iteration. The requested values are the existing Pruned.result; an empty set leaves the value row untouched. The memory frame and timestamp bound hold at the same final state as the charged continuation.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_node_enter {w L f a0 b0 d N : ℕ} (x : WordRAM.Data registers) (hregs : KernelRegs L f a0 b0 x) (hd : x.regs level = d) (hdL : d < L) (hm : x.regs mode = 0) (hN : x.mem (f + 4 * d) = N) (hcap : N ≤ 10 ^ L) (input : ℕ → ℕ) (hinput : ∀ i < N, x.mem (f + 4 * (L + 1) + d * 10 ^ L + i) = input i) (hcodes : ∀ i < N, input i < 10 ^ L) (hw : WordRAM.Fits w (8 * f + 64 * (L + 1) * 10 ^ L + 128)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w step x y (7 * N + 28) ∧ KernelRegs L f a0 b0 y ∧ y.regs level = d ∧ y.regs mode = 1 ∧ y.regs epoch = x.regs epoch ∧ y.regs active = x.regs active ∧ y.mem = Function.update (zeroQueryPrefix x.mem (f + 4 * (L + 1) + (L + 1) * 10 ^ L + d * 10 ^ L) input N) (f + 4 * d + 3) 0 ∧ (∀ i < N, y.mem (f + 4 * (L + 1) + d * 10 ^ L + i) = input i) ∧ WordRAM.Modifies (nodeWrites L f d) x.mem y.mem

Enter an internal node by clearing only its listed accumulators and storing the actual zero term counter. This is a complete controller step, including frame loads and comparisons. Its displayed address budget contains only ordinary workspace parameters and list length.