Relocated native copy and queried-product calls #
All registers of each existing native program are renamed together. Memory relocation is performed by the callable product's actual address compiler, not by register renaming. These internal execution rules preserve the low producer bank and full outside-memory frame.
theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_copy {W s d n : ℕ} (x : WordRAM.Data 320) (hs : x.regs Reg.source = s) (hd : x.regs Reg.destination = d) (hn : x.regs Reg.length = n) (hsep : s + n ≤ d) (hfit : WordRAM.Fits W (s + d + n + 2)) :
∃ (y : WordRAM.Data 320),
WordRAM.ExecWithin W copy x y (7 * n + 4) ∧ y.mem = WordRAM.ArrayCopy.copyPrefix x.mem s d n ∧ y.regs Reg.source = s ∧ y.regs Reg.destination = d ∧ y.regs Reg.length = n ∧ ∀ (i : Fin 320), ↑i < 96 ∨ 103 ≤ ↑i → y.regs i = x.regs i
The real copy loop preserves all adapter metadata and the complete producer register bank.
theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_invoke {W b m N : ℕ} (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (x : WordRAM.Data 320) (hb : x.regs Reg.base = b) (hinput :
∀ a < MatrixMultiplication.Schonhage.QueriedProduct.inputEnd m N qs.length,
x.mem (b + a) = (WordRAM.State.init (MatrixMultiplication.Schonhage.QueriedProduct.input true (19 * m) X Y qs)).data.mem a) (hX : ∀ (i : Fin N) (k : Fin (MatrixMultiplication.Schonhage.D m)), 0 ≤ X i k ∧ X i k ≤ 1) (hY : ∀ (k : Fin (MatrixMultiplication.Schonhage.D m)) (j : Fin N), 0 ≤ Y k j ∧ Y k j ≤ 1) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (hfit : WordRAM.Fits W (b + 4 * MatrixMultiplication.Schonhage.CallableProduct.windowSize N qs.length + 1024)) :
∃ (y : WordRAM.Data 320),
WordRAM.ExecWithin W invoke x y (MatrixMultiplication.Schonhage.CallableProduct.timeBound qs + 2) ∧ y.regs Reg.result = b + MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m N qs.length ∧ (∀ (i : Fin qs.length),
y.mem (b + (MatrixMultiplication.Schonhage.QueriedProduct.outputBase (19 * m) m N qs.length + ↑i)) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ (∀ a < MatrixMultiplication.Schonhage.QueriedProduct.inputEnd m N qs.length, y.mem (b + a) = x.mem (b + a)) ∧ (∀ (a : ℕ),
a < b ∨ b + MatrixMultiplication.Schonhage.CallableProduct.windowSize N qs.length ≤ a →
y.mem a = x.mem a) ∧ ∀ (i : Fin 320), ↑i < 128 → i ≠ Reg.result → y.regs i = x.regs i
The concrete original-input callee derives its execution from the matrices and coordinate occurrences. No execution or time certificate is accepted by this invocation rule.