1use ark_crypto_primitives::sponge::Absorb;
  2use ark_ec::CurveGroup;
  3use ark_std::fmt::Debug;
  4use ark_std::{rand::RngCore, UniformRand};
  5
  6use super::{CommittedInstance, Witness};
  7use crate::arith::ArithSampler;
  8use crate::arith::{r1cs::R1CS, Arith};
  9use crate::commitment::CommitmentScheme;
 10use crate::folding::circuits::CF1;
 11use crate::transcript::Transcript;
 12use crate::Error;
 13
 14/// Defines the NIFS (Non-Interactive Folding Scheme) trait, initially defined in
 15/// [Nova](https://eprint.iacr.org/2021/370.pdf), and it's variants
 16/// [Ova](https://hackmd.io/V4838nnlRKal9ZiTHiGYzw) and
 17/// [Mova](https://eprint.iacr.org/2024/1220.pdf).
 18/// `H` specifies whether the NIFS will use a blinding factor.
 19pub trait NIFSTrait<C: CurveGroup, CS: CommitmentScheme<C, H>, const H: bool = false> {
 20    type CommittedInstance: Debug + Clone + Absorb;
 21    type Witness: Debug + Clone;
 22    type ProverAux: Debug + Clone; // Prover's aux params
 23    type VerifierAux: Debug + Clone; // Verifier's aux params
 24
 25    fn new_witness(w: Vec<C::ScalarField>, e_len: usize, rng: impl RngCore) -> Self::Witness;
 26    fn new_instance(
 27        w: &Self::Witness,
 28        params: &CS::ProverParams,
 29        x: Vec<C::ScalarField>,
 30        aux: Vec<C::ScalarField>, // t_or_e in Ova, empty for Nova
 31    ) -> Result<Self::CommittedInstance, Error>;
 32
 33    fn fold_witness(
 34        r: C::ScalarField,
 35        W: &Self::Witness, // running witness
 36        w: &Self::Witness, // incoming witness
 37        aux: &Self::ProverAux,
 38    ) -> Result<Self::Witness, Error>;
 39
 40    /// computes the auxiliary parameters, eg. in Nova: (T, cmT), in Ova: T
 41    fn compute_aux(
 42        cs_prover_params: &CS::ProverParams,
 43        r1cs: &R1CS<C::ScalarField>,
 44        W_i: &Self::Witness,
 45        U_i: &Self::CommittedInstance,
 46        w_i: &Self::Witness,
 47        u_i: &Self::CommittedInstance,
 48    ) -> Result<(Self::ProverAux, Self::VerifierAux), Error>;
 49
 50    fn get_challenge<T: Transcript<C::ScalarField>>(
 51        transcript: &mut T,
 52        pp_hash: C::ScalarField, // public params hash
 53        U_i: &Self::CommittedInstance,
 54        u_i: &Self::CommittedInstance,
 55        aux: &Self::VerifierAux, // ie. in Nova wouild be cmT, in Ova it's empty
 56    ) -> Vec<bool>;
 57
 58    /// NIFS.P. Notice that this method is implemented at the trait level, and depends on the other
 59    /// two methods `fold_witness` and `verify`.
 60    fn prove(
 61        r: C::ScalarField,
 62        W_i: &Self::Witness,           // running witness
 63        U_i: &Self::CommittedInstance, // running committed instance
 64        w_i: &Self::Witness,           // incoming witness
 65        u_i: &Self::CommittedInstance, // incoming committed instance
 66        aux_p: &Self::ProverAux,
 67        aux_v: &Self::VerifierAux,
 68    ) -> Result<(Self::Witness, Self::CommittedInstance), Error> {
 69        let w = Self::fold_witness(r, W_i, w_i, aux_p)?;
 70        let ci = Self::verify(r, U_i, u_i, aux_v);
 71        Ok((w, ci))
 72    }
 73
 74    /// NIFS.V
 75    fn verify(
 76        // r comes from the transcript, and is a n-bit (N_BITS_CHALLENGE) element
 77        r: C::ScalarField,
 78        U_i: &Self::CommittedInstance,
 79        u_i: &Self::CommittedInstance,
 80        aux: &Self::VerifierAux,
 81    ) -> Self::CommittedInstance;
 82}
 83
 84/// Implements `Arith` for R1CS, where the witness is of type [`Witness`], and
 85/// the committed instance is of type [`CommittedInstance`].
 86///
 87/// Due to the error terms `Witness.E` and `CommittedInstance.u`, R1CS here is
 88/// considered as a relaxed R1CS.
 89///
 90/// One may wonder why we do not provide distinct structs for R1CS and relaxed
 91/// R1CS.
 92/// This is because both plain R1CS and relaxed R1CS have the same structure:
 93/// they are both represented by three matrices.
 94/// What makes them different is the error terms, which are not part of the R1CS
 95/// struct, but are part of the witness and committed instance.
 96///
 97/// As a follow-up, one may further ask why not providing a trait for relaxed
 98/// R1CS and implement it for the `R1CS` struct, where the relaxed R1CS trait
 99/// has methods for relaxed satisfiability check, while the `Arith` trait that
100/// `R1CS` implements has methods for plain satisfiability check.
101/// However, it would be more ideal if we have a single method that can smartly
102/// choose the type of satisfiability check, which would make the code more
103/// generic and easier to maintain.
104///
105/// This is achieved thanks to the new design of the [`Arith`] trait, where we
106/// can implement the trait for the same constraint system with different types
107/// of witnesses and committed instances.
108/// For R1CS, whether it is relaxed or not is now determined by the types of `W`
109/// and `U`: the satisfiability check is relaxed if `W` and `U` are defined by
110/// folding schemes, and plain if they are vectors of field elements.
111impl<C: CurveGroup> Arith<Witness<C>, CommittedInstance<C>> for R1CS<CF1<C>> {
112    type Evaluation = Vec<CF1<C>>;
113
114    fn eval_relation(
115        &self,
116        w: &Witness<C>,
117        u: &CommittedInstance<C>,
118    ) -> Result<Self::Evaluation, Error> {
119        self.eval_at_z(&[&[u.u][..], &u.x, &w.W].concat())
120    }
121
122    fn check_evaluation(
123        w: &Witness<C>,
124        _u: &CommittedInstance<C>,
125        e: Self::Evaluation,
126    ) -> Result<(), Error> {
127        (w.E == e).then_some(()).ok_or(Error::NotSatisfied)
128    }
129}
130
131impl<C: CurveGroup> ArithSampler<C, Witness<C>, CommittedInstance<C>> for R1CS<CF1<C>> {
132    fn sample_witness_instance<CS: CommitmentScheme<C, true>>(
133        &self,
134        params: &CS::ProverParams,
135        mut rng: impl RngCore,
136    ) -> Result<(Witness<C>, CommittedInstance<C>), Error> {
137        // Implements sampling a (committed) RelaxedR1CS
138        // See construction 5 in https://eprint.iacr.org/2023/573.pdf
139        let u = C::ScalarField::rand(&mut rng);
140        let rE = C::ScalarField::rand(&mut rng);
141        let rW = C::ScalarField::rand(&mut rng);
142
143        let W = (0..self.A.n_cols - self.l - 1)
144            .map(|_| C::ScalarField::rand(&mut rng))
145            .collect();
146        let x = (0..self.l)
147            .map(|_| C::ScalarField::rand(&mut rng))
148            .collect::<Vec<C::ScalarField>>();
149        let mut z = vec![u];
150        z.extend(&x);
151        z.extend(&W);
152
153        let E = self.eval_at_z(&z)?;
154
155        let witness = Witness { E, rE, W, rW };
156        let mut cm_witness = witness.commit::<CS, true>(params, x)?;
157
158        // witness.commit() sets u to 1, we set it to the sampled u value
159        cm_witness.u = u;
160
161        debug_assert!(
162            self.check_relation(&witness, &cm_witness).is_ok(),
163            "Sampled a non satisfiable relaxed R1CS, sampled u: {}, computed E: {:?}",
164            u,
165            witness.E
166        );
167
168        Ok((witness, cm_witness))
169    }
170}