Skip to content

Commit

Permalink
Merge pull request #1378 from o1-labs/feature/revert-bad-par
Browse files Browse the repository at this point in the history 
Revert bad PR #1263
  • Loading branch information
@mrmr1993
mrmr1993 authored Dec 4, 2023
2 parents bde1c05 + 267105a commit 5685f41
Show file tree
Hide file tree
Showing 17 changed files with 124 additions and 350 deletions.
4 changes: 2 additions & 2 deletions book/src/specs/kimchi.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1641,8 +1641,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 that are specified implicitly
3. Concatenate explicit runtime lookup tables with the ones (implicitly) used by gates.
2. Get the lookup selectors and lookup tables (TODO: how?)
3. Concatenate runtime lookup tables with the ones 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.
Expand Down
15 changes: 13 additions & 2 deletions kimchi/src/circuits/constraints.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -736,7 +736,18 @@ impl<F: PrimeField + SquareRootField> Builder<F> {

let lookup_domain_size = {
// First we sum over the lookup table size
let mut lookup_domain_size: usize = lookup_tables.iter().map(|lt| lt.len()).sum();
let mut lookup_domain_size: usize = lookup_tables
.iter()
.map(
|LookupTable { data, id: _ }| {
if data.is_empty() {
0
} else {
data[0].len()
}
},
)
.sum();
// After that on the runtime tables
if let Some(runtime_tables) = runtime_tables.as_ref() {
for runtime_table in runtime_tables.iter() {
Expand Down Expand Up @@ -846,7 +857,7 @@ impl<F: PrimeField + SquareRootField> Builder<F> {
&domain,
zk_rows as usize,
)
.map_err(SetupError::LookupCreation)?;
.map_err(|e| SetupError::ConstraintSystem(e.to_string()))?;

let sid = shifts.map[0].clone();

Expand Down
202 changes: 38 additions & 164 deletions kimchi/src/circuits/lookup/index.rs
View file
Original file line number Diff line number Diff line change
@@ -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,
},
};
Expand All @@ -21,15 +21,17 @@ use std::iter;
use thiserror::Error;

/// Represents an error found when computing the lookup constraint system
#[derive(Debug, Error, Clone)]
#[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("Cannot create a combined table since ids for sub-tables are colliding. The collision type is: {collision_type}")]
LookupTableIdCollision { collision_type: String },
#[error("The table with id 0 must have an entry of all zeros")]
TableIDZeroMustHaveZeroEntry,
}

/// Lookup selectors
Expand Down Expand Up @@ -198,7 +200,7 @@ impl<F: PrimeField + SquareRootField> LookupConstraintSystem<F> {
/// Will give error if inputs validation do not match.
pub fn create(
gates: &[CircuitGate<F>],
fixed_lookup_tables: Vec<LookupTable<F>>,
lookup_tables: Vec<LookupTable<F>>,
runtime_tables: Option<Vec<RuntimeTableCfg<F>>>,
domain: &EvaluationDomains<F>,
zk_rows: usize,
Expand All @@ -215,64 +217,21 @@ 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 that are specified implicitly
// by the lookup gates.
//~ 2. Get the lookup selectors and lookup tables (TODO: how?)
let (lookup_selectors, gate_lookup_tables) =
lookup_info.selector_polynomials_and_tables(domain, gates);

// 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
//~ 3. Concatenate runtime lookup tables with the ones used by gates
let mut lookup_tables: Vec<_> = gate_lookup_tables
.into_iter()
.chain(gate_lookup_tables)
.chain(lookup_tables)
.collect();

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",
)?;
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 {
let runtime_tables_ids: Vec<i32> =
runtime_tables.iter().map(|rt| rt.id).collect();
check_id_duplicates(runtime_tables_ids.iter(), "runtime table duplicates")?;
check_id_duplicates(
runtime_tables_ids
.iter()
.chain(fixed_lookup_tables_ids.iter()),
"duplicates between runtime and fixed tables",
)?;

// save the offset of the end of the table
let mut runtime_table_offset = 0;
for table in &lookup_tables {
Expand Down Expand Up @@ -313,15 +272,18 @@ 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];
// 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");

let table = LookupTable { id, data };
lookup_tables.push(table);
}

Expand Down Expand Up @@ -383,21 +345,31 @@ 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 {
if table.id == 0 {
has_table_id_0 = true;
if table.has_zero_entry() {
has_table_id_0_with_zero_entry = true;
}
} else {
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() {
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 @@ -407,6 +379,12 @@ 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 All @@ -433,8 +411,6 @@ 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 {
Expand Down Expand Up @@ -467,105 +443,3 @@ 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 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!(
matches!(
cs,
Err(SetupError::LookupCreation(
LookupError::LookupTableIdCollision { .. }
))
),
"LookupConstraintSystem::create(...) must fail, collision between runtime and lookup ids"
);
}
}
2 changes: 1 addition & 1 deletion kimchi/src/circuits/lookup/lookups.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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().take(n).enumerate() {
for (i, gate) in gates.iter().enumerate().take(n) {
let typ = gate.typ;

if let Some(lookup_pattern) = LookupPattern::from_gate(typ, CurrOrNext::Curr) {
Expand Down
10 changes: 3 additions & 7 deletions kimchi/src/circuits/lookup/runtime_tables.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,17 +18,14 @@ 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, i.e.
/// keys when a table is viewed as a (k,v) array.
/// The content of the first column of the runtime table.
pub first_column: Vec<F>,
}

Expand Down Expand Up @@ -59,13 +56,12 @@ impl<F> From<RuntimeTableCfg<F>> for RuntimeTableSpec {
}

/// A runtime table. Runtime tables must match the configuration
/// specified in [`RuntimeTableCfg`].
/// that was specified in [`RuntimeTableCfg`].
#[derive(Debug, Clone)]
pub struct RuntimeTable<F> {
/// The table id.
pub id: i32,
/// A single column. Represents runtime table values, where
/// ['RuntimeTableCfg'] defines compile-time keys.
/// A single column.
pub data: Vec<F>,
}

Expand Down
Loading

0 comments on commit 5685f41

Please sign in to comment.