From 442a7842fdc546b6877eb22e2d7e001c54b9cb0a Mon Sep 17 00:00:00 2001 From: Mikhail Volkhov Date: Thu, 12 Oct 2023 12:56:28 +0100 Subject: [PATCH] Move lookup table consistency checks into LookupTable#create() --- kimchi/src/circuits/lookup/index.rs | 71 +------------------- kimchi/src/circuits/lookup/tables/mod.rs | 84 +++++++++++++++++++++++- 2 files changed, 85 insertions(+), 70 deletions(-) diff --git a/kimchi/src/circuits/lookup/index.rs b/kimchi/src/circuits/lookup/index.rs index d1f24d3dbf..592fd0db48 100644 --- a/kimchi/src/circuits/lookup/index.rs +++ b/kimchi/src/circuits/lookup/index.rs @@ -23,15 +23,11 @@ use thiserror::Error; /// Represents an error found when computing the lookup constraint system #[derive(Debug, Error)] 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, } /// Lookup selectors @@ -227,8 +223,6 @@ impl LookupConstraintSystem { .chain(lookup_tables) .collect(); - let mut has_table_id_0 = false; - // if we are using runtime tables let (runtime_table_offset, runtime_selector) = if let Some(runtime_tables) = &runtime_tables { @@ -272,11 +266,8 @@ impl LookupConstraintSystem { 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; - } + // @volhovm: Do we need to enforce that there is at least one table + // with id 0? // important: we still need a placeholder column to make sure that // if all other tables have a single column @@ -345,17 +336,11 @@ impl LookupConstraintSystem { let mut table_ids: Vec = 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; } @@ -366,10 +351,6 @@ impl LookupConstraintSystem { //~~ * 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); - } lookup_table[i].extend(col); } @@ -379,12 +360,6 @@ impl LookupConstraintSystem { } } - // 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 { @@ -443,43 +418,3 @@ impl LookupConstraintSystem { } } } - -#[cfg(test)] -mod tests { - - use super::*; - use crate::circuits::{ - gate::{CircuitGate, GateType}, - wires::Wire, - }; - use mina_curves::pasta::Fp; - - #[test] - fn test_zero_table_zero_row() { - let lookup_r: u64 = 32; - let num_lookups: usize = 16; - if let Ok(domain) = EvaluationDomains::::create(2 * lookup_r as usize) { - // Table column that /does not/ contain zeros - let lookup_table_values_1: Vec<_> = (1..lookup_r+1).map(From::from).collect(); - // Another table column that /does/ contain zeros. - // Jointly two tables /do not/ have a full zero now. - let lookup_table_values_2: Vec<_> = (0..lookup_r).map(From::from).collect(); - - let lookup_tables: Vec> = vec![LookupTable { - id: 0, - data: vec![lookup_table_values_1, lookup_table_values_2], - }]; - - let gates: Vec> = (0..num_lookups) - .map(|i| CircuitGate::new(GateType::Lookup, Wire::for_row(i), vec![])) - .collect(); - - let res = - LookupConstraintSystem::create(gates.as_slice(), lookup_tables, None, &domain); - assert!( - matches!(res, Err(LookupError::TableIDZeroMustHaveZeroEntry)), - "LookupConstraintSystem::create(...) must fail when zero table has no zero rows" - ); - } - } -} diff --git a/kimchi/src/circuits/lookup/tables/mod.rs b/kimchi/src/circuits/lookup/tables/mod.rs index d57d36a828..845107bcd1 100644 --- a/kimchi/src/circuits/lookup/tables/mod.rs +++ b/kimchi/src/circuits/lookup/tables/mod.rs @@ -1,6 +1,7 @@ use ark_ff::{FftField, One, Zero}; use poly_commitment::PolyComm; use serde::{Deserialize, Serialize}; +use thiserror::Error; pub mod range_check; pub mod xor; @@ -27,12 +28,42 @@ pub struct LookupTable { pub data: Vec>, } +/// Represents inconsistency errors during table construction and composition. +#[derive(Debug, Error)] +pub enum LookupTableError { + #[error("One of the lookup tables has columns of different lengths")] + InconsistentTableLength, + #[error("The table with id 0 must have an entry of all zeros")] + TableIDZeroMustHaveZeroEntry, +} + impl LookupTable where F: FftField, { + pub fn create(id: i32, data: Vec>) -> Result{ + + let res = LookupTable {id, data}; + let table_len = res.len(); + + // All columns in the table must have same length + for col in res.data.iter() { + if col.len() != table_len { + return Err(LookupTableError::InconsistentTableLength); + } + } + + // If a table has ID 0, then it must have a zero entry. + // This is for the dummy lookups to work. + if id == 0 && !res.has_zero_entry() { + return Err(LookupTableError::TableIDZeroMustHaveZeroEntry); + } + + Ok(res) + } + /// Return true if the table has an entry (row) containing all zeros. - pub fn has_zero_entry(&self) -> bool { + fn has_zero_entry(&self) -> bool { // reminder: a table is written as a list of columns, // not as a list of row entries. for row in 0..self.len() { @@ -58,8 +89,11 @@ where self.data.len() } - /// Returns the length of the table. + /// Returns the length (height) of the table. pub fn len(&self) -> usize { + if self.is_empty() { + panic!("LookupTable#len() is called on an empty table") + } self.data[0].len() } @@ -212,3 +246,49 @@ pub mod caml { } } } + +#[cfg(test)] +mod tests { + + use super::*; + use mina_curves::pasta::Fp; + + #[test] + fn test_zero_table_zero_row() { + let lookup_r: u64 = 32; + // Table column that /does not/ contain zeros + let lookup_table_values_1: Vec<_> = (1..lookup_r+1).map(From::from).collect(); + // Another table column that /does/ contain zeros. + let lookup_table_values_2: Vec<_> = (0..lookup_r).map(From::from).collect(); + + // Jointly two columns /do not/ have a full zero now. + let table: Result,_> = + LookupTable::create( + 0, + vec![lookup_table_values_1, lookup_table_values_2]); + + assert!( + matches!(table, Err(LookupTableError::TableIDZeroMustHaveZeroEntry)), + "LookupTable::create(...) must fail when zero table has no zero rows" + ); + } + + #[test] + fn test_inconsistent_lengths() { + let lookup_r: u64 = 32; + // Two columns of different lengths + let lookup_table_values_1: Vec<_> = (0..2*lookup_r).map(From::from).collect(); + let lookup_table_values_2: Vec<_> = (0..lookup_r).map(From::from).collect(); + + let table: Result,_> = + LookupTable::create( + 0, + vec![lookup_table_values_1, lookup_table_values_2]); + + assert!( + matches!(table, Err(LookupTableError::InconsistentTableLength)), + "LookupTable::create(...) must fail when columns are not of the same length" + ); + } + +}