One computed wanted-query scatter #
Main results #
Wanted.exec_scatterStep: the actual coordinate loads, table lookup, output-digit loop and three scatter stores preserve the exact stable-counting cursor invariant.
This stage contract is an internal implementation API; the query code is calculated from the original pair, rather than supplied as a source memory word or an output certificate.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_scatterStep {w L m N Q n : ℕ} (hm : m ≤ L) (pairs : ℕ → ℕ × ℕ) (hn : n < Q) (hpair : (pairs n).1 < N ∧ (pairs n).2 < N) (x : WordRAM.Data 96) (hx : Parameters L m N Q x) (hi : x.regs index = n) (hinput : x.mem (5 + 2 * n) = (pairs n).1 ∧ x.mem (5 + 2 * n + 1) = (pairs n).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 + Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k = t) n) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w scatterStep x y (15 * L + 39) ∧ Parameters L m N Q y ∧ y.regs index = n + 1 ∧ (∀ 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) Q + Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k = t) (n + 1)) ∧ y.mem (codeAddress L m N Q + CountingSort.position (tileKey L m N ∘ pairs) Q n) = ↑(PrunedQuery.queryIndex
(MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm)
(pairs n).1 (pairs n).2)) ∧ y.mem (originalAddress L m N Q + CountingSort.position (tileKey L m N ∘ pairs) Q n) = n ∧ ∀ (a : ℕ),
a ≠ cursorAddressBase L m N Q + (tileKey L m N ∘ pairs) n →
a ≠ codeAddress L m N Q + CountingSort.position (tileKey L m N ∘ pairs) Q n →
a ≠ originalAddress L m N Q + CountingSort.position (tileKey L m N ∘ pairs) Q n → y.mem a = x.mem a
Load, compute and scatter one original query, preserving the original input and exact per-tile cursors. Every loop in the digit computation and every address instruction is charged.