Native routing and stable grouping of wanted positions

The initialized input contains only L,m,N,Q and Q ordinary row/column pairs. The code computes the valid-mask tables, band parameters, tile counts, prefix offsets and scatter positions. Each scatter writes the unchanged pruned-query code and its original position. No sorted request list, layout certificate or dispatch decision is supplied as input.

Main definitions

• Wanted.routeCode: compute one tile and one query code using the computed table.
• Wanted.program: computed tables followed by counting, prefix and stable scatter passes.

These programs use only the existing standard unsigned instructions. Correctness, width, frame and resource theorems are separate from the definitions. Supporting exec_* lemmas are internal implementation APIs exported across proof modules; consumers use runs, runs_grouped or the generic-memory exec_program when composing a caller.

References

The routing goal comes from [AlmanWilliams2026, Section 2.4.4] and Anthropic's pinned Wanted/Codes.lean at revision 16a5ce41304fcdaea4e0be7c132e1c361dc26da5. This is original native code with its own charged proofs, using the existing finite output-string definitions. It does not import the source Light machine, its sorting procedure or its instruction counts.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.packRegisters (i : Fin 16) : Fin 96

Register embedding for the unchanged sixteen-register digit packer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.queryRow : Fin 96

Original row of the current query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.queryCol : Fin 96

Original column of the current query.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.rowBand : Fin 96

Computed row band.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.colBand : Fin 96

Computed column band.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.tile : Fin 96

Row-major tile key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.queries : Fin 96

Address of the first original row/column pair.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.queryCount : Fin 96

Number of original query positions, including duplicates.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.index : Fin 96

Current original query position or tile position.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.counts : Fin 96

Tile-count array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.offsets : Fin 96

Prefix-offset array base, with one additional terminal cell.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.cursors : Fin 96

Current stable-scatter cursor array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.codes : Fin 96

Grouped query-code array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.originals : Fin 96

Grouped original-position array base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.count : Fin 96

Current tile's query count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.total : Fin 96

Running prefix sum.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.tileCount : Fin 96

Number of tiles.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.bandWidth : Fin 96

Number of original positions in one band.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.inputEnd : Fin 96

One past the readonly initialized query input.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.memoryEnd : Fin 96

One past the grouping arrays.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.pointer : Fin 96

Address scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.cursorAddress : Fin 96

Saved address of the current scatter cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.position : Fin 96

Current grouped output position.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.tileCode : WordRAM.Code WordRAM.Basis.standard 96

Compute just the row-major tile key. No memory is touched.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.routeHead : WordRAM.Code WordRAM.Basis.standard 96

Compute the selected subset rank and load its actual mask from the computed table.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.routeCode : WordRAM.Code WordRAM.Basis.standard 96

Compute a tile key and its output code, with actual digit decisions and table load.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.setup : WordRAM.Code WordRAM.Basis.standard 96

Relocate the computed tables and every grouping array after the initialized input.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.clearCounts : WordRAM.Code WordRAM.Basis.standard 96

Zero each tile count once.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.loadQuery : WordRAM.Code WordRAM.Basis.standard 96

Load one original pair without changing its input words.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.countStep : WordRAM.Code WordRAM.Basis.standard 96

Count one input position in its actual tile, retaining duplicates.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.countQueries : WordRAM.Code WordRAM.Basis.standard 96

Scan the original list once to obtain tile counts.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.prefixStep : WordRAM.Code WordRAM.Basis.standard 96

Store both the immutable prefix offset and the initial scatter cursor of one tile.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.prefixCode : WordRAM.Code WordRAM.Basis.standard 96

Compute exact tile spans, including the terminal offset after the last tile.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.scatterWrite : WordRAM.Code WordRAM.Basis.standard 96

Append one code and original position to its tile, advancing the actual cursor.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.scatterStep : WordRAM.Code WordRAM.Basis.standard 96

Recompute one query's code and scatter it stably into its counted tile.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.scatter : WordRAM.Code WordRAM.Basis.standard 96

The second original-order scan retains every occurrence and its original position.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.program : WordRAM.Code WordRAM.Basis.standard 96

Complete initialized native routing; no mathematical layout is an input word.