Nova/tests/nonnative.rs
tests/nonnative.rsRaw
1use bellperson::{ConstraintSystem, SynthesisError};
2use bellperson_nonnative::{
3 mp::bignat::BigNat,
4 util::{convert::nat_to_f, num::Num},
5};
6use ff::PrimeField;
7use nova_snark::bellperson::{
8 r1cs::{NovaShape, NovaWitness},
9 shape_cs::ShapeCS,
10 solver::SatisfyingAssignment,
11};
12use rug::Integer;
13
14fn synthesize_is_equal<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
15 cs: &mut CS,
16 a_val: &Integer,
17 limb_width: usize,
18 n_limbs: usize,
19) -> Result<(), SynthesisError> {
20 let a1 = BigNat::alloc_from_nat(
21 cs.namespace(|| "alloc a2"),
22 || Ok(a_val.clone()),
23 limb_width,
24 n_limbs,
25 )?;
26 let _ = a1.inputize(cs.namespace(|| "make a input"));
27
28 let a_num = Num::alloc(cs.namespace(|| "alloc a num"), || {
29 Ok(nat_to_f(a_val).unwrap())
30 })?;
31 let a2 = BigNat::from_num(
32 cs.namespace(|| "allocate a1_limbs"),
33 a_num,
34 limb_width,
35 n_limbs,
36 )?;
37
38 let _ = a1.equal_when_carried(cs.namespace(|| "check equal"), &a2)?;
39 Ok(())
40}
41
42#[allow(clippy::too_many_arguments)]
43fn synthesize_mult_mod<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
44 cs: &mut CS,
45 a_val: &Integer,
46 b_val: &Integer,
47 m_val: &Integer,
48 q_val: &Integer,
49 r_val: &Integer,
50 limb_width: usize,
51 n_limbs: usize,
52) -> Result<(), SynthesisError> {
53 let a_num = Num::alloc(cs.namespace(|| "alloc a num"), || {
54 Ok(nat_to_f(a_val).unwrap())
55 })?;
56 let m = BigNat::alloc_from_nat(
57 cs.namespace(|| "m"),
58 || Ok(m_val.clone()),
59 limb_width,
60 n_limbs,
61 )?;
62 let _ = m.inputize(cs.namespace(|| "modulus m"))?;
63
64 let a = BigNat::from_num(
65 cs.namespace(|| "allocate a_limbs"),
66 a_num,
67 limb_width,
68 n_limbs,
69 )?;
70 let b = BigNat::alloc_from_nat(
71 cs.namespace(|| "b"),
72 || Ok(b_val.clone()),
73 limb_width,
74 n_limbs,
75 )?;
76 let q = BigNat::alloc_from_nat(
77 cs.namespace(|| "q"),
78 || Ok(q_val.clone()),
79 limb_width,
80 n_limbs,
81 )?;
82 let r = BigNat::alloc_from_nat(
83 cs.namespace(|| "r"),
84 || Ok(r_val.clone()),
85 limb_width,
86 n_limbs,
87 )?;
88 let (qa, ra) = a.mult_mod(cs.namespace(|| "prod"), &b, &m)?;
89 qa.equal(cs.namespace(|| "qcheck"), &q)?;
90 ra.equal(cs.namespace(|| "rcheck"), &r)?;
91 Ok(())
92}
93
94fn synthesize_add<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
95 cs: &mut CS,
96 a_val: &Integer,
97 b_val: &Integer,
98 c_val: &Integer,
99 limb_width: usize,
100 n_limbs: usize,
101) -> Result<(), SynthesisError> {
102 let a = BigNat::alloc_from_nat(
103 cs.namespace(|| "a"),
104 || Ok(a_val.clone()),
105 limb_width,
106 n_limbs,
107 )?;
108 let _ = a.inputize(cs.namespace(|| "input a"))?;
109 let b = BigNat::alloc_from_nat(
110 cs.namespace(|| "b"),
111 || Ok(b_val.clone()),
112 limb_width,
113 n_limbs,
114 )?;
115 let _ = b.inputize(cs.namespace(|| "input b"))?;
116 let c = BigNat::alloc_from_nat(
117 cs.namespace(|| "c"),
118 || Ok(c_val.clone()),
119 limb_width,
120 n_limbs,
121 )?;
122 let ca = a.add::<CS>(&b)?;
123 ca.equal(cs.namespace(|| "ccheck"), &c)?;
124 Ok(())
125}
126
127fn synthesize_add_mod<Fr: PrimeField, CS: ConstraintSystem<Fr>>(
128 cs: &mut CS,
129 a_val: &Integer,
130 b_val: &Integer,
131 c_val: &Integer,
132 m_val: &Integer,
133 limb_width: usize,
134 n_limbs: usize,
135) -> Result<(), SynthesisError> {
136 let a = BigNat::alloc_from_nat(
137 cs.namespace(|| "a"),
138 || Ok(a_val.clone()),
139 limb_width,
140 n_limbs,
141 )?;
142 let _ = a.inputize(cs.namespace(|| "input a"))?;
143 let b = BigNat::alloc_from_nat(
144 cs.namespace(|| "b"),
145 || Ok(b_val.clone()),
146 limb_width,
147 n_limbs,
148 )?;
149 let _ = b.inputize(cs.namespace(|| "input b"))?;
150 let c = BigNat::alloc_from_nat(
151 cs.namespace(|| "c"),
152 || Ok(c_val.clone()),
153 limb_width,
154 n_limbs,
155 )?;
156 let m = BigNat::alloc_from_nat(
157 cs.namespace(|| "m"),
158 || Ok(m_val.clone()),
159 limb_width,
160 n_limbs,
161 )?;
162 let d = a.add::<CS>(&b)?;
163 let ca = d.red_mod(cs.namespace(|| "reduce"), &m)?;
164 ca.equal(cs.namespace(|| "ccheck"), &c)?;
165 Ok(())
166}
167
168#[test]
169fn test_mult_mod() {
170 type G = pasta_curves::pallas::Point;
171
172 //Set the inputs
173 let a_val = Integer::from_str_radix(
174 "11572336752428856981970994795408771577024165681374400871001196932361466228192",
175 10,
176 )
177 .unwrap();
178 let b_val = Integer::from_str_radix(
179 "87673389408848523602668121701204553693362841135953267897017930941776218798802",
180 10,
181 )
182 .unwrap();
183 let m_val = Integer::from_str_radix(
184 "40000000000000000000000000000000224698fc094cf91b992d30ed00000001",
185 16,
186 )
187 .unwrap();
188 let q_val = Integer::from_str_radix(
189 "35048542371029440058224000662033175648615707461806414787901284501179083518342",
190 10,
191 )
192 .unwrap();
193 let r_val = Integer::from_str_radix(
194 "26362617993085418618858432307761590013874563896298265114483698919121453084730",
195 10,
196 )
197 .unwrap();
198
199 //First create the shape
200 let mut cs: ShapeCS<G> = ShapeCS::new();
201 let _ = synthesize_mult_mod(&mut cs, &a_val, &b_val, &m_val, &q_val, &r_val, 32, 8);
202 let shape = cs.r1cs_shape();
203 let gens = cs.r1cs_gens();
204 println!("Mult mod constraint no: {}", cs.num_constraints());
205
206 //Now get the assignment
207 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
208 let _ = synthesize_mult_mod(&mut cs, &a_val, &b_val, &m_val, &q_val, &r_val, 32, 8);
209 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
210
211 //Make sure that this is satisfiable
212 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
213}
214
215#[test]
216fn test_add() {
217 type G = pasta_curves::pallas::Point;
218
219 //Set the inputs
220 let a_val = Integer::from_str_radix(
221 "11572336752428856981970994795408771577024165681374400871001196932361466228192",
222 10,
223 )
224 .unwrap();
225 let b_val = Integer::from_str_radix("1", 10).unwrap();
226 let c_val = Integer::from_str_radix(
227 "11572336752428856981970994795408771577024165681374400871001196932361466228193",
228 10,
229 )
230 .unwrap();
231
232 //First create the shape
233 let mut cs: ShapeCS<G> = ShapeCS::new();
234 let _ = synthesize_add(&mut cs, &a_val, &b_val, &c_val, 32, 8);
235 let shape = cs.r1cs_shape();
236 let gens = cs.r1cs_gens();
237 println!("Add mod constraint no: {}", cs.num_constraints());
238
239 //Now get the assignment
240 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
241 let _ = synthesize_add(&mut cs, &a_val, &b_val, &c_val, 32, 8);
242 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
243
244 //Make sure that this is satisfiable
245 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
246}
247
248#[test]
249fn test_add_mod() {
250 type G = pasta_curves::pallas::Point;
251
252 //Set the inputs
253 let a_val = Integer::from_str_radix(
254 "11572336752428856981970994795408771577024165681374400871001196932361466228192",
255 10,
256 )
257 .unwrap();
258 let b_val = Integer::from_str_radix("1", 10).unwrap();
259 let c_val = Integer::from_str_radix(
260 "11572336752428856981970994795408771577024165681374400871001196932361466228193",
261 10,
262 )
263 .unwrap();
264 let m_val = Integer::from_str_radix(
265 "40000000000000000000000000000000224698fc094cf91b992d30ed00000001",
266 16,
267 )
268 .unwrap();
269
270 //First create the shape
271 let mut cs: ShapeCS<G> = ShapeCS::new();
272 let _ = synthesize_add_mod(&mut cs, &a_val, &b_val, &c_val, &m_val, 32, 8);
273 let shape = cs.r1cs_shape();
274 let gens = cs.r1cs_gens();
275 println!("Add mod constraint no: {}", cs.num_constraints());
276
277 //Now get the assignment
278 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
279 let _ = synthesize_add_mod(&mut cs, &a_val, &b_val, &c_val, &m_val, 32, 8);
280 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
281
282 //Make sure that this is satisfiable
283 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
284}
285
286#[test]
287fn test_equal() {
288 type G = pasta_curves::pallas::Point;
289
290 //Set the inputs
291 let a_val = Integer::from_str_radix("1157233675242885698197099479540877", 10).unwrap();
292
293 //First create the shape
294 let mut cs: ShapeCS<G> = ShapeCS::new();
295 let _ = synthesize_is_equal(&mut cs, &a_val, 32, 8);
296 let shape = cs.r1cs_shape();
297 let gens = cs.r1cs_gens();
298 println!("Equal constraint no: {}", cs.num_constraints());
299
300 //Now get the assignment
301 let mut cs: SatisfyingAssignment<G> = SatisfyingAssignment::new();
302 let _ = synthesize_is_equal(&mut cs, &a_val, 32, 8);
303 let (inst, witness) = cs.r1cs_instance_and_witness(&shape, &gens).unwrap();
304
305 //Make sure that this is satisfiable
306 assert!(shape.is_sat(&gens, &inst, &witness).is_ok());
307}