Complete actual native queried matrix products #
Main results #
QueriedProduct.exec: original matrix/coordinate words suffice for actual finite native execution, exact original-order product values, original-input restoration and outside frame.
The program computes all tables, groups, catalogues, tile arguments, epochs and reporting
decisions. The original-word predicate permits arbitrary header zero and arbitrary outside
memory; initialized clients discharge it directly from the literal input list.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec {w L m N A : ℕ} (hw : 0 < w) (hm : m ≤ L) (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) (hinput :
∀ (a : ℕ), 0 < a → a < inputEnd m N qs.length → x.mem a = (WordRAM.State.init (input bits L X Y qs)).data.mem 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) (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) (program bits) x y (timeBound hm qs) ∧ Parameters L m N qs.length y ∧ (∀ (i : Fin qs.length),
y.mem (outputBase L m N qs.length + ↑i) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ ∀ (a : ℕ), ¬(inputEnd m N qs.length ≤ a ∧ a < memoryEnd L m N qs.length) → y.mem a = x.mem a
Actual composed execution from only ordinary original words, with every phase charged. No table/layout/query/producer/run/time certificate or fast-solver assumption is an input.