A self-delimiting binary code for natural numbers

The prefix-free code used by the machine-description format (planning/tm-infrastructure.md, Milestone C, normative):

encodeNat n = 1^L 0 d₀ … d_{L-1}

where d₀ … d_{L-1} are the little-endian binary digits of n (Turing.natToBits; canonical: the empty string for 0, and the last digit of a nonzero number is true) and L is their count. So encodeNat 0 = [false], and in general (encodeNat n).length = 2·L + 1 with L = ⌈log₂ (n+1)⌉, characterized here without Nat.log2 by lt_two_pow_natToBits and natToBits_length_le.

The parser parseNat accepts only canonical digit strings (a digit block ending in false is rejected), which gives genuine canonicality: parseNat_sound says every accepted prefix is encodeNat of the parsed value. Together with the prefix property parseNat_encodeNat, all downstream codec soundness proofs are compositional (decision D11).

Everything is structurally recursive — natToBits runs on an explicit fuel, with a fuel-irrelevance lemma — so the kernel can evaluate the whole codec and tests can be by decide (decision D10).

Little-endian binary digits

def Turing.natToBitsAux : ℕ → ℕ → List Bool

Little-endian binary digits, structurally recursive in an explicit fuel (so that the kernel can evaluate it); use Turing.natToBits, which instantiates the fuel.

Equations

• Turing.natToBitsAux x✝ 0 = []
• Turing.natToBitsAux 0 n.succ = []
• Turing.natToBitsAux fuel.succ n.succ = ((n + 1) % 2 == 1) :: Turing.natToBitsAux fuel ((n + 1) / 2)

def Turing.natToBits (n : ℕ) : List Bool

The little-endian binary digits of a natural number: [] for 0; the last digit of a nonzero number is true.

Equations

• Turing.natToBits n = Turing.natToBitsAux n n

def Turing.bitsToNat (l : List Bool) : ℕ

The value of a little-endian digit string.

Equations

• Turing.bitsToNat l = List.foldr (fun (b : Bool) (acc : ℕ) => 2 * acc + if b = true then 1 else 0) 0 l

theorem Turing.natToBitsAux_congr {f₁ f₂ n : ℕ} (h₁ : n ≤ f₁) (h₂ : n ≤ f₂) : natToBitsAux f₁ n = natToBitsAux f₂ n

The digits do not depend on the fuel, as long as there is enough of it.

@[simp]

theorem Turing.natToBits_zero : natToBits 0 = []

theorem Turing.natToBits_succ (n : ℕ) : natToBits (n + 1) = ((n + 1) % 2 == 1) :: natToBits ((n + 1) / 2)

@[simp]

theorem Turing.bitsToNat_nil : bitsToNat [] = 0

@[simp]

theorem Turing.bitsToNat_cons (b : Bool) (l : List Bool) : bitsToNat (b :: l) = 2 * bitsToNat l + if b = true then 1 else 0

theorem Turing.natToBits_two_mul {m : ℕ} (hm : 0 < m) : natToBits (2 * m) = false :: natToBits m

The digits of 2·m (for m > 0): a false in front of the digits of m.

theorem Turing.natToBits_two_mul_add_one (m : ℕ) : natToBits (2 * m + 1) = true :: natToBits m

The digits of 2·m + 1: a true in front of the digits of m.

@[simp]

theorem Turing.bitsToNat_natToBits (n : ℕ) : bitsToNat (natToBits n) = n

Digits round-trip: the value of the digits of n is n.

theorem Turing.natToBits_getLast?_ne_false (n : ℕ) : (natToBits n).getLast? ≠ some false

Canonicality: no digit string produced by natToBits ends in false.

theorem Turing.bitsToNat_pos {l : List Bool} (h : l.getLast? = some true) : 0 < bitsToNat l

A canonical nonempty digit string has positive value.

theorem Turing.natToBits_bitsToNat (l : List Bool) : l.getLast? ≠ some false → natToBits (bitsToNat l) = l

Digits round-trip the other way: on canonical strings, natToBits ∘ bitsToNat is the identity.

The length of the digit string

theorem Turing.lt_two_pow_natToBits (n : ℕ) : n < 2 ^ (natToBits n).length

natToBits n has enough digits for n.

theorem Turing.natToBits_length_le {n k : ℕ} : n < 2 ^ k → (natToBits n).length ≤ k

natToBits n has no more digits than any binary bound on n.

theorem Turing.natToBits_length_mono {m n : ℕ} (h : m ≤ n) : (natToBits m).length ≤ (natToBits n).length

The digit count is monotone.

The self-delimiting code

def Turing.encodeNat (n : ℕ) : List Bool

The self-delimiting code of a natural number: the digit count in unary, a false separator, then the digits.

Equations

• Turing.encodeNat n = List.replicate (Turing.natToBits n).length true ++ false :: Turing.natToBits n

def Turing.parseUnary : List Bool → ℕ × List Bool

Split a maximal run of leading trues.

Equations

• Turing.parseUnary (true :: s) = match Turing.parseUnary s with | (k, r) => (k + 1, r)
• Turing.parseUnary x✝ = (0, x✝)

def Turing.parseNat (s : List Bool) : Option (ℕ × List Bool)

Parse one self-delimiting natural number; rejects non-canonical digit strings.

Equations

• One or more equations did not get rendered due to their size.

theorem Turing.parseUnary_replicate (k : ℕ) (r : List Bool) : parseUnary (List.replicate k true ++ false :: r) = (k, false :: r)

theorem Turing.parseUnary_sound (s : List Bool) : s = List.replicate (parseUnary s).fst true ++ (parseUnary s).snd

@[simp]

theorem Turing.parseNat_encodeNat (n : ℕ) (rest : List Bool) : parseNat (encodeNat n ++ rest) = some (n, rest)

Prefix property: parseNat consumes exactly encodeNat n and returns the rest.

theorem Turing.parseNat_sound {s rest : List Bool} {n : ℕ} (h : parseNat s = some (n, rest)) : s = encodeNat n ++ rest

Soundness: every accepted prefix is the canonical encoding of the parsed value.

theorem Turing.encodeNat_injective : Function.Injective encodeNat

theorem Turing.encodeNat_length (n : ℕ) : (encodeNat n).length = 2 * (natToBits n).length + 1

theorem Turing.encodeNat_length_le {n k : ℕ} (h : n < 2 ^ k) : (encodeNat n).length ≤ 2 * k + 1

The code of n < 2^k takes at most 2k + 1 bits.

theorem Turing.encodeNat_length_mono {m n : ℕ} (h : m ≤ n) : (encodeNat m).length ≤ (encodeNat n).length

The code length is monotone.