Native routing of one wanted position

Main results

• Wanted.exec_route: actual divisions, selected-mask lookup and digit packing return exactly the tile and outStrOfPos code for an original matrix position.

The table contract is an ordinary memory equation supplied by the actual computed-table routine. It supplies neither an output string nor an execution or time certificate.

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

Scalar values read by the one-query router. The table may be relocated by its caller.

• levels : x.regs BandPreparation.levels = L

  Original depth.

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

  Compressed outer dimension.

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

  Computed root of the valid-subset count.

• bandWidth : x.regs Wanted.bandWidth = MatrixMultiplication.Schonhage.bandSize L m

  Computed band width.

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

  Computed band count.

• table : x.regs BandPreparation.table = tab

  Actual forward-table base.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.routeBudget (L m N tab : ℕ) : ℕ

Numeric bound for all arithmetic performed by one router and its digit kernel.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.RouteLocal (i : Fin 96) : Prop

Only the packer bank and three computed routing registers are written.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.instDecidableRouteLocal (i : Fin 96) : Decidable (RouteLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.packRegisters_injective : Function.Injective packRegisters

The register map embeds the packer without identifying any pair of registers.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_route {w L m N tab : ℕ} (hm : m ≤ L) (I J : Fin N) (x : WordRAM.Data 96) (hx : RouteParameters L m N tab x) (hI : x.regs queryRow = ↑I) (hJ : x.regs queryCol = ↑J) (htable : ∀ (gh : Fin (MatrixMultiplication.Schonhage.K0 L m) × Fin (MatrixMultiplication.Schonhage.K0 L m)), x.mem (tab + ↑(MatrixMultiplication.Schonhage.MaskTable.pairRank gh)) = ↑(MatrixMultiplication.Schonhage.MaskTable.selectedMask gh)) (hfit : WordRAM.Fits w (routeBudget L m N tab)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w routeCode x y (15 * L + 25) ∧ y.regs rowBand = MatrixMultiplication.Schonhage.bandOf L m ↑I ∧ y.regs colBand = MatrixMultiplication.Schonhage.bandOf L m ↑J ∧ y.regs tile = MatrixMultiplication.Schonhage.bandOf L m ↑I * MatrixMultiplication.Schonhage.numBands L m N + MatrixMultiplication.Schonhage.bandOf L m ↑J ∧ y.regs (packRegisters code) = ↑(PrunedQuery.queryIndex (MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm) ↑I ↑J)) ∧ y.mem = x.mem ∧ ∀ (i : Fin 96), ¬RouteLocal i → y.regs i = x.regs i

Actual routing on one admitted original position. Original row/column words, all persistent parameters and all memory survive; only the declared local registers change.