1use ark_ec::CurveGroup;
  2use ark_relations::r1cs::SynthesisError;
  3use ark_std::rand::RngCore;
  4
  5use crate::{commitment::CommitmentScheme, folding::traits::Dummy, Error};
  6
  7pub mod ccs;
  8pub mod r1cs;
  9
 10/// `Arith` defines the operations that a constraint system (e.g., R1CS, CCS,
 11/// etc.) should support.
 12///
 13/// Here, `W` is the type of witness, and `U` is the type of statement / public
 14/// input / public IO / instance.
 15/// Note that the same constraint system may support different types of `W` and
 16/// `U`, and the satisfiability check may vary.
 17///
 18/// For example, both plain R1CS and relaxed R1CS are represented by 3 matrices,
 19/// but the types of `W` and `U` are different:
 20/// - The plain R1CS has `W` and `U` as vectors of field elements.
 21///   
 22///   `W = w` and `U = x` satisfy R1CS if `Az ∘ Bz = Cz`, where `z = [1, x, w]`.
 23///
 24/// - In Nova, Relaxed R1CS has `W` as [`crate::folding::nova::Witness`],
 25///   and `U` as [`crate::folding::nova::CommittedInstance`].
 26///  
 27///   `W = (w, e, ...)` and `U = (u, x, ...)` satisfy Relaxed R1CS if
 28///   `Az ∘ Bz = uCz + e`, where `z = [u, x, w]`.
 29///   (commitments in `U` are not checked here)
 30///
 31///   Also, `W` and `U` have non-native field elements as their components when
 32///   used as CycleFold witness and instance.
 33///
 34/// - In ProtoGalaxy, Relaxed R1CS has `W` as [`crate::folding::protogalaxy::Witness`],
 35///   and `U` as [`crate::folding::protogalaxy::CommittedInstance`].
 36///    
 37///   `W = (w, ...)` and `U = (x, e, β, ...)` satisfy Relaxed R1CS if
 38///   `e = Σ pow_i(β) v_i`, where `v = Az ∘ Bz - Cz`, `z = [1, x, w]`.
 39///   (commitments in `U` are not checked here)
 40///
 41/// This is also the case of CCS, where `W` and `U` may be vectors of field
 42/// elements, [`crate::folding::hypernova::Witness`] and [`crate::folding::hypernova::lcccs::LCCCS`],
 43/// or [`crate::folding::hypernova::Witness`] and [`crate::folding::hypernova::cccs::CCCS`].
 44pub trait Arith<W, U>: Clone {
 45    type Evaluation;
 46
 47    /// Returns a dummy witness and instance
 48    fn dummy_witness_instance<'a>(&'a self) -> (W, U)
 49    where
 50        W: Dummy<&'a Self>,
 51        U: Dummy<&'a Self>,
 52    {
 53        (W::dummy(self), U::dummy(self))
 54    }
 55
 56    /// Evaluates the constraint system `self` at witness `w` and instance `u`.
 57    /// Returns the evaluation result.
 58    ///
 59    /// The evaluation result is usually a vector of field elements.
 60    /// For instance:
 61    /// - Evaluating the plain R1CS at `W = w` and `U = x` returns
 62    ///   `Az ∘ Bz - Cz`, where `z = [1, x, w]`.
 63    ///
 64    /// - Evaluating the relaxed R1CS in Nova at `W = (w, e, ...)` and
 65    ///   `U = (u, x, ...)` returns `Az ∘ Bz - uCz`, where `z = [u, x, w]`.
 66    ///
 67    /// - Evaluating the relaxed R1CS in ProtoGalaxy at `W = (w, ...)` and
 68    ///   `U = (x, e, β, ...)` returns `Az ∘ Bz - Cz`, where `z = [1, x, w]`.
 69    ///
 70    /// However, we use `Self::Evaluation` to represent the evaluation result
 71    /// for future extensibility.
 72    fn eval_relation(&self, w: &W, u: &U) -> Result<Self::Evaluation, Error>;
 73
 74    /// Checks if the evaluation result is valid. The witness `w` and instance
 75    /// `u` are also parameters, because the validity check may need information
 76    /// contained in `w` and/or `u`.
 77    ///
 78    /// For instance:
 79    /// - The evaluation `v` of plain R1CS at satisfying `W` and `U` should be
 80    ///   an all-zero vector.
 81    ///
 82    /// - The evaluation `v` of relaxed R1CS in Nova at satisfying `W` and `U`
 83    ///   should be equal to the error term `e` in the witness.
 84    ///
 85    /// - The evaluation `v` of relaxed R1CS in ProtoGalaxy at satisfying `W`
 86    ///   and `U` should satisfy `e = Σ pow_i(β) v_i`, where `e` is the error
 87    ///   term in the committed instance.
 88    fn check_evaluation(w: &W, u: &U, v: Self::Evaluation) -> Result<(), Error>;
 89
 90    /// Checks if witness `w` and instance `u` satisfy the constraint system
 91    /// `self` by first computing the evaluation result and then checking the
 92    /// validity of the evaluation result.
 93    ///
 94    /// Used only for testing.
 95    fn check_relation(&self, w: &W, u: &U) -> Result<(), Error> {
 96        let e = self.eval_relation(w, u)?;
 97        Self::check_evaluation(w, u, e)
 98    }
 99}
100
101/// `ArithSerializer` is for serializing constraint systems.
102///
103/// Currently we only support converting parameters to bytes, but in the future
104/// we may consider implementing methods for serializing the actual data (e.g.,
105/// R1CS matrices).
106pub trait ArithSerializer {
107    /// Returns the bytes that represent the parameters, that is, the matrices sizes, the amount of
108    /// public inputs, etc, without the matrices/polynomials values.
109    fn params_to_le_bytes(&self) -> Vec<u8>;
110}
111
112/// `ArithSampler` allows sampling random pairs of witness and instance that
113/// satisfy the constraint system `self`.
114///
115/// This is useful for constructing a zero-knowledge layer for a folding-based
116/// IVC.
117/// An example of such a layer can be found in Appendix D of the [HyperNova]
118/// paper.
119///
120/// Note that we use a separate trait for sampling, because this operation may
121/// not be supported by all witness-instance pairs.
122/// For instance, it is difficult (if not impossible) to do this for `w` and `x`
123/// in a plain R1CS.
124///
125/// [HyperNova]: https://eprint.iacr.org/2023/573.pdf
126pub trait ArithSampler<C: CurveGroup, W, U>: Arith<W, U> {
127    /// Samples a random witness and instance that satisfy the constraint system.
128    fn sample_witness_instance<CS: CommitmentScheme<C, true>>(
129        &self,
130        params: &CS::ProverParams,
131        rng: impl RngCore,
132    ) -> Result<(W, U), Error>;
133}
134
135/// `ArithGadget` defines the in-circuit counterparts of operations specified in
136/// `Arith` on constraint systems.
137pub trait ArithGadget<WVar, UVar> {
138    type Evaluation;
139
140    /// Evaluates the constraint system `self` at witness `w` and instance `u`.
141    /// Returns the evaluation result.
142    fn eval_relation(&self, w: &WVar, u: &UVar) -> Result<Self::Evaluation, SynthesisError>;
143
144    /// Generates constraints for enforcing that witness `w` and instance `u`
145    /// satisfy the constraint system `self` by first computing the evaluation
146    /// result and then checking the validity of the evaluation result.
147    fn enforce_relation(&self, w: &WVar, u: &UVar) -> Result<(), SynthesisError> {
148        let e = self.eval_relation(w, u)?;
149        Self::enforce_evaluation(w, u, e)
150    }
151
152    /// Generates constraints for enforcing that the evaluation result is valid.
153    /// The witness `w` and instance `u` are also parameters, because the
154    /// validity check may need information contained in `w` and/or `u`.
155    fn enforce_evaluation(w: &WVar, u: &UVar, e: Self::Evaluation) -> Result<(), SynthesisError>;
156}