Independent blocks of uniform bit lists

Reading a uniform list of count * width bits as fixed-width rows gives exactly count independent uniform bit strings. This includes zero-width rows and zero rows.

Main results

• Cslib.BitString.uniformList_ofList: a uniform list gives a uniform finite bit string.
• Cslib.BitString.uniformList_blocks: fixed-width blocks are jointly uniform.
• Cslib.BitString.uniformList_listRows: the same law for the ordinary list-of-lists program.
• Cslib.BitString.uniformList_map_listXor: XOR with a fixed word preserves uniformity.

References

Adapted from Probability/WordBits.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared block representation.

theorem Cslib.BitString.uniformList_ofList (n : ℕ) : PMF.map (ofList n) (uniformList n) = Probability.PMF.uniformOfFintype (BitString n)

A uniform list gives exactly a uniform finite bit string.

theorem Cslib.BitString.uniformList_blocks (count width : ℕ) : PMF.map (fun (word : List Bool) => (ofList (count * width) word).block) (uniformList (count * width)) = Probability.PMF.uniformOfFintype (Fin count → BitString width)

Disjoint fixed-width blocks of a uniform list are jointly uniform.

theorem Cslib.BitString.uniformList_listRows (count width : ℕ) : PMF.map (listRows count width) (uniformList (count * width)) = PMF.map (fun (rows : Fin count → BitString width) => List.ofFn fun (i : Fin count) => List.ofFn (rows i)) (Probability.PMF.uniformOfFintype (Fin count → BitString width))

Extracting fixed-width rows realizes the joint law of independent uniform seeds.

theorem Cslib.BitString.uniformList_map_listXor (m : ℕ) (r : List Bool) : PMF.map (fun (y : List Bool) => listXor m [y, r]) (uniformList m) = uniformList m

XORing a uniform m-bit word with any word r preserves the uniform distribution.