mirror of https://github.com/zcash/halo2.git
Merge pull request #169 from zcash/circuit-constraint-refinements
Circuit constraint refinements to reduce proof size
This commit is contained in:
commit
3dd2a1872a
|
@ -60,7 +60,8 @@ 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([poly1, poly2]).map(move |poly| q_add_incomplete.clone() * poly)
|
||||
array::IntoIter::new([("x_r", poly1), ("y_r", poly2)])
|
||||
.map(move |(name, poly)| (name, q_add_incomplete.clone() * poly))
|
||||
});
|
||||
}
|
||||
|
||||
|
|
|
@ -99,12 +99,12 @@ impl Config {
|
|||
meta.create_gate("LSB check", |meta| {
|
||||
let q_mul_lsb = meta.query_selector(self.q_mul_lsb);
|
||||
|
||||
let z_1 = meta.query_advice(self.complete_config.z_complete, Rotation::prev());
|
||||
let z_0 = meta.query_advice(self.complete_config.z_complete, Rotation::cur());
|
||||
let x_p = meta.query_advice(self.add_config.x_p, Rotation::prev());
|
||||
let y_p = meta.query_advice(self.add_config.y_p, Rotation::prev());
|
||||
let base_x = meta.query_advice(self.add_config.x_p, Rotation::cur());
|
||||
let base_y = meta.query_advice(self.add_config.y_p, Rotation::cur());
|
||||
let z_1 = meta.query_advice(self.complete_config.z_complete, Rotation::cur());
|
||||
let z_0 = meta.query_advice(self.complete_config.z_complete, Rotation::next());
|
||||
let x_p = meta.query_advice(self.add_config.x_p, Rotation::cur());
|
||||
let y_p = meta.query_advice(self.add_config.y_p, Rotation::cur());
|
||||
let base_x = meta.query_advice(self.add_config.x_p, Rotation::next());
|
||||
let base_y = meta.query_advice(self.add_config.y_p, Rotation::next());
|
||||
|
||||
// z_0 = 2 * z_1 + k_0
|
||||
// => k_0 = z_0 - 2 * z_1
|
||||
|
@ -118,8 +118,12 @@ impl Config {
|
|||
let lsb_x = (lsb.clone() * x_p.clone()) + one_minus_lsb.clone() * (x_p - base_x);
|
||||
let lsb_y = (lsb * y_p.clone()) + one_minus_lsb * (y_p + base_y);
|
||||
|
||||
std::array::IntoIter::new([bool_check, lsb_x, lsb_y])
|
||||
.map(move |poly| q_mul_lsb.clone() * poly)
|
||||
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))
|
||||
});
|
||||
|
||||
self.hi_config.create_gate(meta);
|
||||
|
@ -271,8 +275,8 @@ impl Config {
|
|||
/// addition subregion.
|
||||
///
|
||||
/// ```text
|
||||
/// | x_p | y_p | acc_x | acc_y | complete addition | z_1 |
|
||||
/// |base_x|base_y| res_x | res_y | | | | | | z_0 | q_mul_lsb = 1
|
||||
/// | x_p | y_p | acc_x | acc_y | complete addition | z_1 | q_mul_lsb = 1
|
||||
/// |base_x|base_y| res_x | res_y | | | | | | z_0 |
|
||||
/// ```
|
||||
fn process_lsb(
|
||||
&self,
|
||||
|
@ -284,7 +288,7 @@ impl Config {
|
|||
lsb: Option<bool>,
|
||||
) -> Result<(EccPoint, Z<pallas::Base>), Error> {
|
||||
// Enforce switching logic on LSB using a custom gate
|
||||
self.q_mul_lsb.enable(region, offset + 1)?;
|
||||
self.q_mul_lsb.enable(region, offset)?;
|
||||
|
||||
// z_1 has been assigned at (z_complete, offset).
|
||||
// Assign z_0 = 2⋅z_1 + k_0
|
||||
|
|
|
@ -42,6 +42,11 @@ impl Config {
|
|||
/// addition gate (controlled by `q_mul`) already checks scalar decomposition for
|
||||
/// the other bits.
|
||||
pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<pallas::Base>) {
|
||||
// | y_p | z_complete |
|
||||
// --------------------
|
||||
// | y_p | z_{i + 1} |
|
||||
// | | base_y |
|
||||
// | | z_i |
|
||||
meta.create_gate(
|
||||
"Decompose scalar for complete bits of variable-base mul",
|
||||
|meta| {
|
||||
|
@ -122,6 +127,12 @@ impl Config {
|
|||
// Each iteration uses 2 rows (two complete additions)
|
||||
let row = 2 * iter;
|
||||
|
||||
// | x_p | y_p | x_qr | y_qr | z_complete |
|
||||
// ------------------------------------------
|
||||
// | U_x | U_y | acc_x | acc_y | z_{i + 1} | row + offset
|
||||
// |acc_x|acc_y|acc+U_x|acc+U_y| base_y |
|
||||
// | | | res_x | res_y | z_i |
|
||||
|
||||
// Update `z`.
|
||||
z = {
|
||||
// z_next = z_cur * 2 + k_next
|
||||
|
|
|
@ -81,12 +81,12 @@ impl Config {
|
|||
let canonicity = (one.clone() - k_254) * (one - z_130 * eta) * s_minus_lo_130;
|
||||
|
||||
iter::empty()
|
||||
.chain(Some(s_check))
|
||||
.chain(Some(recovery))
|
||||
.chain(Some(lo_zero))
|
||||
.chain(Some(s_minus_lo_130_check))
|
||||
.chain(Some(canonicity))
|
||||
.map(|poly| q_mul_overflow.clone() * poly)
|
||||
.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<_>>()
|
||||
});
|
||||
}
|
||||
|
|
|
@ -45,8 +45,8 @@ impl Config {
|
|||
- Expression::Constant(pallas::Affine::b());
|
||||
|
||||
vec![
|
||||
q_point.clone() * x * curve_eqn.clone(),
|
||||
q_point * y * curve_eqn,
|
||||
("x == 0 ∨ on_curve", q_point.clone() * x * curve_eqn.clone()),
|
||||
("y == 0 ∨ on_curve", q_point * y * curve_eqn),
|
||||
]
|
||||
});
|
||||
}
|
||||
|
|
|
@ -110,10 +110,14 @@ impl<F: FieldExt> Pow5T3Chip<F> {
|
|||
- next[next_idx].clone())
|
||||
};
|
||||
|
||||
vec![full_round(0), full_round(1), full_round(2)]
|
||||
vec![
|
||||
("state[0]", full_round(0)),
|
||||
("state[1]", full_round(1)),
|
||||
("state[2]", full_round(2)),
|
||||
]
|
||||
});
|
||||
|
||||
meta.create_gate("partial round", |meta| {
|
||||
meta.create_gate("partial rounds", |meta| {
|
||||
let cur_0 = meta.query_advice(state[0], Rotation::cur());
|
||||
let cur_1 = meta.query_advice(state[1], Rotation::cur());
|
||||
let cur_2 = meta.query_advice(state[2], Rotation::cur());
|
||||
|
@ -143,18 +147,24 @@ impl<F: FieldExt> Pow5T3Chip<F> {
|
|||
};
|
||||
|
||||
vec![
|
||||
s_partial.clone() * (pow_5(cur_0 + rc_a0) - mid_0.clone()),
|
||||
s_partial.clone()
|
||||
* (pow_5(
|
||||
mid_0.clone() * m_reg[0][0]
|
||||
+ (cur_1.clone() + rc_a1.clone()) * m_reg[0][1]
|
||||
+ (cur_2.clone() + rc_a2.clone()) * m_reg[0][2]
|
||||
+ rc_b0,
|
||||
) - (next_0.clone() * m_inv[0][0]
|
||||
+ next_1.clone() * m_inv[0][1]
|
||||
+ next_2.clone() * m_inv[0][2])),
|
||||
partial_round_linear(1, rc_b1),
|
||||
partial_round_linear(2, rc_b2),
|
||||
(
|
||||
"state[0] round a",
|
||||
s_partial.clone() * (pow_5(cur_0 + rc_a0) - mid_0.clone()),
|
||||
),
|
||||
(
|
||||
"state[0] round b",
|
||||
s_partial.clone()
|
||||
* (pow_5(
|
||||
mid_0.clone() * m_reg[0][0]
|
||||
+ (cur_1.clone() + rc_a1.clone()) * m_reg[0][1]
|
||||
+ (cur_2.clone() + rc_a2.clone()) * m_reg[0][2]
|
||||
+ rc_b0,
|
||||
) - (next_0.clone() * m_inv[0][0]
|
||||
+ next_1.clone() * m_inv[0][1]
|
||||
+ next_2.clone() * m_inv[0][2])),
|
||||
),
|
||||
("state[1]", partial_round_linear(1, rc_b1)),
|
||||
("state[2]", partial_round_linear(2, rc_b2)),
|
||||
]
|
||||
});
|
||||
|
||||
|
@ -177,10 +187,19 @@ impl<F: FieldExt> Pow5T3Chip<F> {
|
|||
};
|
||||
|
||||
vec![
|
||||
pad_and_add(initial_state_0, input_0, output_state_0),
|
||||
pad_and_add(initial_state_1, input_1, output_state_1),
|
||||
(
|
||||
"state[0]",
|
||||
pad_and_add(initial_state_0, input_0, output_state_0),
|
||||
),
|
||||
(
|
||||
"state[1]",
|
||||
pad_and_add(initial_state_1, input_1, output_state_1),
|
||||
),
|
||||
// The capacity element is never altered by the input.
|
||||
s_pad_and_add * (initial_state_2 - output_state_2),
|
||||
(
|
||||
"state[2]",
|
||||
s_pad_and_add * (initial_state_2 - output_state_2),
|
||||
),
|
||||
]
|
||||
});
|
||||
|
||||
|
|
|
@ -59,8 +59,8 @@ impl CommitIvkConfig {
|
|||
|
||||
| A_0 | A_1 | A_2 | A_3 | A_4 | A_5 | A_6 | A_7 | A_8 | q_commit_ivk |
|
||||
-----------------------------------------------------------------------------------------------------
|
||||
| ak | a | b | b_0 | b_1 | b_2 | z13_a | a_prime | z13_a_prime | 0 |
|
||||
| nk | c | d | d_0 | d_1 | | z13_c | b2_c_prime| z14_b2_c_prime | 1 |
|
||||
| ak | a | b | b_0 | b_1 | b_2 | z13_a | a_prime | z13_a_prime | 1 |
|
||||
| nk | c | d | d_0 | d_1 | | z13_c | b2_c_prime| z14_b2_c_prime | 0 |
|
||||
|
||||
*/
|
||||
meta.create_gate("CommitIvk canonicity check", |meta| {
|
||||
|
@ -73,27 +73,27 @@ impl CommitIvkConfig {
|
|||
let two_pow_250 = pallas::Base::from_u128(1 << 125).square();
|
||||
let two_pow_254 = two_pow_250 * two_pow_4;
|
||||
|
||||
let ak = meta.query_advice(config.advices[0], Rotation::prev());
|
||||
let nk = meta.query_advice(config.advices[0], Rotation::cur());
|
||||
let ak = meta.query_advice(config.advices[0], Rotation::cur());
|
||||
let nk = meta.query_advice(config.advices[0], Rotation::next());
|
||||
|
||||
// `a` is constrained by the Sinsemilla hash to be 250 bits.
|
||||
let a = meta.query_advice(config.advices[1], Rotation::prev());
|
||||
let a = meta.query_advice(config.advices[1], Rotation::cur());
|
||||
// `b` is constrained by the Sinsemilla hash to be 10 bits.
|
||||
let b_whole = meta.query_advice(config.advices[2], Rotation::prev());
|
||||
let b_whole = meta.query_advice(config.advices[2], Rotation::cur());
|
||||
// `c` is constrained by the Sinsemilla hash to be 240 bits.
|
||||
let c = meta.query_advice(config.advices[1], Rotation::cur());
|
||||
let c = meta.query_advice(config.advices[1], Rotation::next());
|
||||
// `d` is constrained by the Sinsemilla hash to be 10 bits.
|
||||
let d_whole = meta.query_advice(config.advices[2], Rotation::cur());
|
||||
let d_whole = meta.query_advice(config.advices[2], Rotation::next());
|
||||
|
||||
// b = b_0||b_1||b_2`
|
||||
// = (bits 250..=253 of `ak`) || (bit 254 of `ak`) || (bits 0..=4 of `nk`)
|
||||
//
|
||||
// b_0 has been constrained outside this gate to be a four-bit value.
|
||||
let b_0 = meta.query_advice(config.advices[3], Rotation::prev());
|
||||
let b_0 = meta.query_advice(config.advices[3], Rotation::cur());
|
||||
// This gate constrains b_1 to be a one-bit value.
|
||||
let b_1 = meta.query_advice(config.advices[4], Rotation::prev());
|
||||
let b_1 = meta.query_advice(config.advices[4], Rotation::cur());
|
||||
// b_2 has been constrained outside this gate to be a five-bit value.
|
||||
let b_2 = meta.query_advice(config.advices[5], Rotation::prev());
|
||||
let b_2 = meta.query_advice(config.advices[5], Rotation::cur());
|
||||
// Check that b_whole is consistent with the witnessed subpieces.
|
||||
let b_decomposition_check =
|
||||
b_whole - (b_0.clone() + b_1.clone() * two_pow_4 + b_2.clone() * two_pow_5);
|
||||
|
@ -101,9 +101,9 @@ impl CommitIvkConfig {
|
|||
// d = d_0||d_1` = (bits 245..=253 of `nk`) || (bit 254 of `nk`)
|
||||
//
|
||||
// d_0 has been constrained outside this gate to be a nine-bit value.
|
||||
let d_0 = meta.query_advice(config.advices[3], Rotation::cur());
|
||||
let d_0 = meta.query_advice(config.advices[3], Rotation::next());
|
||||
// This gate constrains d_1 to be a one-bit value.
|
||||
let d_1 = meta.query_advice(config.advices[4], Rotation::cur());
|
||||
let d_1 = meta.query_advice(config.advices[4], Rotation::next());
|
||||
// Check that d_whole is consistent with the witnessed subpieces.
|
||||
let d_decomposition_check = d_whole - (d_0.clone() + d_1.clone() * two_pow_9);
|
||||
|
||||
|
@ -137,14 +137,14 @@ impl CommitIvkConfig {
|
|||
// z13_a is the 13th running sum output by the 10-bit Sinsemilla decomposition of `a`.
|
||||
// b_1 = 1 => z13_a = 0
|
||||
let z13_a_check = {
|
||||
let z13_a = meta.query_advice(config.advices[6], Rotation::prev());
|
||||
let z13_a = meta.query_advice(config.advices[6], Rotation::cur());
|
||||
b_1.clone() * z13_a
|
||||
};
|
||||
|
||||
// Check that a_prime = a + 2^130 - t_P.
|
||||
// This is checked regardless of the value of b_1.
|
||||
let a_prime_check = {
|
||||
let a_prime = meta.query_advice(config.advices[7], Rotation::prev());
|
||||
let a_prime = meta.query_advice(config.advices[7], Rotation::cur());
|
||||
let two_pow_130 =
|
||||
Expression::Constant(pallas::Base::from_u128(1 << 65).square());
|
||||
let t_p = Expression::Constant(pallas::Base::from_u128(T_P));
|
||||
|
@ -154,15 +154,15 @@ impl CommitIvkConfig {
|
|||
// Check that the running sum output by the 130-bit little-endian decomposition of
|
||||
// `a_prime` is zero.
|
||||
let z13_a_prime = {
|
||||
let z13_a_prime = meta.query_advice(config.advices[8], Rotation::prev());
|
||||
let z13_a_prime = meta.query_advice(config.advices[8], Rotation::cur());
|
||||
b_1 * z13_a_prime
|
||||
};
|
||||
|
||||
std::iter::empty()
|
||||
.chain(Some(b0_canon_check))
|
||||
.chain(Some(z13_a_check))
|
||||
.chain(Some(a_prime_check))
|
||||
.chain(Some(z13_a_prime))
|
||||
.chain(Some(("b0_canon_check", b0_canon_check)))
|
||||
.chain(Some(("z13_a_check", z13_a_check)))
|
||||
.chain(Some(("a_prime_check", a_prime_check)))
|
||||
.chain(Some(("z13_a_prime", z13_a_prime)))
|
||||
};
|
||||
|
||||
// nk = b_2 (5 bits) || c (240 bits) || d_0 (9 bits) || d_1 (1 bit)
|
||||
|
@ -174,7 +174,7 @@ impl CommitIvkConfig {
|
|||
// d_1 = 1 => z13_c = 0, where z13_c is the 13th running sum
|
||||
// output by the 10-bit Sinsemilla decomposition of `c`.
|
||||
let z13_c_check = {
|
||||
let z13_c = meta.query_advice(config.advices[6], Rotation::cur());
|
||||
let z13_c = meta.query_advice(config.advices[6], Rotation::next());
|
||||
d_1.clone() * z13_c
|
||||
};
|
||||
|
||||
|
@ -185,34 +185,34 @@ impl CommitIvkConfig {
|
|||
let two_pow_140 =
|
||||
Expression::Constant(pallas::Base::from_u128(1 << 70).square());
|
||||
let t_p = Expression::Constant(pallas::Base::from_u128(T_P));
|
||||
let b2_c_prime = meta.query_advice(config.advices[7], Rotation::cur());
|
||||
let b2_c_prime = meta.query_advice(config.advices[7], Rotation::next());
|
||||
b_2 + c * two_pow_5 + two_pow_140 - t_p - b2_c_prime
|
||||
};
|
||||
|
||||
// Check that the running sum output by the 140-bit little-
|
||||
// endian decomposition of b2_c_prime is zero.
|
||||
let z14_b2_c_prime = {
|
||||
let z14_b2_c_prime = meta.query_advice(config.advices[8], Rotation::cur());
|
||||
let z14_b2_c_prime = meta.query_advice(config.advices[8], Rotation::next());
|
||||
d_1 * z14_b2_c_prime
|
||||
};
|
||||
|
||||
std::iter::empty()
|
||||
.chain(Some(c0_canon_check))
|
||||
.chain(Some(z13_c_check))
|
||||
.chain(Some(b2_c_prime_check))
|
||||
.chain(Some(z14_b2_c_prime))
|
||||
.chain(Some(("c0_canon_check", c0_canon_check)))
|
||||
.chain(Some(("z13_c_check", z13_c_check)))
|
||||
.chain(Some(("b2_c_prime_check", b2_c_prime_check)))
|
||||
.chain(Some(("z14_b2_c_prime", z14_b2_c_prime)))
|
||||
};
|
||||
|
||||
std::iter::empty()
|
||||
.chain(Some(b1_bool_check))
|
||||
.chain(Some(d1_bool_check))
|
||||
.chain(Some(b_decomposition_check))
|
||||
.chain(Some(d_decomposition_check))
|
||||
.chain(Some(ak_decomposition_check))
|
||||
.chain(Some(nk_decomposition_check))
|
||||
.chain(Some(("b1_bool_check", b1_bool_check)))
|
||||
.chain(Some(("d1_bool_check", d1_bool_check)))
|
||||
.chain(Some(("b_decomposition_check", b_decomposition_check)))
|
||||
.chain(Some(("d_decomposition_check", d_decomposition_check)))
|
||||
.chain(Some(("ak_decomposition_check", ak_decomposition_check)))
|
||||
.chain(Some(("nk_decomposition_check", nk_decomposition_check)))
|
||||
.chain(ak_canonicity_checks)
|
||||
.chain(nk_canonicity_checks)
|
||||
.map(move |poly| q_commit_ivk.clone() * poly)
|
||||
.map(move |(name, poly)| (name, q_commit_ivk.clone() * poly))
|
||||
});
|
||||
|
||||
config
|
||||
|
@ -455,8 +455,8 @@ impl CommitIvkConfig {
|
|||
|
||||
| A_0 | A_1 | A_2 | A_3 | A_4 | A_5 | A_6 | A_7 | A_8 | q_commit_ivk |
|
||||
-----------------------------------------------------------------------------------------------------
|
||||
| ak | a | b | b_0 | b_1 | b_2 | z13_a | a_prime | z13_a_prime | 0 |
|
||||
| nk | c | d | d_0 | d_1 | | z13_c | b2_c_prime| z14_b2_c_prime | 1 |
|
||||
| ak | a | b | b_0 | b_1 | b_2 | z13_a | a_prime | z13_a_prime | 1 |
|
||||
| nk | c | d | d_0 | d_1 | | z13_c | b2_c_prime| z14_b2_c_prime | 0 |
|
||||
|
||||
*/
|
||||
fn assign_gate(
|
||||
|
@ -467,8 +467,8 @@ impl CommitIvkConfig {
|
|||
layouter.assign_region(
|
||||
|| "Assign cells used in canonicity gate",
|
||||
|mut region| {
|
||||
// Enable selector on offset 1
|
||||
self.q_commit_ivk.enable(&mut region, 1)?;
|
||||
// Enable selector on offset 0
|
||||
self.q_commit_ivk.enable(&mut region, 0)?;
|
||||
|
||||
// Offset 0
|
||||
{
|
||||
|
|
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue