Nova/src/gadgets/utils.rs
src/gadgets/utils.rsRaw
1//! This module implements various low-level gadgets
2use super::nonnative::bignat::{nat_to_limbs, BigNat};
3use crate::traits::Group;
4use bellperson::{
5 gadgets::{
6 boolean::{AllocatedBit, Boolean},
7 num::AllocatedNum,
8 Assignment,
9 },
10 ConstraintSystem, LinearCombination, SynthesisError,
11};
12use ff::{Field, PrimeField, PrimeFieldBits};
13use num_bigint::BigInt;
14
15/// Gets as input the little indian representation of a number and spits out the number
16pub fn le_bits_to_num<Scalar, CS>(
17 mut cs: CS,
18 bits: &[AllocatedBit],
19) -> Result<AllocatedNum<Scalar>, SynthesisError>
20where
21 Scalar: PrimeField + PrimeFieldBits,
22 CS: ConstraintSystem<Scalar>,
23{
24 // We loop over the input bits and construct the constraint
25 // and the field element that corresponds to the result
26 let mut lc = LinearCombination::zero();
27 let mut coeff = Scalar::ONE;
28 let mut fe = Some(Scalar::ZERO);
29 for bit in bits.iter() {
30 lc = lc + (coeff, bit.get_variable());
31 fe = bit.get_value().map(|val| {
32 if val {
33 fe.unwrap() + coeff
34 } else {
35 fe.unwrap()
36 }
37 });
38 coeff = coeff.double();
39 }
40 let num = AllocatedNum::alloc(cs.namespace(|| "Field element"), || {
41 fe.ok_or(SynthesisError::AssignmentMissing)
42 })?;
43 lc = lc - num.get_variable();
44 cs.enforce(|| "compute number from bits", |lc| lc, |lc| lc, |_| lc);
45 Ok(num)
46}
47
48/// Allocate a variable that is set to zero
49pub fn alloc_zero<F: PrimeField, CS: ConstraintSystem<F>>(
50 mut cs: CS,
51) -> Result<AllocatedNum<F>, SynthesisError> {
52 let zero = AllocatedNum::alloc(cs.namespace(|| "alloc"), || Ok(F::ZERO))?;
53 cs.enforce(
54 || "check zero is valid",
55 |lc| lc,
56 |lc| lc,
57 |lc| lc + zero.get_variable(),
58 );
59 Ok(zero)
60}
61
62/// Allocate a variable that is set to one
63pub fn alloc_one<F: PrimeField, CS: ConstraintSystem<F>>(
64 mut cs: CS,
65) -> Result<AllocatedNum<F>, SynthesisError> {
66 let one = AllocatedNum::alloc(cs.namespace(|| "alloc"), || Ok(F::ONE))?;
67 cs.enforce(
68 || "check one is valid",
69 |lc| lc + CS::one(),
70 |lc| lc + CS::one(),
71 |lc| lc + one.get_variable(),
72 );
73
74 Ok(one)
75}
76
77/// Allocate a scalar as a base. Only to be used is the scalar fits in base!
78pub fn alloc_scalar_as_base<G, CS>(
79 mut cs: CS,
80 input: Option<G::Scalar>,
81) -> Result<AllocatedNum<G::Base>, SynthesisError>
82where
83 G: Group,
84 <G as Group>::Scalar: PrimeFieldBits,
85 CS: ConstraintSystem<<G as Group>::Base>,
86{
87 AllocatedNum::alloc(cs.namespace(|| "allocate scalar as base"), || {
88 let input_bits = input.unwrap_or(G::Scalar::ZERO).clone().to_le_bits();
89 let mut mult = G::Base::ONE;
90 let mut val = G::Base::ZERO;
91 for bit in input_bits {
92 if bit {
93 val += mult;
94 }
95 mult = mult + mult;
96 }
97 Ok(val)
98 })
99}
100
101/// interepret scalar as base
102pub fn scalar_as_base<G: Group>(input: G::Scalar) -> G::Base {
103 let input_bits = input.to_le_bits();
104 let mut mult = G::Base::ONE;
105 let mut val = G::Base::ZERO;
106 for bit in input_bits {
107 if bit {
108 val += mult;
109 }
110 mult = mult + mult;
111 }
112 val
113}
114
115/// Allocate bignat a constant
116pub fn alloc_bignat_constant<F: PrimeField, CS: ConstraintSystem<F>>(
117 mut cs: CS,
118 val: &BigInt,
119 limb_width: usize,
120 n_limbs: usize,
121) -> Result<BigNat<F>, SynthesisError> {
122 let limbs = nat_to_limbs(val, limb_width, n_limbs).unwrap();
123 let bignat = BigNat::alloc_from_limbs(
124 cs.namespace(|| "alloc bignat"),
125 || Ok(limbs.clone()),
126 None,
127 limb_width,
128 n_limbs,
129 )?;
130 // Now enforce that the limbs are all equal to the constants
131 #[allow(clippy::needless_range_loop)]
132 for i in 0..n_limbs {
133 cs.enforce(
134 || format!("check limb {i}"),
135 |lc| lc + &bignat.limbs[i],
136 |lc| lc + CS::one(),
137 |lc| lc + (limbs[i], CS::one()),
138 );
139 }
140 Ok(bignat)
141}
142
143/// Check that two numbers are equal and return a bit
144pub fn alloc_num_equals<F: PrimeField, CS: ConstraintSystem<F>>(
145 mut cs: CS,
146 a: &AllocatedNum<F>,
147 b: &AllocatedNum<F>,
148) -> Result<AllocatedBit, SynthesisError> {
149 // Allocate and constrain `r`: result boolean bit.
150 // It equals `true` if `a` equals `b`, `false` otherwise
151 let r_value = match (a.get_value(), b.get_value()) {
152 (Some(a), Some(b)) => Some(a == b),
153 _ => None,
154 };
155
156 let r = AllocatedBit::alloc(cs.namespace(|| "r"), r_value)?;
157
158 // Allocate t s.t. t=1 if z1 == z2 else 1/(z1 - z2)
159
160 let t = AllocatedNum::alloc(cs.namespace(|| "t"), || {
161 Ok(if *a.get_value().get()? == *b.get_value().get()? {
162 F::ONE
163 } else {
164 (*a.get_value().get()? - *b.get_value().get()?)
165 .invert()
166 .unwrap()
167 })
168 })?;
169
170 cs.enforce(
171 || "t*(a - b) = 1 - r",
172 |lc| lc + t.get_variable(),
173 |lc| lc + a.get_variable() - b.get_variable(),
174 |lc| lc + CS::one() - r.get_variable(),
175 );
176
177 cs.enforce(
178 || "r*(a - b) = 0",
179 |lc| lc + r.get_variable(),
180 |lc| lc + a.get_variable() - b.get_variable(),
181 |lc| lc,
182 );
183
184 Ok(r)
185}
186
187/// If condition return a otherwise b
188pub fn conditionally_select<F: PrimeField, CS: ConstraintSystem<F>>(
189 mut cs: CS,
190 a: &AllocatedNum<F>,
191 b: &AllocatedNum<F>,
192 condition: &Boolean,
193) -> Result<AllocatedNum<F>, SynthesisError> {
194 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
195 if *condition.get_value().get()? {
196 Ok(*a.get_value().get()?)
197 } else {
198 Ok(*b.get_value().get()?)
199 }
200 })?;
201
202 // a * condition + b*(1-condition) = c ->
203 // a * condition - b*condition = c - b
204 cs.enforce(
205 || "conditional select constraint",
206 |lc| lc + a.get_variable() - b.get_variable(),
207 |_| condition.lc(CS::one(), F::ONE),
208 |lc| lc + c.get_variable() - b.get_variable(),
209 );
210
211 Ok(c)
212}
213
214/// If condition return a otherwise b
215pub fn conditionally_select_vec<F: PrimeField, CS: ConstraintSystem<F>>(
216 mut cs: CS,
217 a: &[AllocatedNum<F>],
218 b: &[AllocatedNum<F>],
219 condition: &Boolean,
220) -> Result<Vec<AllocatedNum<F>>, SynthesisError> {
221 a.iter()
222 .zip(b.iter())
223 .enumerate()
224 .map(|(i, (a, b))| {
225 conditionally_select(cs.namespace(|| format!("select_{i}")), a, b, condition)
226 })
227 .collect::<Result<Vec<AllocatedNum<F>>, SynthesisError>>()
228}
229
230/// If condition return a otherwise b where a and b are BigNats
231pub fn conditionally_select_bignat<F: PrimeField, CS: ConstraintSystem<F>>(
232 mut cs: CS,
233 a: &BigNat<F>,
234 b: &BigNat<F>,
235 condition: &Boolean,
236) -> Result<BigNat<F>, SynthesisError> {
237 assert!(a.limbs.len() == b.limbs.len());
238 let c = BigNat::alloc_from_nat(
239 cs.namespace(|| "conditional select result"),
240 || {
241 if *condition.get_value().get()? {
242 Ok(a.value.get()?.clone())
243 } else {
244 Ok(b.value.get()?.clone())
245 }
246 },
247 a.params.limb_width,
248 a.params.n_limbs,
249 )?;
250
251 // a * condition + b*(1-condition) = c ->
252 // a * condition - b*condition = c - b
253 for i in 0..c.limbs.len() {
254 cs.enforce(
255 || format!("conditional select constraint {i}"),
256 |lc| lc + &a.limbs[i] - &b.limbs[i],
257 |_| condition.lc(CS::one(), F::ONE),
258 |lc| lc + &c.limbs[i] - &b.limbs[i],
259 );
260 }
261 Ok(c)
262}
263
264/// Same as the above but Condition is an AllocatedNum that needs to be
265/// 0 or 1. 1 => True, 0 => False
266pub fn conditionally_select2<F: PrimeField, CS: ConstraintSystem<F>>(
267 mut cs: CS,
268 a: &AllocatedNum<F>,
269 b: &AllocatedNum<F>,
270 condition: &AllocatedNum<F>,
271) -> Result<AllocatedNum<F>, SynthesisError> {
272 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
273 if *condition.get_value().get()? == F::ONE {
274 Ok(*a.get_value().get()?)
275 } else {
276 Ok(*b.get_value().get()?)
277 }
278 })?;
279
280 // a * condition + b*(1-condition) = c ->
281 // a * condition - b*condition = c - b
282 cs.enforce(
283 || "conditional select constraint",
284 |lc| lc + a.get_variable() - b.get_variable(),
285 |lc| lc + condition.get_variable(),
286 |lc| lc + c.get_variable() - b.get_variable(),
287 );
288
289 Ok(c)
290}
291
292/// If condition set to 0 otherwise a. Condition is an allocated num
293pub fn select_zero_or_num2<F: PrimeField, CS: ConstraintSystem<F>>(
294 mut cs: CS,
295 a: &AllocatedNum<F>,
296 condition: &AllocatedNum<F>,
297) -> Result<AllocatedNum<F>, SynthesisError> {
298 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
299 if *condition.get_value().get()? == F::ONE {
300 Ok(F::ZERO)
301 } else {
302 Ok(*a.get_value().get()?)
303 }
304 })?;
305
306 // a * (1 - condition) = c
307 cs.enforce(
308 || "conditional select constraint",
309 |lc| lc + a.get_variable(),
310 |lc| lc + CS::one() - condition.get_variable(),
311 |lc| lc + c.get_variable(),
312 );
313
314 Ok(c)
315}
316
317/// If condition set to a otherwise 0. Condition is an allocated num
318pub fn select_num_or_zero2<F: PrimeField, CS: ConstraintSystem<F>>(
319 mut cs: CS,
320 a: &AllocatedNum<F>,
321 condition: &AllocatedNum<F>,
322) -> Result<AllocatedNum<F>, SynthesisError> {
323 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
324 if *condition.get_value().get()? == F::ONE {
325 Ok(*a.get_value().get()?)
326 } else {
327 Ok(F::ZERO)
328 }
329 })?;
330
331 cs.enforce(
332 || "conditional select constraint",
333 |lc| lc + a.get_variable(),
334 |lc| lc + condition.get_variable(),
335 |lc| lc + c.get_variable(),
336 );
337
338 Ok(c)
339}
340
341/// If condition set to a otherwise 0
342pub fn select_num_or_zero<F: PrimeField, CS: ConstraintSystem<F>>(
343 mut cs: CS,
344 a: &AllocatedNum<F>,
345 condition: &Boolean,
346) -> Result<AllocatedNum<F>, SynthesisError> {
347 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
348 if *condition.get_value().get()? {
349 Ok(*a.get_value().get()?)
350 } else {
351 Ok(F::ZERO)
352 }
353 })?;
354
355 cs.enforce(
356 || "conditional select constraint",
357 |lc| lc + a.get_variable(),
358 |_| condition.lc(CS::one(), F::ONE),
359 |lc| lc + c.get_variable(),
360 );
361
362 Ok(c)
363}
364
365/// If condition set to 1 otherwise a
366pub fn select_one_or_num2<F: PrimeField, CS: ConstraintSystem<F>>(
367 mut cs: CS,
368 a: &AllocatedNum<F>,
369 condition: &AllocatedNum<F>,
370) -> Result<AllocatedNum<F>, SynthesisError> {
371 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
372 if *condition.get_value().get()? == F::ONE {
373 Ok(F::ONE)
374 } else {
375 Ok(*a.get_value().get()?)
376 }
377 })?;
378
379 cs.enforce(
380 || "conditional select constraint",
381 |lc| lc + CS::one() - a.get_variable(),
382 |lc| lc + condition.get_variable(),
383 |lc| lc + c.get_variable() - a.get_variable(),
384 );
385 Ok(c)
386}
387
388/// If condition set to 1 otherwise a - b
389pub fn select_one_or_diff2<F: PrimeField, CS: ConstraintSystem<F>>(
390 mut cs: CS,
391 a: &AllocatedNum<F>,
392 b: &AllocatedNum<F>,
393 condition: &AllocatedNum<F>,
394) -> Result<AllocatedNum<F>, SynthesisError> {
395 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
396 if *condition.get_value().get()? == F::ONE {
397 Ok(F::ONE)
398 } else {
399 Ok(*a.get_value().get()? - *b.get_value().get()?)
400 }
401 })?;
402
403 cs.enforce(
404 || "conditional select constraint",
405 |lc| lc + CS::one() - a.get_variable() + b.get_variable(),
406 |lc| lc + condition.get_variable(),
407 |lc| lc + c.get_variable() - a.get_variable() + b.get_variable(),
408 );
409 Ok(c)
410}
411
412/// If condition set to a otherwise 1 for boolean conditions
413pub fn select_num_or_one<F: PrimeField, CS: ConstraintSystem<F>>(
414 mut cs: CS,
415 a: &AllocatedNum<F>,
416 condition: &Boolean,
417) -> Result<AllocatedNum<F>, SynthesisError> {
418 let c = AllocatedNum::alloc(cs.namespace(|| "conditional select result"), || {
419 if *condition.get_value().get()? {
420 Ok(*a.get_value().get()?)
421 } else {
422 Ok(F::ONE)
423 }
424 })?;
425
426 cs.enforce(
427 || "conditional select constraint",
428 |lc| lc + a.get_variable() - CS::one(),
429 |_| condition.lc(CS::one(), F::ONE),
430 |lc| lc + c.get_variable() - CS::one(),
431 );
432
433 Ok(c)
434}