use super::{shape_cs::ShapeCS, solver::SatisfyingAssignment, test_shape_cs::TestShapeCS};
use crate::{
errors::NovaError,
frontend::{Index, LinearCombination},
r1cs::{R1CSInstance, R1CSShape, R1CSWitness, SparseMatrix},
traits::Engine,
CommitmentKey,
};
use ff::PrimeField;
pub trait NovaWitness<E: Engine> {
fn r1cs_instance_and_witness(
&self,
shape: &R1CSShape<E>,
ck: &CommitmentKey<E>,
) -> Result<(R1CSInstance<E>, R1CSWitness<E>), NovaError>;
}
pub trait NovaShape<E: Engine> {
fn r1cs_shape(&self) -> Result<R1CSShape<E>, NovaError>;
}
impl<E: Engine> NovaWitness<E> for SatisfyingAssignment<E> {
fn r1cs_instance_and_witness(
&self,
shape: &R1CSShape<E>,
ck: &CommitmentKey<E>,
) -> Result<(R1CSInstance<E>, R1CSWitness<E>), NovaError> {
let W = R1CSWitness::<E>::new(shape, self.aux_assignment())?;
let X = &self.input_assignment()[1..];
let comm_W = W.commit(ck);
let instance = R1CSInstance::<E>::new(shape, &comm_W, X)?;
Ok((instance, W))
}
}
macro_rules! impl_nova_shape {
( $name:ident) => {
impl<E: Engine> NovaShape<E> for $name<E>
where
E::Scalar: PrimeField,
{
fn r1cs_shape(&self) -> Result<R1CSShape<E>, NovaError> {
let mut A = SparseMatrix::<E::Scalar>::empty();
let mut B = SparseMatrix::<E::Scalar>::empty();
let mut C = SparseMatrix::<E::Scalar>::empty();
let mut num_cons_added = 0;
let mut X = (&mut A, &mut B, &mut C, &mut num_cons_added);
let num_inputs = self.num_inputs();
let num_constraints = self.num_constraints();
let num_vars = self.num_aux();
for constraint in self.constraints.iter() {
add_constraint(
&mut X,
num_vars,
&constraint.0,
&constraint.1,
&constraint.2,
);
}
assert_eq!(num_cons_added, num_constraints);
A.cols = num_vars + num_inputs;
B.cols = num_vars + num_inputs;
C.cols = num_vars + num_inputs;
R1CSShape::new(num_constraints, num_vars, num_inputs - 1, A, B, C)
}
}
};
}
impl_nova_shape!(ShapeCS);
impl_nova_shape!(TestShapeCS);
fn add_constraint<S: PrimeField>(
X: &mut (
&mut SparseMatrix<S>,
&mut SparseMatrix<S>,
&mut SparseMatrix<S>,
&mut usize,
),
num_vars: usize,
a_lc: &LinearCombination<S>,
b_lc: &LinearCombination<S>,
c_lc: &LinearCombination<S>,
) {
let (A, B, C, nn) = X;
let n = **nn;
assert_eq!(n + 1, A.indptr.len(), "A: invalid shape");
assert_eq!(n + 1, B.indptr.len(), "B: invalid shape");
assert_eq!(n + 1, C.indptr.len(), "C: invalid shape");
let add_constraint_component = |index: Index, coeff: &S, M: &mut SparseMatrix<S>| {
if *coeff != S::ZERO {
match index {
Index::Input(idx) => {
let idx = idx + num_vars;
M.data.push(*coeff);
M.indices.push(idx);
}
Index::Aux(idx) => {
M.data.push(*coeff);
M.indices.push(idx);
}
}
}
};
for (index, coeff) in a_lc.iter() {
add_constraint_component(index.0, coeff, A);
}
A.indptr.push(A.indices.len());
for (index, coeff) in b_lc.iter() {
add_constraint_component(index.0, coeff, B)
}
B.indptr.push(B.indices.len());
for (index, coeff) in c_lc.iter() {
add_constraint_component(index.0, coeff, C)
}
C.indptr.push(C.indices.len());
**nn += 1;
}