Resurrect lookup PR1263 [do not merge]

book/src/specs/kimchi.md

@@ -1648,8 +1648,8 @@ If lookup is used, the following values are added to the common index:
 To create the index, follow these steps:
 
 1. If no lookup is used in the circuit, do not create a lookup index
-2. Get the lookup selectors and lookup tables (TODO: how?)
-3. Concatenate runtime lookup tables with the ones used by gates
+2. Get the lookup selectors and lookup tables that are specified implicitly
+3. Concatenate explicit runtime lookup tables with the ones (implicitly) used by gates.
 4. Get the highest number of columns `max_table_width`
    that a lookup table can have.
 5. Create the concatenated table of all the fixed lookup tables.

kimchi/src/circuits/constraints.rs

@@ -683,7 +683,9 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
     /// If not invoked, it is `vec![]` by default.
     ///
     /// **Warning:** you have to make sure that the IDs of the lookup tables,
-    /// are unique and  not colliding with IDs of built-in lookup tables
+    /// are unique and not colliding with IDs of built-in lookup tables, otherwise
+    /// the error will be raised.
+    ///
     /// (see [crate::circuits::lookup::tables]).
     pub fn lookup(mut self, lookup_tables: Vec<LookupTable<F>>) -> Self {
         self.lookup_tables = lookup_tables;
@@ -693,8 +695,10 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
     /// Set up the runtime tables.
     /// If not invoked, it is `None` by default.
     ///
-    /// **Warning:** you have to make sure that the IDs of the runtime lookup tables,
-    /// are unique and not colliding with IDs of built-in lookup tables
+    /// **Warning:** you have to make sure that the IDs of the runtime
+    /// lookup tables, are unique, i.e. not colliding internaly (with other runtime tables),
+    /// otherwise error will be raised.
+    ///
     /// (see [crate::circuits::lookup::tables]).
     pub fn runtime(mut self, runtime_tables: Option<Vec<RuntimeTableCfg<F>>>) -> Self {
         self.runtime_tables = runtime_tables;
@@ -739,16 +743,12 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
             let mut has_table_with_id_0 = false;
             let mut lookup_domain_size: usize = lookup_tables
                 .iter()
-                .map(|LookupTable { id, data }| {
+                .map(|lt| {
                     // See below for the reason
-                    if *id == 0_i32 {
+                    if lt.id() == 0_i32 {
                         has_table_with_id_0 = true
                     }
-                    if data.is_empty() {
-                        0
-                    } else {
-                        data[0].len()
-                    }
+                    lt.len()
                 })
                 .sum();
             // After that on the runtime tables
@@ -872,7 +872,7 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
             &domain,
             zk_rows as usize,
         )
-        .map_err(|e| SetupError::ConstraintSystem(e.to_string()))?;
+        .map_err(SetupError::LookupCreation)?;
 
         let sid = shifts.map[0].clone();
 

kimchi/src/circuits/lookup/index.rs

@@ -1,10 +1,10 @@
-use super::runtime_tables::{RuntimeTableCfg, RuntimeTableSpec};
 use crate::circuits::{
     domains::EvaluationDomains,
     gate::CircuitGate,
     lookup::{
         constraints::LookupConfiguration,
         lookups::{LookupInfo, LookupPattern},
+        runtime_tables::{RuntimeTableCfg, RuntimeTableSpec},
         tables::LookupTable,
     },
 };
@@ -21,17 +21,15 @@ use std::iter;
 use thiserror::Error;
 
 /// Represents an error found when computing the lookup constraint system
-#[derive(Debug, Error)]
+#[derive(Debug, Error, Clone)]
 pub enum LookupError {
-    #[error("One of the lookup tables has columns of different lengths")]
-    InconsistentTableLength,
     #[error("The combined lookup table is larger than allowed by the domain size. Observed: {length}, expected: {maximum_allowed}")]
     LookupTableTooLong {
         length: usize,
         maximum_allowed: usize,
     },
-    #[error("The table with id 0 must have an entry of all zeros")]
-    TableIDZeroMustHaveZeroEntry,
+    #[error("Cannot create a combined table since ids for sub-tables are colliding. The collision type is: {collision_type}")]
+    LookupTableIdCollision { collision_type: String },
 }
 
 /// Lookup selectors
@@ -200,7 +198,7 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
     /// Will give error if inputs validation do not match.
     pub fn create(
         gates: &[CircuitGate<F>],
-        lookup_tables: Vec<LookupTable<F>>,
+        fixed_lookup_tables: Vec<LookupTable<F>>,
         runtime_tables: Option<Vec<RuntimeTableCfg<F>>>,
         domain: &EvaluationDomains<F>,
         zk_rows: usize,
@@ -217,21 +215,60 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
                 // product is 1, we cannot use those rows to store any values.
                 let max_num_entries = d1_size - zk_rows - 1;
 
-                //~ 2. Get the lookup selectors and lookup tables (TODO: how?)
+                //~ 2. Get the lookup selectors and lookup tables that are specified implicitly
+                // by the lookup gates.
                 let (lookup_selectors, gate_lookup_tables) =
                     lookup_info.selector_polynomials_and_tables(domain, gates);
 
-                //~ 3. Concatenate runtime lookup tables with the ones used by gates
-                let mut lookup_tables: Vec<_> = gate_lookup_tables
+                // Checks whether an iterator contains any duplicates, and if yes, raises
+                // a corresponding LookupTableIdCollision error.
+                fn check_id_duplicates<'a, I: Iterator<Item = &'a i32>>(
+                    iter: I,
+                    msg: &str,
+                ) -> Result<(), LookupError> {
+                    use itertools::Itertools;
+                    match iter.duplicates().collect::<Vec<_>>() {
+                        dups if !dups.is_empty() => Err(LookupError::LookupTableIdCollision {
+                            collision_type: format!("{}: {:?}", msg, dups).to_string(),
+                        }),
+                        _ => Ok(()),
+                    }
+                }
+
+                // If there is a gate using a lookup table, this table must not be added
+                // explicitly to the constraint system.
+                let fixed_gate_joint_ids: Vec<i32> = fixed_lookup_tables
+                    .iter()
+                    .map(|lt| lt.id())
+                    .chain(gate_lookup_tables.iter().map(|lt| lt.id()))
+                    .collect();
+                check_id_duplicates(
+                    fixed_gate_joint_ids.iter(),
+                    "duplicates between fixed given and fixed from-gate tables",
+                )?;
+
+                //~ 3. Concatenate explicit runtime lookup tables with the ones (implicitly) used by gates.
+                let mut lookup_tables: Vec<LookupTable<_>> = fixed_lookup_tables
                     .into_iter()
-                    .chain(lookup_tables)
+                    .chain(gate_lookup_tables)
                     .collect();
 
-                let mut has_table_id_0 = false;
+                let fixed_lookup_tables_ids: Vec<i32> =
+                    lookup_tables.iter().map(|lt| lt.id()).collect();
+                check_id_duplicates(
+                    fixed_lookup_tables_ids.iter(),
+                    "fixed lookup table duplicates",
+                )?;
 
                 // if we are using runtime tables
                 let (runtime_table_offset, runtime_selector) =
                     if let Some(runtime_tables) = &runtime_tables {
+                        let runtime_tables_ids: Vec<i32> =
+                            runtime_tables.iter().map(|rt| rt.id).collect();
+                        check_id_duplicates(runtime_tables_ids.iter(), "runtime table duplicates")?;
+                        // Runtime table IDs may collide with lookup
+                        // table IDs, so we intentionally do not perform another potential check.
+
                         // save the offset of the end of the table
                         let mut runtime_table_offset = 0;
                         for table in &lookup_tables {
@@ -272,18 +309,15 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
                             let (id, first_column) =
                                 (runtime_table.id, runtime_table.first_column.clone());
 
-                            // record if table ID 0 is used in one of the runtime tables
-                            // note: the check later will still force you to have a fixed table with ID 0
-                            if id == 0 {
-                                has_table_id_0 = true;
-                            }
-
                             // important: we still need a placeholder column to make sure that
                             // if all other tables have a single column
                             // we don't use the second table as table ID column.
                             let placeholders = vec![F::zero(); first_column.len()];
                             let data = vec![first_column, placeholders];
-                            let table = LookupTable { id, data };
+                            // TODO Check it does not fail actually. Maybe this should throw a different error.
+                            let table = LookupTable::create(id, data)
+                                .expect("Runtime table creation must succeed");
+
                             lookup_tables.push(table);
                         }
 
@@ -345,31 +379,21 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
                 let mut table_ids: Vec<F> = Vec::with_capacity(d1_size);
 
                 let mut non_zero_table_id = false;
-                let mut has_table_id_0_with_zero_entry = false;
 
                 for table in &lookup_tables {
                     let table_len = table.len();
 
-                    if table.id == 0 {
-                        has_table_id_0 = true;
-                        if table.has_zero_entry() {
-                            has_table_id_0_with_zero_entry = true;
-                        }
-                    } else {
+                    if table.id() != 0 {
                         non_zero_table_id = true;
                     }
 
                     //~~ * Update the corresponding entries in a table id vector (of size the domain as well)
                     //~    with the table ID of the table.
-                    let table_id: F = i32_to_field(table.id);
+                    let table_id: F = i32_to_field(table.id());
                     table_ids.extend(repeat_n(table_id, table_len));
 
                     //~~ * Copy the entries from the table to new rows in the corresponding columns of the concatenated table.
-                    for (i, col) in table.data.iter().enumerate() {
-                        // See GH issue: https://github.com/MinaProtocol/mina/issues/14097
-                        if col.len() != table_len {
-                            return Err(LookupError::InconsistentTableLength);
-                        }
+                    for (i, col) in table.data().iter().enumerate() {
                         lookup_table[i].extend(col);
                     }
 
@@ -379,12 +403,6 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
                     }
                 }
 
-                // If a table has ID 0, then it must have a zero entry.
-                // This is for the dummy lookups to work.
-                if has_table_id_0 && !has_table_id_0_with_zero_entry {
-                    return Err(LookupError::TableIDZeroMustHaveZeroEntry);
-                }
-
                 // Note: we use `>=` here to leave space for the dummy value.
                 if lookup_table[0].len() >= max_num_entries {
                     return Err(LookupError::LookupTableTooLong {
@@ -420,6 +438,8 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
                     lookup_table8.push(eval);
                 }
 
+                // @volhovm: Do we need to enforce that there is at least one table
+                // with id 0?
                 //~ 9. pre-compute polynomial and evaluation form for the table IDs,
                 //~    only if a table with an ID different from zero was used.
                 let (table_ids, table_ids8) = if non_zero_table_id {
@@ -452,3 +472,100 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
         }
     }
 }
+
+#[cfg(test)]
+mod tests {
+
+    use super::{LookupError, LookupTable, RuntimeTableCfg};
+    use crate::{
+        circuits::constraints::ConstraintSystem, circuits::gate::CircuitGate,
+        circuits::lookup::tables::xor, circuits::polynomials::range_check, error::SetupError,
+    };
+    use mina_curves::pasta::Fp;
+
+    #[test]
+    fn test_colliding_table_ids() {
+        let (_, gates) = CircuitGate::<Fp>::create_multi_range_check(0);
+        let collision_id: i32 = 5;
+
+        let cs = ConstraintSystem::<Fp>::create(gates.clone())
+            .lookup(vec![range_check::gadget::lookup_table()])
+            .build();
+
+        assert!(
+            matches!(
+                cs,
+                Err(SetupError::LookupCreation(
+                    LookupError::LookupTableIdCollision { .. }
+                ))
+            ),
+            "LookupConstraintSystem::create(...) must fail due to range table passed twice"
+        );
+
+        let cs = ConstraintSystem::<Fp>::create(gates.clone())
+            .lookup(vec![xor::xor_table()])
+            .build();
+
+        assert!(
+            cs.is_ok(),
+            "LookupConstraintSystem::create(...) must succeed, no duplicates exist"
+        );
+
+        let cs = ConstraintSystem::<Fp>::create(gates.clone())
+            .lookup(vec![
+                LookupTable::create(collision_id, vec![vec![From::from(0); 16]]).unwrap(),
+                LookupTable::create(collision_id, vec![vec![From::from(1); 16]]).unwrap(),
+            ])
+            .build();
+
+        assert!(
+            matches!(
+                cs,
+                Err(SetupError::LookupCreation(
+                    LookupError::LookupTableIdCollision { .. }
+                ))
+            ),
+            "LookupConstraintSystem::create(...) must fail, collision in fixed ids"
+        );
+
+        let cs = ConstraintSystem::<Fp>::create(gates.clone())
+            .runtime(Some(vec![
+                RuntimeTableCfg {
+                    id: collision_id,
+                    first_column: vec![From::from(0); 16],
+                },
+                RuntimeTableCfg {
+                    id: collision_id,
+                    first_column: vec![From::from(1); 16],
+                },
+            ]))
+            .build();
+
+        assert!(
+            matches!(
+                cs,
+                Err(SetupError::LookupCreation(
+                    LookupError::LookupTableIdCollision { .. }
+                ))
+            ),
+            "LookupConstraintSystem::create(...) must fail, collision in runtime ids"
+        );
+
+        let cs = ConstraintSystem::<Fp>::create(gates.clone())
+            .lookup(vec![LookupTable::create(
+                collision_id,
+                vec![vec![From::from(0); 16]],
+            )
+            .unwrap()])
+            .runtime(Some(vec![RuntimeTableCfg {
+                id: collision_id,
+                first_column: vec![From::from(1); 16],
+            }]))
+            .build();
+
+        assert!(
+            cs.is_ok(),
+            "LookupConstraintSystem::create(...) must not fail when there is a collision between runtime and lookup ids"
+        );
+    }
+}

kimchi/src/circuits/lookup/lookups.rs

@@ -222,7 +222,7 @@ impl LookupInfo {
         };
 
         // TODO: is take(n) useful here? I don't see why we need this
-        for (i, gate) in gates.iter().enumerate().take(n) {
+        for (i, gate) in gates.iter().take(n).enumerate() {
             let typ = gate.typ;
 
             if let Some(lookup_pattern) = LookupPattern::from_gate(typ, CurrOrNext::Curr) {

kimchi/src/circuits/lookup/runtime_tables.rs

@@ -18,14 +18,17 @@ pub struct RuntimeTableSpec {
     pub len: usize,
 }
 
+/// A configuration of the runtime table as known at setup time.
+///
 /// Use this type at setup time, to list all the runtime tables.
 ///
 /// Note: care must be taken as table IDs can collide with IDs of other types of lookup tables.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct RuntimeTableCfg<F> {
     /// The table ID.
     pub id: i32,
-    /// The content of the first column of the runtime table.
+    /// The content of the first column of the runtime table, i.e.
+    /// keys when a table is viewed as a (k,v) array.
     pub first_column: Vec<F>,
 }
 
@@ -56,12 +59,13 @@ impl<F> From<RuntimeTableCfg<F>> for RuntimeTableSpec {
 }
 
 /// A runtime table. Runtime tables must match the configuration
-/// that was specified in [`RuntimeTableCfg`].
+/// specified in [`RuntimeTableCfg`].
 #[derive(Debug, Clone)]
 pub struct RuntimeTable<F> {
     /// The table id.
     pub id: i32,
-    /// A single column.
+    /// A single column. Represents runtime table values, where
+    /// ['RuntimeTableCfg'] defines compile-time keys.
     pub data: Vec<F>,
 }