From 7d769484303926af12d1941dcaa45ac7dc4ec7eb Mon Sep 17 00:00:00 2001 From: Colin Roberts Date: Fri, 20 Dec 2024 07:16:21 -0700 Subject: [PATCH] docs: `arith` module --- folding-schemes/src/arith/ccs/circuits.rs | 11 ++- folding-schemes/src/arith/ccs/mod.rs | 40 +++++++++- folding-schemes/src/arith/mod.rs | 90 +++++++++++++++++++++- folding-schemes/src/arith/r1cs/circuits.rs | 63 +++++++++++++-- folding-schemes/src/arith/r1cs/mod.rs | 69 ++++++++++++++--- 5 files changed, 250 insertions(+), 23 deletions(-) diff --git a/folding-schemes/src/arith/ccs/circuits.rs b/folding-schemes/src/arith/ccs/circuits.rs index 5a2e99ab..ebdaeb7a 100644 --- a/folding-schemes/src/arith/ccs/circuits.rs +++ b/folding-schemes/src/arith/ccs/circuits.rs @@ -1,3 +1,9 @@ +//! Circuit implementations for Customizable Constraint Systems (CCS). +//! +//! This module provides the circuit (gadget) variants of CCS components for use in +//! constraint system implementations. These are used when CCS operations need to +//! be performed inside another constraint system. + use super::CCS; use crate::utils::gadgets::SparseMatrixVar; use ark_ff::PrimeField; @@ -8,10 +14,11 @@ use ark_r1cs_std::{ use ark_relations::r1cs::{Namespace, SynthesisError}; use ark_std::borrow::Borrow; -/// CCSMatricesVar contains the matrices 'M' of the CCS without the rest of CCS parameters. +/// [`CCSMatricesVar`] contains the matrices 'M' of the CCS without the rest of CCS parameters. #[derive(Debug, Clone)] pub struct CCSMatricesVar { - // we only need native representation, so the constraint field==F + /// Vector of sparse matrices in their circuit representation + /// We only need native representation, so the constraint field equals F pub M: Vec>>, } diff --git a/folding-schemes/src/arith/ccs/mod.rs b/folding-schemes/src/arith/ccs/mod.rs index 666ef9e2..9758bf85 100644 --- a/folding-schemes/src/arith/ccs/mod.rs +++ b/folding-schemes/src/arith/ccs/mod.rs @@ -1,3 +1,29 @@ +//! Implementation of Customizable Constraint Systems (CCS). +//! +//! This module provides an implementation of CCS as defined in the +//! [CCS paper](https://eprint.iacr.org/2023/552). CCS is a generalization +//! of constraint systems that allows for flexible constraint expressions +//! via configurable matrix operations. +//! +//! # Structure +//! +//! A CCS consists of: +//! * A set of sparse matrices M₁...Mₜ ∈ F^{m×n} +//! * A collection of multisets S₁...Sₘ containing indices into these matrices +//! * A vector of coefficients c₁...cₘ +//! +//! # Example +//! +//! A simple R1CS constraint system can be represented as a CCS with: +//! * Three matrices A, B, C +//! * Two multisets S₁ = {0,1}, S₂ = {2} +//! * Coefficients c₁ = 1, c₂ = -1 +//! +//! # Organization +//! +//! * [`CCS`] - The main CCS type implementing the [`Arith`] trait +//! * [`circuits`] - Circuit implementations for CCS operations + use ark_ff::PrimeField; use ark_std::log2; @@ -42,6 +68,13 @@ pub struct CCS { impl CCS { /// Evaluates the CCS relation at a given vector of assignments `z` + /// + /// # Errors + /// + /// Returns an error if: + /// * Vector operations fail due to mismatched dimensions + /// * Matrix-vector multiplication fails + /// * Vector addition or hadamard multiplication fails pub fn eval_at_z(&self, z: &[F]) -> Result, Error> { let mut result = vec![F::zero(); self.m]; @@ -51,7 +84,7 @@ impl CCS { // complete the hadamard chain let mut hadamard_result = vec![F::one(); self.m]; - for M_j in vec_M_j.into_iter() { + for M_j in vec_M_j { hadamard_result = hadamard(&hadamard_result, &mat_vec_mul(M_j, z)?)?; } @@ -67,7 +100,7 @@ impl CCS { /// 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()) + (z[self.l + 1..].to_vec(), z[1..=self.l].to_vec()) } } @@ -101,7 +134,7 @@ impl From> for CCS { fn from(r1cs: R1CS) -> Self { let m = r1cs.num_constraints(); let n = r1cs.num_variables(); - CCS { + Self { m, n, l: r1cs.num_public_inputs(), @@ -130,6 +163,7 @@ pub mod tests { pub fn get_test_ccs() -> CCS { get_test_r1cs::().into() } + pub fn get_test_z(input: usize) -> Vec { r1cs_get_test_z(input) } diff --git a/folding-schemes/src/arith/mod.rs b/folding-schemes/src/arith/mod.rs index b5ebd7b8..98bd28d8 100644 --- a/folding-schemes/src/arith/mod.rs +++ b/folding-schemes/src/arith/mod.rs @@ -1,3 +1,48 @@ +//! Trait definitions and implementations for arithmetic constraint systems. +//! +//! This module provides core abstractions for working with different types of arithmetic +//! constraint systems like R1CS (Rank-1 Constraint Systems) and CCS (Customizable Constraint Systems). +//! The key trait [`Arith`] defines a generic interface that constraint systems must implement, +//! allowing the rest of the library to work with different constraint system implementations in a +//! uniform way. +//! +//! # Key Traits +//! +//! * [`Arith`] - Core trait defining operations that constraint systems must support +//! * [`ArithGadget`] - In-circuit counterpart operations for constraint systems +//! * [`ArithSampler`] - Optional trait for sampling random satisfying witness-instance pairs +//! * [`ArithSerializer`] - Serialization support for constraint systems +//! +//! # Modules +//! +//! * [`ccs`] - Implementation of Customizable Constraint Systems (CCS) +//! * [`r1cs`] - Implementation of Rank-1 Constraint Systems (R1CS) +//! +//! # Examples of Supported Systems +//! +//! The module supports various constraint system types including: +//! +//! * Plain R1CS - Traditional rank-1 constraint systems +//! * Nova's Relaxed R1CS - Modified R1CS with relaxation terms +//! * ProtoGalaxy's Relaxed R1CS - Alternative relaxation approach +//! * CCS - Customizable constraint systems with different witness/instance types +//! +//! Each system can define its own witness (`W`) and instance (`U`) types while implementing +//! the common [`Arith`] interface, allowing for flexible constraint system implementations +//! while maintaining a consistent API. +//! +//! # Evaluation Types +//! +//! Different constraint systems can have different evaluation semantics: +//! +//! * Plain R1CS evaluates to `Az ∘ Bz - Cz` +//! * Nova's Relaxed R1CS evaluates to `Az ∘ Bz - uCz` +//! * ProtoGalaxy's version evaluates to `Az ∘ Bz - Cz` +//! * CCS can have various evaluation forms +//! +//! The [`Arith`] trait's associated `Evaluation` type allows each system to define its own +//! evaluation result type while maintaining type safety. + use ark_ec::CurveGroup; use ark_relations::r1cs::SynthesisError; use ark_std::rand::RngCore; @@ -42,6 +87,7 @@ pub mod r1cs; /// elements, [`crate::folding::hypernova::Witness`] and [`crate::folding::hypernova::lcccs::LCCCS`], /// or [`crate::folding::hypernova::Witness`] and [`crate::folding::hypernova::cccs::CCCS`]. pub trait Arith: Clone { + /// The type for the output of the relation's evalation. type Evaluation; /// Returns a dummy witness and instance @@ -64,11 +110,16 @@ pub trait Arith: Clone { /// - Evaluating the relaxed R1CS in Nova at `W = (w, e, ...)` and /// `U = (u, x, ...)` returns `Az ∘ Bz - uCz`, where `z = [u, x, w]`. /// - /// - Evaluating the relaxed R1CS in ProtoGalaxy at `W = (w, ...)` and + /// - Evaluating the relaxed R1CS in [`crate::folding::protogalaxy`] at `W = (w, ...)` and /// `U = (x, e, β, ...)` returns `Az ∘ Bz - Cz`, where `z = [1, x, w]`. /// /// However, we use `Self::Evaluation` to represent the evaluation result /// for future extensibility. + /// + /// # Errors + /// Returns an error if: + /// - The dimensions of vectors don't match the expected sizes + /// - The evaluation calculations fail fn eval_relation(&self, w: &W, u: &U) -> Result; /// Checks if the evaluation result is valid. The witness `w` and instance @@ -82,9 +133,14 @@ pub trait Arith: Clone { /// - The evaluation `v` of relaxed R1CS in Nova at satisfying `W` and `U` /// should be equal to the error term `e` in the witness. /// - /// - The evaluation `v` of relaxed R1CS in ProtoGalaxy at satisfying `W` + /// - The evaluation `v` of relaxed R1CS in [`crate::folding::protogalaxy`] at satisfying `W` /// and `U` should satisfy `e = Σ pow_i(β) v_i`, where `e` is the error /// term in the committed instance. + /// + /// # Errors + /// Returns an error if: + /// - The evaluation result is not valid for the given witness and instance + /// - The evaluation result fails to satisfy the constraint system requirements fn check_evaluation(w: &W, u: &U, v: Self::Evaluation) -> Result<(), Error>; /// Checks if witness `w` and instance `u` satisfy the constraint system @@ -92,6 +148,12 @@ pub trait Arith: Clone { /// validity of the evaluation result. /// /// Used only for testing. + /// + /// # Errors + /// Returns an error if: + /// - The evaluation fails (`eval_relation` errors) + /// - The evaluation check fails (`check_evaluation` errors) + /// - The witness and instance do not satisfy the constraint system fn check_relation(&self, w: &W, u: &U) -> Result<(), Error> { let e = self.eval_relation(w, u)?; Self::check_evaluation(w, u, e) @@ -125,6 +187,12 @@ pub trait ArithSerializer { /// [HyperNova]: https://eprint.iacr.org/2023/573.pdf pub trait ArithSampler: Arith { /// Samples a random witness and instance that satisfy the constraint system. + /// + /// # Errors + /// Returns an error if: + /// - Sampling of random values fails + /// - The commitment scheme operations fail + /// - The sampled values do not satisfy the constraint system fn sample_witness_instance>( &self, params: &CS::ProverParams, @@ -135,15 +203,28 @@ pub trait ArithSampler: Arith { /// `ArithGadget` defines the in-circuit counterparts of operations specified in /// `Arith` on constraint systems. pub trait ArithGadget { + /// The type for the output of the relation's evalation. type Evaluation; /// Evaluates the constraint system `self` at witness `w` and instance `u`. /// Returns the evaluation result. + /// + /// # Errors + /// Returns a `SynthesisError` if: + /// - Circuit constraint generation fails + /// - Variable allocation fails + /// - Required witness values are missing fn eval_relation(&self, w: &WVar, u: &UVar) -> Result; /// Generates constraints for enforcing that witness `w` and instance `u` /// satisfy the constraint system `self` by first computing the evaluation /// result and then checking the validity of the evaluation result. + /// + /// # Errors + /// Returns a `SynthesisError` if: + /// - The evaluation fails (`eval_relation` errors) + /// - The enforcement of evaluation constraints fails + /// - Circuit constraint generation fails fn enforce_relation(&self, w: &WVar, u: &UVar) -> Result<(), SynthesisError> { let e = self.eval_relation(w, u)?; Self::enforce_evaluation(w, u, e) @@ -152,5 +233,10 @@ pub trait ArithGadget { /// Generates constraints for enforcing that the evaluation result is valid. /// The witness `w` and instance `u` are also parameters, because the /// validity check may need information contained in `w` and/or `u`. + /// + /// # Errors + /// Returns a `SynthesisError` if: + /// - Circuit constraint generation fails for the evaluation check + /// - The enforcement of evaluation constraints fails fn enforce_evaluation(w: &WVar, u: &UVar, e: Self::Evaluation) -> Result<(), SynthesisError>; } diff --git a/folding-schemes/src/arith/r1cs/circuits.rs b/folding-schemes/src/arith/r1cs/circuits.rs index e870b585..b8f6c574 100644 --- a/folding-schemes/src/arith/r1cs/circuits.rs +++ b/folding-schemes/src/arith/r1cs/circuits.rs @@ -1,3 +1,9 @@ +//! Circuit implementations for Rank-1 Constraint Systems (R1CS). +//! +//! This module provides an in-circuit representation of R1CS for use within other circuits. +//! It includes support for both native field operations and non-native field arithmetic +//! through generic matrix and vector operations. + use crate::{ arith::ArithGadget, utils::gadgets::{EquivalenceGadget, MatrixGadget, SparseMatrixVar, VectorGadget}, @@ -11,19 +17,44 @@ use super::R1CS; /// An in-circuit representation of the `R1CS` struct. /// -/// `M` is for the modulo operation involved in the satisfiability check when -/// the underlying `FVar` is `NonNativeUintVar`. +/// This gadget allows R1CS operations to be performed within another constraint system. +/// +/// # Type Parameters +/// +/// * `M` - Type for the modulo operation in satisfiability checks when `FVar` is `NonNativeUintVar` +/// * `FVar` - Variable type representing field elements in the circuit #[derive(Debug, Clone)] pub struct R1CSMatricesVar { + /// Phantom data for the modulo type _m: PhantomData, + /// In-circuit representation of matrix A pub A: SparseMatrixVar, + /// In-circuit representation of matrix B pub B: SparseMatrixVar, + /// In-circuit representation of matrix C pub C: SparseMatrixVar, } impl> AllocVar, ConstraintF> for R1CSMatricesVar { + /// Creates a new circuit representation of R1CS matrices + /// + /// # Type Parameters + /// + /// * `T` - Type that can be borrowed as `R1CS` + /// + /// # Arguments + /// + /// * `cs` - Constraint system handle + /// * `f` - Function that returns the R1CS to be converted to circuit form + /// * `_mode` - Allocation mode (unused as matrices are allocated as constants) + /// + /// # Errors + /// + /// Returns a `SynthesisError` if: + /// * Matrix conversion to circuit form fails + /// * Circuit variable allocation fails fn new_variable>>( cs: impl Into>, f: impl FnOnce() -> Result, @@ -32,11 +63,12 @@ impl> f().and_then(|val| { let cs = cs.into(); + // TODO (autoparallel): How expensive are these clones? Is there a cheaper way to do this? Ok(Self { _m: PhantomData, A: SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().A)?, B: SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().B)?, - C: SparseMatrixVar::::new_constant(cs.clone(), &val.borrow().C)?, + C: SparseMatrixVar::::new_constant(cs, &val.borrow().C)?, }) }) } @@ -47,6 +79,24 @@ where SparseMatrixVar: MatrixGadget, [FVar]: VectorGadget, { + /// Evaluates the R1CS matrices at given circuit variable assignments + /// + /// # Arguments + /// + /// * `z` - Vector of circuit variables to evaluate at + /// + /// # Returns + /// + /// Returns a tuple (AzBz, uCz) where: + /// * AzBz is the Hadamard product of Az and Bz + /// * uCz is Cz scaled by z[0] + /// + /// # Errors + /// + /// Returns a `SynthesisError` if: + /// * Matrix-vector multiplication fails + /// * Hadamard product computation fails + /// * Vector operations fail pub fn eval_at_z(&self, z: &[FVar]) -> Result<(Vec, Vec), SynthesisError> { // Multiply Cz by z[0] (u) here, allowing this method to be reused for // both relaxed and unrelaxed R1CS. @@ -225,7 +275,7 @@ pub mod tests { 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 y = Vec::>::new_input(cs, || Ok(self.y))?; let unitVar = UnitVar::default(); let comp_y = as CRHSchemeGadget>::evaluate(&unitVar, &x)?; @@ -289,15 +339,14 @@ pub mod tests { let cs = ConstraintSystem::::new_ref(); let wVar = WitnessVar::new_witness(cs.clone(), || Ok(&w))?; let uVar = CommittedInstanceVar::new_witness(cs.clone(), || Ok(&u))?; - let r1csVar = R1CSMatricesVar::>::new_witness(cs.clone(), || Ok(&r1cs))?; + let r1csVar = R1CSMatricesVar::>::new_witness(cs, || Ok(&r1cs))?; r1csVar.enforce_relation(&wVar, &uVar)?; // non-natively let cs = ConstraintSystem::::new_ref(); let wVar = CycleFoldWitnessVar::new_witness(cs.clone(), || Ok(w))?; let uVar = CycleFoldCommittedInstanceVar::<_, GVar2>::new_witness(cs.clone(), || Ok(u))?; - let r1csVar = - R1CSMatricesVar::>::new_witness(cs.clone(), || Ok(r1cs))?; + let r1csVar = R1CSMatricesVar::>::new_witness(cs, || Ok(r1cs))?; r1csVar.enforce_relation(&wVar, &uVar)?; Ok(()) } diff --git a/folding-schemes/src/arith/r1cs/mod.rs b/folding-schemes/src/arith/r1cs/mod.rs index 683d0888..d8039617 100644 --- a/folding-schemes/src/arith/r1cs/mod.rs +++ b/folding-schemes/src/arith/r1cs/mod.rs @@ -1,3 +1,23 @@ +//! Implementation of Rank-1 Constraint Systems (R1CS). +//! +//! This module provides an implementation of R1CS, which represents arithmetic circuits +//! as a system of bilinear constraints. An R1CS consists of three sparse matrices A, B, C +//! and defines relations of the form: +//! +//! (Az) ∘ (Bz) = Cz +//! +//! where z is a vector containing all circuit variables including: +//! * A constant 1 +//! * Public inputs +//! * Private witness values +//! +//! # Features +//! +//! * Standard R1CS constraint system +//! * Conversion to/from CCS format +//! * Support for relaxed R1CS variants +//! * Extraction from arkworks constraint systems + use ark_ff::PrimeField; use ark_relations::r1cs::ConstraintSystem; use ark_serialize::{CanonicalDeserialize, CanonicalSerialize}; @@ -12,16 +32,27 @@ use crate::Error; pub mod circuits; +/// Represents a Rank-1 Constraint System with three sparse matrices A, B, C. #[derive(Debug, Clone, Eq, PartialEq, CanonicalSerialize, CanonicalDeserialize)] pub struct R1CS { - pub l: usize, // io len + /// Number of public inputs/outputs + pub l: usize, + /// Left matrix A pub A: SparseMatrix, + /// Right matrix B pub B: SparseMatrix, + /// Output matrix C pub C: SparseMatrix, } impl R1CS { /// Evaluates the CCS relation at a given vector of variables `z` + /// + /// # Errors + /// + /// Returns an error if: + /// * The length of z doesn't match the number of columns in the matrices + /// * Matrix operations fail due to dimension mismatches pub fn eval_at_z(&self, z: &[F]) -> Result, Error> { if z.len() != self.A.n_cols { return Err(Error::NotSameLength( @@ -66,15 +97,19 @@ impl ArithSerializer for R1CS { } } +// TODO (autoparallel): Many of these functions could be marked with `#[must_use]`(i.e., just like functions that return `Result` do). impl R1CS { + /// Creates an empty R1CS pub fn empty() -> Self { - R1CS { + Self { l: 0, A: SparseMatrix::empty(), B: SparseMatrix::empty(), C: SparseMatrix::empty(), } } + + /// Creates a random R1CS with given dimensions pub fn rand(rng: &mut R, n_rows: usize, n_cols: usize) -> Self { Self { l: 1, @@ -84,35 +119,39 @@ impl R1CS { } } + /// Returns the number of constraints #[inline] - pub fn num_constraints(&self) -> usize { + pub const fn num_constraints(&self) -> usize { self.A.n_rows } + /// Returns the number of public inputs #[inline] - pub fn num_public_inputs(&self) -> usize { + pub const fn num_public_inputs(&self) -> usize { self.l } + /// Returns the total number of variables #[inline] - pub fn num_variables(&self) -> usize { + pub const fn num_variables(&self) -> usize { self.A.n_cols } + /// Returns the number of witness variables #[inline] - pub fn num_witnesses(&self) -> usize { + pub const fn num_witnesses(&self) -> usize { self.num_variables() - self.num_public_inputs() - 1 } /// 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()) + (z[self.l + 1..].to_vec(), z[1..=self.l].to_vec()) } } impl From> for R1CS { fn from(ccs: CCS) -> Self { - R1CS:: { + Self { l: ccs.l, A: ccs.M[0].clone(), B: ccs.M[1].clone(), @@ -121,8 +160,14 @@ impl From> for R1CS { } } -/// extracts arkworks ConstraintSystem matrices into crate::utils::vec::SparseMatrix format as R1CS +/// extracts arkworks [`ConstraintSystem`] matrices into [`crate::utils::vec::SparseMatrix`] format as R1CS /// struct. +/// +/// # Errors +/// +/// Returns an error if: +/// * The constraint system matrices haven't been generated yet +/// * The conversion between matrix formats fails pub fn extract_r1cs(cs: &ConstraintSystem) -> Result, Error> { let m = cs.to_matrices().ok_or_else(|| { Error::ConversionError( @@ -160,6 +205,12 @@ pub fn extract_r1cs(cs: &ConstraintSystem) -> Result, } /// extracts the witness and the public inputs from arkworks ConstraintSystem. +/// +/// # Returns +/// +/// Returns a tuple (w, x) containing: +/// * w: The witness assignment vector +/// * x: The public input vector (excluding the constant 1) pub fn extract_w_x(cs: &ConstraintSystem) -> (Vec, Vec) { ( cs.witness_assignment.clone(),