Skip to content

Commit

Permalink
[#14097,#14070] Move lookup table consistency checks into LookupTable…
Browse files Browse the repository at this point in the history
…#create()
  • Loading branch information
volhovm committed Oct 12, 2023
1 parent 74b5b0c commit 670bf26
Show file tree
Hide file tree
Showing 2 changed files with 85 additions and 70 deletions.
71 changes: 3 additions & 68 deletions kimchi/src/circuits/lookup/index.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -227,8 +223,6 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
.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 {
Expand Down Expand Up @@ -272,11 +266,8 @@ 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;
}
// @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
Expand Down Expand Up @@ -345,17 +336,11 @@ 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;
}

Expand All @@ -366,10 +351,6 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {

//~~ * 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);
}

Expand All @@ -379,12 +360,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 {
Expand Down Expand Up @@ -443,43 +418,3 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
}
}
}

#[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::<Fp>::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<LookupTable<Fp>> = vec![LookupTable {
id: 0,
data: vec![lookup_table_values_1, lookup_table_values_2],
}];

let gates: Vec<CircuitGate<Fp>> = (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"
);
}
}
}
84 changes: 82 additions & 2 deletions kimchi/src/circuits/lookup/tables/mod.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -27,12 +28,42 @@ pub struct LookupTable<F> {
pub data: Vec<Vec<F>>,
}

/// 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<F> LookupTable<F>
where
F: FftField,
{
pub fn create(id: i32, data: Vec<Vec<F>>) -> Result<Self,LookupTableError>{

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() {
Expand All @@ -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()
}

Expand Down Expand Up @@ -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<Fp>,_> =
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<Fp>,_> =
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"
);
}

}

0 comments on commit 670bf26

Please sign in to comment.