Actual initialization of wanted-query parameters #
Main results #
Wanted.exec_setup: read the query count and compute all relocated addresses natively.Wanted.exec_tables: scalar/header/count setup and actual valid-mask tables from the original four input words, preserving every original query word.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.memoryLimit_eq (L m N Q : ℕ) :
Expanded allocated size, useful without hiding any arithmetic behind a layout record.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.local_fits {w L m N Q : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
WordRAM.Fits w
(16 * (L + N + Q + memoryLimit L m N Q + 10 ^ L + 2 ^ L + MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 16))
The original numerical word budget covers every scalar used by the grouping loops.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_setup {w L m N Q : ℕ} (x : WordRAM.Data 96) (hx : BandPreparation.BandParameters L m N x) (hQ : x.mem 4 = Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w setup x y 16 ∧ Parameters L m N Q y ∧ y.mem = x.mem
Relocate the actual computed-table parameters after the input and allocate all count/prefix/cursor/code/permutation arrays using charged native arithmetic.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_tables {w L m N Q : ℕ} (hm : m ≤ L) (x : WordRAM.Data 96) (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N) (hQ : x.mem 4 = Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w
(BandPreparation.header.seq (BandPreparation.countCode.seq (setup.seq BandPreparation.tablesCode))) x y
(16 * L + (12 * L + 33) * 2 ^ L + 83) ∧ Parameters L m N Q y ∧ (∀ (gh : Fin (MatrixMultiplication.Schonhage.K0 L m) × Fin (MatrixMultiplication.Schonhage.K0 L m)),
y.mem (tableAddress L Q + ↑(MatrixMultiplication.Schonhage.MaskTable.pairRank gh)) = ↑(MatrixMultiplication.Schonhage.MaskTable.selectedMask gh)) ∧ ∀ (a : ℕ), a < inputLimit Q ∨ tableAddress L Q + 2 ^ L ≤ a → y.mem a = x.mem a
The initialized producer of the tables used by routing, without invoking any encoders. The only memory changes are the two relocated mask tables after the complete query input.