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