Actual routing in the product caller's register bank #
Main results #
QueriedProduct.exec_wanted: invoke the existing router on real coordinates while retaining the caller's protected addresses, including its untouched original-input snapshot.
No routing or permutation certificate is an input. The computed memory equations in this internal interface are conclusions of the actual finite native program.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_wanted {w L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (x : WordRAM.Data 160) (hp : Parameters L m N qs.length x) (hL : x.mem 1 = L) (hmemory : x.mem 2 = m) (hN : x.mem 3 = N) (hQ : x.mem 4 = qs.length) (hinput :
∀ i < qs.length, x.mem (5 + 2 * i) = (Wanted.inputPairs qs i).1 ∧ x.mem (5 + 2 * i + 1) = (Wanted.inputPairs qs i).2) (hfit : WordRAM.Fits w (wordBudget L m N qs.length)) :
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin w (WordRAM.Code.rename bank Wanted.program) x y (Wanted.timeBound L m N qs.length) ∧ Parameters L m N qs.length y ∧ Wanted.Parameters L m N qs.length (WordRAM.Data.comap bank y) ∧ (∀ (i : Fin qs.length),
y.mem
(Wanted.codeAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.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
(Wanted.originalAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = ↑i) ∧ (∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2,
y.mem (Wanted.offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) k < t) qs.length) ∧ y.mem (Wanted.offsetAddress L m N qs.length + MatrixMultiplication.Schonhage.numBands L m N ^ 2) = qs.length ∧ ∀ (a : ℕ), a < Wanted.inputLimit qs.length ∨ Wanted.memoryLimit L m N qs.length ≤ a → y.mem a = x.mem a
The existing actual router runs in the low bank and preserves every caller scalar. Its stable permutation retains separate occurrences of duplicate requests.