feat: add ciphertext addition to circuit

examples/CRISP/circuits/Nargo.toml

@@ -8,6 +8,7 @@ license = "MIT"
 [dependencies]
 greco = { path = "../../../circuits/crates/libs/greco" }
 polynomial = { path = "../../../circuits/crates/libs/polynomial" }
+safe = { path = "../../../circuits/crates/libs/safe" }
 keccak256 = { tag = "v0.1.0", git = "https://github.com/noir-lang/keccak256" }
 poseidon = { tag = "v0.1.1", git = "https://github.com/noir-lang/poseidon" }
 binary_merkle_root = { git = "https://github.com/zk-kit/zk-kit.noir", tag = "binary-merkle-root-v0.0.1", directory = "packages/binary-merkle-root" }

examples/CRISP/circuits/src/ciphertext_addition.nr

@@ -0,0 +1,188 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+//
+// This file contains ciphertext addition verification for BFV ciphertexts.
+
+use greco::CryptographicParams;
+use polynomial::{flatten, Polynomial};
+use safe::SafeSponge;
+
+/// Parameters for ciphertext addition verification.
+///
+/// # Arguments
+/// * `N` - Polynomial degree.
+/// * `L` - Number of CRT bases.
+/// * `BIT_ZERO_CT` - Bit length of the zero ciphertext polynomials.
+/// * `BIT_PREV_CT` - Bit length of the previous ciphertext polynomials.
+/// * `BIT_SUM_CT` - Bit length of the sum ciphertext polynomials.
+pub struct CiphertextAddition<let N: u32, let L: u32, let BIT_ZERO_CT: u32, let BIT_PREV_CT: u32, let BIT_SUM_CT: u32> {
+    crypto_params: CryptographicParams<L>,
+    zero_ct0is: [Polynomial<N>; L],
+    zero_ct1is: [Polynomial<N>; L],
+    prev_ct0is: [Polynomial<N>; L],
+    prev_ct1is: [Polynomial<N>; L],
+    sum_ct0is: [Polynomial<N>; L],
+    sum_ct1is: [Polynomial<N>; L],
+    r0is: [Polynomial<N>; L],
+    r1is: [Polynomial<N>; L],
+}
+
+impl<let N: u32, let L: u32, let BIT_ZERO_CT: u32, let BIT_PREV_CT: u32, let BIT_SUM_CT: u32> CiphertextAddition<N, L, BIT_ZERO_CT, BIT_PREV_CT, BIT_SUM_CT> {
+    /// Creates a new CiphertextAddition instance.
+    ///
+    /// # Arguments
+    /// * `crypto_params` - Cryptographic parameters for the ciphertext addition circuit.
+    /// * `zero_ct0is`, `zero_ct1is` - Zero ciphertext polynomials.
+    /// * `prev_ct0is`, `prev_ct1is` - Previous ciphertext polynomials.
+    /// * `sum_ct0is`, `sum_ct1is` - Ciphertext addition polynomials.
+    /// * `r0is`, `r1is` - Randomness polynomials.
+    pub fn new(
+        crypto_params: CryptographicParams<L>,
+        zero_ct0is: [Polynomial<N>; L],
+        zero_ct1is: [Polynomial<N>; L],
+        prev_ct0is: [Polynomial<N>; L],
+        prev_ct1is: [Polynomial<N>; L],
+        sum_ct0is: [Polynomial<N>; L],
+        sum_ct1is: [Polynomial<N>; L],
+        r0is: [Polynomial<N>; L],
+        r1is: [Polynomial<N>; L],
+    ) -> Self {
+        Self {
+            crypto_params,
+            zero_ct0is,
+            zero_ct1is,
+            prev_ct0is,
+            prev_ct1is,
+            sum_ct0is,
+            sum_ct1is,
+            r0is,
+            r1is,
+        }
+    }
+
+    /// Flattens all polynomials coefficients into a single array for challenge generation.
+    ///
+    /// This function serializes all polynomial coefficients into a 1D array to enable
+    /// the generation of random challenge values using the Fiat-Shamir transform.
+    /// The coefficients are arranged in a specific order to ensure deterministic
+    /// challenge generation.
+    ///
+    /// # Returns
+    /// An array containing all polynomials coefficients in flattened form
+    fn payload(self) -> Vec<Field> {
+        let mut inputs = Vec::new();
+
+        // Flatten zero ciphertext polynomials
+        inputs = flatten::<_, _, BIT_ZERO_CT>(inputs, self.zero_ct0is);
+        inputs = flatten::<_, _, BIT_ZERO_CT>(inputs, self.zero_ct1is);
+
+        // Flatten previous ciphertext polynomials
+        inputs = flatten::<_, _, BIT_PREV_CT>(inputs, self.prev_ct0is);
+        inputs = flatten::<_, _, BIT_PREV_CT>(inputs, self.prev_ct1is);
+
+        // Flatten sum ciphertext polynomials
+        inputs = flatten::<_, _, BIT_SUM_CT>(inputs, self.sum_ct0is);
+        inputs = flatten::<_, _, BIT_SUM_CT>(inputs, self.sum_ct1is);
+
+        // Flatten randomness polynomials
+        inputs = flatten::<_, _, 1>(inputs, self.r0is);
+        inputs = flatten::<_, _, 1>(inputs, self.r1is);
+
+        inputs
+    }
+
+    /// Verifies the correct addition constraints for the ciphertext addition circuit.
+    ///
+    /// This function implements the core zero-knowledge proof by checking:
+    /// 1. Range constraints on all polynomials coefficients
+    /// 2. Correct addition equations
+    ///
+    /// The proof uses the Schwartz-Zippel lemma: if polynomial equations hold
+    /// when evaluated at random points, then the polynomials are identical with
+    /// high probability.
+    ///
+    /// # Addition Equations
+    /// For each CRT basis i:
+    /// * sum0i(gamma) = zero_ct0i(gamma) + prev_ct0i(gamma) + r0i(gamma) * qi
+    /// * sum1i(gamma) = zero_ct1i(gamma) + prev_ct1i(gamma) + r1i(gamma) * qi
+    ///
+    /// Where:
+    /// * qi are constants from the cryptographic parameters
+    /// * r0i, r1i are the correction terms for each i-th CRT basis.
+    pub fn verify_correct_ciphertext_addition(self) {
+        // Step 1: Perform range checks on all polynomial coefficients
+        self.check_range_bounds();
+
+        // Step 2: Generate Fiat-Shamir challenges
+        let gammas = self.generate_challenge();
+
+        // Step 3: Verify ciphertext addition constraints using challenges
+        self.check_ciphertext_addition_constraints(gammas);
+    }
+
+    /// Verifies range constraints on r0is and r1is.
+    fn check_range_bounds(self) {
+        for i in 0..L {
+            // For M=2 (adding two ciphertexts), each coefficient of the quotient polynomial.
+            // must be in {-1, 0, 1}, so the bound will always be 1 for all CRT moduli.
+            self.r0is[i].range_check_1bound::<1>(1);
+            self.r1is[i].range_check_1bound::<1>(1);
+        }
+    }
+
+    /// Generates Fiat-Shamir challenge values using a cryptographic sponge
+    ///
+    /// The sponge absorbs all witness values and squeezes out deterministic random field elements
+    /// that will be used to evaluate polynomials for the Schwartz-Zippel lemma.
+    ///
+    /// # Returns
+    /// Vector of challenge values [gamma_0, gamma_1, ..., gamma_{2L-1}]
+    fn generate_challenge(self) -> Vec<Field> {
+        let inputs = self.payload();
+
+        // Domain separator for ciphertext addition circuit - "CiphertextAddition" in hex
+        let domain_separator = [
+            0x43, 0x69, 0x70, 0x68, 0x65, 0x72, 0x74, 0x65, 0x78, 0x74, 0x41, 0x64, 0x64, 0x69,
+            0x74, 0x69, 0x6f, 0x6e, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+            0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+            0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+            0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+        ];
+
+        // IO Pattern: ABSORB(input_size), SQUEEZE(2*L)
+        let input_size = inputs.len();
+        let io_pattern = [0x80000000 | input_size, 0x00000000 | (2 * L)];
+
+        let mut sponge = SafeSponge::start(io_pattern, domain_separator);
+        sponge.absorb(inputs);
+        let gammas = sponge.squeeze();
+        sponge.finish();
+        gammas
+    }
+
+    /// Verifies ciphertext addition constraints using Fiat-Shamir challenges.
+    ///
+    /// # Arguments
+    /// * `gammas` - Vector of challenge values [gamma_0, gamma_1, ..., gamma_{2L-1}]
+    fn check_ciphertext_addition_constraints(self, gammas: Vec<Field>) {
+        for i in 0..L {
+            let gamma_i = gammas.get(i);
+
+            let sum0 = self.sum_ct0is[i].eval(gamma_i);
+            let sum1 = self.sum_ct1is[i].eval(gamma_i);
+
+            let ct0 = self.zero_ct0is[i].eval(gamma_i);
+            let ct1 = self.zero_ct1is[i].eval(gamma_i);
+
+            let old0 = self.prev_ct0is[i].eval(gamma_i);
+            let old1 = self.prev_ct1is[i].eval(gamma_i);
+
+            let q_i = self.crypto_params.qis[i];
+
+            let radd0 = self.r0is[i].eval(gamma_i);
+            let radd1 = self.r1is[i].eval(gamma_i);
+
+            assert(sum0 == ct0 + old0 + radd0 * q_i);
+            assert(sum1 == ct1 + old1 + radd1 * q_i);
+        }
+    }
+}

examples/CRISP/circuits/src/main.nr

@@ -7,6 +7,8 @@
 use greco::{Greco, Params};
 use polynomial::Polynomial;
 
+mod ciphertext_addition;
+use ciphertext_addition::CiphertextAddition;
 mod ecdsa;
 use ecdsa::{address_to_field, derive_address, verify_signature};
 mod merkle_tree;
@@ -15,6 +17,14 @@ mod utils;
 use utils::check_coefficient_values;
 
 fn main(
+    // Ciphertext Addition Section.
+    prev_ct0is: pub [Polynomial<2048>; 1],
+    prev_ct1is: pub [Polynomial<2048>; 1],
+    sum_ct0is: [Polynomial<2048>; 1],
+    sum_ct1is: [Polynomial<2048>; 1],
+    sum_r0is: [Polynomial<2048>; 1],
+    sum_r1is: [Polynomial<2048>; 1],
+    // Greco Section.
     params: pub Params<2048, 1>,
     pk0is: pub [Polynomial<2048>; 1],
     pk1is: pub [Polynomial<2048>; 1],
@@ -28,15 +38,18 @@ fn main(
     r2is: [Polynomial<2047>; 1],
     p1is: [Polynomial<4095>; 1],
     p2is: [Polynomial<2047>; 1],
+    // ECDSA Section.
     public_key_x: [u8; 32],
     public_key_y: [u8; 32],
     signature: [u8; 64],
     hashed_message: [u8; 32],
-    balance: Field,
+    // Merkle Tree Section.
     merkle_root: pub Field,
     merkle_proof_length: u32,
     merkle_proof_indices: [u1; 20],
     merkle_proof_siblings: [Field; 20],
+    // Balance Section.
+    balance: Field,
 ) {
     // First verify the signature.
     let is_signature_valid =
@@ -61,8 +74,7 @@ fn main(
         is_voter = true;
     }
 
-    // then verify that the vote was encrypted correctly
-    let circuit: Greco<2048, 1, 54, 54, 5, 5, 20, 20, 54, 16, 54> = Greco::new(
+    let greco: Greco<2048, 1, 54, 54, 5, 5, 20, 20, 54, 16, 54> = Greco::new(
         params,
         pk0is,
         pk1is,
@@ -78,7 +90,20 @@ fn main(
         p2is,
     );
 
-    check_coefficient_values(k1, params.crypto_params().q_mod_t);
+    let ct_add: CiphertextAddition<2048, 1, 54, 54, 54> = CiphertextAddition::new(
+        params.crypto_params(),
+        ct0is,
+        ct1is,
+        prev_ct0is,
+        prev_ct1is,
+        sum_ct0is,
+        sum_ct1is,
+        sum_r0is,
+        sum_r1is,
+    );
 
-    circuit.verify_correct_ciphertext_encryption();
+    greco.verify_correct_ciphertext_encryption();
+    ct_add.verify_correct_ciphertext_addition();
+
+    check_coefficient_values(k1, params.crypto_params().q_mod_t);
 }

examples/CRISP/crates/zk-inputs/src/ciphertext_addition.rs

@@ -30,7 +30,6 @@ pub struct CiphertextAdditionInputs {
     pub sum_ct1is: Vec<Vec<BigInt>>,
     pub r0is: Vec<Vec<BigInt>>,
     pub r1is: Vec<Vec<BigInt>>,
-    pub r_bound: u64,
 }
 
 impl CiphertextAdditionInputs {
@@ -47,7 +46,6 @@ impl CiphertextAdditionInputs {
             sum_ct1is: vec![vec![BigInt::zero(); degree]; num_moduli],
             r0is: vec![vec![BigInt::zero(); degree]; num_moduli],
             r1is: vec![vec![BigInt::zero(); degree]; num_moduli],
-            r_bound: 0,
         }
     }
 
@@ -93,10 +91,6 @@ impl CiphertextAdditionInputs {
         // Initialize matrices to store results.
         let mut res = CiphertextAdditionInputs::new(params.moduli().len(), n as usize);
 
-        // For M=2 (adding two ciphertexts), each coefficient of the quotient polynomial.
-        // must be in {-1, 0, 1}, so the bound is 1 for all CRT moduli.
-        let r_bound = 1u64;
-
         let prev_ct0_coeffs = prev_ct0.coefficients();
         let prev_ct1_coeffs = prev_ct1.coefficients();
         let ct0_coeffs = ct0.coefficients();
@@ -232,9 +226,6 @@ impl CiphertextAdditionInputs {
             res.r1is[i] = r1i;
         }
 
-        // Set the bound for the quotient polynomials.
-        res.r_bound = r_bound;
-
         Ok(res)
     }
 
@@ -251,7 +242,6 @@ impl CiphertextAdditionInputs {
             sum_ct1is: reduce_coefficients_2d(&self.sum_ct1is, zkp_modulus),
             r0is: reduce_coefficients_2d(&self.r0is, zkp_modulus),
             r1is: reduce_coefficients_2d(&self.r1is, zkp_modulus),
-            r_bound: self.r_bound,
         }
     }
 }
@@ -294,7 +284,6 @@ mod tests {
         assert_eq!(inputs.sum_ct1is.len(), 2);
         assert_eq!(inputs.r0is.len(), 2);
         assert_eq!(inputs.r1is.len(), 2);
-        assert_eq!(inputs.r_bound, 0);
     }
 
     #[test]
@@ -326,7 +315,6 @@ mod tests {
         assert_eq!(inputs.sum_ct1is.len(), 1);
         assert_eq!(inputs.r0is.len(), 1);
         assert_eq!(inputs.r1is.len(), 1);
-        assert_eq!(inputs.r_bound, 1);
     }
 
     #[test]
@@ -345,6 +333,5 @@ mod tests {
 
         // Verify structure is preserved.
         assert_eq!(standard_form.prev_ct0is.len(), inputs.prev_ct0is.len());
-        assert_eq!(standard_form.r_bound, inputs.r_bound);
     }
 }

examples/CRISP/crates/zk-inputs/src/lib.rs

@@ -335,11 +335,17 @@ mod tests {
 
         // Check required top-level fields.
         assert!(parsed.get("params").is_some());
+        assert!(parsed.get("prev_ct0is").is_some());
+        assert!(parsed.get("prev_ct1is").is_some());
+        assert!(parsed.get("sum_ct0is").is_some());
+        assert!(parsed.get("sum_ct1is").is_some());
+        assert!(parsed.get("sum_r0is").is_some());
+        assert!(parsed.get("sum_r1is").is_some());
+        assert!(parsed.get("sum_r_bound").is_some());
         assert!(parsed.get("ct0is").is_some());
         assert!(parsed.get("ct1is").is_some());
         assert!(parsed.get("pk0is").is_some());
         assert!(parsed.get("pk1is").is_some());
-        assert!(parsed.get("ct_add").is_some());
     }
 
     #[test]
@@ -362,7 +368,7 @@ mod tests {
 
         // Test that same vote produces different ciphertexts (due to randomness).
         let ct0_2 = generator
-            .encrypt_vote(&public_key, create_vote_vector(DEFAULT_DEGREE))
+            .encrypt_vote(&public_key, create_vote_vector())
             .expect("Failed to encrypt vote 0 again");
         assert_ne!(ct0, ct0_2);