Probability lemmas for uniform BitVec sampling

Lemmas about probOutput for ProbComp (BitVec n) computations involving XOR with uniformly sampled keys. These are reusable building blocks for encryption proofs (e.g., one-time pad privacy).

theorem probOutput_xor_uniform (sp : ℕ) (msg σ : BitVec sp) : Pr[= σ | (fun (k : BitVec sp) => k ^^^ msg) <$> ($ᵗ BitVec sp)] = (↑(Fintype.card (BitVec sp)))⁻¹

theorem probOutput_pair_xor_uniform (sp : ℕ) (mx : ProbComp (BitVec sp)) (msg σ : BitVec sp) : Pr[= (msg, σ) | do let msg' ← mx let k ← $ᵗ BitVec sp pure (msg', k ^^^ msg')] = Pr[= msg | mx] * (↑(Fintype.card (BitVec sp)))⁻¹

theorem probOutput_cipher_from_pair_uniform (sp : ℕ) (mx : ProbComp (BitVec sp)) (σ : BitVec sp) : Pr[= σ | do let msg' ← mx let k ← $ᵗ BitVec sp pure (k ^^^ msg')] = (↑(Fintype.card (BitVec sp)))⁻¹