Finite sampling for the GSW construction

Residues are sampled from exactly w fair bits. Each integer error is the difference of two independent counts of η fair bits, so every supported error has magnitude at most η. The actual key-generation and encryption programs feed these independent draws to the GSW formulas. Their correctness holds for every supported draw under an explicit strict margin.

This exact noise distribution is a construction choice. No Gaussian equivalence, LWE hardness, encryption security, complete native algorithm certificate or bootstrappability is asserted.

Main definitions

• sampleResidue, sampleVector, sampleMatrix, sampleCoins: independent finite samplers.
• KeyInputs, sampleKeyInputs: the independent inputs to the public-key formula.
• keyGen, encrypt: the actual finite randomized key generation and encryption programs.

Main results

• eval_sampleResidue, eval_sampleVector, eval_sampleMatrix, eval_sampleCoins: exact uniform laws.
• mem_support_sampleKeyInputs_iff: the exact support condition on the chosen integer errors.
• keyGen_encrypt_correct, keyGen_nand_correct: correctness for all supported draws.

References

• C. Gentry, A. Sahai and B. Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based, Section 3.1
• NIST, Module-Lattice-Based Key-Encapsulation Mechanism Standard, Algorithm 8 for the scalar finite noise construction, without identifying the encryption schemes.

noncomputable def Cslib.Crypto.Homomorphic.GSW.sampleResidue (w : ℕ) : ProbComp (ZMod (2 ^ w))

Sample one residue from w independent fair bits.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.eval_sampleResidue (w : ℕ) : (sampleResidue w).eval = Probability.PMF.uniformOfFintype (ZMod (2 ^ w))

The fair-bit residue sampler is exactly uniform, including at width zero.

noncomputable def Cslib.Crypto.Homomorphic.GSW.sampleVector (count w : ℕ) : ProbComp (Fin count → ZMod (2 ^ w))

Sample independent residues into a length-indexed vector.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.eval_sampleVector (count w : ℕ) : (sampleVector count w).eval = Probability.PMF.uniformOfFintype (Fin count → ZMod (2 ^ w))

noncomputable def Cslib.Crypto.Homomorphic.GSW.sampleMatrix (rows cols w : ℕ) : ProbComp (Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w)))

Sample independent rows of independent residues.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.eval_sampleMatrix (rows cols w : ℕ) : (sampleMatrix rows cols w).eval = Probability.PMF.uniformOfFintype (Matrix (Fin rows) (Fin cols) (ZMod (2 ^ w)))

noncomputable def Cslib.Crypto.Homomorphic.GSW.sampleCoins (n m w : ℕ) : ProbComp (Matrix (Fin (n + 1) × Fin w) (Fin m) Bool)

Sample every entry of the binary encryption matrix independently.

@[simp]

theorem Cslib.Crypto.Homomorphic.GSW.eval_sampleCoins (n m w : ℕ) : (sampleCoins n m w).eval = Probability.PMF.uniformOfFintype (Matrix (Fin (n + 1) × Fin w) (Fin m) Bool)

structure Cslib.Crypto.Homomorphic.GSW.KeyInputs (n m w : ℕ) : Type

The separately sampled secret, public-matrix part and integer errors.

• secret : Fin n → ZMod (2 ^ w)

  Uniform secret entries.

• publicPart : Matrix (Fin m) (Fin n) (ZMod (2 ^ w))

  Uniform public matrix entries.

• error : Fin m → ℤ

  Independent bounded integer errors.

noncomputable def Cslib.Crypto.Homomorphic.GSW.sampleKeyInputs (n m w η : ℕ) : ProbComp (KeyInputs n m w)

Draw the three inputs independently, using the specified finite error distribution.

theorem Cslib.Crypto.Homomorphic.GSW.eval_sampleKeyInputs (n m w η : ℕ) : (sampleKeyInputs n m w η).eval = do let secret ← Probability.PMF.uniformOfFintype (Fin n → ZMod (2 ^ w)) let publicPart ← Probability.PMF.uniformOfFintype (Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) let error ← ProbComp.eval (OracleComp.replicateFin m (Probability.sampleCenteredBinomial η)) pure { secret := secret, publicPart := publicPart, error := error }

The complete joint law retains the independence of the secret, public part and errors.

theorem Cslib.Crypto.Homomorphic.GSW.mem_support_sampleKeyInputs_iff (n m w η : ℕ) (inputs : KeyInputs n m w) : inputs ∈ (sampleKeyInputs n m w η).eval.support ↔ ∀ (i : Fin m), (inputs.error i).natAbs ≤ η

Every secret and public part is possible; the exact error restriction is coordinatewise.

noncomputable def Cslib.Crypto.Homomorphic.GSW.keyGen (n m w η : ℕ) : ProbComp (Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) × (Fin n → ZMod (2 ^ w)))

Generate the actual public matrix and retain the sampled secret.

noncomputable def Cslib.Crypto.Homomorphic.GSW.encrypt {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) (μ : Bool) : ProbComp (Ciphertext n w)

Encrypt a Boolean message using only the public matrix and independently sampled coins.

theorem Cslib.Crypto.Homomorphic.GSW.mem_support_encrypt_iff {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) (μ : Bool) (C : Ciphertext n w) : C ∈ (encrypt A μ).eval.support ↔ ∃ (coins : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool), encryptWithCoins A μ coins = C

A supported ciphertext is precisely an encryption with some binary coin matrix.

theorem Cslib.Crypto.Homomorphic.GSW.keyGen_encrypt_correct {n m w η : ℕ} (hw : 0 < w) (hmargin : 4 * (m * η) < 2 ^ w) {keys : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) × (Fin n → ZMod (2 ^ w))} (hkeys : keys ∈ (keyGen n m w η).eval.support) (μ : Bool) {C : Ciphertext n w} (hC : C ∈ (encrypt keys.1 μ).eval.support) : decrypt keys.2 C = μ

Every generated key and every supported fresh ciphertext are correct under the strict margin.

theorem Cslib.Crypto.Homomorphic.GSW.keyGen_nand_correct {n m w η : ℕ} (hw : 0 < w) (hmargin : 4 * ((1 + (n + 1) * w) * (m * η)) < 2 ^ w) {keys : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w)) × (Fin n → ZMod (2 ^ w))} (hkeys : keys ∈ (keyGen n m w η).eval.support) (μ₁ μ₂ : Bool) {C₁ C₂ : Ciphertext n w} (hC₁ : C₁ ∈ (encrypt keys.1 μ₁).eval.support) (hC₂ : C₂ ∈ (encrypt keys.1 μ₂).eval.support) : decrypt keys.2 (nand C₁ C₂) = !(μ₁ && μ₂)

NAND of any two supported fresh ciphertexts is correct for every generated key.