Complete native padded-band preparation #
Main results #
BandPreparation.exec_prepareBand: initialize and fill every band-array cell by actual native digit decoding, inverse-table lookup and guarded signed matrix loads.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.band_input_le_snapshot (L m N : ℕ) :
Every prepared-band cell is below the protected original input.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_prepareBand {w L m N : ℕ} (side : Bool) (β : ℕ) (x : WordRAM.Data 96) (hx : BandParameters L m N x) (hβ : β < MatrixMultiplication.Schonhage.numBands L m N) (hb : x.regs band = β) (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)) (hfit : WordRAM.Fits w (wordBudget L m N)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w (prepareBand side) x y ((13 * L + 39) * 7 ^ L + 5) ∧ BandParameters L m N y ∧ y.regs band = β ∧ y.mem 1 = L ∧ (∀ a < 7 ^ L, y.mem (2 + a) = WordRAM.Signed.encode (bandValue L m N β side matrix a)) ∧ ∀ (b : ℕ), ¬(1 ≤ b ∧ b < 2 + 7 ^ L) → y.mem b = x.mem b
The entire input band is materialized with charged initialization, digit/index work, padding and loop control. No cell outside the depth header and the band input is changed.