Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: folding-schemes docs + lint #188

Draft
wants to merge 11 commits into
base: main
Choose a base branch
from
11 changes: 9 additions & 2 deletions folding-schemes/src/arith/ccs/circuits.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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>>>,
}

Expand Down
40 changes: 37 additions & 3 deletions folding-schemes/src/arith/ccs/mod.rs
Original file line number Diff line number Diff line change
@@ -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;

Expand Down Expand Up @@ -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];

Expand All @@ -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)?)?;
}

Expand All @@ -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())
}
}

Expand Down Expand Up @@ -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(),
Expand Down Expand Up @@ -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)
}
Expand Down
90 changes: 88 additions & 2 deletions folding-schemes/src/arith/mod.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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,
Expand All @@ -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)
Expand All @@ -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>;
}
63 changes: 56 additions & 7 deletions folding-schemes/src/arith/r1cs/circuits.rs
Original file line number Diff line number Diff line change
@@ -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},
Expand All @@ -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>,
Expand All @@ -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)?,
})
})
}
Expand All @@ -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.
Expand Down Expand Up @@ -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)?;
Expand Down Expand Up @@ -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(())
}
Expand Down
Loading