Complete computed scalar parameters for native bands

Main results

• BandPreparation.exec_countCode: compute binomial count, block count and band count from actual scalar parameters, retaining the previously computed header layout.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.headerRegisters : Finset (Fin 96)

Registers containing the persistent header and concrete layout.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.headerPost_reframe {L m N : ℕ} {x y : WordRAM.Data 96} (hx : HeaderPost L m N x) (h : ∀ i ∈ headerRegisters, y.regs i = x.regs i) : HeaderPost L m N y

The concrete layout survives any native execution that preserves its scalar registers.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.BandParameters (L m N : ℕ) (x : WordRAM.Data 96) extends Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.HeaderPost L m N x : Prop

Persistent concrete layout and the additional scalar results actually computed by the mask-count/root/band-count code. No fit or execution bound is bundled here.

• fixed : BasicParameters L m N x
• columns : x.regs BandPreparation.columns = MatrixMultiplication.Schonhage.D m
• outerSize : x.regs BandPreparation.outerSize = MatrixMultiplication.Schonhage.N0 L m
• masks : x.regs BandPreparation.masks = 2 ^ L
• cells : x.regs BandPreparation.cells = 7 ^ L
• leaves : x.regs BandPreparation.leaves = 10 ^ L
• prefixSize : x.regs BandPreparation.prefixSize = inputEnd m N
• snapshot : x.regs BandPreparation.snapshot = snapshotBase L m N
• inverse : x.regs BandPreparation.inverse = inverseBase L m N
• table : x.regs BandPreparation.table = tableBase L m N
• catalogue : x.regs BandPreparation.catalogue = catalogueBase L m N
• root : x.regs BandPreparation.root = MatrixMultiplication.Schonhage.K0 L m

  Computed floor square root of the binomial count.

• square : x.regs BandPreparation.square = MatrixMultiplication.Schonhage.K0 L m * MatrixMultiplication.Schonhage.K0 L m

  Number of selected subset masks.

• bands : x.regs BandPreparation.bands = MatrixMultiplication.Schonhage.numBands L m N

  Computed number of shared bands per side.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parameterRegisters : Finset (Fin 96)

All scalar parameters retained throughout preparation and encoder calls.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.parameters_reframe {L m N : ℕ} {x y : WordRAM.Data 96} (hx : BandParameters L m N x) (h : ∀ i ∈ parameterRegisters, y.regs i = x.regs i) : BandParameters L m N y

Preserve the computed parameters by preserving their actual registers.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.local_fits {w L m N : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N)) : WordRAM.Fits w (16 * (L + N + N * MatrixMultiplication.Schonhage.D m + 2 ^ L + 10 ^ L + 1))

A convenient local numerical bound, derived from the original global word budget.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_countCode {w L m N : ℕ} (x : WordRAM.Data 96) (hx : HeaderPost L m N x) (hfit : WordRAM.Fits w (wordBudget L m N)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w countCode x y ((6 * L + 16) * 2 ^ L + 14) ∧ BandParameters L m N y ∧ y.mem = x.mem

Compute the root and band counts with the actual native loops.