Charged copies into the shared band catalogue #
Main results #
BandPreparation.catalogue_block_le: each band has one disjoint catalogue block.BandPreparation.exec_collectBand: the real native encoder-output copy, including every address calculation and the unchanged copy kernel's instruction count.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.catalogue_block_le {L m N β : ℕ} (side : Bool) (hβ : β < MatrixMultiplication.Schonhage.numBands L m N) :
Every complete band block lies in the catalogue allocation.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.catalogue_le_address (L m N β : ℕ) (side : Bool) :
No band output is placed in the protected snapshot, tables or native workspace.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_collectBand {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 = β) (hfit : WordRAM.Fits w (wordBudget L m N)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w (collectBand side) x y (7 * 10 ^ L + 10) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (Encoding.outputBase L) (catalogueAddress L m N side β 0) (10 ^ L) ∧ BandParameters L m N y ∧ y.regs band = β
Address arithmetic and the full copy are charged. The copy's source and destination are disjoint by the concrete allocation; arbitrary words outside its destination are retained.