Remove witness from CCCS & LCCCS instances

src/ccs/cccs.rs

@@ -34,8 +34,8 @@ use super::CCS;
 #[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
 #[serde(bound = "")]
 pub struct CCCS<G: Group> {
-  // The `z` vector used as input for this instance.
-  pub(crate) z: Vec<G::Scalar>,
+  // The `x` vector represents public IO.
+  pub(crate) x: Option<Vec<G::Scalar>>,
   // Commitment to the witness of `z`.
   pub(crate) w_comm: Commitment<G>,
 }
@@ -48,22 +48,34 @@ impl<G: Group> CCCS<G> {
     z: Vec<G::Scalar>,
     ck: &CommitmentKey<G>,
   ) -> Self {
-    let w_comm = CE::<G>::commit(ck, &z[(1 + ccs.l)..]);
-
     Self {
-      z: z.to_vec(),
-      w_comm,
+      x: if ccs.l == 0 {
+        None
+      } else {
+        Some(z[(1..ccs.l + 1)].to_vec())
+      },
+      w_comm: CE::<G>::commit(ck, &z[(1 + ccs.l)..]),
     }
   }
 
+  pub(crate) fn construct_z(&self, witness: &[G::Scalar]) -> Vec<G::Scalar> {
+    concat(vec![
+      vec![G::Scalar::ONE],
+      self.x.clone().unwrap_or(vec![]),
+      witness.to_vec(),
+    ])
+  }
+
   /// Computes q(x) = \sum^q c_i * \prod_{j \in S_i} ( \sum_{y \in {0,1}^s'} M_j(x, y) * z(y) )
   /// polynomial over x
   pub(crate) fn compute_q(
     &self,
     ccs: &CCS<G>,
     ccs_mles: &[MultilinearPolynomial<G::Scalar>],
+    witness: &[G::Scalar],
   ) -> Result<VirtualPolynomial<G::Scalar>, NovaError> {
-    let z_mle = dense_vec_to_mle::<G::Scalar>(ccs.s_prime, &self.z);
+    let tmp_z = self.construct_z(witness);
+    let z_mle = dense_vec_to_mle::<G::Scalar>(ccs.s_prime, &tmp_z);
     if z_mle.get_num_vars() != ccs.s_prime {
       // this check if redundant if dense_vec_to_mle is correct
       return Err(NovaError::VpArith);
@@ -106,8 +118,9 @@ impl<G: Group> CCCS<G> {
     ccs: &CCS<G>,
     ccs_mles: &[MultilinearPolynomial<G::Scalar>],
     beta: &[G::Scalar],
+    witness: &[G::Scalar],
   ) -> Result<VirtualPolynomial<G::Scalar>, NovaError> {
-    let q = self.compute_q(ccs, ccs_mles)?;
+    let q = self.compute_q(ccs, ccs_mles, witness)?;
     q.build_f_hat(beta)
   }
 
@@ -117,13 +130,14 @@ impl<G: Group> CCCS<G> {
     ccs: &CCS<G>,
     ccs_mles: &[MultilinearPolynomial<G::Scalar>],
     ck: &CommitmentKey<G>,
+    witness: &[G::Scalar],
   ) -> Result<(), NovaError> {
     // check that C is the commitment of w. Notice that this is not verifying a Pedersen
     // opening, but checking that the Commmitment comes from committing to the witness.
-    assert_eq!(self.w_comm, CE::<G>::commit(ck, &self.z[(1 + ccs.l)..]));
+    assert_eq!(self.w_comm, CE::<G>::commit(ck, witness));
 
     // A CCCS relation is satisfied if the q(x) multivariate polynomial evaluates to zero in the hypercube
-    let q_x = self.compute_q(ccs, ccs_mles).unwrap();
+    let q_x = self.compute_q(ccs, ccs_mles, witness).unwrap();
     for x in BooleanHypercube::new(ccs.s) {
       if !q_x.evaluate(&x).unwrap().is_zero().unwrap_u8() == 0 {
         return Err(NovaError::UnSat);
@@ -176,7 +190,7 @@ mod tests {
 
     // Generate CCCS artifacts
     let cccs = CCCS::new(&ccs, &mles, z, &ck);
-    let q = cccs.compute_q(&ccs, &mles).unwrap();
+    let q = cccs.compute_q(&ccs, &mles, &ccs_witness.w).unwrap();
 
     // Evaluate inside the hypercube
     BooleanHypercube::new(ccs.s).for_each(|x| {
@@ -204,7 +218,7 @@ mod tests {
     let beta: Vec<G::Scalar> = (0..ccs.s).map(|_| G::Scalar::random(&mut rng)).collect();
     // Compute Q(x) = eq(beta, x) * q(x).
     let Q = cccs
-      .compute_Q(&ccs, &mles, &beta)
+      .compute_Q(&ccs, &mles, &beta, &ccs_witness.w)
       .expect("Computation of Q should not fail");
 
     // Let's consider the multilinear polynomial G(x) = \sum_{y \in {0, 1}^s} eq(x, y) q(y)
@@ -241,12 +255,12 @@ mod tests {
     // Now test that if we create Q(x) with eq(d,y) where d is inside the hypercube, \sum Q(x) should be G(d) which
     // should be equal to q(d), since G(x) interpolates q(x) inside the hypercube
     let q = cccs
-      .compute_q(&ccs, &mles)
+      .compute_q(&ccs, &mles, &ccs_witness.w)
       .expect("Computing q shoud not fail");
 
     for d in BooleanHypercube::new(ccs.s) {
       let Q_at_d = cccs
-        .compute_Q(&ccs, &mles, &d)
+        .compute_Q(&ccs, &mles, &d, &ccs_witness.w)
         .expect("Computing Q_at_d shouldn't fail");
 
       // Get G(d) by summing over Q_d(x) over the hypercube
@@ -259,7 +273,7 @@ mod tests {
     // Now test that they should disagree outside of the hypercube
     let r: Vec<G::Scalar> = (0..ccs.s).map(|_| G::Scalar::random(&mut rng)).collect();
     let Q_at_r = cccs
-      .compute_Q(&ccs, &mles, &r)
+      .compute_Q(&ccs, &mles, &r, &ccs_witness.w)
       .expect("Computing Q_at_r shouldn't fail");
 
     // Get G(d) by summing over Q_d(x) over the hypercube

src/ccs/lcccs.rs

@@ -34,11 +34,16 @@ use std::sync::Arc;
 #[derive(Clone, Debug, Serialize, Deserialize)]
 #[serde(bound = "")]
 pub struct LCCCS<G: Group> {
+  /// Commitment to witness
   pub(crate) w_comm: Commitment<G>,
+  /// Vector of v_i (result of folding thetas and sigmas).
   pub(crate) v: Vec<G::Scalar>,
-  // Random evaluation point for the v_i
+  /// Random evaluation point for the v_i
   pub(crate) r_x: Vec<G::Scalar>,
-  pub(crate) z: Vec<G::Scalar>,
+  /// Public input/output
+  pub(crate) x: Option<Vec<G::Scalar>>,
+  /// Relaxation factor of z for folded LCCCS
+  pub(crate) u: G::Scalar,
 }
 
 impl<G: Group> LCCCS<G> {
@@ -56,7 +61,28 @@ impl<G: Group> LCCCS<G> {
     // Evaluation points for `v`
     let v = ccs.compute_v_j(&z, &r_x, ccs_m_mle);
 
-    Self { w_comm, v, r_x, z }
+    // Circuit might not have public IO. Hence, if so, we default it to zero.
+    let x = if ccs.l == 0 {
+      None
+    } else {
+      Some(z[1..ccs.l + 1].to_vec())
+    };
+
+    Self {
+      w_comm,
+      v,
+      r_x,
+      u: G::Scalar::ONE,
+      x,
+    }
+  }
+
+  pub(crate) fn construct_z(&self, witness: &[G::Scalar]) -> Vec<G::Scalar> {
+    concat(vec![
+      vec![self.u],
+      self.x.clone().unwrap_or(vec![]),
+      witness.to_vec(),
+    ])
   }
 
   /// Checks if the CCS instance is satisfiable given a witness and its shape
@@ -65,16 +91,19 @@ impl<G: Group> LCCCS<G> {
     ccs: &CCS<G>,
     ccs_m_mle: &[MultilinearPolynomial<G::Scalar>],
     ck: &CommitmentKey<G>,
+    witness: &[G::Scalar],
   ) -> Result<(), NovaError> {
-    dbg!(self.z.clone());
-    let w = &self.z[(1 + ccs.l)..];
     // check that C is the commitment of w. Notice that this is not verifying a Pedersen
     // opening, but checking that the Commmitment comes from committing to the witness.
-    let comm_eq = self.w_comm == CE::<G>::commit(ck, w);
+    let comm_eq = self.w_comm == CE::<G>::commit(ck, witness);
+
+    let computed_v = compute_all_sum_Mz_evals::<G>(
+      ccs_m_mle,
+      &self.construct_z(witness),
+      &self.r_x,
+      ccs.s_prime,
+    );
 
-    let computed_v = compute_all_sum_Mz_evals::<G>(ccs_m_mle, &self.z, &self.r_x, ccs.s_prime);
-    dbg!(self.v.clone());
-    dbg!(computed_v.clone());
     let vs_eq = computed_v == self.v;
 
     if vs_eq && comm_eq {
@@ -89,8 +118,9 @@ impl<G: Group> LCCCS<G> {
     &self,
     ccs: &CCS<G>,
     ccs_m_mle: &[MultilinearPolynomial<G::Scalar>],
+    lcccs_witness: &[G::Scalar],
   ) -> Vec<VirtualPolynomial<G::Scalar>> {
-    let z_mle = dense_vec_to_mle(ccs.s_prime, self.z.as_slice());
+    let z_mle = dense_vec_to_mle(ccs.s_prime, self.construct_z(lcccs_witness).as_slice());
 
     let mut vec_L_j_x = Vec::with_capacity(ccs.t);
     for M_j in ccs_m_mle.iter() {
@@ -124,31 +154,30 @@ mod tests {
     // LCCCS with the correct z should pass
     let r_x: Vec<G::Scalar> = (0..ccs.s).map(|_| G::Scalar::random(&mut OsRng)).collect();
     let mut lcccs = LCCCS::new(&ccs, &mles, &ck, z.clone(), r_x);
-    assert!(lcccs.is_sat(&ccs, &mles, &ck).is_ok());
+    assert!(lcccs.is_sat(&ccs, &mles, &ck, &witness.w).is_ok());
 
-    // Wrong z so that the relation does not hold
-    let mut bad_z = z;
-    bad_z[3] = G::Scalar::ZERO;
+    // Wrong witness so that the relation does not hold
+    let mut bad_witness = witness.w.clone();
+    bad_witness[2] = G::Scalar::ZERO;
 
     // LCCCS with the wrong z should not pass `is_sat`.
-    lcccs.z = bad_z;
-    assert!(lcccs.is_sat(&ccs, &mles, &ck).is_err());
+    assert!(lcccs.is_sat(&ccs, &mles, &ck, &bad_witness).is_err());
   }
 
   fn test_lcccs_v_j_with<G: Group>() {
     let mut rng = OsRng;
 
     // Gen test vectors & artifacts
     let z = CCS::<G>::get_test_z(3);
-    let (ccs, _, _, mles) = CCS::<G>::gen_test_ccs(&z);
+    let (ccs, witness, _, mles) = CCS::<G>::gen_test_ccs(&z);
     let ck = ccs.commitment_key();
 
     let r_x: Vec<G::Scalar> = (0..ccs.s).map(|_| G::Scalar::random(&mut rng)).collect();
 
     // Get LCCCS
     let lcccs = LCCCS::new(&ccs, &mles, &ck, z, r_x);
 
-    let vec_L_j_x = lcccs.compute_Ls(&ccs, &mles);
+    let vec_L_j_x = lcccs.compute_Ls(&ccs, &mles, &witness.w);
     assert_eq!(vec_L_j_x.len(), lcccs.v.len());
 
     for (v_i, L_j_x) in lcccs.v.into_iter().zip(vec_L_j_x) {
@@ -167,22 +196,21 @@ mod tests {
     let (ccs, witness, instance, mles) = CCS::<G>::gen_test_ccs(&z);
     let ck = ccs.commitment_key();
 
-    // Mutate z so that the relation does not hold
-    let mut bad_z = z.clone();
-    bad_z[3] = G::Scalar::ZERO;
+    // Mutate witness so that the relation does not hold
+    let mut bad_witness = witness.w.clone();
+    bad_witness[2] = G::Scalar::ZERO;
 
     // Compute v_j with the right z
     let r_x: Vec<G::Scalar> = (0..ccs.s).map(|_| G::Scalar::random(&mut rng)).collect();
     let mut lcccs = LCCCS::new(&ccs, &mles, &ck, z, r_x);
     // Assert LCCCS is satisfied with the original Z
-    assert!(lcccs.is_sat(&ccs, &mles, &ck).is_ok());
+    assert!(lcccs.is_sat(&ccs, &mles, &ck, &witness.w).is_ok());
 
     // Compute L_j(x) with the bad z
-    lcccs.z = bad_z;
-    let vec_L_j_x = lcccs.compute_Ls(&ccs, &mles);
+    let vec_L_j_x = lcccs.compute_Ls(&ccs, &mles, &bad_witness);
     assert_eq!(vec_L_j_x.len(), lcccs.v.len());
     // Assert LCCCS is not satisfied with the bad Z
-    assert!(lcccs.is_sat(&ccs, &mles, &ck).is_err());
+    assert!(lcccs.is_sat(&ccs, &mles, &ck, &bad_witness).is_err());
 
     // Make sure that the LCCCS is not satisfied given these L_j(x)
     // i.e. summing L_j(x) over the hypercube should not give v_j for all j