Concrete memory layout of native wanted-query grouping

Main definitions

• Wanted.tableAddress: computed selected-mask table after the readonly query input.
• Wanted.Parameters: scalar register equalities used by all three grouping passes.
• Wanted.wordBudget: an original-input-derived sufficient bound for unsigned words.

All layout definitions are numeric specifications of actual address instructions. Neither the layout nor the parameter record contains a run, time bound or assumed solver.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.inputLimit (Q : ℕ) : ℕ

The original length word, four headers and two words per wanted position.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.tableAddress (L Q : ℕ) : ℕ

The forward table follows a complete 2^L-word inverse table.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.countAddress (L Q : ℕ) : ℕ

Tile counts follow both computed tables.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.offsetAddress (L m N Q : ℕ) : ℕ

One immutable prefix offset per tile, followed by one terminal offset.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.cursorAddressBase (L m N Q : ℕ) : ℕ

Mutable stable-scatter cursors follow the immutable prefix offsets.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.codeAddress (L m N Q : ℕ) : ℕ

One actual query code per original occurrence.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.originalAddress (L m N Q : ℕ) : ℕ

Every code retains its original input position in the adjacent array.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.memoryLimit (L m N Q : ℕ) : ℕ

One past both grouped output arrays.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.wordBudget (L m N Q : ℕ) : ℕ

This sufficient budget covers the reused parameter kernels as well as all routing and grouping arithmetic. It depends only on the original four scalar parameters.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.Parameters (L m N Q : ℕ) (x : WordRAM.Data 96) : Prop

Persistent scalar register values after actual table relocation and allocation.

• tables : BandPreparation.TableParameters L m (inputLimit Q) (tableAddress L Q) x

  The reused table kernel's actual scalar contents.

• route : RouteParameters L m N (tableAddress L Q) x

  The one-query router's actual scalar contents.

• queries : x.regs Wanted.queries = 5

  Original query input starts after its four scalar headers.

• queryCount : x.regs Wanted.queryCount = Q

  Number of positions, retaining repetitions.

• counts : x.regs Wanted.counts = countAddress L Q

  Allocated tile counts.

• offsets : x.regs Wanted.offsets = offsetAddress L m N Q

  Immutable prefix offsets.

• cursors : x.regs Wanted.cursors = cursorAddressBase L m N Q

  Mutable cursor addresses.

• codes : x.regs Wanted.codes = codeAddress L m N Q

  Grouped query codes.

• originals : x.regs Wanted.originals = originalAddress L m N Q

  Original-position permutation.

• tileCount : x.regs Wanted.tileCount = MatrixMultiplication.Schonhage.numBands L m N ^ 2

  Actual tile count.

• inputEnd : x.regs Wanted.inputEnd = inputLimit Q

  The entire readonly original prefix.

• memoryEnd : x.regs Wanted.memoryEnd = memoryLimit L m N Q

  One past the allocated arrays.

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

The exact scalar register footprint shared by the grouping passes.

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

Persistent scalar contracts survive preservation of their concrete registers.