Charged polynomial workspace reservation

The outer controller computes its preprocessing word envelope by actual multiplication and decrement instructions. The exponent is fixed with the input-magnitude parameter, not supplied by an oracle. All other controls and every memory cell are preserved by the reservation loop.

Main results

• exec_power: the complete native exponentiation loop and its charged frame.

These finite native reservation proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.exec_power {w B E : ℕ} (x : WordRAM.Data 16) (hB : 1 ≤ B) (hs : x.regs scale = B) (hc : x.regs remaining = E) (hv : x.regs envelope = 1) (ho : x.regs one = 1) (hz : x.regs zero = 0) (hfit : WordRAM.Fits w (B ^ E)) (hcount : WordRAM.Fits w E) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w power x y (4 * E + 2) ∧ y.regs envelope = B ^ E ∧ y.regs remaining = 0 ∧ (∀ (i : Fin 16), i ≠ envelope → i ≠ remaining → y.regs i = x.regs i) ∧ y.mem = x.mem

Native exponentiation from the actual loop registers, with all multiplication work charged.