kimchi/circuits/polynomials/range_check/
witness.rs

1//! Range check witness computation
2
3use ark_ff::PrimeField;
4use core::array;
5use num_bigint::BigUint;
6use num_integer::Integer;
7use o1_utils::{field_helpers::BigUintFieldHelpers, FieldHelpers, ForeignElement};
8
9use crate::{
10    circuits::{
11        polynomial::COLUMNS,
12        polynomials::foreign_field_common::{BigUintForeignFieldHelpers, LIMB_BITS},
13        witness::{init_row, CopyBitsCell, CopyCell, VariableCell, Variables, WitnessCell},
14    },
15    variable_map, variables,
16};
17
18/// Witness layout
19///   * The values and cell contents are in little-endian order.
20///     This is important for compatibility with other gates, where
21///     elements of the first 7 columns could be copied and reused by them.
22///     So they should be in the usual little-endian witness byte order.
23///   * Limbs are mapped to columns so that those containing the MSBs
24///     are in lower numbered columns (i.e. big-endian column mapping).
25///     This is important so that copy constraints are possible on the MSBs.
26///     For example, we can convert the `RangeCheck0` circuit gate into
27///     a 64-bit lookup by adding two copy constraints to constrain
28///     columns 1 and 2 to zero.
29fn layout<F: PrimeField>() -> [Vec<Box<dyn WitnessCell<F>>>; 4] {
30    [
31        /* row 1, RangeCheck0 row */
32        range_check_0_row("v0", 0),
33        /* row 2, RangeCheck0 row */
34        range_check_0_row("v1", 1),
35        /* row 3, RangeCheck1 row */
36        vec![
37            VariableCell::create("v2"),
38            VariableCell::create("v12"), // optional
39            /* 2-bit crumbs (placed here to keep lookup pattern */
40            /*               the same as RangeCheck0) */
41            CopyBitsCell::create(2, 0, 86, 88),
42            /* 12-bit plookups */
43            CopyBitsCell::create(2, 0, 74, 86),
44            CopyBitsCell::create(2, 0, 62, 74),
45            CopyBitsCell::create(2, 0, 50, 62),
46            CopyBitsCell::create(2, 0, 38, 50),
47            /* 2-bit crumbs */
48            CopyBitsCell::create(2, 0, 36, 38),
49            CopyBitsCell::create(2, 0, 34, 36),
50            CopyBitsCell::create(2, 0, 32, 34),
51            CopyBitsCell::create(2, 0, 30, 32),
52            CopyBitsCell::create(2, 0, 28, 30),
53            CopyBitsCell::create(2, 0, 26, 28),
54            CopyBitsCell::create(2, 0, 24, 26),
55            CopyBitsCell::create(2, 0, 22, 24),
56        ],
57        /* row 4, Zero row */
58        vec![
59            CopyBitsCell::create(2, 0, 20, 22),
60            /* 2-bit crumbs (placed here to keep lookup pattern */
61            /*               the same as RangeCheck0) */
62            CopyBitsCell::create(2, 0, 18, 20),
63            CopyBitsCell::create(2, 0, 16, 18),
64            /* 12-bit plookups (see note about copies in range_check_row) */
65            CopyCell::create(0, 1),
66            CopyCell::create(0, 2),
67            CopyCell::create(1, 1),
68            CopyCell::create(1, 2),
69            /* 2-bit crumbs */
70            CopyBitsCell::create(2, 0, 14, 16),
71            CopyBitsCell::create(2, 0, 12, 14),
72            CopyBitsCell::create(2, 0, 10, 12),
73            CopyBitsCell::create(2, 0, 8, 10),
74            CopyBitsCell::create(2, 0, 6, 8),
75            CopyBitsCell::create(2, 0, 4, 6),
76            CopyBitsCell::create(2, 0, 2, 4),
77            CopyBitsCell::create(2, 0, 0, 2),
78        ],
79    ]
80}
81
82/// The row layout for `RangeCheck0`
83pub fn range_check_0_row<F: PrimeField>(
84    limb_name: &'static str,
85    row: usize,
86) -> Vec<Box<dyn WitnessCell<F>>> {
87    vec![
88        VariableCell::create(limb_name),
89        /* 12-bit copies */
90        // Copy cells are required because we have a limit
91        // of 4 lookups per row.  These two lookups are moved to
92        // the 4th row, which is a Zero circuit gate, and the
93        // RangeCheck1 circuit gate triggers the lookup constraints.
94        CopyBitsCell::create(row, 0, 76, 88),
95        CopyBitsCell::create(row, 0, 64, 76),
96        /* 12-bit plookups */
97        CopyBitsCell::create(row, 0, 52, 64),
98        CopyBitsCell::create(row, 0, 40, 52),
99        CopyBitsCell::create(row, 0, 28, 40),
100        CopyBitsCell::create(row, 0, 16, 28),
101        /* 2-bit crumbs */
102        CopyBitsCell::create(row, 0, 14, 16),
103        CopyBitsCell::create(row, 0, 12, 14),
104        CopyBitsCell::create(row, 0, 10, 12),
105        CopyBitsCell::create(row, 0, 8, 10),
106        CopyBitsCell::create(row, 0, 6, 8),
107        CopyBitsCell::create(row, 0, 4, 6),
108        CopyBitsCell::create(row, 0, 2, 4),
109        CopyBitsCell::create(row, 0, 0, 2),
110    ]
111}
112
113/// Create a multi range check witness from three 88-bit values: v0, v1 and v2
114pub fn create_multi<F: PrimeField>(v0: F, v1: F, v2: F) -> [Vec<F>; COLUMNS] {
115    let layout = layout();
116    let mut witness: [Vec<F>; COLUMNS] = array::from_fn(|_| vec![F::zero(); 4]);
117
118    init_row(&mut witness, 0, 0, &layout, &variables!(v0));
119    init_row(&mut witness, 0, 1, &layout, &variables!(v1));
120    init_row(
121        &mut witness,
122        0,
123        2,
124        &layout,
125        &variable_map!("v2" => v2, "v12" => F::zero()),
126    );
127    init_row(&mut witness, 0, 3, &layout, &variables!());
128
129    witness
130}
131
132/// Create a multi range check witness from two limbs: v01 (176 bits), v2 (88 bits),
133/// where v2 is the most significant limb and v01 is the least significant limb
134pub fn create_multi_compact<F: PrimeField>(v01: F, v2: F) -> [Vec<F>; COLUMNS] {
135    let layout = layout();
136    let mut witness: [Vec<F>; COLUMNS] = array::from_fn(|_| vec![F::zero(); 4]);
137
138    let (v1, v0) = v01.to_biguint().div_rem(&BigUint::two_to_limb());
139    let v0: F = v0.to_field().expect("failed to convert to field element");
140    let v1: F = v1.to_field().expect("failed to convert to field element");
141
142    init_row(&mut witness, 0, 0, &layout, &variable_map!("v0" => v2));
143    init_row(&mut witness, 0, 1, &layout, &variable_map!("v1" => v0));
144
145    init_row(
146        &mut witness,
147        0,
148        2,
149        &layout,
150        &variable_map!("v2" => v1, "v12" => v01),
151    );
152    init_row(&mut witness, 0, 3, &layout, &variables!());
153
154    witness
155}
156
157/// Create a multi range check witness from limbs
158pub fn create_multi_limbs<F: PrimeField>(limbs: &[F; 3]) -> [Vec<F>; COLUMNS] {
159    create_multi(limbs[0], limbs[1], limbs[2])
160}
161
162/// Create a multi range check witness from compact limbs
163pub fn create_multi_compact_limbs<F: PrimeField>(limbs: &[F; 2]) -> [Vec<F>; COLUMNS] {
164    create_multi_compact(limbs[0], limbs[1])
165}
166
167/// Create a single range check witness
168/// Input: 88-bit value v0
169pub fn create<F: PrimeField>(v0: F) -> [Vec<F>; COLUMNS] {
170    let layout = vec![range_check_0_row("v0", 0)];
171    let mut witness: [Vec<F>; COLUMNS] = array::from_fn(|_| vec![F::zero()]);
172
173    init_row(&mut witness, 0, 0, &layout, &variables!(v0));
174
175    witness
176}
177
178/// Extend an existing witness with a multi-range-check gadget for three 88-bit values: v0, v1 and v2
179pub fn extend_multi<F: PrimeField>(witness: &mut [Vec<F>; COLUMNS], v0: F, v1: F, v2: F) {
180    let limbs_witness = create_multi(v0, v1, v2);
181    for col in 0..COLUMNS {
182        witness[col].extend(limbs_witness[col].iter())
183    }
184}
185
186/// Extend and existing witness with a multi range check witness for two limbs: v01 (176 bits), v2 (88 bits),
187/// where v2 is the most significant limb and v01 is the least significant limb
188pub fn extend_multi_compact<F: PrimeField>(witness: &mut [Vec<F>; COLUMNS], v01: F, v2: F) {
189    let limbs_witness = create_multi_compact(v01, v2);
190    for col in 0..COLUMNS {
191        witness[col].extend(limbs_witness[col].iter())
192    }
193}
194
195/// Extend an existing witness with a multi-range-check gadget for limbs
196pub fn extend_multi_limbs<F: PrimeField>(witness: &mut [Vec<F>; COLUMNS], limbs: &[F; 3]) {
197    let limbs_witness = create_multi_limbs(limbs);
198    for col in 0..COLUMNS {
199        witness[col].extend(limbs_witness[col].iter())
200    }
201}
202
203/// Extend an existing witness with a multi-range-check gadget for compact limbs
204pub fn extend_multi_compact_limbs<F: PrimeField>(witness: &mut [Vec<F>; COLUMNS], limbs: &[F; 2]) {
205    let limbs_witness = create_multi_compact_limbs(limbs);
206    for col in 0..COLUMNS {
207        witness[col].extend(limbs_witness[col].iter())
208    }
209}
210
211/// Extend an existing witness with a multi-range-check gadget for ForeignElement
212pub fn extend_multi_from_fe<F: PrimeField>(
213    witness: &mut [Vec<F>; COLUMNS],
214    fe: &ForeignElement<F, LIMB_BITS, 3>,
215) {
216    extend_multi(witness, fe.limbs[0], fe.limbs[1], fe.limbs[2]);
217}
218
219/// Extend an existing witness with a single range check witness for foreign field element
220pub fn extend<F: PrimeField>(witness: &mut [Vec<F>; COLUMNS], fe: F) {
221    let limbs_witness = create(fe);
222    for col in 0..COLUMNS {
223        witness[col].extend(limbs_witness[col].iter())
224    }
225}
226
227/// Extend an existing witness with a single-range-check gate for 88bits
228pub fn extend_single<F: PrimeField>(witness: &mut [Vec<F>; COLUMNS], elem: F) {
229    let single_wit = create(elem);
230    for col in 0..COLUMNS {
231        witness[col].extend(single_wit[col].iter())
232    }
233}
kimchi/circuits/polynomials/range_check/witness.rs

kimchi/circuits/polynomials/range_check/
witness.rs
