A charged native binary logarithm

Main definitions

• NatLog.program: successive division by two.

Main results

• NatLog.exec: the floor logarithm with a logarithmic charged instruction bound.
• NatLog.shiftLoop_exec: the same logarithm by right shifts, on any three registers.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.NatLog.arg : Fin 4

Quotient, initially the input.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.NatLog.result : Fin 4

Floor logarithm output.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.NatLog.one : Fin 4

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.NatLog.two : Fin 4

Constant two.

def Cslib.Algorithms.WordRAM.NatLog.body : WordRAM.Code WordRAM.Basis.standard 4

Divide the quotient by two and increment the answer.

def Cslib.Algorithms.WordRAM.NatLog.program : WordRAM.Code WordRAM.Basis.standard 4

Fixed code for Nat.log 2, including its value zero at input zero.

theorem Cslib.Algorithms.WordRAM.NatLog.exec {w : ℕ} (x : WordRAM.Data 4) (h2 : WordRAM.Fits w 2) (hn : WordRAM.Fits w (x.regs arg)) (hout : WordRAM.Fits w (Nat.log 2 (x.regs arg) + 1)) : ∃ (y : WordRAM.Data 4), WordRAM.ExecWithin w program x y (4 * Nat.log 2 (x.regs arg) + 5) ∧ y.regs result = Nat.log 2 (x.regs arg) ∧ y.mem = x.mem ∧ y.regs one = 1 ∧ y.regs two = 2

Compute the floor binary logarithm in at most 4 log₂ n + 5 instructions. Memory is untouched and the input quotient is consumed.

theorem Cslib.Algorithms.WordRAM.NatLog.exec_rename {r w : ℕ} (f : Fin 4 → Fin r) (hf : Function.Injective f) (x : WordRAM.Data r) (h2 : WordRAM.Fits w 2) (hn : WordRAM.Fits w (x.regs (f arg))) (hout : WordRAM.Fits w (Nat.log 2 (x.regs (f arg)) + 1)) : ∃ (y : WordRAM.Data r), WordRAM.ExecWithin w (WordRAM.Code.rename f program) x y (4 * Nat.log 2 (x.regs (f arg)) + 5) ∧ y.regs (f result) = Nat.log 2 (x.regs (f arg)) ∧ y.mem = x.mem ∧ y.regs (f one) = 1 ∧ y.regs (f two) = 2

Run the routine on any injectively chosen registers.

theorem Cslib.Algorithms.WordRAM.NatLog.shiftLoop_exec {r w n : ℕ} {one rem idx : Fin r} (hor : one ≠ rem) (hoi : one ≠ idx) (hri : rem ≠ idx) {x : WordRAM.Data r} (hn : 1 ≤ n) (hone : x.regs one = 1) (hrem : x.regs rem = n) (hidx : x.regs idx = 0) (hn_fit : WordRAM.Fits w n) (hlg_fit : WordRAM.Fits w (Nat.log 2 n)) : ∃ (y : WordRAM.Data r), WordRAM.ExecWithin w (WordRAM.Code.loop (WordRAM.Cond.lt one rem) ((WordRAM.Code.op (WordRAM.Op.bin WordRAM.BinOp.shiftRight rem rem one)).seq (WordRAM.Code.op (WordRAM.Op.bin WordRAM.BinOp.add idx idx one)))) x y (4 * Nat.log 2 n + 2) ∧ y.mem = x.mem ∧ y.regs idx = Nat.log 2 n ∧ ∀ (i : Fin r), i ≠ rem → i ≠ idx → y.regs i = x.regs i

Halving by right shifts on any three distinct registers: from rem = n ≥ 1 and idx = 0, while one < rem do [rem ← rem >>> one; idx ← idx + one] leaves idx = Nat.log 2 n within 4 * Nat.log 2 n + 2 instructions. Memory and every register other than rem and idx are unchanged. Cslib.WordRAM.ExactLog.log2Loop is the exact-basis counterpart.