Complete native tile-prefix pass #
Main results #
Wanted.exec_prefix: compute every exact tile span and initialize its scatter cursor, including the terminal query-count offset, with native loads, stores and loop controls.
This is an internal implementation API of the complete routing program.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_prefix {w L m N Q : ℕ} (key : ℕ → ℕ) (hkey : ∀ i < Q, key i < MatrixMultiplication.Schonhage.numBands L m N ^ 2) (x : WordRAM.Data 96) (hx : Parameters L m N Q x) (hcounts :
∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2,
x.mem (countAddress L Q + t) = Nat.count (fun (k : ℕ) => key k = t) Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w prefixCode x y (10 * MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 6) ∧ Parameters L m N Q y ∧ (∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2,
y.mem (offsetAddress L m N Q + t) = Nat.count (fun (k : ℕ) => key k < t) Q) ∧ (∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2,
y.mem (cursorAddressBase L m N Q + t) = Nat.count (fun (k : ℕ) => key k < t) Q) ∧ y.mem (offsetAddress L m N Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2) = Q ∧ ∀ (a : ℕ), a < offsetAddress L m N Q ∨ codeAddress L m N Q ≤ a → y.mem a = x.mem a
The actual prefix loop initializes every immutable span and mutable cursor. Neither the offsets nor the total input length are supplied as precomputed memory certificates.