Native copies used by the band-preparation caller #
Main results #
BandPreparation.exec_copyKernel: reuse the actual array-copy program in its fixed low register bank, preserving every persistent register and permitting both address orders.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.copyRegisters_injective :
The seven low copy registers are embedded injectively.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.encoderRegisters_injective :
The unchanged encoder occupies precisely its original low register bank.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_copyKernel {w : ℕ} (x : WordRAM.Data 96) (h1 : WordRAM.Fits w 1) (hs : WordRAM.Fits w (x.regs copySrc + x.regs copyLen)) (hd : WordRAM.Fits w (x.regs copyDst + x.regs copyLen)) (hsep :
x.regs copySrc + x.regs copyLen ≤ x.regs copyDst ∨ x.regs copyDst + x.regs copyLen ≤ x.regs copySrc ∨ x.regs copySrc = x.regs copyDst) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w (WordRAM.Code.rename copyRegisters WordRAM.ArrayCopy.program) x y (7 * x.regs copyLen + 4) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (x.regs copySrc) (x.regs copyDst) (x.regs copyLen) ∧ ∀ (i : Fin 96), 7 ≤ ↑i → y.regs i = x.regs i
Copying uses only the original seven-register routine and its actual native cost.
The persistent high register bank is untouched; arbitrary outside memory is preserved
by the explicit copyPrefix result.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_saveInput {w L m N : ℕ} (x : WordRAM.Data 96) (hx : HeaderPost L m N x) (hfit : WordRAM.Fits w (wordBudget L m N)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w saveInput x y (7 * inputEnd m N + 7) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem 0 (snapshotBase L m N) (inputEnd m N) ∧ ∀ (i : Fin 96), 7 ≤ ↑i → y.regs i = x.regs i
Protect the entire original initialized prefix, including header zero, with the actual native copy. Source words and all memory outside the snapshot block remain untouched.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_restoreInput {w L m N : ℕ} (x : WordRAM.Data 96) (hx : HeaderPost L m N x) (hfit : WordRAM.Fits w (wordBudget L m N)) :
∃ (y : WordRAM.Data 96),
WordRAM.ExecWithin w restoreInput x y (7 * inputEnd m N + 7) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem (snapshotBase L m N) 0 (inputEnd m N) ∧ ∀ (i : Fin 96), 7 ≤ ↑i → y.regs i = x.regs i
Restore the complete original input using the reverse disjoint-copy case. This copies the actual protected words rather than reconstructing or assuming the input is unchanged.