sonobe/examples/external_inputs.rs
examples/external_inputs.rsRaw
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_crypto_primitives::{
7 crh::{
8 poseidon::constraints::{CRHGadget, CRHParametersVar},
9 poseidon::CRH,
10 CRHScheme, CRHSchemeGadget,
11 },
12 sponge::{poseidon::PoseidonConfig, Absorb},
13};
14use ark_ff::PrimeField;
15use ark_pallas::{constraints::GVar, Fr, Projective};
16use ark_r1cs_std::fields::fp::FpVar;
17use ark_r1cs_std::{alloc::AllocVar, fields::FieldVar};
18use ark_relations::r1cs::{ConstraintSystemRef, SynthesisError};
19use ark_std::Zero;
20use ark_vesta::{constraints::GVar as GVar2, Projective as Projective2};
21use core::marker::PhantomData;
22use std::time::Instant;
23
24use folding_schemes::commitment::pedersen::Pedersen;
25use folding_schemes::folding::nova::Nova;
26use folding_schemes::frontend::FCircuit;
27use folding_schemes::{Error, FoldingScheme};
28mod utils;
29use folding_schemes::transcript::poseidon::poseidon_test_config;
30use utils::test_nova_setup;
31
32/// This is the circuit that we want to fold, it implements the FCircuit trait. The parameter z_i
33/// denotes the current state which contains 2 elements, and z_{i+1} denotes the next state which
34/// we get by applying the step.
35///
36/// In this example we set the state to be the previous state together with an external input, and
37/// the new state is an array which contains the new state and a zero which will be ignored.
38///
39/// This is useful for example if we want to fold multiple verifications of signatures, where the
40/// circuit F checks the signature and is folded for each of the signatures and public keys. To
41/// keep things simpler, the following example does not verify signatures but does a similar
42/// approach with a chain of hashes, where each iteration hashes the previous step output (z_i)
43/// together with an external input (w_i).
44///
45/// w_1 w_2 w_3 w_4
46/// │ │ │ │
47/// ▼ ▼ ▼ ▼
48/// ┌─┐ ┌─┐ ┌─┐ ┌─┐
49/// ─────►│F├────►│F├────►│F├────►│F├────►
50/// z_1 └─┘ z_2 └─┘ z_3 └─┘ z_4 └─┘ z_5
51///
52///
53/// where each F is:
54/// w_i
55/// │ ┌────────────────────┐
56/// │ │FCircuit │
57/// │ │ │
58/// └────►│ h =Hash(z_i[0],w_i)│
59/// │ │ =Hash(v, w_i) │
60/// ────────►│ │ ├───────►
61/// z_i=[v,0] │ └──►z_{i+1}=[h, 0] │ z_{i+1}=[h,0]
62/// │ │
63/// └────────────────────┘
64///
65/// where each w_i value is set at the external_inputs array.
66///
67/// The last state z_i is used together with the external input w_i as inputs to compute the new
68/// state z_{i+1}.
69/// The function F will output the new state in an array of two elements, where the second element
70/// is a 0. In other words, z_{i+1} = [F([z_i, w_i]), 0], and the 0 will be replaced by w_{i+1} in
71/// the next iteration, so z_{i+2} = [F([z_{i+1}, w_{i+1}]), 0].
72#[derive(Clone, Debug)]
73pub struct ExternalInputsCircuits<F: PrimeField>
74where
75 F: Absorb,
76{
77 _f: PhantomData<F>,
78 poseidon_config: PoseidonConfig<F>,
79 external_inputs: Vec<F>,
80}
81impl<F: PrimeField> FCircuit<F> for ExternalInputsCircuits<F>
82where
83 F: Absorb,
84{
85 type Params = (PoseidonConfig<F>, Vec<F>); // where Vec<F> contains the external inputs
86
87 fn new(params: Self::Params) -> Self {
88 Self {
89 _f: PhantomData,
90 poseidon_config: params.0,
91 external_inputs: params.1,
92 }
93 }
94 fn state_len(&self) -> usize {
95 2
96 }
97
98 /// computes the next state values in place, assigning z_{i+1} into z_i, and computing the new
99 /// z_{i+1}
100 fn step_native(&self, i: usize, z_i: Vec<F>) -> Result<Vec<F>, Error> {
101 let input: [F; 2] = [z_i[0], self.external_inputs[i]];
102 let h = CRH::<F>::evaluate(&self.poseidon_config, input).unwrap();
103 Ok(vec![h, F::zero()])
104 }
105
106 /// generates the constraints for the step of F for the given z_i
107 fn generate_step_constraints(
108 &self,
109 cs: ConstraintSystemRef<F>,
110 i: usize,
111 z_i: Vec<FpVar<F>>,
112 ) -> Result<Vec<FpVar<F>>, SynthesisError> {
113 let crh_params =
114 CRHParametersVar::<F>::new_constant(cs.clone(), self.poseidon_config.clone())?;
115 let external_inputVar =
116 FpVar::<F>::new_witness(cs.clone(), || Ok(self.external_inputs[i])).unwrap();
117 let input: [FpVar<F>; 2] = [z_i[0].clone(), external_inputVar.clone()];
118 let h = CRHGadget::<F>::evaluate(&crh_params, &input)?;
119 Ok(vec![h, FpVar::<F>::zero()])
120 }
121}
122
123/// cargo test --example external_inputs
124#[cfg(test)]
125pub mod tests {
126 use super::*;
127 use ark_r1cs_std::R1CSVar;
128 use ark_relations::r1cs::ConstraintSystem;
129
130 // test to check that the ExternalInputsCircuits computes the same values inside and outside the circuit
131 #[test]
132 fn test_f_circuit() {
133 let poseidon_config = poseidon_test_config::<Fr>();
134
135 let cs = ConstraintSystem::<Fr>::new_ref();
136
137 let circuit = ExternalInputsCircuits::<Fr>::new((poseidon_config, vec![Fr::from(3_u32)]));
138 let z_i = vec![Fr::from(1_u32), Fr::zero()];
139
140 let z_i1 = circuit.step_native(0, z_i.clone()).unwrap();
141
142 let z_iVar = Vec::<FpVar<Fr>>::new_witness(cs.clone(), || Ok(z_i)).unwrap();
143 let computed_z_i1Var = circuit
144 .generate_step_constraints(cs.clone(), 0, z_iVar.clone())
145 .unwrap();
146 assert_eq!(computed_z_i1Var.value().unwrap(), z_i1);
147 }
148}
149
150/// cargo run --release --example external_inputs
151fn main() {
152 let num_steps = 5;
153 let initial_state = vec![Fr::from(1_u32), Fr::zero()];
154
155 // set the external inputs to be used at each folding step
156 let external_inputs = vec![
157 Fr::from(3_u32),
158 Fr::from(33_u32),
159 Fr::from(73_u32),
160 Fr::from(103_u32),
161 Fr::from(125_u32),
162 ];
163 assert_eq!(external_inputs.len(), num_steps);
164
165 let poseidon_config = poseidon_test_config::<Fr>();
166 let F_circuit = ExternalInputsCircuits::<Fr>::new((poseidon_config, external_inputs));
167
168 println!("Prepare Nova ProverParams & VerifierParams");
169 let (prover_params, verifier_params) =
170 test_nova_setup::<ExternalInputsCircuits<Fr>>(F_circuit.clone());
171
172 /// The idea here is that eventually we could replace the next line chunk that defines the
173 /// `type NOVA = Nova<...>` by using another folding scheme that fulfills the `FoldingScheme`
174 /// trait, and the rest of our code would be working without needing to be updated.
175 type NOVA = Nova<
176 Projective,
177 GVar,
178 Projective2,
179 GVar2,
180 ExternalInputsCircuits<Fr>,
181 Pedersen<Projective>,
182 Pedersen<Projective2>,
183 >;
184
185 println!("Initialize FoldingScheme");
186 let mut folding_scheme = NOVA::init(&prover_params, F_circuit, initial_state.clone()).unwrap();
187
188 // compute a step of the IVC
189 for i in 0..num_steps {
190 let start = Instant::now();
191 folding_scheme.prove_step().unwrap();
192 println!("Nova::prove_step {}: {:?}", i, start.elapsed());
193 }
194 println!(
195 "state at last step (after {} iterations): {:?}",
196 num_steps,
197 folding_scheme.state()
198 );
199
200 let (running_instance, incoming_instance, cyclefold_instance) = folding_scheme.instances();
201
202 println!("Run the Nova's IVC verifier");
203 NOVA::verify(
204 verifier_params,
205 initial_state.clone(),
206 folding_scheme.state(), // latest state
207 Fr::from(num_steps as u32),
208 running_instance,
209 incoming_instance,
210 cyclefold_instance,
211 )
212 .unwrap();
213}