Browse Source
refactor frontend composition, update usage of arkworks CS helpers, refactor test circuits (#54)
Changes:
- get rid of `extract_r1cs_and_z` and `extract_z`
- move `extract_r1cs` and `extract_w_x` from `frontend/arkworks` into
`r1cs.rs`
The reasoning: they are not methods needed for the Frontend interface,
but only needed internally for the folding scheme to extract values from
the AugmentedF circuit and similar.
- set the `FCircuit` as the trait for the `src/frontend`
- remove the `frontend/arkworks` since the `FCircuit` trait can be
directly implemented without a middle layer
- reorganize test circuits into `src/frontend/mod.rs`, updating them into
`CubicFCircuit`: the typical x^3+x+5=y circuit
`CustomFCircuit`: a circuit in which you can specify the number of
constraints that it will take
where both fulfill the `FCircuit` trait, and they are used for
different tests being folded.
main
GitHub
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 263 additions and 256 deletions
Unified View
Diff Options
-
+44 -0src/ccs/r1cs.rs
-
+11 -66src/folding/nova/circuits.rs
-
+33 -61src/folding/nova/decider.rs
-
+7 -6src/folding/nova/ivc.rs
-
+0 -122src/frontend/arkworks/mod.rs
-
+168 -1src/frontend/mod.rs
@ -1,122 +0,0 @@ |
|||||
/// arkworks frontend
|
|
||||
use ark_ff::PrimeField;
|
|
||||
use ark_relations::r1cs::ConstraintSystem;
|
|
||||
|
|
||||
use crate::ccs::r1cs::R1CS;
|
|
||||
use crate::utils::vec::SparseMatrix;
|
|
||||
|
|
||||
/// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format, and
|
|
||||
/// extracts public inputs and witness into z vector. Returns a tuple containing (R1CS, z).
|
|
||||
pub fn extract_r1cs_and_z<F: PrimeField>(cs: &ConstraintSystem<F>) -> (R1CS<F>, Vec<F>) {
|
|
||||
let r1cs = extract_r1cs(cs);
|
|
||||
|
|
||||
// z = (1, x, w)
|
|
||||
let z = extract_z(cs);
|
|
||||
|
|
||||
(r1cs, z)
|
|
||||
}
|
|
||||
|
|
||||
/// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format as R1CS
|
|
||||
/// struct.
|
|
||||
pub fn extract_r1cs<F: PrimeField>(cs: &ConstraintSystem<F>) -> R1CS<F> {
|
|
||||
let m = cs.to_matrices().unwrap();
|
|
||||
|
|
||||
let n_rows = cs.num_constraints;
|
|
||||
let n_cols = cs.num_instance_variables + cs.num_witness_variables; // cs.num_instance_variables already counts the 1
|
|
||||
|
|
||||
let A = SparseMatrix::<F> {
|
|
||||
n_rows,
|
|
||||
n_cols,
|
|
||||
coeffs: m.a,
|
|
||||
};
|
|
||||
let B = SparseMatrix::<F> {
|
|
||||
n_rows,
|
|
||||
n_cols,
|
|
||||
coeffs: m.b,
|
|
||||
};
|
|
||||
let C = SparseMatrix::<F> {
|
|
||||
n_rows,
|
|
||||
n_cols,
|
|
||||
coeffs: m.c,
|
|
||||
};
|
|
||||
|
|
||||
R1CS::<F> {
|
|
||||
l: cs.num_instance_variables - 1, // -1 to substract the first '1'
|
|
||||
A,
|
|
||||
B,
|
|
||||
C,
|
|
||||
}
|
|
||||
}
|
|
||||
|
|
||||
/// extracts public inputs and witness into z vector from arkworks ConstraintSystem.
|
|
||||
pub fn extract_z<F: PrimeField>(cs: &ConstraintSystem<F>) -> Vec<F> {
|
|
||||
// z = (1, x, w)
|
|
||||
[
|
|
||||
// 1 is already included in cs.instance_assignment
|
|
||||
cs.instance_assignment.clone(),
|
|
||||
cs.witness_assignment.clone(),
|
|
||||
]
|
|
||||
.concat()
|
|
||||
}
|
|
||||
|
|
||||
/// extracts the witness and the public inputs from arkworks ConstraintSystem.
|
|
||||
pub fn extract_w_x<F: PrimeField>(cs: &ConstraintSystem<F>) -> (Vec<F>, Vec<F>) {
|
|
||||
(
|
|
||||
cs.witness_assignment.clone(),
|
|
||||
// skip the first element which is '1'
|
|
||||
cs.instance_assignment[1..].to_vec(),
|
|
||||
)
|
|
||||
}
|
|
||||
|
|
||||
#[cfg(test)]
|
|
||||
pub mod tests {
|
|
||||
use super::*;
|
|
||||
use ark_ff::PrimeField;
|
|
||||
use ark_pallas::Fr;
|
|
||||
use ark_r1cs_std::{alloc::AllocVar, eq::EqGadget, fields::fp::FpVar};
|
|
||||
use ark_relations::r1cs::{
|
|
||||
ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
|
|
||||
};
|
|
||||
|
|
||||
// TestCircuit implements the R1CS for: x^3 + x + 5 = y (example from article
|
|
||||
// https://www.vitalik.ca/general/2016/12/10/qap.html )
|
|
||||
#[derive(Clone, Copy, Debug)]
|
|
||||
pub struct TestCircuit<F: PrimeField> {
|
|
||||
pub x: F,
|
|
||||
pub y: F,
|
|
||||
}
|
|
||||
impl<F: PrimeField> ConstraintSynthesizer<F> for TestCircuit<F> {
|
|
||||
fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
|
|
||||
let x = FpVar::<F>::new_input(cs.clone(), || Ok(self.x))?;
|
|
||||
let y = FpVar::<F>::new_witness(cs.clone(), || Ok(self.y))?;
|
|
||||
let five = FpVar::<F>::new_constant(cs.clone(), F::from(5u32))?;
|
|
||||
|
|
||||
let comp_y = (&x * &x * &x) + &x + &five;
|
|
||||
comp_y.enforce_equal(&y)?;
|
|
||||
Ok(())
|
|
||||
}
|
|
||||
}
|
|
||||
|
|
||||
#[test]
|
|
||||
fn test_cs_to_matrices() {
|
|
||||
let cs = ConstraintSystem::<Fr>::new_ref();
|
|
||||
|
|
||||
let x = Fr::from(5_u32);
|
|
||||
let y = x * x * x + x + Fr::from(5_u32);
|
|
||||
|
|
||||
let test_circuit = TestCircuit::<Fr> { x, y };
|
|
||||
test_circuit.generate_constraints(cs.clone()).unwrap();
|
|
||||
cs.finalize();
|
|
||||
assert!(cs.is_satisfied().unwrap());
|
|
||||
|
|
||||
let cs = cs.into_inner().unwrap();
|
|
||||
|
|
||||
// ensure that num_instance_variables is 2: 1 + 1 public input
|
|
||||
assert_eq!(cs.num_instance_variables, 2);
|
|
||||
|
|
||||
let (r1cs, z) = extract_r1cs_and_z::<Fr>(&cs);
|
|
||||
r1cs.check_relation(&z).unwrap();
|
|
||||
// ensure that number of public inputs (l) is 1
|
|
||||
assert_eq!(r1cs.l, 1);
|
|
||||
}
|
|
||||
}
|
|
||||
@ -1,2 +1,169 @@ |
|||||
pub mod arkworks;
|
|
||||
pub mod circom;
|
pub mod circom;
|
||||
|
|
||||
|
use crate::Error;
|
||||
|
use ark_ff::PrimeField;
|
||||
|
use ark_r1cs_std::fields::fp::FpVar;
|
||||
|
use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError};
|
||||
|
use ark_std::fmt::Debug;
|
||||
|
|
||||
|
/// FCircuit defines the trait of the circuit of the F function, which is the one being folded (ie.
|
||||
|
/// inside the agmented F' function).
|
||||
|
pub trait FCircuit<F: PrimeField>: Clone + Copy + Debug {
|
||||
|
type Params: Debug;
|
||||
|
|
||||
|
/// returns a new FCircuit instance
|
||||
|
fn new(params: Self::Params) -> Self;
|
||||
|
|
||||
|
/// computes the next state values in place, assigning z_{i+1} into z_i, and computing the new
|
||||
|
/// z_{i+1}
|
||||
|
fn step_native(
|
||||
|
// this method uses self, so that each FCircuit implementation (and different frontends)
|
||||
|
// can hold a state if needed to store data to compute the next state.
|
||||
|
self,
|
||||
|
z_i: Vec<F>,
|
||||
|
) -> Result<Vec<F>, Error>;
|
||||
|
|
||||
|
/// generates the constraints for the step of F for the given z_i
|
||||
|
fn generate_step_constraints(
|
||||
|
// this method uses self, so that each FCircuit implementation (and different frontends)
|
||||
|
// can hold a state if needed to store data to generate the constraints.
|
||||
|
self,
|
||||
|
cs: ConstraintSystemRef<F>,
|
||||
|
z_i: Vec<FpVar<F>>,
|
||||
|
) -> Result<Vec<FpVar<F>>, SynthesisError>;
|
||||
|
}
|
||||
|
|
||||
|
#[cfg(test)]
|
||||
|
pub mod tests {
|
||||
|
use super::*;
|
||||
|
use ark_pallas::Fr;
|
||||
|
use ark_r1cs_std::{alloc::AllocVar, eq::EqGadget};
|
||||
|
use ark_relations::r1cs::{
|
||||
|
ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError,
|
||||
|
};
|
||||
|
use core::marker::PhantomData;
|
||||
|
|
||||
|
/// CubicFCircuit is a struct that implements the FCircuit trait, for the R1CS example circuit
|
||||
|
/// from https://www.vitalik.ca/general/2016/12/10/qap.html, which checks `x^3 + x + 5 = y`. It
|
||||
|
/// has 2 public inputs which are used as the state. `z_i` is used as `x`, and `z_{i+1}` is
|
||||
|
/// used as `y`, and at the next step, `z_{i+1}` will be assigned to `z_i`, and a new `z+{i+1}`
|
||||
|
/// will be computted.
|
||||
|
#[derive(Clone, Copy, Debug)]
|
||||
|
pub struct CubicFCircuit<F: PrimeField> {
|
||||
|
_f: PhantomData<F>,
|
||||
|
}
|
||||
|
impl<F: PrimeField> FCircuit<F> for CubicFCircuit<F> {
|
||||
|
type Params = ();
|
||||
|
fn new(_params: Self::Params) -> Self {
|
||||
|
Self { _f: PhantomData }
|
||||
|
}
|
||||
|
fn step_native(self, z_i: Vec<F>) -> Result<Vec<F>, Error> {
|
||||
|
Ok(vec![z_i[0] * z_i[0] * z_i[0] + z_i[0] + F::from(5_u32)])
|
||||
|
}
|
||||
|
fn generate_step_constraints(
|
||||
|
self,
|
||||
|
cs: ConstraintSystemRef<F>,
|
||||
|
z_i: Vec<FpVar<F>>,
|
||||
|
) -> Result<Vec<FpVar<F>>, SynthesisError> {
|
||||
|
let five = FpVar::<F>::new_constant(cs.clone(), F::from(5u32))?;
|
||||
|
let z_i = z_i[0].clone();
|
||||
|
|
||||
|
Ok(vec![&z_i * &z_i * &z_i + &z_i + &five])
|
||||
|
}
|
||||
|
}
|
||||
|
|
||||
|
/// CustomFCircuit is a circuit that has the number of constraints specified in the
|
||||
|
/// `n_constraints` parameter. Note that the generated circuit will have very sparse matrices.
|
||||
|
#[derive(Clone, Copy, Debug)]
|
||||
|
pub struct CustomFCircuit<F: PrimeField> {
|
||||
|
_f: PhantomData<F>,
|
||||
|
pub n_constraints: usize,
|
||||
|
}
|
||||
|
impl<F: PrimeField> FCircuit<F> for CustomFCircuit<F> {
|
||||
|
type Params = usize;
|
||||
|
|
||||
|
fn new(params: Self::Params) -> Self {
|
||||
|
Self {
|
||||
|
_f: PhantomData,
|
||||
|
n_constraints: params,
|
||||
|
}
|
||||
|
}
|
||||
|
fn step_native(self, z_i: Vec<F>) -> Result<Vec<F>, Error> {
|
||||
|
let mut z_i1 = F::one();
|
||||
|
for _ in 0..self.n_constraints - 1 {
|
||||
|
z_i1 *= z_i[0];
|
||||
|
}
|
||||
|
Ok(vec![z_i1])
|
||||
|
}
|
||||
|
fn generate_step_constraints(
|
||||
|
self,
|
||||
|
cs: ConstraintSystemRef<F>,
|
||||
|
z_i: Vec<FpVar<F>>,
|
||||
|
) -> Result<Vec<FpVar<F>>, SynthesisError> {
|
||||
|
let mut z_i1 = FpVar::<F>::new_witness(cs.clone(), || Ok(F::one()))?;
|
||||
|
for _ in 0..self.n_constraints - 1 {
|
||||
|
z_i1 *= z_i[0].clone();
|
||||
|
}
|
||||
|
|
||||
|
Ok(vec![z_i1])
|
||||
|
}
|
||||
|
}
|
||||
|
|
||||
|
/// WrapperCircuit is a circuit that wraps any circuit that implements the FCircuit trait. This
|
||||
|
/// is used to test the `FCircuit.generate_step_constraints` method. This is a similar wrapping
|
||||
|
/// than the one done in the `AugmentedFCircuit`, but without adding all the extra constraints
|
||||
|
/// of the AugmentedF circuit logic, in order to run lighter tests when we're not interested in
|
||||
|
/// the the AugmentedF logic but in the wrapping of the circuits.
|
||||
|
pub struct WrapperCircuit<F: PrimeField, FC: FCircuit<F>> {
|
||||
|
pub FC: FC, // F circuit
|
||||
|
pub z_i: Option<Vec<F>>,
|
||||
|
pub z_i1: Option<Vec<F>>,
|
||||
|
}
|
||||
|
impl<F, FC> ConstraintSynthesizer<F> for WrapperCircuit<F, FC>
|
||||
|
where
|
||||
|
F: PrimeField,
|
||||
|
FC: FCircuit<F>,
|
||||
|
{
|
||||
|
fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
|
||||
|
let z_i = Vec::<FpVar<F>>::new_witness(cs.clone(), || {
|
||||
|
Ok(self.z_i.unwrap_or(vec![F::zero()]))
|
||||
|
})?;
|
||||
|
let z_i1 = Vec::<FpVar<F>>::new_input(cs.clone(), || {
|
||||
|
Ok(self.z_i1.unwrap_or(vec![F::zero()]))
|
||||
|
})?;
|
||||
|
let computed_z_i1 = self.FC.generate_step_constraints(cs.clone(), z_i.clone())?;
|
||||
|
|
||||
|
computed_z_i1.enforce_equal(&z_i1)?;
|
||||
|
Ok(())
|
||||
|
}
|
||||
|
}
|
||||
|
|
||||
|
#[test]
|
||||
|
fn test_testfcircuit() {
|
||||
|
let cs = ConstraintSystem::<Fr>::new_ref();
|
||||
|
let F_circuit = CubicFCircuit::<Fr>::new(());
|
||||
|
|
||||
|
let wrapper_circuit = WrapperCircuit::<Fr, CubicFCircuit<Fr>> {
|
||||
|
FC: F_circuit,
|
||||
|
z_i: Some(vec![Fr::from(3_u32)]),
|
||||
|
z_i1: Some(vec![Fr::from(35_u32)]),
|
||||
|
};
|
||||
|
wrapper_circuit.generate_constraints(cs.clone()).unwrap();
|
||||
|
assert_eq!(cs.num_constraints(), 3);
|
||||
|
}
|
||||
|
|
||||
|
#[test]
|
||||
|
fn test_customtestfcircuit() {
|
||||
|
let cs = ConstraintSystem::<Fr>::new_ref();
|
||||
|
let n_constraints = 1000;
|
||||
|
let custom_circuit = CustomFCircuit::<Fr>::new(n_constraints);
|
||||
|
let z_i = vec![Fr::from(5_u32)];
|
||||
|
let wrapper_circuit = WrapperCircuit::<Fr, CustomFCircuit<Fr>> {
|
||||
|
FC: custom_circuit,
|
||||
|
z_i: Some(z_i.clone()),
|
||||
|
z_i1: Some(custom_circuit.step_native(z_i).unwrap()),
|
||||
|
};
|
||||
|
wrapper_circuit.generate_constraints(cs.clone()).unwrap();
|
||||
|
assert_eq!(cs.num_constraints(), n_constraints);
|
||||
|
}
|
||||
|
}
|
||||