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.

@[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.