Alternating buffers for the shared native encoder

Main definitions

• Encoding.destination, Encoding.source: the alternating buffer addresses.
• Encoding.Progress: the mixed-radix array and frame invariant after a stage.

References

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

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

Destination of the next coordinate transform; always one of the two fixed buffers.

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

Source of the next coordinate transform; initially the preserved input segment.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.destination_cases (L j : ℕ) : destination L j = outputBase L ∨ destination L j = scratchBase L

A destination is either the fixed output block or the scratch block.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.source_cases {L j : ℕ} (hj : 0 < j) : source L j = outputBase L ∨ source L j = scratchBase L

After the initial transform, the source is also one of the two buffers.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.source_ne_destination (L j : ℕ) : source L j ≠ destination L j

The two alternating buffer addresses differ at every stage.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.buffer_address_le (L j : ℕ) : source L j ≤ 2 + 2 * 10 ^ L ∧ destination L j ≤ 2 + 2 * 10 ^ L

Both current addresses are bounded by the end of the second buffer.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.buffers_separated {L j k N : ℕ} (hjk : j + k = L) (hN : N ≤ 10 ^ L) : source L j + 10 ^ j * 7 ^ k ≤ destination L j ∨ destination L j + N ≤ source L j

Arrays stored at consecutive buffers are disjoint, in either order. The initial input ends exactly at the first output address.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.Progress (side : Bool) (L j : ℕ) (arr : ℕ → ℤ) (initial : ℕ → ℕ) (y : WordRAM.Data 32) : Prop

The shared-array invariant at depth j. All fields describe ordinary registers or mathematical memory values. Execution, timing and width are proved separately.

• fixed : y.regs depth = L ∧ y.regs capacity = 10 ^ L ∧ y.regs output = outputBase L ∧ y.regs scratch = scratchBase L ∧ y.regs one = 1 ∧ y.regs seven = 7 ∧ y.regs ten = 10

  Fixed parameters retained across coordinate stages.

• stage : y.regs Encoding.stage = j

  Number of transformed coordinates.

• prefixes : y.regs Encoding.prefixes = 10 ^ j

  Number of transformed prefixes.

• stride : y.regs Encoding.stride = 7 ^ (L - j)

  Original suffix length in the current source.

• src : y.regs Encoding.src = source L j

  Current source address.

• dst : y.regs Encoding.dst = destination L j

  Current destination address.

• values (p : ℕ) : p < 10 ^ j → ∀ r < 7 ^ (L - j), y.mem (source L j + p * 7 ^ (L - j) + r) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.CoordinateTransform.value (MatrixMultiplication.Schonhage.CoordinateTransform.table (coefficients side)) j (L - j) arr p r)

  The source holds exactly the shared prefix sums.

• frame (a : ℕ) : ¬(outputBase L ≤ a ∧ a < scratchBase L + 10 ^ L) → y.mem a = initial a

  Input, headers and all cells outside both work buffers are preserved.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.progress_zero (side : Bool) (L : ℕ) (arr : ℕ → ℤ) (x y : WordRAM.Data 32) (hy : SetupPost L x y) (hinput : ∀ i < 7 ^ L, x.mem (2 + i) = WordRAM.Signed.encode (arr i)) : Progress side L 0 arr x.mem y

The actual header initialization establishes the zero-stage invariant from the original flat input segment. No scratch values or preinitialized coefficient tables are required.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.progress_step {w L j : ℕ} (hw : 0 < w) (hj : j < L) (side : Bool) (arr : ℕ → ℤ) (initial : ℕ → ℕ) (x : WordRAM.Data 32) (hx : Progress side L j 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) (stageBody side) x y (207 * 10 ^ L + 12) ∧ Progress side L (j + 1) arr initial y

One proved native stage advances the mixed-radix invariant. The signed magnitude bound comes from the original input and the number of coordinates already transformed.