Rejection sampling of a translated uniform distribution

Draw y uniformly from a finite set B of an additive group, shift it by v, and keep the result only if it lands in an acceptance set S; otherwise output none (an abort). When every accepted value z ∈ S has its preimage z - v in B, the output law does not depend on v at all: the sampler accepts with probability exactly |S| / |B|, and given acceptance its value is uniform on S (PMF.shiftReject_apply_some, PMF.shiftReject_apply_none). This is the exact, finite form of the rejection-sampling lemma behind Lyubashevsky's identification scheme and signatures ([Lyu09], [Lyu12]).

The box instance (PMF.boxReject) is the variant used in Dilithium ([DKL+18]): y is uniform in the integer box [-γ, γ]^ι and the shift v has sup norm at most β ≤ γ. The accepted values are then uniform on [-(γ - β), γ - β]^ι, the acceptance probability is exactly ((2 (γ - β) + 1) / (2 γ + 1)) ^ |ι|, and the abort probability is at most 2 |ι| β / (2 γ + 1). Unlike the discrete-Gaussian version, every statement is exact.

Main definitions

• Cslib.Probability.intBox: integer vectors with every coordinate in [-γ, γ].
• Cslib.Probability.PMF.shiftReject: rejection sampling of a translate of a uniform set.
• Cslib.Probability.PMF.boxReject: its instance for integer boxes.

Main results

• Cslib.Probability.PMF.shiftReject_apply_some, Cslib.Probability.PMF.shiftReject_apply_none: the exact law, whatever the shift.
• Cslib.Probability.PMF.shiftReject_eq: the law does not depend on the shift.
• Cslib.Probability.PMF.boxReject_apply_some, Cslib.Probability.PMF.boxReject_apply_none, Cslib.Probability.PMF.boxReject_eq: the same for boxes.
• Cslib.Probability.PMF.boxReject_apply_none_le: the abort probability is at most 2 |ι| β / (2 γ + 1).

References

• V. Lyubashevsky, Fiat-Shamir with Aborts: Applications to Lattice and Factoring-Based Signatures
• V. Lyubashevsky, Lattice Signatures without Trapdoors
• L. Ducas et al., CRYSTALS-Dilithium: A Lattice-Based Digital Signature Scheme

Integer boxes

def Cslib.Probability.intBox (ι : Type u_2) [Fintype ι] [DecidableEq ι] (γ : ℕ) : Finset (ι → ℤ)

The integer vectors whose coordinates all lie in [-γ, γ], that is, of sup norm at most γ.

@[simp]

theorem Cslib.Probability.mem_intBox {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ : ℕ} {z : ι → ℤ} : z ∈ intBox ι γ ↔ ∀ (i : ι), |z i| ≤ ↑γ

A vector lies in the box [-γ, γ]^ι when each coordinate has absolute value at most γ.

@[instance_reducible]

instance Cslib.Probability.instDecidablePredForallIntMemFinsetIntBox {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ : ℕ) : DecidablePred fun (x : ι → ℤ) => x ∈ intBox ι γ

Membership in a box is decided coordinate by coordinate.

theorem Cslib.Probability.zero_mem_intBox {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ : ℕ) : 0 ∈ intBox ι γ

Every box contains the zero vector.

theorem Cslib.Probability.intBox_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ : ℕ) : (intBox ι γ).Nonempty

Every box is nonempty, so it supports a uniform distribution.

theorem Cslib.Probability.card_intBox {ι : Type u_1} [Fintype ι] [DecidableEq ι] (γ : ℕ) : (intBox ι γ).card = (2 * γ + 1) ^ Fintype.card ι

The box [-γ, γ]^ι has (2 γ + 1) ^ |ι| points.

theorem Cslib.Probability.intBox_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ γ' : ℕ} (h : γ ≤ γ') : intBox ι γ ⊆ intBox ι γ'

Boxes grow with their radius.

theorem Cslib.Probability.sub_mem_intBox {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ℕ} (hβ : β ≤ γ) {z v : ι → ℤ} (hz : z ∈ intBox ι (γ - β)) (hv : v ∈ intBox ι β) : z - v ∈ intBox ι γ

Removing a vector of sup norm at most β from the inner box [-(γ - β), γ - β]^ι stays in the outer box [-γ, γ]^ι.

Rejection sampling of a translate

noncomputable def Cslib.Probability.PMF.shiftReject {α : Type u_1} [AddGroup α] [DecidableEq α] (B S : Finset α) (hB : B.Nonempty) (v : α) : PMF (Option α)

Rejection sampling of a translate: draw y uniformly from B, and output some (y + v) when y + v lies in the acceptance set S, and none (an abort) otherwise.

theorem Cslib.Probability.PMF.mem_of_some_mem_support_shiftReject {α : Type u_1} [AddGroup α] [DecidableEq α] {B S : Finset α} {hB : B.Nonempty} {v z : α} (h : some z ∈ (shiftReject B S hB v).support) : z ∈ S

Accepted values lie in the acceptance set.

theorem Cslib.Probability.PMF.shiftReject_apply_some {α : Type u_1} [AddGroup α] [DecidableEq α] {B S : Finset α} {hB : B.Nonempty} {v : α} (hv : ∀ z ∈ S, z - v ∈ B) (z : α) : (shiftReject B S hB v) (some z) = if z ∈ S then (↑B.card)⁻¹ else 0

Rejection sampling, accepted values. If every accepted value z ∈ S comes from some z - v ∈ B, then each z ∈ S is output with probability 1 / |B|, whatever the shift.

theorem Cslib.Probability.PMF.shiftReject_apply_none {α : Type u_1} [AddGroup α] [DecidableEq α] {B S : Finset α} {hB : B.Nonempty} {v : α} (hv : ∀ z ∈ S, z - v ∈ B) : (shiftReject B S hB v) none = 1 - ↑S.card / ↑B.card

Rejection sampling, aborts. Under the same hypothesis, the sampler aborts with probability exactly 1 - |S| / |B|, whatever the shift.

theorem Cslib.Probability.PMF.shiftReject_apply_some_eq_mul {α : Type u_1} [AddGroup α] [DecidableEq α] {B S : Finset α} {hB : B.Nonempty} {v : α} (hv : ∀ z ∈ S, z - v ∈ B) (hS : S.Nonempty) (z : α) : (shiftReject B S hB v) (some z) = ↑S.card / ↑B.card * (uniformOfFinset S hS) z

Rejection sampling lemma (exact form). Given acceptance, the output is uniform on S: the probability of some z is the acceptance probability |S| / |B| times the uniform probability of z in S.

theorem Cslib.Probability.PMF.shiftReject_eq {α : Type u_1} [AddGroup α] [DecidableEq α] {B S : Finset α} {hB : B.Nonempty} {v v' : α} (hv : ∀ z ∈ S, z - v ∈ B) (hv' : ∀ z ∈ S, z - v' ∈ B) : shiftReject B S hB v = shiftReject B S hB v'

The output law of rejection sampling is the same for all admissible shifts.

Rejection sampling in integer boxes

noncomputable def Cslib.Probability.PMF.boxReject (ι : Type u_2) [Fintype ι] [DecidableEq ι] (γ β : ℕ) (v : ι → ℤ) : PMF (Option (ι → ℤ))

Rejection sampling in integer boxes: draw y uniformly from [-γ, γ]^ι, and keep y + v only when it lies in [-(γ - β), γ - β]^ι.

theorem Cslib.Probability.PMF.boxReject_apply_some {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ℕ} {v : ι → ℤ} (hβ : β ≤ γ) (hv : v ∈ intBox ι β) (z : ι → ℤ) : (boxReject ι γ β v) (some z) = (↑(2 * (γ - β) + 1) / (2 * ↑γ + 1)) ^ Fintype.card ι * (uniformOfFinset (intBox ι (γ - β)) ⋯) z

Box rejection sampling, accepted values. If ‖v‖∞ ≤ β ≤ γ, the sampler accepts with probability ((2 (γ - β) + 1) / (2 γ + 1)) ^ |ι|, and given acceptance its value is uniform on [-(γ - β), γ - β]^ι, whatever v.

theorem Cslib.Probability.PMF.boxReject_apply_none {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ℕ} {v : ι → ℤ} (hβ : β ≤ γ) (hv : v ∈ intBox ι β) : (boxReject ι γ β v) none = 1 - (↑(2 * (γ - β) + 1) / (2 * ↑γ + 1)) ^ Fintype.card ι

Box rejection sampling, aborts. If ‖v‖∞ ≤ β ≤ γ, the sampler aborts with probability exactly 1 - ((2 (γ - β) + 1) / (2 γ + 1)) ^ |ι|.

theorem Cslib.Probability.PMF.boxReject_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ℕ} {v v' : ι → ℤ} (hβ : β ≤ γ) (hv : v ∈ intBox ι β) (hv' : v' ∈ intBox ι β) : boxReject ι γ β v = boxReject ι γ β v'

The law of box rejection sampling is the same for all shifts of sup norm at most β.

theorem Cslib.Probability.PMF.mem_intBox_of_some_mem_support_boxReject {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ℕ} {v z : ι → ℤ} (h : some z ∈ (boxReject ι γ β v).support) : z ∈ intBox ι (γ - β)

Accepted values lie in the inner box.

theorem Cslib.Probability.PMF.boxReject_apply_none_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {γ β : ℕ} {v : ι → ℤ} (hβ : β ≤ γ) (hv : v ∈ intBox ι β) : (boxReject ι γ β v) none ≤ 2 * ↑(Fintype.card ι) * ↑β / (2 * ↑γ + 1)

Abort bound. If ‖v‖∞ ≤ β ≤ γ, the sampler aborts with probability at most 2 |ι| β / (2 γ + 1), by Bernoulli's inequality.