sonobe/src/folding/nova/ivc.rs
src/folding/nova/ivc.rsRaw
1use ark_crypto_primitives::sponge::{poseidon::PoseidonConfig, Absorb};
2use ark_ec::{CurveGroup, Group};
3use ark_ff::PrimeField;
4use ark_relations::r1cs::ConstraintSynthesizer;
5use ark_relations::r1cs::ConstraintSystem;
6use ark_std::rand::Rng;
7use ark_std::{One, Zero};
8use core::marker::PhantomData;
9
10use super::circuits::{AugmentedFCircuit, FCircuit};
11use super::{nifs::NIFS, traits::NovaR1CS, CommittedInstance, Witness};
12use crate::ccs::r1cs::R1CS;
13use crate::frontend::arkworks::{extract_r1cs, extract_z}; // TODO once Frontend trait is ready, use that
14use crate::pedersen::{Params as PedersenParams, Pedersen};
15use crate::Error;
16
17/// Implements the Incremental Verifiable Computation described in sections 1.2 and 5 of
18/// [Nova](https://eprint.iacr.org/2021/370.pdf)
19pub struct IVC<C1, C2, FC>
20where
21 C1: CurveGroup,
22 C2: CurveGroup,
23 FC: FCircuit<C1::ScalarField>,
24{
25 _c2: PhantomData<C2>,
26 r1cs: R1CS<C1::ScalarField>,
27 poseidon_config: PoseidonConfig<C1::ScalarField>,
28 pedersen_params: PedersenParams<C1>,
29 F: FC, // F circuit
30 i: C1::ScalarField,
31 z_0: Vec<C1::ScalarField>,
32 z_i: Vec<C1::ScalarField>,
33 w_i: Witness<C1>,
34 u_i: CommittedInstance<C1>,
35 W_i: Witness<C1>,
36 U_i: CommittedInstance<C1>,
37}
38
39impl<C1, C2, FC> IVC<C1, C2, FC>
40where
41 C1: CurveGroup,
42 C2: CurveGroup,
43 FC: FCircuit<C1::ScalarField>,
44 <C1 as CurveGroup>::BaseField: PrimeField,
45 <C1 as Group>::ScalarField: Absorb,
46{
47 /// Initializes the IVC for the given parameters and initial state `z_0`.
48 pub fn new<R: Rng>(
49 rng: &mut R,
50 poseidon_config: PoseidonConfig<C1::ScalarField>,
51 F: FC,
52 z_0: Vec<C1::ScalarField>,
53 ) -> Result<Self, Error> {
54 // prepare the circuit to obtain its R1CS
55 let cs = ConstraintSystem::<C1::ScalarField>::new_ref();
56
57 let augmented_F_circuit = AugmentedFCircuit::<C1, FC>::empty(&poseidon_config, F);
58
59 augmented_F_circuit.generate_constraints(cs.clone())?;
60 cs.finalize();
61 let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
62 let r1cs = extract_r1cs::<C1::ScalarField>(&cs);
63
64 let pedersen_params = Pedersen::<C1>::new_params(rng, r1cs.A.n_rows);
65
66 // setup the dummy instances
67 let (w_dummy, u_dummy) = r1cs.dummy_instance();
68
69 // W_i=W_0 is a 'dummy witness', all zeroes, but with the size corresponding to the R1CS that
70 // we're working with.
71 // Set U_i to be dummy instance
72 Ok(Self {
73 _c2: PhantomData,
74 r1cs,
75 poseidon_config,
76 pedersen_params,
77 F,
78 i: C1::ScalarField::zero(),
79 z_0: z_0.clone(),
80 z_i: z_0,
81 w_i: w_dummy.clone(),
82 u_i: u_dummy.clone(),
83 W_i: w_dummy,
84 U_i: u_dummy,
85 })
86 }
87
88 /// Implements IVC.P
89 pub fn prove_step(&mut self) -> Result<(), Error> {
90 let u_i1_x: C1::ScalarField;
91 let augmented_F_circuit: AugmentedFCircuit<C1, FC>;
92 let z_i1 = self.F.step_native(self.z_i.clone());
93
94 let (W_i1, U_i1, cmT): (Witness<C1>, CommittedInstance<C1>, C1);
95
96 if self.i == C1::ScalarField::zero() {
97 // base case: i=0, z_i=z_0, U_i = U_d := dummy instance
98 // u_1.x = H(1, z_0, z_i, U_i)
99 u_i1_x = self.U_i.hash(
100 &self.poseidon_config,
101 C1::ScalarField::one(),
102 self.z_0.clone(),
103 z_i1.clone(),
104 )?;
105
106 (W_i1, U_i1, cmT) = (self.w_i.clone(), self.u_i.clone(), C1::generator());
107
108 // base case
109 augmented_F_circuit = AugmentedFCircuit::<C1, FC> {
110 poseidon_config: self.poseidon_config.clone(),
111 i: Some(C1::ScalarField::zero()), // = i=0
112 z_0: Some(self.z_0.clone()), // = z_i
113 z_i: Some(self.z_i.clone()),
114 u_i: Some(self.u_i.clone()), // = dummy
115 U_i: Some(self.U_i.clone()), // = dummy
116 U_i1: Some(U_i1.clone()), // = dummy
117 cmT: Some(cmT),
118 F: self.F,
119 x: Some(u_i1_x),
120 };
121 } else {
122 let T: Vec<C1::ScalarField>;
123 (T, cmT) = NIFS::<C1>::compute_cmT(
124 &self.pedersen_params,
125 &self.r1cs,
126 &self.w_i,
127 &self.u_i,
128 &self.W_i,
129 &self.U_i,
130 )?;
131
132 let r_Fr = AugmentedFCircuit::<C1, FC>::get_challenge_native(
133 &self.poseidon_config,
134 self.u_i.clone(),
135 self.U_i.clone(),
136 cmT,
137 )?;
138
139 // compute W_{i+1} and U_{i+1}
140 (W_i1, U_i1) = NIFS::<C1>::fold_instances(
141 r_Fr, &self.w_i, &self.u_i, &self.W_i, &self.U_i, &T, cmT,
142 )?;
143
144 self.r1cs.check_relaxed_instance_relation(&W_i1, &U_i1)?;
145
146 // folded instance output (public input, x)
147 // u_{i+1}.x = H(i+1, z_0, z_{i+1}, U_{i+1})
148 u_i1_x = U_i1.hash(
149 &self.poseidon_config,
150 self.i + C1::ScalarField::one(),
151 self.z_0.clone(),
152 z_i1.clone(),
153 )?;
154
155 augmented_F_circuit = AugmentedFCircuit::<C1, FC> {
156 poseidon_config: self.poseidon_config.clone(),
157 i: Some(self.i),
158 z_0: Some(self.z_0.clone()),
159 z_i: Some(self.z_i.clone()),
160 u_i: Some(self.u_i.clone()),
161 U_i: Some(self.U_i.clone()),
162 U_i1: Some(U_i1.clone()),
163 cmT: Some(cmT),
164 F: self.F,
165 x: Some(u_i1_x),
166 };
167 }
168
169 let cs = ConstraintSystem::<C1::ScalarField>::new_ref();
170
171 augmented_F_circuit.generate_constraints(cs.clone())?;
172
173 let cs = cs.into_inner().ok_or(Error::NoInnerConstraintSystem)?;
174 // notice that here we use 'Z' (uppercase) to denote the 'z-vector' as in the paper, not
175 // the value 'z' (lowercase) which is the state
176 let Z_i1 = extract_z::<C1::ScalarField>(&cs);
177 let (w_i1, x_i1) = self.r1cs.split_z(&Z_i1);
178 assert_eq!(x_i1.len(), 1);
179 assert_eq!(x_i1[0], u_i1_x);
180
181 // compute committed instances, w_{i+1}, u_{i+1}, which will be used as w_i, u_i, so we
182 // assign them directly to w_i, u_i.
183 self.w_i = Witness::<C1>::new(w_i1.clone(), self.r1cs.A.n_rows);
184 self.u_i = self.w_i.commit(&self.pedersen_params, vec![u_i1_x])?;
185
186 // set values for next iteration
187 self.i += C1::ScalarField::one();
188 self.z_i = z_i1.clone();
189 self.U_i = U_i1.clone();
190 self.W_i = W_i1.clone();
191
192 Ok(())
193 }
194
195 /// Implements IVC.V
196 pub fn verify(&mut self, z_0: Vec<C1::ScalarField>, num_steps: u32) -> Result<(), Error> {
197 if self.i != C1::ScalarField::from(num_steps) {
198 return Err(Error::IVCVerificationFail);
199 }
200
201 if self.u_i.x.len() != 1 || self.U_i.x.len() != 1 {
202 return Err(Error::IVCVerificationFail);
203 }
204
205 // check that u_i's output points to the running instance
206 // u_i.X == H(i, z_0, z_i, U_i)
207 let expected_u_i_x = self
208 .U_i
209 .hash(&self.poseidon_config, self.i, z_0, self.z_i.clone())?;
210 if expected_u_i_x != self.u_i.x[0] {
211 return Err(Error::IVCVerificationFail);
212 }
213
214 // check u_i.cmE==0, u_i.u==1 (=u_i is a un-relaxed instance)
215 if self.u_i.cmE != C1::zero() || self.u_i.u != C1::ScalarField::one() {
216 return Err(Error::IVCVerificationFail);
217 }
218
219 // check R1CS satisfiability
220 self.r1cs.check_instance_relation(&self.w_i, &self.u_i)?;
221 // check RelaxedR1CS satisfiability
222 self.r1cs
223 .check_relaxed_instance_relation(&self.W_i, &self.U_i)?;
224
225 Ok(())
226 }
227}
228
229#[cfg(test)]
230mod tests {
231 use super::*;
232 use ark_pallas::{Fr, Projective};
233 use ark_vesta::Projective as Projective2;
234
235 use crate::folding::nova::circuits::tests::TestFCircuit;
236 use crate::transcript::poseidon::tests::poseidon_test_config;
237
238 #[test]
239 fn test_ivc() {
240 let mut rng = ark_std::test_rng();
241 let poseidon_config = poseidon_test_config::<Fr>();
242
243 let F_circuit = TestFCircuit::<Fr>::new();
244 let z_0 = vec![Fr::from(3_u32)];
245
246 let mut ivc = IVC::<Projective, Projective2, TestFCircuit<Fr>>::new(
247 &mut rng,
248 poseidon_config, // poseidon config
249 F_circuit,
250 z_0.clone(),
251 )
252 .unwrap();
253
254 let num_steps: usize = 3;
255 for _ in 0..num_steps {
256 ivc.prove_step().unwrap();
257 }
258
259 ivc.verify(z_0, num_steps as u32).unwrap();
260 }
261}