Running the actual shared catalogue producer in the product caller #
Main results #
QueriedProduct.exec_bands: invoke the complete actual band/encoding program in the low bank, yielding the unchanged mathematicalencodingL/Rarrays and preserving the caller's scalars.
The input memory equations are discharged by the preceding charged matrix adaptation. No encoded catalogue, subset layout or producer execution is supplied to the program.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_bands {w L m N Q A : ℕ} (hw : 0 < w) (hm : m ≤ L) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N) (hmat :
∀ (side : Bool),
∀ r < N,
∀ k < MatrixMultiplication.Schonhage.D m,
x.mem (BandPreparation.matrixOffset m N side r k + 4) = WordRAM.Signed.encode (BandPreparation.matrixValues X Y side r k)) (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 : magnitudeBound L A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin (w + 2) (WordRAM.Code.rename bank BandPreparation.program) x y (BandPreparation.timeBound L m N) ∧ Parameters L m N Q y ∧ (∀ β < MatrixMultiplication.Schonhage.numBands L m N,
∀ (τ : MatrixMultiplication.Schonhage.Leaf L),
y.mem (BandPreparation.catalogueAddress L m N false β ↑(Encoding.leafIndex τ)) = WordRAM.Signed.encode
(MatrixMultiplication.Schonhage.encodingL
(MatrixMultiplication.Schonhage.bandArrayL (MatrixMultiplication.Schonhage.MaskTable.layout hm) X β)
τ)) ∧ (∀ β < MatrixMultiplication.Schonhage.numBands L m N,
∀ (τ : MatrixMultiplication.Schonhage.Leaf L),
y.mem (BandPreparation.catalogueAddress L m N true β ↑(Encoding.leafIndex τ)) = WordRAM.Signed.encode
(MatrixMultiplication.Schonhage.encodingR
(MatrixMultiplication.Schonhage.bandArrayR (MatrixMultiplication.Schonhage.MaskTable.layout hm) Y β)
τ)) ∧ ∀ (a : ℕ), a < BandPreparation.inputEnd m N ∨ BandPreparation.memoryEnd L m N ≤ a → y.mem a = x.mem a
The actual native producer computes every shared band encoding, once per band. Its complete outside frame protects the caller's original input and saved routing arrays.