1/// Implementation of [HyperNova](https://eprint.iacr.org/2023/573.pdf) NIMFS verifier circuit
  2use ark_ff::PrimeField;
  3use ark_r1cs_std::{
  4    alloc::AllocVar,
  5    fields::{fp::FpVar, FieldVar},
  6};
  7use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError};
  8
  9use crate::ccs::CCS;
 10use crate::folding::circuits::utils::EqEvalGadget;
 11
 12/// computes c from the step 5 in section 5 of HyperNova, adapted to multiple LCCCS & CCCS
 13/// instances:
 14/// $$
 15/// c = \sum_{i \in [\mu]} \left(\sum_{j \in [t]} \gamma^{i \cdot t + j} \cdot e_i \cdot \sigma_{i,j} \right)
 16/// + \sum_{k \in [\nu]} \gamma^{\mu \cdot t+k} \cdot e_k \cdot \left( \sum_{i=1}^q c_i \cdot \prod_{j \in S_i}
 17/// \theta_{k,j} \right)
 18/// $$
 19#[allow(dead_code)] // TMP while the other circuits are not ready
 20#[allow(clippy::too_many_arguments)]
 21fn compute_c_gadget<F: PrimeField>(
 22    cs: ConstraintSystemRef<F>,
 23    ccs: &CCS<F>,
 24    vec_sigmas: Vec<Vec<FpVar<F>>>,
 25    vec_thetas: Vec<Vec<FpVar<F>>>,
 26    gamma: FpVar<F>,
 27    beta: Vec<FpVar<F>>,
 28    vec_r_x: Vec<Vec<FpVar<F>>>,
 29    vec_r_x_prime: Vec<FpVar<F>>,
 30) -> Result<FpVar<F>, SynthesisError> {
 31    let mut e_lcccs = Vec::new();
 32    for r_x in vec_r_x.iter() {
 33        e_lcccs.push(EqEvalGadget::eq_eval(r_x, &vec_r_x_prime)?);
 34    }
 35
 36    let mut c = FpVar::<F>::zero();
 37    let mut current_gamma = FpVar::<F>::one();
 38    for i in 0..vec_sigmas.len() {
 39        for j in 0..ccs.t {
 40            c += current_gamma.clone() * e_lcccs[i].clone() * vec_sigmas[i][j].clone();
 41            current_gamma *= gamma.clone();
 42        }
 43    }
 44
 45    let ccs_c = Vec::<FpVar<F>>::new_constant(cs.clone(), ccs.c.clone())?;
 46    let e_k = EqEvalGadget::eq_eval(&beta, &vec_r_x_prime)?;
 47    #[allow(clippy::needless_range_loop)]
 48    for k in 0..vec_thetas.len() {
 49        let mut sum = FpVar::<F>::zero();
 50        for i in 0..ccs.q {
 51            let mut prod = FpVar::<F>::one();
 52            for j in ccs.S[i].clone() {
 53                prod *= vec_thetas[k][j].clone();
 54            }
 55            sum += ccs_c[i].clone() * prod;
 56        }
 57        c += current_gamma.clone() * e_k.clone() * sum;
 58        current_gamma *= gamma.clone();
 59    }
 60    Ok(c)
 61}
 62
 63#[cfg(test)]
 64mod tests {
 65    use ark_pallas::{Fr, Projective};
 66    use ark_r1cs_std::{alloc::AllocVar, fields::fp::FpVar, R1CSVar};
 67    use ark_relations::r1cs::ConstraintSystem;
 68    use ark_std::{test_rng, UniformRand};
 69
 70    use super::*;
 71    use crate::{
 72        ccs::{
 73            tests::{get_test_ccs, get_test_z},
 74            CCS,
 75        },
 76        commitment::{pedersen::Pedersen, CommitmentScheme},
 77        folding::hypernova::utils::{compute_c, compute_sigmas_and_thetas},
 78    };
 79
 80    #[test]
 81    pub fn test_compute_c_gadget() {
 82        // number of LCCCS & CCCS instances to fold in a single step
 83        let mu = 32;
 84        let nu = 42;
 85
 86        let mut z_lcccs = Vec::new();
 87        for i in 0..mu {
 88            let z = get_test_z(i + 3);
 89            z_lcccs.push(z);
 90        }
 91        let mut z_cccs = Vec::new();
 92        for i in 0..nu {
 93            let z = get_test_z(i + 3);
 94            z_cccs.push(z);
 95        }
 96
 97        let ccs: CCS<Fr> = get_test_ccs();
 98
 99        let mut rng = test_rng();
100        let gamma: Fr = Fr::rand(&mut rng);
101        let beta: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
102        let r_x_prime: Vec<Fr> = (0..ccs.s).map(|_| Fr::rand(&mut rng)).collect();
103
104        let (pedersen_params, _) =
105            Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
106
107        // Create the LCCCS instances out of z_lcccs
108        let mut lcccs_instances = Vec::new();
109        for z_i in z_lcccs.iter() {
110            let (inst, _) = ccs.to_lcccs(&mut rng, &pedersen_params, z_i).unwrap();
111            lcccs_instances.push(inst);
112        }
113        // Create the CCCS instance out of z_cccs
114        let mut cccs_instances = Vec::new();
115        for z_i in z_cccs.iter() {
116            let (inst, _) = ccs.to_cccs(&mut rng, &pedersen_params, z_i).unwrap();
117            cccs_instances.push(inst);
118        }
119
120        let sigmas_thetas = compute_sigmas_and_thetas(&ccs, &z_lcccs, &z_cccs, &r_x_prime);
121
122        let expected_c = compute_c(
123            &ccs,
124            &sigmas_thetas,
125            gamma,
126            &beta,
127            &lcccs_instances
128                .iter()
129                .map(|lcccs| lcccs.r_x.clone())
130                .collect(),
131            &r_x_prime,
132        );
133
134        let cs = ConstraintSystem::<Fr>::new_ref();
135        let mut vec_sigmas = Vec::new();
136        let mut vec_thetas = Vec::new();
137        for sigmas in sigmas_thetas.0 {
138            vec_sigmas
139                .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(sigmas.clone())).unwrap());
140        }
141        for thetas in sigmas_thetas.1 {
142            vec_thetas
143                .push(Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(thetas.clone())).unwrap());
144        }
145        let vec_r_x: Vec<Vec<FpVar<Fr>>> = lcccs_instances
146            .iter()
147            .map(|lcccs| {
148                Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(lcccs.r_x.clone())).unwrap()
149            })
150            .collect();
151        let vec_r_x_prime =
152            Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(r_x_prime.clone())).unwrap();
153        let gamma_var = FpVar::<Fr>::new_witness(cs.clone(), || Ok(gamma)).unwrap();
154        let beta_var = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(beta.clone())).unwrap();
155        let computed_c = compute_c_gadget(
156            cs.clone(),
157            &ccs,
158            vec_sigmas,
159            vec_thetas,
160            gamma_var,
161            beta_var,
162            vec_r_x,
163            vec_r_x_prime,
164        )
165        .unwrap();
166
167        assert_eq!(expected_c, computed_c.value().unwrap());
168    }
169}