GSW parameters with a logarithmic-depth noise margin

For t = 1 + clog 2 (λ + 2), choose digit width w = 16384 * t^2, ciphertext dimension N = (n + 1) * w, sample count m = N + 2λ, and depth budget L = 512 * t. The secret and positive-noise dimensions reuse Parameters.dimension and Parameters.noise, both λ + 1. The complete margin 4 * m * η * (N + 1)^L < 2^w holds at every security parameter.

All dimensions and the budget have uniform unary native routines. The modulus has a binary routine; its value is not claimed polynomially bounded. Security assumes decision LWE for exactly this family's centered-binomial law. These numerical bounds do not establish that an actual augmented decryption circuit fits the budget, or assert lattice hardness or circular security.

Main definitions

• logSize, width, rows, samples, depthBudget, modulus: the numerical family.

Main results

• noise_margin: the strict decoding margin after the entire declared depth budget.
• entropy_margin, negligible_statistical_error: the statistical part of the security bound.
• polynomiallyBounded_parameters: polynomial bounds for the unary numerical parameters.
• computableTidilyInPolyTime_modulus: native computation of the binary modulus.

References

• Gentry, Sahai and Waters, Sections 3.3–3.4

The constants here supply explicit compatible inequalities for the power-of-two specialization; they are not a claim about the paper's hardness parameters.

def Cslib.Crypto.Homomorphic.GSW.DepthParameters.logSize (security : ℕ) : ℕ

A positive logarithmic size, at least two even at security parameter zero.

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

Binary digits in each modular coordinate.

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

Ciphertext rows and columns.

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

Public samples and independent source bits in each encryption row.

def Cslib.Crypto.Homomorphic.GSW.DepthParameters.depthBudget (security : ℕ) : ℕ

Number of NAND levels covered by the proved noise margin.

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

Modulus, represented in binary by the native routine below.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.two_le_logSize (security : ℕ) : 2 ≤ logSize security

The logarithmic size is uniformly bounded away from zero.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.logSize_le (security : ℕ) : logSize security ≤ security + 2

A simple linear majorant for the logarithmic size.

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

Every parameter has a nonempty modular word.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.depthBudget_pos (security : ℕ) : 0 < depthBudget security

The depth budget is positive for every security parameter.

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

The number of samples has exactly the required entropy surplus.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.width_le (security : ℕ) : width security ≤ 16384 * (security + 2) ^ 2

The binary digit width has an explicit quadratic majorant.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.rows_le (security : ℕ) : rows security ≤ 16384 * (security + 2) ^ 3

The ciphertext dimension has an explicit cubic majorant.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.samples_le (security : ℕ) : samples security ≤ 16386 * (security + 2) ^ 3

The public sample count has an explicit cubic majorant.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.depthBudget_le (security : ℕ) : depthBudget security ≤ 512 * (security + 2)

The logarithmic budget also has a linear majorant.

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

The complete declared NAND depth remains strictly inside the original decoding margin.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.noise_margin_of_le {security depth : ℕ} (hdepth : depth ≤ depthBudget security) : 4 * samples security * Parameters.noise security * (rows security + 1) ^ depth < modulus security

Every smaller depth also satisfies the full noise margin.

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

Fresh ciphertexts satisfy the strict decoding margin.

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

A NAND of two fresh ciphertexts satisfies the existing sampler theorem's margin.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.computableTidilyInPolyTime_logSize : Turing.MultiTapeTM.ComputableTidilyInPolyTime logSize Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

The logarithmic size is uniformly computable with unary input and output.

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

Compute the unary digit width, including its quadratic dependence on the logarithm.

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

Compute the unary ciphertext dimension.

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

Compute the unary public sample count.

theorem Cslib.Crypto.Homomorphic.GSW.DepthParameters.computableTidilyInPolyTime_depthBudget : Turing.MultiTapeTM.ComputableTidilyInPolyTime depthBudget Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

Compute the unary logarithmic depth budget.

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

Compute the modulus in binary; this does not assert efficient unary output.

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

All unary parameters have polynomial bounds; the modulus is deliberately excluded.

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

The actual shared-public-matrix error bound is negligible for this new family.