A charged native ceiling binary logarithm

Main definitions

• NatClog.program: successive ceiling division by two.

Main results

• NatClog.exec: the ceiling logarithm with a logarithmic charged instruction bound.

@[reducible, inline]

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

Quotient, initially the input.

@[reducible, inline]

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

Ceiling logarithm output.

@[reducible, inline]

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

Constant one.

@[reducible, inline]

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

Constant two.

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

Divide the quotient by two and increment the answer.

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

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

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

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

theorem Cslib.Algorithms.WordRAM.NatClog.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) + 1)) (hout : WordRAM.Fits w (Nat.clog 2 (x.regs (f arg)) + 1)) : ∃ (y : WordRAM.Data r), WordRAM.ExecWithin w (WordRAM.Code.rename f program) x y (5 * Nat.clog 2 (x.regs (f arg)) + 5) ∧ y.regs (f result) = Nat.clog 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.