mirror of
https://github.com/logos-storage/plonky2.git
synced 2026-01-11 10:13:09 +00:00
Merge pull request #564 from mir-protocol/ctl_linear_comb
Linear combinations as columns in CTL
This commit is contained in:
wborgeaud
GitHub
commit
31435944f1
@ -62,7 +62,7 @@ mod tests {
|
||||
use crate::config::StarkConfig;
|
||||
use crate::cpu::columns::{KECCAK_INPUT_LIMBS, KECCAK_OUTPUT_LIMBS};
|
||||
use crate::cpu::cpu_stark::CpuStark;
|
||||
use crate::cross_table_lookup::{CrossTableLookup, TableWithColumns};
|
||||
use crate::cross_table_lookup::{Column, CrossTableLookup, TableWithColumns};
|
||||
use crate::keccak::keccak_stark::{KeccakStark, NUM_INPUTS, NUM_ROUNDS};
|
||||
use crate::proof::AllProof;
|
||||
use crate::prover::prove;
|
||||
@ -98,8 +98,8 @@ mod tests {
|
||||
.map(|i| {
|
||||
(0..2 * NUM_INPUTS)
|
||||
.map(|j| {
|
||||
keccak_trace[keccak::registers::reg_input_limb(j)].values
|
||||
[(i + 1) * NUM_ROUNDS - 1]
|
||||
keccak::registers::reg_input_limb(j)
|
||||
.eval_table(&keccak_trace, (i + 1) * NUM_ROUNDS - 1)
|
||||
})
|
||||
.collect::<Vec<_>>()
|
||||
.try_into()
|
||||
@ -143,18 +143,19 @@ mod tests {
|
||||
let mut keccak_keccak_input_output = (0..2 * NUM_INPUTS)
|
||||
.map(keccak::registers::reg_input_limb)
|
||||
.collect::<Vec<_>>();
|
||||
keccak_keccak_input_output
|
||||
.extend((0..2 * NUM_INPUTS).map(keccak::registers::reg_output_limb));
|
||||
keccak_keccak_input_output.extend(Column::singles(
|
||||
(0..2 * NUM_INPUTS).map(keccak::registers::reg_output_limb),
|
||||
));
|
||||
let cross_table_lookups = vec![CrossTableLookup::new(
|
||||
vec![TableWithColumns::new(
|
||||
Table::Cpu,
|
||||
cpu_keccak_input_output,
|
||||
vec![cpu::columns::IS_KECCAK],
|
||||
Column::singles(cpu_keccak_input_output).collect(),
|
||||
Some(Column::single(cpu::columns::IS_KECCAK)),
|
||||
)],
|
||||
TableWithColumns::new(
|
||||
Table::Keccak,
|
||||
keccak_keccak_input_output,
|
||||
vec![keccak::registers::reg_step(NUM_ROUNDS - 1)],
|
||||
Some(Column::single(keccak::registers::reg_step(NUM_ROUNDS - 1))),
|
||||
),
|
||||
None,
|
||||
)];
|
||||
|
||||
@ -1,3 +1,5 @@
|
||||
use std::iter::repeat;
|
||||
|
||||
use anyhow::{ensure, Result};
|
||||
use itertools::Itertools;
|
||||
use plonky2::field::extension_field::{Extendable, FieldExtension};
|
||||
@ -21,42 +23,127 @@ use crate::proof::{StarkProofWithPublicInputs, StarkProofWithPublicInputsTarget}
|
||||
use crate::stark::Stark;
|
||||
use crate::vars::{StarkEvaluationTargets, StarkEvaluationVars};
|
||||
|
||||
/// Represent a linear combination of columns.
|
||||
#[derive(Clone)]
|
||||
pub struct TableWithColumns {
|
||||
table: Table,
|
||||
columns: Vec<usize>,
|
||||
/// Vector of columns `[c_1,...,c_k]` used as a filter using the sum `c_1 + ... + c_k`.
|
||||
/// An empty vector corresponds to no filter.
|
||||
filter_columns: Vec<usize>,
|
||||
pub struct Column<F: Field> {
|
||||
linear_combination: Vec<(usize, F)>,
|
||||
constant: F,
|
||||
}
|
||||
|
||||
impl TableWithColumns {
|
||||
pub fn new(table: Table, columns: Vec<usize>, filter_columns: Vec<usize>) -> Self {
|
||||
impl<F: Field> Column<F> {
|
||||
pub fn single(c: usize) -> Self {
|
||||
Self {
|
||||
linear_combination: vec![(c, F::ONE)],
|
||||
constant: F::ZERO,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn singles<I: IntoIterator<Item = usize>>(cs: I) -> impl Iterator<Item = Self> {
|
||||
cs.into_iter().map(Self::single)
|
||||
}
|
||||
|
||||
pub fn linear_combination_with_constant<I: IntoIterator<Item = (usize, F)>>(
|
||||
iter: I,
|
||||
constant: F,
|
||||
) -> Self {
|
||||
let v = iter.into_iter().collect::<Vec<_>>();
|
||||
assert!(!v.is_empty());
|
||||
debug_assert_eq!(
|
||||
filter_columns.iter().unique().count(),
|
||||
filter_columns.len(),
|
||||
"Duplicate filter columns."
|
||||
v.iter().map(|(c, _)| c).unique().count(),
|
||||
v.len(),
|
||||
"Duplicate columns."
|
||||
);
|
||||
Self {
|
||||
linear_combination: v,
|
||||
constant,
|
||||
}
|
||||
}
|
||||
|
||||
pub fn linear_combination<I: IntoIterator<Item = (usize, F)>>(iter: I) -> Self {
|
||||
Self::linear_combination_with_constant(iter, F::ZERO)
|
||||
}
|
||||
|
||||
pub fn le_bits<I: IntoIterator<Item = usize>>(cs: I) -> Self {
|
||||
Self::linear_combination(cs.into_iter().zip(F::TWO.powers()))
|
||||
}
|
||||
|
||||
pub fn sum<I: IntoIterator<Item = usize>>(cs: I) -> Self {
|
||||
Self::linear_combination(cs.into_iter().zip(repeat(F::ONE)))
|
||||
}
|
||||
|
||||
pub fn eval<FE, P, const D: usize>(&self, 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>()
|
||||
+ 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
|
||||
.iter()
|
||||
.map(|&(c, f)| table[c].values[row] * f)
|
||||
.sum::<F>()
|
||||
+ self.constant
|
||||
}
|
||||
|
||||
pub fn eval_circuit<const D: usize>(
|
||||
&self,
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
v: &[ExtensionTarget<D>],
|
||||
) -> ExtensionTarget<D>
|
||||
where
|
||||
F: RichField + Extendable<D>,
|
||||
{
|
||||
let pairs = self
|
||||
.linear_combination
|
||||
.iter()
|
||||
.map(|&(c, f)| {
|
||||
(
|
||||
v[c],
|
||||
builder.constant_extension(F::Extension::from_basefield(f)),
|
||||
)
|
||||
})
|
||||
.collect::<Vec<_>>();
|
||||
let constant = builder.constant_extension(F::Extension::from_basefield(self.constant));
|
||||
builder.inner_product_extension(F::ONE, constant, pairs)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct TableWithColumns<F: Field> {
|
||||
table: Table,
|
||||
columns: Vec<Column<F>>,
|
||||
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 {
|
||||
Self {
|
||||
table,
|
||||
columns,
|
||||
filter_columns,
|
||||
filter_column,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct CrossTableLookup<F: Field> {
|
||||
looking_tables: Vec<TableWithColumns>,
|
||||
looked_table: TableWithColumns,
|
||||
looking_tables: Vec<TableWithColumns<F>>,
|
||||
looked_table: TableWithColumns<F>,
|
||||
/// Default value if filters are not used.
|
||||
default: Option<Vec<F>>,
|
||||
}
|
||||
|
||||
impl<F: Field> CrossTableLookup<F> {
|
||||
pub fn new(
|
||||
looking_tables: Vec<TableWithColumns>,
|
||||
looked_table: TableWithColumns,
|
||||
looking_tables: Vec<TableWithColumns<F>>,
|
||||
looked_table: TableWithColumns<F>,
|
||||
default: Option<Vec<F>>,
|
||||
) -> Self {
|
||||
assert!(looking_tables
|
||||
@ -65,8 +152,8 @@ impl<F: Field> CrossTableLookup<F> {
|
||||
assert!(
|
||||
looking_tables
|
||||
.iter()
|
||||
.all(|twc| twc.filter_columns.is_empty() == default.is_some())
|
||||
&& default.is_some() == looked_table.filter_columns.is_empty(),
|
||||
.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 {
|
||||
@ -87,7 +174,7 @@ pub struct CtlData<F: Field> {
|
||||
pub(crate) challenges: GrandProductChallengeSet<F>,
|
||||
/// Vector of `(Z, columns, filter_columns)` where `Z` is a Z-polynomial for a lookup
|
||||
/// on columns `columns` with filter columns `filter_columns`.
|
||||
pub zs_columns: Vec<(PolynomialValues<F>, Vec<usize>, Vec<usize>)>,
|
||||
pub zs_columns: Vec<(PolynomialValues<F>, Vec<Column<F>>, Option<Column<F>>)>,
|
||||
}
|
||||
|
||||
impl<F: Field> CtlData<F> {
|
||||
@ -130,14 +217,14 @@ pub fn cross_table_lookup_data<F: RichField, C: GenericConfig<D, F = F>, const D
|
||||
partial_products(
|
||||
&trace_poly_values[table.table as usize],
|
||||
&table.columns,
|
||||
&table.filter_columns,
|
||||
&table.filter_column,
|
||||
challenge,
|
||||
)
|
||||
});
|
||||
let z_looked = partial_products(
|
||||
&trace_poly_values[looked_table.table as usize],
|
||||
&looked_table.columns,
|
||||
&looked_table.filter_columns,
|
||||
&looked_table.filter_column,
|
||||
challenge,
|
||||
);
|
||||
|
||||
@ -168,7 +255,7 @@ pub fn cross_table_lookup_data<F: RichField, C: GenericConfig<D, F = F>, const D
|
||||
ctl_data_per_table[table.table as usize].zs_columns.push((
|
||||
z,
|
||||
table.columns.clone(),
|
||||
table.filter_columns.clone(),
|
||||
table.filter_column.clone(),
|
||||
));
|
||||
}
|
||||
ctl_data_per_table[looked_table.table as usize]
|
||||
@ -176,7 +263,7 @@ pub fn cross_table_lookup_data<F: RichField, C: GenericConfig<D, F = F>, const D
|
||||
.push((
|
||||
z_looked,
|
||||
looked_table.columns.clone(),
|
||||
looked_table.filter_columns.clone(),
|
||||
looked_table.filter_column.clone(),
|
||||
));
|
||||
}
|
||||
}
|
||||
@ -185,21 +272,25 @@ pub fn cross_table_lookup_data<F: RichField, C: GenericConfig<D, F = F>, const D
|
||||
|
||||
fn partial_products<F: Field>(
|
||||
trace: &[PolynomialValues<F>],
|
||||
columns: &[usize],
|
||||
filter_columns: &[usize],
|
||||
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 {
|
||||
let filter = if filter_columns.is_empty() {
|
||||
F::ONE
|
||||
let filter = if let Some(column) = filter_column {
|
||||
column.eval_table(trace, i)
|
||||
} else {
|
||||
filter_columns.iter().map(|&j| trace[j].values[i]).sum()
|
||||
F::ONE
|
||||
};
|
||||
if filter.is_one() {
|
||||
partial_prod *= challenge.combine(columns.iter().map(|&j| &trace[j].values[i]));
|
||||
let evals = columns
|
||||
.iter()
|
||||
.map(|c| c.eval_table(trace, i))
|
||||
.collect::<Vec<_>>();
|
||||
partial_prod *= challenge.combine(evals.iter());
|
||||
} else {
|
||||
assert_eq!(filter, F::ZERO, "Non-binary filter?")
|
||||
};
|
||||
@ -218,8 +309,8 @@ where
|
||||
pub(crate) local_z: P,
|
||||
pub(crate) next_z: P,
|
||||
pub(crate) challenges: GrandProductChallenge<F>,
|
||||
pub(crate) columns: &'a [usize],
|
||||
pub(crate) filter_columns: &'a [usize],
|
||||
pub(crate) columns: &'a [Column<F>],
|
||||
pub(crate) filter_column: &'a Option<Column<F>>,
|
||||
}
|
||||
|
||||
impl<'a, F: RichField + Extendable<D>, const D: usize>
|
||||
@ -258,7 +349,7 @@ impl<'a, F: RichField + Extendable<D>, const D: usize>
|
||||
next_z: *looking_z_next,
|
||||
challenges,
|
||||
columns: &table.columns,
|
||||
filter_columns: &table.filter_columns,
|
||||
filter_column: &table.filter_column,
|
||||
});
|
||||
}
|
||||
|
||||
@ -268,7 +359,7 @@ impl<'a, F: RichField + Extendable<D>, const D: usize>
|
||||
next_z: *looked_z_next,
|
||||
challenges,
|
||||
columns: &looked_table.columns,
|
||||
filter_columns: &looked_table.filter_columns,
|
||||
filter_column: &looked_table.filter_column,
|
||||
});
|
||||
}
|
||||
}
|
||||
@ -293,14 +384,17 @@ pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, C, S, const D: usize, con
|
||||
next_z,
|
||||
challenges,
|
||||
columns,
|
||||
filter_columns,
|
||||
filter_column,
|
||||
} = lookup_vars;
|
||||
let combine = |v: &[P]| -> P { challenges.combine(columns.iter().map(|&i| &v[i])) };
|
||||
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 filter_columns.is_empty() {
|
||||
P::ONES
|
||||
if let Some(column) = filter_column {
|
||||
column.eval(v)
|
||||
} else {
|
||||
filter_columns.iter().map(|&i| v[i]).sum()
|
||||
P::ONES
|
||||
}
|
||||
};
|
||||
let local_filter = filter(vars.local_values);
|
||||
@ -317,16 +411,16 @@ pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, C, S, const D: usize, con
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct CtlCheckVarsTarget<'a, const D: usize> {
|
||||
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 [usize],
|
||||
pub(crate) filter_columns: &'a [usize],
|
||||
pub(crate) columns: &'a [Column<F>],
|
||||
pub(crate) filter_column: &'a Option<Column<F>>,
|
||||
}
|
||||
|
||||
impl<'a, const D: usize> CtlCheckVarsTarget<'a, D> {
|
||||
pub(crate) fn from_proofs<F: Field>(
|
||||
impl<'a, F: Field, const D: usize> CtlCheckVarsTarget<'a, F, D> {
|
||||
pub(crate) fn from_proofs(
|
||||
proofs: &[StarkProofWithPublicInputsTarget<D>],
|
||||
cross_table_lookups: &'a [CrossTableLookup<F>],
|
||||
ctl_challenges: &'a GrandProductChallengeSet<Target>,
|
||||
@ -359,7 +453,7 @@ impl<'a, const D: usize> CtlCheckVarsTarget<'a, D> {
|
||||
next_z: *looking_z_next,
|
||||
challenges,
|
||||
columns: &table.columns,
|
||||
filter_columns: &table.filter_columns,
|
||||
filter_column: &table.filter_column,
|
||||
});
|
||||
}
|
||||
|
||||
@ -369,7 +463,7 @@ impl<'a, const D: usize> CtlCheckVarsTarget<'a, D> {
|
||||
next_z: *looked_z_next,
|
||||
challenges,
|
||||
columns: &looked_table.columns,
|
||||
filter_columns: &looked_table.filter_columns,
|
||||
filter_column: &looked_table.filter_column,
|
||||
});
|
||||
}
|
||||
}
|
||||
@ -384,7 +478,7 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
|
||||
>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
vars: StarkEvaluationTargets<D, { S::COLUMNS }, { S::PUBLIC_INPUTS }>,
|
||||
ctl_vars: &[CtlCheckVarsTarget<D>],
|
||||
ctl_vars: &[CtlCheckVarsTarget<F, D>],
|
||||
consumer: &mut RecursiveConstraintConsumer<F, D>,
|
||||
) {
|
||||
for lookup_vars in ctl_vars {
|
||||
@ -393,19 +487,19 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
|
||||
next_z,
|
||||
challenges,
|
||||
columns,
|
||||
filter_columns,
|
||||
filter_column,
|
||||
} = lookup_vars;
|
||||
|
||||
let one = builder.one_extension();
|
||||
let local_filter = if filter_columns.is_empty() {
|
||||
one
|
||||
let local_filter = if let Some(column) = filter_column {
|
||||
column.eval_circuit(builder, vars.local_values)
|
||||
} else {
|
||||
builder.add_many_extension(filter_columns.iter().map(|&i| vars.local_values[i]))
|
||||
one
|
||||
};
|
||||
let next_filter = if filter_columns.is_empty() {
|
||||
one
|
||||
let next_filter = if let Some(column) = filter_column {
|
||||
column.eval_circuit(builder, vars.next_values)
|
||||
} else {
|
||||
builder.add_many_extension(filter_columns.iter().map(|&i| vars.next_values[i]))
|
||||
one
|
||||
};
|
||||
fn select<F: RichField + Extendable<D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
@ -418,24 +512,20 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
|
||||
}
|
||||
|
||||
// Check value of `Z(1)`
|
||||
let combined_local = challenges.combine_circuit(
|
||||
builder,
|
||||
&columns
|
||||
.iter()
|
||||
.map(|&i| vars.local_values[i])
|
||||
.collect::<Vec<_>>(),
|
||||
);
|
||||
let local_columns_eval = 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 combined_next = challenges.combine_circuit(
|
||||
builder,
|
||||
&columns
|
||||
.iter()
|
||||
.map(|&i| vars.next_values[i])
|
||||
.collect::<Vec<_>>(),
|
||||
);
|
||||
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 mut transition = builder.mul_extension(*local_z, selected_next);
|
||||
transition = builder.sub_extension(*next_z, transition);
|
||||
|
||||
@ -17,7 +17,7 @@ use crate::keccak::logic::{
|
||||
};
|
||||
use crate::keccak::registers::{
|
||||
reg_a, reg_a_prime, reg_a_prime_prime, reg_a_prime_prime_0_0_bit, reg_a_prime_prime_prime,
|
||||
reg_b, reg_c, reg_c_partial, reg_input_limb, reg_step, NUM_REGISTERS,
|
||||
reg_b, reg_c, reg_c_partial, reg_step, NUM_REGISTERS,
|
||||
};
|
||||
use crate::keccak::round_flags::{eval_round_flags, eval_round_flags_recursively};
|
||||
use crate::stark::Stark;
|
||||
@ -62,7 +62,6 @@ impl<F: RichField + Extendable<D>, const D: usize> KeccakStark<F, D> {
|
||||
fn generate_trace_rows_for_perm(&self, input: [u64; NUM_INPUTS]) -> Vec<[F; NUM_REGISTERS]> {
|
||||
let mut rows = vec![[F::ZERO; NUM_REGISTERS]; NUM_ROUNDS];
|
||||
|
||||
self.copy_input(input, &mut rows[0]);
|
||||
for x in 0..5 {
|
||||
for y in 0..5 {
|
||||
let input_xy = input[x * 5 + y];
|
||||
@ -74,7 +73,6 @@ impl<F: RichField + Extendable<D>, const D: usize> KeccakStark<F, D> {
|
||||
|
||||
self.generate_trace_row_for_round(&mut rows[0], 0);
|
||||
for round in 1..24 {
|
||||
self.copy_input(input, &mut rows[round]);
|
||||
self.copy_output_to_input(rows[round - 1], &mut rows[round]);
|
||||
self.generate_trace_row_for_round(&mut rows[round], round);
|
||||
}
|
||||
@ -187,14 +185,6 @@ impl<F: RichField + Extendable<D>, const D: usize> KeccakStark<F, D> {
|
||||
row[out_reg_hi] = F::from_canonical_u64(row[in_reg_hi].to_canonical_u64() ^ rc_hi);
|
||||
}
|
||||
|
||||
fn copy_input(&self, input: [u64; NUM_INPUTS], row: &mut [F; NUM_REGISTERS]) {
|
||||
for i in 0..NUM_INPUTS {
|
||||
let (low, high) = (input[i] as u32, input[i] >> 32);
|
||||
row[reg_input_limb(2 * i)] = F::from_canonical_u32(low);
|
||||
row[reg_input_limb(2 * i + 1)] = F::from_canonical_u64(high);
|
||||
}
|
||||
}
|
||||
|
||||
pub fn generate_trace(&self, inputs: Vec<[u64; NUM_INPUTS]>) -> Vec<PolynomialValues<F>> {
|
||||
let mut timing = TimingTree::new("generate trace", log::Level::Debug);
|
||||
|
||||
@ -230,23 +220,6 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for KeccakStark<F
|
||||
{
|
||||
eval_round_flags(vars, yield_constr);
|
||||
|
||||
for i in 0..2 * NUM_INPUTS {
|
||||
let local_input_limb = vars.local_values[reg_input_limb(i)];
|
||||
let next_input_limb = vars.next_values[reg_input_limb(i)];
|
||||
let is_last_round = vars.local_values[reg_step(NUM_ROUNDS - 1)];
|
||||
// Constrain the input registers to be equal throughout the rounds of a permutation.
|
||||
yield_constr.constraint_transition(
|
||||
(P::ONES - is_last_round) * (next_input_limb - local_input_limb),
|
||||
);
|
||||
|
||||
// Verify that the bit decomposition is done correctly.
|
||||
let range = if i % 2 == 0 { 0..32 } else { 32..64 };
|
||||
let bits = range.map(|j| vars.local_values[reg_a((i / 2) / 5, (i / 2) % 5, j)]);
|
||||
let expected_input_limb = bits.rev().fold(P::ZEROS, |acc, b| acc.doubles() + b);
|
||||
let is_first_round = vars.local_values[reg_step(0)];
|
||||
yield_constr.constraint(is_first_round * (local_input_limb - expected_input_limb));
|
||||
}
|
||||
|
||||
// C_partial[x] = xor(A[x, 0], A[x, 1], A[x, 2])
|
||||
for x in 0..5 {
|
||||
for z in 0..64 {
|
||||
@ -390,25 +363,6 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for KeccakStark<F
|
||||
|
||||
eval_round_flags_recursively(builder, vars, yield_constr);
|
||||
|
||||
for i in 0..2 * NUM_INPUTS {
|
||||
let local_input_limb = vars.local_values[reg_input_limb(i)];
|
||||
let next_input_limb = vars.next_values[reg_input_limb(i)];
|
||||
let is_last_round = vars.local_values[reg_step(NUM_ROUNDS - 1)];
|
||||
let diff = builder.sub_extension(local_input_limb, next_input_limb);
|
||||
let constraint = builder.mul_sub_extension(is_last_round, diff, diff);
|
||||
yield_constr.constraint_transition(builder, constraint);
|
||||
|
||||
let range = if i % 2 == 0 { 0..32 } else { 32..64 };
|
||||
let bits = range
|
||||
.map(|j| vars.local_values[reg_a((i / 2) / 5, (i / 2) % 5, j)])
|
||||
.collect::<Vec<_>>();
|
||||
let expected_input_limb = reduce_with_powers_ext_circuit(builder, &bits, two);
|
||||
let is_first_round = vars.local_values[reg_step(0)];
|
||||
let diff = builder.sub_extension(local_input_limb, expected_input_limb);
|
||||
let constraint = builder.mul_extension(is_first_round, diff);
|
||||
yield_constr.constraint(builder, constraint);
|
||||
}
|
||||
|
||||
// C_partial[x] = xor(A[x, 0], A[x, 1], A[x, 2])
|
||||
for x in 0..5 {
|
||||
for z in 0..64 {
|
||||
|
||||
@ -1,3 +1,6 @@
|
||||
use plonky2::field::field_types::Field;
|
||||
|
||||
use crate::cross_table_lookup::Column;
|
||||
use crate::keccak::keccak_stark::{NUM_INPUTS, NUM_ROUNDS};
|
||||
|
||||
/// A register which is set to 1 if we are in the `i`th round, otherwise 0.
|
||||
@ -9,9 +12,11 @@ pub const fn reg_step(i: usize) -> usize {
|
||||
/// Registers to hold permutation inputs.
|
||||
/// `reg_input_limb(2*i) -> input[i] as u32`
|
||||
/// `reg_input_limb(2*i+1) -> input[i] >> 32`
|
||||
pub const fn reg_input_limb(i: usize) -> usize {
|
||||
pub fn reg_input_limb<F: Field>(i: usize) -> Column<F> {
|
||||
debug_assert!(i < 2 * NUM_INPUTS);
|
||||
NUM_ROUNDS + i
|
||||
let range = if i % 2 == 0 { 0..32 } else { 32..64 };
|
||||
let bits = range.map(|j| reg_a((i / 2) / 5, (i / 2) % 5, j));
|
||||
Column::le_bits(bits)
|
||||
}
|
||||
|
||||
/// Registers to hold permutation outputs.
|
||||
@ -37,7 +42,7 @@ const R: [[u8; 5]; 5] = [
|
||||
[27, 20, 39, 8, 14],
|
||||
];
|
||||
|
||||
const START_A: usize = NUM_ROUNDS + 2 * NUM_INPUTS;
|
||||
const START_A: usize = NUM_ROUNDS;
|
||||
pub(crate) const fn reg_a(x: usize, y: usize, z: usize) -> usize {
|
||||
debug_assert!(x < 5);
|
||||
debug_assert!(y < 5);
|
||||
|
||||
@ -41,7 +41,6 @@ pub fn prove<F, C, const D: usize>(
|
||||
where
|
||||
F: RichField + Extendable<D>,
|
||||
C: GenericConfig<D, F = F>,
|
||||
[(); <<F as Packable>::Packing>::WIDTH]:,
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
[(); CpuStark::<F, D>::COLUMNS]:,
|
||||
[(); CpuStark::<F, D>::PUBLIC_INPUTS]:,
|
||||
@ -139,7 +138,6 @@ where
|
||||
F: RichField + Extendable<D>,
|
||||
C: GenericConfig<D, F = F>,
|
||||
S: Stark<F, D>,
|
||||
[(); <<F as Packable>::Packing>::WIDTH]:,
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
[(); S::COLUMNS]:,
|
||||
[(); S::PUBLIC_INPUTS]:,
|
||||
@ -313,7 +311,6 @@ where
|
||||
S: Stark<F, D>,
|
||||
[(); S::COLUMNS]:,
|
||||
[(); S::PUBLIC_INPUTS]:,
|
||||
[(); P::WIDTH]:,
|
||||
{
|
||||
let degree = 1 << degree_bits;
|
||||
let rate_bits = config.fri_config.rate_bits;
|
||||
@ -392,14 +389,14 @@ where
|
||||
.iter()
|
||||
.enumerate()
|
||||
.map(
|
||||
|(i, (_, columns, filter_columns))| CtlCheckVars::<F, F, P, 1> {
|
||||
|(i, (_, columns, filter_column))| CtlCheckVars::<F, F, P, 1> {
|
||||
local_z: permutation_ctl_zs_commitment.get_lde_values_packed(i_start, step)
|
||||
[num_permutation_zs + i],
|
||||
next_z: permutation_ctl_zs_commitment
|
||||
.get_lde_values_packed(i_next_start, step)[num_permutation_zs + i],
|
||||
challenges: ctl_data.challenges.challenges[i % config.num_challenges],
|
||||
columns,
|
||||
filter_columns,
|
||||
filter_column,
|
||||
},
|
||||
)
|
||||
.collect::<Vec<_>>();
|
||||
@ -510,14 +507,14 @@ fn check_constraints<'a, F, C, S, const D: usize>(
|
||||
.iter()
|
||||
.enumerate()
|
||||
.map(
|
||||
|(iii, (_, columns, filter_columns))| CtlCheckVars::<F, F, F, 1> {
|
||||
|(iii, (_, columns, filter_column))| CtlCheckVars::<F, F, F, 1> {
|
||||
local_z: get_comm_values(permutation_ctl_zs_commitment, i)
|
||||
[num_permutation_zs + iii],
|
||||
next_z: get_comm_values(permutation_ctl_zs_commitment, i_next)
|
||||
[num_permutation_zs + iii],
|
||||
challenges: ctl_data.challenges.challenges[iii % config.num_challenges],
|
||||
columns,
|
||||
filter_columns,
|
||||
filter_column,
|
||||
},
|
||||
)
|
||||
.collect::<Vec<_>>();
|
||||
|
||||
@ -100,7 +100,7 @@ fn verify_stark_proof_with_challenges_circuit<
|
||||
stark: S,
|
||||
proof_with_pis: &StarkProofWithPublicInputsTarget<D>,
|
||||
challenges: &StarkProofChallengesTarget<D>,
|
||||
ctl_vars: &[CtlCheckVarsTarget<D>],
|
||||
ctl_vars: &[CtlCheckVarsTarget<F, D>],
|
||||
inner_config: &StarkConfig,
|
||||
) where
|
||||
C::Hasher: AlgebraicHasher<F>,
|
||||
|
||||
@ -50,7 +50,7 @@ pub(crate) fn eval_vanishing_poly_circuit<F, C, S, const D: usize>(
|
||||
config: &StarkConfig,
|
||||
vars: StarkEvaluationTargets<D, { S::COLUMNS }, { S::PUBLIC_INPUTS }>,
|
||||
permutation_data: Option<PermutationCheckDataTarget<D>>,
|
||||
ctl_vars: &[CtlCheckVarsTarget<D>],
|
||||
ctl_vars: &[CtlCheckVarsTarget<F, D>],
|
||||
consumer: &mut RecursiveConstraintConsumer<F, D>,
|
||||
) where
|
||||
F: RichField + Extendable<D>,
|
||||
|
||||
@ -42,7 +42,6 @@ where
|
||||
S: Stark<F, D>,
|
||||
[(); S::COLUMNS]:,
|
||||
[(); S::PUBLIC_INPUTS]:,
|
||||
[(); <<F as Packable>::Packing>::WIDTH]:,
|
||||
[(); C::Hasher::HASH_SIZE]:,
|
||||
{
|
||||
let degree = trace_poly_values[0].len();
|
||||
@ -216,7 +215,6 @@ where
|
||||
S: Stark<F, D>,
|
||||
[(); S::COLUMNS]:,
|
||||
[(); S::PUBLIC_INPUTS]:,
|
||||
[(); P::WIDTH]:,
|
||||
{
|
||||
let degree = 1 << degree_bits;
|
||||
let rate_bits = config.fri_config.rate_bits;
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user