nova_snark/frontend/
r1cs.rs

1//! Support for generating R1CS using bellpepper.
2use super::{shape_cs::ShapeCS, solver::SatisfyingAssignment, test_shape_cs::TestShapeCS};
3use crate::{
4  errors::NovaError,
5  frontend::{Index, LinearCombination},
6  r1cs::{R1CSInstance, R1CSShape, R1CSWitness, SparseMatrix},
7  traits::Engine,
8  CommitmentKey,
9};
10use ff::PrimeField;
11
12/// `NovaWitness` provide a method for acquiring an `R1CSInstance` and `R1CSWitness` from implementers.
13pub trait NovaWitness<E: Engine> {
14  /// Return an instance and witness, given a shape and ck.
15  fn r1cs_instance_and_witness(
16    &self,
17    shape: &R1CSShape<E>,
18    ck: &CommitmentKey<E>,
19  ) -> Result<(R1CSInstance<E>, R1CSWitness<E>), NovaError>;
20}
21
22/// `NovaShape` provides methods for acquiring `R1CSShape` from implementers.
23pub trait NovaShape<E: Engine> {
24  /// Return an appropriate `R1CSShape` struct.
25  fn r1cs_shape(&self) -> Result<R1CSShape<E>, NovaError>;
26}
27
28impl<E: Engine> NovaWitness<E> for SatisfyingAssignment<E> {
29  fn r1cs_instance_and_witness(
30    &self,
31    shape: &R1CSShape<E>,
32    ck: &CommitmentKey<E>,
33  ) -> Result<(R1CSInstance<E>, R1CSWitness<E>), NovaError> {
34    let W = R1CSWitness::<E>::new(shape, self.aux_assignment())?;
35    let X = &self.input_assignment()[1..];
36
37    let comm_W = W.commit(ck);
38
39    let instance = R1CSInstance::<E>::new(shape, &comm_W, X)?;
40
41    Ok((instance, W))
42  }
43}
44
45macro_rules! impl_nova_shape {
46  ( $name:ident) => {
47    impl<E: Engine> NovaShape<E> for $name<E>
48    where
49      E::Scalar: PrimeField,
50    {
51      fn r1cs_shape(&self) -> Result<R1CSShape<E>, NovaError> {
52        let mut A = SparseMatrix::<E::Scalar>::empty();
53        let mut B = SparseMatrix::<E::Scalar>::empty();
54        let mut C = SparseMatrix::<E::Scalar>::empty();
55
56        let mut num_cons_added = 0;
57        let mut X = (&mut A, &mut B, &mut C, &mut num_cons_added);
58        let num_inputs = self.num_inputs();
59        let num_constraints = self.num_constraints();
60        let num_vars = self.num_aux();
61
62        for constraint in self.constraints.iter() {
63          add_constraint(
64            &mut X,
65            num_vars,
66            &constraint.0,
67            &constraint.1,
68            &constraint.2,
69          );
70        }
71        assert_eq!(num_cons_added, num_constraints);
72
73        A.cols = num_vars + num_inputs;
74        B.cols = num_vars + num_inputs;
75        C.cols = num_vars + num_inputs;
76
77        // Don't count One as an input for shape's purposes.
78        R1CSShape::new(num_constraints, num_vars, num_inputs - 1, A, B, C)
79      }
80    }
81  };
82}
83
84impl_nova_shape!(ShapeCS);
85impl_nova_shape!(TestShapeCS);
86
87fn add_constraint<S: PrimeField>(
88  X: &mut (
89    &mut SparseMatrix<S>,
90    &mut SparseMatrix<S>,
91    &mut SparseMatrix<S>,
92    &mut usize,
93  ),
94  num_vars: usize,
95  a_lc: &LinearCombination<S>,
96  b_lc: &LinearCombination<S>,
97  c_lc: &LinearCombination<S>,
98) {
99  let (A, B, C, nn) = X;
100  let n = **nn;
101  assert_eq!(n + 1, A.indptr.len(), "A: invalid shape");
102  assert_eq!(n + 1, B.indptr.len(), "B: invalid shape");
103  assert_eq!(n + 1, C.indptr.len(), "C: invalid shape");
104
105  let add_constraint_component = |index: Index, coeff: &S, M: &mut SparseMatrix<S>| {
106    // we add constraints to the matrix only if the associated coefficient is non-zero
107    if *coeff != S::ZERO {
108      match index {
109        Index::Input(idx) => {
110          // Inputs come last, with input 0, representing 'one',
111          // at position num_vars within the witness vector.
112          let idx = idx + num_vars;
113          M.data.push(*coeff);
114          M.indices.push(idx);
115        }
116        Index::Aux(idx) => {
117          M.data.push(*coeff);
118          M.indices.push(idx);
119        }
120      }
121    }
122  };
123
124  for (index, coeff) in a_lc.iter() {
125    add_constraint_component(index.0, coeff, A);
126  }
127  A.indptr.push(A.indices.len());
128
129  for (index, coeff) in b_lc.iter() {
130    add_constraint_component(index.0, coeff, B)
131  }
132  B.indptr.push(B.indices.len());
133
134  for (index, coeff) in c_lc.iter() {
135    add_constraint_component(index.0, coeff, C)
136  }
137  C.indptr.push(C.indices.len());
138
139  **nn += 1;
140}
nova_snark/frontend/r1cs.rs

nova_snark/frontend/
r1cs.rs
