Execution of the native wanted-output digit loop

Main results

• Wanted.exec_pack: actual unsigned packing with an explicit linear instruction bound and unchanged memory, for arbitrary initial scratch-register contents.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.PackParameters (L : ℕ) (x : WordRAM.Data 16) : Prop

Scalar contents retained throughout packing. These are only register equalities.

• depth : x.regs Wanted.depth = L

  Original depth.

• one : x.regs Wanted.one = 1

  Initialized unit.

• two : x.regs Wanted.two = 2

  Binary radix.

• three : x.regs Wanted.three = 3

  Compressed offset radix.

• ten : x.regs Wanted.ten = 10

  Output radix.

• nine : x.regs Wanted.nine = 9

  Inner output digit.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.PackProgress (L M R C : ℕ) (x : WordRAM.Data 16) : Prop

A consumed prefix and the remaining arithmetic recurrence give the original output.

• fixed : PackParameters L x

  Persistent constants and depth.

• level_le : x.regs level ≤ L

  A coordinate is visited at most once.

• mask_le : x.regs mask ≤ M

  Binary division decreases the mask.

• row_le : x.regs row ≤ R

  Ternary division decreases the row offset.

• col_le : x.regs col ≤ C

  Ternary division decreases the column offset.

• power_eq : x.regs power = 10 ^ x.regs level

  Actual next output place.

• code_lt : x.regs code < x.regs power

  Already emitted digits fit below the next place.

• value : x.regs code + x.regs power * MatrixMultiplication.Schonhage.QueryDigits.pack (L - x.regs level) (x.regs mask) (x.regs row) (x.regs col) = MatrixMultiplication.Schonhage.QueryDigits.pack L M R C

  Prefix and residual recurrence have the desired complete value.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_packBody {w L M R C : ℕ} (x : WordRAM.Data 16) (hx : PackProgress L M R C x) (hc : (WordRAM.Cond.lt level depth).Holds x) (hfit : WordRAM.Fits w (M + R + C + L + 32 * 10 ^ L + 32)) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w packBody x y 13 ∧ PackProgress L M R C y ∧ y.mem = x.mem ∧ L - y.regs level < L - x.regs level

One coordinate's actual test, arithmetic and register updates. The numeric budget is derived from original inputs, rather than an assumed bound on intermediate states.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_pack {w : ℕ} (L M R C : ℕ) (x : WordRAM.Data 16) (hL : x.regs depth = L) (hM : x.regs mask = M) (hR : x.regs row = R) (hC : x.regs col = C) (hfit : WordRAM.Fits w (M + R + C + L + 32 * 10 ^ L + 32)) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w packCode x y (15 * L + 10) ∧ y.regs code = MatrixMultiplication.Schonhage.QueryDigits.pack L M R C ∧ y.regs depth = L ∧ y.mem = x.mem

Execute the entire fixed packer from ordinary register inputs. Every branch, division, remainder, index update and loop control is charged; memory and the depth are preserved.