Native natural powers

Main definitions

• Power.program: repeated native multiplication, with base and exponent in registers.

Main results

• Power.exec: b^n within 4n+5 instructions, with input-derived intermediate fits.

@[reducible, inline]

abbrev Cslib.WordRAM.Power.value : Fin 5

Result accumulator, initially one.

@[reducible, inline]

abbrev Cslib.WordRAM.Power.counter : Fin 5

Number of completed multiplications.

@[reducible, inline]

abbrev Cslib.WordRAM.Power.base : Fin 5

Input base.

@[reducible, inline]

abbrev Cslib.WordRAM.Power.exponent : Fin 5

Input exponent.

@[reducible, inline]

abbrev Cslib.WordRAM.Power.one : Fin 5

Constant one, initialized by the routine.

def Cslib.WordRAM.Power.body : Code Basis.standard 5

One multiplication and one counter increment.

def Cslib.WordRAM.Power.program : Code Basis.standard 5

A fixed program for natural exponentiation by repeated multiplication.

theorem Cslib.WordRAM.Power.exec {w : ℕ} (b n : ℕ) (hb : 1 ≤ b) (x : Data 5) (hx : x.regs base = b) (hn : x.regs exponent = n) (hfit : Fits w (b ^ n + n + 2)) : ∃ (y : Data 5), ExecWithin w program x y (4 * n + 5) ∧ y.regs value = b ^ n ∧ y.regs counter = n ∧ y.regs one = 1 ∧ y.mem = x.mem ∧ y.regs base = b ∧ y.regs exponent = n

The routine is uniform in its arguments and preserves memory and both input registers. Every multiplication fit follows from the final power and exponent bound.