Saving actual routing arrays across producer calls

Main results

• QueriedProduct.exec_saveOffsets: save all computed offsets, including the terminal word.
• QueriedProduct.exec_saveCodes: save the actual grouped query codes.
• QueriedProduct.exec_saveOriginals: save the actual original-position permutation.

Each internal interface proves its charged copy execution. The protected outputs are copied from actual router memory, without constructing or supplying a routing certificate.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.group_copy_bounds (L m N Q : ℕ) : Wanted.offsetAddress L m N Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 1 ≤ Wanted.memoryLimit L m N Q ∧ Wanted.codeAddress L m N Q + Q ≤ Wanted.memoryLimit L m N Q ∧ Wanted.originalAddress L m N Q + Q ≤ Wanted.memoryLimit L m N Q ∧ Wanted.memoryLimit L m N Q ≤ offsetBase L m N Q ∧ offsetBase L m N Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 1 ≤ memoryEnd L m N Q ∧ codeBase L m N Q + Q ≤ memoryEnd L m N Q ∧ originalBase L m N Q + Q ≤ memoryEnd L m N Q

Every low routing source precedes the protected destinations.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_saveOffsets {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hsrc : x.regs (bank Wanted.offsets) = Wanted.offsetAddress L m N Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w saveOffsets x y (7 * MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 17) ∧ Parameters L m N Q y ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (Wanted.offsetAddress L m N Q) (offsetBase L m N Q) (MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 1) ∧ ∀ (i : Fin 160), 7 ≤ ↑i → i ≠ source → i ≠ destination → i ≠ length → y.regs i = x.regs i

Actual argument setup and native copying preserve the caller protocol and every other register beyond the copy routine. This is an internal producer-consumer execution interface.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_saveCodes {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hsrc : x.regs (bank Wanted.codes) = Wanted.codeAddress L m N Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w saveCodes x y (7 * Q + 10) ∧ Parameters L m N Q y ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (Wanted.codeAddress L m N Q) (codeBase L m N Q) Q ∧ ∀ (i : Fin 160), 7 ≤ ↑i → i ≠ source → i ≠ destination → i ≠ length → y.regs i = x.regs i

Actual argument setup and native copying preserve the caller protocol and every other register beyond the copy routine. This is an internal producer-consumer execution interface.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_saveOriginals {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hsrc : x.regs (bank Wanted.originals) = Wanted.originalAddress L m N Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w saveOriginals x y (7 * Q + 10) ∧ Parameters L m N Q y ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (Wanted.originalAddress L m N Q) (originalBase L m N Q) Q ∧ ∀ (i : Fin 160), 7 ≤ ↑i → i ≠ source → i ≠ destination → i ≠ length → y.regs i = x.regs i

Actual argument setup and native copying preserve the caller protocol and every other register beyond the copy routine. This is an internal producer-consumer execution interface.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_saveGroups {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (wp : Wanted.Parameters L m N Q (WordRAM.Data.comap bank x)) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w saveGroups x y (7 * MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 14 * Q + 37) ∧ Parameters L m N Q y ∧ (∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2, y.mem (offsetBase L m N Q + t) = x.mem (Wanted.offsetAddress L m N Q + t)) ∧ (∀ j < Q, y.mem (codeBase L m N Q + j) = x.mem (Wanted.codeAddress L m N Q + j)) ∧ (∀ j < Q, y.mem (originalBase L m N Q + j) = x.mem (Wanted.originalAddress L m N Q + j)) ∧ ∀ (a : ℕ), a < offsetBase L m N Q ∨ originalBase L m N Q + Q ≤ a → y.mem a = x.mem a

Save all three actual routing arrays before the second producer reuses low memory. Every protected value is read from the router's executed memory, and the complete outside frame includes the protected original input and all untouched low cells.