Charged initialization and encoding-array size

Main results

• PrunedQuery.exec_powers: compute 10^L using the actual native multiplication loop, preserving all caller parameters and memory.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.PowersLocal (i : Fin registers) : Prop

The scalar registers initialized or advanced by the power loop.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidablePowersLocal (i : Fin registers) : Decidable (PowersLocal i)

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_powers {w L Q : ℕ} (x : WordRAM.Data registers) (hL : x.regs inputDepth = L) (hbound : WordRAM.Fits w (addressBound L Q)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w powers x y (4 * L + 10) ∧ y.mem = x.mem ∧ y.regs inputDepth = L ∧ y.regs span = 10 ^ L ∧ y.regs index = L ∧ y.regs nil = 0 ∧ y.regs one = 1 ∧ y.regs two = 2 ∧ y.regs ten = 10 ∧ y.regs nine = 9 ∧ y.regs frameWidth = 4 ∧ ∀ (i : Fin registers), ¬PowersLocal i → y.regs i = x.regs i

The power loop charges its eight initializations, both body instructions, loop tests and jumps. The only width premise is a bound on ordinary input-derived natural numbers.