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