1#![allow(non_snake_case)]
  2#![allow(non_upper_case_globals)]
  3#![allow(non_camel_case_types)]
  4#![allow(clippy::upper_case_acronyms)]
  5
  6use ark_ff::PrimeField;
  7use ark_r1cs_std::alloc::AllocVar;
  8use ark_r1cs_std::fields::fp::FpVar;
  9use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError};
 10use core::marker::PhantomData;
 11use std::time::Instant;
 12
 13use ark_pallas::{constraints::GVar, Fr, Projective};
 14use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
 15
 16use folding_schemes::commitment::pedersen::Pedersen;
 17use folding_schemes::folding::nova::Nova;
 18use folding_schemes::frontend::FCircuit;
 19use folding_schemes::{Error, FoldingScheme};
 20mod utils;
 21use utils::test_nova_setup;
 22
 23/// This is the circuit that we want to fold, it implements the FCircuit trait. The parameter z_i
 24/// denotes the current state which contains 5 elements, and z_{i+1} denotes the next state which
 25/// we get by applying the step.
 26/// In this example we set z_i and z_{i+1} to have five elements, and at each step we do different
 27/// operations on each of them.
 28#[derive(Clone, Copy, Debug)]
 29pub struct MultiInputsFCircuit<F: PrimeField> {
 30    _f: PhantomData<F>,
 31}
 32impl<F: PrimeField> FCircuit<F> for MultiInputsFCircuit<F> {
 33    type Params = ();
 34
 35    fn new(_params: Self::Params) -> Self {
 36        Self { _f: PhantomData }
 37    }
 38    fn state_len(self) -> usize {
 39        5
 40    }
 41
 42    /// computes the next state values in place, assigning z_{i+1} into z_i, and computing the new
 43    /// z_{i+1}
 44    fn step_native(self, z_i: Vec<F>) -> Result<Vec<F>, Error> {
 45        let a = z_i[0] + F::from(4_u32);
 46        let b = z_i[1] + F::from(40_u32);
 47        let c = z_i[2] * F::from(4_u32);
 48        let d = z_i[3] * F::from(40_u32);
 49        let e = z_i[4] + F::from(100_u32);
 50
 51        Ok(vec![a, b, c, d, e])
 52    }
 53
 54    /// generates the constraints for the step of F for the given z_i
 55    fn generate_step_constraints(
 56        self,
 57        cs: ConstraintSystemRef<F>,
 58        z_i: Vec<FpVar<F>>,
 59    ) -> Result<Vec<FpVar<F>>, SynthesisError> {
 60        let four = FpVar::<F>::new_constant(cs.clone(), F::from(4u32))?;
 61        let fourty = FpVar::<F>::new_constant(cs.clone(), F::from(40u32))?;
 62        let onehundred = FpVar::<F>::new_constant(cs.clone(), F::from(100u32))?;
 63        let a = z_i[0].clone() + four.clone();
 64        let b = z_i[1].clone() + fourty.clone();
 65        let c = z_i[2].clone() * four;
 66        let d = z_i[3].clone() * fourty;
 67        let e = z_i[4].clone() + onehundred;
 68
 69        Ok(vec![a, b, c, d, e])
 70    }
 71}
 72
 73/// cargo test --example multi_inputs
 74#[cfg(test)]
 75pub mod tests {
 76    use super::*;
 77    use ark_r1cs_std::alloc::AllocVar;
 78    use ark_relations::r1cs::ConstraintSystem;
 79
 80    // test to check that the MultiInputsFCircuit computes the same values inside and outside the circuit
 81    #[test]
 82    fn test_add_f_circuit() {
 83        let cs = ConstraintSystem::<Fr>::new_ref();
 84
 85        let circuit = MultiInputsFCircuit::<Fr>::new(());
 86        let z_i = vec![
 87            Fr::from(1_u32),
 88            Fr::from(1_u32),
 89            Fr::from(1_u32),
 90            Fr::from(1_u32),
 91            Fr::from(1_u32),
 92        ];
 93
 94        let z_i1 = circuit.step_native(z_i.clone()).unwrap();
 95
 96        let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i)).unwrap();
 97        let computed_z_i1Var = circuit
 98            .generate_step_constraints(cs.clone(), z_iVar.clone())
 99            .unwrap();
100        assert_eq!(computed_z_i1Var.value().unwrap(), z_i1);
101    }
102}
103
104/// cargo run --release --example multi_inputs
105fn main() {
106    let num_steps = 10;
107    let initial_state = vec![
108        Fr::from(1_u32),
109        Fr::from(1_u32),
110        Fr::from(1_u32),
111        Fr::from(1_u32),
112        Fr::from(1_u32),
113    ];
114
115    let F_circuit = MultiInputsFCircuit::<Fr>::new(());
116
117    println!("Prepare Nova ProverParams & VerifierParams");
118    let (prover_params, verifier_params) = test_nova_setup::<MultiInputsFCircuit<Fr>>(F_circuit);
119
120    /// The idea here is that eventually we could replace the next line chunk that defines the
121    /// `type NOVA = Nova<...>` by using another folding scheme that fulfills the `FoldingScheme`
122    /// trait, and the rest of our code would be working without needing to be updated.
123    type NOVA = Nova<
124        Projective,
125        GVar,
126        Projective2,
127        GVar2,
128        MultiInputsFCircuit<Fr>,
129        Pedersen<Projective>,
130        Pedersen<Projective2>,
131    >;
132
133    println!("Initialize FoldingScheme");
134    let mut folding_scheme = NOVA::init(&prover_params, F_circuit, initial_state.clone()).unwrap();
135
136    // compute a step of the IVC
137    for i in 0..num_steps {
138        let start = Instant::now();
139        folding_scheme.prove_step().unwrap();
140        println!("Nova::prove_step {}: {:?}", i, start.elapsed());
141    }
142
143    let (running_instance, incomming_instance, cyclefold_instance) = folding_scheme.instances();
144
145    println!("Run the Nova's IVC verifier");
146    NOVA::verify(
147        verifier_params,
148        initial_state.clone(),
149        folding_scheme.state(), // latest state
150        Fr::from(num_steps as u32),
151        running_instance,
152        incomming_instance,
153        cyclefold_instance,
154    )
155    .unwrap();
156}