Complete native count pass for wanted positions

Main results

• Wanted.exec_clearCounts: initialize exactly the actual tile-count cells.
• Wanted.exec_countQueries: all original occurrences, including repetitions, are counted by the actual coordinate-loading and tile-index code in linear charged time.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_clearCounts {w L m N Q : ℕ} (x : WordRAM.Data 96) (hx : Parameters L m N Q x) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w clearCounts x y (5 * MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 3) ∧ Parameters L m N Q y ∧ (∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2, y.mem (countAddress L Q + t) = 0) ∧ ∀ (a : ℕ), a < countAddress L Q ∨ countAddress L Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2 ≤ a → y.mem a = x.mem a

Actual dense initialization of tile counts. It touches no query or computed table.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_countQueries {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) (hzero : ∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2, x.mem (countAddress L Q + t) = 0) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w countQueries x y (16 * Q + 3) ∧ Parameters L m N Q y ∧ (∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2, y.mem (countAddress L Q + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k = t) Q) ∧ ∀ (a : ℕ), a < countAddress L Q ∨ countAddress L Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2 ≤ a → y.mem a = x.mem a

Every original query is loaded and its actual tile computed. Duplicate input pairs increase counts independently; the readonly input and both computed tables are preserved.