1use ark_crypto_primitives::{
  2    crh::{poseidon::CRH, CRHScheme},
  3    sponge::{poseidon::PoseidonConfig, Absorb},
  4};
  5use ark_ec::{CurveGroup, Group};
  6use ark_ff::PrimeField;
  7use ark_poly::DenseMultilinearExtension;
  8use ark_poly::MultilinearExtension;
  9use ark_std::rand::Rng;
 10use ark_std::Zero;
 11
 12use super::Witness;
 13use crate::ccs::CCS;
 14use crate::commitment::CommitmentScheme;
 15use crate::folding::circuits::nonnative::affine::nonnative_affine_to_field_elements;
 16use crate::utils::mle::dense_vec_to_dense_mle;
 17use crate::utils::vec::mat_vec_mul;
 18use crate::Error;
 19
 20/// Linearized Committed CCS instance
 21#[derive(Debug, Clone, Eq, PartialEq)]
 22pub struct LCCCS<C: CurveGroup> {
 23    // Commitment to witness
 24    pub C: C,
 25    // Relaxation factor of z for folded LCCCS
 26    pub u: C::ScalarField,
 27    // Public input/output
 28    pub x: Vec<C::ScalarField>,
 29    // Random evaluation point for the v_i
 30    pub r_x: Vec<C::ScalarField>,
 31    // Vector of v_i
 32    pub v: Vec<C::ScalarField>,
 33}
 34
 35impl<F: PrimeField> CCS<F> {
 36    pub fn to_lcccs<R: Rng, C: CurveGroup, CS: CommitmentScheme<C>>(
 37        &self,
 38        rng: &mut R,
 39        cs_params: &CS::ProverParams,
 40        z: &[C::ScalarField],
 41    ) -> Result<(LCCCS<C>, Witness<C::ScalarField>), Error>
 42    where
 43        // enforce that CCS's F is the C::ScalarField
 44        C: CurveGroup<ScalarField = F>,
 45    {
 46        let w: Vec<C::ScalarField> = z[(1 + self.l)..].to_vec();
 47        // if the commitment scheme is set to be hiding, set the random blinding parameter
 48        let r_w = if CS::is_hiding() {
 49            C::ScalarField::rand(rng)
 50        } else {
 51            C::ScalarField::zero()
 52        };
 53        let C = CS::commit(cs_params, &w, &r_w)?;
 54
 55        let r_x: Vec<C::ScalarField> = (0..self.s).map(|_| C::ScalarField::rand(rng)).collect();
 56
 57        let Mzs: Vec<DenseMultilinearExtension<F>> = self
 58            .M
 59            .iter()
 60            .map(|M_j| Ok(dense_vec_to_dense_mle(self.s, &mat_vec_mul(M_j, z)?)))
 61            .collect::<Result<_, Error>>()?;
 62
 63        // compute v_j
 64        let v: Vec<F> = Mzs
 65            .iter()
 66            .map(|Mz| Mz.evaluate(&r_x).ok_or(Error::EvaluationFail))
 67            .collect::<Result<_, Error>>()?;
 68
 69        Ok((
 70            LCCCS::<C> {
 71                C,
 72                u: C::ScalarField::one(),
 73                x: z[1..(1 + self.l)].to_vec(),
 74                r_x,
 75                v,
 76            },
 77            Witness::<C::ScalarField> { w, r_w },
 78        ))
 79    }
 80}
 81
 82impl<C: CurveGroup> LCCCS<C> {
 83    pub fn dummy(l: usize, t: usize, s: usize) -> LCCCS<C>
 84    where
 85        C::ScalarField: PrimeField,
 86    {
 87        LCCCS::<C> {
 88            C: C::zero(),
 89            u: C::ScalarField::zero(),
 90            x: vec![C::ScalarField::zero(); l],
 91            r_x: vec![C::ScalarField::zero(); s],
 92            v: vec![C::ScalarField::zero(); t],
 93        }
 94    }
 95
 96    /// Perform the check of the LCCCS instance described at section 4.2,
 97    /// notice that this method does not check the commitment correctness
 98    pub fn check_relation(
 99        &self,
100        ccs: &CCS<C::ScalarField>,
101        w: &Witness<C::ScalarField>,
102    ) -> Result<(), Error> {
103        // check CCS relation
104        let z: Vec<C::ScalarField> = [vec![self.u], self.x.clone(), w.w.to_vec()].concat();
105
106        let computed_v: Vec<C::ScalarField> = ccs
107            .M
108            .iter()
109            .map(|M_j| {
110                let Mz_mle = dense_vec_to_dense_mle(ccs.s, &mat_vec_mul(M_j, &z)?);
111                Mz_mle.evaluate(&self.r_x).ok_or(Error::EvaluationFail)
112            })
113            .collect::<Result<_, Error>>()?;
114        if computed_v != self.v {
115            return Err(Error::NotSatisfied);
116        }
117        Ok(())
118    }
119}
120
121impl<C: CurveGroup> LCCCS<C>
122where
123    <C as Group>::ScalarField: Absorb,
124    <C as ark_ec::CurveGroup>::BaseField: ark_ff::PrimeField,
125{
126    /// [`LCCCS`].hash implements the committed instance hash compatible with the gadget
127    /// implemented in nova/circuits.rs::CommittedInstanceVar.hash.
128    /// Returns `H(i, z_0, z_i, U_i)`, where `i` can be `i` but also `i+1`, and `U_i` is the LCCCS.
129    pub fn hash(
130        &self,
131        poseidon_config: &PoseidonConfig<C::ScalarField>,
132        i: C::ScalarField,
133        z_0: Vec<C::ScalarField>,
134        z_i: Vec<C::ScalarField>,
135    ) -> Result<C::ScalarField, Error> {
136        let (C_x, C_y) = nonnative_affine_to_field_elements::<C>(self.C)?;
137
138        CRH::<C::ScalarField>::evaluate(
139            poseidon_config,
140            vec![
141                vec![i],
142                z_0,
143                z_i,
144                C_x,
145                C_y,
146                vec![self.u],
147                self.x.clone(),
148                self.r_x.clone(),
149                self.v.clone(),
150            ]
151            .concat(),
152        )
153        .map_err(|e| Error::Other(e.to_string()))
154    }
155}
156
157#[cfg(test)]
158pub mod tests {
159    use ark_pallas::{Fr, Projective};
160    use ark_std::test_rng;
161    use ark_std::One;
162    use ark_std::UniformRand;
163    use ark_std::Zero;
164    use std::sync::Arc;
165
166    use super::*;
167    use crate::ccs::{
168        r1cs::R1CS,
169        tests::{get_test_ccs, get_test_z},
170    };
171    use crate::commitment::pedersen::Pedersen;
172    use crate::utils::hypercube::BooleanHypercube;
173    use crate::utils::virtual_polynomial::{build_eq_x_r_vec, VirtualPolynomial};
174
175    // method for testing
176    pub fn compute_Ls<C: CurveGroup>(
177        ccs: &CCS<C::ScalarField>,
178        lcccs: &LCCCS<C>,
179        z: &[C::ScalarField],
180    ) -> Vec<VirtualPolynomial<C::ScalarField>> {
181        let eq_rx = build_eq_x_r_vec(&lcccs.r_x).unwrap();
182        let eq_rx_mle = dense_vec_to_dense_mle(ccs.s, &eq_rx);
183
184        let mut Ls = Vec::with_capacity(ccs.t);
185        for M_j in ccs.M.iter() {
186            let mut L = VirtualPolynomial::<C::ScalarField>::new(ccs.s);
187            let mut Mz = vec![dense_vec_to_dense_mle(ccs.s, &mat_vec_mul(M_j, z).unwrap())];
188            Mz.push(eq_rx_mle.clone());
189            L.add_mle_list(
190                Mz.iter().map(|v| Arc::new(v.clone())),
191                C::ScalarField::one(),
192            )
193            .unwrap();
194            Ls.push(L);
195        }
196        Ls
197    }
198
199    #[test]
200    /// Test linearized CCCS v_j against the L_j(x)
201    fn test_lcccs_v_j() {
202        let mut rng = test_rng();
203
204        let n_rows = 2_u32.pow(5) as usize;
205        let n_cols = 2_u32.pow(5) as usize;
206        let r1cs = R1CS::<Fr>::rand(&mut rng, n_rows, n_cols);
207        let ccs = CCS::from_r1cs(r1cs);
208        let z: Vec<Fr> = (0..n_cols).map(|_| Fr::rand(&mut rng)).collect();
209
210        let (pedersen_params, _) =
211            Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
212
213        let (lcccs, _) = ccs
214            .to_lcccs::<_, Projective, Pedersen<Projective>>(&mut rng, &pedersen_params, &z)
215            .unwrap();
216        // with our test vector coming from R1CS, v should have length 3
217        assert_eq!(lcccs.v.len(), 3);
218
219        let vec_L_j_x = compute_Ls(&ccs, &lcccs, &z);
220        assert_eq!(vec_L_j_x.len(), lcccs.v.len());
221
222        for (v_i, L_j_x) in lcccs.v.into_iter().zip(vec_L_j_x) {
223            let sum_L_j_x = BooleanHypercube::new(ccs.s)
224                .map(|y| L_j_x.evaluate(&y).unwrap())
225                .fold(Fr::zero(), |acc, result| acc + result);
226            assert_eq!(v_i, sum_L_j_x);
227        }
228    }
229
230    /// Given a bad z, check that the v_j should not match with the L_j(x)
231    #[test]
232    fn test_bad_v_j() {
233        let mut rng = test_rng();
234
235        let ccs = get_test_ccs();
236        let z = get_test_z(3);
237        ccs.check_relation(&z.clone()).unwrap();
238
239        // Mutate z so that the relation does not hold
240        let mut bad_z = z.clone();
241        bad_z[3] = Fr::zero();
242        assert!(ccs.check_relation(&bad_z.clone()).is_err());
243
244        let (pedersen_params, _) =
245            Pedersen::<Projective>::setup(&mut rng, ccs.n - ccs.l - 1).unwrap();
246        // Compute v_j with the right z
247        let (lcccs, _) = ccs
248            .to_lcccs::<_, Projective, Pedersen<Projective>>(&mut rng, &pedersen_params, &z)
249            .unwrap();
250        // with our test vector coming from R1CS, v should have length 3
251        assert_eq!(lcccs.v.len(), 3);
252
253        // Bad compute L_j(x) with the bad z
254        let vec_L_j_x = compute_Ls(&ccs, &lcccs, &bad_z);
255        assert_eq!(vec_L_j_x.len(), lcccs.v.len());
256
257        // Make sure that the LCCCS is not satisfied given these L_j(x)
258        // i.e. summing L_j(x) over the hypercube should not give v_j for all j
259        let mut satisfied = true;
260        for (v_i, L_j_x) in lcccs.v.into_iter().zip(vec_L_j_x) {
261            let sum_L_j_x = BooleanHypercube::new(ccs.s)
262                .map(|y| L_j_x.evaluate(&y).unwrap())
263                .fold(Fr::zero(), |acc, result| acc + result);
264            if v_i != sum_L_j_x {
265                satisfied = false;
266            }
267        }
268        assert!(!satisfied);
269    }
270}