Better CTL error

This commit is contained in:
wborgeaud 2022-07-11 11:07:16 +02:00
parent 457ac11083
commit 91fcf26289
2 changed files with 118 additions and 2 deletions

View File

@ -47,7 +47,7 @@ impl<F: RichField + Extendable<D>, const D: usize> AllStark<F, D> {
}
}
#[derive(Copy, Clone)]
#[derive(Debug, Copy, Clone)]
pub enum Table {
Cpu = 0,
Keccak = 1,
@ -130,6 +130,7 @@ mod tests {
use crate::all_stark::{all_cross_table_lookups, AllStark};
use crate::config::StarkConfig;
use crate::cpu::cpu_stark::CpuStark;
use crate::cross_table_lookup::testutils::check_ctls;
use crate::keccak::keccak_stark::{KeccakStark, NUM_INPUTS, NUM_ROUNDS};
use crate::logic::{self, LogicStark};
use crate::memory::memory_stark::{generate_random_memory_ops, MemoryStark};
@ -356,10 +357,13 @@ mod tests {
cross_table_lookups: all_cross_table_lookups(),
};
let traces = vec![cpu_trace, keccak_trace, logic_trace, memory_trace];
check_ctls(&traces, &all_stark.cross_table_lookups);
let proof = prove::<F, C, D>(
&all_stark,
config,
vec![cpu_trace, keccak_trace, logic_trace, memory_trace],
traces,
vec![vec![]; 4],
&mut TimingTree::default(),
)?;

View File

@ -649,3 +649,115 @@ pub(crate) fn verify_cross_table_lookups_circuit<
}
debug_assert!(ctl_zs_openings.iter_mut().all(|iter| iter.next().is_none()));
}
#[cfg(test)]
pub(crate) mod testutils {
use std::collections::HashMap;
use plonky2::field::polynomial::PolynomialValues;
use plonky2::field::types::Field;
use crate::all_stark::Table;
use crate::cross_table_lookup::{CrossTableLookup, TableWithColumns};
type MultiSet<F> = HashMap<Vec<F>, Vec<(Table, usize)>>;
fn process_table<F: Field>(
trace_poly_values: &[Vec<PolynomialValues<F>>],
table: &TableWithColumns<F>,
multiset: &mut MultiSet<F>,
) {
let trace = &trace_poly_values[table.table as usize];
for i in 0..trace[0].len() {
let filter = if let Some(column) = &table.filter_column {
column.eval_table(trace, i)
} else {
F::ONE
};
if filter.is_one() {
let row = table
.columns
.iter()
.map(|c| c.eval_table(trace, i))
.collect::<Vec<_>>();
multiset.entry(row).or_default().push((table.table, i));
} else {
assert_eq!(filter, F::ZERO, "Non-binary filter?")
}
}
}
fn check_ctl<F: Field>(
trace_poly_values: &[Vec<PolynomialValues<F>>],
ctl: &CrossTableLookup<F>,
ctl_index: usize,
) {
let CrossTableLookup {
looking_tables,
looked_table,
default,
} = ctl;
let mut looking_multiset = MultiSet::<F>::new();
let mut looked_multiset = MultiSet::<F>::new();
for table in looking_tables {
process_table(trace_poly_values, table, &mut looking_multiset);
}
process_table(trace_poly_values, looked_table, &mut looked_multiset);
let empty = &vec![];
let mut extra_default_count = default.as_ref().map(|_| 0);
for (row, looking_locations) in &looking_multiset {
let looked_locations = looked_multiset.get(row).unwrap_or_else(|| empty);
if let Some(default) = default {
if row == default {
*extra_default_count.as_mut().unwrap() +=
looking_locations.len() - looked_locations.len();
continue;
}
}
check_locations(looking_locations, looked_locations, ctl_index, row);
}
if let Some(count) = extra_default_count {
assert_eq!(
count,
looking_tables
.iter()
.map(|table| trace_poly_values[table.table as usize][0].len())
.sum::<usize>()
- trace_poly_values[looked_table.table as usize][0].len()
);
}
for (row, looked_locations) in &looked_multiset {
let looking_locations = looking_multiset.get(row).unwrap_or_else(|| empty);
check_locations(looking_locations, looked_locations, ctl_index, row);
}
}
fn check_locations<F: Field>(
looking_locations: &[(Table, usize)],
looked_locations: &[(Table, usize)],
ctl_index: usize,
row: &[F],
) {
if looking_locations.len() != looked_locations.len() {
panic!(
"CTL #{ctl_index}:\n\
Row {row:?} is present {l0} times in the looking tables, but {l1} times in the looked table.\n\
Looking locations (Table, Row index): {looking_locations:?}.\n\
Looked locations (Table, Row index): {looked_locations:?}.",
l0 = looking_locations.len(),
l1 = looked_locations.len(),
);
}
}
pub(crate) fn check_ctls<F: Field>(
trace_poly_values: &[Vec<PolynomialValues<F>>],
cross_table_lookups: &[CrossTableLookup<F>],
) {
for (i, ctl) in cross_table_lookups.iter().enumerate() {
check_ctl(trace_poly_values, ctl, i);
}
}
}