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_replaceRow: replacing one row with an independent uniform row preserves uniformity.
• Cslib.BitString.uniformList_map_listXor, Cslib.BitString.uniformList_map_listXor_length, Cslib.BitString.uniformList_map_zipWith_xor, Cslib.BitString.uniformList_map_take_zipWith_xor: XOR with a fixed word preserves uniformity (both in listXor m [y, r] and direct List.zipWith Bool.xor y r forms).

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) => block (ofList (count * width) word)) (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; see uniformList_map_zipWith_xor and uniformList_map_take_zipWith_xor for the direct List.zipWith Bool.xor y r form alongside listXor m [y, r].

theorem Cslib.BitString.uniformList_map_zipWith_xor (msg : List Bool) : PMF.map (fun (pad : List Bool) => List.zipWith xor pad msg) (uniformList msg.length) = uniformList msg.length

Pointwise List.zipWith Bool.xor of a uniform msg.length-bit word with a fixed word msg preserves uniformList msg.length (the direct List.zipWith Bool.xor y r counterpart to uniformList_map_listXor's listXor m [y, r]).

theorem Cslib.BitString.uniformList_map_take_zipWith_xor {n : ℕ} {msg : List Bool} (hmsg : msg.length = n) : PMF.map (fun (pad : List Bool) => List.zipWith xor (List.take n pad) msg) (uniformList n) = uniformList n

Pointwise List.zipWith Bool.xor of pad.take n for a uniform n-bit word pad with an n-bit word msg preserves uniformList n.

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

XORing a uniform m-bit word pad with any word r at width pad.length preserves the uniform distribution uniformList m.

theorem Cslib.BitString.uniformList_replaceRow (width count : ℕ) (j : Fin count) : ((uniformList width).bind fun (x : List Bool) => PMF.map (replaceRow width count (↑j) x) (uniformList (count * width))) = uniformList (count * width)

Replacing row j < count of a uniform count * width-bit string with an independent uniform width-bit string preserves the uniform distribution uniformList (count * width).