Actual producer, tile-kernel and reconstruction code

Main definitions

• QueriedProduct.program: fixed native composition, with signed or raw nonnegative matrices.
• QueriedProduct.tileStep: actual offset loads, catalogue pointers, epoch call and update.
• QueriedProduct.reconstruct: restore the original request order from actual stored indices.

All three existing 96-register callees use the low bank. The caller's 64 additional registers retain its scalar layout and counters. Copying, initial directory clearing, header adaptation, raw-entry doubling, dispatch, reporting and restoration are real instructions. Supporting code definitions are exposed for execution proofs; they are implementation APIs.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.bank (i : Fin 96) : Fin 160

Reuse each existing native program in the same low 96-register bank.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.copyBank (i : Fin 7) : Fin 160

The unchanged copy routine uses the first seven low registers.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.depth : Fin 160

Persistent caller depth.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.inner : Fin 160

Original inner depth, determining the shared dimension 4^m.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.rows : Fin 160

Original outer matrix dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.queryCount : Fin 160

Number of original request occurrences, including duplicates.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.columns : Fin 160

Computed shared dimension 4^m.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.masks : Fin 160

Number of masks visited by the actual subset-table scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.cells : Fin 160

Number of cells in each padded band array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.leaves : Fin 160

Number of leaf entries in each shared encoding.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.bands : Fin 160

Computed number of row bands, also used for column bands.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.tiles : Fin 160

Number of tile calls, the square of the band count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.inputSize : Fin 160

Length of the complete original memory prefix, including word zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.snapshot : Fin 160

Protected snapshot pointer used to restore the original input.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.offsets : Fin 160

Protected copy of the router's immutable prefix offsets.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.codes : Fin 160

Protected copy of the actual grouped query codes.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.originals : Fin 160

Protected permutation from grouped positions to original occurrence indices.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.grouped : Fin 160

Base of the grouped answers written by tile calls.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.output : Fin 160

Base of the reconstructed original-order answers, returned by halt.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.scratch : Fin 160

Base of reusable pruned-kernel stack and cache space.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.stamps : Fin 160

Base of the timestamp directory shared by all tiles.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.memoryLimit : Fin 160

One past the complete caller and kernel allocation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.epoch : Fin 160

Returned kernel epoch propagated to the next tile.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.index : Fin 160

Current tile, directory-entry or reporting-loop index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.first : Fin 160

First grouped position of the current tile's actual span.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.stop : Fin 160

One past the last grouped position of the current tile.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.rowBand : Fin 160

Row band computed by division of the current tile key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.colBand : Fin 160

Column band computed by remainder of the current tile key.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.leftPointer : Fin 160

Actual shared left-encoding pointer for the current tile.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.rightPointer : Fin 160

Actual shared right-encoding pointer for the current tile.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.queryPointer : Fin 160

Actual grouped-query pointer passed to the kernel.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.answerPointer : Fin 160

Current grouped-answer pointer passed to the kernel.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.source : Fin 160

Source pointer supplied to a real native copy.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.destination : Fin 160

Destination pointer supplied to a real native copy.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.length : Fin 160

Number of words supplied to a real native copy.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.address : Fin 160

Temporary address for scalar loads, stores and reporting.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.value : Fin 160

Temporary loaded matrix value, answer or original-position index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.zero : Fin 160

Persistent unsigned zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.one : Fin 160

Persistent loop-increment constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.two : Fin 160

Persistent multiplier two for raw-to-signed conversion.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.four : Fin 160

Persistent constant four for header offsets and kernel stack sizing.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.five : Fin 160

First original matrix-payload address, immediately after the four headers.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.six : Fin 160

Persistent constant six used in the computed router allocation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.matrixWords : Fin 160

Total word count of both original matrix payloads.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.queryOffset : Fin 160

Original coordinate-pair block address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.wantedEnd : Fin 160

One past the actual router allocation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.bandEnd : Fin 160

One past the shared-band producer allocation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.temporary : Fin 160

Temporary product used while computing separated buffer addresses.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.catalogue : Fin 160

Base of the producer's shared two-sided encoding catalogue.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.three : Fin 160

Persistent constant three used in the router allocation.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.parameters : WordRAM.Code WordRAM.Basis.standard 160

Compute genuine band scalars before selecting a protected caller area. No memory writes.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.layout : WordRAM.Code WordRAM.Basis.standard 160

Preserve the computed original parameters and calculate every caller buffer address.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.copyCall : WordRAM.Code WordRAM.Basis.standard 160

Real argument setup followed by the unchanged dynamic-length native copy.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.saveInput : WordRAM.Code WordRAM.Basis.standard 160

Save the entire ordinary input, including its length word and coordinate list.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.prepareQueries : WordRAM.Code WordRAM.Basis.standard 160

Put the original raw coordinate pairs in the actual Wanted input convention.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.saveOffsets : WordRAM.Code WordRAM.Basis.standard 160

Save every computed tile offset, including the terminal offset.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.saveCodes : WordRAM.Code WordRAM.Basis.standard 160

Save the actual grouped query codes.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.saveOriginals : WordRAM.Code WordRAM.Basis.standard 160

Save the actual original-position permutation.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.saveGroups : WordRAM.Code WordRAM.Basis.standard 160

Preserve the computed arrays before the band producer reuses the low work area.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.bitCopyStep : WordRAM.Code WordRAM.Basis.standard 160

One actual load, unsigned doubling and store converts a raw 0/1 matrix entry.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.prepareMatrices (bits : Bool) : WordRAM.Code WordRAM.Basis.standard 160

Copy real matrix words into the band producer's adjacent front input blocks. The bit-input variant executes the conversion instruction at every entry.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.initializeDirectory : WordRAM.Code WordRAM.Basis.standard 160

Initialize the one timestamp directory by actual stores, once for the entire product.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.tileArguments : WordRAM.Code WordRAM.Basis.standard 160

Load actual group endpoints and compute both shared catalogue pointers and kernel ABI.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.tileStep : WordRAM.Code WordRAM.Basis.standard 160

One real pruned-kernel call, with the returned epoch propagated to the next tile.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.evaluateTiles : WordRAM.Code WordRAM.Basis.standard 160

Compute all tiles from the actual group arrays; the zero-tile case never divides by zero.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.reconstructStep : WordRAM.Code WordRAM.Basis.standard 160

Read one actual original index and scatter its computed answer into request order.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.reconstruct : WordRAM.Code WordRAM.Basis.standard 160

Every original occurrence is reconstructed by charged native reads and stores.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.restoreInput : WordRAM.Code WordRAM.Basis.standard 160

Restore the complete actual input after all private low-memory reuse has finished.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.prepareRouting : WordRAM.Code WordRAM.Basis.standard 160

Complete actual routing preparation and protected preservation of the original input.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.program (bits : Bool) : WordRAM.Code WordRAM.Basis.standard 160

The complete fixed producer/consumer program. bits=false takes canonical signed matrix words; bits=true takes raw unsigned 0/1 words and performs actual per-entry doubling.