Complete native routing from original scalar and coordinate inputs #
Main results #
Wanted.exec_program: compute tables, counts, prefix offsets, query codes and stable scatter positions in the fixed native program, retaining the original input and outside frame.
All table and cursor premises of the internal stages are established by actual preceding code. The caller supplies only the original scalar headers and the ordinary coordinate list.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_program {w L m N Q : ℕ} (hm : m ≤ L) (pairs : ℕ → ℕ × ℕ) (hpairs : ∀ i < Q, (pairs i).1 < N ∧ (pairs i).2 < N) (x : WordRAM.Data 96) (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N) (hQ : x.mem 4 = Q) (hinput : ∀ i < Q, x.mem (5 + 2 * i) = (pairs i).1 ∧ x.mem (5 + 2 * i + 1) = (pairs i).2) (hfit : WordRAM.Fits w (wordBudget L m N Q)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w program x y (timeBound L m N Q) ∧ 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 (offsetAddress L m N Q + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k < t) Q) ∧ y.mem (offsetAddress L m N Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2) = Q ∧ ∀ (a : ℕ), a < inputLimit Q ∨ memoryLimit L m N Q ≤ a → y.mem a = x.mem a
The complete native program, with no table, query-code, prefix or permutation oracle. Every original query occurrence has one computed stable destination and retains its index.