Skip to main content

kimchi/circuits/lookup/
lookups.rs

1use crate::circuits::{
2    domains::EvaluationDomains,
3    gate::{CircuitGate, CurrOrNext, GateType},
4    lookup::{
5        index::LookupSelectors,
6        tables::{
7            combine_table_entry, get_table, GateLookupTable, LookupTable, RANGE_CHECK_TABLE_ID,
8            XOR_TABLE_ID,
9        },
10    },
11};
12use ark_ff::{Field, One, PrimeField, Zero};
13use ark_poly::{EvaluationDomain, Evaluations as E, Radix2EvaluationDomain as D};
14use o1_utils::field_helpers::i32_to_field;
15use serde::{Deserialize, Serialize};
16use std::{
17    collections::HashSet,
18    ops::{Mul, Neg},
19};
20use strum_macros::EnumIter;
21
22type Evaluations<Field> = E<Field, D<Field>>;
23
24//~ Lookups patterns are extremely flexible and can be configured in a number of ways.
25//~ Every type of lookup is a JointLookup -- to create a single lookup your create a
26//~ JointLookup that contains one SingleLookup.
27//~
28//~ Generally, the patterns of lookups possible are
29//~   * Multiple lookups per row
30//~    `JointLookup { }, ...,  JointLookup { }`
31//~   * Multiple values in each lookup (via joining, think of it like a tuple)
32//~    `JoinLookup { SingleLookup { }, ..., SingleLookup { } }`
33//~   * Multiple columns combined in linear combination to create each value
34//~    `JointLookup { SingleLookup { value: vec![(scale1, col1), ..., (scale2, col2)] } }`
35//~   * Any combination of these
36
37fn max_lookups_per_row(kinds: LookupPatterns) -> usize {
38    kinds
39        .into_iter()
40        .fold(0, |acc, x| core::cmp::max(x.max_lookups_per_row(), acc))
41}
42
43/// Flags for each of the built-in lookup patterns.
44///
45/// Each pattern corresponds to a specific lookup table and constraint
46/// configuration. When enabled, the corresponding lookup table is included
47/// in the circuit and lookup constraints are generated.
48///
49/// Typically computed via [`Self::from_gates`] by scanning circuit gates.
50#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
51#[cfg_attr(
52    feature = "ocaml_types",
53    derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)
54)]
55#[cfg_attr(feature = "wasm_types", wasm_bindgen::prelude::wasm_bindgen)]
56pub struct LookupPatterns {
57    /// Enables XOR lookup table for bitwise XOR operations.
58    pub xor: bool,
59    /// Enables generic lookup pattern for user-defined tables.
60    pub lookup: bool,
61    /// Enables range check lookup table for 12-bit range constraints.
62    pub range_check: bool,
63    /// Enables lookup tables for foreign field multiplication.
64    pub foreign_field_mul: bool,
65}
66
67impl IntoIterator for LookupPatterns {
68    type Item = LookupPattern;
69    type IntoIter = std::vec::IntoIter<Self::Item>;
70
71    fn into_iter(self) -> Self::IntoIter {
72        // Destructor pattern to make sure we add new lookup patterns.
73        let LookupPatterns {
74            xor,
75            lookup,
76            range_check,
77            foreign_field_mul,
78        } = self;
79
80        let mut patterns = Vec::with_capacity(5);
81
82        if xor {
83            patterns.push(LookupPattern::Xor)
84        }
85        if lookup {
86            patterns.push(LookupPattern::Lookup)
87        }
88        if range_check {
89            patterns.push(LookupPattern::RangeCheck)
90        }
91        if foreign_field_mul {
92            patterns.push(LookupPattern::ForeignFieldMul)
93        }
94        patterns.into_iter()
95    }
96}
97
98impl core::ops::Index<LookupPattern> for LookupPatterns {
99    type Output = bool;
100
101    fn index(&self, index: LookupPattern) -> &Self::Output {
102        match index {
103            LookupPattern::Xor => &self.xor,
104            LookupPattern::Lookup => &self.lookup,
105            LookupPattern::RangeCheck => &self.range_check,
106            LookupPattern::ForeignFieldMul => &self.foreign_field_mul,
107        }
108    }
109}
110
111impl core::ops::IndexMut<LookupPattern> for LookupPatterns {
112    fn index_mut(&mut self, index: LookupPattern) -> &mut Self::Output {
113        match index {
114            LookupPattern::Xor => &mut self.xor,
115            LookupPattern::Lookup => &mut self.lookup,
116            LookupPattern::RangeCheck => &mut self.range_check,
117            LookupPattern::ForeignFieldMul => &mut self.foreign_field_mul,
118        }
119    }
120}
121
122impl LookupPatterns {
123    /// Detects which lookup patterns are used by scanning circuit gates.
124    ///
125    /// Each gate type may require specific lookup patterns. This method
126    /// iterates through all gates and enables the corresponding pattern
127    /// flags based on [`LookupPattern::from_gate`].
128    pub fn from_gates<F: PrimeField>(gates: &[CircuitGate<F>]) -> LookupPatterns {
129        let mut kinds = LookupPatterns::default();
130        for g in gates.iter() {
131            for r in &[CurrOrNext::Curr, CurrOrNext::Next] {
132                if let Some(lookup_pattern) = LookupPattern::from_gate(g.typ, *r) {
133                    kinds[lookup_pattern] = true;
134                }
135            }
136        }
137        kinds
138    }
139
140    /// Returns `true` if any enabled pattern uses joint lookups (multiple
141    /// columns combined into a single lookup).
142    pub fn joint_lookups_used(&self) -> bool {
143        for lookup_pattern in *self {
144            if lookup_pattern.max_joint_size() > 1 {
145                return true;
146            }
147        }
148        false
149    }
150}
151
152/// Configuration for lookup-related features in a circuit.
153///
154/// Lookups allow efficient verification that witness values exist in
155/// precomputed tables. This struct tracks which lookup capabilities are
156/// needed, enabling kimchi to include only the required lookup machinery.
157#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
158#[cfg_attr(
159    feature = "ocaml_types",
160    derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Struct)
161)]
162#[cfg_attr(feature = "wasm_types", wasm_bindgen::prelude::wasm_bindgen)]
163pub struct LookupFeatures {
164    /// Which lookup patterns are enabled. See [`LookupPatterns`].
165    pub patterns: LookupPatterns,
166    /// Whether any enabled pattern uses joint lookups (multiple columns
167    /// combined into a single lookup value).
168    pub joint_lookup_used: bool,
169    /// Whether the circuit uses runtime lookup tables (tables whose contents
170    /// are provided at proving time rather than being fixed at setup).
171    pub uses_runtime_tables: bool,
172}
173
174impl LookupFeatures {
175    /// Detects lookup features by scanning circuit gates.
176    ///
177    /// Determines which lookup patterns are used and whether joint lookups
178    /// are needed based on the gate types present in the circuit.
179    pub fn from_gates<F: PrimeField>(gates: &[CircuitGate<F>], uses_runtime_tables: bool) -> Self {
180        let patterns = LookupPatterns::from_gates(gates);
181
182        let joint_lookup_used = patterns.joint_lookups_used();
183
184        LookupFeatures {
185            patterns,
186            uses_runtime_tables,
187            joint_lookup_used,
188        }
189    }
190}
191
192/// Describes the desired lookup configuration.
193#[derive(Copy, Clone, Serialize, Deserialize, Debug)]
194#[cfg_attr(feature = "wasm_types", wasm_bindgen::prelude::wasm_bindgen)]
195pub struct LookupInfo {
196    /// The maximum length of an element of `kinds`. This can be computed from `kinds`.
197    pub max_per_row: usize,
198    /// The maximum joint size of any joint lookup in a constraint in `kinds`. This can be computed from `kinds`.
199    pub max_joint_size: u32,
200    /// The features enabled for this lookup configuration
201    pub features: LookupFeatures,
202}
203
204impl LookupInfo {
205    /// Create the default lookup configuration.
206    pub fn create(features: LookupFeatures) -> Self {
207        let max_per_row = max_lookups_per_row(features.patterns);
208
209        LookupInfo {
210            max_joint_size: features
211                .patterns
212                .into_iter()
213                .fold(0, |acc, v| core::cmp::max(acc, v.max_joint_size())),
214            max_per_row,
215            features,
216        }
217    }
218
219    pub fn create_from_gates<F: PrimeField>(
220        gates: &[CircuitGate<F>],
221        uses_runtime_tables: bool,
222    ) -> Option<Self> {
223        let features = LookupFeatures::from_gates(gates, uses_runtime_tables);
224
225        if features.patterns == LookupPatterns::default() {
226            None
227        } else {
228            Some(Self::create(features))
229        }
230    }
231
232    /// Each entry in `kinds` has a corresponding selector polynomial that controls whether that
233    /// lookup kind should be enforced at a given row. This computes those selector polynomials.
234    pub fn selector_polynomials_and_tables<F: PrimeField>(
235        &self,
236        domain: &EvaluationDomains<F>,
237        gates: &[CircuitGate<F>],
238    ) -> (LookupSelectors<Evaluations<F>>, Vec<LookupTable<F>>) {
239        let n = domain.d1.size();
240
241        let mut selector_values = LookupSelectors::default();
242        for kind in self.features.patterns {
243            selector_values[kind] = Some(vec![F::zero(); n]);
244        }
245
246        let mut gate_tables = HashSet::new();
247
248        let mut update_selector = |lookup_pattern, i| {
249            let selector = selector_values[lookup_pattern]
250                .as_mut()
251                .unwrap_or_else(|| panic!("has selector for {lookup_pattern:?}"));
252            selector[i] = F::one();
253        };
254
255        // TODO: is take(n) useful here? I don't see why we need this
256        for (i, gate) in gates.iter().enumerate().take(n) {
257            let typ = gate.typ;
258
259            if let Some(lookup_pattern) = LookupPattern::from_gate(typ, CurrOrNext::Curr) {
260                update_selector(lookup_pattern, i);
261                if let Some(table_kind) = lookup_pattern.table() {
262                    gate_tables.insert(table_kind);
263                }
264            }
265            if let Some(lookup_pattern) = LookupPattern::from_gate(typ, CurrOrNext::Next) {
266                update_selector(lookup_pattern, i + 1);
267                if let Some(table_kind) = lookup_pattern.table() {
268                    gate_tables.insert(table_kind);
269                }
270            }
271        }
272
273        // Actually, don't need to evaluate over domain 8 here.
274        // TODO: so why do it :D?
275        let selector_values8: LookupSelectors<_> = selector_values.map(|v| {
276            E::<F, D<F>>::from_vec_and_domain(v, domain.d1)
277                .interpolate()
278                .evaluate_over_domain(domain.d8)
279        });
280        let res_tables: Vec<_> = gate_tables.into_iter().map(get_table).collect();
281        (selector_values8, res_tables)
282    }
283
284    /// For each row in the circuit, which lookup-constraints should be enforced at that row.
285    pub fn by_row<F: PrimeField>(&self, gates: &[CircuitGate<F>]) -> Vec<Vec<JointLookupSpec<F>>> {
286        let mut kinds = vec![vec![]; gates.len() + 1];
287        for i in 0..gates.len() {
288            let typ = gates[i].typ;
289
290            if let Some(lookup_pattern) = LookupPattern::from_gate(typ, CurrOrNext::Curr) {
291                kinds[i] = lookup_pattern.lookups();
292            }
293            if let Some(lookup_pattern) = LookupPattern::from_gate(typ, CurrOrNext::Next) {
294                kinds[i + 1] = lookup_pattern.lookups();
295            }
296        }
297        kinds
298    }
299}
300
301/// A position in the circuit relative to a given row.
302#[derive(Clone, Copy, Debug, Serialize, Deserialize)]
303pub struct LocalPosition {
304    pub row: CurrOrNext,
305    pub column: usize,
306}
307
308/// Look up a single value in a lookup table. The value may be computed as a linear
309/// combination of locally-accessible cells.
310#[derive(Clone, Serialize, Deserialize)]
311pub struct SingleLookup<F> {
312    /// Linear combination of local-positions
313    pub value: Vec<(F, LocalPosition)>,
314}
315
316impl<F: Copy> SingleLookup<F> {
317    /// Evaluate the linear combination specifying the lookup value to a field element.
318    pub fn evaluate<K, G: Fn(LocalPosition) -> K>(&self, eval: G) -> K
319    where
320        K: Zero,
321        K: Mul<F, Output = K>,
322    {
323        self.value
324            .iter()
325            .fold(K::zero(), |acc, (c, p)| acc + eval(*p) * *c)
326    }
327}
328
329/// The table ID associated with a particular lookup
330#[derive(Clone, Serialize, Deserialize, Debug)]
331pub enum LookupTableID {
332    /// Look up the value from the given fixed table ID
333    Constant(i32),
334    /// Look up the value in the table with ID given by the value in the witness column
335    WitnessColumn(usize),
336}
337
338/// A spec for checking that the given vector belongs to a vector-valued lookup table.
339#[derive(Clone, Serialize, Deserialize, Debug)]
340pub struct JointLookup<SingleLookup, LookupTableID> {
341    /// The ID for the table associated with this lookup.
342    /// Positive IDs are intended to be used for the fixed tables associated with individual gates,
343    /// with negative IDs reserved for gates defined by the particular constraint system to avoid
344    /// accidental collisions.
345    pub table_id: LookupTableID,
346    pub entry: Vec<SingleLookup>,
347}
348
349/// A spec for checking that the given vector belongs to a vector-valued lookup table, where the
350/// components of the vector are computed from a linear combination of locally-accessible cells.
351pub type JointLookupSpec<F> = JointLookup<SingleLookup<F>, LookupTableID>;
352
353/// A concrete value or representation of a lookup.
354pub type JointLookupValue<F> = JointLookup<F, F>;
355
356impl<F: Zero + One + Clone + Neg<Output = F> + From<u64>> JointLookupValue<F> {
357    /// Evaluate the combined value of a joint-lookup.
358    pub fn evaluate(&self, joint_combiner: &F, table_id_combiner: &F) -> F {
359        combine_table_entry(
360            joint_combiner,
361            table_id_combiner,
362            self.entry.iter(),
363            &self.table_id,
364        )
365    }
366}
367
368impl<F: Copy> JointLookup<SingleLookup<F>, LookupTableID> {
369    /// Reduce linear combinations in the lookup entries to a single value, resolving local
370    /// positions using the given function.
371    pub fn reduce<K, G: Fn(LocalPosition) -> K>(&self, eval: &G) -> JointLookupValue<K>
372    where
373        K: Zero,
374        K: Mul<F, Output = K>,
375        K: Neg<Output = K>,
376        K: From<u64>,
377    {
378        let table_id = match self.table_id {
379            LookupTableID::Constant(table_id) => i32_to_field(table_id),
380            LookupTableID::WitnessColumn(column) => eval(LocalPosition {
381                row: CurrOrNext::Curr,
382                column,
383            }),
384        };
385        JointLookup {
386            table_id,
387            entry: self.entry.iter().map(|s| s.evaluate(eval)).collect(),
388        }
389    }
390
391    /// Evaluate the combined value of a joint-lookup, resolving local positions using the given
392    /// function.
393    pub fn evaluate<K, G: Fn(LocalPosition) -> K>(
394        &self,
395        joint_combiner: &K,
396        table_id_combiner: &K,
397        eval: &G,
398    ) -> K
399    where
400        K: Zero + One + Clone,
401        K: Mul<F, Output = K>,
402        K: Neg<Output = K>,
403        K: From<u64>,
404    {
405        self.reduce(eval)
406            .evaluate(joint_combiner, table_id_combiner)
407    }
408}
409
410#[derive(
411    Copy, Clone, Serialize, Deserialize, Debug, EnumIter, PartialEq, Eq, PartialOrd, Ord, Hash,
412)]
413#[cfg_attr(
414    feature = "ocaml_types",
415    derive(ocaml::IntoValue, ocaml::FromValue, ocaml_gen::Enum)
416)]
417pub enum LookupPattern {
418    Xor,
419    Lookup,
420    RangeCheck,
421    ForeignFieldMul,
422}
423
424impl LookupPattern {
425    /// Returns the maximum number of lookups per row that are used by the pattern.
426    pub fn max_lookups_per_row(&self) -> usize {
427        match self {
428            LookupPattern::Xor | LookupPattern::RangeCheck | LookupPattern::ForeignFieldMul => 4,
429            LookupPattern::Lookup => 3,
430        }
431    }
432
433    /// Returns the maximum number of values that are used in any vector lookup in this pattern.
434    pub fn max_joint_size(&self) -> u32 {
435        match self {
436            LookupPattern::Xor => 3,
437            LookupPattern::Lookup => 2,
438            LookupPattern::ForeignFieldMul | LookupPattern::RangeCheck => 1,
439        }
440    }
441
442    /// Returns the layout of the lookups used by this pattern.
443    ///
444    /// # Panics
445    ///
446    /// Will panic if `multiplicative inverse` operation fails.
447    pub fn lookups<F: Field>(&self) -> Vec<JointLookupSpec<F>> {
448        let curr_row = |column| LocalPosition {
449            row: CurrOrNext::Curr,
450            column,
451        };
452        match self {
453            LookupPattern::Xor => {
454                (0..4)
455                    .map(|i| {
456                        // each row represents an XOR operation
457                        // where l XOR r = o
458                        //
459                        // 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14
460                        // - - - l - - - r - - -  o  -  -  -
461                        // - - - - l - - - r - -  -  o  -  -
462                        // - - - - - l - - - r -  -  -  o  -
463                        // - - - - - - l - - - r  -  -  -  o
464                        let left = curr_row(3 + i);
465                        let right = curr_row(7 + i);
466                        let output = curr_row(11 + i);
467                        let l = |loc: LocalPosition| SingleLookup {
468                            value: vec![(F::one(), loc)],
469                        };
470                        JointLookup {
471                            table_id: LookupTableID::Constant(XOR_TABLE_ID),
472                            entry: vec![l(left), l(right), l(output)],
473                        }
474                    })
475                    .collect()
476            }
477            LookupPattern::Lookup => {
478                (0..3)
479                    .map(|i| {
480                        // 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14
481                        // - i v - - - - - - - -  -  -  -  -
482                        // - - - i v - - - - - -  -  -  -  -
483                        // - - - - - i v - - - -  -  -  -  -
484                        let index = curr_row(2 * i + 1);
485                        let value = curr_row(2 * i + 2);
486                        let l = |loc: LocalPosition| SingleLookup {
487                            value: vec![(F::one(), loc)],
488                        };
489                        JointLookup {
490                            table_id: LookupTableID::WitnessColumn(0),
491                            entry: vec![l(index), l(value)],
492                        }
493                    })
494                    .collect()
495            }
496            LookupPattern::RangeCheck => {
497                (3..=6)
498                    .map(|column| {
499                        //   0 1 2 3 4 5 6 7 8 9 10 11 12 13 14
500                        //   - - - L L L L - - - -  -  -  -  -
501                        JointLookup {
502                            table_id: LookupTableID::Constant(RANGE_CHECK_TABLE_ID),
503                            entry: vec![SingleLookup {
504                                value: vec![(F::one(), curr_row(column))],
505                            }],
506                        }
507                    })
508                    .collect()
509            }
510            LookupPattern::ForeignFieldMul => {
511                (7..=10)
512                    .map(|col| {
513                        // curr and next (in next carry0 is in w(7))
514                        //   0 1 2 3 4 5 6 7 8 9 10 11 12 13 14
515                        //   - - - - - - - L L L L  -  -  -  -
516                        //    * Constrain w(7), w(8), w(9), w(10) to 12-bits
517                        JointLookup {
518                            table_id: LookupTableID::Constant(RANGE_CHECK_TABLE_ID),
519                            entry: vec![SingleLookup {
520                                value: vec![(F::one(), curr_row(col))],
521                            }],
522                        }
523                    })
524                    .collect()
525            }
526        }
527    }
528
529    /// Returns the lookup table used by the pattern, or `None` if no specific table is rqeuired.
530    pub fn table(&self) -> Option<GateLookupTable> {
531        match self {
532            LookupPattern::Xor => Some(GateLookupTable::Xor),
533            LookupPattern::Lookup => None,
534            LookupPattern::RangeCheck => Some(GateLookupTable::RangeCheck),
535            LookupPattern::ForeignFieldMul => Some(GateLookupTable::RangeCheck),
536        }
537    }
538
539    /// Returns the lookup pattern used by a [`GateType`] on a given row (current or next).
540    pub fn from_gate(gate_type: GateType, curr_or_next: CurrOrNext) -> Option<Self> {
541        use CurrOrNext::{Curr, Next};
542        use GateType::*;
543        match (gate_type, curr_or_next) {
544            (Lookup, Curr) => Some(LookupPattern::Lookup),
545            (RangeCheck0, Curr) | (RangeCheck1, Curr | Next) | (Rot64, Curr) => {
546                Some(LookupPattern::RangeCheck)
547            }
548            (ForeignFieldMul, Curr | Next) => Some(LookupPattern::ForeignFieldMul),
549            (Xor16, Curr) => Some(LookupPattern::Xor),
550            _ => None,
551        }
552    }
553}
554
555impl GateType {
556    /// Which lookup-patterns should be applied on which rows.
557    pub fn lookup_kinds() -> Vec<LookupPattern> {
558        vec![
559            LookupPattern::Xor,
560            LookupPattern::Lookup,
561            LookupPattern::RangeCheck,
562            LookupPattern::ForeignFieldMul,
563        ]
564    }
565}
566
567#[test]
568fn lookup_pattern_constants_correct() {
569    use strum::IntoEnumIterator;
570
571    for pat in LookupPattern::iter() {
572        let lookups = pat.lookups::<mina_curves::pasta::Fp>();
573        let max_joint_size = lookups
574            .iter()
575            .map(|lookup| lookup.entry.len())
576            .max()
577            .unwrap_or(0);
578        // NB: We include pat in the assertions so that the test will print out which pattern failed
579        assert_eq!((pat, pat.max_lookups_per_row()), (pat, lookups.len()));
580        assert_eq!((pat, pat.max_joint_size()), (pat, max_joint_size as u32));
581    }
582}
583
584#[cfg(feature = "wasm_types")]
585pub mod wasm {
586    use super::*;
587
588    #[wasm_bindgen::prelude::wasm_bindgen]
589    impl LookupPatterns {
590        #[wasm_bindgen::prelude::wasm_bindgen(constructor)]
591        pub fn new(
592            xor: bool,
593            lookup: bool,
594            range_check: bool,
595            foreign_field_mul: bool,
596        ) -> LookupPatterns {
597            LookupPatterns {
598                xor,
599                lookup,
600                range_check,
601                foreign_field_mul,
602            }
603        }
604    }
605
606    #[wasm_bindgen::prelude::wasm_bindgen]
607    impl LookupFeatures {
608        #[wasm_bindgen::prelude::wasm_bindgen(constructor)]
609        pub fn new(
610            patterns: LookupPatterns,
611            joint_lookup_used: bool,
612            uses_runtime_tables: bool,
613        ) -> LookupFeatures {
614            LookupFeatures {
615                patterns,
616                joint_lookup_used,
617                uses_runtime_tables,
618            }
619        }
620    }
621
622    #[wasm_bindgen::prelude::wasm_bindgen]
623    impl LookupInfo {
624        #[wasm_bindgen::prelude::wasm_bindgen(constructor)]
625        pub fn new(
626            max_per_row: usize,
627            max_joint_size: u32,
628            features: LookupFeatures,
629        ) -> LookupInfo {
630            LookupInfo {
631                max_per_row,
632                max_joint_size,
633                features,
634            }
635        }
636    }
637}