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