Executing the native ternary reservation

The forest controller computes its output reservation by actual multiplications and a native countdown. The loop has no supplied exponentiation instruction or resource oracle.

Main results

• reserve_exec: exact native power, loop count, memory frame and register frame.

The controller proof and its charged bound are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.reserve_preserves (i : Fin 128) : i ≠ power → i ≠ remaining → WordRAM.Code.Preserves i reserve

The power loop changes only its accumulator and countdown.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.reserve_exec {w F : ℕ} (x : WordRAM.Data 128) (hp : x.regs power = 1) (hr : x.regs remaining = F + 1) (hz : x.regs zero = 0) (ho : x.regs one = 1) (hs : x.regs scalar = 3) (hfit : WordRAM.Fits w (3 ^ (F + 1))) : ∃ (y : WordRAM.Data 128), WordRAM.ExecWithin w reserve x y (4 * (F + 1) + 2) ∧ y.regs power = 3 ^ (F + 1) ∧ y.regs remaining = 0 ∧ y.mem = x.mem ∧ ∀ (i : Fin 128), i ≠ power → i ≠ remaining → y.regs i = x.regs i

Actual multiplication and subtraction compute the complete ternary-tree reservation.