Actual header loads, native powers and concrete band addresses

Main results

• BandPreparation.exec_powerCode: exact reuse of the five-register native power routine.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_powerCode {w : ℕ} (v b n : Fin 96) (hinj : Function.Injective (powerRegisters v b n)) (B M : ℕ) (hB : 1 ≤ B) (x : WordRAM.Data 96) (hb : x.regs b = B) (hn : x.regs n = M) (hfit : WordRAM.Fits w (B ^ M + M + 2)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w (powerCode v b n) x y (4 * M + 5) ∧ y.regs v = B ^ M ∧ y.regs one = 1 ∧ y.mem = x.mem ∧ ∀ (i : Fin 96), i ≠ v → i ≠ counter → i ≠ one → y.regs i = x.regs i

Renaming the actual power routine has no instruction overhead and changes only its accumulator, counter and constant-one register.

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

Scalar parameters loaded from the three actual input headers and small constants.

• levels : x.regs BandPreparation.levels = L

  Input depth.

• inner : x.regs BandPreparation.inner = m

  Input inner cardinality.

• rows : x.regs BandPreparation.rows = N

  Input matrix dimension.

• zero : x.regs BandPreparation.zero = 0

  Constant zero.

• one : x.regs BandPreparation.one = 1

  Constant one.

• two : x.regs BandPreparation.two = 2

  Constant two.

• three : x.regs BandPreparation.three = 3

  Constant three.

• four : x.regs BandPreparation.four = 4

  Constant four.

• seven : x.regs BandPreparation.seven = 7

  Constant seven.

• ten : x.regs BandPreparation.ten = 10

  Constant ten.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.power_fits {w L m N : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N)) (b n : ℕ) (hb : b ≤ 10) (hn : n ≤ L) : WordRAM.Fits w (b ^ n + n + 2)

The global numerical budget bounds every final header power and its exponent.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_headerPowers {w L m N : ℕ} (hm : m ≤ L) (x : WordRAM.Data 96) (hx : BasicParameters L m N x) (hfit : WordRAM.Fits w (wordBudget L m N)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w headerPowers x y (16 * L + 26) ∧ BasicParameters L m N y ∧ y.regs columns = MatrixMultiplication.Schonhage.D m ∧ y.regs outerSize = MatrixMultiplication.Schonhage.N0 L m ∧ y.regs masks = 2 ^ L ∧ y.regs cells = 7 ^ L ∧ y.regs leaves = 10 ^ L ∧ y.mem = x.mem

All header powers are computed by five actual native loops. Their register embeddings are injective and their complete cost is linear in the original depth.

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

Concrete computed powers and addresses after native header initialization.

• fixed : BasicParameters L m N x

  Original scalar headers and constants.

• columns : x.regs BandPreparation.columns = MatrixMultiplication.Schonhage.D m

  Thin dimension.

• outerSize : x.regs BandPreparation.outerSize = MatrixMultiplication.Schonhage.N0 L m

  Outer block dimension.

• masks : x.regs BandPreparation.masks = 2 ^ L

  Complete mask scan range.

• cells : x.regs BandPreparation.cells = 7 ^ L

  Flat input length of each band array.

• leaves : x.regs BandPreparation.leaves = 10 ^ L

  Flat output length of each band encoding.

• prefixSize : x.regs BandPreparation.prefixSize = inputEnd m N

  Original initialized prefix length.

• snapshot : x.regs BandPreparation.snapshot = snapshotBase L m N

  Protected original-input copy address.

• inverse : x.regs BandPreparation.inverse = inverseBase L m N

  Dense inverse-table address.

• table : x.regs BandPreparation.table = tableBase L m N

  Selected-mask forward-table address.

• catalogue : x.regs BandPreparation.catalogue = catalogueBase L m N

  Shared band-encoding output address.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_header {w L m N : ℕ} (hm : m ≤ L) (x : WordRAM.Data 96) (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N) (hfit : WordRAM.Fits w (wordBudget L m N)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w header x y (16 * L + 49) ∧ HeaderPost L m N y ∧ y.mem = x.mem

Header parameters are loaded from real memory, all five powers are computed natively, and every concrete address calculation is charged. Header zero and all unrelated cells may contain arbitrary words; initialization reads only addresses one through three.