github/zk-fhe
1
1
Fork 0
mirror of https://github.com/enricobottazzi/zk-fhe.git synced 2026-01-09 13:18:04 -05:00
Code Issues Packages Projects Releases Wiki Activity

fix: security analysis reviwe

Browse Source
This commit is contained in:
Enrico Bottazzi
2023-10-06 12:48:26 +02:00
parent 15281b86a0
commit 44f8d250d7
4 changed files with 333 additions and 166 deletions
Download Patch File Download Diff File Expand all files Collapse all files

314
examples/bfv.rs
View File

@@ -2,6 +2,7 @@ use std::env::var;
use std::vec;
use clap::Parser;
use halo2_base::safe_types::GateInstructions;
use halo2_base::safe_types::RangeChip;
use halo2_base::safe_types::RangeInstructions;
use halo2_base::utils::ScalarField;
@@ -25,7 +26,6 @@ use zk_fhe::chips::poly_operations::{
/// * `DEG`: Degree of the cyclotomic polynomial `cyclo` of the polynomial ring R_q.
/// * `Q`: Modulus of the cipher text field
/// * `T`: Modulus of the plaintext field
/// * `DELTA` : Q/T rounded to the lower integer
/// * `B`: Upper bound of the Gaussian distribution Chi Error. It is defined as 6 * sigma
///
/// # Fields
@@ -36,22 +36,27 @@ use zk_fhe::chips::poly_operations::{
/// * `u`: Ephemeral key polynomial coefficients from the distribution ChiKey [a_DEG-1, a_DEG-2, ..., a_1, a_0]
/// * `e0`: Error polynomial coefficients from the distribution ChiError [a_DEG-1, a_DEG-2, ..., a_1, a_0]
/// * `e1`: Error polynomial coefficients from the distribution ChiError [a_DEG-1, a_DEG-2, ..., a_1, a_0]
/// * `c0`: First ciphertext component polynomial coefficients of degree DEG-1 [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term
/// * `c1`: Second ciphertext component polynomial coefficients of degree DEG-1 [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term
/// # Assumes that the following checks have been performed outside the circuit
/// - `DEG` must be a power of 2
/// - `Q` must be a prime number
/// - `Q` must be greater than 1.
/// - If n is the number of bits of Q, and m is the number of bits of the prime field of the circuit. n must be set such that (n * 2) + 2 < m to avoid overflow of the coefficients of the polynomials
/// - `T` must be a prime number and must be greater than 1 and less than `Q`
/// - `B` must be a positive integer
/// - `pk0` and `pk1` must be polynomials in the R_q ring. The ring R_q is defined as R_q = Z_q[x]/(x^DEG + 1)
/// - `cyclo` must be the cyclotomic polynomial of degree `DEG` => x^DEG + 1
/// # Assumptions (to be checked outside the circuit)
///
/// * `DEG` must be a power of 2
/// * `Q` must be a prime number and be greater than 1.
/// * `Q` must be less than 2^64
/// * `Q` is less than (Q-1) * (Q-1) * DEG < p where p is the prime field of the circuit
/// * `T` must be a prime number and must be greater than 1 and less than `Q`
/// * `B` must be a positive integer and must be less than `Q`
/// * `cyclo` must be the cyclotomic polynomial of degree `DEG` => x^DEG + 1 (this is a public output of the circuit)
/// * `pk0` and `pk1` must be polynomials in the R_q ring. The ring R_q is defined as R_q = Z_q[x]/(x^DEG + 1)
// DEG and Q Parameters of the BFV encryption scheme chosen according to TABLES of RECOMMENDED PARAMETERS for 128-bits security level
// For real world applications, the parameters should be chosen according to the security level required.
// DEG and Q Parameters of the BFV encryption scheme should be chosen according to TABLES of RECOMMENDED PARAMETERS for 128-bits security level
// https://homomorphicencryption.org/wp-content/uploads/2018/11/HomomorphicEncryptionStandardv1.1.pdf
// B is the upper bound of the distribution Chi Error. We pick standard deviation 𝜎 ≈ 3.2 according to the HomomorphicEncryptionStandardv1 paper.
// T has been picked according to Lattigo (https://github.com/tuneinsight/lattigo/blob/master/bfv/params.go) implementation
// As suggest by https://eprint.iacr.org/2021/204.pdf (paragraph 2) we take B = 6σerr
// B is the upper bound of the distribution Chi Error. Pick standard deviation 𝜎 ≈ 3.2 according to the HomomorphicEncryptionStandardv1 paper.
// T should be be picked according to Lattigo (https://github.com/tuneinsight/lattigo/blob/master/bfv/params.go) implementation
// As suggest by https://eprint.iacr.org/2021/204.pdf (paragraph 2) B = 6σerr
// These are just parameters used for fast testing
const DEG: usize = 4;
const Q: u64 = 4637;
const T: u64 = 7;
@@ -59,14 +64,14 @@ const B: u64 = 18;
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct CircuitInput<const DEG: usize, const Q: u64, const T: u64, const B: u64> {
pub pk0: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. Should live in R_q (to be checked outside the circuit)
pub pk1: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. Should live in R_q (to be checked outside the circuit)
pub m: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. Should in R_t (checked inside the circuit)
pub u: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. Lives in R_q (checked inside the circuit)
pub e0: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. Lives in R_q (checked inside the circuit)
pub e1: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. Lives in R_q (checked inside the circuit)
pub c0: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. It is compared to the ciphertext c0 generated as output by the circuit
pub c1: Vec<u64>, // polynomial coefficients [a_N-1, a_N-2, ..., a_1, a_0] where a_0 is the constant term. It is compared to the ciphertext c1 generated as output by the circuit
pub pk0: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. PUBLIC. Should live in R_q according to assumption
pub pk1: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. PUBLIC. Should live in R_q according to assumption
pub m: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. PRIVATE. Should in R_t (enforced inside the circuit)
pub u: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. PRIVATE. Should live in R_q and be sampled from the distribution ChiKey (checked inside the circuit)
pub e0: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. PRIVATE. Should live in R_q and be sampled from the distribution ChiError (checked inside the circuit)
pub e1: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. PRIVATE. Should live in R_q and be sampled from the distribution ChiError (checked inside the circuit)
pub c0: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. Should live in R_q. This is just a test value compared to the ciphertext c0 generated as (public) output by the circuit
pub c1: Vec<u64>, // polynomial coefficients [a_DEG-1, a_DEG-2, ..., a_1, a_0] where a_0 is the constant term. Should live in R_q. This is just a test value compared to the ciphertext c1 generated as (public) output by the circuit
}
fn bfv_encryption_circuit<F: ScalarField>(
@@ -125,6 +130,7 @@ fn bfv_encryption_circuit<F: ScalarField>(
const DELTA: u64 = Q / T; // Q/T rounded to the lower integer
// This is a setup necessary for halo2_lib in order to create the range chip
// lookup bits must agree with the size of the lookup table, which is specified by an environmental variable
let lookup_bits = var("LOOKUP_BITS")
.unwrap_or_else(|_| panic!("LOOKUP_BITS not set"))
@@ -134,7 +140,11 @@ fn bfv_encryption_circuit<F: ScalarField>(
let range = RangeChip::default(lookup_bits);
// Assign the cyclotomic polynomial to the circuit -> x^DEG + 1
// Performing the assignemnt for the index 0, using a for loop from 1 to DEG - 1, and performing the assignment for the index DEG enforces that the degree of the polynomial is DEG
// Performing the assignemnt for the index 0, using a for loop from 1 to DEG - 1, and performing the assignment for the index DEG enforces that:
// - the degree of the polynomial is DEG
// - the leading coefficient is 1
// - the constant term is 1
// - all the other coefficients are 0
let mut cyclo = vec![];
let leading_coefficient = F::from(1);
@@ -153,36 +163,37 @@ fn bfv_encryption_circuit<F: ScalarField>(
assert!(cyclo.len() - 1 == DEG);
/* Constraints on e0
- e0 must be a polynomial in the R_q ring => Coefficients must be in the [0, Q) range and the degree of e0 must be DEG - 1
/* constraint on e0
- e0 must be a polynomial in the R_q ring => Coefficients must be in the [0, Q-1] range and the degree of e0 must be DEG - 1
- e0 must be sampled from the distribution ChiError
Approach:
- `check_poly_from_distribution_chi_error` chip guarantees that the coefficients of e0 are in the range [0, b] OR [q-b, q-1]
- As this range is a subset of the [0, Q) range, the coefficients of e0 are in the [0, Q) range
- The assignment for loop above guarantees that the degree of e0 is DEG - 1
- As this range is a subset of the [0, Q-1] range, the coefficients of e0 are guaranteed to be in the [0, Q-1] range
- The assignment for loop above enforces that the degree of e0 is DEG - 1
*/
/* Constraints on e1
/* constraint on e1
Same as e0
*/
// Assumption for the chip is that B < Q which is satisfied by circuit assumption
check_poly_from_distribution_chi_error::<{ DEG - 1 }, Q, B, F>(ctx, e0.clone(), &range);
check_poly_from_distribution_chi_error::<{ DEG - 1 }, Q, B, F>(ctx, e1.clone(), &range);
/* Constraints on u
- u must be a polynomial in the R_q ring => Coefficients must be in the [0, Q) range and the degree of u must be DEG - 1
/* constraint on u
- u must be a polynomial in the R_q ring => Coefficients must be in the [0, Q-1] range and the degree of u must be DEG - 1
- u must be sampled from the distribution ChiKey
Approach:
- `check_poly_from_distribution_chi_key` chip guarantees that the coefficients of u are in the range [0, 1, Q-1]
- As this range is a subset of the [0, Q) range, the coefficients of u are in the [0, Q) range
- `check_poly_from_distribution_chi_key` chip guarantees that the coefficients of u are either 0, 1 or Q-1
- As this range is a subset of the [0, Q-1] range, the coefficients of u are guaranteed to be in the [0, Q-1] range
- The assignment for loop above guarantees that the degree of u is DEG - 1
*/
check_poly_from_distribution_chi_key::<{ DEG - 1 }, Q, F>(ctx, u.clone(), range.gate());
/* Constraints on m
/* constraint on m
- m must be a polynomial in the R_t ring => Coefficients must be in the [0, T/2] OR [Q - T/2, Q - 1] range and the degree of m must be DEG - 1
Approach:
@@ -190,48 +201,75 @@ fn bfv_encryption_circuit<F: ScalarField>(
- The assignment for loop above guarantees that the degree of m is DEG - 1
*/
// TO DO: apply constraint on the coefficients of m!
// 1. COMPUTE C0
// 1. COMPUTE C0 (c0 is the first ciphertext component)
// pk0 * u
// Perform the polynomial multiplication between pk0 and u.
// OVERFLOW ANALYSIS
// The coefficients of pk0 are in the range [0, Q) according to the check to be performed outside the circuit.
// The coefficients of u are either [0, 1, Q-1] according to the constraints set above.
// The coefficients of pk0_u are calcualted as $c_k = \sum_{i=0}^{k} pk0[i] * u[k - i]$. Where k is the index of the coefficient of pk0_u.
// DEGREE ANALYSIS
// The degree of pk0 is DEG - 1 according to the constraint set above
// The degree of u is DEG - 1 according to the constraint set above
// The degree of pk0_u is constrained to be DEG - 1 + DEG - 1 = 2*DEG - 2 according to the logic of the `poly_mul_equal_deg` chip
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of pk0 are in the range [0, Q-1] according to the assumption of the circuit
// The coefficients of u are either 0, 1 or Q-1 according to the constraint set above.
// The coefficients of pk0_u are calculated as $c_{k} = \sum_{i=0}^{k} pk0[i] * u[k - i]$. Where k is the index of the coefficient c of pk0_u.
// For two polynomials of the same degree n, the maximum number of multiplications in the sum is for k = n. Namely for the coefficient c_n.
// The number of multiplications in the sum for the coefficient c_n is n + 1.
// Given that the input polynomials are of degree DEG - 1, the maximum number of multiplications in the sum is for k = DEG - 1.
// In that case there are DEG multiplications in the sum.
// For that particular coefficient, the maximum value of the coffiecient of pk0_u is (Q-1) * (Q-1) * DEG.
// The maximum value of the coffiecient of pk0_u is (Q-1) * (Q-1) * DEG.
// Q needs to be chosen such that (Q-1) * (Q-1) * DEG < p where p is the prime field of the circuit in order to avoid overflow during the multiplication.
// In that case there are max DEG multiplications in the sum.
// It follows that the maximum value that a coefficient of pk0_u can have is (Q-1) * (Q-1) * DEG.
// Q needs to be chosen such that (Q-1) * (Q-1) * DEG < p where p is the prime field of the circuit in order to avoid overflow during the polynomial multiplication.
// (Q-1) * (Q-1) * DEG < p according to the assumption of the circuit.
let pk0_u = poly_mul_equal_deg::<{ DEG - 1 }, F>(ctx, pk0.clone(), u.clone(), &range.gate());
// pk0_u is a polynomial of degree (DEG - 1) * 2 = 2*DEG - 2
// pk0_u has coefficients in the [0, (Q-1) * (Q-1) * DEG] range
// Reduce the coefficients by modulo `Q`
// get the number of bits needed to represent the value of (Q-1) * (Q-1) * DEG
let binary_representation = format!("{:b}", ((Q - 1) * (Q - 1) * (DEG as u64)));
let num_bits_1 = binary_representation.len();
// The coefficients of pk0_u are in the range [0, (Q-1) * (Q-1) * DEG] according to the polynomial multiplication constraint set above.
// Therefore the coefficients of pk0_u are known to have <= `num_bits_1` bits, therefore they satisfy the assumption of the `poly_reduce` chip
let pk0_u = poly_reduce::<{ 2 * DEG - 2 }, Q, F>(ctx, pk0_u, &range, num_bits_1);
// pk0_u is a polynomial of degree (DEG - 1) * 2 = 2*DEG - 2
// pk0_u has coefficients in the [0, Q) range
// pk0_u has coefficients in the [0, Q-1] range
// cyclo is a polynomial of degree DEG
// Reduce the coefficients by the cyclotomic polynomial of degree `DEG` => x^DEG + 1 to get a polynomial of degree DEG - 1
// Dealing with the assumption of the `poly_divide_by_cyclo` chip
// - The degree of dividend (pk0_u) is equal to (2 * DEG) - 2 according to the constraint set above
// - The coefficients of dividend are in the [0, Q-1] range according to the constraint set above
// - The divisor is a cyclotomic polynomial of degree DEG with coefficients either 0 or 1
// - The coefficients of dividend and divisor can be expressed as u64 values as long as Q - 1 is less than 2^64
// - Q is chosen such that (Q-1) * (2 * DEG - 2 - DEG + 1)] + Q-1 < p. Note that this is a subset of the condition (Q-1) * (Q-1) * DEG < p which is an assumption of the circuit.
let pk0_u =
poly_divide_by_cyclo::<{ 2 * DEG - 2 }, DEG, Q, F>(ctx, pk0_u, cyclo.clone(), &range);
// assert that the degree of pk0_u is 2*DEG - 2
assert_eq!(pk0_u.len() - 1, 2 * DEG - 2);
// But actually, the degree of pk0_u is DEG - 1, the first DEG - 1 coefficients are just zeroes
// Therefore, we need to trim the first DEG - 1 coefficients
// Enforce that the first DEG - 1 coefficients of pk0_u are zeroes
for i in 0..DEG - 1 {
let bool = range.gate().is_equal(ctx, pk0_u[i], Constant(F::from(0)));
range.gate().assert_is_const(ctx, &bool, &F::from(1));
}
// Therefore, we can safely trim the first DEG - 1 coefficients from pk0_u
let mut pk0_u_trimmed = vec![];
for i in DEG - 1..pk0_u.len() {
@@ -239,6 +277,7 @@ fn bfv_encryption_circuit<F: ScalarField>(
}
// assert that the degree of pk0_u_trimmed is DEG - 1
assert_eq!(pk0_u_trimmed.len() - 1, DEG - 1);
// pk0_u_trimmed is a polynomial in the R_q ring!
@@ -247,122 +286,209 @@ fn bfv_encryption_circuit<F: ScalarField>(
// Perform the polynomial scalar multiplication between m and delta.
// OVERFLOW ANALYSIS
// DEGREE ANALYSIS
// The degree of m is DEG - 1 according to the constraint set above
// Delta is a scalar constant
// The degree of m_delta is constrained to be DEG - 1 according to the logic of the `poly_scalar_mul` chip
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of m are in the range [0, T/2] OR [Q - T/2, Q - 1] according to the constaints set above.
// Delta is a constant in the range [0, Q) as it is defined as Q/T rounded to the lower integer and T < Q and T > 1.
// The maximum value of the coffiecient of m_delta is (Q-1) * (Q-1) = Q^2 - 2Q + 1.
// T has to be less than Q (check performed outside the circuit).
// If the previous condition (Q^2 - 2Q + 1 < p) is satisfied there is no risk of overflow during the scalar multiplication.
// Delta is a constant equal to Q/T (integer division) where T < Q according to the assumption of the circuit.
// The maximum value of a coefficient of m_delta is (Q-1) * (Q/T)
// If the condition (Q-1) * (Q/T) < p is satisfied there is no risk of overflow during the scalar multiplication.
// Note that this condition is a subset of the condition (Q-1) * (Q-1) * DEG < p which is an assumption of the circuit.
let m_delta =
poly_scalar_mul::<{ DEG - 1 }, F>(ctx, m.clone(), Constant(F::from(DELTA)), range.gate());
// m_delta is a polynomial of degree DEG - 1
// Coefficients of m_delta are in the [0, (Q-1) * (Q/T)] range
// Reduce the coefficients of `m_delta` by modulo `Q`
// get the number of bits needed to represent the value of (Q-1) * (Q/T)
let binary_representation = format!("{:b}", ((Q - 1) * (Q / T)));
let num_bits_2 = binary_representation.len();
// The coefficients of m_delta are in the range [0, (Q-1) * (Q/T)] according to the polynomial scalar multiplication constraint set above.
// Therefore the coefficients of m_delta are known to have <= `num_bits_2` bits, therefore they satisfy the assumption of the `poly_reduce` chip
let m_delta = poly_reduce::<{ DEG - 1 }, Q, F>(ctx, m_delta, &range, num_bits_2);
// Note: Scalar multiplication does not change the degree of the polynomial, therefore we do not need to reduce the coefficients by the cyclotomic polynomial of degree `DEG` => x^DEG + 1
let m_delta = poly_reduce::<{ DEG - 1 }, Q, F>(ctx, m_delta, &range, num_bits_1);
// m_delta is a polynomial in the R_q ring
// pk0_u_trimmed + m_delta
// Perform the polynomial addition between pk0_u_trimmed and m_delta.
// Note: Addition does not change the degree of the polynomial, therefore we do not need to reduce the coefficients by the cyclotomic polynomial of degree `DEG` => x^DEG + 1
// OVERFLOW ANALYSIS
// The coefficients of pk0_u_trimmed and m_delta are in the [0, Q) range according to the constraints set above.
// The maximum value of the coffiecient of pk0_u_trimmed_plus_m_delta is (Q-1) + (Q-1) = 2Q - 2.
// If the previous condition (Q^2 - 2Q + 1 < p) is satisfied there is no risk of overflow during the addition.
// DEGREE ANALYSIS
// The degree of pk0_u_trimmed is DEG - 1 according to the constraint set above
// The degree of m_delta is DEG - 1 according to the constraint set above
// The degree of pk0_u_trimmed_plus_m_delta is constrained to be DEG - 1 according to the logic of the `poly_add` chip
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of pk0_u_trimmed and m_delta are in the [0, Q -1] range according to the constraint set above.
// The coefficients of m_delta are in the [0, Q -1] range according to the constraint set above.
// The maximum value of the coefficient of pk0_u_trimmed_plus_m_delta is (Q-1) + (Q-1) = 2Q - 2.
// If the condition (Q-1) + (Q-1) < p is satisfied there is no risk of overflow during the polynomial addition.
// Note that this condition is a subset of the condition (Q-1) * (Q-1) * DEG < p which is an assumption of the circuit.
let pk0_u_trimmed_plus_m_delta =
poly_add::<{ DEG - 1 }, F>(ctx, pk0_u_trimmed, m_delta, range.gate());
// Reduce the coefficients of `pk0_u_trimmed_plus_m_delta` by modulo `Q`
let pk0_u_trimmed_plus_m_delta =
poly_reduce::<{ DEG - 1 }, Q, F>(ctx, pk0_u_trimmed_plus_m_delta, &range, num_bits_1);
// Reduce the coefficients of `m_delta` by modulo `Q`
// Coefficients of pk0_u_trimmed_plus_m_delta are in the [0, 2Q - 2] range
// get the number of bits needed to represent the value of 2Q - 2
let binary_representation = format!("{:b}", (2 * Q - 2));
let num_bits_3 = binary_representation.len();
// The coefficients of pk0_u_trimmed_plus_m_delta are in the range [0, 2Q - 2] according to the polynomial addition constraint set above.
// Therefore the coefficients of m_delta are known to have <= `num_bits_3` bits, therefore they satisfy the assumption of the `poly_reduce` chip
// Reduce the coefficients of `pk0_u_trimmed_plus_m_delta` by modulo `Q`
let pk0_u_trimmed_plus_m_delta =
poly_reduce::<{ DEG - 1 }, Q, F>(ctx, pk0_u_trimmed_plus_m_delta, &range, num_bits_3);
// Note: Addition does not change the degree of the polynomial, therefore we do not need to reduce the coefficients by the cyclotomic polynomial of degree `DEG` => x^DEG + 1
// pk0_u_trimmed_plus_m_delta is a polynomial in the R_q ring
// c0 = pk0_u_trimmed_plus_m_delta + e0
// Perform the polynomial addition between pk0_u_trimmed_plus_m_delta and e0.
// OVERFLOW ANALYSIS
// The coefficients of pk0_u_trimmed_plus_m_delta are in the [0, Q) range according to the constraints set above.
// The coefficients of e0 are in the range [0, b] OR [q-b, q-1] according to the constraints set above.
// The maximum value of the coffiecient of c0 is (Q-1) + (Q-1) = 2Q - 2.
// If the previous condition (Q^2 - 2Q + 1 < p) is satisfied there is no risk of overflow during the addition.
// DEGREE ANALYSIS
// The degree of pk0_u_trimmed_plus_m_delta is DEG - 1 according to the constraint set above
// The degree of e0 is DEG - 1 according to the constraint set above
// The degree of c0 is constrained to be DEG - 1 according to the logic of the `poly_add` chip
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of pk0_u_trimmed_plus_m_delta and m_delta are in the [0, Q -1] range according to the constraint set above.
// The cofficients of e0 are in the range [0, b] OR [q-b, q-1] according to the constraint set above.
// The maximum value of the coefficient of c0 is (Q-1) + (Q-1) = 2Q - 2.
// If the condition (Q-1) + (Q-1) < p is satisfied there is no risk of overflow during the polynomial addition.
// Note that this condition is a subset of the condition (Q-1) * (Q-1) * DEG < p which is an assumption of the circuit.
let c0 = poly_add::<{ DEG - 1 }, F>(ctx, pk0_u_trimmed_plus_m_delta, e0, range.gate());
// get the number of bits needed to represent the value of 2Q - 2.
let binary_representation = format!("{:b}", 2 * Q - 2);
let num_bits_2 = binary_representation.len();
// The coefficients of c0 are in the range [0, 2Q - 2] according to the polynomial addition constraint set above.
// Therefore the coefficients of c0 are known to have <= `num_bits_3` bits, therefore they satisfy the assumption of the `poly_reduce` chip
// Reduce the coefficients of `pk0_u_trimmed_plus_m_delta` by modulo `Q`
let c0 = poly_reduce::<{ DEG - 1 }, Q, F>(ctx, c0, &range, num_bits_3);
// Reduce the coefficients by modulo `Q`
// Note: Addition does not change the degree of the polynomial, therefore we do not need to reduce the coefficients by the cyclotomic polynomial of degree `DEG` => x^DEG + 1
let c0 = poly_reduce::<{ DEG - 1 }, Q, F>(ctx, c0, &range, num_bits_2);
// c0 is a polynomial in the R_q ring!
// c0 is a polynomial in the R_q ring
// 1. COMPUTE C1
// 1. COMPUTE C1 (c1 is the second ciphertext component)
// pk1 * u
// Perform the polynomial multiplication between pk1 and u.
// OVERFLOW ANALYSIS
// The coefficients of pk1 are in the range [0, Q) according to the check to be performed outside the circuit.
// The coefficients of u are either [0, 1, Q-1] according to the constraints set above.
// The coefficients of pk1_u are calcualted as $c_k = \sum_{i=0}^{k} pk1[i] * u[k - i]$. Where k is the index of the coefficient of pk1_u.
// DEGREE ANALYSIS
// The degree of pk1 is DEG - 1 according to the constraint set above
// The degree of u is DEG - 1 according to the constraint set above
// The degree of pk1_u is constrained to be DEG - 1 + DEG - 1 = 2*DEG - 2 according to the logic of the `poly_mul_equal_deg` chip
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of pk1 are in the range [0, Q-1] according to the assumption of the circuit
// The coefficients of u are either 0, 1 or Q-1 according to the constraint set above.
// The coefficients of pk1_u are calculated as $c_{k} = \sum_{i=0}^{k} pk1[i] * u[k - i]$. Where k is the index of the coefficient c of pk1_u.
// For two polynomials of the same degree n, the maximum number of multiplications in the sum is for k = n. Namely for the coefficient c_n.
// The number of multiplications in the sum for the coefficient c_n is n + 1.
// Given that the input polynomials are of degree DEG - 1, the maximum number of multiplications in the sum is for k = DEG - 1.
// In that case there are DEG multiplications in the sum.
// For that particular coefficient, the maximum value of the coffiecient of pk1_u is (Q-1) * (Q-1) * DEG.
// The maximum value of the coffiecient of pk1_u is (Q-1) * (Q-1) * DEG.
// Q needs to be chosen such that (Q-1) * (Q-1) * DEG < p where p is the prime field of the circuit in order to avoid overflow during the multiplication.
// In that case there are max DEG multiplications in the sum.
// It follows that the maximum value that a coefficient of pk1_u can have is (Q-1) * (Q-1) * DEG.
// Q needs to be chosen such that (Q-1) * (Q-1) * DEG < p where p is the prime field of the circuit in order to avoid overflow during the polynomial multiplication.
// (Q-1) * (Q-1) * DEG < p according to the assumption of the circuit.
let pk1_u = poly_mul_equal_deg::<{ DEG - 1 }, F>(ctx, pk1.clone(), u, range.gate());
// pk1_u is a polynomial of degree (DEG - 1) * 2 = 2*DEG - 2
// pk1_u has coefficients in the [0, (Q-1) * (Q-1) * DEG] range
// Reduce the coefficients by modulo `Q`
// The coefficients of pk1_u are in the range [0, (Q-1) * (Q-1) * DEG] according to the polynomial multiplication constraint set above.
// Therefore the coefficients of pk1_u are known to have <= `num_bits_1` bits, therefore they satisfy the assumption of the `poly_reduce` chip
let pk1_u = poly_reduce::<{ 2 * DEG - 2 }, Q, F>(ctx, pk1_u, &range, num_bits_1);
// pk1_u is a polynomial of degree (DEG - 1) * 2 = 2*DEG - 2
// pk1_u has coefficients in the [0, Q) range
// pk1_u has coefficients in the [0, Q-1] range
// cyclo is a polynomial of degree DEG
// Reduce the coefficients by the cyclotomic polynomial of degree `DEG` => x^DEG + 1 to get a polynomial of degree DEG - 1
// Dealing with the assumption of the `poly_divide_by_cyclo` chip
// - The degree of dividend (pk0_1) is equal to (2 * DEG) - 2 according to the constraint set above
// - The coefficients of dividend are in the [0, Q-1] range according to the constraint set above
// - The divisor is a cyclotomic polynomial of degree DEG with coefficients either 0 or 1
// - The coefficients of dividend and divisor can be expressed as u64 values as long as Q - 1 is less than 2^64
// - Q is chosen such that (Q-1) * (2 * DEG - 2 - DEG + 1)] + Q-1 < p. Note that this is a subset of the condition (Q-1) * (Q-1) * DEG < p which is an assumption of the circuit.
let pk1_u =
poly_divide_by_cyclo::<{ 2 * DEG - 2 }, DEG, Q, F>(ctx, pk1_u, cyclo.clone(), &range);
// assert that the degree of pk1_u is 2*DEG - 2
assert_eq!(pk1_u.len() - 1, 2 * DEG - 2);
// But actually, the degree of pk1_u is DEG - 1, the first DEG - 1 coefficients are just zeroes
// Therefore, we need to trim the first DEG - 1 coefficients
// Enforce that the first DEG - 1 coefficients of pk1_u are zeroes
for i in 0..DEG - 1 {
let bool = range.gate().is_equal(ctx, pk1_u[i], Constant(F::from(0)));
range.gate().assert_is_const(ctx, &bool, &F::from(1));
}
// Therefore, we can safely trim the first DEG - 1 coefficients from pk1_u
let mut pk1_u_trimmed = vec![];
for i in DEG - 1..pk1_u.len() {
pk1_u_trimmed.push(pk1_u[i]);
}
// assert that the degree of pk1_u_trimmed is DEG - 1
assert_eq!(pk1_u_trimmed.len() - 1, DEG - 1);
// pk1_u_trimmed is a polynomial in the R_q ring
// pk1_u_trimmed is a polynomial in the R_q ring!
// c1 = pk1_u_trimmed + e0
// c1 = pk1_u_trimmed + e1
// OVERFLOW ANALYSIS
// The coefficients of pk1_u are in the [0, Q) range according to the constraints set above.
// The coefficients of e1 are in the range [0, b] OR [q-b, q-1] according to the constraints set above.
// The maximum value of the coffiecient of c1 is (Q-1) + (Q-1) = 2Q - 2.
// If the previous condition (Q^2 - 2Q + 1 < p) is satisfied there is no risk of overflow during the addition.
// Perform the polynomial addition between pk1_u_trimmed and e1.
// DEGREE ANALYSIS
// FIX The degree of pk1_u_trimmed is DEG - 1 according to the constraint set above
// The degree of e1 is DEG - 1 according to the constraint set above
// The degree of c1 is constrained to be DEG - 1 according to the logic of the `poly_add` chip
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of pk1_u_trimmed are in the [0, Q-1] range according to the constraint set above.
// The cofficients of e1 are in the range [0, b] OR [q-b, q-1] according to the constraint set above.
// The maximum value of the coefficient of c1 is (Q-1) + (Q-1) = 2Q - 2.
// If the condition (Q-1) + (Q-1) < p is satisfied there is no risk of overflow during the polynomial addition.
// Note that this condition is a subset of the condition (Q-1) * (Q-1) * DEG < p which is an assumption of the circuit.
// Perform the polynomial addition between pk1_u_trimmed and e1.
// Perform the polynomial addition between pk1_u and e1.
let c1 = poly_add::<{ DEG - 1 }, F>(ctx, pk1_u_trimmed, e1, range.gate());
// Reduce the coefficients by modulo `Q`
let c1 = poly_reduce::<{ DEG - 1 }, Q, F>(ctx, c1, &range, num_bits_2);
// The coefficients of c1 are in the range [0, 2Q - 2] according to the polynomial addition constraint set above.
// Therefore the coefficients of c1 are known to have <= `num_bits_3` bits, therefore they satisfy the assumption of the `poly_reduce` chip
// Reduce the coefficients of `c1` by modulo `Q`
let c1 = poly_reduce::<{ DEG - 1 }, Q, F>(ctx, c1, &range, num_bits_3);
// Note: Addition does not change the degree of the polynomial, therefore we do not need to reduce the coefficients by the cyclotomic polynomial of degree `DEG` => x^DEG + 1
// c1 is a polynomial in the R_q ring
// That that c0 and c1 computed inside the circuit are equal to the ciphertexts provided as input in the test vector json file

24
src/chips/poly_distribution.rs
View File

@@ -8,8 +8,10 @@ use halo2_base::Context;
use halo2_base::QuantumCell::Constant;
/// Enforce that polynomial a of degree DEG is sampled from the distribution chi error
/// Namely, that the coefficients are in the range [0, B] OR [Q-B, Q-1]
/// DEG is the degree of the polynomial
///
/// * Namely, that the coefficients are in the range [0, B] OR [Q-B, Q-1]
/// * DEG is the degree of the polynomial
/// * Assumes that B < Q
pub fn check_poly_from_distribution_chi_error<
const DEG: usize,
const Q: u64,
@@ -29,7 +31,7 @@ pub fn check_poly_from_distribution_chi_error<
// - Check that coeff is in the range [Q-B, Q-1] and store the boolean result in in_partial_range_2_vec
// We then perform (`in_partial_range_1` OR `in_partial_range_2`) to check that coeff is in the range [0, B] OR [Q-B, Q-1]
// The result of this check is stored in the `in_range` vector.
// The bool value of `in_range` is then enforced to be true
// All the boolean values in `in_range` are then enforced to be true
let mut in_range_vec = Vec::with_capacity(DEG + 1);
// get the number of bits needed to represent the value of Q
@@ -37,25 +39,26 @@ pub fn check_poly_from_distribution_chi_error<
let q_bits = binary_representation.len();
for coeff in &a {
// First of all, enforce that coefficients are in the [0, 2^q_bits) range to satisfy the assumption of `is_less_than` chip
range.is_less_than_safe(ctx, *coeff, 1 << q_bits as u64);
// First of all, enforce that coefficient is in the [0, 2^q_bits] range
let bool = range.is_less_than_safe(ctx, *coeff, (1 << q_bits as u64) + 1);
range.gate().assert_is_const(ctx, &bool, &F::from(1));
// Check for the range [0, B]
// coeff is known are known to have <= `q_bits` bits according to the constraint set above
// B + 1 is known to have <= `q_bits` bits as public constant
// B + 1 is known to have <= `q_bits` bits according to assumption of the chip
// Therefore it satisfies the assumption of `is_less_than` chip
let in_partial_range_1 = range.is_less_than(ctx, *coeff, Constant(F::from(B + 1)), q_bits);
// Check for the range [Q-B, Q-1]
// coeff is known are known to have <= `q_bits` bits according to the constraint set above
// Q - B is known to have <= `q_bits` bits as public constant
// Q - B is known to have <= `q_bits` bits according to assumption of the chip
// Therefore it satisfies the assumption of `is_less_than` chip
let not_in_range_lower_bound =
range.is_less_than(ctx, *coeff, Constant(F::from(Q - B)), q_bits);
let in_range_lower_bound = range.gate.not(ctx, not_in_range_lower_bound);
// coeff is known are known to have <= `q_bits` bits according to the constraint set above
// Q is known to have <= `q_bits` bits as public constant
// Q is known to have <= `q_bits` by definition
// Therefore it satisfies the assumption of `is_less_than` chip
let in_range_upper_bound = range.is_less_than(ctx, *coeff, Constant(F::from(Q)), q_bits);
let in_partial_range_2 = range
@@ -75,8 +78,9 @@ pub fn check_poly_from_distribution_chi_error<
}
/// Enforce that polynomial a of degree DEG is sampled from the distribution chi key
/// Namely, that the coefficients are in the range [0, 1, Q-1].
/// DEG is the degree of the polynomial
///
/// * Namely, that the coefficients are in the range [0, 1, Q-1].
/// * DEG is the degree of the polynomial
pub fn check_poly_from_distribution_chi_key<const DEG: usize, const Q: u64, F: ScalarField>(
ctx: &mut Context<F>,
a: Vec<AssignedValue<F>>,

148
src/chips/poly_operations.rs
View File

@@ -9,8 +9,10 @@ use halo2_base::Context;
use halo2_base::QuantumCell;
/// Build the sum of the polynomials a and b as sum of the coefficients
/// DEG is the degree of the input polynomials
/// Input polynomials are parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
///
/// * DEG is the degree of the input polynomials
/// * Input polynomials are parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// * It assumes that the coefficients are constrained such to overflow during the polynomial addition
pub fn poly_add<const DEG: usize, F: ScalarField>(
ctx: &mut Context<F>,
a: Vec<AssignedValue<F>>,
@@ -21,12 +23,12 @@ pub fn poly_add<const DEG: usize, F: ScalarField>(
assert_eq!(a.len() - 1, b.len() - 1);
assert_eq!(a.len() - 1, DEG);
let c: Vec<AssignedValue<F>> = a
.iter()
.zip(b.iter())
.take(2 * (DEG) - 1)
.map(|(&a, &b)| gate.add(ctx, a, b))
.collect();
let mut c = vec![];
for i in 0..=DEG {
let val = gate.add(ctx, a[i], b[i]);
c.push(val);
}
// assert that the sum polynomial has degree DEG
assert_eq!(c.len() - 1, DEG);
@@ -35,9 +37,11 @@ pub fn poly_add<const DEG: usize, F: ScalarField>(
}
/// Build the product of the polynomials a and b as dot product of the coefficients of a and b
/// Compared to `poly_mul_diff_deg`, this function assumes that the polynomials have the same degree and therefore optimizes the computation
/// DEG is the degree of the input polynomials
/// Input polynomials are parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
///
/// * Compared to `poly_mul_diff_deg`, this function assumes that the polynomials have the same degree and therefore optimizes the computation
/// * DEG is the degree of the input polynomials
/// * Input polynomials are parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// * It assumes that the coefficients are constrained such to overflow during the polynomial multiplication
pub fn poly_mul_equal_deg<const DEG: usize, F: ScalarField>(
ctx: &mut Context<F>,
a: Vec<AssignedValue<F>>,
@@ -81,8 +85,10 @@ pub fn poly_mul_equal_deg<const DEG: usize, F: ScalarField>(
}
/// Build the product of the polynomials a and b as dot product of the coefficients of a and b
/// Compared to `poly_mul_equal_deg`, this function doesn't assume that the polynomials have the same degree. Therefore the computation is less efficient.
/// Input polynomials are parsed as a vector of assigned coefficients [a_n, a_n-1, ..., a_1, a_0] where a_0 is the constant term and n is the degree of the polynomial
///
/// * Compared to `poly_mul_equal_deg`, this function doesn't assume that the polynomials have the same degree. Therefore the computation is less efficient.
/// * Input polynomials are parsed as a vector of assigned coefficients [a_n, a_n-1, ..., a_1, a_0] where a_0 is the constant term and n is the degree of the polynomial
/// * It assumes that the coefficients are constrained such to overflow during the polynomial multiplication
pub fn poly_mul_diff_deg<F: ScalarField>(
ctx: &mut Context<F>,
a: Vec<AssignedValue<F>>,
@@ -122,8 +128,10 @@ pub fn poly_mul_diff_deg<F: ScalarField>(
}
/// Build the scalar multiplication of the polynomials a and the scalar k as scalar multiplication of the coefficients of a and k
/// DEG is the degree of the polynomial
/// Input polynomial is parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
///
/// * DEG is the degree of the polynomial
/// * Input polynomial is parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// * It assumes that the coefficients are constrained such to overflow during the scalar multiplication
pub fn poly_scalar_mul<const DEG: usize, F: ScalarField>(
ctx: &mut Context<F>,
a: Vec<AssignedValue<F>>,
@@ -133,7 +141,12 @@ pub fn poly_scalar_mul<const DEG: usize, F: ScalarField>(
// assert that the degree of the polynomial a is equal to DEG
assert_eq!(a.len() - 1, DEG);
let c: Vec<AssignedValue<F>> = a.iter().map(|&a| gate.mul(ctx, a, b)).collect();
let mut c = vec![];
for i in 0..=DEG {
let val = gate.mul(ctx, a[i], b);
c.push(val);
}
// assert that the product polynomial has degree DEG
assert_eq!(c.len() - 1, DEG);
@@ -142,9 +155,10 @@ pub fn poly_scalar_mul<const DEG: usize, F: ScalarField>(
}
/// Takes a polynomial represented by its coefficients in a vector and output a new polynomial reduced by applying modulo Q to each coefficient
/// DEG is the degree of the polynomial
/// Input polynomial is parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// It assumes that the coefficients of the input polynomial can be expressed in at most num_bits bits
///
/// * DEG is the degree of the polynomial
/// * Input polynomial is parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// * It assumes that the coefficients of the input polynomial can be expressed in at most num_bits bits
pub fn poly_reduce<const DEG: usize, const Q: u64, F: ScalarField>(
ctx: &mut Context<F>,
input: Vec<AssignedValue<F>>,
@@ -154,12 +168,13 @@ pub fn poly_reduce<const DEG: usize, const Q: u64, F: ScalarField>(
// Assert that degree of input polynomial is equal to the constant DEG
assert_eq!(input.len() - 1, DEG);
let mut rem_assigned = vec![];
// Enforce that in_assigned[i] % Q = rem_assigned[i]
let rem_assigned: Vec<AssignedValue<F>> = input
.iter()
.take(2 * DEG - 1)
.map(|&x| range.div_mod(ctx, x, Q, num_bits).1)
.collect();
for i in 0..=DEG {
let rem = range.div_mod(ctx, input[i], Q, num_bits).1;
rem_assigned.push(rem);
}
// assert that the reduced polynomial has degree DEG
assert_eq!(rem_assigned.len() - 1, DEG);
@@ -167,15 +182,19 @@ pub fn poly_reduce<const DEG: usize, const Q: u64, F: ScalarField>(
rem_assigned
}
/// Takes a polynomial `divisor` represented by its coefficients in a vector
/// Takes a polynomial `divisor` represented by its coefficients in a vector.
/// Takes a cyclotomic polynomial `dividend` f(x)=x^m+1 (m is a power of 2) of the form represented by its coefficients in a vector
/// Output the remainder of the division of `dividend` by `dividend` as a vector of coefficients
/// DEG_DVD is the degree of the `dividend` polynomial
/// DEG_DVS is the degree of the `divisor` polynomial
/// Q is the modulus of the Ring
/// Input polynomials is parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// Assumes that the coefficients of `dividend` are in the range [0, Q - 1]
/// Assumes that divisor is a cyclotomic polynomial with coefficients either 0 or 1
///
/// * DEG_DVD is the degree of the `dividend` polynomial
/// * DEG_DVS is the degree of the `divisor` polynomial
/// * Q is the modulus of the Ring
/// * Input polynomials is parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// * Assumes that the degree of dividend is equal to (2 * DEG_DVS) - 2
/// * Assumes that the coefficients of `dividend` are in the range [0, Q - 1]
/// * Assumes that divisor is a cyclotomic polynomial with coefficients either 0 or 1
/// * Assumes that dividend and divisor can be expressed as u64 values
/// * Assumes that Q is chosen such that (Q-1) * (DEG_DVD - DEG_DVS + 1)] + Q-1 < p where p is the prime field of the circuit in order to avoid overflow during the multiplication
pub fn poly_divide_by_cyclo<
const DEG_DVD: usize,
const DEG_DVS: usize,
@@ -191,6 +210,8 @@ pub fn poly_divide_by_cyclo<
assert_eq!(dividend.len() - 1, DEG_DVD);
// Assert that degree of divisor poly is equal to the constant DEG_DVS
assert_eq!(divisor.len() - 1, DEG_DVS);
// Assert that degree of dividend is equal to (2 * DEG_DVS) - 2
assert_eq!(dividend.len() - 1, (2 * DEG_DVS) - 2);
// DEG_DVS must be strictly less than DEG_DVD
assert!(DEG_DVS < DEG_DVD);
@@ -244,6 +265,12 @@ pub fn poly_divide_by_cyclo<
remainder.push(assigned_val);
}
// assert that the degree of quotient is DEG_DVD - DEG_DVS
assert_eq!(quotient.len() - 1, DEG_DVD - DEG_DVS);
// assert that the degree of remainder is DEG_DVD
assert_eq!(remainder.len() - 1, DEG_DVD);
// Quotient is obtained by dividing the coefficients of the dividend by the highest degree coefficient of divisor
// The coefficients of dividend are in the range [0, Q - 1] by assumption.
// The leading coefficient of divisor is 1 by assumption.
@@ -258,7 +285,7 @@ pub fn poly_divide_by_cyclo<
// The coefficients of quotient are in the range [0, Q - 1] by constraint set above.
// The coefficients of divisior are either 0, 1 by assumption of the cyclotomic polynomial.
// It follows that the coefficients of quotient * divisor are in the range [0, Q - 1]
// The remainder might have coefficients that are negative. In that case we add Q to them to make them positive.
// The remainder (as result dividend - (quotient * divisor)) might have coefficients that are negative. In that case we add Q to them to make them positive.
// Therefore, the coefficients of remainder are in the range [0, Q - 1]
// Since the remainder is computed outside the circuit, we need to enforce this constraint
for i in 0..DEG_DVS {
@@ -271,56 +298,63 @@ pub fn poly_divide_by_cyclo<
// Quotient is of degree DEG_DVD - DEG_DVS
// Divisor is of degree DEG_DVS
// Quotient * divisor is of degree DEG_DVD
// Remainder is of degree DEG_DVS - 1
// Remainder is of degree DEG_DVD
// Quotient * divisor + rem is of degree DEG_DVD
// Dividend is of degree DEG_DVD
// Perform the multiplication between quotient and divisor
// No risk of overflowing the circuit prime here when performing multiplication across coefficients
// Perform the polynomial multiplication between quotient and divisor
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of quotient are in the range [0, Q - 1] by constraint set above.
// The coefficients of divisor are either 0, 1 by assumption.
// We use a polynomial multiplication algorithm that does not require the input polynomials to be of the same degree
let prod = poly_mul_diff_deg(ctx, quotient, divisor, range.gate());
// The coefficients of Divisor are in the range [0, Q - 1] by assumption.
// The coefficients of Quotient are in the range [0, Q - 1] as per constraint set above.
// The coefficients of pk0_u are calcualted as $c_k = \sum_{i=0}^{k} pk0[i] * u[k - i]$. Where k is the index of the coefficient of pk0_u.
// The coefficients of prod are calculated as $c_{k} = \sum_{i=0}^{k} quotient[i] * divisor[k - i]$. Where k is the index of the coefficient c of prod.
// For two polynomials of differents degree n and m (where m < n), the max number of multiplication performed inside the summation is m + 1.
// The quotient is of degree DEG_DVD - DEG_DVS
// The divisor is of degree DEG_DVS
// The maximum number of multiplications in the sum is DEG_DVD + 1
// For that particular coefficient, the maximum value of the coffiecient of pk0_u is (Q-1) * (Q-1) * (DEG_DVD + 1).
// The maximum value of the coffiecient of pk0_u is (Q-1) * (Q-1) * (DEG_DVD + 1).
// Q needs to be chosen such that (Q-1) * (Q-1) * (DEG_DVD + 1) < p where p is the prime field of the circuit in order to avoid overflow during the multiplication.
// Therefore, the coefficients of prod are in the range [0, (Q-1) * (Q-1) * (DEG_DVD + 1)]
// Since DEG_DVD = (2 * DEG_DVS) - 2 it follows that the degree of the divisor is greater than the degree of quotient.
// In that case there are max (degree quotient + 1) multiplications in the sum. Namely DEG_DVD - DEG_DVS + 1 multiplications.
// The maximum value of the coffiecient of prod is (Q-1) * (1) * (DEG_DVD - DEG_DVS + 1).
// Q needs to be chosen such that (Q-1) * (DEG_DVD - DEG_DVS + 1) < p where p is the prime field of the circuit in order to avoid overflow during the multiplication.
// Note that this is a subset of the assumption of the circuit
// Therefore, the coefficients of prod are in the range [0, (Q-1) * (DEG_DVD - DEG_DVS + 1)]
// We use a polynomial multiplication algorithm that does not require the input polynomials to be of the same degree
let prod = poly_mul_diff_deg(ctx, quotient, divisor, range.gate());
// The degree of prod is DEG_DVD
assert_eq!(prod.len() - 1, DEG_DVD);
// Perform the addition between prod and remainder
// The degree of prod is DEG_DVD
// The degree of remainder is DEG_DVS - 1
// prod + remainder
// DEGREE ANALYSIS
// Prod is of degree DEG_DVD
// Remainder is of degree DEG_DVD
// Prod + rem is of degree DEG_DVD
// No risk of overflowing the circuit prime here when performing addition across coefficients
// The coefficients of prod are in the range [0, (Q-1) * (Q-1) * (DEG_DVD + 1)] by the operation above.
// COEFFICIENTS OVERFLOW ANALYSIS
// The coefficients of prod are in the range [0, (Q-1) * (DEG_DVD - DEG_DVS + 1)] by the constraint above.
// The coefficients of remainder are in the range [0, Q - 1] by constraint set above.
// Therefore, the coefficients of prod + remainder are in the range [0, [0, (Q-1) * (DEG_DVD - DEG_DVS + 1)] + Q-1].
// Q needs to be chosen such that (Q-1) * (DEG_DVD - DEG_DVS + 1)] + Q-1 < p where p is the prime field of the circuit in order to avoid overflow during the addition.
// This is true by assumption of the chip.
let sum = poly_add::<DEG_DVD, F>(ctx, prod, remainder.clone(), range.gate());
// assert that the degree of sum is DEG_DVD
assert_eq!(sum.len() - 1, DEG_DVD);
// The coefficients of prod are in the range [0, (Q-1) * (Q-1) * (DEG_DVD + 1)]
// The coefficients of remainder are in the range [0, Q - 1] by constraint set above.
// Therefore, the coefficients of sum are in the range [0, (Q-1) * (Q-1) * (DEG_DVD + 1) + Q - 1].
// We can reduce the coefficients of sum modulo Q to make them in the range [0, Q - 1]
// get the number of bits needed to represent the value of 2 * (Q - 1)
let binary_representation = format!("{:b}", (Q - 1) * (Q - 1) * ((DEG_DVD as u64) + 1) + Q - 1); // Convert to binary (base-2)
// get the number of bits needed to represent the value of (Q-1) * (DEG_DVD - DEG_DVS + 1)] + Q-1
let binary_representation = format!(
"{:b}",
(Q - 1) * (DEG_DVD as u64 - DEG_DVS as u64 + 1) + (Q - 1)
); // Convert to binary (base-2)
let num_bits = binary_representation.len();
// The coefficients of sum are in the range [0, (Q-1) * (DEG_DVD - DEG_DVS + 1)] + Q-1] according to the polynomial addition constraint set above.
// Therefore the coefficients of sum are known to have <= `num_bits` bits, therefore they satisfy the assumption of the `poly_reduce` chip
let sum_mod = poly_reduce::<DEG_DVD, Q, F>(ctx, sum, range, num_bits);
// assert that the degree of sum_mod is DEG_DVD

13
src/chips/utils.rs
View File

@@ -2,10 +2,12 @@ use halo2_base::{utils::ScalarField, AssignedValue};
/// Performs long polynomial division on two polynomials
/// Returns the quotient and remainder
/// Input polynomials are parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// DEG_DVD is the degree of the dividend
/// DEG_DVS is the degree of the divisor
/// Q is the modulus of the Ring. All the coefficients will be in the range [0, Q-1]
///
/// * Input polynomials are parsed as a vector of assigned coefficients [a_DEG, a_DEG-1, ..., a_1, a_0] where a_0 is the constant term
/// * DEG_DVD is the degree of the dividend
/// * DEG_DVS is the degree of the divisor
/// * Q is the modulus of the Ring. All the coefficients will be in the range [0, Q-1]
/// * Assumes that coefficients of the dividend and divisor are u64 values
pub fn div_euclid<const DEG_DVD: usize, const DEG_DVS: usize, const Q: u64>(
dividend: &Vec<u64>,
divisor: &Vec<u64>,
@@ -85,7 +87,8 @@ pub fn div_euclid<const DEG_DVD: usize, const DEG_DVS: usize, const Q: u64>(
}
/// Convert a vector of AssignedValue to a vector of u64
/// Assumes that each element of AssignedValue can be represented in 8 bytes
///
/// * Assumes that each element of AssignedValue can be represented in 8 bytes
pub fn vec_assigned_to_vec_u64<F: ScalarField>(vec: &Vec<AssignedValue<F>>) -> Vec<u64> {
let mut vec_u64 = Vec::new();