Algebraic operations on lists of bits

Finite bit strings and ordinary lists agree under pointwise XOR, Boolean dot products, basis vectors, subset sums and strict majority. List algorithms are total: an out-of-range basis index produces zeros, missing selectors are false, and pointwise XOR truncates to the shorter list. Collection XOR has a declared width and treats missing bits as false.

Main definitions

• Cslib.BitString.listStrictMajority: strict majority, returning false on a tie.
• Cslib.BitString.listNonpositiveMargin: compare correct votes with all votes.
• Cslib.BitString.listSingle, Cslib.BitString.listSingles: basis vectors in coordinate order.
• Cslib.BitString.listXorSelected: sum selected rows using an ordinary fold.
• Cslib.BitString.listXor: sum every row at a declared width, padding missing bits with false.

Main results

• Cslib.BitString.ofFn_add, Cslib.BitString.dotProduct_eq_foldl: algebraic representation laws.
• Cslib.BitString.listStrictMajority_map: a list with distinct voting indices agrees with finite-set strict majority.
• Cslib.BitString.listXorSelected_eq_ofFn_sum: the selector fold computes the finite mask sum.
• Cslib.BitString.listXor_eq_ofFn_sum: collection XOR computes the finite sum of padded views.

References

Adapted from Probability/WordBits.lean and Crypto/Computational/GoldreichLevin/WordDecoder.lean and Crypto/Computational/Pseudoentropy/Boosting/Vote.lean and Crypto/Computational/GeneratorXor.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.BitString.ofFn_add {n : ℕ} (left right : BitString n) : List.ofFn (left + right) = List.zipWith xor (List.ofFn left) (List.ofFn right)

Adding finite masks is exactly coordinatewise XOR of their word representations.

theorem Cslib.BitString.dotProduct_eq_foldl {n : ℕ} (left right : BitString n) : left ⬝ᵥ right = List.foldl xor false (List.zipWith and (List.ofFn left) (List.ofFn right))

A Boolean dot product is a pointwise AND followed by a parity fold on words.

def Cslib.BitString.listStrictMajority (votes : List Bool) : Bool

Strict majority of a word of votes, choosing false on a tie.

def Cslib.BitString.listNonpositiveMargin (votes : List Bool) (truth : Bool) : Bool

Whether the correct votes fail to form a strict majority. This test uses natural arithmetic.

theorem Cslib.BitString.listStrictMajority_eq_decide_count (votes : List Bool) : listStrictMajority votes = decide (votes.length < 2 * List.count true votes)

The existing strict-majority operation is equivalently a comparison of vote counts.

theorem Cslib.BitString.listStrictMajority_map {ι : Type} [DecidableEq ι] (indices : List ι) (hnodup : indices.Nodup) (vote : ι → Bool) : listStrictMajority (List.map vote indices) = strictMajorityOn indices.toFinset vote

Listing each voting index once gives exactly finite-set strict majority.

def Cslib.BitString.listSingle (dimension index : ℕ) : List Bool

A coordinate mask, with all zeros when the index is outside the requested dimension.

theorem Cslib.BitString.listSingle_eq_ofFn_single {n : ℕ} (index : Fin n) : listSingle n ↑index = List.ofFn (Pi.single index true)

The coordinate-mask program agrees with the finite basis vector.

def Cslib.BitString.listSingles (dimension : ℕ) : List (List Bool)

All coordinate queries in their ordinary increasing order.

theorem Cslib.BitString.listSingles_eq_ofFn (dimension : ℕ) : listSingles dimension = List.ofFn fun (index : Fin dimension) => List.ofFn (Pi.single index true)

The coordinate masks list the finite basis vectors in increasing index order.

def Cslib.BitString.listXorSelected (dimension : ℕ) (selector : List Bool) (rows : List (List Bool)) : List Bool

XOR the rows selected by a word of bits. Missing selector bits are false. The accumulator starts at the requested dimension; rows of that dimension preserve its length.

theorem Cslib.BitString.listXorSelected_eq_ofFn_sum {n k : ℕ} (selector : BitString k) (masks : Fin k → BitString n) : listXorSelected n (List.ofFn selector) (List.ofFn fun (i : Fin k) => List.ofFn (masks i)) = List.ofFn (∑ i : Fin k, if selector i = true then masks i else 0)

On finite masks, the selector fold is exactly the sum of the selected rows.

theorem Cslib.BitString.listXorSelected_eq_ofFn_sum_subset {n k : ℕ} (indices : Finset (Fin k)) (masks : Fin k → BitString n) : listXorSelected n (List.ofFn fun (i : Fin k) => decide (i ∈ indices)) (List.ofFn fun (i : Fin k) => List.ofFn (masks i)) = List.ofFn (∑ i ∈ indices, masks i)

Selecting the characteristic word of a finite subset computes its mask sum.

def Cslib.BitString.listXor (width : ℕ) (words : List (List Bool)) : List Bool

XOR a collection at the supplied width, treating missing bits as false.

@[simp]

theorem Cslib.BitString.length_listXor (width : ℕ) (words : List (List Bool)) : (listXor width words).length = width

The result has the declared width, also for an empty collection or short rows.

theorem Cslib.BitString.listXor_eq_ofFn_sum {count : ℕ} (width : ℕ) (words : Fin count → List Bool) : listXor width (List.ofFn words) = List.ofFn (∑ i : Fin count, ofList width (words i))

The list program agrees exactly with the sum of the finite bit-string views.

theorem Cslib.BitString.listXor_pair (m : ℕ) (u v : List Bool) : listXor m [u, v] = List.ofFn (ofList m u + ofList m v)

Two-word listXor agrees with addition in BitString m.

@[simp]

theorem Cslib.BitString.ofList_listXor_pair (m : ℕ) (u v : List Bool) : ofList m (listXor m [u, v]) = ofList m u + ofList m v

Fixed-width view of a two-word listXor.

theorem Cslib.BitString.listXor_pair_comm (m : ℕ) (u v : List Bool) : listXor m [u, v] = listXor m [v, u]

Two-word listXor is commutative.

theorem Cslib.BitString.getD_listXor_pair (m : ℕ) (u v : List Bool) (i : ℕ) (hi : i < m) : (listXor m [u, v]).getD i false = (u.getD i false ^^ v.getD i false)

Below the width m, each bit of a two-word listXor is the XOR of the corresponding bits of the words, with missing bits read as false.

theorem Cslib.BitString.getD_listRow_zero (m : ℕ) (u : List Bool) (i : ℕ) (hi : i < m) : (listRow m 0 u).getD i false = u.getD i false

Below the width m, row 0 of a word agrees bitwise with the word itself, with missing bits read as false.