Initialized flat runs of native wanted-query grouping #
Main results #
Wanted.runs: one actual initialized native run returns grouped query codes, their original-position permutation and exact tile spans; halt is charged on that same run.Wanted.bounded_reachable: every initialized reachable prefix has fitting data words.
The returned unsigned pointer names the code array. Other addresses are explicit functions of the original headers, and the complete original input and outside memory are preserved.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.runs {w L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (hfit : WordRAM.Fits w (wordBudget L m N qs.length)) :
WordRAM.InputFits w (input L m qs) ∧ ∃ (y : WordRAM.Data 96),
∃ n ≤ timeBound L m N qs.length,
WordRAM.Runs w (program.program codes) (WordRAM.State.init (input L m qs)) { pc := program.size, data := y } n ∧ WordRAM.Executes w (program.program codes) (WordRAM.State.init (input L m qs)) (codeAddress L m N qs.length)
(n + 1) ∧ WordRAM.Data.Bounded w y ∧ (∀ (i : Fin qs.length),
y.mem
(codeAddress L m N qs.length + CountingSort.position (tileKey L m N ∘ inputPairs qs) qs.length ↑i) = ↑(PrunedQuery.queryIndex
(MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm)
↑(qs.get i).1 ↑(qs.get i).2)) ∧ y.mem
(originalAddress L m N qs.length + CountingSort.position (tileKey L m N ∘ inputPairs qs) qs.length ↑i) = ↑i) ∧ (∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2,
y.mem (offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ inputPairs qs) k < t) qs.length) ∧ y.mem (offsetAddress L m N qs.length + MatrixMultiplication.Schonhage.numBands L m N ^ 2) = qs.length ∧ ∀ (a : ℕ),
a < inputLimit qs.length ∨ memoryLimit L m N qs.length ≤ a →
y.mem a = (WordRAM.State.init (input L m qs)).data.mem a
Actual initialized standard WordRAM runs, with the same final memory carrying all answers, a charged halt, and the readonly-input/outside frame.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.bounded_reachable {w L m N n : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (hfit : WordRAM.Fits w (wordBudget L m N qs.length)) {y : WordRAM.State 96} (hy : WordRAM.Runs w (program.program codes) (WordRAM.State.init (input L m qs)) y n) :
Ordinary initialized native safety holds at every reachable prefix, including the parameter, table, count and scatter stages, from the same original-input fit guarantee.