Merge pull request #556 from zcash/migrate-chip-gates-to-constraints-helper

halo2_gadgets: Migrate chip gates to `Constraints::with_selector`
This commit is contained in:
ebfull 2022-04-26 12:28:04 -06:00 committed by GitHub
commit 5f867336eb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
18 changed files with 176 additions and 136 deletions

View File

@ -4,7 +4,7 @@ use super::EccPoint;
use ff::{BatchInvert, Field};
use halo2_proofs::{
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Expression, Selector},
poly::Rotation,
};
use pasta_curves::{arithmetic::FieldExt, pallas};
@ -204,11 +204,13 @@ impl Config {
// ((1 - (x_q - x_p) * α - (y_q + y_p) * δ)) * y_r
let poly12 = (one - if_alpha - if_delta) * y_r;
array::IntoIter::new([
poly1, poly2, poly3, poly4, poly5, poly6, poly7, poly8, poly9, poly10, poly11,
poly12,
])
.map(move |poly| q_add.clone() * poly)
Constraints::with_selector(
q_add,
array::IntoIter::new([
poly1, poly2, poly3, poly4, poly5, poly6, poly7, poly8, poly9, poly10, poly11,
poly12,
]),
)
});
}

View File

@ -5,7 +5,7 @@ use ff::Field;
use group::Curve;
use halo2_proofs::{
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Selector},
poly::Rotation,
};
use pasta_curves::{arithmetic::CurveAffine, pallas};
@ -74,8 +74,10 @@ impl Config {
// (y_r + y_q)(x_p x_q) (y_p y_q)(x_q x_r) = 0
let poly2 = (y_r + y_q.clone()) * (x_p - x_q.clone()) - (y_p - y_q) * (x_q - x_r);
array::IntoIter::new([("x_r", poly1), ("y_r", poly2)])
.map(move |(name, poly)| (name, q_add_incomplete.clone() * poly))
Constraints::with_selector(
q_add_incomplete,
array::IntoIter::new([("x_r", poly1), ("y_r", poly2)]),
)
});
}

View File

@ -12,7 +12,7 @@ use ff::PrimeField;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{AssignedCell, Layouter, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Selector},
poly::Rotation,
};
use uint::construct_uint;
@ -151,12 +151,14 @@ impl Config {
let lsb_x = ternary(lsb.clone(), x_p.clone(), x_p - base_x);
let lsb_y = ternary(lsb, y_p.clone(), y_p + base_y);
std::array::IntoIter::new([
("bool_check", bool_check),
("lsb_x", lsb_x),
("lsb_y", lsb_y),
])
.map(move |(name, poly)| (name, q_mul_lsb.clone() * poly))
Constraints::with_selector(
q_mul_lsb,
std::array::IntoIter::new([
("bool_check", bool_check),
("lsb_x", lsb_x),
("lsb_y", lsb_y),
]),
)
});
}

View File

@ -4,7 +4,7 @@ use crate::utilities::{bool_check, ternary};
use halo2_proofs::{
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Expression, Selector},
poly::Rotation,
};
@ -72,8 +72,10 @@ impl Config {
// k_i = 1 => y_p = base_y
let y_switch = ternary(k, base_y.clone() - y_p.clone(), base_y + y_p);
std::array::IntoIter::new([("bool_check", bool_check), ("y_switch", y_switch)])
.map(move |(name, poly)| (name, q_mul_decompose_var.clone() * poly))
Constraints::with_selector(
q_mul_decompose_var,
std::array::IntoIter::new([("bool_check", bool_check), ("y_switch", y_switch)]),
)
},
);
}

View File

@ -4,7 +4,9 @@ use crate::utilities::bool_check;
use ff::Field;
use halo2_proofs::{
circuit::Region,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector, VirtualCells},
plonk::{
Advice, Column, ConstraintSystem, Constraints, Error, Expression, Selector, VirtualCells,
},
poly::Rotation,
};
@ -77,7 +79,6 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
// Constraints used for q_mul_{2, 3} == 1
let for_loop = |meta: &mut VirtualCells<pallas::Base>,
q_mul: Expression<pallas::Base>,
y_a_next: Expression<pallas::Base>| {
let one = Expression::Constant(pallas::Base::one());
@ -121,10 +122,10 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
let gradient_2 = lambda2_cur * (x_a_cur - x_a_next) - y_a_cur - y_a_next;
std::iter::empty()
.chain(Some(("bool_check", q_mul.clone() * bool_check)))
.chain(Some(("gradient_1", q_mul.clone() * gradient_1)))
.chain(Some(("secant_line", q_mul.clone() * secant_line)))
.chain(Some(("gradient_2", q_mul * gradient_2)))
.chain(Some(("bool_check", bool_check)))
.chain(Some(("gradient_1", gradient_1)))
.chain(Some(("secant_line", secant_line)))
.chain(Some(("gradient_2", gradient_2)))
};
// q_mul_1 == 1 checks
@ -133,7 +134,7 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
let y_a_next = y_a(meta, Rotation::next());
let y_a_witnessed = meta.query_advice(self.lambda1, Rotation::cur());
vec![("init y_a", q_mul_1 * (y_a_witnessed - y_a_next))]
Constraints::with_selector(q_mul_1, Some(("init y_a", y_a_witnessed - y_a_next)))
});
// q_mul_2 == 1 checks
@ -156,17 +157,20 @@ impl<const NUM_BITS: usize> Config<NUM_BITS> {
let x_p_check = x_p_cur - x_p_next;
let y_p_check = y_p_cur - y_p_next;
std::iter::empty()
.chain(Some(("x_p_check", q_mul_2.clone() * x_p_check)))
.chain(Some(("y_p_check", q_mul_2.clone() * y_p_check)))
.chain(for_loop(meta, q_mul_2, y_a_next))
Constraints::with_selector(
q_mul_2,
std::iter::empty()
.chain(Some(("x_p_check", x_p_check)))
.chain(Some(("y_p_check", y_p_check)))
.chain(for_loop(meta, y_a_next)),
)
});
// q_mul_3 == 1 checks
meta.create_gate("q_mul_3 == 1 checks", |meta| {
let q_mul_3 = meta.query_selector(self.q_mul.2);
let y_a_final = meta.query_advice(self.lambda1, Rotation::next());
for_loop(meta, q_mul_3, y_a_final)
Constraints::with_selector(q_mul_3, for_loop(meta, y_a_final))
});
}

View File

@ -3,7 +3,7 @@ use crate::{primitives::sinsemilla, utilities::lookup_range_check::LookupRangeCh
use halo2_proofs::circuit::AssignedCell;
use halo2_proofs::{
circuit::Layouter,
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Expression, Selector},
poly::Rotation,
};
@ -82,14 +82,15 @@ impl Config {
// (1 - k_254) * (1 - z_130 * eta) * s_minus_lo_130 = 0
let canonicity = (one.clone() - k_254) * (one - z_130 * eta) * s_minus_lo_130;
iter::empty()
.chain(Some(("s_check", s_check)))
.chain(Some(("recovery", recovery)))
.chain(Some(("lo_zero", lo_zero)))
.chain(Some(("s_minus_lo_130_check", s_minus_lo_130_check)))
.chain(Some(("canonicity", canonicity)))
.map(|(name, poly)| (name, q_mul_overflow.clone() * poly))
.collect::<Vec<_>>()
Constraints::with_selector(
q_mul_overflow,
iter::empty()
.chain(Some(("s_check", s_check)))
.chain(Some(("recovery", recovery)))
.chain(Some(("lo_zero", lo_zero)))
.chain(Some(("s_minus_lo_130_check", s_minus_lo_130_check)))
.chain(Some(("canonicity", canonicity))),
)
});
}

View File

@ -9,7 +9,10 @@ use std::marker::PhantomData;
use group::{ff::PrimeField, Curve};
use halo2_proofs::{
circuit::{AssignedCell, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector, VirtualCells},
plonk::{
Advice, Column, ConstraintSystem, Constraints, Error, Expression, Fixed, Selector,
VirtualCells,
},
poly::Rotation,
};
use lazy_static::lazy_static;
@ -139,7 +142,7 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
// => a_i = z_i - z_{i+1} * 2^3
let word = z_cur - z_next * pallas::Base::from(H as u64);
self.coords_check(meta, q_mul_fixed_running_sum, word)
Constraints::with_selector(q_mul_fixed_running_sum, self.coords_check(meta, word))
});
}
@ -147,7 +150,6 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
fn coords_check(
&self,
meta: &mut VirtualCells<'_, pallas::Base>,
toggle: Expression<pallas::Base>,
window: Expression<pallas::Base>,
) -> Vec<(&'static str, Expression<pallas::Base>)> {
let y_p = meta.query_advice(self.y_p, Rotation::cur());
@ -179,9 +181,9 @@ impl<FixedPoints: super::FixedPoints<pallas::Affine>> Config<FixedPoints> {
y_p.square() - x_p.clone().square() * x_p - Expression::Constant(pallas::Affine::b());
vec![
("check x", toggle.clone() * x_check),
("check y", toggle.clone() * y_check),
("on-curve", toggle * on_curve),
("check x", x_check),
("check y", y_check),
("on-curve", on_curve),
]
}

View File

@ -9,7 +9,7 @@ use crate::{
use group::ff::PrimeField;
use halo2_proofs::{
circuit::{AssignedCell, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Expression, Selector},
poly::Rotation,
};
use pasta_curves::{arithmetic::FieldExt, pallas};
@ -148,10 +148,12 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
)))
};
canon_checks
.chain(decomposition_checks)
.chain(Some(("alpha_0_prime check", alpha_0_prime_check)))
.map(move |(name, poly)| (name, q_mul_fixed_base_field.clone() * poly))
Constraints::with_selector(
q_mul_fixed_base_field,
canon_checks
.chain(decomposition_checks)
.chain(Some(("alpha_0_prime check", alpha_0_prime_check))),
)
});
}

View File

@ -5,7 +5,7 @@ use arrayvec::ArrayVec;
use ff::PrimeField;
use halo2_proofs::{
circuit::{AssignedCell, Layouter, Region},
plonk::{ConstraintSystem, Error, Selector},
plonk::{ConstraintSystem, Constraints, Error, Selector},
poly::Rotation,
};
use pasta_curves::pallas;
@ -37,15 +37,15 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
let q_mul_fixed_full = meta.query_selector(self.q_mul_fixed_full);
let window = meta.query_advice(self.super_config.window, Rotation::cur());
self.super_config
.coords_check(meta, q_mul_fixed_full.clone(), window.clone())
.into_iter()
// Constrain each window to a 3-bit value:
// 1 * (window - 0) * (window - 1) * ... * (window - 7)
.chain(Some((
"window range check",
q_mul_fixed_full * range_check(window, H),
)))
Constraints::with_selector(
q_mul_fixed_full,
self.super_config
.coords_check(meta, window.clone())
.into_iter()
// Constrain each window to a 3-bit value:
// 1 * (window - 0) * (window - 1) * ... * (window - 7)
.chain(Some(("window range check", range_check(window, H)))),
)
});
}

View File

@ -5,7 +5,7 @@ use crate::{ecc::chip::MagnitudeSign, utilities::bool_check};
use halo2_proofs::{
circuit::{Layouter, Region},
plonk::{ConstraintSystem, Error, Expression, Selector},
plonk::{ConstraintSystem, Constraints, Error, Expression, Selector},
poly::Rotation,
};
use pasta_curves::pallas;
@ -57,13 +57,15 @@ impl<Fixed: FixedPoints<pallas::Affine>> Config<Fixed> {
// Check that the correct sign is witnessed s.t. sign * y_p = y_a
let negation_check = sign * y_p - y_a;
array::IntoIter::new([
("last_window_check", last_window_check),
("sign_check", sign_check),
("y_check", y_check),
("negation_check", negation_check),
])
.map(move |(name, poly)| (name, q_mul_fixed_short.clone() * poly))
Constraints::with_selector(
q_mul_fixed_short,
array::IntoIter::new([
("last_window_check", last_window_check),
("sign_check", sign_check),
("y_check", y_check),
("negation_check", negation_check),
]),
)
});
}

View File

@ -1,10 +1,14 @@
use std::array;
use super::{EccPoint, NonIdentityEccPoint};
use group::prime::PrimeCurveAffine;
use halo2_proofs::{
circuit::{AssignedCell, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector, VirtualCells},
plonk::{
Advice, Column, ConstraintSystem, Constraints, Error, Expression, Selector, VirtualCells,
},
poly::Rotation,
};
use pasta_curves::{arithmetic::CurveAffine, pallas};
@ -60,10 +64,14 @@ impl Config {
let x = meta.query_advice(self.x, Rotation::cur());
let y = meta.query_advice(self.y, Rotation::cur());
vec![
// We can't use `Constraints::with_selector` because that creates constraints
// of the form `q_point * (x * curve_eqn)`, but this was implemented without
// parentheses, and thus evaluates as `(q_point * x) * curve_eqn`, which is
// structurally different in the pinned verifying key.
array::IntoIter::new([
("x == 0 v on_curve", q_point.clone() * x * curve_eqn(meta)),
("y == 0 v on_curve", q_point * y * curve_eqn(meta)),
]
])
});
meta.create_gate("witness non-identity point", |meta| {
@ -72,7 +80,7 @@ impl Config {
let q_point_non_id = meta.query_selector(self.q_point_non_id);
vec![("on_curve", q_point_non_id * curve_eqn(meta))]
Constraints::with_selector(q_point_non_id, Some(("on_curve", curve_eqn(meta))))
});
}

View File

@ -4,7 +4,9 @@ use std::iter;
use halo2_proofs::{
arithmetic::FieldExt,
circuit::{AssignedCell, Cell, Chip, Layouter, Region},
plonk::{Advice, Any, Column, ConstraintSystem, Error, Expression, Fixed, Selector},
plonk::{
Advice, Any, Column, ConstraintSystem, Constraints, Error, Expression, Fixed, Selector,
},
poly::Rotation,
};
@ -94,20 +96,23 @@ impl<F: FieldExt, const WIDTH: usize, const RATE: usize> Pow5Chip<F, WIDTH, RATE
meta.create_gate("full round", |meta| {
let s_full = meta.query_selector(s_full);
(0..WIDTH)
.map(|next_idx| {
let state_next = meta.query_advice(state[next_idx], Rotation::next());
let expr = (0..WIDTH)
.map(|idx| {
let state_cur = meta.query_advice(state[idx], Rotation::cur());
let rc_a = meta.query_fixed(rc_a[idx], Rotation::cur());
pow_5(state_cur + rc_a) * m_reg[next_idx][idx]
})
.reduce(|acc, term| acc + term)
.expect("WIDTH > 0");
s_full.clone() * (expr - state_next)
})
.collect::<Vec<_>>()
Constraints::with_selector(
s_full,
(0..WIDTH)
.map(|next_idx| {
let state_next = meta.query_advice(state[next_idx], Rotation::next());
let expr = (0..WIDTH)
.map(|idx| {
let state_cur = meta.query_advice(state[idx], Rotation::cur());
let rc_a = meta.query_fixed(rc_a[idx], Rotation::cur());
pow_5(state_cur + rc_a) * m_reg[next_idx][idx]
})
.reduce(|acc, term| acc + term)
.expect("WIDTH > 0");
expr - state_next
})
.collect::<Vec<_>>(),
)
});
meta.create_gate("partial rounds", |meta| {
@ -140,24 +145,20 @@ impl<F: FieldExt, const WIDTH: usize, const RATE: usize> Pow5Chip<F, WIDTH, RATE
};
let partial_round_linear = |idx: usize, meta: &mut VirtualCells<F>| {
let expr = {
let rc_b = meta.query_fixed(rc_b[idx], Rotation::cur());
mid(idx, meta) + rc_b - next(idx, meta)
};
s_partial.clone() * expr
let rc_b = meta.query_fixed(rc_b[idx], Rotation::cur());
mid(idx, meta) + rc_b - next(idx, meta)
};
std::iter::empty()
// state[0] round a
.chain(Some(
s_partial.clone() * (pow_5(cur_0 + rc_a0) - mid_0.clone()),
))
// state[0] round b
.chain(Some(
s_partial.clone() * (pow_5(mid(0, meta) + rc_b0) - next(0, meta)),
))
.chain((1..WIDTH).map(|idx| partial_round_linear(idx, meta)))
.collect::<Vec<_>>()
Constraints::with_selector(
s_partial,
std::iter::empty()
// state[0] round a
.chain(Some(pow_5(cur_0 + rc_a0) - mid_0.clone()))
// state[0] round b
.chain(Some(pow_5(mid(0, meta) + rc_b0) - next(0, meta)))
.chain((1..WIDTH).map(|idx| partial_round_linear(idx, meta)))
.collect::<Vec<_>>(),
)
});
meta.create_gate("pad-and-add", |meta| {
@ -173,16 +174,17 @@ impl<F: FieldExt, const WIDTH: usize, const RATE: usize> Pow5Chip<F, WIDTH, RATE
// We pad the input by storing the required padding in fixed columns and
// then constraining the corresponding input columns to be equal to it.
s_pad_and_add.clone() * (initial_state + input - output_state)
initial_state + input - output_state
};
(0..RATE)
.map(pad_and_add)
// The capacity element is never altered by the input.
.chain(Some(
s_pad_and_add.clone() * (initial_state_rate - output_state_rate),
))
.collect::<Vec<_>>()
Constraints::with_selector(
s_pad_and_add,
(0..RATE)
.map(pad_and_add)
// The capacity element is never altered by the input.
.chain(Some(initial_state_rate - output_state_rate))
.collect::<Vec<_>>(),
)
});
Pow5Config {

View File

@ -16,8 +16,8 @@ use std::marker::PhantomData;
use halo2_proofs::{
circuit::{AssignedCell, Chip, Layouter},
plonk::{
Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector, TableColumn,
VirtualCells,
Advice, Column, ConstraintSystem, Constraints, Error, Expression, Fixed, Selector,
TableColumn, VirtualCells,
},
poly::Rotation,
};
@ -210,7 +210,7 @@ where
// 2 * y_q - Y_{A,0} = 0
let init_y_q_check = y_q * two - Y_A_cur;
vec![q_s4 * init_y_q_check]
Constraints::with_selector(q_s4, Some(("init_y_q_check", init_y_q_check)))
});
meta.create_gate("Sinsemilla gate", |meta| {
@ -259,10 +259,10 @@ where
lhs - rhs
};
vec![
("Secant line", q_s1.clone() * secant_line),
("y check", q_s1 * y_check),
]
Constraints::with_selector(
q_s1,
std::array::IntoIter::new([("Secant line", secant_line), ("y check", y_check)]),
)
});
config

View File

@ -2,7 +2,7 @@
use halo2_proofs::{
circuit::{AssignedCell, Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Selector},
poly::Rotation,
};
use pasta_curves::{arithmetic::FieldExt, pallas};
@ -163,13 +163,15 @@ where
// <https://zips.z.cash/protocol/protocol.pdf#merklepath>
let right_check = b_2 + c_whole * two_pow_5 - right_node;
array::IntoIter::new([
("l_check", l_check),
("left_check", left_check),
("right_check", right_check),
("b1_b2_check", b1_b2_check),
])
.map(move |(name, poly)| (name, q_decompose.clone() * poly))
Constraints::with_selector(
q_decompose,
array::IntoIter::new([
("l_check", l_check),
("left_check", left_check),
("right_check", right_check),
("b1_b2_check", b1_b2_check),
]),
)
});
MerkleConfig {

View File

@ -186,7 +186,7 @@ mod tests {
use halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner},
dev::{FailureLocation, MockProver, VerifyFailure},
plonk::{Any, Circuit, ConstraintSystem, Error, Selector},
plonk::{Any, Circuit, ConstraintSystem, Constraints, Error, Selector},
poly::Rotation,
};
use pasta_curves::{arithmetic::FieldExt, pallas};
@ -226,7 +226,7 @@ mod tests {
let selector = meta.query_selector(selector);
let advice = meta.query_advice(advice, Rotation::cur());
vec![selector * range_check(advice, RANGE)]
Constraints::with_selector(selector, Some(range_check(advice, RANGE)))
});
Config { selector, advice }

View File

@ -3,7 +3,7 @@
use super::{bool_check, ternary, UtilitiesInstructions};
use halo2_proofs::{
circuit::{AssignedCell, Chip, Layouter},
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Selector},
poly::Rotation,
};
use pasta_curves::arithmetic::FieldExt;
@ -189,8 +189,14 @@ impl<F: FieldExt> CondSwapChip<F> {
// Check `swap` is boolean.
let bool_check = bool_check(swap);
array::IntoIter::new([a_check, b_check, bool_check])
.map(move |poly| q_swap.clone() * poly)
Constraints::with_selector(
q_swap,
array::IntoIter::new([
("a check", a_check),
("b check", b_check),
("swap is bool", bool_check),
]),
)
});
config

View File

@ -25,7 +25,7 @@
use ff::PrimeFieldBits;
use halo2_proofs::{
circuit::{AssignedCell, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Selector},
poly::Rotation,
};
@ -92,7 +92,7 @@ impl<F: FieldExt + PrimeFieldBits, const WINDOW_NUM_BITS: usize>
// => k_i = z_i - 2^{K}⋅z_{i + 1}
let word = z_cur - z_next * F::from(1 << WINDOW_NUM_BITS);
vec![q_range_check * range_check(word, 1 << WINDOW_NUM_BITS)]
Constraints::with_selector(q_range_check, Some(range_check(word, 1 << WINDOW_NUM_BITS)))
});
config

View File

@ -3,7 +3,7 @@
use halo2_proofs::{
circuit::{AssignedCell, Layouter, Region},
plonk::{Advice, Column, ConstraintSystem, Error, Selector, TableColumn},
plonk::{Advice, Column, ConstraintSystem, Constraints, Error, Selector, TableColumn},
poly::Rotation,
};
use std::{convert::TryInto, marker::PhantomData};
@ -109,7 +109,10 @@ impl<F: FieldExt + PrimeFieldBits, const K: usize> LookupRangeCheckConfig<F, K>
// shifted_word = word * 2^{K-s}
// = word * 2^K * inv_two_pow_s
vec![q_bitshift * (word * two_pow_k * inv_two_pow_s - shifted_word)]
Constraints::with_selector(
q_bitshift,
Some(word * two_pow_k * inv_two_pow_s - shifted_word),
)
});
config