Merge pull request #1229 from topos-protocol/next_row_ctls

Make next row available to CTLs
This commit is contained in:
Hamy Ratoanina 2023-09-18 15:19:10 +02:00 committed by GitHub
commit 15064b3aa7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 184 additions and 94 deletions

View File

@ -25,6 +25,7 @@ use crate::vars::{StarkEvaluationTargets, StarkEvaluationVars};
#[derive(Clone, Debug)]
pub struct Column<F: Field> {
linear_combination: Vec<(usize, F)>,
next_row_linear_combination: Vec<(usize, F)>,
constant: F,
}
@ -32,6 +33,7 @@ impl<F: Field> Column<F> {
pub fn single(c: usize) -> Self {
Self {
linear_combination: vec![(c, F::ONE)],
next_row_linear_combination: vec![],
constant: F::ZERO,
}
}
@ -42,9 +44,24 @@ impl<F: Field> Column<F> {
cs.into_iter().map(|c| Self::single(*c.borrow()))
}
pub fn single_next_row(c: usize) -> Self {
Self {
linear_combination: vec![],
next_row_linear_combination: vec![(c, F::ONE)],
constant: F::ZERO,
}
}
pub fn singles_next_row<I: IntoIterator<Item = impl Borrow<usize>>>(
cs: I,
) -> impl Iterator<Item = Self> {
cs.into_iter().map(|c| Self::single_next_row(*c.borrow()))
}
pub fn constant(constant: F) -> Self {
Self {
linear_combination: vec![],
next_row_linear_combination: vec![],
constant,
}
}
@ -70,6 +87,34 @@ impl<F: Field> Column<F> {
);
Self {
linear_combination: v,
next_row_linear_combination: vec![],
constant,
}
}
pub fn linear_combination_and_next_row_with_constant<I: IntoIterator<Item = (usize, F)>>(
iter: I,
next_row_iter: I,
constant: F,
) -> Self {
let v = iter.into_iter().collect::<Vec<_>>();
let next_row_v = next_row_iter.into_iter().collect::<Vec<_>>();
assert!(!v.is_empty() || !next_row_v.is_empty());
debug_assert_eq!(
v.iter().map(|(c, _)| c).unique().count(),
v.len(),
"Duplicate columns."
);
debug_assert_eq!(
next_row_v.iter().map(|(c, _)| c).unique().count(),
next_row_v.len(),
"Duplicate columns."
);
Self {
linear_combination: v,
next_row_linear_combination: next_row_v,
constant,
}
}
@ -106,13 +151,43 @@ impl<F: Field> Column<F> {
+ FE::from_basefield(self.constant)
}
pub fn eval_with_next<FE, P, const D: usize>(&self, v: &[P], next_v: &[P]) -> P
where
FE: FieldExtension<D, BaseField = F>,
P: PackedField<Scalar = FE>,
{
self.linear_combination
.iter()
.map(|&(c, f)| v[c] * FE::from_basefield(f))
.sum::<P>()
+ self
.next_row_linear_combination
.iter()
.map(|&(c, f)| next_v[c] * FE::from_basefield(f))
.sum::<P>()
+ FE::from_basefield(self.constant)
}
/// Evaluate on an row of a table given in column-major form.
pub fn eval_table(&self, table: &[PolynomialValues<F>], row: usize) -> F {
self.linear_combination
let mut res = self
.linear_combination
.iter()
.map(|&(c, f)| table[c].values[row] * f)
.sum::<F>()
+ self.constant
+ self.constant;
// If we access the next row at the last row, for sanity, we consider the next row's values to be 0.
// If CTLs are correctly written, the filter should be 0 in that case anyway.
if !self.next_row_linear_combination.is_empty() && row < table.len() - 1 {
res += self
.next_row_linear_combination
.iter()
.map(|&(c, f)| table[c].values[row + 1] * f)
.sum::<F>();
}
res
}
pub fn eval_circuit<const D: usize>(
@ -136,6 +211,36 @@ impl<F: Field> Column<F> {
let constant = builder.constant_extension(F::Extension::from_basefield(self.constant));
builder.inner_product_extension(F::ONE, constant, pairs)
}
pub fn eval_with_next_circuit<const D: usize>(
&self,
builder: &mut CircuitBuilder<F, D>,
v: &[ExtensionTarget<D>],
next_v: &[ExtensionTarget<D>],
) -> ExtensionTarget<D>
where
F: RichField + Extendable<D>,
{
let mut pairs = self
.linear_combination
.iter()
.map(|&(c, f)| {
(
v[c],
builder.constant_extension(F::Extension::from_basefield(f)),
)
})
.collect::<Vec<_>>();
let next_row_pairs = self.next_row_linear_combination.iter().map(|&(c, f)| {
(
next_v[c],
builder.constant_extension(F::Extension::from_basefield(f)),
)
});
pairs.extend(next_row_pairs);
let constant = builder.constant_extension(F::Extension::from_basefield(self.constant));
builder.inner_product_extension(F::ONE, constant, pairs)
}
}
#[derive(Clone, Debug)]
@ -276,7 +381,7 @@ fn partial_products<F: Field>(
let mut partial_prod = F::ONE;
let degree = trace[0].len();
let mut res = Vec::with_capacity(degree);
for i in 0..degree {
for i in (0..degree).rev() {
let filter = if let Some(column) = filter_column {
column.eval_table(trace, i)
} else {
@ -293,6 +398,7 @@ fn partial_products<F: Field>(
};
res.push(partial_prod);
}
res.reverse();
res.into()
}
@ -362,6 +468,10 @@ impl<'a, F: RichField + Extendable<D>, const D: usize>
}
}
/// CTL Z partial products are upside down: the complete product is on the first row, and
/// the first term is on the last row. This allows the transition constraint to be:
/// Z(w) = Z(gw) * combine(w) where combine is called on the local row
/// and not the next. This enables CTLs across two rows.
pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const D2: usize>(
vars: StarkEvaluationVars<FE, P, { S::COLUMNS }>,
ctl_vars: &[CtlCheckVars<F, FE, P, D2>],
@ -380,27 +490,23 @@ pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const
columns,
filter_column,
} = lookup_vars;
let combine = |v: &[P]| -> P {
let evals = columns.iter().map(|c| c.eval(v)).collect::<Vec<_>>();
challenges.combine(evals.iter())
};
let filter = |v: &[P]| -> P {
if let Some(column) = filter_column {
column.eval(v)
} else {
P::ONES
}
};
let local_filter = filter(vars.local_values);
let next_filter = filter(vars.next_values);
let select = |filter, x| filter * x + P::ONES - filter;
// Check value of `Z(1)`
consumer.constraint_first_row(*local_z - select(local_filter, combine(vars.local_values)));
// Check `Z(gw) = combination * Z(w)`
consumer.constraint_transition(
*local_z * select(next_filter, combine(vars.next_values)) - *next_z,
);
let evals = columns
.iter()
.map(|c| c.eval_with_next(vars.local_values, vars.next_values))
.collect::<Vec<_>>();
let combined = challenges.combine(evals.iter());
let local_filter = if let Some(column) = filter_column {
column.eval(vars.local_values)
} else {
P::ONES
};
let select = local_filter * combined + P::ONES - local_filter;
// Check value of `Z(g^(n-1))`
consumer.constraint_last_row(*local_z - select);
// Check `Z(w) = combination * Z(gw)`
consumer.constraint_transition(*next_z * select - *local_z);
}
}
@ -493,11 +599,6 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
} else {
one
};
let next_filter = if let Some(column) = filter_column {
column.eval_circuit(builder, vars.next_values)
} else {
one
};
fn select<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
filter: ExtensionTarget<D>,
@ -508,34 +609,30 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
builder.mul_add_extension(filter, x, tmp) // filter * x + 1 - filter
}
// Check value of `Z(1)`
let local_columns_eval = columns
let evals = columns
.iter()
.map(|c| c.eval_circuit(builder, vars.local_values))
.map(|c| c.eval_with_next_circuit(builder, vars.local_values, vars.next_values))
.collect::<Vec<_>>();
let combined_local = challenges.combine_circuit(builder, &local_columns_eval);
let selected_local = select(builder, local_filter, combined_local);
let first_row = builder.sub_extension(*local_z, selected_local);
consumer.constraint_first_row(builder, first_row);
// Check `Z(gw) = combination * Z(w)`
let next_columns_eval = columns
.iter()
.map(|c| c.eval_circuit(builder, vars.next_values))
.collect::<Vec<_>>();
let combined_next = challenges.combine_circuit(builder, &next_columns_eval);
let selected_next = select(builder, next_filter, combined_next);
let transition = builder.mul_sub_extension(*local_z, selected_next, *next_z);
let combined = challenges.combine_circuit(builder, &evals);
let select = select(builder, local_filter, combined);
// Check value of `Z(g^(n-1))`
let last_row = builder.sub_extension(*local_z, select);
consumer.constraint_last_row(builder, last_row);
// Check `Z(w) = combination * Z(gw)`
let transition = builder.mul_sub_extension(*next_z, select, *local_z);
consumer.constraint_transition(builder, transition);
}
}
pub(crate) fn verify_cross_table_lookups<F: RichField + Extendable<D>, const D: usize>(
cross_table_lookups: &[CrossTableLookup<F>],
ctl_zs_lasts: [Vec<F>; NUM_TABLES],
ctl_zs_first: [Vec<F>; NUM_TABLES],
ctl_extra_looking_products: Vec<Vec<F>>,
config: &StarkConfig,
) -> Result<()> {
let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::<Vec<_>>();
let mut ctl_zs_openings = ctl_zs_first.iter().map(|v| v.iter()).collect::<Vec<_>>();
for (
index,
CrossTableLookup {
@ -568,11 +665,11 @@ pub(crate) fn verify_cross_table_lookups<F: RichField + Extendable<D>, const D:
pub(crate) fn verify_cross_table_lookups_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
cross_table_lookups: Vec<CrossTableLookup<F>>,
ctl_zs_lasts: [Vec<Target>; NUM_TABLES],
ctl_zs_first: [Vec<Target>; NUM_TABLES],
ctl_extra_looking_products: Vec<Vec<Target>>,
inner_config: &StarkConfig,
) {
let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::<Vec<_>>();
let mut ctl_zs_openings = ctl_zs_first.iter().map(|v| v.iter()).collect::<Vec<_>>();
for CrossTableLookup {
looking_tables,
looked_table,

View File

@ -526,7 +526,7 @@ where
verify_cross_table_lookups_circuit::<F, D>(
&mut builder,
all_cross_table_lookups(),
pis.map(|p| p.ctl_zs_last),
pis.map(|p| p.ctl_zs_first),
extra_looking_products,
stark_config,
);

View File

@ -623,7 +623,7 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize> S
}
pub fn num_ctl_zs(&self) -> usize {
self.openings.ctl_zs_last.len()
self.openings.ctl_zs_first.len()
}
}
@ -704,8 +704,8 @@ pub struct StarkOpeningSet<F: RichField + Extendable<D>, const D: usize> {
pub permutation_ctl_zs: Vec<F::Extension>,
/// Openings of permutations and cross-table lookups `Z` polynomials at `g * zeta`.
pub permutation_ctl_zs_next: Vec<F::Extension>,
/// Openings of cross-table lookups `Z` polynomials at `g^-1`.
pub ctl_zs_last: Vec<F>,
/// Openings of cross-table lookups `Z` polynomials at `1`.
pub ctl_zs_first: Vec<F>,
/// Openings of quotient polynomials at `zeta`.
pub quotient_polys: Vec<F::Extension>,
}
@ -717,7 +717,6 @@ impl<F: RichField + Extendable<D>, const D: usize> StarkOpeningSet<F, D> {
trace_commitment: &PolynomialBatch<F, C, D>,
permutation_ctl_zs_commitment: &PolynomialBatch<F, C, D>,
quotient_commitment: &PolynomialBatch<F, C, D>,
degree_bits: usize,
num_permutation_zs: usize,
) -> Self {
let eval_commitment = |z: F::Extension, c: &PolynomialBatch<F, C, D>| {
@ -738,10 +737,8 @@ impl<F: RichField + Extendable<D>, const D: usize> StarkOpeningSet<F, D> {
next_values: eval_commitment(zeta_next, trace_commitment),
permutation_ctl_zs: eval_commitment(zeta, permutation_ctl_zs_commitment),
permutation_ctl_zs_next: eval_commitment(zeta_next, permutation_ctl_zs_commitment),
ctl_zs_last: eval_commitment_base(
F::primitive_root_of_unity(degree_bits).inverse(),
permutation_ctl_zs_commitment,
)[num_permutation_zs..]
ctl_zs_first: eval_commitment_base(F::ONE, permutation_ctl_zs_commitment)
[num_permutation_zs..]
.to_vec(),
quotient_polys: eval_commitment(zeta, quotient_commitment),
}
@ -765,10 +762,10 @@ impl<F: RichField + Extendable<D>, const D: usize> StarkOpeningSet<F, D> {
.copied()
.collect_vec(),
};
debug_assert!(!self.ctl_zs_last.is_empty());
let ctl_last_batch = FriOpeningBatch {
debug_assert!(!self.ctl_zs_first.is_empty());
let ctl_first_batch = FriOpeningBatch {
values: self
.ctl_zs_last
.ctl_zs_first
.iter()
.copied()
.map(F::Extension::from_basefield)
@ -776,7 +773,7 @@ impl<F: RichField + Extendable<D>, const D: usize> StarkOpeningSet<F, D> {
};
FriOpenings {
batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch],
batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch],
}
}
}
@ -787,7 +784,7 @@ pub struct StarkOpeningSetTarget<const D: usize> {
pub next_values: Vec<ExtensionTarget<D>>,
pub permutation_ctl_zs: Vec<ExtensionTarget<D>>,
pub permutation_ctl_zs_next: Vec<ExtensionTarget<D>>,
pub ctl_zs_last: Vec<Target>,
pub ctl_zs_first: Vec<Target>,
pub quotient_polys: Vec<ExtensionTarget<D>>,
}
@ -797,7 +794,7 @@ impl<const D: usize> StarkOpeningSetTarget<D> {
buffer.write_target_ext_vec(&self.next_values)?;
buffer.write_target_ext_vec(&self.permutation_ctl_zs)?;
buffer.write_target_ext_vec(&self.permutation_ctl_zs_next)?;
buffer.write_target_vec(&self.ctl_zs_last)?;
buffer.write_target_vec(&self.ctl_zs_first)?;
buffer.write_target_ext_vec(&self.quotient_polys)?;
Ok(())
}
@ -807,7 +804,7 @@ impl<const D: usize> StarkOpeningSetTarget<D> {
let next_values = buffer.read_target_ext_vec::<D>()?;
let permutation_ctl_zs = buffer.read_target_ext_vec::<D>()?;
let permutation_ctl_zs_next = buffer.read_target_ext_vec::<D>()?;
let ctl_zs_last = buffer.read_target_vec()?;
let ctl_zs_first = buffer.read_target_vec()?;
let quotient_polys = buffer.read_target_ext_vec::<D>()?;
Ok(Self {
@ -815,7 +812,7 @@ impl<const D: usize> StarkOpeningSetTarget<D> {
next_values,
permutation_ctl_zs,
permutation_ctl_zs_next,
ctl_zs_last,
ctl_zs_first,
quotient_polys,
})
}
@ -838,10 +835,10 @@ impl<const D: usize> StarkOpeningSetTarget<D> {
.copied()
.collect_vec(),
};
debug_assert!(!self.ctl_zs_last.is_empty());
let ctl_last_batch = FriOpeningBatchTarget {
debug_assert!(!self.ctl_zs_first.is_empty());
let ctl_first_batch = FriOpeningBatchTarget {
values: self
.ctl_zs_last
.ctl_zs_first
.iter()
.copied()
.map(|t| t.to_ext_target(zero))
@ -849,7 +846,7 @@ impl<const D: usize> StarkOpeningSetTarget<D> {
};
FriOpeningsTarget {
batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch],
batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch],
}
}
}

View File

@ -453,7 +453,6 @@ where
trace_commitment,
&permutation_ctl_zs_commitment,
&quotient_commitment,
degree_bits,
stark.num_permutation_batches(config),
);
challenger.observe_openings(&openings.to_fri_openings());
@ -468,7 +467,7 @@ where
timing,
"compute openings proof",
PolynomialBatch::prove_openings(
&stark.fri_instance(zeta, g, degree_bits, ctl_data.len(), config),
&stark.fri_instance(zeta, g, ctl_data.len(), config),
&initial_merkle_trees,
challenger,
&fri_params,

View File

@ -59,7 +59,7 @@ pub struct RecursiveAllProof<
pub(crate) struct PublicInputs<T: Copy + Default + Eq + PartialEq + Debug, P: PlonkyPermutation<T>>
{
pub(crate) trace_cap: Vec<Vec<T>>,
pub(crate) ctl_zs_last: Vec<T>,
pub(crate) ctl_zs_first: Vec<T>,
pub(crate) ctl_challenges: GrandProductChallengeSet<T>,
pub(crate) challenger_state_before: P,
pub(crate) challenger_state_after: P,
@ -85,11 +85,11 @@ impl<T: Copy + Debug + Default + Eq + PartialEq, P: PlonkyPermutation<T>> Public
};
let challenger_state_before = P::new(&mut iter);
let challenger_state_after = P::new(&mut iter);
let ctl_zs_last: Vec<_> = iter.collect();
let ctl_zs_first: Vec<_> = iter.collect();
Self {
trace_cap,
ctl_zs_last,
ctl_zs_first,
ctl_challenges,
challenger_state_before,
challenger_state_after,
@ -150,7 +150,7 @@ impl<F: RichField + Extendable<D>, C: GenericConfig<D, F = F>, const D: usize>
// Verify the CTL checks.
verify_cross_table_lookups::<F, D>(
&cross_table_lookups,
pis.map(|p| p.ctl_zs_last),
pis.map(|p| p.ctl_zs_first),
extra_looking_products,
inner_config,
)?;
@ -350,7 +350,7 @@ where
let challenger_state = challenger.compact(&mut builder);
builder.register_public_inputs(challenger_state.as_ref());
builder.register_public_inputs(&proof_target.openings.ctl_zs_last);
builder.register_public_inputs(&proof_target.openings.ctl_zs_first);
verify_stark_proof_with_challenges_circuit::<F, C, _, D>(
&mut builder,
@ -414,7 +414,7 @@ fn verify_stark_proof_with_challenges_circuit<
next_values,
permutation_ctl_zs,
permutation_ctl_zs_next,
ctl_zs_last,
ctl_zs_first,
quotient_polys,
} = &proof.openings;
let vars = StarkEvaluationTargets {
@ -484,8 +484,7 @@ fn verify_stark_proof_with_challenges_circuit<
builder,
challenges.stark_zeta,
F::primitive_root_of_unity(degree_bits),
degree_bits,
ctl_zs_last.len(),
ctl_zs_first.len(),
inner_config,
);
builder.verify_fri_proof::<C>(
@ -869,7 +868,7 @@ fn add_virtual_stark_opening_set<F: RichField + Extendable<D>, S: Stark<F, D>, c
.add_virtual_extension_targets(stark.num_permutation_batches(config) + num_ctl_zs),
permutation_ctl_zs_next: builder
.add_virtual_extension_targets(stark.num_permutation_batches(config) + num_ctl_zs),
ctl_zs_last: builder.add_virtual_targets(num_ctl_zs),
ctl_zs_first: builder.add_virtual_targets(num_ctl_zs),
quotient_polys: builder
.add_virtual_extension_targets(stark.quotient_degree_factor() * num_challenges),
}

View File

@ -84,7 +84,6 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
&self,
zeta: F::Extension,
g: F,
degree_bits: usize,
num_ctl_zs: usize,
config: &StarkConfig,
) -> FriInstanceInfo<F, D> {
@ -131,13 +130,13 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
point: zeta.scalar_mul(g),
polynomials: [trace_info, permutation_ctl_zs_info].concat(),
};
let ctl_last_batch = FriBatchInfo {
point: F::Extension::primitive_root_of_unity(degree_bits).inverse(),
let ctl_first_batch = FriBatchInfo {
point: F::Extension::ONE,
polynomials: ctl_zs_info,
};
FriInstanceInfo {
oracles: vec![trace_oracle, permutation_ctl_oracle, quotient_oracle],
batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch],
batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch],
}
}
@ -147,7 +146,6 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
builder: &mut CircuitBuilder<F, D>,
zeta: ExtensionTarget<D>,
g: F,
degree_bits: usize,
num_ctl_zs: usize,
inner_config: &StarkConfig,
) -> FriInstanceInfoTarget<D> {
@ -195,14 +193,13 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
point: zeta_next,
polynomials: [trace_info, permutation_ctl_zs_info].concat(),
};
let ctl_last_batch = FriBatchInfoTarget {
point: builder
.constant_extension(F::Extension::primitive_root_of_unity(degree_bits).inverse()),
let ctl_first_batch = FriBatchInfoTarget {
point: builder.one_extension(),
polynomials: ctl_zs_info,
};
FriInstanceInfoTarget {
oracles: vec![trace_oracle, permutation_ctl_oracle, quotient_oracle],
batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch],
batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch],
}
}

View File

@ -135,7 +135,9 @@ where
verify_cross_table_lookups::<F, D>(
cross_table_lookups,
all_proof.stark_proofs.map(|p| p.proof.openings.ctl_zs_last),
all_proof
.stark_proofs
.map(|p| p.proof.openings.ctl_zs_first),
extra_looking_products,
config,
)
@ -308,7 +310,7 @@ where
next_values,
permutation_ctl_zs,
permutation_ctl_zs_next,
ctl_zs_last,
ctl_zs_first,
quotient_polys,
} = &proof.openings;
let vars = StarkEvaluationVars {
@ -374,8 +376,7 @@ where
&stark.fri_instance(
challenges.stark_zeta,
F::primitive_root_of_unity(degree_bits),
degree_bits,
ctl_zs_last.len(),
ctl_zs_first.len(),
config,
),
&proof.openings.to_fri_openings(),
@ -415,7 +416,7 @@ where
next_values,
permutation_ctl_zs,
permutation_ctl_zs_next,
ctl_zs_last,
ctl_zs_first,
quotient_polys,
} = openings;
@ -432,7 +433,7 @@ where
ensure!(next_values.len() == S::COLUMNS);
ensure!(permutation_ctl_zs.len() == num_zs);
ensure!(permutation_ctl_zs_next.len() == num_zs);
ensure!(ctl_zs_last.len() == num_ctl_zs);
ensure!(ctl_zs_first.len() == num_ctl_zs);
ensure!(quotient_polys.len() == stark.num_quotient_polys(config));
Ok(())