From 91fcf262896a4f298b8e9e162ac1f3d4988ae4e1 Mon Sep 17 00:00:00 2001 From: wborgeaud Date: Mon, 11 Jul 2022 11:07:16 +0200 Subject: [PATCH 1/6] Better CTL error --- evm/src/all_stark.rs | 8 ++- evm/src/cross_table_lookup.rs | 112 ++++++++++++++++++++++++++++++++++ 2 files changed, 118 insertions(+), 2 deletions(-) diff --git a/evm/src/all_stark.rs b/evm/src/all_stark.rs index d1f993cd..1f54a4ce 100644 --- a/evm/src/all_stark.rs +++ b/evm/src/all_stark.rs @@ -47,7 +47,7 @@ impl, const D: usize> AllStark { } } -#[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::( &all_stark, config, - vec![cpu_trace, keccak_trace, logic_trace, memory_trace], + traces, vec![vec![]; 4], &mut TimingTree::default(), )?; diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index 60ce25d7..f316a17a 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -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 = HashMap, Vec<(Table, usize)>>; + + fn process_table( + trace_poly_values: &[Vec>], + table: &TableWithColumns, + multiset: &mut MultiSet, + ) { + 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::>(); + multiset.entry(row).or_default().push((table.table, i)); + } else { + assert_eq!(filter, F::ZERO, "Non-binary filter?") + } + } + } + + fn check_ctl( + trace_poly_values: &[Vec>], + ctl: &CrossTableLookup, + ctl_index: usize, + ) { + let CrossTableLookup { + looking_tables, + looked_table, + default, + } = ctl; + let mut looking_multiset = MultiSet::::new(); + let mut looked_multiset = MultiSet::::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::() + - 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( + 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( + trace_poly_values: &[Vec>], + cross_table_lookups: &[CrossTableLookup], + ) { + for (i, ctl) in cross_table_lookups.iter().enumerate() { + check_ctl(trace_poly_values, ctl, i); + } + } +} From 36c8aa34c16bb4d348ea0f2f47598a7512d46511 Mon Sep 17 00:00:00 2001 From: wborgeaud Date: Mon, 11 Jul 2022 14:13:07 +0200 Subject: [PATCH 2/6] Comments --- evm/src/cross_table_lookup.rs | 117 ++++++++++++++++++---------------- 1 file changed, 61 insertions(+), 56 deletions(-) diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index f316a17a..b243d760 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -662,6 +662,67 @@ pub(crate) mod testutils { type MultiSet = HashMap, Vec<(Table, usize)>>; + /// Check that the provided traces and cross-table lookups are consistent. + pub(crate) fn check_ctls( + trace_poly_values: &[Vec>], + cross_table_lookups: &[CrossTableLookup], + ) { + for (i, ctl) in cross_table_lookups.iter().enumerate() { + check_ctl(trace_poly_values, ctl, i); + } + } + + fn check_ctl( + trace_poly_values: &[Vec>], + ctl: &CrossTableLookup, + ctl_index: usize, + ) { + let CrossTableLookup { + looking_tables, + looked_table, + default, + } = ctl; + let mut looking_multiset = MultiSet::::new(); + let mut looked_multiset = MultiSet::::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![]; + // Check that every row in the looking tables appears in the looked table the same number of times + // with some special logic for the default row. + 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); + } + // Check that the number of extra default rows is correct. + 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::() + - trace_poly_values[looked_table.table as usize][0].len() + ); + } + // Check that every row in the looked tables appears in the looked table the same number of times. + 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 process_table( trace_poly_values: &[Vec>], table: &TableWithColumns, @@ -687,53 +748,6 @@ pub(crate) mod testutils { } } - fn check_ctl( - trace_poly_values: &[Vec>], - ctl: &CrossTableLookup, - ctl_index: usize, - ) { - let CrossTableLookup { - looking_tables, - looked_table, - default, - } = ctl; - let mut looking_multiset = MultiSet::::new(); - let mut looked_multiset = MultiSet::::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::() - - 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( looking_locations: &[(Table, usize)], looked_locations: &[(Table, usize)], @@ -751,13 +765,4 @@ pub(crate) mod testutils { ); } } - - pub(crate) fn check_ctls( - trace_poly_values: &[Vec>], - cross_table_lookups: &[CrossTableLookup], - ) { - for (i, ctl) in cross_table_lookups.iter().enumerate() { - check_ctl(trace_poly_values, ctl, i); - } - } } From 3ff67e38dc281a3b23ef03c1f739bc03999b99a0 Mon Sep 17 00:00:00 2001 From: wborgeaud Date: Mon, 11 Jul 2022 14:16:58 +0200 Subject: [PATCH 3/6] Minor --- evm/src/cross_table_lookup.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index b243d760..049821e0 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -757,9 +757,9 @@ pub(crate) mod testutils { 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:?}.", + 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(), ); From 50ebf39d37a5941ddc06115b672b68a2385e720e Mon Sep 17 00:00:00 2001 From: wborgeaud Date: Mon, 11 Jul 2022 14:24:12 +0200 Subject: [PATCH 4/6] Comment --- evm/src/cross_table_lookup.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index 049821e0..a01fbfa1 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -682,6 +682,9 @@ pub(crate) mod testutils { looked_table, default, } = ctl; + + // Maps `m` with `(table, i) in m[row]` iff the `i`-th row of `table` is equal to `row` and + // the filter is 1. Without default values, the CTL check holds iff `looking_multiset == looked_multiset`. let mut looking_multiset = MultiSet::::new(); let mut looked_multiset = MultiSet::::new(); From 5e27e7264dbe4be286a4158f6953ff454f3149c8 Mon Sep 17 00:00:00 2001 From: wborgeaud Date: Mon, 11 Jul 2022 14:56:27 +0200 Subject: [PATCH 5/6] unwrap_or_else -> unwrap_or --- evm/src/cross_table_lookup.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index a01fbfa1..12d8984e 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -698,7 +698,7 @@ pub(crate) mod testutils { // with some special logic for the default row. 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); + let looked_locations = looked_multiset.get(row).unwrap_or(empty); if let Some(default) = default { if row == default { *extra_default_count.as_mut().unwrap() += @@ -721,7 +721,7 @@ pub(crate) mod testutils { } // Check that every row in the looked tables appears in the looked table the same number of times. for (row, looked_locations) in &looked_multiset { - let looking_locations = looking_multiset.get(row).unwrap_or_else(|| empty); + let looking_locations = looking_multiset.get(row).unwrap_or(empty); check_locations(looking_locations, looked_locations, ctl_index, row); } } From d35d3e20951b9ae8cd440c385262e6ac714357c3 Mon Sep 17 00:00:00 2001 From: wborgeaud Date: Mon, 11 Jul 2022 19:53:00 +0200 Subject: [PATCH 6/6] PR feedback + underflow check --- evm/src/cross_table_lookup.rs | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index 12d8984e..4097df7b 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -696,18 +696,32 @@ pub(crate) mod testutils { let empty = &vec![]; // Check that every row in the looking tables appears in the looked table the same number of times // with some special logic for the default row. - 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(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); } + let extra_default_count = default.as_ref().map(|d| { + let looking_default_locations = looking_multiset.get(d).unwrap_or(empty); + let looked_default_locations = looked_multiset.get(d).unwrap_or(empty); + looking_default_locations + .len() + .checked_sub(looked_default_locations.len()) + .unwrap_or_else(|| { + // If underflow, panic. There should be more default rows in the looking side. + check_locations( + looking_default_locations, + looked_default_locations, + ctl_index, + d, + ); + unreachable!() + }) + }); // Check that the number of extra default rows is correct. if let Some(count) = extra_default_count { assert_eq!(