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