docs: arith module

Author: Colin Roberts

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<F: PrimeField> {
-    // 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<SparseMatrixVar<FpVar<F>>>,
 }
 

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<F: PrimeField> {
 
 impl<F: PrimeField> CCS<F> {
     /// 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<Vec<F>, Error> {
         let mut result = vec![F::zero(); self.m];
 
@@ -51,7 +84,7 @@ impl<F: PrimeField> CCS<F> {
 
             // 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<F: PrimeField> CCS<F> {
 
     /// returns a tuple containing (w, x) (witness and public inputs respectively)
     pub fn split_z(&self, z: &[F]) -> (Vec<F>, Vec<F>) {
-        (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<F: PrimeField> From<R1CS<F>> for CCS<F> {
     fn from(r1cs: R1CS<F>) -> 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<F: PrimeField>() -> CCS<F> {
         get_test_r1cs::<F>().into()
     }
+
     pub fn get_test_z<F: PrimeField>(input: usize) -> Vec<F> {
         r1cs_get_test_z(input)
     }

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<W, U>: 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<W, U>: 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<Self::Evaluation, Error>;
 
     /// Checks if the evaluation result is valid. The witness `w` and instance
@@ -82,16 +133,27 @@ pub trait Arith<W, U>: 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
     /// `self` by first computing the evaluation result and then checking the
     /// 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<C: CurveGroup, W, U>: Arith<W, U> {
     /// 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<CS: CommitmentScheme<C, true>>(
         &self,
         params: &CS::ProverParams,
@@ -135,15 +203,28 @@ pub trait ArithSampler<C: CurveGroup, W, U>: Arith<W, U> {
 /// `ArithGadget` defines the in-circuit counterparts of operations specified in
 /// `Arith` on constraint systems.
 pub trait ArithGadget<WVar, UVar> {
+    /// 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<Self::Evaluation, SynthesisError>;
 
     /// 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<WVar, UVar> {
     /// 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>;
 }

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<M, FVar> {
+    /// Phantom data for the modulo type
     _m: PhantomData<M>,
+    /// In-circuit representation of matrix A
     pub A: SparseMatrixVar<FVar>,
+    /// In-circuit representation of matrix B
     pub B: SparseMatrixVar<FVar>,
+    /// In-circuit representation of matrix C
     pub C: SparseMatrixVar<FVar>,
 }
 
 impl<F: PrimeField, ConstraintF: PrimeField, FVar: AllocVar<F, ConstraintF>>
     AllocVar<R1CS<F>, ConstraintF> for R1CSMatricesVar<F, FVar>
 {
+    /// Creates a new circuit representation of R1CS matrices
+    ///
+    /// # Type Parameters
+    ///
+    /// * `T` - Type that can be borrowed as `R1CS<F>`
+    ///
+    /// # 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<T: Borrow<R1CS<F>>>(
         cs: impl Into<Namespace<ConstraintF>>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
@@ -32,11 +63,12 @@ impl<F: PrimeField, ConstraintF: PrimeField, FVar: AllocVar<F, ConstraintF>>
         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::<FVar>::new_constant(cs.clone(), &val.borrow().A)?,
                 B: SparseMatrixVar::<FVar>::new_constant(cs.clone(), &val.borrow().B)?,
-                C: SparseMatrixVar::<FVar>::new_constant(cs.clone(), &val.borrow().C)?,
+                C: SparseMatrixVar::<FVar>::new_constant(cs, &val.borrow().C)?,
             })
         })
     }
@@ -47,6 +79,24 @@ where
     SparseMatrixVar<FVar>: MatrixGadget<FVar>,
     [FVar]: VectorGadget<FVar>,
 {
+    /// 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<FVar>, Vec<FVar>), 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<F: PrimeField> ConstraintSynthesizer<F> for Sha256TestCircuit<F> {
         fn generate_constraints(self, cs: ConstraintSystemRef<F>) -> Result<(), SynthesisError> {
             let x = Vec::<UInt8<F>>::new_witness(cs.clone(), || Ok(self.x))?;
-            let y = Vec::<UInt8<F>>::new_input(cs.clone(), || Ok(self.y))?;
+            let y = Vec::<UInt8<F>>::new_input(cs, || Ok(self.y))?;
 
             let unitVar = UnitVar::default();
             let comp_y = <Sha256Gadget<F> as CRHSchemeGadget<Sha256, F>>::evaluate(&unitVar, &x)?;
@@ -289,15 +339,14 @@ pub mod tests {
         let cs = ConstraintSystem::<Fq>::new_ref();
         let wVar = WitnessVar::new_witness(cs.clone(), || Ok(&w))?;
         let uVar = CommittedInstanceVar::new_witness(cs.clone(), || Ok(&u))?;
-        let r1csVar = R1CSMatricesVar::<Fq, FpVar<Fq>>::new_witness(cs.clone(), || Ok(&r1cs))?;
+        let r1csVar = R1CSMatricesVar::<Fq, FpVar<Fq>>::new_witness(cs, || Ok(&r1cs))?;
         r1csVar.enforce_relation(&wVar, &uVar)?;
 
         // non-natively
         let cs = ConstraintSystem::<Fr>::new_ref();
         let wVar = CycleFoldWitnessVar::new_witness(cs.clone(), || Ok(w))?;
         let uVar = CycleFoldCommittedInstanceVar::<_, GVar2>::new_witness(cs.clone(), || Ok(u))?;
-        let r1csVar =
-            R1CSMatricesVar::<Fq, NonNativeUintVar<Fr>>::new_witness(cs.clone(), || Ok(r1cs))?;
+        let r1csVar = R1CSMatricesVar::<Fq, NonNativeUintVar<Fr>>::new_witness(cs, || Ok(r1cs))?;
         r1csVar.enforce_relation(&wVar, &uVar)?;
         Ok(())
     }