Compatible positive-noise GSW parameters

For k = λ + 1, choose n = η = k, w = 16 + 8 * clog 2 k, ciphertext dimension N = (n + 1) * w, and m = N + 2 * λ samples. This explicit family satisfies the statistical entropy margin and the strict fresh-encryption and one-NAND noise margins simultaneously.

These are arithmetic and native-runtime facts about the parameter functions. They neither assert decision-LWE hardness for the finite centered-binomial error nor prove bootstrappability.

Main definitions

• dimension, noise, width, rows, samples, modulus: the numerical parameter family.

Main results

• entropy_margin: twice the security parameter in surplus source bits.
• fresh_margin, nand_margin: strict decoding margins with positive noise.
• negligible_statistical_error: the shared-public-matrix error is negligible.
• computableTidilyInPolyTime_*: uniform unary native computation of each parameter.

References

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

The family here supplies explicit compatible inequalities for the power-of-two specialization; it is not a claim about the paper's hardness parameters.

def Cslib.Crypto.Homomorphic.GSW.Parameters.dimension (security : ℕ) : ℕ

Number of secret coordinates.

def Cslib.Crypto.Homomorphic.GSW.Parameters.noise (security : ℕ) : ℕ

Positive centered-binomial width.

def Cslib.Crypto.Homomorphic.GSW.Parameters.width (security : ℕ) : ℕ

Number of binary digits in one modular coordinate.

def Cslib.Crypto.Homomorphic.GSW.Parameters.rows (security : ℕ) : ℕ

Number of ciphertext rows.

def Cslib.Crypto.Homomorphic.GSW.Parameters.samples (security : ℕ) : ℕ

Number of public samples and source bits in each encryption row.

def Cslib.Crypto.Homomorphic.GSW.Parameters.modulus (security : ℕ) : ℕ

Power-of-two modulus.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.noise_pos (security : ℕ) : 0 < noise security

The noise is positive even at security parameter zero.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.width_pos (security : ℕ) : 0 < width security

Every parameter uses a nonempty modular bit representation.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.entropy_margin (security : ℕ) : rows security + 2 * security ≤ samples security

Each encryption row has the surplus required by the shared-public-matrix bound.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.width_le (security : ℕ) : width security ≤ 16 * (security + 1)

The digit width has a simple linear majorant.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.rows_le (security : ℕ) : rows security ≤ 32 * (security + 1) ^ 2

The ciphertext dimension has a uniform quadratic majorant.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.samples_le (security : ℕ) : samples security ≤ 34 * (security + 1) ^ 2

The number of public samples has a uniform quadratic majorant.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.modulus_ge (security : ℕ) : 65536 * (security + 1) ^ 8 ≤ modulus security

The modulus dominates the eighth power of the positive parameter.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.modulus_le (security : ℕ) : modulus security ≤ 16777216 * (security + 1) ^ 8

The modulus also has an explicit polynomial upper bound.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.nand_margin (security : ℕ) : 4 * (1 + rows security) * samples security * noise security < modulus security

NAND of two fresh ciphertexts lies strictly inside the decoder's noise margin.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.fresh_margin (security : ℕ) : 4 * samples security * noise security < modulus security

Fresh encryption lies strictly inside the decoder's noise margin.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_dimension : Turing.MultiTapeTM.ComputableTidilyInPolyTime dimension Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The secret dimension is uniformly computable on unary parameters.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_noise : Turing.MultiTapeTM.ComputableTidilyInPolyTime noise Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The positive noise width is uniformly computable on unary parameters.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_width : Turing.MultiTapeTM.ComputableTidilyInPolyTime width Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The logarithmic digit width is uniformly computable on unary parameters.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_rows : Turing.MultiTapeTM.ComputableTidilyInPolyTime rows Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The ciphertext dimension is uniformly computable on unary parameters.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_samples : Turing.MultiTapeTM.ComputableTidilyInPolyTime samples Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The public sample count is uniformly computable on unary parameters.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.computableTidilyInPolyTime_modulus : Turing.MultiTapeTM.ComputableTidilyInPolyTime modulus Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

Even the modulus itself has a uniform unary native certificate. This uses bounded powers of a ceiling logarithm, rather than treating arbitrary unary exponentiation as efficient.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.polynomiallyBounded_parameters : PolynomiallyBounded dimension ∧ PolynomiallyBounded noise ∧ PolynomiallyBounded width ∧ PolynomiallyBounded rows ∧ PolynomiallyBounded samples ∧ PolynomiallyBounded modulus

Every numerical parameter, including the modulus, is polynomially bounded.

theorem Cslib.Crypto.Homomorphic.GSW.Parameters.negligible_statistical_error : Negligible fun (security : ℕ) => ↑(rows security) * NNReal.sqrt (2 ^ rows security / 2 ^ samples security)

The exact shared-public-matrix error bound is negligible for this positive-noise family.