Complete native per-record product execution

The native preparation is followed by the complete existing callable product. Every returned word answers its original occurrence; the whole producer catalogue remains below the owned window and is preserved. These are internal readback composition rules; the producer client discharges their descriptor and source-span assertions from its actual initialized execution.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.timeBound {m n : ℕ} (qs : List (Fin n × Fin n)) : ℕ

The complete per-record charge includes actual decoding, copying and callee invocation.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.preparation_margin {m n Q : ℕ} (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) : 2 * (n * MatrixMultiplication.Schonhage.D m) + 2 * Q + 20 * m + MatrixMultiplication.Schonhage.D m + n + 256 < MatrixMultiplication.Schonhage.CallableProduct.windowSize n Q

All preparation arithmetic and the original input lie below the already computed virtual window. This follows from the existing actual product admission, rather than an input fit table.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec {W b m n i out rho piece s t q : ℕ} (X : Matrix (Fin n) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin n) ℤ) (qs : List (Fin n × Fin n)) (x : WordRAM.Data 320) (hD : x.mem 1 = MatrixMultiplication.Schonhage.D m) (hn : x.mem 3 = n) (hi : x.regs Reg.ordinal = i) (hout : x.regs 39 = out) (hb : x.regs 42 = b) (hrec : out + i * (6 + 2 * (n * MatrixMultiplication.Schonhage.D m)) + 6 ≤ b) (hrecord : { base := out + i * (6 + 2 * (n * MatrixMultiplication.Schonhage.D m)), length := 6 }.Realizes x.mem ![rho, piece, q, qs.length, s, t]) (hsb : s + n * MatrixMultiplication.Schonhage.D m ≤ b) (htb : t + n * MatrixMultiplication.Schonhage.D m ≤ b) (hqb : q + 2 * qs.length ≤ b) (hleft : ∀ a < n * MatrixMultiplication.Schonhage.D m, x.mem (s + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + a)) (hright : ∀ a < n * MatrixMultiplication.Schonhage.D m, x.mem (t + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + n * MatrixMultiplication.Schonhage.D m + a)) (hqueries : ∀ a < 2 * qs.length, x.mem (q + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem (5 + 2 * (n * MatrixMultiplication.Schonhage.D m) + a)) (hX : ∀ (a : Fin n) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ X a k ∧ X a k ≤ 1) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (a : Fin n), 0 ≤ Y k a ∧ Y k a ≤ 1) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ n) (hfit : WordRAM.Fits W (2 * b + 4 * MatrixMultiplication.Schonhage.CallableProduct.windowSize n qs.length + 1024)) : ∃ (y : WordRAM.Data 320), WordRAM.ExecWithin W program x y (timeBound qs) ∧ y.regs Reg.result = b + MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m n qs.length ∧ (∀ (j : Fin qs.length), y.mem (b + (MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m n qs.length + ↑j)) = WordRAM.Signed.encode ((X * Y) (qs.get j).1 (qs.get j).2)) ∧ (∀ (a : ℕ), a < b ∨ b + MatrixMultiplication.Schonhage.CallableProduct.windowSize n qs.length ≤ a → y.mem a = x.mem a) ∧ ∀ (j : Fin 320), ↑j < 65 → y.regs j = x.regs j

Actual record-to-product execution, with only original input/readback premises and no solver/run/time oracle. The final initialized client derives these premises from the producer.