Charged native splitting of tensor-string digits

Main results

• BandPreparation.exec_split: the actual base-seven digit loop computes the binary mask and both compressed offsets with every native arithmetic operation charged.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.SplitParameters (L : ℕ) (x : WordRAM.Data 96) : Prop

Fixed scalar inputs to a digit loop, without execution or fit assumptions.

• levels : x.regs BandPreparation.levels = L

  Original depth.

• one : x.regs BandPreparation.one = 1

  Constant one.

• two : x.regs BandPreparation.two = 2

  Constant two.

• three : x.regs BandPreparation.three = 3

  Constant three.

• four : x.regs BandPreparation.four = 4

  Constant four.

• seven : x.regs BandPreparation.seven = 7

  Constant seven.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.SplitProgress (L a : ℕ) (x : WordRAM.Data 96) : Prop

Remaining-digit equations and elementary counter bounds during the native scan.

• fixed : SplitParameters L x

  Parameters are retained.

• level_le : x.regs level ≤ L

  Number of consumed levels.

• residue_le : x.regs residue ≤ a

  Division only decreases the residual index.

• mask_power : x.regs maskPower = 2 ^ x.regs level

  Binary place weight.

• outer_power : x.regs outerPower ≤ 3 ^ x.regs level

  At most one outer place is consumed per level.

• inner_power : x.regs innerPower ≤ 4 ^ x.regs level

  At most one inner place is consumed per level.

• mask_acc : x.regs maskAcc < x.regs maskPower

  Partial binary value is below its next place.

• outer_acc : x.regs outerAcc < x.regs outerPower

  Partial base-three value is below its next place.

• inner_acc : x.regs innerAcc < x.regs innerPower

  Partial base-four value is below its next place.

• mask_value : x.regs maskAcc + x.regs maskPower * (MatrixMultiplication.Schonhage.BandDigits.parts (L - x.regs level) (x.regs residue)).mask = (MatrixMultiplication.Schonhage.BandDigits.parts L a).mask

  The binary accumulator and remaining digits give the complete mask.

• outer_value : x.regs outerAcc + x.regs outerPower * (MatrixMultiplication.Schonhage.BandDigits.parts (L - x.regs level) (x.regs residue)).outer = (MatrixMultiplication.Schonhage.BandDigits.parts L a).outer

  The outer accumulator and remaining digits give the complete outer offset.

• inner_value : x.regs innerAcc + x.regs innerPower * (MatrixMultiplication.Schonhage.BandDigits.parts (L - x.regs level) (x.regs residue)).inner = (MatrixMultiplication.Schonhage.BandDigits.parts L a).inner

  The inner accumulator and remaining digits give the complete inner offset.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_splitBody {w : ℕ} (L a : ℕ) (x : WordRAM.Data 96) (hx : SplitProgress L a x) (hc : (WordRAM.Cond.lt level levels).Holds x) (hfit : WordRAM.Fits w (a + L + 16 * 10 ^ L + 16)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w splitBody x y 11 ∧ SplitProgress L a y ∧ y.mem = x.mem ∧ L - y.regs level < L - x.regs level

One native digit iteration, using only bounds derived from the original index/depth.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_split {w : ℕ} (L a : ℕ) (x : WordRAM.Data 96) (hx : SplitParameters L x) (ha : x.regs index = a) (hfit : WordRAM.Fits w (a + L + 16 * 10 ^ L + 16)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w splitCode x y (13 * L + 10) ∧ SplitParameters L y ∧ y.regs maskAcc = (MatrixMultiplication.Schonhage.BandDigits.parts L a).mask ∧ y.regs outerAcc = (MatrixMultiplication.Schonhage.BandDigits.parts L a).outer ∧ y.regs innerAcc = (MatrixMultiplication.Schonhage.BandDigits.parts L a).inner ∧ y.mem = x.mem

All digits are split by the fixed native loop. Scratch need not start at zero: every accumulator and place weight is explicitly initialized and its initialization is charged.