A native mixed-radix encoding cell

Main results

• Encoding.exec_cell: charged index arithmetic, coefficient dispatch, signed linear form, output store and counter increment for one cell of a shared coordinate transform.

References

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

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.CellLocal (i : Fin 32) : Prop

The registers modified by a cell, apart from the nine signed-arithmetic scratch registers.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.instDecidableCellLocal (i : Fin 32) : Decidable (CellLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec_cell {w : ℕ} (hw : 0 < w) (side : Bool) (x : WordRAM.Data 32) (P n s d i : ℕ) (hP : 0 < P) (hnpos : 0 < n) (hi : i < 10 * P * n) (hsrc : x.regs src = s) (hdst : x.regs dst = d) (hcell : x.regs cell = i) (hn : x.regs stride = n) (hseven : x.regs seven = 7) (hten : x.regs ten = 10) (hone : x.regs one = 1) (v : Fin 7 → ℤ) (B : ℤ) (hB : 0 ≤ B) (hv : ∀ (a : Fin 7), |v a| ≤ B) (hmem : ∀ (a : Fin 7), x.mem (s + (i / (10 * n) * 7 + ↑a) * n + i % n) = WordRAM.Signed.encode (v a)) (hval : 7 * B < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (s + d + 64 + 64 * P * n)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) (cellBody side) x y 205 ∧ y.mem = Function.update x.mem (d + i) (WordRAM.Signed.encode (∑ a : Fin 7, coefficients side ⟨i / n % 10, ⋯⟩ a * v a)) ∧ y.regs cell = i + 1 ∧ ∀ (a : Fin 32), 9 ≤ ↑a → ¬CellLocal a → y.regs a = x.regs a

One output entry, with all index arithmetic and the counter increment charged. A single ordinary explicit natural-number bound covers the addresses and index products; no fit condition is imposed on an unspecified intermediate machine state.