1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
use crate::cmp::CmpGadget;
use super::*;
impl<F: PrimeField> CmpGadget<F> for Boolean<F> {
fn is_ge(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
// a | b | (a | !b) | a >= b
// --|---|--------|--------
// 0 | 0 | 1 | 1
// 1 | 0 | 1 | 1
// 0 | 1 | 0 | 0
// 1 | 1 | 1 | 1
Ok(self | &(!other))
}
}
impl<F: PrimeField> Boolean<F> {
/// Enforces that `bits`, when interpreted as a integer, is less than
/// `F::characteristic()`, That is, interpret bits as a little-endian
/// integer, and enforce that this integer is "in the field Z_p", where
/// `p = F::characteristic()` .
#[tracing::instrument(target = "gr1cs")]
pub fn enforce_in_field_le(bits: &[Self]) -> Result<(), SynthesisError> {
// `bits` < F::characteristic() <==> `bits` <= F::characteristic() -1
let mut b = F::characteristic().to_vec();
assert_eq!(b[0] % 2, 1);
b[0] -= 1; // This works, because the LSB is one, so there's no borrows.
let run = Self::enforce_smaller_or_equal_than_le(bits, b)?;
// We should always end in a "run" of zeros, because
// the characteristic is an odd prime. So, this should
// be empty.
assert!(run.is_empty());
Ok(())
}
/// Enforces that `bits` is less than or equal to `element`,
/// when both are interpreted as (little-endian) integers.
#[tracing::instrument(target = "gr1cs", skip(element))]
pub fn enforce_smaller_or_equal_than_le(
bits: &[Self],
element: impl AsRef<[u64]>,
) -> Result<Vec<Self>, SynthesisError> {
let b: &[u64] = element.as_ref();
let mut bits_iter = bits.iter().rev(); // Iterate in big-endian
// Runs of ones in r
let mut last_run = Boolean::TRUE;
let mut current_run = vec![];
let mut element_num_bits = 0;
for _ in BitIteratorBE::without_leading_zeros(b) {
element_num_bits += 1;
}
if bits.len() > element_num_bits {
let mut or_result = Boolean::FALSE;
for should_be_zero in &bits[element_num_bits..] {
or_result |= should_be_zero;
let _ = bits_iter.next().unwrap();
}
or_result.enforce_equal(&Boolean::FALSE)?;
}
for (b, a) in BitIteratorBE::without_leading_zeros(b).zip(bits_iter.by_ref()) {
if b {
// This is part of a run of ones.
current_run.push(a.clone());
} else {
if !current_run.is_empty() {
// This is the start of a run of zeros, but we need
// to k-ary AND against `last_run` first.
current_run.push(last_run.clone());
last_run = Self::kary_and(¤t_run)?;
current_run.truncate(0);
}
// If `last_run` is true, `a` must be false, or it would
// not be in the field.
//
// If `last_run` is false, `a` can be true or false.
//
// Ergo, at least one of `last_run` and `a` must be false.
Self::enforce_kary_nand(&[last_run.clone(), a.clone()])?;
}
}
assert!(bits_iter.next().is_none());
Ok(current_run)
}
}