Skip to main content

kimchi/circuits/lookup/
index.rs

1use super::runtime_tables::{RuntimeTableCfg, RuntimeTableSpec};
2use crate::circuits::{
3    domains::EvaluationDomains,
4    gate::CircuitGate,
5    lookup::{
6        constraints::LookupConfiguration,
7        lookups::{LookupInfo, LookupPattern},
8        tables::LookupTable,
9    },
10};
11use alloc::{format, string::String, vec, vec::Vec};
12use ark_ff::{FftField, PrimeField};
13use ark_poly::{
14    univariate::DensePolynomial as DP, EvaluationDomain, Evaluations as E,
15    Radix2EvaluationDomain as D,
16};
17use o1_utils::field_helpers::i32_to_field;
18use serde::{de::DeserializeOwned, Deserialize, Serialize};
19use serde_with::serde_as;
20use thiserror::Error;
21
22/// Represents an error found when computing the lookup constraint system
23#[derive(Debug, Error, Clone, Serialize, Deserialize)]
24pub enum LookupError {
25    #[error("One of the lookup tables has columns of different lengths")]
26    InconsistentTableLength,
27    #[error("The combined lookup table is larger than allowed by the domain size. Observed: {length}, expected: {maximum_allowed}")]
28    LookupTableTooLong {
29        length: usize,
30        maximum_allowed: usize,
31    },
32    #[error("The table with id 0 must have an entry of all zeros")]
33    TableIDZeroMustHaveZeroEntry,
34    #[error("Cannot create a combined table since ids for sub-tables are colliding. The collision type is: {collision_type}")]
35    LookupTableIdCollision { collision_type: String },
36}
37
38/// Lookup selectors
39#[derive(Clone, Serialize, Deserialize, Debug, Default)]
40pub struct LookupSelectors<T> {
41    /// XOR pattern lookup selector
42    pub xor: Option<T>,
43    /// Lookup pattern lookup selector
44    pub lookup: Option<T>,
45    /// Range check pattern lookup selector
46    pub range_check: Option<T>,
47    /// Foreign field multiplication pattern lookup selector
48    pub ffmul: Option<T>,
49}
50
51#[serde_as]
52#[derive(Clone, Serialize, Deserialize, Debug, Default)]
53struct LookupSelectorsSerdeAs<F: FftField> {
54    #[serde_as(as = "Option<o1_utils::serialization::SerdeAs>")]
55    pub xor: Option<E<F, D<F>>>,
56    #[serde_as(as = "Option<o1_utils::serialization::SerdeAs>")]
57    pub lookup: Option<E<F, D<F>>>,
58    #[serde_as(as = "Option<o1_utils::serialization::SerdeAs>")]
59    pub range_check: Option<E<F, D<F>>>,
60    #[serde_as(as = "Option<o1_utils::serialization::SerdeAs>")]
61    pub ffmul: Option<E<F, D<F>>>,
62}
63
64impl<F: FftField> serde_with::SerializeAs<LookupSelectors<E<F, D<F>>>>
65    for LookupSelectorsSerdeAs<F>
66{
67    fn serialize_as<S>(val: &LookupSelectors<E<F, D<F>>>, serializer: S) -> Result<S::Ok, S::Error>
68    where
69        S: serde::Serializer,
70    {
71        let repr = LookupSelectorsSerdeAs {
72            xor: val.xor.clone(),
73            lookup: val.lookup.clone(),
74            range_check: val.range_check.clone(),
75            ffmul: val.ffmul.clone(),
76        };
77        repr.serialize(serializer)
78    }
79}
80
81impl<'de, F: FftField> serde_with::DeserializeAs<'de, LookupSelectors<E<F, D<F>>>>
82    for LookupSelectorsSerdeAs<F>
83{
84    fn deserialize_as<Dz>(deserializer: Dz) -> Result<LookupSelectors<E<F, D<F>>>, Dz::Error>
85    where
86        Dz: serde::Deserializer<'de>,
87    {
88        let LookupSelectorsSerdeAs {
89            xor,
90            lookup,
91            range_check,
92            ffmul,
93        } = LookupSelectorsSerdeAs::deserialize(deserializer)?;
94        Ok(LookupSelectors {
95            xor,
96            lookup,
97            range_check,
98            ffmul,
99        })
100    }
101}
102
103impl<T> core::ops::Index<LookupPattern> for LookupSelectors<T> {
104    type Output = Option<T>;
105
106    fn index(&self, index: LookupPattern) -> &Self::Output {
107        match index {
108            LookupPattern::Xor => &self.xor,
109            LookupPattern::Lookup => &self.lookup,
110            LookupPattern::RangeCheck => &self.range_check,
111            LookupPattern::ForeignFieldMul => &self.ffmul,
112        }
113    }
114}
115
116impl<T> core::ops::IndexMut<LookupPattern> for LookupSelectors<T> {
117    fn index_mut(&mut self, index: LookupPattern) -> &mut Self::Output {
118        match index {
119            LookupPattern::Xor => &mut self.xor,
120            LookupPattern::Lookup => &mut self.lookup,
121            LookupPattern::RangeCheck => &mut self.range_check,
122            LookupPattern::ForeignFieldMul => &mut self.ffmul,
123        }
124    }
125}
126
127impl<T> LookupSelectors<T> {
128    pub fn map<U, F: Fn(T) -> U>(self, f: F) -> LookupSelectors<U> {
129        let LookupSelectors {
130            xor,
131            lookup,
132            range_check,
133            ffmul,
134        } = self;
135        // This closure isn't really redundant -- it shields the parameter from a copy -- but
136        // clippy isn't smart enough to figure that out..
137        #[allow(clippy::redundant_closure)]
138        let f = |x| f(x);
139        LookupSelectors {
140            xor: xor.map(f),
141            lookup: lookup.map(f),
142            range_check: range_check.map(f),
143            ffmul: ffmul.map(f),
144        }
145    }
146
147    pub fn as_ref(&self) -> LookupSelectors<&T> {
148        LookupSelectors {
149            xor: self.xor.as_ref(),
150            lookup: self.lookup.as_ref(),
151            range_check: self.range_check.as_ref(),
152            ffmul: self.ffmul.as_ref(),
153        }
154    }
155}
156
157#[serde_as]
158#[derive(Clone, Serialize, Deserialize, Debug)]
159pub struct LookupConstraintSystem<F: FftField> {
160    /// Lookup tables
161    #[serde_as(as = "Vec<o1_utils::serialization::SerdeAs>")]
162    pub lookup_table: Vec<DP<F>>,
163    #[serde_as(as = "Vec<o1_utils::serialization::SerdeAs>")]
164    pub lookup_table8: Vec<E<F, D<F>>>,
165
166    /// Table IDs for the lookup values.
167    /// This may be `None` if all lookups originate from table 0.
168    #[serde_as(as = "Option<o1_utils::serialization::SerdeAs>")]
169    pub table_ids: Option<DP<F>>,
170    #[serde_as(as = "Option<o1_utils::serialization::SerdeAs>")]
171    pub table_ids8: Option<E<F, D<F>>>,
172
173    /// Lookup selectors:
174    /// For each kind of lookup-pattern, we have a selector that's
175    /// 1 at the rows where that pattern should be enforced, and 0 at
176    /// all other rows.
177    #[serde_as(as = "LookupSelectorsSerdeAs<F>")]
178    pub lookup_selectors: LookupSelectors<E<F, D<F>>>,
179
180    /// An optional runtime table selector. It is 0 everywhere,
181    /// except at the rows where the runtime tables apply.
182    #[serde_as(as = "Option<o1_utils::serialization::SerdeAs>")]
183    pub runtime_selector: Option<E<F, D<F>>>,
184
185    /// Optional runtime tables, listed as tuples `(length, id)`.
186    pub runtime_tables: Option<Vec<RuntimeTableSpec>>,
187
188    /// The offset of the runtime table within the concatenated table
189    pub runtime_table_offset: Option<usize>,
190
191    /// Configuration for the lookup constraint.
192    #[serde(bound = "LookupConfiguration<F>: Serialize + DeserializeOwned")]
193    pub configuration: LookupConfiguration<F>,
194}
195
196impl<F: PrimeField> LookupConstraintSystem<F> {
197    /// Create the `LookupConstraintSystem`.
198    ///
199    /// # Errors
200    ///
201    /// Will give error if inputs validation do not match.
202    pub fn create(
203        gates: &[CircuitGate<F>],
204        fixed_lookup_tables: Vec<LookupTable<F>>,
205        runtime_tables: Option<Vec<RuntimeTableCfg<F>>>,
206        domain: &EvaluationDomains<F>,
207        zk_rows: usize,
208    ) -> Result<Option<Self>, LookupError> {
209        //~ 1. If no lookup is used in the circuit, do not create a lookup index
210        match LookupInfo::create_from_gates(gates, runtime_tables.is_some()) {
211            None => Ok(None),
212            Some(lookup_info) => {
213                let d1_size = domain.d1.size();
214
215                // The maximum number of entries that can be provided across all tables.
216                // Since we do not assert the lookup constraint on the final `zk_rows` rows, and
217                // because the row before is used to assert that the lookup argument's final
218                // product is 1, we cannot use those rows to store any values.
219                let max_num_entries = d1_size - zk_rows - 1;
220
221                //~ 2. Get the lookup selectors and lookup tables that are specified implicitly
222                // by the lookup gates.
223                let (lookup_selectors, gate_lookup_tables) =
224                    lookup_info.selector_polynomials_and_tables(domain, gates);
225
226                // If there is a gate using a lookup table, this table must not be added
227                // explicitly to the constraint system.
228                let fixed_gate_joint_ids: Vec<i32> = fixed_lookup_tables
229                    .iter()
230                    .map(|lt| lt.id)
231                    .chain(gate_lookup_tables.iter().map(|lt| lt.id))
232                    .collect();
233                check_id_duplicates(
234                    &fixed_gate_joint_ids,
235                    "duplicates between fixed given and fixed from-gate tables",
236                )?;
237
238                //~ 3. Concatenate explicit runtime lookup tables with the ones (implicitly) used by gates.
239                let mut lookup_tables: Vec<_> = fixed_lookup_tables
240                    .into_iter()
241                    .chain(gate_lookup_tables)
242                    .collect();
243
244                let mut has_table_id_0 = false;
245
246                // if we are using runtime tables
247                let (runtime_table_offset, runtime_selector) =
248                    if let Some(runtime_tables) = &runtime_tables {
249                        // Check duplicates in runtime table ids
250                        let runtime_tables_ids: Vec<i32> =
251                            runtime_tables.iter().map(|rt| rt.id).collect();
252                        check_id_duplicates(&runtime_tables_ids, "runtime table duplicates")?;
253                        // Runtime table IDs /may/ collide with lookup
254                        // table IDs, so we intentionally do not perform another potential check.
255
256                        // save the offset of the end of the table
257                        let mut runtime_table_offset = 0;
258                        for table in &lookup_tables {
259                            runtime_table_offset += table.len();
260                        }
261
262                        // compute the length of the runtime table
263                        let mut runtime_len = 0;
264                        for t in runtime_tables {
265                            runtime_len += t.len();
266                        }
267
268                        // compute the runtime selector
269                        let runtime_selector = {
270                            let mut evals = Vec::with_capacity(d1_size);
271
272                            // it's 1 everywhere, except at the entries where
273                            // the runtime table applies
274                            evals.extend(core::iter::repeat_n(F::one(), runtime_table_offset));
275                            evals.extend(core::iter::repeat_n(F::zero(), runtime_len));
276                            evals.extend(core::iter::repeat_n(
277                                F::one(),
278                                d1_size - runtime_table_offset - runtime_len,
279                            ));
280
281                            // although the last zk_rows are fine
282                            for e in evals.iter_mut().rev().take(zk_rows) {
283                                *e = F::zero();
284                            }
285
286                            E::<F, D<F>>::from_vec_and_domain(evals, domain.d1)
287                                .interpolate()
288                                .evaluate_over_domain(domain.d8)
289                        };
290
291                        // create fixed tables for indexing the runtime tables
292                        for runtime_table in runtime_tables {
293                            let (id, first_column) =
294                                (runtime_table.id, runtime_table.first_column.clone());
295
296                            // record if table ID 0 is used in one of the runtime tables
297                            // note: the check later will still force you to have a fixed table with ID 0
298                            if id == 0 {
299                                has_table_id_0 = true;
300                            }
301
302                            // important: we still need a placeholder column to make sure that
303                            // if all other tables have a single column
304                            // we don't use the second table as table ID column.
305                            let placeholders = vec![F::zero(); first_column.len()];
306                            let data = vec![first_column, placeholders];
307                            let table = LookupTable { id, data };
308                            lookup_tables.push(table);
309                        }
310
311                        (Some(runtime_table_offset), Some(runtime_selector))
312                    } else {
313                        (None, None)
314                    };
315
316                //~ 4. Get the highest number of columns `max_table_width`
317                //~    that a lookup table can have.
318                let max_table_width = lookup_tables
319                    .iter()
320                    .map(|table| table.width())
321                    .max()
322                    .unwrap_or(0);
323
324                let max_table_width = core::cmp::max(
325                    max_table_width,
326                    lookup_info.max_joint_size.try_into().unwrap(),
327                );
328
329                //~ 5. Create the concatenated table of all the fixed lookup tables.
330                //~    It will be of height the size of the domain,
331                //~    and of width the maximum width of any of the lookup tables.
332                //~    In addition, create an additional column to store all the tables' table IDs.
333                //~
334                //~    For example, if you have a table with ID 0
335                //~
336                //~    |       |       |       |
337                //~    | :---: | :---: | :---: |
338                //~    |   1   |   2   |   3   |
339                //~    |   5   |   6   |   7   |
340                //~    |   0   |   0   |   0   |
341                //~
342                //~    and another table with ID 1
343                //~
344                //~    |       |       |
345                //~    | :---: | :---: |
346                //~    |   8   |   9   |
347                //~
348                //~    the concatenated table in a domain of size 5 looks like this:
349                //~
350                //~    |       |       |       |
351                //~    | :---: | :---: | :---: |
352                //~    |   1   |   2   |   3   |
353                //~    |   5   |   6   |   7   |
354                //~    |   0   |   0   |   0   |
355                //~    |   8   |   9   |   0   |
356                //~    |   0   |   0   |   0   |
357                //~
358                //~    with the table id vector:
359                //~
360                //~    | table id |
361                //~    | :------: |
362                //~    |    0     |
363                //~    |    0     |
364                //~    |    0     |
365                //~    |    1     |
366                //~    |    0     |
367                //~
368                //~    To do this, for each table:
369                //~
370                let mut lookup_table = vec![Vec::with_capacity(d1_size); max_table_width];
371                let mut table_ids: Vec<F> = Vec::with_capacity(d1_size);
372
373                let mut non_zero_table_id = false;
374                let mut has_table_id_0_with_zero_entry = false;
375
376                for table in &lookup_tables {
377                    let table_len = table.len();
378
379                    if table.id == 0 {
380                        has_table_id_0 = true;
381                        if table.has_zero_entry() {
382                            has_table_id_0_with_zero_entry = true;
383                        }
384                    } else {
385                        non_zero_table_id = true;
386                    }
387
388                    //~~ * Update the corresponding entries in a table id vector (of size the domain as well)
389                    //~    with the table ID of the table.
390                    let table_id: F = i32_to_field(table.id);
391                    table_ids.extend(core::iter::repeat_n(table_id, table_len));
392
393                    //~~ * Copy the entries from the table to new rows in the corresponding columns of the concatenated table.
394                    for (i, col) in table.data.iter().enumerate() {
395                        // See GH issue: https://github.com/MinaProtocol/mina/issues/14097
396                        if col.len() != table_len {
397                            return Err(LookupError::InconsistentTableLength);
398                        }
399                        lookup_table[i].extend(col);
400                    }
401
402                    //~~ * Fill in any unused columns with 0 (to match the dummy value)
403                    for lookup_table in lookup_table.iter_mut().skip(table.width()) {
404                        lookup_table.extend(core::iter::repeat_n(F::zero(), table_len));
405                    }
406                }
407
408                // If a table has ID 0, then it must have a zero entry.
409                // This is for the dummy lookups to work.
410                if has_table_id_0 && !has_table_id_0_with_zero_entry {
411                    return Err(LookupError::TableIDZeroMustHaveZeroEntry);
412                }
413
414                // Note: we use `>=` here to leave space for the dummy value.
415                if lookup_table[0].len() >= max_num_entries {
416                    return Err(LookupError::LookupTableTooLong {
417                        length: lookup_table[0].len(),
418                        maximum_allowed: max_num_entries - 1,
419                    });
420                }
421
422                //~ 6. Pad the end of the concatened table with the dummy value.
423                //     By padding with 0, we constraint the table with ID 0 to
424                //     have a zero entry.
425                //     This is for the rows which do not have a lookup selector,
426                //     see ../../../../book/src/kimchi/lookup.md.
427                //     The zero entry row is contained in the built-in XOR table.
428                //     An error is raised when creating the CS if a user-defined
429                //     table is defined with ID 0 without a row contain zeroes.
430                //     If no such table is used, we artificially add a dummy
431                //     table with ID 0 and a row containing only zeroes.
432                lookup_table.iter_mut().for_each(|col| {
433                    col.extend(core::iter::repeat_n(F::zero(), max_num_entries - col.len()))
434                });
435
436                //~ 7. Pad the end of the table id vector with 0s.
437                table_ids.extend(core::iter::repeat_n(
438                    F::zero(),
439                    max_num_entries - table_ids.len(),
440                ));
441
442                //~ 8. pre-compute polynomial and evaluation form for the look up tables
443                let mut lookup_table_polys: Vec<DP<F>> = vec![];
444                let mut lookup_table8: Vec<E<F, D<F>>> = vec![];
445                for col in lookup_table {
446                    let poly = E::<F, D<F>>::from_vec_and_domain(col, domain.d1).interpolate();
447                    let eval = poly.evaluate_over_domain_by_ref(domain.d8);
448                    lookup_table_polys.push(poly);
449                    lookup_table8.push(eval);
450                }
451
452                //~ 9. pre-compute polynomial and evaluation form for the table IDs,
453                //~    only if a table with an ID different from zero was used.
454                let (table_ids, table_ids8) = if non_zero_table_id {
455                    let table_ids: DP<F> =
456                        E::<F, D<F>>::from_vec_and_domain(table_ids, domain.d1).interpolate();
457                    let table_ids8: E<F, D<F>> = table_ids.evaluate_over_domain_by_ref(domain.d8);
458                    (Some(table_ids), Some(table_ids8))
459                } else {
460                    (None, None)
461                };
462
463                // store only the length of custom runtime tables in the index
464                let runtime_tables =
465                    runtime_tables.map(|rt| rt.into_iter().map(Into::into).collect());
466
467                let configuration = LookupConfiguration::new(lookup_info);
468
469                Ok(Some(Self {
470                    lookup_selectors,
471                    lookup_table8,
472                    lookup_table: lookup_table_polys,
473                    table_ids,
474                    table_ids8,
475                    runtime_selector,
476                    runtime_tables,
477                    runtime_table_offset,
478                    configuration,
479                }))
480            }
481        }
482    }
483}
484
485// Checks whether an iterator contains any duplicates, and if yes, raises
486// a corresponding LookupTableIdCollision error.
487fn check_id_duplicates(ids: &[i32], msg: &str) -> Result<(), LookupError> {
488    let mut set = crate::collections::HashSet::new();
489    let mut dups = Vec::new();
490    for id in ids {
491        if !set.insert(*id) {
492            dups.push(*id);
493        }
494    }
495
496    match dups.as_slice() {
497        [] => Ok(()),
498        _ => Err(LookupError::LookupTableIdCollision {
499            collision_type: format!("{}: {:?}", msg, dups),
500        }),
501    }
502}
503
504#[cfg(all(test, feature = "std"))]
505mod tests {
506
507    use super::{check_id_duplicates, LookupError, LookupTable, RuntimeTableCfg};
508    use crate::{
509        circuits::{
510            constraints::ConstraintSystem, gate::CircuitGate, lookup::tables::xor,
511            polynomials::range_check,
512        },
513        error::SetupError,
514    };
515    use mina_curves::pasta::Fp;
516
517    #[test]
518    fn test_check_id_duplicates() {
519        // no duplicates
520        let ids = &[1, 2, 3];
521        assert!(
522            check_id_duplicates(ids, "test no duplicates").is_ok(),
523            "check_id_duplicates should not find duplicates when there are none"
524        );
525
526        let msg = "test-with-dups";
527
528        let ids = &[1, 2, 3, 2, 4, 1];
529
530        let error = match check_id_duplicates(ids, msg) {
531            Err(LookupError::LookupTableIdCollision { collision_type }) => collision_type,
532            _ => panic!("check_id_duplicates should find duplicates when they exist"),
533        };
534
535        assert_eq!(error, format!("{}: [2, 1]", msg));
536    }
537
538    #[test]
539    fn test_colliding_table_ids() {
540        let (_, gates) = CircuitGate::<Fp>::create_multi_range_check(0);
541        let collision_id: i32 = 5;
542
543        let cs = ConstraintSystem::<Fp>::create(gates.clone())
544            .lookup(vec![range_check::gadget::lookup_table()])
545            .build();
546
547        assert!(
548            matches!(
549                cs,
550                Err(SetupError::LookupCreation(
551                    LookupError::LookupTableIdCollision { .. }
552                ))
553            ),
554            "LookupConstraintSystem::create(...) must fail due to range table passed twice"
555        );
556
557        let cs = ConstraintSystem::<Fp>::create(gates.clone())
558            .lookup(vec![xor::xor_table()])
559            .build();
560
561        assert!(
562            cs.is_ok(),
563            "LookupConstraintSystem::create(...) must succeed, no duplicates exist"
564        );
565
566        let cs = ConstraintSystem::<Fp>::create(gates.clone())
567            .lookup(vec![
568                LookupTable {
569                    id: collision_id,
570                    data: vec![vec![From::from(0); 16]],
571                },
572                LookupTable {
573                    id: collision_id,
574                    data: vec![vec![From::from(1); 16]],
575                },
576            ])
577            .build();
578
579        assert!(
580            matches!(
581                cs,
582                Err(SetupError::LookupCreation(
583                    LookupError::LookupTableIdCollision { .. }
584                ))
585            ),
586            "LookupConstraintSystem::create(...) must fail, collision in fixed ids"
587        );
588
589        let cs = ConstraintSystem::<Fp>::create(gates.clone())
590            .runtime(Some(vec![
591                RuntimeTableCfg {
592                    id: collision_id,
593                    first_column: vec![From::from(0); 16],
594                },
595                RuntimeTableCfg {
596                    id: collision_id,
597                    first_column: vec![From::from(1); 16],
598                },
599            ]))
600            .build();
601
602        assert!(
603            matches!(
604                cs,
605                Err(SetupError::LookupCreation(
606                    LookupError::LookupTableIdCollision { .. }
607                ))
608            ),
609            "LookupConstraintSystem::create(...) must fail, collision in runtime ids"
610        );
611
612        let cs = ConstraintSystem::<Fp>::create(gates.clone())
613            .lookup(vec![LookupTable {
614                id: collision_id,
615                data: vec![vec![From::from(0); 16]],
616            }])
617            .runtime(Some(vec![RuntimeTableCfg {
618                id: collision_id,
619                first_column: vec![From::from(1); 16],
620            }]))
621            .build();
622
623        assert!(
624            cs.is_ok(),
625            "LookupConstraintSystem::create(...) must not fail when there is a collision between runtime and lookup ids"
626        );
627    }
628}