mirror of
https://github.com/logos-storage/plonky2.git
synced 2026-01-07 00:03:10 +00:00
Make next row available to CTLs
This commit is contained in:
parent
d1c395ef75
commit
3c4f938f85
@ -120,11 +120,13 @@ fn ctl_keccak<F: Field>() -> CrossTableLookup<F> {
|
||||
let keccak_sponge_looking = TableWithColumns::new(
|
||||
Table::KeccakSponge,
|
||||
keccak_sponge_stark::ctl_looking_keccak(),
|
||||
vec![],
|
||||
Some(keccak_sponge_stark::ctl_looking_keccak_filter()),
|
||||
);
|
||||
let keccak_looked = TableWithColumns::new(
|
||||
Table::Keccak,
|
||||
keccak_stark::ctl_data(),
|
||||
vec![],
|
||||
Some(keccak_stark::ctl_filter()),
|
||||
);
|
||||
CrossTableLookup::new(vec![keccak_sponge_looking], keccak_looked)
|
||||
@ -134,11 +136,13 @@ fn ctl_keccak_sponge<F: Field>() -> CrossTableLookup<F> {
|
||||
let cpu_looking = TableWithColumns::new(
|
||||
Table::Cpu,
|
||||
cpu_stark::ctl_data_keccak_sponge(),
|
||||
vec![],
|
||||
Some(cpu_stark::ctl_filter_keccak_sponge()),
|
||||
);
|
||||
let keccak_sponge_looked = TableWithColumns::new(
|
||||
Table::KeccakSponge,
|
||||
keccak_sponge_stark::ctl_looked_data(),
|
||||
vec![],
|
||||
Some(keccak_sponge_stark::ctl_looked_filter()),
|
||||
);
|
||||
CrossTableLookup::new(vec![cpu_looking], keccak_sponge_looked)
|
||||
@ -148,6 +152,7 @@ fn ctl_logic<F: Field>() -> CrossTableLookup<F> {
|
||||
let cpu_looking = TableWithColumns::new(
|
||||
Table::Cpu,
|
||||
cpu_stark::ctl_data_logic(),
|
||||
vec![],
|
||||
Some(cpu_stark::ctl_filter_logic()),
|
||||
);
|
||||
let mut all_lookers = vec![cpu_looking];
|
||||
@ -155,12 +160,17 @@ fn ctl_logic<F: Field>() -> CrossTableLookup<F> {
|
||||
let keccak_sponge_looking = TableWithColumns::new(
|
||||
Table::KeccakSponge,
|
||||
keccak_sponge_stark::ctl_looking_logic(i),
|
||||
vec![],
|
||||
Some(keccak_sponge_stark::ctl_looking_logic_filter()),
|
||||
);
|
||||
all_lookers.push(keccak_sponge_looking);
|
||||
}
|
||||
let logic_looked =
|
||||
TableWithColumns::new(Table::Logic, logic::ctl_data(), Some(logic::ctl_filter()));
|
||||
let logic_looked = TableWithColumns::new(
|
||||
Table::Logic,
|
||||
logic::ctl_data(),
|
||||
vec![],
|
||||
Some(logic::ctl_filter()),
|
||||
);
|
||||
CrossTableLookup::new(all_lookers, logic_looked)
|
||||
}
|
||||
|
||||
@ -168,12 +178,14 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
|
||||
let cpu_memory_code_read = TableWithColumns::new(
|
||||
Table::Cpu,
|
||||
cpu_stark::ctl_data_code_memory(),
|
||||
vec![],
|
||||
Some(cpu_stark::ctl_filter_code_memory()),
|
||||
);
|
||||
let cpu_memory_gp_ops = (0..NUM_GP_CHANNELS).map(|channel| {
|
||||
TableWithColumns::new(
|
||||
Table::Cpu,
|
||||
cpu_stark::ctl_data_gp_memory(channel),
|
||||
vec![],
|
||||
Some(cpu_stark::ctl_filter_gp_memory(channel)),
|
||||
)
|
||||
});
|
||||
@ -181,6 +193,7 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
|
||||
TableWithColumns::new(
|
||||
Table::KeccakSponge,
|
||||
keccak_sponge_stark::ctl_looking_memory(i),
|
||||
vec![],
|
||||
Some(keccak_sponge_stark::ctl_looking_memory_filter(i)),
|
||||
)
|
||||
});
|
||||
@ -191,6 +204,7 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
|
||||
let memory_looked = TableWithColumns::new(
|
||||
Table::Memory,
|
||||
memory_stark::ctl_data(),
|
||||
vec![],
|
||||
Some(memory_stark::ctl_filter()),
|
||||
);
|
||||
CrossTableLookup::new(all_lookers, memory_looked)
|
||||
|
||||
@ -81,6 +81,7 @@ pub fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
|
||||
TableWithColumns::new(
|
||||
Table::Arithmetic,
|
||||
cpu_arith_data_link(&ARITH_OPS, ®ISTER_MAP),
|
||||
vec![],
|
||||
Some(Column::sum(ARITH_OPS)),
|
||||
)
|
||||
}
|
||||
|
||||
@ -118,6 +118,7 @@ pub fn ctl_arithmetic_base_rows<F: Field>() -> TableWithColumns<F> {
|
||||
TableWithColumns::new(
|
||||
Table::Cpu,
|
||||
ctl_data_ternops(&OPS, false),
|
||||
vec![],
|
||||
Some(Column::sum(OPS)),
|
||||
)
|
||||
}
|
||||
@ -149,6 +150,7 @@ pub fn ctl_arithmetic_shift_rows<F: Field>() -> TableWithColumns<F> {
|
||||
TableWithColumns::new(
|
||||
Table::Cpu,
|
||||
ctl_data_ternops(&OPS, true),
|
||||
vec![],
|
||||
Some(Column::sum([COL_MAP.op.shl, COL_MAP.op.shr])),
|
||||
)
|
||||
}
|
||||
|
||||
@ -141,15 +141,22 @@ impl<F: Field> Column<F> {
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct TableWithColumns<F: Field> {
|
||||
table: Table,
|
||||
columns: Vec<Column<F>>,
|
||||
local_columns: Vec<Column<F>>,
|
||||
next_columns: Vec<Column<F>>,
|
||||
pub(crate) filter_column: Option<Column<F>>,
|
||||
}
|
||||
|
||||
impl<F: Field> TableWithColumns<F> {
|
||||
pub fn new(table: Table, columns: Vec<Column<F>>, filter_column: Option<Column<F>>) -> Self {
|
||||
pub fn new(
|
||||
table: Table,
|
||||
local_columns: Vec<Column<F>>,
|
||||
next_columns: Vec<Column<F>>,
|
||||
filter_column: Option<Column<F>>,
|
||||
) -> Self {
|
||||
Self {
|
||||
table,
|
||||
columns,
|
||||
local_columns,
|
||||
next_columns,
|
||||
filter_column,
|
||||
}
|
||||
}
|
||||
@ -168,7 +175,8 @@ impl<F: Field> CrossTableLookup<F> {
|
||||
) -> Self {
|
||||
assert!(looking_tables
|
||||
.iter()
|
||||
.all(|twc| twc.columns.len() == looked_table.columns.len()));
|
||||
.all(|twc| (twc.local_columns.len() + twc.next_columns.len())
|
||||
== (looked_table.local_columns.len() + looked_table.next_columns.len())));
|
||||
Self {
|
||||
looking_tables,
|
||||
looked_table,
|
||||
@ -196,7 +204,8 @@ pub struct CtlData<F: Field> {
|
||||
pub(crate) struct CtlZData<F: Field> {
|
||||
pub(crate) z: PolynomialValues<F>,
|
||||
pub(crate) challenge: GrandProductChallenge<F>,
|
||||
pub(crate) columns: Vec<Column<F>>,
|
||||
pub(crate) local_columns: Vec<Column<F>>,
|
||||
pub(crate) next_columns: Vec<Column<F>>,
|
||||
pub(crate) filter_column: Option<Column<F>>,
|
||||
}
|
||||
|
||||
@ -233,14 +242,16 @@ pub(crate) fn cross_table_lookup_data<F: RichField, const D: usize>(
|
||||
let zs_looking = looking_tables.iter().map(|table| {
|
||||
partial_products(
|
||||
&trace_poly_values[table.table as usize],
|
||||
&table.columns,
|
||||
&table.local_columns,
|
||||
&table.next_columns,
|
||||
&table.filter_column,
|
||||
challenge,
|
||||
)
|
||||
});
|
||||
let z_looked = partial_products(
|
||||
&trace_poly_values[looked_table.table as usize],
|
||||
&looked_table.columns,
|
||||
&looked_table.local_columns,
|
||||
&looked_table.next_columns,
|
||||
&looked_table.filter_column,
|
||||
challenge,
|
||||
);
|
||||
@ -250,7 +261,8 @@ pub(crate) fn cross_table_lookup_data<F: RichField, const D: usize>(
|
||||
.push(CtlZData {
|
||||
z,
|
||||
challenge,
|
||||
columns: table.columns.clone(),
|
||||
local_columns: table.local_columns.clone(),
|
||||
next_columns: table.next_columns.clone(),
|
||||
filter_column: table.filter_column.clone(),
|
||||
});
|
||||
}
|
||||
@ -259,7 +271,8 @@ pub(crate) fn cross_table_lookup_data<F: RichField, const D: usize>(
|
||||
.push(CtlZData {
|
||||
z: z_looked,
|
||||
challenge,
|
||||
columns: looked_table.columns.clone(),
|
||||
local_columns: looked_table.local_columns.clone(),
|
||||
next_columns: looked_table.next_columns.clone(),
|
||||
filter_column: looked_table.filter_column.clone(),
|
||||
});
|
||||
}
|
||||
@ -269,23 +282,31 @@ pub(crate) fn cross_table_lookup_data<F: RichField, const D: usize>(
|
||||
|
||||
fn partial_products<F: Field>(
|
||||
trace: &[PolynomialValues<F>],
|
||||
columns: &[Column<F>],
|
||||
local_columns: &[Column<F>],
|
||||
next_columns: &[Column<F>],
|
||||
filter_column: &Option<Column<F>>,
|
||||
challenge: GrandProductChallenge<F>,
|
||||
) -> PolynomialValues<F> {
|
||||
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 {
|
||||
F::ONE
|
||||
};
|
||||
if filter.is_one() {
|
||||
let evals = columns
|
||||
let evals = local_columns
|
||||
.iter()
|
||||
.map(|c| c.eval_table(trace, i))
|
||||
.chain(
|
||||
next_columns
|
||||
.iter()
|
||||
// The modulo is there to avoid out of bounds. For any CTL using next row
|
||||
// values, we expect the filter to be 0 at the last row.
|
||||
.map(|c| c.eval_table(trace, (i + 1) % degree)),
|
||||
)
|
||||
.collect::<Vec<_>>();
|
||||
partial_prod *= challenge.combine(evals.iter());
|
||||
} else {
|
||||
@ -293,6 +314,7 @@ fn partial_products<F: Field>(
|
||||
};
|
||||
res.push(partial_prod);
|
||||
}
|
||||
res.reverse();
|
||||
res.into()
|
||||
}
|
||||
|
||||
@ -306,7 +328,8 @@ where
|
||||
pub(crate) local_z: P,
|
||||
pub(crate) next_z: P,
|
||||
pub(crate) challenges: GrandProductChallenge<F>,
|
||||
pub(crate) columns: &'a [Column<F>],
|
||||
pub(crate) local_columns: &'a [Column<F>],
|
||||
pub(crate) next_columns: &'a [Column<F>],
|
||||
pub(crate) filter_column: &'a Option<Column<F>>,
|
||||
}
|
||||
|
||||
@ -343,7 +366,8 @@ impl<'a, F: RichField + Extendable<D>, const D: usize>
|
||||
local_z: *looking_z,
|
||||
next_z: *looking_z_next,
|
||||
challenges,
|
||||
columns: &table.columns,
|
||||
local_columns: &table.local_columns,
|
||||
next_columns: &table.next_columns,
|
||||
filter_column: &table.filter_column,
|
||||
});
|
||||
}
|
||||
@ -353,7 +377,8 @@ impl<'a, F: RichField + Extendable<D>, const D: usize>
|
||||
local_z: *looked_z,
|
||||
next_z: *looked_z_next,
|
||||
challenges,
|
||||
columns: &looked_table.columns,
|
||||
local_columns: &looked_table.local_columns,
|
||||
next_columns: &looked_table.next_columns,
|
||||
filter_column: &looked_table.filter_column,
|
||||
});
|
||||
}
|
||||
@ -362,6 +387,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>],
|
||||
@ -377,30 +406,28 @@ pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const
|
||||
local_z,
|
||||
next_z,
|
||||
challenges,
|
||||
columns,
|
||||
local_columns,
|
||||
next_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 mut evals = local_columns
|
||||
.iter()
|
||||
.map(|c| c.eval(vars.local_values))
|
||||
.collect::<Vec<_>>();
|
||||
evals.extend(next_columns.iter().map(|c| c.eval(vars.next_values)));
|
||||
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);
|
||||
}
|
||||
}
|
||||
|
||||
@ -409,7 +436,8 @@ pub struct CtlCheckVarsTarget<'a, F: Field, const D: usize> {
|
||||
pub(crate) local_z: ExtensionTarget<D>,
|
||||
pub(crate) next_z: ExtensionTarget<D>,
|
||||
pub(crate) challenges: GrandProductChallenge<Target>,
|
||||
pub(crate) columns: &'a [Column<F>],
|
||||
pub(crate) local_columns: &'a [Column<F>],
|
||||
pub(crate) next_columns: &'a [Column<F>],
|
||||
pub(crate) filter_column: &'a Option<Column<F>>,
|
||||
}
|
||||
|
||||
@ -445,7 +473,8 @@ impl<'a, F: Field, const D: usize> CtlCheckVarsTarget<'a, F, D> {
|
||||
local_z: *looking_z,
|
||||
next_z: *looking_z_next,
|
||||
challenges,
|
||||
columns: &looking_table.columns,
|
||||
local_columns: &looking_table.local_columns,
|
||||
next_columns: &looking_table.next_columns,
|
||||
filter_column: &looking_table.filter_column,
|
||||
});
|
||||
}
|
||||
@ -457,7 +486,8 @@ impl<'a, F: Field, const D: usize> CtlCheckVarsTarget<'a, F, D> {
|
||||
local_z: *looked_z,
|
||||
next_z: *looked_z_next,
|
||||
challenges,
|
||||
columns: &looked_table.columns,
|
||||
local_columns: &looked_table.local_columns,
|
||||
next_columns: &looked_table.next_columns,
|
||||
filter_column: &looked_table.filter_column,
|
||||
});
|
||||
}
|
||||
@ -483,7 +513,8 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
|
||||
local_z,
|
||||
next_z,
|
||||
challenges,
|
||||
columns,
|
||||
local_columns,
|
||||
next_columns,
|
||||
filter_column,
|
||||
} = lookup_vars;
|
||||
|
||||
@ -493,11 +524,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 +534,35 @@ 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 mut evals = local_columns
|
||||
.iter()
|
||||
.map(|c| c.eval_circuit(builder, vars.local_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);
|
||||
evals.extend(
|
||||
next_columns
|
||||
.iter()
|
||||
.map(|c| c.eval_circuit(builder, vars.next_values)),
|
||||
);
|
||||
|
||||
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 CrossTableLookup {
|
||||
looking_tables,
|
||||
looked_table,
|
||||
@ -564,11 +591,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,
|
||||
@ -661,9 +688,15 @@ pub(crate) mod testutils {
|
||||
};
|
||||
if filter.is_one() {
|
||||
let row = table
|
||||
.columns
|
||||
.local_columns
|
||||
.iter()
|
||||
.map(|c| c.eval_table(trace, i))
|
||||
.chain(
|
||||
table
|
||||
.next_columns
|
||||
.iter()
|
||||
.map(|c| c.eval_table(trace, (i + 1) % trace[0].len())),
|
||||
)
|
||||
.collect::<Vec<_>>();
|
||||
multiset.entry(row).or_default().push((table.table, i));
|
||||
} else {
|
||||
|
||||
@ -510,7 +510,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,
|
||||
);
|
||||
|
||||
@ -763,7 +763,8 @@ mod tests {
|
||||
beta: F::ZERO,
|
||||
gamma: F::ZERO,
|
||||
},
|
||||
columns: vec![],
|
||||
local_columns: vec![],
|
||||
next_columns: vec![],
|
||||
filter_column: None,
|
||||
};
|
||||
let ctl_data = CtlData {
|
||||
|
||||
@ -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],
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@ -433,7 +433,6 @@ where
|
||||
trace_commitment,
|
||||
&permutation_ctl_zs_commitment,
|
||||
"ient_commitment,
|
||||
degree_bits,
|
||||
stark.num_permutation_batches(config),
|
||||
);
|
||||
challenger.observe_openings(&openings.to_fri_openings());
|
||||
@ -448,7 +447,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,
|
||||
@ -570,7 +569,8 @@ where
|
||||
next_z: permutation_ctl_zs_commitment.get_lde_values_packed(i_next_start, step)
|
||||
[num_permutation_zs + i],
|
||||
challenges: zs_columns.challenge,
|
||||
columns: &zs_columns.columns,
|
||||
local_columns: &zs_columns.local_columns,
|
||||
next_columns: &zs_columns.next_columns,
|
||||
filter_column: &zs_columns.filter_column,
|
||||
})
|
||||
.collect::<Vec<_>>();
|
||||
@ -688,7 +688,8 @@ fn check_constraints<'a, F, C, S, const D: usize>(
|
||||
local_z: permutation_ctl_zs_subgroup_evals[i][num_permutation_zs + iii],
|
||||
next_z: permutation_ctl_zs_subgroup_evals[i_next][num_permutation_zs + iii],
|
||||
challenges: zs_columns.challenge,
|
||||
columns: &zs_columns.columns,
|
||||
local_columns: &zs_columns.local_columns,
|
||||
next_columns: &zs_columns.next_columns,
|
||||
filter_column: &zs_columns.filter_column,
|
||||
})
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
@ -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),
|
||||
}
|
||||
|
||||
@ -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],
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
@ -128,7 +128,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,
|
||||
)
|
||||
@ -301,7 +303,7 @@ where
|
||||
next_values,
|
||||
permutation_ctl_zs,
|
||||
permutation_ctl_zs_next,
|
||||
ctl_zs_last,
|
||||
ctl_zs_first,
|
||||
quotient_polys,
|
||||
} = &proof.openings;
|
||||
let vars = StarkEvaluationVars {
|
||||
@ -367,8 +369,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(),
|
||||
@ -408,7 +409,7 @@ where
|
||||
next_values,
|
||||
permutation_ctl_zs,
|
||||
permutation_ctl_zs_next,
|
||||
ctl_zs_last,
|
||||
ctl_zs_first,
|
||||
quotient_polys,
|
||||
} = openings;
|
||||
|
||||
@ -425,7 +426,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(())
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user