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

feat: add constrain_poly_mul using Challenge API (#10)

Browse Source 
* feat: add `constrain_poly_mul` using Challenge API

* chore: fix conflicts merging errors

* feat: added polynomials to `make_public` and enforced equality constraint on `c0` and `c1`

* feat: remove `poly_mul_equal_deg`

* chore: add further explanation on `Challenge API`

* fix: constraints on polynomial length

* chore: update `README`

* fix: overflow bug on `poly_mul`

* chore: update `benches`
This commit is contained in:
enrico.eth
2023-11-16 18:26:36 +01:00
committed by GitHub
parent da6cb27d3f
commit 378fe40330
7 changed files with 693 additions and 470 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
Cargo.toml
View File

@@ -6,6 +6,7 @@ edition = "2021"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
axiom-eth = { git = "https://github.com/axiom-crypto/axiom-eth.git", branch = "community-edition", default-features = false, features = ["halo2-axiom", "aggregation", "evm", "clap"] }
halo2-base = { git = "https://github.com/axiom-crypto/halo2-lib", tag = "v0.3.0-ce" }
halo2-scaffold = {git = "https://github.com/axiom-crypto/halo2-scaffold" }
clap = { version = "=4.1", features = ["derive"] }
@@ -14,5 +15,31 @@ env_logger = "=0.10"
rand = "0.8"
num-bigint = "0.4"
# Dev / testing mode. We make opt-level = 3 to improve proving times (otherwise it is really slow)
[profile.dev]
opt-level = 3
debug = 1 # change to 0 or 2 for more or less debug info
overflow-checks = true # default
incremental = true # default
# Local "release" mode, more optimized than dev but faster to compile than release
[profile.local]
inherits = "dev"
opt-level = 3
# Set this to 1 or 2 to get more useful backtraces
debug = 1
debug-assertions = false
panic = 'unwind'
# better recompile times
incremental = true
lto = "thin"
codegen-units = 16
[profile.release]
opt-level = 3
debug = false
debug-assertions = false
lto = "fat"
panic = "abort"
incremental = false

13
README.md
View File

@@ -9,7 +9,7 @@ The application is not production ready and is only meant to be used for educati
**Mock Prover**
`LOOKUP_BITS=8 cargo run --example bfv -- --name bfv -k 9 --input bfv.in mock`
`cargo run --example bfv -- --name bfv -k 9 --input bfv.in mock`
The `MockProver` does not run the cryptographic prover on your circuit, but instead directly checks if constraints are satisfied. This is useful for testing purposes, and runs faster than the actual prover.
@@ -20,7 +20,7 @@ The `MockProver` does not run the cryptographic prover on your circuit, but inst
**Key Generation**
`LOOKUP_BITS=8 cargo run --example bfv -- --name bfv -k 9 --input bfv.in keygen`
`cargo run --example bfv -- --name bfv -k 9 --input bfv.in keygen`
To generate a random universal trusted setup (for testing only!) and the proving and verifying keys for your circuit.
@@ -30,7 +30,7 @@ This will generate a proving key `data/bfv.pk` and a verifying key `data/bfv.vk`
**Proof Generation**
`LOOKUP_BITS=8 cargo run --example bfv -- --name bfv -k 9 --input bfv.in prove`
`cargo run --example bfv -- --name bfv -k 9 --input bfv.in prove`
This creates a SNARK proof, stored as a binary file `data/bfv.snark`, using the inputs read (by default) from `data/halbfvo2_lib.in``. You can specify a different input file with the option `--input filename.in`, which would look for a file at `data/filename.in``.
@@ -38,7 +38,7 @@ Using the same proving key, you can generate proofs for the same ZK circuit on d
**Proof Verification**
`LOOKUP_BITS=8 cargo run --example bfv -- --name bfv -k 9 verify`
`cargo run --example bfv -- --name bfv -k 9 verify`
Verify the proof generated above
@@ -55,7 +55,10 @@ Verify the proof generated above
## Benchmarks
Proving time: 1077s (17.95 minutes) using `bfv_2` as input run on M2 Macbook Pro with 12 cores and 32GB of RAM.
**Proving time: 61s**
**Verification time: 261ms**
Benches run using `bfv_2` run on M2 Macbook Pro with 12 cores and 32GB of RAM.
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.

106
configs/bfv.json
View File

@@ -1,22 +1,98 @@
{
"params": {
"degree": 9,
"num_advice": 8,
"num_lookup_advice": 2,
"degree": 18,
"num_rlc_columns": 1,
"num_range_advice": [
1,
70,
0
],
"num_lookup_advice": [
0,
2,
0
],
"num_fixed": 1,
"unusable_rows": 109,
"keccak_rows_per_round": 50,
"lookup_bits": 8
},
"break_points": [
[
501,
500,
501,
502,
502,
500,
501
"break_points": {
"gate": [
[],
[
262034,
262032,
262034,
262032,
262032,
262034,
262034,
262033,
262033,
262034,
262034,
262032,
262033,
262034,
262034,
262032,
262034,
262034,
262033,
262032,
262034,
262034,
262034,
262034,
262034,
262034,
262034,
262034,
262032,
262034,
262034,
262034,
262033,
262032,
262034,
262032,
262032,
262033,
262034,
262033,
262034,
262033,
262034,
262034,
262034,
262032,
262034,
262034,
262034,
262033,
262034,
262034,
262032,
262033,
262033,
262034,
262034,
262034,
262034,
262034,
262033,
262034,
262032,
262034,
262033,
262034,
262034,
262033,
262034
],
[]
],
[],
[]
]
"rlc": []
}
}

848
examples/bfv.rs
View File

@@ -1,24 +1,18 @@
use std::env::var;
use std::vec;
use axiom_eth::keccak::KeccakChip;
use axiom_eth::{EthChip, Field};
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;
use halo2_base::AssignedValue;
use halo2_base::Context;
use halo2_base::QuantumCell::Constant;
use halo2_scaffold::scaffold::cmd::Cli;
use halo2_scaffold::scaffold::run;
use halo2_base::safe_types::{GateInstructions, RangeInstructions};
use halo2_base::{AssignedValue, Context, QuantumCell::Constant};
use halo2_scaffold::scaffold::{cmd::Cli, run_eth};
use num_bigint::BigUint;
use serde::{Deserialize, Serialize};
use zk_fhe::chips::poly_distribution::{
check_poly_coefficients_in_range, check_poly_from_distribution_chi_key,
};
use zk_fhe::chips::poly_operations::{
poly_add, poly_divide_by_cyclo, poly_mul_equal_deg, poly_reduce, poly_scalar_mul,
constrain_poly_mul, poly_add, poly_divide_by_cyclo, poly_reduce, poly_scalar_mul,
};
use zk_fhe::chips::utils::{big_uint_to_fp, poly_mul};
/// Circuit inputs for BFV encryption operations
///
@@ -58,8 +52,8 @@ use zk_fhe::chips::poly_operations::{
// 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 DEG: usize = 1024;
const Q: u64 = 536870909;
const T: u64 = 7;
const B: u64 = 18;
@@ -71,15 +65,17 @@ pub struct CircuitInput<const DEG: usize, const Q: u64, const T: u64, const B: u
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
pub c0: 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. We constraint equality between c0 and computed_c0 namely the ciphertext generated 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. PUBLIC. Should live in R_q. We constraint equality between c1 and computed_c1 namely the ciphertext generated by the circuit
}
fn bfv_encryption_circuit<F: ScalarField>(
fn bfv_encryption_circuit<F: Field>(
ctx: &mut Context<F>,
_eth_chip: &EthChip<F>,
_keccak: &mut KeccakChip<F>,
input: CircuitInput<DEG, Q, T, B>,
make_public: &mut Vec<AssignedValue<F>>,
) {
) -> impl FnOnce(&mut Context<F>, &mut Context<F>, &EthChip<F>) + Clone {
// assert that the input polynomials have the same degree and this is equal to DEG - 1
assert_eq!(input.pk0.len() - 1, DEG - 1);
assert_eq!(input.pk1.len() - 1, DEG - 1);
@@ -96,8 +92,17 @@ fn bfv_encryption_circuit<F: ScalarField>(
let mut m = vec![];
let mut e0 = vec![];
let mut e1 = vec![];
let mut c0 = vec![];
let mut c1 = vec![];
// Assign the input polynomials to the circuit
// The circuit logic requires to access some random value
// In order to draw randomness within the circuit we use Axiom's Challenge API (https://hackmd.io/@axiom/SJw3p-qX3)
// Challenge API requires a Phase 0 of witness generation. A commitment from the witness generated during Phase 0 is then hashed to generate the random value according to Fiat-Shamir heuristic.
// This random challenge can be then used as part of witness generation during Phase 1. We will need this to perform efficient polynomial multiplication.
// Note that if you wanna verify something with the challenge API (eg enforcing polynomial multiplcation)
// the stuffs you verify (namely the input polynomials) must be assigned in phase 0 so their values can be part of the Phase 0 commtiment and contribute to Gamma.
// Phase 0: Assign the input polynomials to the circuit witness table
// Using a for loop from 0 to DEG - 1 enforces that the assigned input polynomials have the same degree and this is equal to DEG - 1
for i in 0..DEG {
let pk0_val = F::from(input.pk0[i]);
@@ -106,6 +111,8 @@ fn bfv_encryption_circuit<F: ScalarField>(
let m_val = F::from(input.m[i]);
let e0_val = F::from(input.e0[i]);
let e1_val = F::from(input.e1[i]);
let c0_val = F::from(input.c0[i]);
let c1_val = F::from(input.c1[i]);
let pk0_assigned_value = ctx.load_witness(pk0_val);
let pk1_assigned_value = ctx.load_witness(pk1_val);
@@ -113,6 +120,8 @@ fn bfv_encryption_circuit<F: ScalarField>(
let m_assigned_value = ctx.load_witness(m_val);
let e0_assigned_value = ctx.load_witness(e0_val);
let e1_assigned_value = ctx.load_witness(e1_val);
let c0_assigned_value = ctx.load_witness(c0_val);
let c1_assigned_value = ctx.load_witness(c1_val);
pk0.push(pk0_assigned_value);
pk1.push(pk1_assigned_value);
@@ -120,6 +129,8 @@ fn bfv_encryption_circuit<F: ScalarField>(
m.push(m_assigned_value);
e0.push(e0_assigned_value);
e1.push(e1_assigned_value);
c0.push(c0_assigned_value);
c1.push(c1_assigned_value);
}
assert!(pk0.len() - 1 == DEG - 1);
@@ -128,18 +139,11 @@ fn bfv_encryption_circuit<F: ScalarField>(
assert!(m.len() - 1 == DEG - 1);
assert!(e0.len() - 1 == DEG - 1);
assert!(e1.len() - 1 == DEG - 1);
assert!(c0.len() - 1 == DEG - 1);
assert!(c1.len() - 1 == DEG - 1);
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"))
.parse()
.unwrap();
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
@@ -164,366 +168,462 @@ fn bfv_encryption_circuit<F: ScalarField>(
assert!(cyclo.len() - 1 == DEG);
/* 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
// Assign the length of the input polynomials pk0 and u to the circuit. This is equal to DEG
let poly_len = ctx.load_witness(F::from(DEG as u64));
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-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
*/
// Compute the polynomial pk0 * u outside the circuit
let pk0_u_u64 = poly_mul(&input.pk0, &input.u);
/* constraint on e1
Same as e0
*/
// Assign the polynomial pk0_u_u64 to the circuit
let mut pk0_u = vec![];
// Assumption for the chip is that B < Q which is satisfied by circuit assumption
check_poly_coefficients_in_range::<{ DEG - 1 }, Q, B, F>(ctx, &e0, &range);
check_poly_coefficients_in_range::<{ DEG - 1 }, Q, B, F>(ctx, &e1, &range);
/* 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 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, range.gate());
/* 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:
- Perform a range check on the coefficients of m to be in the [0, T/2] OR [Q - T/2, Q - 1] range
- The assignment for loop above guarantees that the degree of m is DEG - 1
*/
check_poly_coefficients_in_range::<{ DEG - 1 }, Q, { T / 2 }, F>(ctx, &m, &range);
// 1. COMPUTE C0 (c0 is the first ciphertext component)
// pk0 * u
// Perform the polynomial multiplication between pk0 and 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 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, &u, &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 q = BigUint::from(Q as u64);
let deg = BigUint::from(DEG as u64);
let q_minus_1 = q - 1u64;
let binary_representation = format!("{:b}", (q_minus_1.clone() * q_minus_1 * deg));
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-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, &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
// 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));
// This should be a polynomial of degree 2*(DEG - 1)
// Using a for loop from 0 to 2*(DEG - 1) enforces that pk0_u has degree equal to 2*(DEG - 1)
for item in pk0_u_u64.iter().take(2 * (DEG - 1) + 1) {
let pk0_u_val = big_uint_to_fp(&item);
let pk0_u_assigned_value = ctx.load_witness(pk0_u_val);
pk0_u.push(pk0_u_assigned_value);
}
// Therefore, we can safely trim the first DEG - 1 coefficients from pk0_u
assert!(pk0_u.len() - 1 == 2 * (DEG - 1));
let mut pk0_u_trimmed = vec![];
for i in DEG - 1..pk0_u.len() {
pk0_u_trimmed.push(pk0_u[i]);
// Assign the length of the polynomial pk0_u to the circuit -> this is equal to 2*(DEG - 1) + 1
let pk_u_len = ctx.load_witness(F::from((2 * (DEG - 1) + 1) as u64));
// Compute the polynomial pk1 * u outside the circuit
let pk1_u_u64 = poly_mul(&input.pk1, &input.u);
// Assign the polynomial pk1_u_u64 to the circuit
let mut pk1_u = vec![];
// This should be a polynomial of degree 2*(DEG - 1)
// Using a for loop from 0 to 2*(DEG - 1) enforces that pk1_u has degree equal to 2*(DEG - 1)
for item in pk1_u_u64.iter().take(2 * (DEG - 1) + 1) {
let pk1_u_val = big_uint_to_fp(&item);
let pk1_u_assigned_value = ctx.load_witness(pk1_u_val);
pk1_u.push(pk1_u_assigned_value);
}
// 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!
// m * delta
// Perform the polynomial scalar multiplication between m and delta.
// 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 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, &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
// 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.
// 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 `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.
// 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());
// 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);
// 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
// c0 is a polynomial in the R_q ring!
// 1. COMPUTE C1 (c1 is the second ciphertext component)
// pk1 * u
// Perform the polynomial multiplication between pk1 and 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 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, &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-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, &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
// 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!
// c1 = pk1_u_trimmed + e1
// 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.
let c1 = poly_add::<{ DEG - 1 }, F>(ctx, &pk1_u_trimmed, &e1, range.gate());
// 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
// Check outside the circuit that the remainder matches the expected one
for i in 0..DEG {
assert_eq!(*c0[i].value(), F::from(input.c0[i]));
assert_eq!(*c1[i].value(), F::from(input.c1[i]));
}
// Expose to the public the coefficients of c0 and c1
for i in 0..DEG {
make_public.push(c0[i]);
}
for i in 0..DEG {
make_public.push(c1[i]);
}
assert!(pk1_u.len() - 1 == 2 * (DEG - 1));
// Expose to the public pk0 and pk1
for i in 0..DEG {
make_public.push(pk0[i]);
for &assigned_coefficient_pk0 in pk0.iter().take(DEG) {
make_public.push(assigned_coefficient_pk0);
}
for i in 0..DEG {
make_public.push(pk1[i]);
for &assigned_coefficient_pk1 in pk1.iter().take(DEG) {
make_public.push(assigned_coefficient_pk1);
}
// Expose to the public c0 and c1
for &assigned_coefficient_c0 in c0.iter().take(DEG) {
make_public.push(assigned_coefficient_c0);
}
for &assigned_coefficient_c1 in c1.iter().take(DEG) {
make_public.push(assigned_coefficient_c1);
}
// Expose to the public `cyclo`
for i in 0..DEG + 1 {
make_public.push(cyclo[i]);
for &assigned_coefficient_cyclo in cyclo.iter().take(DEG + 1) {
make_public.push(assigned_coefficient_cyclo);
}
// Phase 0 is over, we can now move to Phase 1, in which we will leverage the random challenge generated during Phase 0.
// According to the design of this API, all the constraints must be written inside a callback function.
#[allow(clippy::let_and_return)]
let callback = move |ctx_gate: &mut Context<F>,
ctx_rlc: &mut Context<F>,
eth_chip: &EthChip<F>| {
let range = eth_chip.range();
let rlc = eth_chip.rlc();
/* 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-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
*/
/* constraint on e1
Same as e0
*/
// Assumption for the chip is that B < Q which is satisfied by circuit assumption
check_poly_coefficients_in_range::<{ DEG - 1 }, Q, B, F>(ctx_gate, &e0, range);
check_poly_coefficients_in_range::<{ DEG - 1 }, Q, B, F>(ctx_gate, &e1, range);
/* 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 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_gate, &u, range.gate());
/* 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:
- Perform a range check on the coefficients of m to be in the [0, T/2] OR [Q - T/2, Q - 1] range
- The assignment for loop above guarantees that the degree of m is DEG - 1
*/
check_poly_coefficients_in_range::<{ DEG - 1 }, Q, { T / 2 }, F>(ctx_gate, &m, range);
// 1. COMPUTE C0 (c0 is the first ciphertext component)
// // pk0 * u
// // Perform the polynomial multiplication between pk0 and 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 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_gate, pk0.clone(), u.clone(), range.gate());
// Enforce pk0_u = pk0 * u using `constrain_poly_mul` gate
constrain_poly_mul(
pk0,
poly_len,
u.clone(),
poly_len,
pk0_u.clone(),
pk_u_len,
ctx_gate,
ctx_rlc,
rlc,
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
// get the number of bits needed to represent the value of (Q-1) * (Q-1) * DEG
let q = BigUint::from(Q as u64);
let deg = BigUint::from(DEG as u64);
let q_minus_1 = q - 1u64;
let binary_representation = format!("{:b}", (q_minus_1.clone() * q_minus_1 * deg));
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_gate, &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-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_gate, &pk0_u, &cyclo, 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
// Enforce that the first DEG - 1 coefficients of pk0_u are zeroes
for pk0_u_element in pk0_u.iter().take(DEG - 1) {
let bool = range
.gate()
.is_equal(ctx_gate, *pk0_u_element, Constant(F::from(0)));
range.gate().assert_is_const(ctx_gate, &bool, &F::from(1));
}
// Therefore, we can safely trim the first DEG - 1 coefficients from pk0_u
let pk0_u_trimmed: Vec<_> = pk0_u.iter().skip(DEG - 1).cloned().collect();
// 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!
// m * delta
// Perform the polynomial scalar multiplication between m and delta.
// 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 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_gate,
&m,
&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_gate, &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
// 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.
// 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_gate, &pk0_u_trimmed, &m_delta, range.gate());
// 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_gate,
&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.
// 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 computed_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 computed_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 computed_c0 =
poly_add::<{ DEG - 1 }, F>(ctx_gate, &pk0_u_trimmed_plus_m_delta, &e0, range.gate());
// The coefficients of computed_c0 are in the range [0, 2Q - 2] according to the polynomial addition constraint set above.
// Therefore the coefficients of computed_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 computed_c0 =
poly_reduce::<{ DEG - 1 }, Q, F>(ctx_gate, &computed_c0, 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
// computed_c0 is a polynomial in the R_q ring!
// 1. COMPUTE C1 (c1 is the second ciphertext component)
// pk1 * u
// Perform the polynomial multiplication between pk1 and 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 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_gate, pk1.clone(), u.clone(), range.gate());
// Enforce pk1_u = pk1 * u using `constrain_poly_mul` gate
constrain_poly_mul(
pk1,
poly_len,
u.clone(),
poly_len,
pk1_u.clone(),
pk_u_len,
ctx_gate,
ctx_rlc,
rlc,
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_gate, &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-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_gate, &pk1_u, &cyclo, 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
// Enforce that the first DEG - 1 coefficients of pk1_u are zeroes
for pk1_u_element in pk1_u.iter().take(DEG - 1) {
let bool = range
.gate()
.is_equal(ctx_gate, *pk1_u_element, Constant(F::from(0)));
range.gate().assert_is_const(ctx_gate, &bool, &F::from(1));
}
// Therefore, we can safely trim the first DEG - 1 coefficients from pk1_u
let pk1_u_trimmed: Vec<_> = pk1_u.iter().skip(DEG - 1).cloned().collect();
// 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!
// c1 = pk1_u_trimmed + e1
// 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 computed_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 computed_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.
let computed_c1 = poly_add::<{ DEG - 1 }, F>(ctx_gate, &pk1_u_trimmed, &e1, range.gate());
// The coefficients of computed_c1 are in the range [0, 2Q - 2] according to the polynomial addition constraint set above.
// Therefore the coefficients of computed_c1 are known to have <= `num_bits_3` bits, therefore they satisfy the assumption of the `poly_reduce` chip
// Reduce the coefficients of `computed_c1` by modulo `Q`
let computed_c1 =
poly_reduce::<{ DEG - 1 }, Q, F>(ctx_gate, &computed_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
// computed_c1 is a polynomial in the R_q ring
// Enforce equality between `c0` and `computed_c0` using equality check
// Enfroce equality between `c1` and `computed_c1` using equality check
for i in 0..DEG {
let bool_0 = range.gate().is_equal(ctx_gate, c0[i], computed_c0[i]);
range.gate().assert_is_const(ctx_gate, &bool_0, &F::from(1));
let bool_1 = range.gate().is_equal(ctx_gate, c1[i], computed_c1[i]);
range.gate().assert_is_const(ctx_gate, &bool_1, &F::from(1));
}
};
callback
}
fn main() {
@@ -531,5 +631,5 @@ fn main() {
let args = Cli::parse();
run(bfv_encryption_circuit, args);
run_eth(bfv_encryption_circuit, args);
}

24
src/chips/poly_distribution.rs
View File

@@ -1,11 +1,10 @@
use halo2_base::gates::GateChip;
use halo2_base::safe_types::GateInstructions;
use halo2_base::safe_types::RangeChip;
use halo2_base::safe_types::RangeInstructions;
use halo2_base::utils::ScalarField;
use halo2_base::AssignedValue;
use halo2_base::Context;
use halo2_base::QuantumCell::Constant;
use axiom_eth::Field;
use halo2_base::{
gates::GateChip,
safe_types::{GateInstructions, RangeChip, RangeInstructions},
AssignedValue, Context,
QuantumCell::Constant,
};
/// Enforce that polynomial a of degree DEG has coefficients in the range [0, Z] or [Q-Z, Q-1]
///
@@ -13,12 +12,7 @@ use halo2_base::QuantumCell::Constant;
/// * Q is the modulus of the ring R_q (cipher text space)
/// * Z is the constant that defines the range
/// * Assumes that Z < Q
pub fn check_poly_coefficients_in_range<
const DEG: usize,
const Q: u64,
const Z: u64,
F: ScalarField,
>(
pub fn check_poly_coefficients_in_range<const DEG: usize, const Q: u64, const Z: u64, F: Field>(
ctx: &mut Context<F>,
a: &Vec<AssignedValue<F>>,
range: &RangeChip<F>,
@@ -83,7 +77,7 @@ pub fn check_poly_coefficients_in_range<
/// * Namely, that the coefficients are in the range [0, 1, Q-1].
/// * DEG is the degree of the polynomial
/// * Q is the modulus of the ring R_q (cipher text space)
pub fn check_poly_from_distribution_chi_key<const DEG: usize, const Q: u64, F: ScalarField>(
pub fn check_poly_from_distribution_chi_key<const DEG: usize, const Q: u64, F: Field>(
ctx: &mut Context<F>,
a: &Vec<AssignedValue<F>>,
gate: &GateChip<F>,

111
src/chips/poly_operations.rs
View File

@@ -1,19 +1,19 @@
use crate::chips::utils::{div_euclid, vec_assigned_to_vec_u64};
use halo2_base::gates::GateChip;
use halo2_base::gates::GateInstructions;
use halo2_base::safe_types::RangeChip;
use halo2_base::safe_types::RangeInstructions;
use halo2_base::utils::ScalarField;
use halo2_base::AssignedValue;
use halo2_base::Context;
use halo2_base::QuantumCell;
use axiom_eth::rlp::rlc::RlcChip;
use axiom_eth::Field;
use halo2_base::{
gates::{GateChip, GateInstructions},
safe_types::{RangeChip, RangeInstructions},
AssignedValue, Context, QuantumCell,
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
/// * It assumes that the coefficients are constrained such to overflow during the polynomial addition
pub fn poly_add<const DEG: usize, F: ScalarField>(
pub fn poly_add<const DEG: usize, F: Field>(
ctx: &mut Context<F>,
a: &Vec<AssignedValue<F>>,
b: &Vec<AssignedValue<F>>,
@@ -36,52 +36,50 @@ pub fn poly_add<const DEG: usize, F: ScalarField>(
c
}
/// Build the product of the polynomials a and b as dot product of the coefficients of a and b
/// Enforce that a * b = c
/// This constraint leverages the Axiom's Challenge API
/// The challenge API allows us to access a random challenge gamma inside the circuit.
/// Any polynomial identity can be checked using gamma. e.g. p(x) = q(x) with high probability if p(gamma) = q(gamma) for a challenge gamma
/// because a random gamma has vanishing probability of being a root of p(x) - q(x).
/// Analogously, we can check the identity a(gamma) * b(gamma) = c(gamma) for a random gamma.
///
/// * 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>>,
b: &Vec<AssignedValue<F>>,
/// Complexity:
/// Computing the polynomial multiplication using the direct method would take O(N^2) constraints
/// This algorithm takes O(N) constraints as it requires to:
/// - Evaluate the polynomials a, b and c at gamma (3N constraints)
/// - Enforce the identity a(gamma) * b(gamma) - c(gamma) = 0 (1 constraint)
pub fn constrain_poly_mul<F: Field>(
a_assigned: Vec<AssignedValue<F>>,
a_len: AssignedValue<F>,
b_assigned: Vec<AssignedValue<F>>,
b_len: AssignedValue<F>,
c_assigned: Vec<AssignedValue<F>>,
c_len: AssignedValue<F>,
ctx_gate: &mut Context<F>,
ctx_rlc: &mut Context<F>,
rlc: &RlcChip<F>,
gate: &GateChip<F>,
) -> Vec<AssignedValue<F>> {
// assert that the input polynomials have the same degree and this is equal to DEG
assert_eq!(a.len() - 1, b.len() - 1);
assert_eq!(a.len() - 1, DEG);
) {
// `compute_rlc` evaluates the polynomial at gamma and returns the evaluation
let poly_a_trace = rlc.compute_rlc((ctx_gate, ctx_rlc), gate, a_assigned, a_len);
let poly_a_eval_assigned = poly_a_trace.rlc_val;
let mut c = vec![];
let poly_b_trace = rlc.compute_rlc((ctx_gate, ctx_rlc), gate, b_assigned, b_len);
let poly_b_eval_assigned = poly_b_trace.rlc_val;
for i in 0..(2 * DEG + 1) {
let mut coefficient_accumaltor = vec![];
let poly_c_trace = rlc.compute_rlc((ctx_gate, ctx_rlc), gate, c_assigned, c_len);
let poly_c_eval_assigned = poly_c_trace.rlc_val;
if i < (DEG + 1) {
for a_idx in 0..=i {
let a_coef = a[a_idx];
let b_coef = b[(i - a_idx)];
coefficient_accumaltor.push(gate.mul(ctx, a_coef, b_coef));
}
} else {
for a_idx in (i - DEG)..=DEG {
let a_coef = a[a_idx];
let b_coef = b[(i - a_idx)];
coefficient_accumaltor.push(gate.mul(ctx, a_coef, b_coef));
}
}
let c_val = coefficient_accumaltor
.iter()
.fold(ctx.load_witness(F::zero()), |acc, x| gate.add(ctx, acc, *x));
c.push(c_val);
}
// assert that the product polynomial has degree 2*DEG
assert_eq!(c.len() - 1, 2 * DEG);
c
// enforce gate a(gamma) * b(gamma) - c(gamma) = 0
ctx_gate.assign_region(
[
Constant(F::from(0)),
Existing(poly_a_eval_assigned),
Existing(poly_b_eval_assigned),
Existing(poly_c_eval_assigned),
],
[0],
);
}
/// Build the product of the polynomials a and b as dot product of the coefficients of a and b
@@ -89,7 +87,7 @@ pub fn poly_mul_equal_deg<const DEG: usize, F: ScalarField>(
/// * 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>(
pub fn poly_mul_diff_deg<F: Field>(
ctx: &mut Context<F>,
a: &Vec<AssignedValue<F>>,
b: &Vec<AssignedValue<F>>,
@@ -132,7 +130,7 @@ pub fn poly_mul_diff_deg<F: ScalarField>(
/// * 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>(
pub fn poly_scalar_mul<const DEG: usize, F: Field>(
ctx: &mut Context<F>,
a: &Vec<AssignedValue<F>>,
b: &QuantumCell<F>,
@@ -159,7 +157,7 @@ pub fn poly_scalar_mul<const DEG: usize, F: ScalarField>(
/// * 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>(
pub fn poly_reduce<const DEG: usize, const Q: u64, F: Field>(
ctx: &mut Context<F>,
input: &Vec<AssignedValue<F>>,
range: &RangeChip<F>,
@@ -195,12 +193,7 @@ pub fn poly_reduce<const DEG: usize, const Q: u64, F: ScalarField>(
/// * 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,
const Q: u64,
F: ScalarField,
>(
pub fn poly_divide_by_cyclo<const DEG_DVD: usize, const DEG_DVS: usize, const Q: u64, F: Field>(
ctx: &mut Context<F>,
dividend: &Vec<AssignedValue<F>>,
divisor: &Vec<AssignedValue<F>>,

34
src/chips/utils.rs
View File

@@ -1,8 +1,9 @@
use halo2_base::{utils::ScalarField, AssignedValue};
use num_bigint::BigUint;
/// 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
@@ -87,7 +88,7 @@ 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
pub fn vec_assigned_to_vec_u64<F: ScalarField>(vec: &Vec<AssignedValue<F>>) -> Vec<u64> {
let mut vec_u64 = Vec::new();
@@ -104,3 +105,32 @@ pub fn vec_assigned_to_vec_u64<F: ScalarField>(vec: &Vec<AssignedValue<F>>) -> V
}
vec_u64
}
/// Performs polynomial multiplication on two polynomials using direct method
/// Returns the product 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
pub fn poly_mul(a: &Vec<u64>, b: &Vec<u64>) -> Vec<BigUint> {
let deg_a = a.len() - 1;
let deg_b = b.len() - 1;
let deg_c = deg_a + deg_b;
// initialize the output polynomial with zeroes
let mut c = vec![BigUint::from(0 as u64); deg_c + 1];
// perform polynomial multiplication
for i in 0..=deg_a {
for j in 0..=deg_b {
c[i + j] += BigUint::from(a[i]) * BigUint::from(b[j]);
}
}
assert!(c.len() == deg_c + 1);
c
}
/// Converts a BigUint to a Field Element
pub fn big_uint_to_fp<F: ScalarField>(big_uint: &BigUint) -> F {
F::from_str_vartime(&big_uint.to_str_radix(10)[..]).unwrap()
}