Actual reconstruction in original request order #
Main results #
QueriedProduct.exec_reconstruct: read the stored original indices and grouped answers, then scatter every answer to its original request position, charging every instruction.
The existing stable-position bijection proves that no earlier answer is overwritten. Neither an inverse permutation nor a scatter execution is supplied to the program.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_reconstruct {w L m N : ℕ} (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (old : ℕ → ℕ) (x : WordRAM.Data 160) (hp : Parameters L m N qs.length x) (hg : SavedGroups L m N qs.length old x.mem) (horiginals :
∀ (i : Fin qs.length),
old
(Wanted.originalAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = ↑i) (hanswers :
∀ (i : Fin qs.length),
x.mem
(groupedBase L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) (hfit : WordRAM.Fits w (wordBudget L m N qs.length)) :
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin w reconstruct x y (9 * qs.length + 3) ∧ Parameters L m N qs.length y ∧ (∀ (i : Fin qs.length),
y.mem (outputBase L m N qs.length + ↑i) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ ∀ (a : ℕ), a < outputBase L m N qs.length ∨ scratchBase L m N qs.length ≤ a → y.mem a = x.mem a
Actual reconstruction retains repeated input occurrences, input words and outside memory. Only the designated original-order answer block is written.