Saturating binary decoding

Words are read most significant bit first. Saturating at every step keeps a unary accumulator bounded on arbitrary input words; it agrees with capping the full mathematical binary value.

Main definitions

• binaryValue: the natural represented by a binary word, without a size bound.
• boundedBinaryValue: the same fold with a cap at every step.
• binaryWord: the word of a given width representing a number.
• lowBits: a fixed-width word in the opposite, least-significant-first order.

Main results

• binaryValue_injective_of_length_eq: fixed-width words have distinct binary values.
• boundedBinaryValue_eq: incremental saturation equals a single final cap.
• boundedBinaryValue_le: every output is at most the cap.
• binaryValue_lt_two_pow, exists_binaryValue_eq: the words of t bits represent exactly the numbers below 2 ^ t.
• length_binaryWord, binaryValue_binaryWord: the word of width t of a number below 2 ^ t.

References

Adapted from Probability/UniformNat.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.BitString.lowBits (width value : ℕ) : List Bool

The first width digits of a natural, least significant first. Unlike binaryWord, this always has the declared width: high digits are truncated and absent digits are false.

@[simp]

theorem Cslib.BitString.length_lowBits (width value : ℕ) : (lowBits width value).length = width

lowBits width value has width digits.

theorem Cslib.BitString.lowBits_eq_ofFn (width value : ℕ) : lowBits width value = List.ofFn fun (i : Fin width) => value.testBit ↑i

The executable digit loop agrees with the finite coordinate view.

def Cslib.BitString.binaryValue (word : List Bool) : ℕ

The natural number represented by a word, most significant bit first.

def Cslib.BitString.boundedBinaryValue (bound : ℕ) (word : List Bool) : ℕ

Decode binary digits with a saturating accumulator.

theorem Cslib.BitString.boundedBinaryValue_eq (bound : ℕ) (word : List Bool) : boundedBinaryValue bound word = min bound (binaryValue word)

Saturating at each step agrees with capping the final mathematical value.

theorem Cslib.BitString.boundedBinaryValue_le (bound : ℕ) (word : List Bool) : boundedBinaryValue bound word ≤ bound

The unary result never exceeds the declared bound.

theorem Cslib.BitString.binaryValue_snoc (word : List Bool) (bit : Bool) : binaryValue (word ++ [bit]) = 2 * binaryValue word + bit.toNat

Append a low-order bit to a most-significant-first binary word.

theorem Cslib.BitString.binaryValue_reverse_bits (n : ℕ) : binaryValue n.bits.reverse = n

Reversing the little-endian digits gives the corresponding most-significant-first value.

theorem Cslib.BitString.binaryValue_replicate_true (k : ℕ) : binaryValue (List.replicate k true) + 1 = 2 ^ k

An all-one binary word represents one less than the corresponding power of two.

theorem Cslib.BitString.binaryValue_lt_two_pow (word : List Bool) : binaryValue word < 2 ^ word.length

A word of n bits represents a number below 2 ^ n.

theorem Cslib.BitString.binaryValue_replicate_false_append (n : ℕ) (word : List Bool) : binaryValue (List.replicate n false ++ word) = binaryValue word

Leading zeros do not change the represented number.

def Cslib.BitString.binaryWord (w a : ℕ) : List Bool

The word of width w representing a in binary, most significant bit first, padded with leading zeros; it has width w when a < 2 ^ w (length_binaryWord).

theorem Cslib.BitString.length_binaryWord {w a : ℕ} (ha : a < 2 ^ w) : (binaryWord w a).length = w

The word of width w representing a has w bits when a < 2 ^ w.

@[simp]

theorem Cslib.BitString.binaryValue_binaryWord (w a : ℕ) : binaryValue (binaryWord w a) = a

The word binaryWord w a represents a, whatever the width w.

theorem Cslib.BitString.exists_binaryValue_eq {t k : ℕ} (hk : k < 2 ^ t) : ∃ (u : Fin t → Bool), binaryValue (List.ofFn u) = k

Every number below 2 ^ t is represented by a word of t bits.

theorem Cslib.BitString.binaryValue_injective_of_length_eq {u v : List Bool} (hlen : u.length = v.length) (h : binaryValue u = binaryValue v) : u = v

Fixed-width binary words represent their values injectively.