Computing each tile's actual kernel arguments #
Main results #
QueriedProduct.exec_tileArguments: load real group endpoints, divide the tile index, compute shared catalogue/query/output pointers and populate the existing native kernel ABI.
The span values in this internal interface describe the actual saved offset words. The full caller establishes their bounds from its executed counting/prefix/scatter passes.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_tileArguments {w L m N Q t a b : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hx : x.regs index = t) (ht : t < MatrixMultiplication.Schonhage.numBands L m N ^ 2) (ha : x.mem (offsetBase L m N Q + t) = a) (hb : x.mem (offsetBase L m N Q + t + 1) = b) (hab : a ≤ b) (hbQ : b ≤ Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin w tileArguments x y 21 ∧ Parameters L m N Q y ∧ y.mem = x.mem ∧ y.regs index = t ∧ y.regs epoch = x.regs epoch ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.inputDepth = L ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.arrayA = BandPreparation.catalogueBase L m N + t / MatrixMultiplication.Schonhage.numBands L m N * 10 ^ L ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.arrayB = BandPreparation.catalogueBase L m N + (MatrixMultiplication.Schonhage.numBands L m N + t % MatrixMultiplication.Schonhage.numBands L m N) * 10 ^ L ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.queries = codeBase L m N Q + a ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.queryCount = b - a ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.output = groupedBase L m N Q + a ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.scratch = scratchBase L m N Q ∧ (WordRAM.Data.comap bank y).regs PrunedQuery.epoch = x.regs epoch
Actual tile-index arithmetic and kernel-argument setup cost twenty-one instructions. Only the two real offset words are read. Every unsigned arithmetic fit follows from the original allocation bound and the computed span bounds.