sonobe_primitives/arithmetizations/ccs/
mod.rs

1//! This module implements the Customizable Constraint System (CCS) and its
2//! relation checks against plain witnesses and instances.
3//!
4//! Proposed in the CCS [paper], it is a generalization of R1CS as well as many
5//! other constraint systems.
6//! A CCS structure is defined by the following components:
7//! - The number of constraints `m`, the number of variables `n`, and the number
8//!   of public inputs `l`.
9//! - The degree `d`.
10//! - A sequence of `t` matrices `M`.
11//! - A sequence of `q` multisets `S`, where each multiset `S_i` has at most `d`
12//!   elements and each element is an index in `[0, t - 1]` pointing to a matrix
13//!   `M_j`.
14//! - A sequence of `q` coefficients `c`.
15//!
16//! A vector of assignments `z` satisfies the CCS if its evaluation
17//! `Σ_{i ∈ {0, q-1}} (c_i · 〇_{j ∈ S_i} (M_j · z))` is zero, where `〇` denotes
18//! the Hadamard product among all `M_j · z`.
19//!
20//! [paper]: https://eprint.iacr.org/2023/552.pdf
21
22use ark_ff::Field;
23use ark_poly::DenseMultilinearExtension;
24use ark_relations::gr1cs::{ConstraintSystem, Matrix};
25use ark_std::{cfg_into_iter, cfg_iter};
26#[cfg(feature = "parallel")]
27use rayon::prelude::*;
28
29use super::{Arith, Error};
30use crate::{algebra::ops::poly::MLEHelper, circuits::Assignments};
31
32/// [`CCS`] is an abstract trait that defines the behavior of all CCS variants,
33/// including but not limited to R1CS.
34pub trait CCS:
35    Arith + for<'a> From<&'a ConstraintSystem<Self::Field>> + From<ConstraintSystem<Self::Field>>
36{
37    /// [`CCS::Field`] specifies the underlying field of a CCS instance
38    type Field: Field;
39
40    /// [`CCS::matrices`] returns the matrices contained in a concrete CCS
41    /// instance `self`.
42    fn matrices(&self) -> &[Matrix<Self::Field>];
43
44    /// [`CCS::evaluate_ccs`] evaluates the CCS relation at a given vector of
45    /// assignments, multisets, and coefficients.
46    fn evaluate_ccs<const Q: usize>(
47        &self,
48        z: Assignments<Self::Field, impl AsRef<[Self::Field]> + Sync>,
49        multisets: [Vec<usize>; Q],
50        coefficients: [Self::Field; Q],
51    ) -> Result<Vec<Self::Field>, Error> {
52        let cfg = self.config();
53        let matrices = self.matrices();
54
55        let public_len = z.public.as_ref().len();
56        let private_len = z.private.as_ref().len();
57        if public_len != cfg.n_public_inputs {
58            return Err(Error::MalformedAssignments(format!(
59                "The number of public inputs in R1CS ({}) does not match the length of the provided public inputs ({}).",
60                cfg.n_public_inputs, public_len
61            )));
62        }
63        if private_len != cfg.n_witnesses {
64            return Err(Error::MalformedAssignments(format!(
65                "The number of witnesses in R1CS ({}) does not match the length of the provided witnesses ({}).",
66                cfg.n_witnesses, private_len
67            )));
68        }
69
70        // Recall that the evaluation of CCS at z is defined as:
71        // `Σ_{i ∈ {0, q-1}} (c_i · 〇_{j ∈ S_i} (M_j · z))`,
72        // where $\prod$ denotes the Hadamard product.
73        //
74        // Below, we manually expand the vector and matrix operations for less
75        // allocations and better efficiency.
76        // Specifically, we independently compute each entry of the resulting
77        // vector, and collect them at the end.
78        // We parallelize the outer loop over rows (when the `parallel` feature
79        // is enabled), since the number of constraints in the CCS is typically
80        // large in practice.
81        Ok(cfg_into_iter!(0..cfg.n_constraints)
82            .map(|row| {
83                // The `row`-th entry of the resulting vector is:
84                // `Σ_{i ∈ {0, q-1}} (c_i · 〇_{j ∈ S_i} (M_j[row] · z))`
85                multisets
86                    .iter()
87                    .zip(coefficients)
88                    .map(|(s, c)| {
89                        // Each term in the sum is:
90                        // `c_i · 〇_{j ∈ S_i} (M_j[row] · z)`
91                        c * s
92                            .iter()
93                            .map(|&i| {
94                                // Each factor in the product is `M_j[row] · z`,
95                                // i.e., the dot product of `M_j[row]` and `z`.
96                                matrices[i][row]
97                                    .iter()
98                                    .map(|(val, col)| z[*col] * val)
99                                    .sum::<Self::Field>()
100                            })
101                            .product::<Self::Field>()
102                    })
103                    .sum()
104            })
105            .collect())
106    }
107
108    /// [`CCS::mles`] returns the multilinear extensions of all CCS matrices
109    /// `M_i` evaluated over the assignments `z`.
110    fn mles(
111        &self,
112        z: Assignments<Self::Field, impl AsRef<[Self::Field]> + Sync>,
113    ) -> Vec<DenseMultilinearExtension<Self::Field>> {
114        self.matrices()
115            .iter()
116            .map(|matrix| {
117                DenseMultilinearExtension::from_evaluations(
118                    &cfg_iter!(matrix)
119                        .map(|row| row.iter().map(|(val, col)| z[*col] * val).sum())
120                        .collect::<Vec<_>>(),
121                )
122            })
123            .collect()
124    }
125}
sonobe_primitives/arithmetizations/ccs/mod.rs

sonobe_primitives/arithmetizations/ccs/
mod.rs
