Original matrices through the actual native input adapter #
Main results #
QueriedProduct.exec_prepareInputMatrices: real signed copies or raw-entry doubling establish the exact input words required by the existing band producer.
The source-word equalities come from the preceding native original-input snapshot. The raw path represents nonnegative entries, including the ET frontend's raw zero/one matrices.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_prepareInputMatrices {w L m N A : ℕ} (hw : 0 < w) (bits : Bool) (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 160) (hp : Parameters L m N qs.length x) (hsource :
∀ j < 2 * (N * MatrixMultiplication.Schonhage.D m),
x.mem (snapshotBase L m N qs.length + 5 + j) = (WordRAM.State.init (input bits L X Y qs)).data.mem (5 + j)) (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) (hbits :
bits = true →
(∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ X i k) ∧ ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), 0 ≤ Y k j) (hmag : magnitudeBound L A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N qs.length)) :
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin (w + 2) (prepareMatrices bits) x y (8 * (2 * (N * MatrixMultiplication.Schonhage.D m)) + 10) ∧ Parameters L m N qs.length y ∧ (∀ (side : Bool),
∀ r < N,
∀ k < MatrixMultiplication.Schonhage.D m,
y.mem (BandPreparation.matrixOffset m N side r k + 4) = WordRAM.Signed.encode (BandPreparation.matrixValues X Y side r k)) ∧ ∀ (a : ℕ), a < 4 ∨ 4 + 2 * (N * MatrixMultiplication.Schonhage.D m) ≤ a → y.mem a = x.mem a
Every original matrix entry reaches the producer in its canonical signed convention. The instruction envelope includes the actual conversion at every raw input entry.