Actual native encoder calls on the prepared bands

Main definitions

• BandPreparation.catalogueValue: flat shared-transform values, using the existing coordinate transform and the computed, padded band array.

Main results

• BandPreparation.exec_band: one complete native preparation, unchanged encoder call and catalogue copy, with charged instructions and an explicit memory frame.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.catalogueValue (L m N : ℕ) (side : Bool) (matrix : ℕ → ℕ → ℤ) (β p : ℕ) : ℤ

The shared catalogue uses exactly the existing flat coordinate-transform values. Encoding.value_final_left/right and bandValue_left/right identify these with the public encodingL/R of the original mathematical bandArrayL/R.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.abs_bandValue_le {L m N β : ℕ} (side : Bool) (matrix : ℕ → ℕ → ℤ) (A : ℤ) (hA : 0 ≤ A) (hmat : ∀ r < N, ∀ k < MatrixMultiplication.Schonhage.D m, |matrix r k| ≤ A) (a : Fin (7 ^ L)) : |bandValue L m N β side matrix ↑a| ≤ A

The guarded band only reads real bounded matrix entries; all other entries are zero.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_encoderKernel {w L m N : ℕ} (hw : 0 < w) (side : Bool) (arr : ℕ → ℤ) (x : WordRAM.Data 96) (hheader : x.mem 1 = L) (hinput : ∀ i < 7 ^ L, x.mem (2 + i) = WordRAM.Signed.encode (arr i)) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ i < 7 ^ L, |arr i| ≤ 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) (WordRAM.Code.rename encoderRegisters (Encoding.program side)) x y (Encoding.timeBound L) ∧ (∀ p < 10 ^ L, y.mem (Encoding.outputBase L + p) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (Encoding.coefficients side)) L 0 arr p 0)) ∧ (∀ (b : ℕ), ¬(Encoding.outputBase L ≤ b ∧ b < Encoding.scratchBase L + 10 ^ L) → y.mem b = x.mem b) ∧ ∀ (i : Fin 96), 32 ≤ ↑i → y.regs i = x.regs i

A real call of the unchanged encoder in its low 32-register bank. Parameters in the other registers, arbitrary input headers and arbitrary outside memory are preserved.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.bandTime (L : ℕ) : ℕ

Native cost of preparing, encoding and collecting one shared band.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_band {w L m N : ℕ} (hw : 0 < w) (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)) (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) ((prepareBand side).seq ((WordRAM.Code.rename encoderRegisters (Encoding.program side)).seq (collectBand side))) x y (bandTime L) ∧ BandParameters L m N y ∧ y.regs band = β ∧ (∀ 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 ≤ b ∧ b < catalogueAddress L m N side β 0 + 10 ^ L) → y.mem b = x.mem b

Every band invokes the actual encoder code and copies its complete output. Only the low workspace and this single shared catalogue block can change. Original matrix/table data and arbitrary caller query regions outside those blocks remain untouched.