AtHeartEngineer/halo2
1
0
Fork 0
mirror of https://github.com/AtHeartEngineer/halo2.git synced 2026-01-10 13:07:58 -05:00
Code Issues Packages Projects Releases Wiki Activity

endoscale::chip: Implement endoscale_fixed_base, endoscale_var_base.

Browse Source
This commit is contained in:
therealyingtong
2022-02-28 22:49:55 +08:00
parent 432ecaf8b0
commit fda2a562a5
2 changed files with 337 additions and 17 deletions
Download Patch File Download Diff File Expand all files Collapse all files

349
halo2_gadgets/src/endoscale/chip/alg_1.rs
View File

@@ -1,15 +1,18 @@
use ff::PrimeFieldBits;
use ff::{Field, PrimeFieldBits};
use halo2_proofs::{
arithmetic::CurveAffine,
circuit::Layouter,
plonk::{Advice, Column, ConstraintSystem, Error, Selector},
arithmetic::{CurveAffine, FieldExt},
circuit::{Layouter, Region, Value},
plonk::{Advice, Assigned, Column, ConstraintSystem, Constraints, Error, Expression, Selector},
poly::Rotation,
};
use super::super::util::endoscale_point_pair;
use crate::{
ecc::chip::{add_incomplete, double, NonIdentityEccPoint},
utilities::{
bool_check,
decompose_running_sum::{RunningSum, RunningSumConfig},
double_and_add::DoubleAndAdd,
double_and_add::{DoubleAndAdd, X, Y},
},
};
@@ -83,17 +86,117 @@ where
meta.enable_equality(add_incomplete.y_p);
meta.create_gate("init double-and-add", |meta| {
// TODO
let selector = meta.query_selector(q_double_and_add_init);
// The accumulator is initialised to [2](φ(P) + P).
vec![selector]
// Check that the x-coordinate of the inputs to the incomplete addition
// are related as x, ζx.
// The y-coordinate is copy-constrained.
let incomplete_add_x_check = {
let x_p = meta.query_advice(add_incomplete.x_p, Rotation::prev());
let phi_x_p = meta.query_advice(add_incomplete.x_qr, Rotation::prev());
x_p * C::Base::ZETA - phi_x_p
};
// Check that the initial accumulator's y-coordinate `y_a` is consistent
// with the one derived internally by `double_and_add`.
let init_y_a_check = {
let y_a = meta.query_advice(double.y_r, Rotation::cur());
let derived_y_a = double_and_add.y_a(meta, Rotation::next());
y_a - derived_y_a
};
Constraints::with_selector(
selector,
[
("incomplete_add_x_check", incomplete_add_x_check),
("init_y_a_check", init_y_a_check),
],
)
});
meta.create_gate("final double-and-add", |meta| {
// TODO
// Check that the final witnessed y_a is consistent with the y_a
// derived internally by `double_and_add`.
let selector = meta.query_selector(q_double_and_add_final);
vec![selector]
// x_{A,i}
let x_a_prev = meta.query_advice(double_and_add.x_a, Rotation::prev());
// x_{A,i-1}
let x_a_cur = meta.query_advice(double_and_add.x_a, Rotation::cur());
// λ_{2,i}
let lambda2_prev = meta.query_advice(double_and_add.lambda_2, Rotation::prev());
let y_a_prev = double_and_add.y_a(meta, Rotation::prev());
let lhs = lambda2_prev * (x_a_prev - x_a_cur);
let rhs = {
let y_a_final = meta.query_advice(lambda_1, Rotation::cur());
y_a_prev + y_a_final
};
Constraints::with_selector(selector, [lhs - rhs])
});
/*
The accumulator is initialised to [2](φ(P) + P) = (init_x, init_y).
| pair.0 | pair.1 | base.0 | base.1 | double_and_add.x_a | double_and_add.lambda_1| <- column names
---------------------------------------------------------------------------------------------------|
| b_0 | b_1 | init endo_x | init endo_y | init acc_x | init acc_y |
| ... | ... | ... | ... | ... | (acc_y not witnessed) |
| b_{n-2}| b_{n-1}| final endo_x | final endo_y | final acc_x | final acc_y |
(0, 0) -> (P_x, -P_y)
(0, 1) -> (ζ * P_x, -P_y)
(1, 0) -> (P_x, P_y)
(1, 1) -> (ζ * P_x, P_y)
*/
meta.create_gate("Endoscale base", |meta| {
let q_endoscale_base = meta.query_selector(q_endoscale_base);
// Pair of bits from the decomposition.
let b_0 = meta.query_advice(pair.0, Rotation::cur());
let b_1 = meta.query_advice(pair.1, Rotation::cur());
// Boolean-constrain b_0, b_1
let b_0_check = bool_check(b_0.clone());
let b_1_check = bool_check(b_1.clone());
// Check that `b_0, b_1` are consistent with the running sum decomposition.
let decomposition_check = {
let word = b_0.clone() + Expression::Constant(C::Base::from(2)) * b_1.clone();
let expected_word = running_sum_pairs.window_expr(meta);
word - expected_word
};
// If the first bit is not set, check that endo_y = -P_y
let y_check = {
let endo_y = double_and_add.y_p(meta, Rotation::cur());
let p_y = meta.query_advice(base.1, Rotation::cur());
let not_b0 = Expression::Constant(C::Base::one()) - b_0;
not_b0 * (endo_y + p_y)
};
// If the second bit is set, check that endo_x = ζ * P_x
let x_check = {
let endo_x = meta.query_advice(double_and_add.x_p, Rotation::cur());
let p_x = meta.query_advice(base.0, Rotation::cur());
let zeta = Expression::Constant(C::Base::ZETA);
b_1 * (endo_x - zeta * p_x)
};
Constraints::with_selector(
q_endoscale_base,
std::array::IntoIter::new([
("b_0_check", b_0_check),
("b_1_check", b_1_check),
("decomposition_check", decomposition_check),
("x_check", x_check),
("y_check", y_check),
]),
)
});
Self {
@@ -112,19 +215,231 @@ where
pub(super) fn endoscale_fixed_base(
&self,
mut _layouter: &mut impl Layouter<C::Base>,
_bitstring: &RunningSum<C::Base, 2>,
_bases: &C,
layouter: &mut impl Layouter<C::Base>,
bitstring: &RunningSum<C::Base, 2>,
base: &C,
) -> Result<NonIdentityEccPoint<C>, Error> {
todo!()
layouter.assign_region(
|| "endoscale with fixed base",
|mut region| {
let offset = 0;
let base = {
// Assign base_x
let x = region.assign_advice_from_constant(
|| "base_x",
self.add_incomplete.x_p,
offset,
Assigned::from(*base.coordinates().unwrap().x()),
)?;
// Assign base_y
let y = region.assign_advice_from_constant(
|| "base_y",
self.add_incomplete.y_p,
offset,
Assigned::from(*base.coordinates().unwrap().y()),
)?;
NonIdentityEccPoint::from_coordinates_unchecked(x, y)
};
self.endoscale_base_inner(&mut region, offset, &base, bitstring)
},
)
}
pub(super) fn endoscale_var_base(
&self,
mut _layouter: &mut impl Layouter<C::Base>,
_bitstring: &RunningSum<C::Base, 2>,
_bases: &NonIdentityEccPoint<C>,
layouter: &mut impl Layouter<C::Base>,
bitstring: &RunningSum<C::Base, 2>,
base: &NonIdentityEccPoint<C>,
) -> Result<NonIdentityEccPoint<C>, Error> {
todo!()
layouter.assign_region(
|| "endoscale with variable base",
|mut region| {
let offset = 0;
let base = {
let x = base.x().copy_advice(
|| "base_x",
&mut region,
self.add_incomplete.x_p,
offset,
)?;
let y = base.y().copy_advice(
|| "base_y",
&mut region,
self.add_incomplete.y_p,
offset,
)?;
NonIdentityEccPoint::from_coordinates_unchecked(x.into(), y.into())
};
self.endoscale_base_inner(&mut region, offset, &base, bitstring)
},
)
}
}
impl<C: CurveAffine> Alg1Config<C>
where
C::Base: PrimeFieldBits,
{
#[allow(clippy::type_complexity)]
fn endoscale_base_init(
&self,
region: &mut Region<'_, C::Base>,
mut offset: usize,
base: &NonIdentityEccPoint<C>,
) -> Result<(usize, (X<C::Base>, Y<C::Base>)), Error> {
// The accumulator is initialised to [2](φ(P) + P)
self.q_double_and_add_init.enable(region, offset + 1)?;
// Incomplete addition of (φ(P) + P), where φ(P) = φ((x, y)) = (ζx, y)
let sum = {
let zeta_x = base.x().value().map(|p| Assigned::from(*p * C::Base::ZETA));
let zeta_x =
region.assign_advice(|| "ζ * x", self.add_incomplete.x_qr, offset, || zeta_x)?;
let phi_p = NonIdentityEccPoint::from_coordinates_unchecked(zeta_x, base.y().into());
self.add_incomplete
.assign_region(base, &phi_p, offset, region)?
};
offset += 1;
let acc = self
.double
.assign_region(&sum, offset, region)
.map(|acc| (X(acc.x().into()), Y(acc.y().value().copied().into())))?;
offset += 1;
Ok((offset, acc))
}
#[allow(clippy::type_complexity)]
fn endoscale_base_main(
&self,
region: &mut Region<'_, C::Base>,
mut offset: usize,
mut acc: (X<C::Base>, Y<C::Base>),
base: &NonIdentityEccPoint<C>,
// Bitstring decomposed into 2-bit windows using a running sum.
// This internally enables the `q_range_check` selector, which is
// used in the "Endoscale base" gate.
bitstring: &RunningSum<C::Base, 2>,
) -> Result<(usize, (X<C::Base>, Y<C::Base>)), Error> {
// Copy in running sum
for (idx, z) in bitstring.zs().iter().enumerate() {
z.copy_advice(
|| format!("z[{:?}]", idx),
region,
self.running_sum_pairs.z(),
offset + idx,
)?;
}
// Enable selector for steady-state double-and-add on all but last row
for idx in 0..(bitstring.bits().len() - 1) {
self.q_double_and_add.enable(region, offset + idx)?;
}
for (pair_idx, pair) in bitstring.bits().iter().enumerate() {
self.q_endoscale_base.enable(region, offset)?;
// Assign base
base.x()
.copy_advice(|| "base_x", region, self.base.0, offset)?;
base.y()
.copy_advice(|| "base_y", region, self.base.1, offset)?;
// Assign b_0
let b_0 = pair.map(|pair| pair[0]);
region.assign_advice(
|| format!("pair_idx: {}, b_0", pair_idx),
self.pair.0,
offset,
|| b_0.map(|b| C::Base::from(b as u64)),
)?;
// Assign b_1
let b_1 = pair.map(|pair| pair[1]);
region.assign_advice(
|| format!("pair_idx: {}, b_1", pair_idx),
self.pair.1,
offset,
|| b_1.map(|b| C::Base::from(b as u64)),
)?;
let endo = {
let base = base.point();
let endo = pair
.zip(base)
.map(|(pair, base)| endoscale_point_pair::<C>(pair, base).unwrap());
let endo_x = endo.map(|endo| *endo.coordinates().unwrap().x());
let endo_y = endo.map(|endo| *endo.coordinates().unwrap().y());
(endo_x, endo_y)
};
// Add endo to acc.
acc = self.double_and_add.assign_region(
region,
offset,
(endo.0.map(|v| v.into()), endo.1.map(|v| v.into())),
acc.0,
acc.1,
)?;
offset += 1;
}
Ok((offset, acc))
}
#[allow(clippy::type_complexity)]
fn endoscale_base_final(
&self,
region: &mut Region<'_, C::Base>,
offset: usize,
(x, y): (X<C::Base>, Y<C::Base>),
) -> Result<NonIdentityEccPoint<C>, Error> {
self.q_double_and_add_final.enable(region, offset)?;
let y =
region.assign_advice(|| "final y_a", self.double_and_add.lambda_1, offset, || *y)?;
Ok(NonIdentityEccPoint::from_coordinates_unchecked(x.0, y))
}
fn endoscale_base_inner(
&self,
region: &mut Region<'_, C::Base>,
offset: usize,
base: &NonIdentityEccPoint<C>,
bitstring: &RunningSum<C::Base, 2>,
) -> Result<NonIdentityEccPoint<C>, Error> {
let (offset, acc) = self.endoscale_base_init(region, offset, base)?;
let (offset, (x, y)) = self.endoscale_base_main(region, offset, acc, base, bitstring)?;
self.endoscale_base_final(region, offset, (x, y))
}
}
impl<F: FieldExt + PrimeFieldBits> RunningSum<F, 2> {
fn bits(&self) -> Vec<Value<[bool; 2]>> {
self.windows()
.iter()
.map(|window| {
window.map(|window| {
window
.to_le_bits()
.into_iter()
.take(2)
.collect::<Vec<_>>()
.try_into()
.unwrap()
})
})
.collect()
}
}

5
halo2_gadgets/src/utilities/decompose_running_sum.rs
View File

@@ -83,6 +83,11 @@ impl<F: FieldExt + PrimeFieldBits, const WINDOW_NUM_BITS: usize>
self.q_range_check
}
/// Returns the `z` advice column of this [`RunningSumConfig`].
pub(crate) fn z(&self) -> Column<Advice> {
self.z
}
/// `perm` MUST include the advice column `z`.
///
/// # Side-effects