Protected original-input and coordinate transfers

Main results

• QueriedProduct.exec_saveInput: snapshot the complete original input by actual native copying.
• QueriedProduct.exec_prepareQueries: adapt real coordinates to the router's input convention.

These internal execution interfaces derive copy separation and arithmetic fits from the original numerical parameters. Their memory conclusions describe the actual executed state.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.transfer_bounds (L m N Q : ℕ) : inputEnd m N Q ≤ snapshotBase L m N Q ∧ snapshotBase L m N Q + inputEnd m N Q ≤ memoryEnd L m N Q ∧ 5 + 2 * Q ≤ snapshotBase L m N Q + queryInputBase m N ∧ snapshotBase L m N Q + queryInputBase m N + 2 * Q ≤ memoryEnd L m N Q

Original input, its protected copy and the coordinate adaptation all fit the allocation.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.allocated_fits {w L m N Q a : ℕ} (hfit : WordRAM.Fits w (wordBudget L m N Q)) (ha : a ≤ memoryEnd L m N Q + 16) : WordRAM.Fits w a

Any allocated endpoint fits without assumptions about intermediate machine states.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_saveInput {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w saveInput x y (7 * inputEnd m N Q + 10) ∧ Parameters L m N Q y ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem 0 (snapshotBase L m N Q) (inputEnd m N Q)

The actual input snapshot uses three argument instructions and the native copy loop.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_prepareQueries {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w prepareQueries x y (14 * Q + 10) ∧ Parameters L m N Q y ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (snapshotBase L m N Q + queryInputBase m N) 5 (2 * Q)

Real coordinate words are copied from the protected original input to address five. The caller's original prefix remains protected in its snapshot for final restoration.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_restoreInput {w L m N Q : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 160), WordRAM.ExecWithin w restoreInput x y (7 * inputEnd m N Q + 10) ∧ Parameters L m N Q y ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (snapshotBase L m N Q) 0 (inputEnd m N Q)

Restore the entire original prefix through the same actual copy routine. Answers and all memory outside the prefix remain unchanged.