Actual matrix-word adaptation between producer inputs #
Main results #
QueriedProduct.exec_prepareBits: copy each original raw unsigned entry while actually doubling it for the canonical signed producer convention.
The conversion uses a native load/multiply/store loop. Its original-entry bound derives every arithmetic fit; its invariant protects unread source words and all caller scalars.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.matrix_transfer_bounds (L m N Q : ℕ) :
4 + 2 * (N * MatrixMultiplication.Schonhage.D m) ≤ snapshotBase L m N Q + 5 ∧ snapshotBase L m N Q + 5 + 2 * (N * MatrixMultiplication.Schonhage.D m) ≤ memoryEnd L m N Q
Source and destination blocks in the actual matrix adaptation are disjoint and fit.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_prepareBits {w L m N Q A : ℕ} (x : WordRAM.Data 160) (hp : Parameters L m N Q x) (hfit : WordRAM.Fits w (wordBudget L m N Q)) (hA : WordRAM.Fits w (2 * A)) (hentries : ∀ i < 2 * (N * MatrixMultiplication.Schonhage.D m), x.mem (snapshotBase L m N Q + 5 + i) ≤ A) :
∃ (y : WordRAM.Data 160),
WordRAM.ExecWithin w (prepareMatrices true) x y (8 * (2 * (N * MatrixMultiplication.Schonhage.D m)) + 4) ∧ Parameters L m N Q y ∧ (∀ i < 2 * (N * MatrixMultiplication.Schonhage.D m), y.mem (4 + i) = 2 * x.mem (snapshotBase L m N Q + 5 + i)) ∧ ∀ (a : ℕ), a < 4 ∨ 4 + 2 * (N * MatrixMultiplication.Schonhage.D m) ≤ a → y.mem a = x.mem a
Every raw entry is converted by an actual charged multiplication, with the complete outside frame. The numerical bound concerns original source words, not intermediate states.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.exec_prepareSigned {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 (prepareMatrices false) x y (7 * (2 * (N * MatrixMultiplication.Schonhage.D m)) + 10) ∧ Parameters L m N Q y ∧ (∀ i < 2 * (N * MatrixMultiplication.Schonhage.D m), y.mem (4 + i) = x.mem (snapshotBase L m N Q + 5 + i)) ∧ ∀ (a : ℕ), a < 4 ∨ 4 + 2 * (N * MatrixMultiplication.Schonhage.D m) ≤ a → y.mem a = x.mem a
Canonical signed inputs use actual dynamic copying with no conversion arithmetic.