Remove CTL defaults

We ended up not needing the feature.
This commit is contained in:
Daniel Lubarov 2023-01-03 11:36:42 -08:00
parent 0ca308400a
commit 6655e776a8
4 changed files with 12 additions and 70 deletions

View File

@ -114,7 +114,7 @@ fn ctl_keccak<F: Field>() -> CrossTableLookup<F> {
keccak_stark::ctl_data(),
Some(keccak_stark::ctl_filter()),
);
CrossTableLookup::new(vec![keccak_sponge_looking], keccak_looked, None)
CrossTableLookup::new(vec![keccak_sponge_looking], keccak_looked)
}
fn ctl_keccak_sponge<F: Field>() -> CrossTableLookup<F> {
@ -128,7 +128,7 @@ fn ctl_keccak_sponge<F: Field>() -> CrossTableLookup<F> {
keccak_sponge_stark::ctl_looked_data(),
Some(keccak_sponge_stark::ctl_looked_filter()),
);
CrossTableLookup::new(vec![cpu_looking], keccak_sponge_looked, None)
CrossTableLookup::new(vec![cpu_looking], keccak_sponge_looked)
}
fn ctl_logic<F: Field>() -> CrossTableLookup<F> {
@ -148,7 +148,7 @@ fn ctl_logic<F: Field>() -> CrossTableLookup<F> {
}
let logic_looked =
TableWithColumns::new(Table::Logic, logic::ctl_data(), Some(logic::ctl_filter()));
CrossTableLookup::new(all_lookers, logic_looked, None)
CrossTableLookup::new(all_lookers, logic_looked)
}
fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
@ -180,5 +180,5 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
memory_stark::ctl_data(),
Some(memory_stark::ctl_filter()),
);
CrossTableLookup::new(all_lookers, memory_looked, None)
CrossTableLookup::new(all_lookers, memory_looked)
}

View File

@ -159,34 +159,19 @@ impl<F: Field> TableWithColumns<F> {
pub struct CrossTableLookup<F: Field> {
pub(crate) looking_tables: Vec<TableWithColumns<F>>,
pub(crate) looked_table: TableWithColumns<F>,
/// Default value if filters are not used.
// TODO: Remove? Ended up not using it.
default: Option<Vec<F>>,
}
impl<F: Field> CrossTableLookup<F> {
pub fn new(
looking_tables: Vec<TableWithColumns<F>>,
looked_table: TableWithColumns<F>,
default: Option<Vec<F>>,
) -> Self {
assert!(looking_tables
.iter()
.all(|twc| twc.columns.len() == looked_table.columns.len()));
assert!(
looking_tables
.iter()
.all(|twc| twc.filter_column.is_none() == default.is_some())
&& default.is_some() == looked_table.filter_column.is_none(),
"Default values should be provided iff there are no filter columns."
);
if let Some(default) = &default {
assert_eq!(default.len(), looked_table.columns.len());
}
Self {
looking_tables,
looked_table,
default,
}
}
@ -241,7 +226,6 @@ pub(crate) fn cross_table_lookup_data<F: RichField, C: GenericConfig<D, F = F>,
for CrossTableLookup {
looking_tables,
looked_table,
default,
} in cross_table_lookups
{
log::debug!("Processing CTL for {:?}", looked_table.table);
@ -267,21 +251,6 @@ pub(crate) fn cross_table_lookup_data<F: RichField, C: GenericConfig<D, F = F>,
.map(|z| *z.values.last().unwrap())
.product::<F>(),
*z_looked.values.last().unwrap()
* default
.as_ref()
.map(|default| {
challenge.combine(default).exp_u64(
looking_tables
.iter()
.map(|table| {
trace_poly_values[table.table as usize][0].len() as u64
})
.sum::<u64>()
- trace_poly_values[looked_table.table as usize][0].len()
as u64,
)
})
.unwrap_or(F::ONE)
);
for (table, z) in looking_tables.iter().zip(zs_looking) {
@ -374,7 +343,6 @@ impl<'a, F: RichField + Extendable<D>, const D: usize>
for CrossTableLookup {
looking_tables,
looked_table,
..
} in cross_table_lookups
{
for &challenges in &ctl_challenges.challenges {
@ -477,7 +445,6 @@ impl<'a, F: Field, const D: usize> CtlCheckVarsTarget<'a, F, D> {
for CrossTableLookup {
looking_tables,
looked_table,
..
} in cross_table_lookups
{
for &challenges in &ctl_challenges.challenges {
@ -580,42 +547,25 @@ pub(crate) fn verify_cross_table_lookups<
>(
cross_table_lookups: &[CrossTableLookup<F>],
ctl_zs_lasts: [Vec<F>; NUM_TABLES],
degrees_bits: [usize; NUM_TABLES],
challenges: GrandProductChallengeSet<F>,
config: &StarkConfig,
) -> Result<()> {
let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::<Vec<_>>();
for (
i,
CrossTableLookup {
looking_tables,
looked_table,
default,
..
},
) in cross_table_lookups.iter().enumerate()
for CrossTableLookup {
looking_tables,
looked_table,
} in cross_table_lookups.into_iter()
{
for _ in 0..config.num_challenges {
let looking_degrees_sum = looking_tables
.iter()
.map(|table| 1 << degrees_bits[table.table as usize])
.sum::<u64>();
let looked_degree = 1 << degrees_bits[looked_table.table as usize];
let looking_zs_prod = looking_tables
.iter()
.map(|table| *ctl_zs_openings[table.table as usize].next().unwrap())
.product::<F>();
let looked_z = *ctl_zs_openings[looked_table.table as usize].next().unwrap();
let challenge = challenges.challenges[i % config.num_challenges];
if let Some(default) = default.as_ref() {
let combined_default = challenge.combine(default.iter());
ensure!(
looking_zs_prod
== looked_z * combined_default.exp_u64(looking_degrees_sum - looked_degree),
"Cross-table lookup verification failed."
);
}
ensure!(
looking_zs_prod == looked_z,
"Cross-table lookup verification failed."
);
}
}
debug_assert!(ctl_zs_openings.iter_mut().all(|iter| iter.next().is_none()));
@ -637,7 +587,6 @@ pub(crate) fn verify_cross_table_lookups_circuit<
for CrossTableLookup {
looking_tables,
looked_table,
..
} in cross_table_lookups.into_iter()
{
for _ in 0..inner_config.num_challenges {

View File

@ -147,12 +147,9 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize>
}
// Verify the CTL checks.
let degrees_bits = std::array::from_fn(|i| verifier_data[i].common.degree_bits());
verify_cross_table_lookups::<F, C, D>(
&cross_table_lookups,
pis.map(|p| p.ctl_zs_last),
degrees_bits,
ctl_challenges,
inner_config,
)?;

View File

@ -97,13 +97,9 @@ where
config,
)?;
let degrees_bits =
std::array::from_fn(|i| all_proof.stark_proofs[i].proof.recover_degree_bits(config));
verify_cross_table_lookups::<F, C, D>(
cross_table_lookups,
all_proof.stark_proofs.map(|p| p.proof.openings.ctl_zs_last),
degrees_bits,
ctl_challenges,
config,
)
}