Every shared band, computed once #
Main results #
BandPreparation.exec_encodeBands: the complete native loop prepares, encodes and collects all bands of one matrix side. Catalogue cells retain the existing flat leaf numbering.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.catalogue_block_inside {L m N β : ℕ} (side : Bool) (hβ : β < MatrixMultiplication.Schonhage.numBands L m N) :
catalogueAddress L m N side 0 0 ≤ catalogueAddress L m N side β 0 ∧ catalogueAddress L m N side β 0 + 10 ^ L ≤ catalogueAddress L m N side (MatrixMultiplication.Schonhage.numBands L m N) 0
The full one-side catalogue interval ends at the block immediately after its last band.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.bands_fits {w L m N : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N)) :
All ordinary band counters fit from the original explicit allocation budget.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_encodeBands {w L m N : ℕ} (hw : 0 < w) (side : Bool) (x : WordRAM.Data 96) (hx : BandParameters L m N x) (htable : ∀ t < 2 ^ L, x.mem (inverseBase L m N + t) = MatrixMultiplication.Schonhage.MaskTable.lookup L m t) (matrix : ℕ → ℕ → ℤ) (hmat :
∀ r < N,
∀ k < MatrixMultiplication.Schonhage.D m, x.mem (matrixAddress L m N side r k) = WordRAM.Signed.encode (matrix r k)) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ r < N, ∀ k < MatrixMultiplication.Schonhage.D m, |matrix r k| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (wordBudget L m N)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin (w + 2) (encodeBands side) x y
(MatrixMultiplication.Schonhage.numBands L m N * (bandTime L + 3) + 3) ∧ BandParameters L m N y ∧ (∀ β < 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 matrix β p)) ∧ ∀ (b : ℕ),
¬(1 ≤ b ∧ b < Encoding.scratchBase L + 10 ^ L) →
¬(catalogueAddress L m N side 0 0 ≤ b ∧ b < catalogueAddress L m N side (MatrixMultiplication.Schonhage.numBands L m N) 0) →
y.mem b = x.mem b
The actual native loop calls the complete encoder once for every shared band, charges all loop control and counter increments, and preserves any outside caller memory.