Initialized flat callable products #
The same final native data witnesses the charged prefix run, exact physical product words, restored local original input, protected caller memory and the final halt. The program and its 163 registers are fixed independently of dimensions, runtime base and physical word width.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.runs {W m N : ℕ} (caller : List ℕ) (X : Matrix (Fin N) (Fin (MatrixMultiplication.Schonhage.D m)) ℤ) (Y : Matrix (Fin (MatrixMultiplication.Schonhage.D m)) (Fin N) ℤ) (qs : List (Fin N × Fin N)) (hN : MatrixMultiplication.Schonhage.D m ^ 18 ≤ N) (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) (hcaller : ∀ v ∈ caller, WordRAM.Fits W v) (hfit : WordRAM.Fits W (inputBase caller + 4 * windowSize N qs.length + 1024)) :
WordRAM.InputFits W (input caller X Y qs) ∧ ∃ (y : WordRAM.Data 163),
∃ n ≤ timeBound qs + 2,
WordRAM.Runs W (entryProgram.program Reg.result) (WordRAM.State.init (input caller X Y qs))
{ pc := entryProgram.size, data := y } n ∧ WordRAM.Executes W (entryProgram.program Reg.result) (WordRAM.State.init (input caller X Y qs))
(inputBase caller + QueriedProduct.outputBase (19 * m) m N qs.length) (n + 1) ∧ WordRAM.Data.Bounded W y ∧ (∀ (i : Fin qs.length),
y.mem (inputBase caller + (QueriedProduct.outputBase (19 * m) m N qs.length + ↑i)) = WordRAM.Signed.encode ((X * Y) (qs.get i).1 (qs.get i).2)) ∧ (∀ a < QueriedProduct.inputEnd m N qs.length,
y.mem (inputBase caller + a) = (WordRAM.State.init (input caller X Y qs)).data.mem (inputBase caller + a)) ∧ ∀ (a : ℕ),
a < inputBase caller ∨ inputBase caller + windowSize N qs.length ≤ a →
y.mem a = (WordRAM.State.init (input caller X Y qs)).data.mem a
Actual initialized execution with no computed-layout, bounded-scratch or execution premise.
Every original duplicate request has its own exact physical answer cell. The n+1 charge
includes the halt reached by the same final data y in the prefix Runs.
The complete standalone caller has a fixed finite flat program, including halt.
The width-independent code computes its own virtual modulus without reading physical width.