Flat standard-WordRAM clients for the complete encoders #
Main results #
Encoding.runs_left,Encoding.runs_right: actual flat runs fromState.init, the complete output memory block, preserved outside frame, and a charged final halt.Encoding.program_length_le: one finite code-size bound independent of depth and width.
The final halt returns the output block's address. Its length is 10^L and its cells contain
the canonical signed encodings of the public mathematical values.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.program_length_le (side : Bool) :
A single code-size bound for both fixed encoders, including the final halt.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.leafIndex_bijective (L : ℕ) :
Every one of the 10^L flat output cells corresponds to exactly one original leaf.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.runs_left {w L : ℕ} (hw : 0 < w) (a : MatrixMultiplication.Schonhage.LeftStr L → ℤ) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ (u : MatrixMultiplication.Schonhage.LeftStr L), |a u| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) :
WordRAM.InputFits (w + 2) (inputL a) ∧ ∃ (y : WordRAM.Data 32),
∃ n ≤ timeBound L,
WordRAM.Runs (w + 2) ((program false).program output) (WordRAM.State.init (inputL a))
{ pc := (program false).size, data := y } n ∧ WordRAM.Executes (w + 2) ((program false).program output) (WordRAM.State.init (inputL a)) (outputBase L)
(n + 1) ∧ (∀ (τ : MatrixMultiplication.Schonhage.Leaf L),
y.mem (outputBase L + ↑(leafIndex τ)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.encodingL a τ)) ∧ ∀ (b : ℕ),
¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) → y.mem b = (WordRAM.State.init (inputL a)).data.mem b
Actual flat native left-encoding execution. The prefix exposes every output memory cell; the same run then halts at its fixed final instruction, charging one more instruction.
theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.runs_right {w L : ℕ} (hw : 0 < w) (a : MatrixMultiplication.Schonhage.RightStr L → ℤ) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ (u : MatrixMultiplication.Schonhage.RightStr L), |a u| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) :
WordRAM.InputFits (w + 2) (inputR a) ∧ ∃ (y : WordRAM.Data 32),
∃ n ≤ timeBound L,
WordRAM.Runs (w + 2) ((program true).program output) (WordRAM.State.init (inputR a))
{ pc := (program true).size, data := y } n ∧ WordRAM.Executes (w + 2) ((program true).program output) (WordRAM.State.init (inputR a)) (outputBase L)
(n + 1) ∧ (∀ (τ : MatrixMultiplication.Schonhage.Leaf L),
y.mem (outputBase L + ↑(leafIndex τ)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.encodingR a τ)) ∧ ∀ (b : ℕ),
¬(outputBase L ≤ b ∧ b < scratchBase L + 10 ^ L) → y.mem b = (WordRAM.State.init (inputR a)).data.mem b
Actual flat native right-encoding execution, with all output cells and the same charged standard-WordRAM calling convention and final halt.