Actual initialized header and signed-matrix inputs

Main definitions

• BandPreparation.matrixValues: zero extension of the two original finite matrices for stating the already proved native guarded-load specification.

Main results

• BandPreparation.input_fits: the actual initialized list fits from original magnitude and parameter bounds.
• BandPreparation.exec_input: complete charged native execution from State.init.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.matrixValues {m N : ℕ} (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (side : Bool) (r k : ℕ) : ℤ

Original matrix entries, zero extended to natural indices. Right-side r denotes a column of Y. This is only the mathematical memory specification; the program loads the concrete row-major input words, after its actual bounds guard.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.input_length {m N : ℕ} (L : ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) : (input L m N X Y).length + 1 = inputEnd m N

The input prefix consists of the native length header, three scalar words and both original matrices, with no powers, tables or precomputed outputs.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.input_fits {w L m N : ℕ} (hw : 0 < w) (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (A : ℤ) (hA : 0 ≤ A) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), |X i k| ≤ A) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), |Y k j| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N)) : WordRAM.InputFits (w + 2) (input L m N X Y)

The sign/magnitude input encoding uses at most w+1 bits; the actual native program uses w+2 bits for its signed arithmetic kernels. Every input word is covered.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_input {w L m N : ℕ} (hw : 0 < w) (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (A : ℤ) (hA : 0 ≤ A) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), |X i k| ≤ A) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), |Y k j| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N)) : WordRAM.InputFits (w + 2) (input L m N X Y) ∧ ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin (w + 2) program (WordRAM.State.init (input L m N X Y)).data y (timeBound L m N) ∧ WordRAM.Data.Bounded (w + 2) y ∧ BandParameters L m N y ∧ (∀ (side : Bool), ∀ β < MatrixMultiplication.Schonhage.numBands L m N, ∀ p < 10 ^ L, y.mem (catalogueAddress L m N side β p) = WordRAM.Signed.encode (catalogueValue L m N side (matrixValues X Y side) β p)) ∧ (∀ a < 2 ^ L, y.mem (inverseBase L m N + a) = MatrixMultiplication.Schonhage.MaskTable.lookup L m a) ∧ (∀ (gh : Fin (MatrixMultiplication.Schonhage.K0 L m) × Fin (MatrixMultiplication.Schonhage.K0 L m)), y.mem (tableBase L m N + ↑(MatrixMultiplication.Schonhage.MaskTable.pairRank gh)) = ↑(MatrixMultiplication.Schonhage.MaskTable.selectedMask gh)) ∧ ∀ (b : ℕ), ¬(inputEnd m N ≤ b ∧ b < memoryEnd L m N) → y.mem b = (WordRAM.State.init (input L m N X Y)).data.mem b

Complete actual State.init execution, with both encoded catalogues, computed tables, preserved input and outside frame, bounded final state and the complete charged time bound.