kimchi/circuits/polynomials/range_check/
witness.rs

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

kimchi/circuits/polynomials/range_check/
witness.rs
