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