From ac913ab573ae41ed3021db966fc35e6acb2ece2d Mon Sep 17 00:00:00 2001 From: arnaucube Date: Thu, 7 Sep 2023 19:21:30 +0200 Subject: [PATCH] Add decider circuit RelaxedR1CS (#21) - Add naive decider circuit `RelaxedR1CSGadget`, which in-circuit checks that the given z satisfies the given RelaxedR1CS instance - Add method to relax the R1CS instance - Add check_relation (for testing only) to R1CS & RelaxedR1CS - Migrate from own SparseMatrix to use ark_relations::r1cs::Matrix - Add frontend helper to use arkworks circuits --- Cargo.toml | 1 + src/ccs/r1cs.rs | 59 +++++++ src/decider/circuit.rs | 291 +++++++++++++++++++++++++++++++++++ src/decider/mod.rs | 1 + src/frontend/arkworks/mod.rs | 100 ++++++++++++ src/frontend/mod.rs | 1 + src/lib.rs | 2 + src/utils/vec.rs | 47 +++++- 8 files changed, 495 insertions(+), 7 deletions(-) create mode 100644 src/decider/circuit.rs create mode 100644 src/decider/mod.rs create mode 100644 src/frontend/arkworks/mod.rs create mode 100644 src/frontend/mod.rs diff --git a/Cargo.toml b/Cargo.toml index 08f0d87..c0a732f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -23,6 +23,7 @@ espresso_transcript = {git="https://github.com/EspressoSystems/hyperplonk", pack [dev-dependencies] ark-pallas = {version="0.4.0", features=["r1cs"]} ark-vesta = {version="0.4.0"} +ark-crypto-primitives = { version = "^0.4.0", default-features = false, features = ["crh"] } [features] default = ["parallel"] diff --git a/src/ccs/r1cs.rs b/src/ccs/r1cs.rs index 78d04b5..c5f1c80 100644 --- a/src/ccs/r1cs.rs +++ b/src/ccs/r1cs.rs @@ -1,6 +1,7 @@ use ark_ff::PrimeField; use crate::utils::vec::*; +use crate::Error; #[derive(Debug, Clone, Eq, PartialEq)] pub struct R1CS { @@ -9,17 +10,67 @@ pub struct R1CS { pub B: SparseMatrix, pub C: SparseMatrix, } + impl R1CS { /// returns a tuple containing (w, x) (witness and public inputs respectively) pub fn split_z(&self, z: &[F]) -> (Vec, Vec) { (z[self.l + 1..].to_vec(), z[1..self.l + 1].to_vec()) } + + /// check that a R1CS structure is satisfied by a z vector. Only for testing. + pub fn check_relation(&self, z: &[F]) -> Result<(), Error> { + let Az = mat_vec_mul_sparse(&self.A, z); + let Bz = mat_vec_mul_sparse(&self.B, z); + let Cz = mat_vec_mul_sparse(&self.C, z); + let AzBz = hadamard(&Az, &Bz); + assert_eq!(AzBz, Cz); + + Ok(()) + } + + /// converts the R1CS instance into a RelaxedR1CS as described in + /// [Nova](https://eprint.iacr.org/2021/370.pdf) section 4.1. + pub fn relax(self) -> RelaxedR1CS { + RelaxedR1CS:: { + l: self.l, + E: vec![F::zero(); self.A.n_rows], + A: self.A, + B: self.B, + C: self.C, + u: F::one(), + } + } +} + +#[derive(Debug, Clone, Eq, PartialEq)] +pub struct RelaxedR1CS { + pub l: usize, // io len + pub A: SparseMatrix, + pub B: SparseMatrix, + pub C: SparseMatrix, + pub u: F, + pub E: Vec, +} +impl RelaxedR1CS { + /// check that a RelaxedR1CS structure is satisfied by a z vector. Only for testing. + pub fn check_relation(&self, z: &[F]) -> Result<(), Error> { + let Az = mat_vec_mul_sparse(&self.A, z); + let Bz = mat_vec_mul_sparse(&self.B, z); + let Cz = mat_vec_mul_sparse(&self.C, z); + let uCz = vec_scalar_mul(&Cz, &self.u); + let uCzE = vec_add(&uCz, &self.E); + let AzBz = hadamard(&Az, &Bz); + assert_eq!(AzBz, uCzE); + + Ok(()) + } } #[cfg(test)] pub mod tests { use super::*; use crate::utils::vec::tests::{to_F_matrix, to_F_vec}; + use ark_pallas::Fr; pub fn get_test_r1cs() -> R1CS { // R1CS for: x^3 + x + 5 = y (example from article @@ -57,4 +108,12 @@ pub mod tests { input * input * input + input, // x^3 + x ]) } + + #[test] + fn test_check_relation() { + let r1cs = get_test_r1cs::(); + let z = get_test_z(5); + r1cs.check_relation(&z).unwrap(); + r1cs.relax().check_relation(&z).unwrap(); + } } diff --git a/src/decider/circuit.rs b/src/decider/circuit.rs new file mode 100644 index 0000000..14fcce6 --- /dev/null +++ b/src/decider/circuit.rs @@ -0,0 +1,291 @@ +use ark_ec::CurveGroup; +use ark_ff::{Field, PrimeField}; +use ark_r1cs_std::{ + alloc::{AllocVar, AllocationMode}, + eq::EqGadget, + fields::{fp::FpVar, FieldVar}, +}; +use ark_relations::r1cs::{Namespace, SynthesisError}; +use core::{borrow::Borrow, marker::PhantomData}; + +use crate::ccs::r1cs::RelaxedR1CS; +use crate::utils::vec::SparseMatrix; + +pub type ConstraintF = <::BaseField as Field>::BasePrimeField; + +#[derive(Debug, Clone)] +pub struct RelaxedR1CSGadget { + _f: PhantomData, +} +impl RelaxedR1CSGadget { + /// performs the RelaxedR1CS check (Az∘Bz==uCz+E) + pub fn check(rel_r1cs: RelaxedR1CSVar, z: Vec>) -> Result<(), SynthesisError> { + let Az = mat_vec_mul_sparse(rel_r1cs.A, z.clone()); + let Bz = mat_vec_mul_sparse(rel_r1cs.B, z.clone()); + let Cz = mat_vec_mul_sparse(rel_r1cs.C, z.clone()); + let uCz = vec_scalar_mul(&Cz, &rel_r1cs.u); + let uCzE = vec_add(&uCz, &rel_r1cs.E); + let AzBz = hadamard(&Az, &Bz); + for i in 0..AzBz.len() { + AzBz[i].enforce_equal(&uCzE[i].clone())?; + } + Ok(()) + } +} + +fn mat_vec_mul_sparse(m: SparseMatrixVar, v: Vec>) -> Vec> { + let mut res = vec![FpVar::::zero(); m.n_rows]; + for (row_i, row) in m.coeffs.iter().enumerate() { + for (value, col_i) in row.iter() { + res[row_i] += value * v[*col_i].clone(); + } + } + res +} +pub fn vec_add(a: &Vec>, b: &Vec>) -> Vec> { + assert_eq!(a.len(), b.len()); + let mut r: Vec> = vec![FpVar::::zero(); a.len()]; + for i in 0..a.len() { + r[i] = a[i].clone() + b[i].clone(); + } + r +} +pub fn vec_scalar_mul(vec: &Vec>, c: &FpVar) -> Vec> { + let mut result = vec![FpVar::::zero(); vec.len()]; + for (i, a) in vec.iter().enumerate() { + result[i] = a.clone() * c; + } + result +} +pub fn hadamard(a: &Vec>, b: &Vec>) -> Vec> { + assert_eq!(a.len(), b.len()); + let mut r: Vec> = vec![FpVar::::zero(); a.len()]; + for i in 0..a.len() { + r[i] = a[i].clone() * b[i].clone(); + } + r +} + +#[derive(Debug, Clone)] +pub struct SparseMatrixVar { + pub n_rows: usize, + pub n_cols: usize, + // same format as the native SparseMatrix (which follows ark_relations::r1cs::Matrix format + pub coeffs: Vec, usize)>>, +} + +impl AllocVar, F> for SparseMatrixVar +where + F: PrimeField, +{ + fn new_variable>>( + cs: impl Into>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let mut coeffs: Vec, usize)>> = Vec::new(); + for row in val.borrow().coeffs.iter() { + let mut rowVar: Vec<(FpVar, usize)> = Vec::new(); + for &(value, col_i) in row.iter() { + let coeffVar = FpVar::::new_variable(cs.clone(), || Ok(value), mode)?; + rowVar.push((coeffVar, col_i)); + } + coeffs.push(rowVar); + } + + Ok(Self { + n_rows: val.borrow().n_rows, + n_cols: val.borrow().n_cols, + coeffs, + }) + }) + } +} + +#[derive(Debug, Clone)] +pub struct RelaxedR1CSVar { + pub A: SparseMatrixVar, + pub B: SparseMatrixVar, + pub C: SparseMatrixVar, + pub u: FpVar, + pub E: Vec>, +} + +impl AllocVar, F> for RelaxedR1CSVar +where + F: PrimeField, +{ + fn new_variable>>( + cs: impl Into>, + f: impl FnOnce() -> Result, + mode: AllocationMode, + ) -> Result { + f().and_then(|val| { + let cs = cs.into(); + + let A = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().A)?; + let B = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().B)?; + let C = SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().C)?; + let E = Vec::>::new_variable(cs.clone(), || Ok(val.borrow().E.clone()), mode)?; + let u = FpVar::::new_variable(cs.clone(), || Ok(val.borrow().u), mode)?; + + Ok(Self { A, B, C, E, u }) + }) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use ark_crypto_primitives::crh::{ + sha256::{ + constraints::{Sha256Gadget, UnitVar}, + Sha256, + }, + CRHScheme, CRHSchemeGadget, + }; + use ark_ff::BigInteger; + use ark_pallas::Fr; + use ark_r1cs_std::{alloc::AllocVar, bits::uint8::UInt8}; + use ark_relations::r1cs::{ + ConstraintSynthesizer, ConstraintSystem, ConstraintSystemRef, SynthesisError, + }; + use ark_std::One; + + use crate::ccs::r1cs::{ + tests::{get_test_r1cs, get_test_z}, + R1CS, + }; + use crate::frontend::arkworks::{extract_r1cs_and_z, tests::TestCircuit}; + + #[test] + fn test_relaxed_r1cs_small_gadget_handcrafted() { + let r1cs: R1CS = get_test_r1cs(); + let rel_r1cs = r1cs.relax(); + let z = get_test_z(3); + + let cs = ConstraintSystem::::new_ref(); + + let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); + let rel_r1csVar = RelaxedR1CSVar::::new_witness(cs.clone(), || Ok(rel_r1cs)).unwrap(); + + RelaxedR1CSGadget::::check(rel_r1csVar, zVar).unwrap(); + assert!(cs.is_satisfied().unwrap()); + dbg!(cs.num_constraints()); + } + + // gets as input a circuit that implements the ConstraintSynthesizer trait, and that has been + // initialized. + fn test_relaxed_r1cs_gadget>(circuit: CS) { + let cs = ConstraintSystem::::new_ref(); + + circuit.generate_constraints(cs.clone()).unwrap(); + cs.finalize(); + assert!(cs.is_satisfied().unwrap()); + + // num constraints of the original circuit + dbg!(cs.num_constraints()); + + let cs = cs.into_inner().unwrap(); + + let (r1cs, z) = extract_r1cs_and_z::(&cs); + r1cs.check_relation(&z).unwrap(); + + let relaxed_r1cs = r1cs.relax(); + relaxed_r1cs.check_relation(&z).unwrap(); + + // set new CS for the circuit that checks the RelaxedR1CS of our original circuit + let cs = ConstraintSystem::::new_ref(); + // prepare the inputs for our circuit + let zVar = Vec::>::new_witness(cs.clone(), || Ok(z)).unwrap(); + let rel_r1csVar = + RelaxedR1CSVar::::new_witness(cs.clone(), || Ok(relaxed_r1cs)).unwrap(); + + RelaxedR1CSGadget::::check(rel_r1csVar, zVar).unwrap(); + assert!(cs.is_satisfied().unwrap()); + + // num constraints of the circuit that checks the RelaxedR1CS of the original circuit + dbg!(cs.num_constraints()); + } + + #[test] + fn test_relaxed_r1cs_small_gadget_arkworks() { + let x = Fr::from(5_u32); + let y = x * x * x + x + Fr::from(5_u32); + let circuit = TestCircuit:: { x, y }; + test_relaxed_r1cs_gadget(circuit); + } + + struct Sha256TestCircuit { + _f: PhantomData, + pub x: Vec, + pub y: Vec, + } + impl ConstraintSynthesizer for Sha256TestCircuit { + fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { + let x = Vec::>::new_witness(cs.clone(), || Ok(self.x))?; + let y = Vec::>::new_input(cs.clone(), || Ok(self.y))?; + + let unitVar = UnitVar::default(); + let comp_y = as CRHSchemeGadget>::evaluate(&unitVar, &x)?; + comp_y.0.enforce_equal(&y)?; + Ok(()) + } + } + #[test] + fn test_relaxed_r1cs_medium_gadget_arkworks() { + let x = Fr::from(5_u32).into_bigint().to_bytes_le(); + let y = ::evaluate(&(), x.clone()).unwrap(); + + let circuit = Sha256TestCircuit:: { + _f: PhantomData, + x, + y, + }; + test_relaxed_r1cs_gadget(circuit); + } + + // circuit that has the numer of constraints specified in the `n_constraints` parameter. Note + // that the generated circuit will have very sparse matrices, so the resulting constraints + // number of the RelaxedR1CS gadget must take that into account. + struct CustomTestCircuit { + _f: PhantomData, + pub n_constraints: usize, + pub x: F, + pub y: F, + } + impl ConstraintSynthesizer for CustomTestCircuit { + fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { + let x = FpVar::::new_witness(cs.clone(), || Ok(self.x))?; + let y = FpVar::::new_input(cs.clone(), || Ok(self.y))?; + + let mut comp_y = FpVar::::new_witness(cs.clone(), || Ok(F::one()))?; + for _ in 0..self.n_constraints - 1 { + comp_y *= x.clone(); + } + + comp_y.enforce_equal(&y)?; + Ok(()) + } + } + #[test] + fn test_relaxed_r1cs_custom_circuit() { + let n_constraints = 10_000; + let x = Fr::from(5_u32); + let mut y = Fr::one(); + for _ in 0..n_constraints - 1 { + y *= x; + } + + let circuit = CustomTestCircuit:: { + _f: PhantomData, + n_constraints, + x, + y, + }; + test_relaxed_r1cs_gadget(circuit); + } +} diff --git a/src/decider/mod.rs b/src/decider/mod.rs new file mode 100644 index 0000000..db89e61 --- /dev/null +++ b/src/decider/mod.rs @@ -0,0 +1 @@ +pub mod circuit; diff --git a/src/frontend/arkworks/mod.rs b/src/frontend/arkworks/mod.rs new file mode 100644 index 0000000..644b912 --- /dev/null +++ b/src/frontend/arkworks/mod.rs @@ -0,0 +1,100 @@ +/// 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(cs: &ConstraintSystem) -> (R1CS, Vec) { + 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:: { + n_rows, + n_cols, + coeffs: m.a, + }; + let B = SparseMatrix:: { + n_rows, + n_cols, + coeffs: m.b, + }; + let C = SparseMatrix:: { + n_rows, + n_cols, + coeffs: m.c, + }; + + // z = (1, x, w) + let z: Vec = [ + // 1 is already included in cs.instance_assignment + cs.instance_assignment.clone(), + cs.witness_assignment.clone(), + ] + .concat(); + + ( + R1CS:: { + l: cs.num_instance_variables, + A, + B, + C, + }, + z, + ) +} + +#[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 { + pub x: F, + pub y: F, + } + impl ConstraintSynthesizer for TestCircuit { + fn generate_constraints(self, cs: ConstraintSystemRef) -> Result<(), SynthesisError> { + let x = FpVar::::new_input(cs.clone(), || Ok(self.x))?; + let y = FpVar::::new_witness(cs.clone(), || Ok(self.y))?; + let five = FpVar::::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::::new_ref(); + + let x = Fr::from(5_u32); + let y = x * x * x + x + Fr::from(5_u32); + + let test_circuit = TestCircuit:: { 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::(&cs); + r1cs.check_relation(&z).unwrap(); + } +} diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs new file mode 100644 index 0000000..3222a46 --- /dev/null +++ b/src/frontend/mod.rs @@ -0,0 +1 @@ +pub mod arkworks; diff --git a/src/lib.rs b/src/lib.rs index 78a01ce..29e7935 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -10,7 +10,9 @@ pub mod transcript; use transcript::Transcript; pub mod ccs; pub mod constants; +pub mod decider; pub mod folding; +pub mod frontend; pub mod pedersen; pub mod utils; diff --git a/src/utils/vec.rs b/src/utils/vec.rs index 9118c78..5552f69 100644 --- a/src/utils/vec.rs +++ b/src/utils/vec.rs @@ -1,4 +1,5 @@ use ark_ff::PrimeField; +pub use ark_relations::r1cs::Matrix as R1CSMatrix; use ark_std::cfg_iter; use rayon::iter::{IndexedParallelIterator, IntoParallelRefIterator, ParallelIterator}; @@ -6,7 +7,21 @@ use rayon::iter::{IndexedParallelIterator, IntoParallelRefIterator, ParallelIter pub struct SparseMatrix { pub n_rows: usize, pub n_cols: usize, - pub coeffs: Vec<(usize, usize, F)>, + /// coeffs = R1CSMatrix = Vec>, which contains each row and the F is the value + /// of the coefficient and the usize indicates the column position + pub coeffs: R1CSMatrix, +} + +impl SparseMatrix { + pub fn to_dense(&self) -> Vec> { + let mut r: Vec> = vec![vec![F::zero(); self.n_cols]; self.n_rows]; + for (row_i, row) in self.coeffs.iter().enumerate() { + for &(value, col_i) in row.iter() { + r[row_i][col_i] = value; + } + } + r + } } pub fn dense_matrix_to_sparse(m: Vec>) -> SparseMatrix { @@ -15,12 +30,14 @@ pub fn dense_matrix_to_sparse(m: Vec>) -> SparseMatrix n_cols: m[0].len(), coeffs: Vec::new(), }; - for (i, m_i) in m.iter().enumerate() { - for (j, m_ij) in m_i.iter().enumerate() { - if !m_ij.is_zero() { - r.coeffs.push((i, j, *m_ij)); + for m_row in m.iter() { + let mut row: Vec<(F, usize)> = Vec::new(); + for (col_i, value) in m_row.iter().enumerate() { + if !value.is_zero() { + row.push((*value, col_i)); } } + r.coeffs.push(row); } r } @@ -75,9 +92,12 @@ pub fn mat_vec_mul(M: &Vec>, z: &[F]) -> Vec { pub fn mat_vec_mul_sparse(matrix: &SparseMatrix, vector: &[F]) -> Vec { let mut res = vec![F::zero(); matrix.n_rows]; - for &(row, col, value) in matrix.coeffs.iter() { - res[row] += value * vector[col]; + for (row_i, row) in matrix.coeffs.iter().enumerate() { + for &(value, col_i) in row.iter() { + res[row_i] += value * vector[col_i]; + } } + res } @@ -109,6 +129,19 @@ pub mod tests { r } + #[test] + fn test_dense_sparse_conversions() { + let A = to_F_matrix::(vec![ + vec![0, 1, 0, 0, 0, 0], + vec![0, 0, 0, 1, 0, 0], + vec![0, 1, 0, 0, 1, 0], + vec![5, 0, 0, 0, 0, 1], + ]); + let A_sparse = dense_matrix_to_sparse(A.clone()); + assert_eq!(A_sparse.to_dense(), A); + } + + // test mat_vec_mul & mat_vec_mul_sparse #[test] fn test_mat_vec_mul() { let A = to_F_matrix::(vec![