initial commit

Cargo.toml

@@ -0,0 +1,21 @@
+[package]
+name = "nova"
+version = "0.1.0"
+authors = ["Srinath Setty <srinath@microsoft.com>"]
+edition = "2018"
+description = "Recursive zkSNARKs without trusted setup"
+documentation = "https://docs.rs/nova/"
+readme = "README.md"
+repository = "https://github.com/Microsoft/Nova"
+license-file = "LICENSE"
+keywords = ["Recursive zkSNARKs", "cryptography", "proofs"]
+
+[dependencies]
+curve25519-dalek = {version = "3.0.0", features = ["simd_backend"]}
+merlin = "2.0.0"
+rand = "0.7.3"
+digest = "0.8.1"
+sha3 = "0.8.2"
+rayon = "1.3.0"
+rand_core = { version = "0.5", default-features = false }
+itertools = "0.9.0"

README.md

@@ -1,14 +1,13 @@
-# Project
+# Nova: Recursive SNARKs without trusted setup
 
-> This repo has been populated by an initial template to help get you started. Please
-> make sure to update the content to build a great experience for community-building.
+Nova is a high-speed recursive SNARK (a SNARK is type cryptographic proof system that enables a prover to prove a mathematical statement to a verifier with a short proof and succinct verification, and a recursive SNARK enables producing proofs that prove statements about prior proofs). The details of Nova are described in our [paper](https://eprint.iacr.org/2021/370). Recursive SNARKs including Nova have a wide variety of applications such as constructions of verifiable delay functions (VDFs), succinct blockchains, and incrementally verifiable versions of [verifiable state machines](https://eprint.iacr.org/2020/758.pdf). A distinctive aspect of Nova is that it is the simplest recursive proof system in the literature. Furthermore, it achieves the smallest verifier circuit (a key metric to minimize in this context): the circuit is constant-sized and its size is dominated by two group scalar multiplications.
 
-As the maintainer of this project, please make a few updates:
+This repository provides `libnova,` a Rust library library implementation of Nova. The current release implements the core building blocks in Nova, and future releases will use cycles of elliptic curves to support recursive composition of proofs.
 
-- Improving this README.MD file to provide a great experience
-- Updating SUPPORT.MD with content about this project's support experience
-- Understanding the security reporting process in SECURITY.MD
-- Remove this section from the README
+To run tests, run:
+```rust
+cargo test
+```
 
 ## Contributing
 

SUPPORT.md

@@ -1,25 +1,10 @@
-# TODO: The maintainer of this repo has not yet edited this file
-
-**REPO OWNER**: Do you want Customer Service & Support (CSS) support for this product/project?
-
-- **No CSS support:** Fill out this template with information about how to file issues and get help.
-- **Yes CSS support:** Fill out an intake form at [aka.ms/spot](https://aka.ms/spot). CSS will work with/help you to determine next steps. More details also available at [aka.ms/onboardsupport](https://aka.ms/onboardsupport).
-- **Not sure?** Fill out a SPOT intake as though the answer were "Yes". CSS will help you decide.
-
-*Then remove this first heading from this SUPPORT.MD file before publishing your repo.*
-
 # Support
 
 ## How to file issues and get help  
 
-This project uses GitHub Issues to track bugs and feature requests. Please search the existing 
-issues before filing new issues to avoid duplicates.  For new issues, file your bug or 
+This project uses GitHub Issues to track bugs and feature requests. Please search the existing issues before filing new issues to avoid duplicates.  For new issues, file your bug or 
 feature request as a new Issue.
 
-For help and questions about using this project, please **REPO MAINTAINER: INSERT INSTRUCTIONS HERE 
-FOR HOW TO ENGAGE REPO OWNERS OR COMMUNITY FOR HELP. COULD BE A STACK OVERFLOW TAG OR OTHER
-CHANNEL. WHERE WILL YOU HELP PEOPLE?**.
-
 ## Microsoft Support Policy  
 
-Support for this **PROJECT or PRODUCT** is limited to the resources listed above.
+Support for this project is limited to the resources listed above.

rustfmt.toml

@@ -0,0 +1,5 @@
+edition = "2018"
+tab_spaces = 2
+newline_style = "Unix"
+report_fixme = "Always"
+use_try_shorthand = true

src/commitments.rs

@@ -0,0 +1,221 @@
+use super::errors::NovaError;
+use core::ops::{Add, AddAssign, Mul, MulAssign};
+use curve25519_dalek::traits::VartimeMultiscalarMul;
+use digest::{ExtendableOutput, Input};
+use merlin::Transcript;
+use sha3::Shake256;
+use std::io::Read;
+
+pub type Scalar = curve25519_dalek::scalar::Scalar;
+type GroupElement = curve25519_dalek::ristretto::RistrettoPoint;
+type CompressedGroup = curve25519_dalek::ristretto::CompressedRistretto;
+
+#[derive(Debug)]
+pub struct CommitGens {
+  gens: Vec<GroupElement>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct Commitment {
+  comm: GroupElement,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct CompressedCommitment {
+  comm: CompressedGroup,
+}
+
+impl CommitGens {
+  pub fn new(label: &[u8], n: usize) -> Self {
+    let mut shake = Shake256::default();
+    shake.input(label);
+    let mut reader = shake.xof_result();
+    let mut gens: Vec<GroupElement> = Vec::new();
+    let mut uniform_bytes = [0u8; 64];
+    for _ in 0..n {
+      reader.read_exact(&mut uniform_bytes).unwrap();
+      gens.push(GroupElement::from_uniform_bytes(&uniform_bytes));
+    }
+
+    CommitGens { gens }
+  }
+}
+
+impl Commitment {
+  pub fn compress(&self) -> CompressedCommitment {
+    CompressedCommitment {
+      comm: self.comm.compress(),
+    }
+  }
+}
+
+impl CompressedCommitment {
+  pub fn decompress(&self) -> Result<Commitment, NovaError> {
+    let comm = self.comm.decompress();
+    if comm.is_none() {
+      return Err(NovaError::DecompressionError);
+    }
+    Ok(Commitment {
+      comm: comm.unwrap(),
+    })
+  }
+}
+
+pub trait CommitTrait {
+  fn commit(&self, gens: &CommitGens) -> Commitment;
+}
+
+impl CommitTrait for [Scalar] {
+  fn commit(&self, gens: &CommitGens) -> Commitment {
+    assert_eq!(gens.gens.len(), self.len());
+    Commitment {
+      comm: GroupElement::vartime_multiscalar_mul(self, &gens.gens),
+    }
+  }
+}
+
+pub trait ProofTranscriptTrait {
+  fn append_protocol_name(&mut self, protocol_name: &'static [u8]);
+  fn challenge_scalar(&mut self, label: &'static [u8]) -> Scalar;
+}
+
+impl ProofTranscriptTrait for Transcript {
+  fn append_protocol_name(&mut self, protocol_name: &'static [u8]) {
+    self.append_message(b"protocol-name", protocol_name);
+  }
+
+  fn challenge_scalar(&mut self, label: &'static [u8]) -> Scalar {
+    let mut buf = [0u8; 64];
+    self.challenge_bytes(label, &mut buf);
+    Scalar::from_bytes_mod_order_wide(&buf)
+  }
+}
+
+pub trait AppendToTranscriptTrait {
+  fn append_to_transcript(&self, label: &'static [u8], transcript: &mut Transcript);
+}
+
+impl AppendToTranscriptTrait for CompressedCommitment {
+  fn append_to_transcript(&self, label: &'static [u8], transcript: &mut Transcript) {
+    transcript.append_message(label, self.comm.as_bytes());
+  }
+}
+
+impl<'b> MulAssign<&'b Scalar> for Commitment {
+  fn mul_assign(&mut self, scalar: &'b Scalar) {
+    let result = (self as &Commitment).comm * scalar;
+    *self = Commitment { comm: result };
+  }
+}
+
+impl<'a, 'b> Mul<&'b Scalar> for &'a Commitment {
+  type Output = Commitment;
+  fn mul(self, scalar: &'b Scalar) -> Commitment {
+    Commitment {
+      comm: self.comm * scalar,
+    }
+  }
+}
+
+impl<'a, 'b> Mul<&'b Commitment> for &'a Scalar {
+  type Output = Commitment;
+
+  fn mul(self, comm: &'b Commitment) -> Commitment {
+    Commitment {
+      comm: self * comm.comm,
+    }
+  }
+}
+
+macro_rules! define_mul_variants {
+  (LHS = $lhs:ty, RHS = $rhs:ty, Output = $out:ty) => {
+    impl<'b> Mul<&'b $rhs> for $lhs {
+      type Output = $out;
+      fn mul(self, rhs: &'b $rhs) -> $out {
+        &self * rhs
+      }
+    }
+
+    impl<'a> Mul<$rhs> for &'a $lhs {
+      type Output = $out;
+      fn mul(self, rhs: $rhs) -> $out {
+        self * &rhs
+      }
+    }
+
+    impl Mul<$rhs> for $lhs {
+      type Output = $out;
+      fn mul(self, rhs: $rhs) -> $out {
+        &self * &rhs
+      }
+    }
+  };
+}
+
+macro_rules! define_mul_assign_variants {
+  (LHS = $lhs:ty, RHS = $rhs:ty) => {
+    impl MulAssign<$rhs> for $lhs {
+      fn mul_assign(&mut self, rhs: $rhs) {
+        *self *= &rhs;
+      }
+    }
+  };
+}
+
+define_mul_assign_variants!(LHS = Commitment, RHS = Scalar);
+define_mul_variants!(LHS = Commitment, RHS = Scalar, Output = Commitment);
+define_mul_variants!(LHS = Scalar, RHS = Commitment, Output = Commitment);
+
+impl<'b> AddAssign<&'b Commitment> for Commitment {
+  fn add_assign(&mut self, other: &'b Commitment) {
+    let result = (self as &Commitment).comm + other.comm;
+    *self = Commitment { comm: result };
+  }
+}
+
+impl<'a, 'b> Add<&'b Commitment> for &'a Commitment {
+  type Output = Commitment;
+  fn add(self, other: &'b Commitment) -> Commitment {
+    Commitment {
+      comm: self.comm + other.comm,
+    }
+  }
+}
+
+macro_rules! define_add_variants {
+  (LHS = $lhs:ty, RHS = $rhs:ty, Output = $out:ty) => {
+    impl<'b> Add<&'b $rhs> for $lhs {
+      type Output = $out;
+      fn add(self, rhs: &'b $rhs) -> $out {
+        &self + rhs
+      }
+    }
+
+    impl<'a> Add<$rhs> for &'a $lhs {
+      type Output = $out;
+      fn add(self, rhs: $rhs) -> $out {
+        self + &rhs
+      }
+    }
+
+    impl Add<$rhs> for $lhs {
+      type Output = $out;
+      fn add(self, rhs: $rhs) -> $out {
+        &self + &rhs
+      }
+    }
+  };
+}
+
+macro_rules! define_add_assign_variants {
+  (LHS = $lhs:ty, RHS = $rhs:ty) => {
+    impl AddAssign<$rhs> for $lhs {
+      fn add_assign(&mut self, rhs: $rhs) {
+        *self += &rhs;
+      }
+    }
+  };
+}
+
+define_add_assign_variants!(LHS = Commitment, RHS = Commitment);
+define_add_variants!(LHS = Commitment, RHS = Commitment, Output = Commitment);

src/errors.rs

@@ -0,0 +1,15 @@
+use core::fmt::Debug;
+
+#[derive(Clone, Debug, Eq, PartialEq)]
+pub enum NovaError {
+  /// returned if the supplied row or col in (row,col,val) tuple is out of range
+  InvalidIndex,
+  /// returned if the supplied input is not of the right length
+  InvalidInputLength,
+  /// returned if the supplied witness is not of the right length
+  InvalidWitnessLength,
+  /// returned if the supplied witness is not a satisfying witness to a given shape and instance
+  UnSat,
+  /// returned when the supplied compressed commitment cannot be decompressed
+  DecompressionError,
+}

src/lib.rs

@@ -0,0 +1,240 @@
+#![allow(non_snake_case)]
+#![feature(test)]
+#![deny(missing_docs)]
+#![feature(external_doc)]
+#![doc(include = "../README.md")]
+
+extern crate core;
+extern crate curve25519_dalek;
+extern crate digest;
+extern crate merlin;
+extern crate rand;
+extern crate rayon;
+extern crate sha3;
+extern crate test;
+
+mod commitments;
+mod errors;
+mod r1cs;
+
+use commitments::{AppendToTranscriptTrait, CompressedCommitment, ProofTranscriptTrait};
+use errors::NovaError;
+use merlin::Transcript;
+use r1cs::{R1CSGens, R1CSInstance, R1CSShape, R1CSWitness};
+
+/// A SNARK that holds the proof of a step of an incremental computation
+pub struct StepSNARK {
+  comm_T: CompressedCommitment,
+}
+
+impl StepSNARK {
+  fn protocol_name() -> &'static [u8] {
+    b"NovaStepSNARK"
+  }
+
+  /// Takes as input two relaxed R1CS instance-witness tuples `(U1, W1)` and `(U2, W2)`
+  /// with the same structure `shape` and defined with respect to the same `gens`,
+  /// and outputs a folded instance-witness tuple `(U, W)` of the same shape `shape`,
+  /// with the guarantee that the folded witness `W` satisfies the folded instance `U`
+  /// if and only if `W1` satisfies `U1` and `W2` satisfies `U2`.
+  pub fn prove(
+    gens: &R1CSGens,
+    S: &R1CSShape,
+    U1: &R1CSInstance,
+    W1: &R1CSWitness,
+    U2: &R1CSInstance,
+    W2: &R1CSWitness,
+    transcript: &mut Transcript,
+  ) -> Result<(StepSNARK, (R1CSInstance, R1CSWitness)), NovaError> {
+    // append the protocol name to the transcript
+    transcript.append_protocol_name(StepSNARK::protocol_name());
+
+    // compute a commitment to the cross-term
+    let (T, comm_T) = S.commit_T(gens, U1, W1, U2, W2)?;
+
+    // append `comm_T` to the transcript and obtain a challenge
+    comm_T.append_to_transcript(b"comm_T", transcript);
+
+    // compute a challenge from the transcript
+    let r = transcript.challenge_scalar(b"r");
+
+    // fold the instance using `r` and `comm_T`
+    let U = U1.fold(U2, &comm_T, &r)?;
+
+    // fold the witness using `r` and `T`
+    let W = W1.fold(W2, &T, &r)?;
+
+    // return the folded instance and witness
+    return Ok((StepSNARK { comm_T }, (U, W)));
+  }
+
+  /// Takes as input two relaxed R1CS instances `U1` and `U2`
+  /// with the same shape and defined with respect to the same parameters,
+  /// and outputs a folded instance `U` with the same shape,
+  /// with the guarantee that the folded instance `U`
+  /// if and only if `U1` and `U2` are satisfiable.
+  pub fn verify(
+    &self,
+    U1: &R1CSInstance,
+    U2: &R1CSInstance,
+    transcript: &mut Transcript,
+  ) -> Result<R1CSInstance, NovaError> {
+    // append the protocol name to the transcript
+    transcript.append_protocol_name(StepSNARK::protocol_name());
+
+    // append `comm_T` to the transcript and obtain a challenge
+    self.comm_T.append_to_transcript(b"comm_T", transcript);
+
+    // compute a challenge from the transcript
+    let r = transcript.challenge_scalar(b"r");
+
+    // fold the instance using `r` and `comm_T`
+    let U = U1.fold(U2, &self.comm_T, &r)?;
+
+    // return the folded instance and witness
+    return Ok(U);
+  }
+}
+
+/// A SNARK that holds the proof of the final step of an incremental computation
+pub struct FinalSNARK {
+  W: R1CSWitness,
+}
+
+impl FinalSNARK {
+  /// Produces a proof of a instance given its satisfying witness `W`.
+  pub fn prove(W: &R1CSWitness) -> Result<FinalSNARK, NovaError> {
+    Ok(FinalSNARK { W: W.clone() })
+  }
+
+  /// Verifies the proof of a folded instance `U` given its shape `S` public parameters `gens`
+  pub fn verify(&self, gens: &R1CSGens, S: &R1CSShape, U: &R1CSInstance) -> Result<(), NovaError> {
+    // check that the witness is a valid witness to the folded instance `U`
+    S.is_sat(gens, U, &self.W)
+  }
+}
+
+#[cfg(test)]
+mod tests {
+  use super::commitments::Scalar;
+  use super::*;
+  use rand::rngs::OsRng;
+
+  #[test]
+  fn test_tiny_r1cs() {
+    let one = Scalar::one();
+    let (num_cons, num_vars, num_inputs, A, B, C) = {
+      let num_cons = 4;
+      let num_vars = 4;
+      let num_inputs = 1;
+
+      // The R1CS for this problem consists of the following constraints:
+      // `Z0 * Z0 - Z1 = 0`
+      // `Z1 * Z0 - Z2 = 0`
+      // `(Z2 + Z0) * 1 - Z3 = 0`
+      // `(Z3 + 5) * 1 - I0 = 0`
+
+      // Relaxed R1CS is a set of three sparse matrices (A B C), where there is a row for every
+      // constraint and a column for every entry in z = (vars, u, inputs)
+      // An R1CS instance is satisfiable iff:
+      // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, inputs)
+      let mut A: Vec<(usize, usize, Scalar)> = Vec::new();
+      let mut B: Vec<(usize, usize, Scalar)> = Vec::new();
+      let mut C: Vec<(usize, usize, Scalar)> = Vec::new();
+
+      // constraint 0 entries in (A,B,C)
+      A.push((0, 0, one));
+      B.push((0, 0, one));
+      C.push((0, 1, one));
+
+      // constraint 1 entries in (A,B,C)
+      A.push((1, 1, one));
+      B.push((1, 0, one));
+      C.push((1, 2, one));
+
+      // constraint 2 entries in (A,B,C)
+      A.push((2, 2, one));
+      A.push((2, 0, one));
+      B.push((2, num_vars, one));
+      C.push((2, 3, one));
+
+      // constraint 3 entries in (A,B,C)
+      A.push((3, 3, one));
+      A.push((3, num_vars, one + one + one + one + one));
+      B.push((3, num_vars, one));
+      C.push((3, num_vars + 1, one));
+
+      (num_cons, num_vars, num_inputs, A, B, C)
+    };
+
+    // create a shape object
+    let S = {
+      let res = R1CSShape::new(num_cons, num_vars, num_inputs, &A, &B, &C);
+      assert!(res.is_ok());
+      res.unwrap()
+    };
+
+    // generate generators
+    let gens = R1CSGens::new(num_cons, num_vars);
+
+    let rand_inst_witness_generator = |gens: &R1CSGens| -> (R1CSInstance, R1CSWitness) {
+      // compute a satisfying (vars, X) tuple
+      let (vars, X) = {
+        let mut csprng: OsRng = OsRng;
+        let z0 = Scalar::random(&mut csprng);
+        let z1 = z0 * z0; // constraint 0
+        let z2 = z1 * z0; // constraint 1
+        let z3 = z2 + z0; // constraint 2
+        let i0 = z3 + one + one + one + one + one; // constraint 3
+
+        let vars = vec![z0, z1, z2, z3];
+        let X = vec![i0];
+        (vars, X)
+      };
+
+      let W = {
+        let E = vec![Scalar::zero(); num_cons]; // default E
+        let res = R1CSWitness::new(&S, &vars, &E);
+        assert!(res.is_ok());
+        res.unwrap()
+      };
+      let U = {
+        let (comm_W, comm_E) = W.commit(&gens);
+        let u = Scalar::one(); //default u
+        let res = R1CSInstance::new(&S, &comm_W, &comm_E, &X, &u);
+        assert!(res.is_ok());
+        res.unwrap()
+      };
+
+      // check that generated instance is satisfiable
+      let is_sat = S.is_sat(&gens, &U, &W);
+      assert!(is_sat.is_ok());
+      (U, W)
+    };
+
+    let (U1, W1) = rand_inst_witness_generator(&gens);
+    let (U2, W2) = rand_inst_witness_generator(&gens);
+
+    // produce a step SNARK
+    let mut prover_transcript = Transcript::new(b"StepSNARKExample");
+    let res = StepSNARK::prove(&gens, &S, &U1, &W1, &U2, &W2, &mut prover_transcript);
+    assert!(res.is_ok());
+    let (step_snark, (_U, W)) = res.unwrap();
+
+    // verify the step SNARK
+    let mut verifier_transcript = Transcript::new(b"StepSNARKExample");
+    let res = step_snark.verify(&U1, &U2, &mut verifier_transcript);
+    assert!(res.is_ok());
+    let U = res.unwrap();
+
+    assert_eq!(U, _U);
+
+    // produce a final SNARK
+    let res = FinalSNARK::prove(&W);
+    assert!(res.is_ok());
+    let final_snark = res.unwrap();
+    // verify the final SNARK
+    let res = final_snark.verify(&gens, &S, &U);
+    assert!(res.is_ok());
+  }
+}

src/r1cs.rs

@@ -0,0 +1,320 @@
+use super::commitments::Scalar;
+use super::commitments::{CommitGens, CommitTrait, Commitment, CompressedCommitment};
+use super::errors::NovaError;
+use itertools::concat;
+use rayon::prelude::*;
+
+pub struct R1CSGens {
+  gens_W: CommitGens,
+  gens_E: CommitGens,
+}
+
+#[derive(Debug)]
+pub struct R1CSShape {
+  num_cons: usize,
+  num_vars: usize,
+  num_inputs: usize,
+  A: Vec<(usize, usize, Scalar)>,
+  B: Vec<(usize, usize, Scalar)>,
+  C: Vec<(usize, usize, Scalar)>,
+}
+
+#[derive(Clone, Debug)]
+pub struct R1CSWitness {
+  W: Vec<Scalar>,
+  E: Vec<Scalar>,
+}
+
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct R1CSInstance {
+  comm_W: Commitment,
+  comm_E: Commitment,
+  X: Vec<Scalar>,
+  u: Scalar,
+}
+
+impl R1CSGens {
+  pub fn new(num_cons: usize, num_vars: usize) -> R1CSGens {
+    // generators to commit to witness vector `W`
+    let gens_W = CommitGens::new(b"gens_W", num_vars);
+
+    // generators to commit to the error/slack vector `E`
+    let gens_E = CommitGens::new(b"gens_E", num_cons);
+
+    R1CSGens { gens_E, gens_W }
+  }
+}
+
+impl R1CSShape {
+  pub fn new(
+    num_cons: usize,
+    num_vars: usize,
+    num_inputs: usize,
+    A: &Vec<(usize, usize, Scalar)>,
+    B: &Vec<(usize, usize, Scalar)>,
+    C: &Vec<(usize, usize, Scalar)>,
+  ) -> Result<R1CSShape, NovaError> {
+    let is_valid = |num_cons: usize,
+                    num_vars: usize,
+                    num_io: usize,
+                    M: &Vec<(usize, usize, Scalar)>|
+     -> Result<(), NovaError> {
+      let res = (0..num_cons)
+        .map(|i| {
+          let (row, col, _val) = M[i];
+          if row >= num_cons {
+            Err(NovaError::InvalidIndex)
+          } else if col >= num_io + num_vars + 1 {
+            Err(NovaError::InvalidIndex)
+          } else {
+            Ok(())
+          }
+        })
+        .collect::<Result<Vec<()>, NovaError>>();
+
+      if res.is_err() {
+        Err(NovaError::InvalidIndex)
+      } else {
+        Ok(())
+      }
+    };
+
+    let res_A = is_valid(num_cons, num_vars, num_inputs, &A);
+    let res_B = is_valid(num_cons, num_vars, num_inputs, &B);
+    let res_C = is_valid(num_cons, num_vars, num_inputs, &C);
+
+    if res_A.is_err() || res_B.is_err() || res_C.is_err() {
+      return Err(NovaError::InvalidIndex);
+    }
+
+    let shape = R1CSShape {
+      num_cons,
+      num_vars,
+      num_inputs,
+      A: A.clone(),
+      B: B.clone(),
+      C: C.clone(),
+    };
+
+    Ok(shape)
+  }
+
+  fn multiply_vec(
+    &self,
+    z: &[Scalar],
+  ) -> Result<(Vec<Scalar>, Vec<Scalar>, Vec<Scalar>), NovaError> {
+    if z.len() != self.num_inputs + self.num_vars + 1 {
+      return Err(NovaError::InvalidWitnessLength);
+    }
+
+    // computes a product between a sparse matrix `M` and a vector `z`
+    // This does not perform any validation of entries in M (e.g., if entries in `M` reference indexes outside the range of `z`)
+    // This is safe since we know that `M` is valid
+    let sparse_matrix_vec_product =
+      |M: &Vec<(usize, usize, Scalar)>, num_rows: usize, z: &[Scalar]| -> Vec<Scalar> {
+        (0..M.len())
+          .map(|i| {
+            let (row, col, val) = M[i];
+            (row, val * z[col])
+          })
+          .fold(vec![Scalar::zero(); num_rows], |mut Mz, (r, v)| {
+            Mz[r] += v;
+            Mz
+          })
+      };
+
+    let Az = sparse_matrix_vec_product(&self.A, self.num_cons, &z);
+    let Bz = sparse_matrix_vec_product(&self.B, self.num_cons, &z);
+    let Cz = sparse_matrix_vec_product(&self.C, self.num_cons, &z);
+
+    Ok((Az, Bz, Cz))
+  }
+
+  pub fn is_sat(
+    &self,
+    gens: &R1CSGens,
+    U: &R1CSInstance,
+    W: &R1CSWitness,
+  ) -> Result<(), NovaError> {
+    assert_eq!(W.W.len(), self.num_vars);
+    assert_eq!(W.E.len(), self.num_cons);
+    assert_eq!(U.X.len(), self.num_inputs);
+
+    // verify if Az * Bz = u*Cz + E
+    let res_eq: bool = {
+      let z = concat(vec![W.W.clone(), vec![U.u], U.X.clone()]);
+      let (Az, Bz, Cz) = self.multiply_vec(&z)?;
+      assert_eq!(Az.len(), self.num_cons);
+      assert_eq!(Bz.len(), self.num_cons);
+      assert_eq!(Cz.len(), self.num_cons);
+
+      let res: usize = (0..self.num_cons)
+        .map(|i| {
+          if Az[i] * Bz[i] == U.u * Cz[i] + W.E[i] {
+            0
+          } else {
+            1
+          }
+        })
+        .sum();
+
+      res == 0
+    };
+
+    assert!(res_eq, true);
+
+    // verify if comm_E and comm_W are commitments to E and W
+    let res_comm: bool = {
+      let comm_W = W.W.commit(&gens.gens_W);
+      let comm_E = W.E.commit(&gens.gens_E);
+
+      U.comm_W == comm_W && U.comm_E == comm_E
+    };
+
+    assert!(res_comm, true);
+
+    if res_eq && res_comm {
+      Ok(())
+    } else {
+      Err(NovaError::UnSat)
+    }
+  }
+
+  pub fn commit_T(
+    &self,
+    gens: &R1CSGens,
+    U1: &R1CSInstance,
+    W1: &R1CSWitness,
+    U2: &R1CSInstance,
+    W2: &R1CSWitness,
+  ) -> Result<(Vec<Scalar>, CompressedCommitment), NovaError> {
+    let (AZ_1, BZ_1, CZ_1) = {
+      let Z1 = concat(vec![W1.W.clone(), vec![U1.u], U1.X.clone()]);
+      self.multiply_vec(&Z1)?
+    };
+
+    let (AZ_2, BZ_2, CZ_2) = {
+      let Z2 = concat(vec![W2.W.clone(), vec![U2.u], U2.X.clone()]);
+      self.multiply_vec(&Z2)?
+    };
+
+    let AZ_1_circ_BZ_2 = (0..AZ_1.len())
+      .map(|i| AZ_1[i] * BZ_2[i])
+      .collect::<Vec<Scalar>>();
+    let AZ_2_circ_BZ_1 = (0..AZ_2.len())
+      .map(|i| AZ_2[i] * BZ_1[i])
+      .collect::<Vec<Scalar>>();
+    let u_1_cdot_CZ_2 = (0..CZ_2.len())
+      .map(|i| U1.u * CZ_2[i])
+      .collect::<Vec<Scalar>>();
+    let u_2_cdot_CZ_1 = (0..CZ_1.len())
+      .map(|i| U2.u * CZ_1[i])
+      .collect::<Vec<Scalar>>();
+
+    let T = AZ_1_circ_BZ_2
+      .par_iter()
+      .zip(&AZ_2_circ_BZ_1)
+      .zip(&u_1_cdot_CZ_2)
+      .zip(&u_2_cdot_CZ_1)
+      .map(|(((a, b), c), d)| a + b - c - d)
+      .collect::<Vec<Scalar>>();
+
+    let T_commit = T.commit(&gens.gens_E).compress();
+
+    Ok((T, T_commit))
+  }
+}
+
+impl R1CSWitness {
+  pub fn new(S: &R1CSShape, W: &Vec<Scalar>, E: &Vec<Scalar>) -> Result<R1CSWitness, NovaError> {
+    if S.num_vars != W.len() || S.num_cons != E.len() {
+      Err(NovaError::InvalidWitnessLength)
+    } else {
+      Ok(R1CSWitness {
+        W: W.clone(),
+        E: E.clone(),
+      })
+    }
+  }
+
+  pub fn commit(&self, gens: &R1CSGens) -> (Commitment, Commitment) {
+    (self.W.commit(&gens.gens_W), self.E.commit(&gens.gens_E))
+  }
+
+  pub fn fold(
+    &self,
+    W2: &R1CSWitness,
+    T: &Vec<Scalar>,
+    r: &Scalar,
+  ) -> Result<R1CSWitness, NovaError> {
+    let (W1, E1) = (&self.W, &self.E);
+    let (W2, E2) = (&W2.W, &W2.E);
+
+    if W1.len() != W2.len() {
+      return Err(NovaError::InvalidWitnessLength);
+    }
+
+    let W = W1
+      .par_iter()
+      .zip(W2)
+      .map(|(a, b)| a + r * b)
+      .collect::<Vec<Scalar>>();
+    let E = E1
+      .par_iter()
+      .zip(T)
+      .zip(E2)
+      .map(|((a, b), c)| a + r * b + r * r * c)
+      .collect::<Vec<Scalar>>();
+    Ok(R1CSWitness { W, E })
+  }
+}
+
+impl R1CSInstance {
+  pub fn new(
+    S: &R1CSShape,
+    comm_W: &Commitment,
+    comm_E: &Commitment,
+    X: &Vec<Scalar>,
+    u: &Scalar,
+  ) -> Result<R1CSInstance, NovaError> {
+    if S.num_inputs != X.len() {
+      Err(NovaError::InvalidInputLength)
+    } else {
+      Ok(R1CSInstance {
+        comm_W: comm_W.clone(),
+        comm_E: comm_E.clone(),
+        X: X.clone(),
+        u: *u,
+      })
+    }
+  }
+
+  pub fn fold(
+    &self,
+    U2: &R1CSInstance,
+    comm_T: &CompressedCommitment,
+    r: &Scalar,
+  ) -> Result<R1CSInstance, NovaError> {
+    let comm_T_unwrapped = comm_T.decompress()?;
+    let (X1, u1, comm_W_1, comm_E_1) =
+      (&self.X, &self.u, &self.comm_W.clone(), &self.comm_E.clone());
+    let (X2, u2, comm_W_2, comm_E_2) = (&U2.X, &U2.u, &U2.comm_W, &U2.comm_E);
+
+    // weighted sum of X
+    let X = X1
+      .par_iter()
+      .zip(X2)
+      .map(|(a, b)| a + r * b)
+      .collect::<Vec<Scalar>>();
+    let comm_W = comm_W_1 + r * comm_W_2;
+    let comm_E = comm_E_1 + r * comm_T_unwrapped + r * r * comm_E_2;
+    let u = u1 + r * u2;
+
+    Ok(R1CSInstance {
+      comm_W,
+      comm_E,
+      X,
+      u,
+    })
+  }
+}