Charged materialization of the subset tables

Main definitions

• BandPreparation.tableStep: the exact memory writes made by one table iteration.

Main results

• BandPreparation.exec_tableWrite: actual inverse/forward table stores and counter updates.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.tableStep (L m inv tab t : ℕ) (μ : ℕ → ℕ) : ℕ → ℕ

The inverse word is initialized even for an unselected mask. Selected masks also write one forward-table cell. This is only a mathematical description of the two native stores.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.TablesPrefix (L m inv tab t : ℕ) (initial current : ℕ → ℕ) : Prop

The part of both tables computed after visiting t masks. The outside frame permits arbitrary caller memory, including future query inputs and scratch regions.

• inverse (a : ℕ) : a < t → current (inv + a) = MatrixMultiplication.Schonhage.MaskTable.lookup L m a

  Every visited inverse word has been initialized.

• forward (a : ℕ) : a < t → MatrixMultiplication.Schonhage.MaskTable.lookup L m a ≠ 0 → current (tab + MatrixMultiplication.Schonhage.MaskTable.prefixCount L m a) = a

  Every selected visited mask has been placed at its prefix rank.

• frame (a : ℕ) : ¬(inv ≤ a ∧ a < inv + 2 ^ L) → ¬(tab ≤ a ∧ a < tab + 2 ^ L) → current a = initial a

  Only the two explicitly reserved table blocks may change.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.TablesPrefix.zero (L m inv tab : ℕ) (μ : ℕ → ℕ) : TablesPrefix L m inv tab 0 μ μ

Empty scan prefix, with no initialized-memory assumption.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.TablesPrefix.step {L m inv tab t : ℕ} {μ μ' : ℕ → ℕ} (h : TablesPrefix L m inv tab t μ μ') (ht : t < 2 ^ L) (hsep : inv + 2 ^ L ≤ tab) : TablesPrefix L m inv tab (t + 1) μ (tableStep L m inv tab t μ')

The actual two stores extend the initialized table prefix by one mask.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_tableWrite {w : ℕ} (L m inv tab t : ℕ) (x : WordRAM.Data 96) (ht : t < 2 ^ L) (hinv : x.regs inverse = inv) (htab : x.regs table = tab) (hmask : x.regs mask = t) (hrank : x.regs rank = MatrixMultiplication.Schonhage.MaskTable.prefixCount L m t) (hpop : x.regs population = MatrixMultiplication.Schonhage.MaskTable.population L t) (hm : x.regs inner = m) (hsq : x.regs square = MatrixMultiplication.Schonhage.K0 L m * MatrixMultiplication.Schonhage.K0 L m) (h0 : x.regs zero = 0) (h1 : x.regs one = 1) (hfit : WordRAM.Fits w (inv + tab + 2 ^ L + 4)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w tableWrite x y 10 ∧ y.mem = tableStep L m inv tab t x.mem ∧ y.regs mask = t + 1 ∧ y.regs rank = MatrixMultiplication.Schonhage.MaskTable.prefixCount L m (t + 1) ∧ ∀ (i : Fin 96), i ≠ address → i ≠ temporary → i ≠ mask → i ≠ rank → y.regs i = x.regs i

Execute the stores after the population loop. The code neither searches a supplied table nor receives a table-validity certificate.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.TableParameters (L m inv tab : ℕ) (x : WordRAM.Data 96) : Prop

Persistent scalar parameters read by the table loops. These are register contents only; there is no execution, fit or cost assumption in this postcondition.

• levels : x.regs BandPreparation.levels = L

  Original depth.

• inner : x.regs BandPreparation.inner = m

  Original inner cardinality.

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

  Computed complete binary-mask range.

• inverse : x.regs BandPreparation.inverse = inv

  Inverse-table base.

• table : x.regs BandPreparation.table = tab

  Forward-table base.

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

  Computed number of selected masks.

• zero : x.regs BandPreparation.zero = 0

  Constant zero.

• one : x.regs BandPreparation.one = 1

  Constant one.

• two : x.regs BandPreparation.two = 2

  Constant two.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_tables {w : ℕ} (L m inv tab : ℕ) (x : WordRAM.Data 96) (hx : TableParameters L m inv tab x) (hsep : inv + 2 ^ L ≤ tab) (hfit : WordRAM.Fits w (inv + tab + 2 ^ L + L + 4)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w tablesCode x y ((6 * L + 17) * 2 ^ L + 4) ∧ TableParameters L m inv tab y ∧ (∀ a < 2 ^ L, y.mem (inv + a) = MatrixMultiplication.Schonhage.MaskTable.lookup L m a) ∧ (∀ (gh : Fin (MatrixMultiplication.Schonhage.K0 L m) × Fin (MatrixMultiplication.Schonhage.K0 L m)), y.mem (tab + ↑(MatrixMultiplication.Schonhage.MaskTable.pairRank gh)) = ↑(MatrixMultiplication.Schonhage.MaskTable.selectedMask gh)) ∧ ∀ (a : ℕ), ¬(inv ≤ a ∧ a < inv + 2 ^ L) → ¬(tab ≤ a ∧ a < tab + 2 ^ L) → y.mem a = x.mem a

The complete native scan computes both tables, with all inner population scans and outer controls charged. Outside memory may contain arbitrary caller data.