Enumerating bit strings

The list BitString.enum n enumerates all n-bit strings once in binary order, least significant bit first. This is an executable enumeration; generating its 2 ^ n entries is not asserted to be polynomial in n.

Main definitions

• Cslib.BitString.enum: enumerate bit strings by prepending both bits to every shorter string.
• Cslib.BitString.enumList: the same enumeration as ordinary lists of bits.

Main results

• Cslib.BitString.mem_enum, Cslib.BitString.length_enum, Cslib.BitString.nodup_enum: the enumeration contains each bit string exactly once and has 2 ^ n entries.
• Cslib.BitString.enum_eq_ofFn, Cslib.BitString.enumList_eq_ofFn: the enumeration lists the bit strings in the order of their numbers Cslib.BitString.equivFin.

References

Adapted from Crypto/Computational/GoldreichLevin/{Reduction,WordDecoder}.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.BitString.enum (k : ℕ) : List (BitString k)

Enumerate bitstrings by prepending each possible bit. This fixes an executable order.

@[simp]

theorem Cslib.BitString.mem_enum (k : ℕ) (guess : BitString k) : guess ∈ enum k

Every bit string is enumerated.

@[simp]

theorem Cslib.BitString.length_enum (k : ℕ) : (enum k).length = 2 ^ k

There are exactly 2 ^ k strings of k bits.

theorem Cslib.BitString.nodup_enum (k : ℕ) : (enum k).Nodup

Each bit string occurs exactly once.

def Cslib.BitString.enumList (count : ℕ) : List (List Bool)

The binary enumeration represented by ordinary lists, in the same order.

@[simp]

theorem Cslib.BitString.enumList_zero : enumList 0 = [[]]

The only word of length 0 is the empty list.

theorem Cslib.BitString.enumList_succ (count : ℕ) : enumList (count + 1) = List.flatMap (fun (word : List Bool) => [false :: word, true :: word]) (enumList count)

Extend every shorter string by both possible first bits.

@[simp]

theorem Cslib.BitString.length_enumList (count : ℕ) : (enumList count).length = 2 ^ count

The word enumeration has the same size as the finite-string enumeration.

theorem Cslib.BitString.countP_enumList (n : ℕ) (verdict : List Bool → Bool) : List.countP verdict (enumList n) = {word : BitString n | verdict (List.ofFn word) = true}.card

Counting an output predicate over the enumeration equals its finite witness cardinality.

theorem Cslib.BitString.length_of_mem_enumList {count : ℕ} {word : List Bool} (hword : word ∈ enumList count) : word.length = count

Every enumerated word has the requested width.

@[simp]

theorem Cslib.BitString.mem_enumList {count : ℕ} {word : List Bool} : word ∈ enumList count ↔ word.length = count

The ordinary-list enumeration contains exactly the words of the specified length.

theorem Cslib.BitString.enum_eq_ofFn (k : ℕ) : enum k = List.ofFn ⇑(equivFin k).symm

The enumeration is in the order of equivFin: binary order, least significant bit first.

theorem Cslib.BitString.enumList_eq_ofFn (k : ℕ) : enumList k = List.ofFn fun (i : Fin (2 ^ k)) => List.ofFn ((equivFin k).symm i)

The word enumeration lists the bits of the strings in the order of equivFin.