Complete native wanted-query scatter #
Main results #
Wanted.exec_scatter: compute every original position's output code and stable destination, retaining repetitions and writing the original-position permutation with a charged bound.
This internal implementation API composes the actual router and stores. The finite scatter permutation is proved from occurrence counts; it is neither supplied nor checked by an oracle.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_scatter {w L m N Q : ℕ} (hm : m ≤ L) (pairs : ℕ → ℕ × ℕ) (hpairs : ∀ i < Q, (pairs i).1 < N ∧ (pairs i).2 < N) (x : WordRAM.Data 96) (hx : Parameters L m N Q x) (hinput : ∀ i < Q, x.mem (5 + 2 * i) = (pairs i).1 ∧ x.mem (5 + 2 * i + 1) = (pairs i).2) (htable :
∀ (gh : Fin (MatrixMultiplication.Schonhage.K0 L m) × Fin (MatrixMultiplication.Schonhage.K0 L m)),
x.mem (tableAddress L Q + ↑(MatrixMultiplication.Schonhage.MaskTable.pairRank gh)) = ↑(MatrixMultiplication.Schonhage.MaskTable.selectedMask gh)) (hcursors :
∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2,
x.mem (cursorAddressBase L m N Q + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k < t) Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w scatter x y ((15 * L + 41) * Q + 3) ∧ Parameters L m N Q y ∧ (∀ i < Q,
y.mem (codeAddress L m N Q + CountingSort.position (tileKey L m N ∘ pairs) Q i) = ↑(PrunedQuery.queryIndex
(MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm)
(pairs i).1 (pairs i).2)) ∧ y.mem (originalAddress L m N Q + CountingSort.position (tileKey L m N ∘ pairs) Q i) = i) ∧ (∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2,
y.mem (cursorAddressBase L m N Q + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k < t + 1) Q) ∧ ∀ (a : ℕ), a < cursorAddressBase L m N Q ∨ memoryLimit L m N Q ≤ a → y.mem a = x.mem a
The actual original-order scan fills all grouped codes and the original-position permutation. Its only writes are scatter cursors and the two grouped output arrays.