Nova/src/nifs.rs
src/nifs.rsRaw
1//! This module implements a non-interactive folding scheme
2#![allow(non_snake_case)]
3#![allow(clippy::type_complexity)]
4
5use super::{
6 commitments::CompressedCommitment,
7 constants::{NUM_CHALLENGE_BITS, NUM_FE_FOR_RO},
8 errors::NovaError,
9 r1cs::{R1CSGens, R1CSInstance, R1CSShape, R1CSWitness, RelaxedR1CSInstance, RelaxedR1CSWitness},
10 traits::{AbsorbInROTrait, Group, ROTrait},
11};
12use core::marker::PhantomData;
13
14/// A SNARK that holds the proof of a step of an incremental computation
15#[allow(clippy::upper_case_acronyms)]
16#[derive(Clone, Debug)]
17pub struct NIFS<G: Group> {
18 pub(crate) comm_T: CompressedCommitment<G::CompressedGroupElement>,
19 _p: PhantomData<G>,
20}
21
22type ROConstants<G> =
23 <<G as Group>::RO as ROTrait<<G as Group>::Base, <G as Group>::Scalar>>::Constants;
24
25impl<G: Group> NIFS<G> {
26 /// Takes as input a Relaxed R1CS instance-witness tuple `(U1, W1)` and
27 /// an R1CS instance-witness tuple `(U2, W2)` with the same structure `shape`
28 /// and defined with respect to the same `gens`, and outputs
29 /// a folded Relaxed R1CS instance-witness tuple `(U, W)` of the same shape `shape`,
30 /// with the guarantee that the folded witness `W` satisfies the folded instance `U`
31 /// if and only if `W1` satisfies `U1` and `W2` satisfies `U2`.
32 pub fn prove(
33 gens: &R1CSGens<G>,
34 ro_consts: &ROConstants<G>,
35 S: &R1CSShape<G>,
36 U1: &RelaxedR1CSInstance<G>,
37 W1: &RelaxedR1CSWitness<G>,
38 U2: &R1CSInstance<G>,
39 W2: &R1CSWitness<G>,
40 ) -> Result<(NIFS<G>, (RelaxedR1CSInstance<G>, RelaxedR1CSWitness<G>)), NovaError> {
41 // initialize a new RO
42 let mut ro = G::RO::new(ro_consts.clone(), NUM_FE_FOR_RO);
43
44 // append S to the transcript
45 S.absorb_in_ro(&mut ro);
46
47 // append U1 and U2 to transcript
48 U1.absorb_in_ro(&mut ro);
49 U2.absorb_in_ro(&mut ro);
50
51 // compute a commitment to the cross-term
52 let (T, comm_T) = S.commit_T(gens, U1, W1, U2, W2)?;
53
54 // append `comm_T` to the transcript and obtain a challenge
55 comm_T.absorb_in_ro(&mut ro);
56
57 // compute a challenge from the RO
58 let r = ro.squeeze(NUM_CHALLENGE_BITS);
59
60 // fold the instance using `r` and `comm_T`
61 let U = U1.fold(U2, &comm_T, &r)?;
62
63 // fold the witness using `r` and `T`
64 let W = W1.fold(W2, &T, &r)?;
65
66 // return the folded instance and witness
67 Ok((
68 Self {
69 comm_T: comm_T.compress(),
70 _p: Default::default(),
71 },
72 (U, W),
73 ))
74 }
75
76 /// Takes as input a relaxed R1CS instance `U1` and and R1CS instance `U2`
77 /// with the same shape and defined with respect to the same parameters,
78 /// and outputs a folded instance `U` with the same shape,
79 /// with the guarantee that the folded instance `U`
80 /// if and only if `U1` and `U2` are satisfiable.
81 pub fn verify(
82 &self,
83 ro_consts: &ROConstants<G>,
84 S: &R1CSShape<G>,
85 U1: &RelaxedR1CSInstance<G>,
86 U2: &R1CSInstance<G>,
87 ) -> Result<RelaxedR1CSInstance<G>, NovaError> {
88 // initialize a new RO
89 let mut ro = G::RO::new(ro_consts.clone(), NUM_FE_FOR_RO);
90
91 // append S to the transcript
92 S.absorb_in_ro(&mut ro);
93
94 // append U1 and U2 to transcript
95 U1.absorb_in_ro(&mut ro);
96 U2.absorb_in_ro(&mut ro);
97
98 // append `comm_T` to the transcript and obtain a challenge
99 let comm_T = self.comm_T.decompress()?;
100 comm_T.absorb_in_ro(&mut ro);
101
102 // compute a challenge from the RO
103 let r = ro.squeeze(NUM_CHALLENGE_BITS);
104
105 // fold the instance using `r` and `comm_T`
106 let U = U1.fold(U2, &comm_T, &r)?;
107
108 // return the folded instance
109 Ok(U)
110 }
111}
112
113#[cfg(test)]
114mod tests {
115 use super::*;
116 use crate::traits::{Group, ROConstantsTrait};
117 use ::bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
118 use ff::{Field, PrimeField};
119 use rand::rngs::OsRng;
120
121 type S = pasta_curves::pallas::Scalar;
122 type G = pasta_curves::pallas::Point;
123
124 fn synthesize_tiny_r1cs_bellperson<Scalar: PrimeField, CS: ConstraintSystem<Scalar>>(
125 cs: &mut CS,
126 x_val: Option<Scalar>,
127 ) -> Result<(), SynthesisError> {
128 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
129 let x = AllocatedNum::alloc(cs.namespace(|| "x"), || Ok(x_val.unwrap()))?;
130 let _ = x.inputize(cs.namespace(|| "x is input"));
131
132 let x_sq = x.square(cs.namespace(|| "x_sq"))?;
133 let x_cu = x_sq.mul(cs.namespace(|| "x_cu"), &x)?;
134 let y = AllocatedNum::alloc(cs.namespace(|| "y"), || {
135 Ok(x_cu.get_value().unwrap() + x.get_value().unwrap() + Scalar::from(5u64))
136 })?;
137 let _ = y.inputize(cs.namespace(|| "y is output"));
138
139 cs.enforce(
140 || "y = x^3 + x + 5",
141 |lc| {
142 lc + x_cu.get_variable()
143 + x.get_variable()
144 + CS::one()
145 + CS::one()
146 + CS::one()
147 + CS::one()
148 + CS::one()
149 },
150 |lc| lc + CS::one(),
151 |lc| lc + y.get_variable(),
152 );
153
154 Ok(())
155 }
156
157 #[test]
158 fn test_tiny_r1cs_bellperson() {
159 use crate::bellperson::{
160 r1cs::{NovaShape, NovaWitness},
161 shape_cs::ShapeCS,
162 solver::SatisfyingAssignment,
163 };
164
165 // First create the shape
166 let mut cs: ShapeCS<G> = ShapeCS::new();
167 let _ = synthesize_tiny_r1cs_bellperson(&mut cs, None);
168 let shape = cs.r1cs_shape();
169 let gens = cs.r1cs_gens();
170 let ro_consts =
171 <<G as Group>::RO as ROTrait<<G as Group>::Base, <G as Group>::Scalar>>::Constants::new();
172
173 // Now get the instance and assignment for one instance
174 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
175 let _ = synthesize_tiny_r1cs_bellperson(&mut cs, Some(S::from(5)));
176 let (U1, W1) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
177
178 // Make sure that the first instance is satisfiable
179 assert!(shape.is_sat(&gens, &U1, &W1).is_ok());
180
181 // Now get the instance and assignment for second instance
182 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
183 let _ = synthesize_tiny_r1cs_bellperson(&mut cs, Some(S::from(135)));
184 let (U2, W2) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
185
186 // Make sure that the second instance is satisfiable
187 assert!(shape.is_sat(&gens, &U2, &W2).is_ok());
188
189 // execute a sequence of folds
190 execute_sequence(&gens, &ro_consts, &shape, &U1, &W1, &U2, &W2);
191 }
192
193 fn execute_sequence(
194 gens: &R1CSGens<G>,
195 ro_consts: &<<G as Group>::RO as ROTrait<<G as Group>::Base, <G as Group>::Scalar>>::Constants,
196 shape: &R1CSShape<G>,
197 U1: &R1CSInstance<G>,
198 W1: &R1CSWitness<G>,
199 U2: &R1CSInstance<G>,
200 W2: &R1CSWitness<G>,
201 ) {
202 // produce a default running instance
203 let mut r_W = RelaxedR1CSWitness::default(shape);
204 let mut r_U = RelaxedR1CSInstance::default(gens, shape);
205
206 // produce a step SNARK with (W1, U1) as the first incoming witness-instance pair
207 let res = NIFS::prove(gens, ro_consts, shape, &r_U, &r_W, U1, W1);
208 assert!(res.is_ok());
209 let (nifs, (_U, W)) = res.unwrap();
210
211 // verify the step SNARK with U1 as the first incoming instance
212 let res = nifs.verify(ro_consts, shape, &r_U, U1);
213 assert!(res.is_ok());
214 let U = res.unwrap();
215
216 assert_eq!(U, _U);
217
218 // update the running witness and instance
219 r_W = W;
220 r_U = U;
221
222 // produce a step SNARK with (W2, U2) as the second incoming witness-instance pair
223 let res = NIFS::prove(gens, ro_consts, shape, &r_U, &r_W, U2, W2);
224 assert!(res.is_ok());
225 let (nifs, (_U, W)) = res.unwrap();
226
227 // verify the step SNARK with U1 as the first incoming instance
228 let res = nifs.verify(ro_consts, shape, &r_U, U2);
229 assert!(res.is_ok());
230 let U = res.unwrap();
231
232 assert_eq!(U, _U);
233
234 // update the running witness and instance
235 r_W = W;
236 r_U = U;
237
238 // check if the running instance is satisfiable
239 assert!(shape.is_sat_relaxed(gens, &r_U, &r_W).is_ok());
240 }
241
242 #[test]
243 fn test_tiny_r1cs() {
244 let one = S::one();
245 let (num_cons, num_vars, num_io, A, B, C) = {
246 let num_cons = 4;
247 let num_vars = 4;
248 let num_io = 2;
249
250 // Consider a cubic equation: `x^3 + x + 5 = y`, where `x` and `y` are respectively the input and output.
251 // The R1CS for this problem consists of the following constraints:
252 // `I0 * I0 - Z0 = 0`
253 // `Z0 * I0 - Z1 = 0`
254 // `(Z1 + I0) * 1 - Z2 = 0`
255 // `(Z2 + 5) * 1 - I1 = 0`
256
257 // Relaxed R1CS is a set of three sparse matrices (A B C), where there is a row for every
258 // constraint and a column for every entry in z = (vars, u, inputs)
259 // An R1CS instance is satisfiable iff:
260 // Az \circ Bz = u \cdot Cz + E, where z = (vars, 1, inputs)
261 let mut A: Vec<(usize, usize, S)> = Vec::new();
262 let mut B: Vec<(usize, usize, S)> = Vec::new();
263 let mut C: Vec<(usize, usize, S)> = Vec::new();
264
265 // constraint 0 entries in (A,B,C)
266 // `I0 * I0 - Z0 = 0`
267 A.push((0, num_vars + 1, one));
268 B.push((0, num_vars + 1, one));
269 C.push((0, 0, one));
270
271 // constraint 1 entries in (A,B,C)
272 // `Z0 * I0 - Z1 = 0`
273 A.push((1, 0, one));
274 B.push((1, num_vars + 1, one));
275 C.push((1, 1, one));
276
277 // constraint 2 entries in (A,B,C)
278 // `(Z1 + I0) * 1 - Z2 = 0`
279 A.push((2, 1, one));
280 A.push((2, num_vars + 1, one));
281 B.push((2, num_vars, one));
282 C.push((2, 2, one));
283
284 // constraint 3 entries in (A,B,C)
285 // `(Z2 + 5) * 1 - I1 = 0`
286 A.push((3, 2, one));
287 A.push((3, num_vars, one + one + one + one + one));
288 B.push((3, num_vars, one));
289 C.push((3, num_vars + 2, one));
290
291 (num_cons, num_vars, num_io, A, B, C)
292 };
293
294 // create a shape object
295 let S = {
296 let res = R1CSShape::new(num_cons, num_vars, num_io, &A, &B, &C);
297 assert!(res.is_ok());
298 res.unwrap()
299 };
300
301 // generate generators and ro constants
302 let gens = R1CSGens::new(num_cons, num_vars);
303 let ro_consts =
304 <<G as Group>::RO as ROTrait<<G as Group>::Base, <G as Group>::Scalar>>::Constants::new();
305
306 let rand_inst_witness_generator =
307 |gens: &R1CSGens<G>, I: &S| -> (S, R1CSInstance<G>, R1CSWitness<G>) {
308 let i0 = *I;
309
310 // compute a satisfying (vars, X) tuple
311 let (O, vars, X) = {
312 let z0 = i0 * i0; // constraint 0
313 let z1 = i0 * z0; // constraint 1
314 let z2 = z1 + i0; // constraint 2
315 let i1 = z2 + one + one + one + one + one; // constraint 3
316
317 // store the witness and IO for the instance
318 let W = vec![z0, z1, z2, S::zero()];
319 let X = vec![i0, i1];
320 (i1, W, X)
321 };
322
323 let W = {
324 let res = R1CSWitness::new(&S, &vars);
325 assert!(res.is_ok());
326 res.unwrap()
327 };
328 let U = {
329 let comm_W = W.commit(gens);
330 let res = R1CSInstance::new(&S, &comm_W, &X);
331 assert!(res.is_ok());
332 res.unwrap()
333 };
334
335 // check that generated instance is satisfiable
336 assert!(S.is_sat(gens, &U, &W).is_ok());
337
338 (O, U, W)
339 };
340
341 let mut csprng: OsRng = OsRng;
342 let I = S::random(&mut csprng); // the first input is picked randomly for the first instance
343 let (O, U1, W1) = rand_inst_witness_generator(&gens, &I);
344 let (_O, U2, W2) = rand_inst_witness_generator(&gens, &O);
345
346 // execute a sequence of folds
347 execute_sequence(&gens, &ro_consts, &S, &U1, &W1, &U2, &W2);
348 }
349}