Bit strings represented by lists

Fixed-width views of ordinary lists pad missing bits with false. A flat list can also be read as a specified number of fixed-width rows. The representation uses the existing blocksEquiv; row extraction is ordinary dropping, padding and taking, including on short or empty lists.

Main definitions

• Cslib.BitString.ofList: a fixed-width view of a list.
• Cslib.BitString.listRow, Cslib.BitString.listRows: fixed-width rows of a flat list.

Main results

• Cslib.BitString.ofList_ofFn, Cslib.BitString.ofFn_ofList: representation round trips.
• Cslib.BitString.ofList_append_of_le, Cslib.BitString.ofList_ofFn_append: fixed-width views ignore bits beyond their width.
• Cslib.BitString.ofFn_eq_append: a string is its prefix followed by its suffix.
• Cslib.BitString.exists_take_ofFn_iff, Cslib.BitString.forall_take_ofFn_iff: quantifying over longer strings through their prefixes.
• Cslib.BitString.ofFn_ofList_eq_take: the fixed-width view pads with false or truncates.
• Cslib.BitString.getElem_listRow, Cslib.BitString.getD_listRow: row indexing, including false padding on short words.
• Cslib.BitString.listRow_flatMap_append, Cslib.BitString.listRow_flatten: recover equal-width rows from concatenated words.
• Cslib.BitString.listRows_eq_ofFn, Cslib.BitString.listRows_ofFn: agreement with the finite block representation.
• Cslib.BitString.listRows_succ_append: the rows of a word whose first row is given.
• Cslib.BitString.ofFn_blocksEquiv_symm: packing fixed-width rows is list concatenation.

References

Adapted from Probability/WordBits.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the shared bit-string block equivalence.

def Cslib.BitString.ofList (n : ℕ) (word : List Bool) : BitString n

View a list as n bits, padding missing bits with false.

@[simp]

theorem Cslib.BitString.ofList_ofFn {n : ℕ} (bits : BitString n) : ofList n (List.ofFn bits) = bits

Viewing List.ofFn bits as an n-bit string recovers bits.

theorem Cslib.BitString.ofFn_ofList {n : ℕ} {word : List Bool} (hlen : word.length = n) : List.ofFn (ofList n word) = word

A list of the declared width loses no data through the finite representation.

theorem Cslib.BitString.ofList_append {n m : ℕ} {u v : List Bool} (hu : u.length = n) (hv : v.length = m) : ofList (n + m) (u ++ v) = Fin.append (ofList n u) (ofList m v)

Concatenating words of the declared widths agrees with concatenating their bit strings.

theorem Cslib.BitString.ofFn_eq_append {k j : ℕ} (y : BitString (k + j)) : List.ofFn y = List.ofFn ((Fin.appendEquiv k j).symm y).1 ++ List.ofFn ((Fin.appendEquiv k j).symm y).2

A string of k + j bits is its first k bits followed by its last j bits.

theorem Cslib.BitString.ofList_append_of_le {n : ℕ} {u : List Bool} (hu : n ≤ u.length) (v : List Bool) : ofList n (u ++ v) = ofList n u

The fixed-width view of a word does not see bits beyond its width.

theorem Cslib.BitString.ofList_ofFn_append {n : ℕ} (bits : BitString n) (word : List Bool) : ofList n (List.ofFn bits ++ word) = bits

Reading n bits of a word that starts with n given bits returns them.

theorem Cslib.BitString.ofFn_ofList_eq_take (n : ℕ) (word : List Bool) : List.ofFn (ofList n word) = List.take n (word ++ List.replicate n false)

Reading a word into a bit string pads it with false or truncates it.

theorem Cslib.BitString.take_ofFn_ofList {k K : ℕ} (h : k ≤ K) (y : BitString k) : List.take k (List.ofFn (ofList K (List.ofFn y))) = List.ofFn y

A string of k ≤ K bits padded with false to K bits has the original string as its prefix of length k.

theorem Cslib.BitString.exists_take_ofFn_iff {k K : ℕ} (h : k ≤ K) {g : List Bool → Prop} : (∃ (y : BitString K), g (List.take k (List.ofFn y))) ↔ ∃ (y : BitString k), g (List.ofFn y)

Prefixes and existential quantifiers. For k ≤ K, some string of K bits has a prefix of length k satisfying g iff some string of k bits does.

theorem Cslib.BitString.forall_take_ofFn_iff {k K : ℕ} (h : k ≤ K) {g : List Bool → Prop} : (∀ (y : BitString K), g (List.take k (List.ofFn y))) ↔ ∀ (y : BitString k), g (List.ofFn y)

Prefixes and universal quantifiers. For k ≤ K, every string of K bits has a prefix of length k satisfying g iff every string of k bits does.

theorem Cslib.BitString.ofFn_blocksEquiv_symm {count width : ℕ} (rows : Fin count → BitString width) : List.ofFn (blocksEquiv.symm rows) = (List.ofFn fun (i : Fin count) => List.ofFn (rows i)).flatten

Packing fixed-width rows in the block representation is ordinary list concatenation.

theorem Cslib.BitString.block_ofList_prefix {count rows width : ℕ} (h : rows ≤ count) (word : List Bool) : (ofList (rows * width) word).block = (ofList (count * width) word).block ∘ Fin.castLE h

Reading fewer rows agrees with restricting the longer fixed-width view.

def Cslib.BitString.listRow (width row : ℕ) (word : List Bool) : List Bool

Read one fixed-width row, using false beyond the end of the supplied list.

@[simp]

theorem Cslib.BitString.length_listRow (width row : ℕ) (word : List Bool) : (listRow width row word).length = width

Every extracted row has length width.

theorem Cslib.BitString.getElem_listRow {width row i : ℕ} {word : List Bool} (hi : i < width) : (listRow width row word)[i] = word.getD (row * width + i) false

Entry i of row row is bit row * width + i of the word, or false beyond its end.

theorem Cslib.BitString.getD_listRow {width row i : ℕ} {word : List Bool} (hi : i < width) : (listRow width row word).getD i false = word.getD (row * width + i) false

Below the row width, defaulted indexing reads the corresponding word bit, even when the word is too short and the row is padded with false.

theorem Cslib.BitString.listRow_zero (width : ℕ) (word : List Bool) : listRow width 0 word = List.ofFn (ofList width word)

Row zero is the fixed-width view of the word.

theorem Cslib.BitString.listRow_flatMap_append {α : Type u_1} {width : ℕ} (f : α → List Bool) (l : List α) (hf : ∀ a ∈ l, (f a).length = width) (rest : List Bool) (j : ℕ) (hj : j < l.length) : listRow width j (List.flatMap f l ++ rest) = f l[j]

Reading an existing row from concatenated equal-width words recovers that row, regardless of the appended suffix. Width zero is allowed.

theorem Cslib.BitString.listRow_flatten {width : ℕ} {words : List (List Bool)} (hwords : ∀ w ∈ words, w.length = width) {i : ℕ} (hi : i < words.length) : listRow width i words.flatten = words.getD i []

Reading an existing row of a flattened list of equal-width words recovers that word.

theorem Cslib.BitString.listRow_eq_ofFn {count : ℕ} (width : ℕ) (row : Fin count) (word : List Bool) : listRow width (↑row) word = List.ofFn ((ofList (count * width) word).block row)

List slicing agrees with the finite block representation, even on short input lists.

def Cslib.BitString.listRows (count width : ℕ) (word : List Bool) : List (List Bool)

Read a specified number of rows, retaining empty rows when the width is zero.

@[simp]

theorem Cslib.BitString.length_listRows (count width : ℕ) (word : List Bool) : (listRows count width word).length = count

Extracting count rows produces a list of length count.

theorem Cslib.BitString.length_of_mem_listRows {count width : ℕ} {word row : List Bool} (hrow : row ∈ listRows count width word) : row.length = width

Every extracted row has the declared width.

theorem Cslib.BitString.listRows_eq_ofFn (count width : ℕ) (word : List Bool) : listRows count width word = List.ofFn fun (row : Fin count) => List.ofFn ((ofList (count * width) word).block row)

Extracting rows gives the list representation of the existing finite block view.

theorem Cslib.BitString.listRows_ofFn {k m : ℕ} (x : BitString (k * m)) : listRows k m (List.ofFn x) = List.ofFn fun (i : Fin k) => List.ofFn (x.block i)

The rows of a word of k * m bits are its blocks.

theorem Cslib.BitString.listRows_succ_append (count width : ℕ) {u : List Bool} (hu : u.length = width) (v : List Bool) : listRows (count + 1) width (u ++ v) = u :: listRows count width v

The rows of a word starting with a full row u are u followed by the rows of the rest.