Nova/src/bellperson/mod.rs
src/bellperson/mod.rsRaw
1//! Support for generating R1CS from [Bellperson].
2//!
3//! [Bellperson]: https://github.com/filecoin-project/bellperson
4
5pub mod r1cs;
6pub mod shape_cs;
7pub mod solver;
8
9#[cfg(test)]
10mod tests {
11 use crate::bellperson::{
12 r1cs::{NovaShape, NovaWitness},
13 shape_cs::ShapeCS,
14 solver::SatisfyingAssignment,
15 };
16 use bellperson::{gadgets::num::AllocatedNum, ConstraintSystem, SynthesisError};
17 use bellperson_nonnative::{
18 mp::bignat::BigNat,
19 util::{convert::nat_to_f, num::Num},
20 };
21 use ff::PrimeField;
22 use num_bigint::BigInt;
23 use num_traits::Num as OtherNum;
24
25 fn synthesize_alloc_bit<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
26 cs: &mut CS,
27 ) -> Result<(), SynthesisError> {
28 // get two bits as input and check that they are indeed bits
29 let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?;
30 let _ = a.inputize(cs.namespace(|| "a is input"));
31 cs.enforce(
32 || "check a is 0 or 1",
33 |lc| lc + CS::one() - a.get_variable(),
34 |lc| lc + a.get_variable(),
35 |lc| lc,
36 );
37 let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?;
38 let _ = b.inputize(cs.namespace(|| "b is input"));
39 cs.enforce(
40 || "check b is 0 or 1",
41 |lc| lc + CS::one() - b.get_variable(),
42 |lc| lc + b.get_variable(),
43 |lc| lc,
44 );
45 Ok(())
46 }
47
48 #[test]
49 fn test_alloc_bit() {
50 type G = pasta_curves::pallas::Point;
51
52 // First create the shape
53 let mut cs: ShapeCS<G> = ShapeCS::new();
54 let _ = synthesize_alloc_bit(&mut cs);
55 let shape = cs.r1cs_shape();
56 let gens = cs.r1cs_gens();
57
58 // Now get the assignment
59 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
60 let _ = synthesize_alloc_bit(&mut cs);
61 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
62
63 // Make sure that this is satisfiable
64 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
65 }
66
67 fn synthesize_use_cs_one<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
68 cs: &mut CS,
69 ) -> Result<(), SynthesisError> {
70 let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?;
71 let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?;
72 cs.enforce(
73 || "check a = b",
74 |lc| lc + a.get_variable() - b.get_variable(),
75 |lc| lc + CS::one(),
76 |lc| lc,
77 );
78 let _ = a.inputize(cs.namespace(|| "a is input"));
79 let _ = b.inputize(cs.namespace(|| "b is input"));
80 Ok(())
81 }
82
83 fn synthesize_use_cs_one_after_inputize<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
84 cs: &mut CS,
85 ) -> Result<(), SynthesisError> {
86 let a = AllocatedNum::alloc(cs.namespace(|| "a"), || Ok(Fr::one()))?;
87 let b = AllocatedNum::alloc(cs.namespace(|| "b"), || Ok(Fr::one()))?;
88 let _ = a.inputize(cs.namespace(|| "a is input"));
89 cs.enforce(
90 || "check a = b",
91 |lc| lc + a.get_variable() - b.get_variable(),
92 |lc| lc + CS::one(),
93 |lc| lc,
94 );
95 let _ = b.inputize(cs.namespace(|| "b is input"));
96 Ok(())
97 }
98
99 #[test]
100 fn test_use_cs_one() {
101 type G = pasta_curves::pallas::Point;
102
103 // First create the shape
104 let mut cs: ShapeCS<G> = ShapeCS::new();
105 let _ = synthesize_use_cs_one(&mut cs);
106 let shape = cs.r1cs_shape();
107 let gens = cs.r1cs_gens();
108
109 // Now get the assignment
110 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
111 let _ = synthesize_use_cs_one(&mut cs);
112 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
113
114 // Make sure that this is satisfiable
115 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
116 }
117
118 #[test]
119 fn test_use_cs_one_after_inputize() {
120 type G = pasta_curves::pallas::Point;
121
122 // First create the shape
123 let mut cs: ShapeCS<G> = ShapeCS::new();
124 let _ = synthesize_use_cs_one_after_inputize(&mut cs);
125 let shape = cs.r1cs_shape();
126 let gens = cs.r1cs_gens();
127
128 // Now get the assignment
129 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
130 let _ = synthesize_use_cs_one_after_inputize(&mut cs);
131 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
132
133 // Make sure that this is satisfiable
134 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
135 }
136
137 fn synthesize_is_equal<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
138 cs: &mut CS,
139 a_val: &BigInt,
140 limb_width: usize,
141 n_limbs: usize,
142 ) -> Result<(), SynthesisError> {
143 let a1 = BigNat::alloc_from_nat(
144 cs.namespace(|| "alloc a2"),
145 || Ok(a_val.clone()),
146 limb_width,
147 n_limbs,
148 )?;
149 let _ = a1.inputize(cs.namespace(|| "make a input"));
150
151 let a_num = Num::alloc(cs.namespace(|| "alloc a num"), || {
152 Ok(nat_to_f(a_val).unwrap())
153 })?;
154 let a2 = BigNat::from_num(
155 cs.namespace(|| "allocate a1_limbs"),
156 a_num,
157 limb_width,
158 n_limbs,
159 )?;
160
161 a1.equal_when_carried(cs.namespace(|| "check equal"), &a2)?;
162 Ok(())
163 }
164
165 #[allow(clippy::too_many_arguments)]
166 fn synthesize_mult_mod<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
167 cs: &mut CS,
168 a_val: &BigInt,
169 b_val: &BigInt,
170 m_val: &BigInt,
171 q_val: &BigInt,
172 r_val: &BigInt,
173 limb_width: usize,
174 n_limbs: usize,
175 ) -> Result<(), SynthesisError> {
176 let a_num = Num::alloc(cs.namespace(|| "alloc a num"), || {
177 Ok(nat_to_f(a_val).unwrap())
178 })?;
179 let m = BigNat::alloc_from_nat(
180 cs.namespace(|| "m"),
181 || Ok(m_val.clone()),
182 limb_width,
183 n_limbs,
184 )?;
185 m.inputize(cs.namespace(|| "modulus m"))?;
186
187 let a = BigNat::from_num(
188 cs.namespace(|| "allocate a_limbs"),
189 a_num,
190 limb_width,
191 n_limbs,
192 )?;
193 let b = BigNat::alloc_from_nat(
194 cs.namespace(|| "b"),
195 || Ok(b_val.clone()),
196 limb_width,
197 n_limbs,
198 )?;
199 let q = BigNat::alloc_from_nat(
200 cs.namespace(|| "q"),
201 || Ok(q_val.clone()),
202 limb_width,
203 n_limbs,
204 )?;
205 let r = BigNat::alloc_from_nat(
206 cs.namespace(|| "r"),
207 || Ok(r_val.clone()),
208 limb_width,
209 n_limbs,
210 )?;
211 let (qa, ra) = a.mult_mod(cs.namespace(|| "prod"), &b, &m)?;
212 qa.equal(cs.namespace(|| "qcheck"), &q)?;
213 ra.equal(cs.namespace(|| "rcheck"), &r)?;
214 Ok(())
215 }
216
217 fn synthesize_add<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
218 cs: &mut CS,
219 a_val: &BigInt,
220 b_val: &BigInt,
221 c_val: &BigInt,
222 limb_width: usize,
223 n_limbs: usize,
224 ) -> Result<(), SynthesisError> {
225 let a = BigNat::alloc_from_nat(
226 cs.namespace(|| "a"),
227 || Ok(a_val.clone()),
228 limb_width,
229 n_limbs,
230 )?;
231 a.inputize(cs.namespace(|| "input a"))?;
232 let b = BigNat::alloc_from_nat(
233 cs.namespace(|| "b"),
234 || Ok(b_val.clone()),
235 limb_width,
236 n_limbs,
237 )?;
238 b.inputize(cs.namespace(|| "input b"))?;
239 let c = BigNat::alloc_from_nat(
240 cs.namespace(|| "c"),
241 || Ok(c_val.clone()),
242 limb_width,
243 n_limbs,
244 )?;
245 let ca = a.add::<CS>(&b)?;
246 ca.equal(cs.namespace(|| "ccheck"), &c)?;
247 Ok(())
248 }
249
250 fn synthesize_add_mod<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
251 cs: &mut CS,
252 a_val: &BigInt,
253 b_val: &BigInt,
254 c_val: &BigInt,
255 m_val: &BigInt,
256 limb_width: usize,
257 n_limbs: usize,
258 ) -> Result<(), SynthesisError> {
259 let a = BigNat::alloc_from_nat(
260 cs.namespace(|| "a"),
261 || Ok(a_val.clone()),
262 limb_width,
263 n_limbs,
264 )?;
265 a.inputize(cs.namespace(|| "input a"))?;
266 let b = BigNat::alloc_from_nat(
267 cs.namespace(|| "b"),
268 || Ok(b_val.clone()),
269 limb_width,
270 n_limbs,
271 )?;
272 b.inputize(cs.namespace(|| "input b"))?;
273 let c = BigNat::alloc_from_nat(
274 cs.namespace(|| "c"),
275 || Ok(c_val.clone()),
276 limb_width,
277 n_limbs,
278 )?;
279 let m = BigNat::alloc_from_nat(
280 cs.namespace(|| "m"),
281 || Ok(m_val.clone()),
282 limb_width,
283 n_limbs,
284 )?;
285 let d = a.add::<CS>(&b)?;
286 let ca = d.red_mod(cs.namespace(|| "reduce"), &m)?;
287 ca.equal(cs.namespace(|| "ccheck"), &c)?;
288 Ok(())
289 }
290
291 #[test]
292 fn test_mult_mod() {
293 type G = pasta_curves::pallas::Point;
294
295 // Set the inputs
296 let a_val = BigInt::from_str_radix(
297 "11572336752428856981970994795408771577024165681374400871001196932361466228192",
298 10,
299 )
300 .unwrap();
301 let b_val = BigInt::from_str_radix(
302 "87673389408848523602668121701204553693362841135953267897017930941776218798802",
303 10,
304 )
305 .unwrap();
306 let m_val = BigInt::from_str_radix(
307 "40000000000000000000000000000000224698fc094cf91b992d30ed00000001",
308 16,
309 )
310 .unwrap();
311 let q_val = BigInt::from_str_radix(
312 "35048542371029440058224000662033175648615707461806414787901284501179083518342",
313 10,
314 )
315 .unwrap();
316 let r_val = BigInt::from_str_radix(
317 "26362617993085418618858432307761590013874563896298265114483698919121453084730",
318 10,
319 )
320 .unwrap();
321
322 // First create the shape
323 let mut cs: ShapeCS<G> = ShapeCS::new();
324 let _ = synthesize_mult_mod(&mut cs, &a_val, &b_val, &m_val, &q_val, &r_val, 32, 8);
325 let shape = cs.r1cs_shape();
326 let gens = cs.r1cs_gens();
327 println!("Mult mod constraint no: {}", cs.num_constraints());
328
329 // Now get the assignment
330 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
331 let _ = synthesize_mult_mod(&mut cs, &a_val, &b_val, &m_val, &q_val, &r_val, 32, 8);
332 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
333
334 // Make sure that this is satisfiable
335 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
336 }
337
338 #[test]
339 fn test_add() {
340 type G = pasta_curves::pallas::Point;
341
342 // Set the inputs
343 let a_val = BigInt::from_str_radix(
344 "11572336752428856981970994795408771577024165681374400871001196932361466228192",
345 10,
346 )
347 .unwrap();
348 let b_val = BigInt::from_str_radix("1", 10).unwrap();
349 let c_val = BigInt::from_str_radix(
350 "11572336752428856981970994795408771577024165681374400871001196932361466228193",
351 10,
352 )
353 .unwrap();
354
355 // First create the shape
356 let mut cs: ShapeCS<G> = ShapeCS::new();
357 let _ = synthesize_add(&mut cs, &a_val, &b_val, &c_val, 32, 8);
358 let shape = cs.r1cs_shape();
359 let gens = cs.r1cs_gens();
360 println!("Add mod constraint no: {}", cs.num_constraints());
361
362 // Now get the assignment
363 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
364 let _ = synthesize_add(&mut cs, &a_val, &b_val, &c_val, 32, 8);
365 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
366
367 // Make sure that this is satisfiable
368 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
369 }
370
371 #[test]
372 fn test_add_mod() {
373 type G = pasta_curves::pallas::Point;
374
375 // Set the inputs
376 let a_val = BigInt::from_str_radix(
377 "11572336752428856981970994795408771577024165681374400871001196932361466228192",
378 10,
379 )
380 .unwrap();
381 let b_val = BigInt::from_str_radix("1", 10).unwrap();
382 let c_val = BigInt::from_str_radix(
383 "11572336752428856981970994795408771577024165681374400871001196932361466228193",
384 10,
385 )
386 .unwrap();
387 let m_val = BigInt::from_str_radix(
388 "40000000000000000000000000000000224698fc094cf91b992d30ed00000001",
389 16,
390 )
391 .unwrap();
392
393 // First create the shape
394 let mut cs: ShapeCS<G> = ShapeCS::new();
395 let _ = synthesize_add_mod(&mut cs, &a_val, &b_val, &c_val, &m_val, 32, 8);
396 let shape = cs.r1cs_shape();
397 let gens = cs.r1cs_gens();
398 println!("Add mod constraint no: {}", cs.num_constraints());
399
400 // Now get the assignment
401 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
402 let _ = synthesize_add_mod(&mut cs, &a_val, &b_val, &c_val, &m_val, 32, 8);
403 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
404
405 // Make sure that this is satisfiable
406 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
407 }
408
409 #[test]
410 fn test_equal() {
411 type G = pasta_curves::pallas::Point;
412
413 // Set the inputs
414 let a_val = BigInt::from_str_radix("1157233675242885698197099479540877", 10).unwrap();
415
416 // First create the shape
417 let mut cs: ShapeCS<G> = ShapeCS::new();
418 let _ = synthesize_is_equal(&mut cs, &a_val, 32, 8);
419 let shape = cs.r1cs_shape();
420 let gens = cs.r1cs_gens();
421 println!("Equal constraint no: {}", cs.num_constraints());
422
423 // Now get the assignment
424 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
425 let _ = synthesize_is_equal(&mut cs, &a_val, 32, 8);
426 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
427
428 // Make sure that this is satisfiable
429 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
430 }
431}