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