Complete charged execution of the shared encoder

Main results

• Encoding.exec_coordinates: all shared coordinate transforms, with charged loop control.
• Encoding.exec: complete initialization, transforms and fixed-output copy with an explicit 240 * (L+1) * 10^L native instruction bound.

The code is directly over the standard unsigned WordRAM. Its signed add/subtract blocks use two extra target bits and respectively at most fifteen/seventeen actual instructions. There is no whole-program signed compiler in this construction and no uncharged simulation premise.

References

The encodings are from [AlmanWilliams2026, Section 2.4.1]; see Encoding for provenance.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.timeBound (L : ℕ) : ℕ

Explicit total instruction bound, including header preparation, all index arithmetic, stage and cell loop control, and the final copy. A final halt costs one additional instruction.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec_coordinates {w L : ℕ} (hw : 0 < w) (side : Bool) (arr : ℕ → ℤ) (initial : ℕ → ℕ) (x : WordRAM.Data 32) (hx : Progress side L 0 arr initial x) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ i < 7 ^ L, |arr i| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) (WordRAM.Code.loop (WordRAM.Cond.lt stage depth) (stageBody side)) x y (L * (207 * 10 ^ L + 14) + 2) ∧ Progress side L L arr initial y

Every coordinate stage is executed natively. Charging every stage at the maximum buffer size gives L * (207 * 10^L + 14) + 2 instructions, including both outer loop controls.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec {w L : ℕ} (hw : 0 < w) (side : Bool) (arr : ℕ → ℤ) (x : WordRAM.Data 32) (hheader : x.mem 1 = L) (hinput : ∀ i < 7 ^ L, x.mem (2 + i) = WordRAM.Signed.encode (arr i)) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ i < 7 ^ L, |arr i| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) (program side) x y (timeBound L) ∧ (∀ p < 10 ^ L, y.mem (outputBase L + p) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (coefficients side)) L 0 arr p 0)) ∧ (∀ (a : ℕ), ¬(outputBase L ≤ a ∧ a < scratchBase L + 10 ^ L) → y.mem a = x.mem a) ∧ y.regs output = outputBase L ∧ y.regs capacity = 10 ^ L

The encoder runs from a concrete flat memory layout and preserves every cell outside its output/scratch region. Only the original input magnitude and explicit address bounds are assumed; every intermediate signed arithmetic fit is derived in the coordinate-stage proof.