Skip to content

Commit

Permalink
Complete create_proof refactor for fe-be split
Browse files Browse the repository at this point in the history
  • Loading branch information
ed255 committed Dec 14, 2023
1 parent 4510059 commit 1b35fab
Show file tree
Hide file tree
Showing 6 changed files with 1,506 additions and 58 deletions.
2 changes: 1 addition & 1 deletion halo2_proofs/src/plonk/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1704,8 +1704,8 @@ impl<F: Field> ConstraintSystemV2Backend<F> {
let max_phase = self
.advice_column_phase
.iter()
.cloned()
.max()
.map(|phase| phase.0)
.unwrap_or_default();
(0..=max_phase).collect()
}
Expand Down
313 changes: 312 additions & 1 deletion halo2_proofs/src/plonk/evaluation.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use crate::multicore;
use crate::plonk::{lookup, permutation, Any, ProvingKey};
use crate::plonk::{lookup, permutation, Any, ProvingKey, ProvingKeyV2};
use crate::poly::Basis;
use crate::{
arithmetic::{parallelize, CurveAffine},
Expand Down Expand Up @@ -383,6 +383,317 @@ impl<C: CurveAffine> Evaluator<C> {
ev
}

/// Evaluate h poly
// NOTE: Copy of evaluate_h with ProvingKeyV2
#[allow(clippy::too_many_arguments)]
pub(in crate::plonk) fn evaluate_h_v2(
&self,
pk: &ProvingKeyV2<C>,
advice_polys: &[&[Polynomial<C::ScalarExt, Coeff>]],
instance_polys: &[&[Polynomial<C::ScalarExt, Coeff>]],
challenges: &[C::ScalarExt],
y: C::ScalarExt,
beta: C::ScalarExt,
gamma: C::ScalarExt,
theta: C::ScalarExt,
lookups: &[Vec<lookup::prover::Committed<C>>],
shuffles: &[Vec<shuffle::prover::Committed<C>>],
permutations: &[permutation::prover::Committed<C>],
) -> Polynomial<C::ScalarExt, ExtendedLagrangeCoeff> {
let domain = &pk.vk.domain;
let size = domain.extended_len();
let rot_scale = 1 << (domain.extended_k() - domain.k());
let fixed = &pk.fixed_cosets[..];
let extended_omega = domain.get_extended_omega();
let isize = size as i32;
let one = C::ScalarExt::ONE;
let l0 = &pk.l0;
let l_last = &pk.l_last;
let l_active_row = &pk.l_active_row;
let p = &pk.vk.cs.permutation;

// Calculate the advice and instance cosets
let advice: Vec<Vec<Polynomial<C::Scalar, ExtendedLagrangeCoeff>>> = advice_polys
.iter()
.map(|advice_polys| {
advice_polys
.iter()
.map(|poly| domain.coeff_to_extended(poly.clone()))
.collect()
})
.collect();
let instance: Vec<Vec<Polynomial<C::Scalar, ExtendedLagrangeCoeff>>> = instance_polys
.iter()
.map(|instance_polys| {
instance_polys
.iter()
.map(|poly| domain.coeff_to_extended(poly.clone()))
.collect()
})
.collect();

let mut values = domain.empty_extended();

// Core expression evaluations
let num_threads = multicore::current_num_threads();
for ((((advice, instance), lookups), shuffles), permutation) in advice
.iter()
.zip(instance.iter())
.zip(lookups.iter())
.zip(shuffles.iter())
.zip(permutations.iter())
{
// Custom gates
multicore::scope(|scope| {
let chunk_size = (size + num_threads - 1) / num_threads;
for (thread_idx, values) in values.chunks_mut(chunk_size).enumerate() {
let start = thread_idx * chunk_size;
scope.spawn(move |_| {
let mut eval_data = self.custom_gates.instance();
for (i, value) in values.iter_mut().enumerate() {
let idx = start + i;
*value = self.custom_gates.evaluate(
&mut eval_data,
fixed,
advice,
instance,
challenges,
&beta,
&gamma,
&theta,
&y,
value,
idx,
rot_scale,
isize,
);
}
});
}
});

// Permutations
let sets = &permutation.sets;
if !sets.is_empty() {
let blinding_factors = pk.vk.cs.blinding_factors();
let last_rotation = Rotation(-((blinding_factors + 1) as i32));
let chunk_len = pk.vk.cs.degree() - 2;
let delta_start = beta * &C::Scalar::ZETA;

let first_set = sets.first().unwrap();
let last_set = sets.last().unwrap();

// Permutation constraints
parallelize(&mut values, |values, start| {
let mut beta_term = extended_omega.pow_vartime([start as u64, 0, 0, 0]);
for (i, value) in values.iter_mut().enumerate() {
let idx = start + i;
let r_next = get_rotation_idx(idx, 1, rot_scale, isize);
let r_last = get_rotation_idx(idx, last_rotation.0, rot_scale, isize);

// Enforce only for the first set.
// l_0(X) * (1 - z_0(X)) = 0
*value = *value * y
+ ((one - first_set.permutation_product_coset[idx]) * l0[idx]);
// Enforce only for the last set.
// l_last(X) * (z_l(X)^2 - z_l(X)) = 0
*value = *value * y
+ ((last_set.permutation_product_coset[idx]
* last_set.permutation_product_coset[idx]
- last_set.permutation_product_coset[idx])
* l_last[idx]);
// Except for the first set, enforce.
// l_0(X) * (z_i(X) - z_{i-1}(\omega^(last) X)) = 0
for (set_idx, set) in sets.iter().enumerate() {
if set_idx != 0 {
*value = *value * y
+ ((set.permutation_product_coset[idx]
- permutation.sets[set_idx - 1].permutation_product_coset
[r_last])
* l0[idx]);
}
}
// And for all the sets we enforce:
// (1 - (l_last(X) + l_blind(X))) * (
// z_i(\omega X) \prod_j (p(X) + \beta s_j(X) + \gamma)
// - z_i(X) \prod_j (p(X) + \delta^j \beta X + \gamma)
// )
let mut current_delta = delta_start * beta_term;
for ((set, columns), cosets) in sets
.iter()
.zip(p.columns.chunks(chunk_len))
.zip(pk.permutation.cosets.chunks(chunk_len))
{
let mut left = set.permutation_product_coset[r_next];
for (values, permutation) in columns
.iter()
.map(|&column| match column.column_type() {
Any::Advice(_) => &advice[column.index()],
Any::Fixed => &fixed[column.index()],
Any::Instance => &instance[column.index()],
})
.zip(cosets.iter())
{
left *= values[idx] + beta * permutation[idx] + gamma;
}

let mut right = set.permutation_product_coset[idx];
for values in columns.iter().map(|&column| match column.column_type() {
Any::Advice(_) => &advice[column.index()],
Any::Fixed => &fixed[column.index()],
Any::Instance => &instance[column.index()],
}) {
right *= values[idx] + current_delta + gamma;
current_delta *= &C::Scalar::DELTA;
}

*value = *value * y + ((left - right) * l_active_row[idx]);
}
beta_term *= &extended_omega;
}
});
}

// Lookups
for (n, lookup) in lookups.iter().enumerate() {
// Polynomials required for this lookup.
// Calculated here so these only have to be kept in memory for the short time
// they are actually needed.
let product_coset = pk.vk.domain.coeff_to_extended(lookup.product_poly.clone());
let permuted_input_coset = pk
.vk
.domain
.coeff_to_extended(lookup.permuted_input_poly.clone());
let permuted_table_coset = pk
.vk
.domain
.coeff_to_extended(lookup.permuted_table_poly.clone());

// Lookup constraints
parallelize(&mut values, |values, start| {
let lookup_evaluator = &self.lookups[n];
let mut eval_data = lookup_evaluator.instance();
for (i, value) in values.iter_mut().enumerate() {
let idx = start + i;

let table_value = lookup_evaluator.evaluate(
&mut eval_data,
fixed,
advice,
instance,
challenges,
&beta,
&gamma,
&theta,
&y,
&C::ScalarExt::ZERO,
idx,
rot_scale,
isize,
);

let r_next = get_rotation_idx(idx, 1, rot_scale, isize);
let r_prev = get_rotation_idx(idx, -1, rot_scale, isize);

let a_minus_s = permuted_input_coset[idx] - permuted_table_coset[idx];
// l_0(X) * (1 - z(X)) = 0
*value = *value * y + ((one - product_coset[idx]) * l0[idx]);
// l_last(X) * (z(X)^2 - z(X)) = 0
*value = *value * y
+ ((product_coset[idx] * product_coset[idx] - product_coset[idx])
* l_last[idx]);
// (1 - (l_last(X) + l_blind(X))) * (
// z(\omega X) (a'(X) + \beta) (s'(X) + \gamma)
// - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
// (\theta^{m-1} s_0(X) + ... + s_{m-1}(X) + \gamma)
// ) = 0
*value = *value * y
+ ((product_coset[r_next]
* (permuted_input_coset[idx] + beta)
* (permuted_table_coset[idx] + gamma)
- product_coset[idx] * table_value)
* l_active_row[idx]);
// Check that the first values in the permuted input expression and permuted
// fixed expression are the same.
// l_0(X) * (a'(X) - s'(X)) = 0
*value = *value * y + (a_minus_s * l0[idx]);
// Check that each value in the permuted lookup input expression is either
// equal to the value above it, or the value at the same index in the
// permuted table expression.
// (1 - (l_last + l_blind)) * (a′(X) − s′(X))⋅(a′(X) − a′(\omega^{-1} X)) = 0
*value = *value * y
+ (a_minus_s
* (permuted_input_coset[idx] - permuted_input_coset[r_prev])
* l_active_row[idx]);
}
});
}

// Shuffle constraints
for (n, shuffle) in shuffles.iter().enumerate() {
let product_coset = pk.vk.domain.coeff_to_extended(shuffle.product_poly.clone());

// Shuffle constraints
parallelize(&mut values, |values, start| {
let input_evaluator = &self.shuffles[2 * n];
let shuffle_evaluator = &self.shuffles[2 * n + 1];
let mut eval_data_input = shuffle_evaluator.instance();
let mut eval_data_shuffle = shuffle_evaluator.instance();
for (i, value) in values.iter_mut().enumerate() {
let idx = start + i;

let input_value = input_evaluator.evaluate(
&mut eval_data_input,
fixed,
advice,
instance,
challenges,
&beta,
&gamma,
&theta,
&y,
&C::ScalarExt::ZERO,
idx,
rot_scale,
isize,
);

let shuffle_value = shuffle_evaluator.evaluate(
&mut eval_data_shuffle,
fixed,
advice,
instance,
challenges,
&beta,
&gamma,
&theta,
&y,
&C::ScalarExt::ZERO,
idx,
rot_scale,
isize,
);

let r_next = get_rotation_idx(idx, 1, rot_scale, isize);

// l_0(X) * (1 - z(X)) = 0
*value = *value * y + ((one - product_coset[idx]) * l0[idx]);
// l_last(X) * (z(X)^2 - z(X)) = 0
*value = *value * y
+ ((product_coset[idx] * product_coset[idx] - product_coset[idx])
* l_last[idx]);
// (1 - (l_last(X) + l_blind(X))) * (z(\omega X) (s(X) + \gamma) - z(X) (a(X) + \gamma)) = 0
*value = *value * y
+ l_active_row[idx]
* (product_coset[r_next] * shuffle_value
- product_coset[idx] * input_value)
}
});
}
}
values
}

/// Evaluate h poly
#[allow(clippy::too_many_arguments)]
pub(in crate::plonk) fn evaluate_h(
Expand Down
Loading

0 comments on commit 1b35fab

Please sign in to comment.