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