Skip to content

Commit

Permalink
Add final lookup constraint. (#667)
Browse files Browse the repository at this point in the history
  • Loading branch information
@alonh5
alonh5 authored Jul 8, 2024
1 parent 71c2e00 commit 6761408
Show file tree
Hide file tree
Showing 2 changed files with 95 additions and 28 deletions.
31 changes: 28 additions & 3 deletions crates/prover/src/examples/wide_fibonacci/component.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,13 +91,14 @@ impl WideFibComponent {
}
}

fn evaluate_lookup_boundary_constraint_at_point(
fn evaluate_lookup_boundary_constraints_at_point(
&self,
point: CirclePoint<SecureField>,
mask: &TreeVec<Vec<Vec<SecureField>>>,
evaluation_accumulator: &mut PointEvaluationAccumulator,
constraint_zero_domain: Coset,
interaction_elements: &InteractionElements,
lookup_values: &LookupValues,
) {
let (alpha, z) = (interaction_elements[ALPHA_ID], interaction_elements[Z_ID]);
let value =
Expand All @@ -116,6 +117,29 @@ impl WideFibComponent {
- shifted_secure_combination(&[mask[0][0][0], mask[0][1][0]], alpha, z);
let denom = point_vanishing(constraint_zero_domain.at(0), point);
evaluation_accumulator.accumulate(numerator / denom);

let numerator = (value
* shifted_secure_combination(
&[
lookup_values[LOOKUP_VALUE_N_MINUS_2_ID],
lookup_values[LOOKUP_VALUE_N_MINUS_1_ID],
],
alpha,
z,
))
- shifted_secure_combination(
&[
lookup_values[LOOKUP_VALUE_0_ID],
lookup_values[LOOKUP_VALUE_1_ID],
],
alpha,
z,
);
let denom = point_vanishing(
constraint_zero_domain.at(constraint_zero_domain.size() - 1),
point,
);
evaluation_accumulator.accumulate(numerator / denom);
}

fn evaluate_lookup_step_constraints_at_point(
Expand Down Expand Up @@ -163,7 +187,7 @@ impl Air for WideFibAir {

impl Component for WideFibComponent {
fn n_constraints(&self) -> usize {
self.n_columns() + 4
self.n_columns() + 5
}

fn max_constraint_log_degree_bound(&self) -> u32 {
Expand Down Expand Up @@ -219,12 +243,13 @@ impl Component for WideFibComponent {
constraint_zero_domain,
interaction_elements,
);
self.evaluate_lookup_boundary_constraint_at_point(
self.evaluate_lookup_boundary_constraints_at_point(
point,
mask,
evaluation_accumulator,
constraint_zero_domain,
interaction_elements,
lookup_values,
);
self.evaluate_trace_step_constraints_at_point(
point,
Expand Down
92 changes: 67 additions & 25 deletions crates/prover/src/examples/wide_fibonacci/constraint_eval.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,19 +88,23 @@ impl WideFibComponent {
BaseField::batch_inverse(&last_point_denoms, &mut last_point_denom_inverses);
let mut first_point_numerators = vec![SecureField::zero(); 1 << (max_constraint_degree)];
let mut last_point_numerators = vec![SecureField::zero(); 1 << (max_constraint_degree)];
let (lookup_value_0, lookup_value_1, lookup_value_n_minus_2, lookup_value_n_minus_1) = (
lookup_values[LOOKUP_VALUE_0_ID],
lookup_values[LOOKUP_VALUE_1_ID],
lookup_values[LOOKUP_VALUE_N_MINUS_2_ID],
lookup_values[LOOKUP_VALUE_N_MINUS_1_ID],
);

#[allow(clippy::needless_range_loop)]
for i in 0..trace_eval_domain.size() {
first_point_numerators[i] = accum.random_coeff_powers[self.n_columns() + 3]
* (trace_evals[0][0][i] - lookup_values[LOOKUP_VALUE_0_ID])
+ accum.random_coeff_powers[self.n_columns() + 2]
* (trace_evals[0][1][i] - lookup_values[LOOKUP_VALUE_1_ID]);
last_point_numerators[i] = accum.random_coeff_powers[self.n_columns() + 1]
* (trace_evals[0][self.n_columns() - 2][i]
- lookup_values[LOOKUP_VALUE_N_MINUS_2_ID])
+ accum.random_coeff_powers[self.n_columns()]
* (trace_evals[0][self.n_columns() - 1][i]
- lookup_values[LOOKUP_VALUE_N_MINUS_1_ID]);
first_point_numerators[i] = accum.random_coeff_powers[self.n_columns() + 4]
* (trace_evals[0][0][i] - lookup_value_0)
+ accum.random_coeff_powers[self.n_columns() + 3]
* (trace_evals[0][1][i] - lookup_value_1);
last_point_numerators[i] = accum.random_coeff_powers[self.n_columns() + 2]
* (trace_evals[0][self.n_columns() - 2][i] - lookup_value_n_minus_2)
+ accum.random_coeff_powers[self.n_columns() + 1]
* (trace_evals[0][self.n_columns() - 1][i] - lookup_value_n_minus_1);
}
for (i, (num, denom_inverse)) in first_point_numerators
.iter()
Expand Down Expand Up @@ -148,32 +152,48 @@ impl WideFibComponent {
}
}

fn evaluate_lookup_boundary_constraint(
fn evaluate_lookup_boundary_constraints(
&self,
trace_evals: &TreeVec<Vec<&CircleEvaluation<CpuBackend, BaseField, BitReversedOrder>>>,
trace_eval_domain: CircleDomain,
zero_domain: Coset,
accum: &mut ColumnAccumulator<'_, CpuBackend>,
interaction_elements: &InteractionElements,
lookup_values: &LookupValues,
) {
let max_constraint_degree = self.max_constraint_log_degree_bound();
let mut denoms = vec![];
let mut first_point_denoms = vec![];
let mut last_point_denoms = vec![];
for point in trace_eval_domain.iter() {
denoms.push(point_vanishing(zero_domain.at(0), point));
first_point_denoms.push(point_vanishing(zero_domain.at(0), point));
last_point_denoms.push(point_vanishing(
zero_domain.at(zero_domain.size() - 1),
point,
));
}
bit_reverse(&mut denoms);
let mut denom_inverses = vec![BaseField::zero(); 1 << (max_constraint_degree)];
BaseField::batch_inverse(&denoms, &mut denom_inverses);
let mut numerators = vec![SecureField::zero(); 1 << (max_constraint_degree)];
bit_reverse(&mut first_point_denoms);
bit_reverse(&mut last_point_denoms);
let mut first_point_denom_inverses = vec![BaseField::zero(); 1 << (max_constraint_degree)];
let mut last_point_denom_inverses = vec![BaseField::zero(); 1 << (max_constraint_degree)];
BaseField::batch_inverse(&first_point_denoms, &mut first_point_denom_inverses);
BaseField::batch_inverse(&last_point_denoms, &mut last_point_denom_inverses);
let mut first_point_numerators = vec![SecureField::zero(); 1 << (max_constraint_degree)];
let mut last_point_numerators = vec![SecureField::zero(); 1 << (max_constraint_degree)];
let (alpha, z) = (interaction_elements[ALPHA_ID], interaction_elements[Z_ID]);
let (lookup_value_0, lookup_value_1, lookup_value_n_minus_2, lookup_value_n_minus_1) = (
lookup_values[LOOKUP_VALUE_0_ID],
lookup_values[LOOKUP_VALUE_1_ID],
lookup_values[LOOKUP_VALUE_N_MINUS_2_ID],
lookup_values[LOOKUP_VALUE_N_MINUS_1_ID],
);

#[allow(clippy::needless_range_loop)]
for i in 0..trace_eval_domain.size() {
let value =
SecureCirclePoly::<CpuBackend>::eval_from_partial_evals(std::array::from_fn(|j| {
trace_evals[1][j][i].into()
}));
numerators[i] = accum.random_coeff_powers[self.n_columns() - 2]
first_point_numerators[i] = accum.random_coeff_powers[self.n_columns() - 1]
* ((value
* shifted_secure_combination(
&[
Expand All @@ -188,8 +208,27 @@ impl WideFibComponent {
alpha,
z,
));
last_point_numerators[i] = accum.random_coeff_powers[self.n_columns() - 2]
* ((value
* shifted_secure_combination(
&[lookup_value_n_minus_2, lookup_value_n_minus_1],
alpha,
z,
))
- shifted_secure_combination(&[lookup_value_0, lookup_value_1], alpha, z));
}
for (i, (num, denom_inverse)) in numerators.iter().zip(denom_inverses.iter()).enumerate() {
for (i, (num, denom_inverse)) in first_point_numerators
.iter()
.zip(first_point_denom_inverses.iter())
.enumerate()
{
accum.accumulate(i, *num * *denom_inverse);
}
for (i, (num, denom_inverse)) in last_point_numerators
.iter()
.zip(last_point_denom_inverses.iter())
.enumerate()
{
accum.accumulate(i, *num * *denom_inverse);
}
}
Expand Down Expand Up @@ -231,7 +270,7 @@ impl WideFibComponent {
SecureCirclePoly::<CpuBackend>::eval_from_partial_evals(std::array::from_fn(|j| {
trace_evals[1][j][prev_index].into()
}));
numerators[i] = accum.random_coeff_powers[self.n_columns() - 1]
numerators[i] = accum.random_coeff_powers[self.n_columns()]
* ((value
* shifted_secure_combination(
&[
Expand Down Expand Up @@ -269,33 +308,36 @@ impl ComponentProver<CpuBackend> for WideFibComponent {
let [mut accum] =
evaluation_accumulator.columns([(max_constraint_degree, self.n_constraints())]);

// TODO(AlonH): Evaluate the numerators together and the denominators together (i.e. in the
// same for loop)
self.evaluate_trace_boundary_constraints(
trace_evals,
trace_eval_domain,
zero_domain,
&mut accum,
lookup_values,
);
self.evaluate_trace_step_constraints(
self.evaluate_lookup_step_constraints(
trace_evals,
trace_eval_domain,
zero_domain,
&mut accum,
interaction_elements,
);
self.evaluate_lookup_boundary_constraint(
self.evaluate_lookup_boundary_constraints(
trace_evals,
trace_eval_domain,
zero_domain,
&mut accum,
interaction_elements,
lookup_values,
);
self.evaluate_lookup_step_constraints(
self.evaluate_trace_step_constraints(
trace_evals,
trace_eval_domain,
zero_domain,
&mut accum,
interaction_elements,
)
);
}

fn lookup_values(&self, trace: &ComponentTrace<'_, CpuBackend>) -> LookupValues {
Expand Down

0 comments on commit 6761408

Please sign in to comment.