The deterministic GSW encryption core

This module constructs the actual public matrix, encryption with explicit binary coins, and NAND operation of Gentry, Sahai and Waters. The modulus is 2 ^ w, with w digits per secret coordinate and N = (n + 1) * w ciphertext rows and columns. As documented in GSW.Gadget, this omits the paper's redundant top digit at this modulus. Ciphertexts are Boolean matrices, so encryption and NAND preserve their dimensions and binary entry invariant by construction. Integer errors witness the modular approximate-eigenvector equations; their magnitudes are bounded separately.

The inputs to key construction and encryption are explicit. No distribution, computational security, native complexity bound, admissible parameter family or bootstrappability theorem is asserted here. In particular, the pointwise error bounds do not follow merely from a negligible probability of excessive noise.

Main definitions

• Ciphertext, secretVector, publicMatrix: the bit-matrix ciphertext and actual key formulas.
• encryptWithCoins, nand, decrypt: the actual deterministic algorithms.
• HasError: the modular equation witnessed by an explicit integer error vector.

Main results

• encryptWithCoins_hasError: the encryption error is the integer subset sum R * error.
• recomposeMatrix_encryptWithCoins: the public ciphertext recomposes to μ * G + R * A.
• encryptWithCoins_eq_decomposeMatrix: the ciphertext is the bit decomposition of that matrix.
• nand_hasError: the actual NAND operation has the stated propagated integer error.
• decrypt_eq_of_hasError: the decoder recovers a bit below its explicit noise threshold.
• decrypt_encryptWithCoins, decrypt_nand: correctness from input noise bounds.

References

• [C. Gentry, A. Sahai and B. Waters, Homomorphic Encryption from Learning with Errors: Conceptually-Simpler, Asymptotically-Faster, Attribute-Based, Sections 3.1--3.4] [GSW13]

@[reducible, inline]

abbrev Cslib.Crypto.Homomorphic.GSW.Ciphertext (n w : ℕ) : Type

A square Boolean ciphertext with (n + 1) * w rows and columns.

def Cslib.Crypto.Homomorphic.GSW.secretVector {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) : Fin (n + 1) → ZMod (2 ^ w)

The secret vector has leading coordinate one, followed by the negated secret entries.

def Cslib.Crypto.Homomorphic.GSW.publicMatrix {n m w : ℕ} (B : Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) (t : Fin n → ZMod (2 ^ w)) (error : Fin m → ℤ) : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))

The public matrix is [B * t + error | B], with integer errors cast modulo 2 ^ w.

theorem Cslib.Crypto.Homomorphic.GSW.publicMatrix_mulVec_secretVector {n m w : ℕ} (B : Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) (t : Fin n → ZMod (2 ^ w)) (error : Fin m → ℤ) : (publicMatrix B t error).mulVec (secretVector t) = fun (i : Fin m) => ↑(error i)

The constructed public matrix has exactly the chosen error against the secret vector.

def Cslib.Crypto.Homomorphic.GSW.gadgetMatrix (n w : ℕ) : Matrix (Fin (n + 1) × Fin w) (Fin (n + 1)) (ZMod (2 ^ w))

The public gadget matrix obtained by recomposing the identity.

theorem Cslib.Crypto.Homomorphic.GSW.gadgetMatrix_apply {n w : ℕ} (i : Fin (n + 1)) (k : Fin w) (j : Fin (n + 1)) : gadgetMatrix n w (i, k) j = if i = j then 2 ^ ↑k else 0

A gadget row contains its binary place value at its original coordinate and zero elsewhere.

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

Encrypt using only the public matrix, the Boolean message, and binary coins.

theorem Cslib.Crypto.Homomorphic.GSW.encryptWithCoins_eq_decomposeMatrix {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) (μ : Bool) (R : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) : encryptWithCoins A μ R = decomposeMatrix w (↑μ.toNat • gadgetMatrix n w + bitMatrix (ZMod (2 ^ w)) R * A)

The actual ciphertext is the canonical decomposition of its message shift and subset sums.

def Cslib.Crypto.Homomorphic.GSW.nand {n w : ℕ} (C₁ C₂ : Ciphertext n w) : Ciphertext n w

Homomorphic NAND, with dimensions and binary output entries preserved structurally.

def Cslib.Crypto.Homomorphic.GSW.HasError {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) (μ : Bool) (error : Fin (n + 1) × Fin w → ℤ) : Prop

The ciphertext's modular product equals the encoded message plus an explicit integer error. This relation does not impose a size bound on the error.

def Cslib.Crypto.Homomorphic.GSW.decrypt {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) : Bool

Decode the highest digit of the leading secret coordinate. Width zero returns false.

theorem Cslib.Crypto.Homomorphic.GSW.recomposeMatrix_encryptWithCoins {n m w : ℕ} (A : Matrix (Fin m) (Fin (n + 1)) (ZMod (2 ^ w))) (μ : Bool) (R : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) : recomposeMatrix w (bitMatrix (ZMod (2 ^ w)) (encryptWithCoins A μ R)) = ↑μ.toNat • gadgetMatrix n w + bitMatrix (ZMod (2 ^ w)) R * A

Recomposition exposes the exact public form used by the later security reduction.

theorem Cslib.Crypto.Homomorphic.GSW.encryptWithCoins_hasError {n m w : ℕ} (B : Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) (t : Fin n → ZMod (2 ^ w)) (error : Fin m → ℤ) (μ : Bool) (R : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) : HasError t (encryptWithCoins (publicMatrix B t error) μ R) μ (encryptionError R error)

Encryption with the actual public key has the exact integer error selected by its coins.

theorem Cslib.Crypto.Homomorphic.GSW.nand_hasError {n w : ℕ} (t : Fin n → ZMod (2 ^ w)) (C₁ C₂ : Ciphertext n w) (μ₁ μ₂ : Bool) (error₁ error₂ : Fin (n + 1) × Fin w → ℤ) (hC₁ : HasError t C₁ μ₁ error₁) (hC₂ : HasError t C₂ μ₂ error₂) : HasError t (nand C₁ C₂) (!(μ₁ && μ₂)) (nandError C₁ μ₂ error₁ error₂)

The actual NAND formula has error -μ₂ * error₁ - C₁ * error₂ over the integers.

theorem Cslib.Crypto.Homomorphic.GSW.decrypt_eq_of_hasError {n w : ℕ} (hw : 0 < w) (t : Fin n → ZMod (2 ^ w)) (C : Ciphertext n w) (μ : Bool) (error : Fin (n + 1) × Fin w → ℤ) (hC : HasError t C μ error) (herror : ∀ (i : Fin (n + 1) × Fin w), 4 * (error i).natAbs < 2 ^ w) : decrypt t C = μ

Every Boolean ciphertext satisfying the actual modular equation decrypts correctly under the strict integer noise margin, whether it is fresh or produced by prior NAND operations.

theorem Cslib.Crypto.Homomorphic.GSW.decrypt_encryptWithCoins {n m w bound : ℕ} (B : Matrix (Fin m) (Fin n) (ZMod (2 ^ w))) (t : Fin n → ZMod (2 ^ w)) (error : Fin m → ℤ) (μ : Bool) (R : Matrix (Fin (n + 1) × Fin w) (Fin m) Bool) (hw : 0 < w) (herror : ∀ (j : Fin m), (error j).natAbs ≤ bound) (hmargin : 4 * (m * bound) < 2 ^ w) : decrypt t (encryptWithCoins (publicMatrix B t error) μ R) = μ

Fresh encryption is correct whenever the sum bound on its integer errors fits below one quarter of the modulus. This holds for every binary choice of encryption coins.

theorem Cslib.Crypto.Homomorphic.GSW.decrypt_nand {n w bound₁ bound₂ : ℕ} (t : Fin n → ZMod (2 ^ w)) (C₁ C₂ : Ciphertext n w) (μ₁ μ₂ : Bool) (error₁ error₂ : Fin (n + 1) × Fin w → ℤ) (hC₁ : HasError t C₁ μ₁ error₁) (hC₂ : HasError t C₂ μ₂ error₂) (hw : 0 < w) (herror₁ : ∀ (i : Fin (n + 1) × Fin w), (error₁ i).natAbs ≤ bound₁) (herror₂ : ∀ (i : Fin (n + 1) × Fin w), (error₂ i).natAbs ≤ bound₂) (hmargin : 4 * (bound₁ + (n + 1) * w * bound₂) < 2 ^ w) : decrypt t (nand C₁ C₂) = !(μ₁ && μ₂)

NAND is correct under its actual propagated noise bound. The inputs can themselves be outputs of earlier operations, provided their integer error equations and bounds hold.