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, _i: usize, 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        _i: usize,
 59        z_i: Vec<FpVar<F>>,
 60    ) -> Result<Vec<FpVar<F>>, SynthesisError> {
 61        let four = FpVar::<F>::new_constant(cs.clone(), F::from(4u32))?;
 62        let forty = FpVar::<F>::new_constant(cs.clone(), F::from(40u32))?;
 63        let onehundred = FpVar::<F>::new_constant(cs.clone(), F::from(100u32))?;
 64        let a = z_i[0].clone() + four.clone();
 65        let b = z_i[1].clone() + forty.clone();
 66        let c = z_i[2].clone() * four;
 67        let d = z_i[3].clone() * forty;
 68        let e = z_i[4].clone() + onehundred;
 69
 70        Ok(vec![a, b, c, d, e])
 71    }
 72}
 73
 74/// cargo test --example multi_inputs
 75#[cfg(test)]
 76pub mod tests {
 77    use super::*;
 78    use ark_r1cs_std::{alloc::AllocVar, R1CSVar};
 79    use ark_relations::r1cs::ConstraintSystem;
 80
 81    // test to check that the MultiInputsFCircuit computes the same values inside and outside the circuit
 82    #[test]
 83    fn test_f_circuit() {
 84        let cs = ConstraintSystem::<Fr>::new_ref();
 85
 86        let circuit = MultiInputsFCircuit::<Fr>::new(());
 87        let z_i = vec![
 88            Fr::from(1_u32),
 89            Fr::from(1_u32),
 90            Fr::from(1_u32),
 91            Fr::from(1_u32),
 92            Fr::from(1_u32),
 93        ];
 94
 95        let z_i1 = circuit.step_native(0, z_i.clone()).unwrap();
 96
 97        let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i)).unwrap();
 98        let computed_z_i1Var = circuit
 99            .generate_step_constraints(cs.clone(), 0, z_iVar.clone())
100            .unwrap();
101        assert_eq!(computed_z_i1Var.value().unwrap(), z_i1);
102    }
103}
104
105/// cargo run --release --example multi_inputs
106fn main() {
107    let num_steps = 10;
108    let initial_state = vec![
109        Fr::from(1_u32),
110        Fr::from(1_u32),
111        Fr::from(1_u32),
112        Fr::from(1_u32),
113        Fr::from(1_u32),
114    ];
115
116    let F_circuit = MultiInputsFCircuit::<Fr>::new(());
117
118    println!("Prepare Nova ProverParams & VerifierParams");
119    let (prover_params, verifier_params) = test_nova_setup::<MultiInputsFCircuit<Fr>>(F_circuit);
120
121    /// The idea here is that eventually we could replace the next line chunk that defines the
122    /// `type NOVA = Nova<...>` by using another folding scheme that fulfills the `FoldingScheme`
123    /// trait, and the rest of our code would be working without needing to be updated.
124    type NOVA = Nova<
125        Projective,
126        GVar,
127        Projective2,
128        GVar2,
129        MultiInputsFCircuit<Fr>,
130        Pedersen<Projective>,
131        Pedersen<Projective2>,
132    >;
133
134    println!("Initialize FoldingScheme");
135    let mut folding_scheme = NOVA::init(&prover_params, F_circuit, initial_state.clone()).unwrap();
136
137    // compute a step of the IVC
138    for i in 0..num_steps {
139        let start = Instant::now();
140        folding_scheme.prove_step().unwrap();
141        println!("Nova::prove_step {}: {:?}", i, start.elapsed());
142    }
143
144    let (running_instance, incoming_instance, cyclefold_instance) = folding_scheme.instances();
145
146    println!("Run the Nova's IVC verifier");
147    NOVA::verify(
148        verifier_params,
149        initial_state.clone(),
150        folding_scheme.state(), // latest state
151        Fr::from(num_steps as u32),
152        running_instance,
153        incoming_instance,
154        cyclefold_instance,
155    )
156    .unwrap();
157}