Documentation

CslibFrontier.Foundations.Data.BitString.List

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 #

Main results #

Packing fixed-width rows is list concatenation by Cslib.BitString.ofFn_blocksEquiv_symm, in CslibFrontier.Foundations.Data.BitString.Block.

References #

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

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

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

Instances For
    source
    @[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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    theorem Cslib.BitString.ofList_take (n : ℕ) (word : List Bool) :
    ofList n (List.take n word) = ofList n word

    The n-bit view of a word reads only its first n bits.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

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

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

    source
    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.

    Instances For
      source
      @[simp]
      theorem Cslib.BitString.length_listRow (width row : ℕ) (word : List Bool) :
      (listRow width row word).length = width

      Every extracted row has length width.

      source
      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.

      source
      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.

      source
      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.

      source
      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.

      source
      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.

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

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

      source
      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.

      Instances For
        source
        @[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.

        source
        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.

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

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

        source
        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 (block x i)

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

        source
        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.

        source
        def Cslib.BitString.replaceRow (width count j : ℕ) (x word : List Bool) :
        List Bool

        Replace row j of a count × width bit string word with x.

        Instances For
          source
          theorem Cslib.BitString.listRow_replaceRow {width count j : ℕ} {x : List Bool} (hx : x.length = width) (word : List Bool) {i : ℕ} (hi : i < count) :
          listRow width i (replaceRow width count j x word) = if i = j then x else listRow width i word

          Reading row i < count from replaceRow width count j x word returns x when i = j and listRow width i word otherwise.