The centered binomial distribution and sign independence

cbd η is the difference of two independent Binomial η 1/2 counts: the noise distribution of ML-KEM, sampled over ℤ. It is not a uniform distribution, and ℤ carries no Fintype instance, so SPComp.sample cannot name a program that draws from it and liftR_uniform_bij cannot relate two such draws. sampleFrom and rHoare_coupling_step can.

The relational content is that cbd η is symmetric under negation, so the sign applied to a noise term is unobservable: cbd_signed_indep states that for a secret sign s, the program e ← cbd η; k ((-1)^s * e) has the same behaviour for both values of s.

Main definitions

• binom n — the number of successes in n fair coin flips
• cbd η — the centered binomial distribution Binomial η 1/2 - Binomial η 1/2
• signed s e — -e when s, else e

Main results

• bind_apply_ne_zero — a bind hits every value its two stages reach
• mass_cbd, isLossless_sampleFrom_cbd — cbd η is a total distribution
• cbd_one_ne_pure — cbd 1 has at least two support points, so the example is not a point mass in disguise
• cbd_symm — cbd η is invariant under negation
• rHoare_cbd_signed — the pRHL sampling step from that invariance
• cbd_signed_indep — a secret sign on the noise term is unobservable
• prTrue_cbd_bind — the unary averaging rule at cbd η

Support of a bind

theorem CatCrypt.NonUniform.bind_apply_ne_zero {α : Type u_1} {β : Type u_2} {d : Prob.SDistr α} {f : α → Prob.SDistr β} {a : α} {b : β} (ha : d (some a) ≠ 0) (hb : (f a) (some b) ≠ 0) : (d.bind f) (some b) ≠ 0

A bind hits b whenever some intermediate a is in the support of d and b is in the support of f a. Converse of SDistr.bind_support_witness.

The distributions

noncomputable def CatCrypt.NonUniform.binom : ℕ → Prob.SDistr ℕ

The number of successes in n fair coin flips.

Equations

• One or more equations did not get rendered due to their size.
• CatCrypt.NonUniform.binom 0 = CatCrypt.Prob.SDistr.pure 0

theorem CatCrypt.NonUniform.binom_zero : binom 0 = Prob.SDistr.pure 0

theorem CatCrypt.NonUniform.binom_succ (n : ℕ) : binom (n + 1) = (binom n).bind fun (k : ℕ) => (Prob.SDistr.uniform Bool).bind fun (b : Bool) => Prob.SDistr.pure (k + if b = true then 1 else 0)

noncomputable def CatCrypt.NonUniform.cbd (η : ℕ) : Prob.SDistr ℤ

The centered binomial distribution: the difference of two independent binom η counts.

Equations

• CatCrypt.NonUniform.cbd η = (CatCrypt.NonUniform.binom η).bind fun (a : ℕ) => (CatCrypt.NonUniform.binom η).bind fun (b : ℕ) => CatCrypt.Prob.SDistr.pure (↑a - ↑b)

@[simp]

theorem CatCrypt.NonUniform.mass_binom (n : ℕ) : (binom n).mass = 1

@[simp]

theorem CatCrypt.NonUniform.mass_cbd (η : ℕ) : (cbd η).mass = 1

theorem CatCrypt.NonUniform.isLossless_sampleFrom_cbd (η : ℕ) : Unary.isLossless (sampleFrom (cbd η))

Drawing centered binomial noise never fails.

Non-degeneracy

cbd 1 puts mass on both 0 and 1, so it is not a point mass; and ℤ has no uniform distribution, so the example is not a uniform draw under another name.

theorem CatCrypt.NonUniform.binom_one_apply_zero : (binom 1) (some 0) ≠ 0

theorem CatCrypt.NonUniform.binom_one_apply_one : (binom 1) (some 1) ≠ 0

theorem CatCrypt.NonUniform.cbd_one_apply_zero : (cbd 1) (some 0) ≠ 0

theorem CatCrypt.NonUniform.cbd_one_apply_one : (cbd 1) (some 1) ≠ 0

theorem CatCrypt.NonUniform.cbd_one_ne_pure (z : ℤ) : cbd 1 ≠ Prob.SDistr.pure z

cbd 1 is not a point mass: 0 and 1 are both in its support.

Symmetry under negation

theorem CatCrypt.NonUniform.cbd_symm (η : ℕ) : ((cbd η).bind fun (z : ℤ) => Prob.SDistr.pure (-z)) = cbd η

cbd η is invariant under negation: negating the difference of the two counts exchanges them, and the two counts are independent and identically distributed.

def CatCrypt.NonUniform.signed (s : Bool) (e : ℤ) : ℤ

Apply a sign to a noise term: signed true negates, signed false is the identity.

Equations

• CatCrypt.NonUniform.signed s e = if s = true then -e else e

theorem CatCrypt.NonUniform.cbd_pushforward_signed (η : ℕ) (s : Bool) : ((cbd η).bind fun (e : ℤ) => Prob.SDistr.pure (signed s e)) = cbd η

The pushforward of cbd η along either sign is cbd η.

theorem CatCrypt.NonUniform.liftR_cbd_signed (η : ℕ) (s : Bool) : cbd η ⟨fun (a b : ℤ) => signed s a = b⟩# cbd η

The coupling of cbd η with itself along a sign.

The pRHL step and sign independence

theorem CatCrypt.NonUniform.rHoare_cbd_sign {γ : Type u_3} {δ : Type u_4} {Φ : Relational.RPre} {Ψ : Relational.RPost γ δ} (η : ℕ) (s : Bool) {k₁ : ℤ → Core.SPComp γ} {k₂ : ℤ → Core.SPComp δ} (h : ∀ (e : ℤ), Relational.rHoare Φ (k₁ e) (k₂ (signed s e)) Ψ) : Relational.rHoare Φ ((sampleFrom (cbd η)).bind k₁) ((sampleFrom (cbd η)).bind k₂) Ψ

pRHL sampling step for centered binomial noise under a sign: a draw on the left is matched by the sign-flipped draw on the right.

theorem CatCrypt.NonUniform.cbd_signed_eq {α : Type u_1} (η : ℕ) (s : Bool) (k : ℤ → Core.SPComp α) : ((sampleFrom (cbd η)).bind fun (e : ℤ) => k (signed s e)) = (sampleFrom (cbd η)).bind k

Applying a sign to the noise term does not change the program.

theorem CatCrypt.NonUniform.cbd_signed_indep {α : Type u_1} (η : ℕ) (k : ℤ → Core.SPComp α) (s₁ s₂ : Bool) : ((sampleFrom (cbd η)).bind fun (e : ℤ) => k (signed s₁ e)) = (sampleFrom (cbd η)).bind fun (e : ℤ) => k (signed s₂ e)

The sign of a centered binomial noise term is unobservable: the program is the same for both secret signs.

The unary rule at cbd

theorem CatCrypt.NonUniform.prTrue_cbd_bind (η : ℕ) (k : ℤ → Core.SPComp Bool) (h₀ : Core.Heap) : Crypto.prTrue ((sampleFrom (cbd η)).bind k) h₀ = ∑' (e : ℤ), (cbd η) (some e) * Crypto.prTrue (k e) h₀

Success probability of a Boolean game that starts with centered binomial noise, as the cbd η-average of the branch probabilities.