diff --git a/Cargo.toml b/Cargo.toml index 4842be2d..f2884cfa 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -38,7 +38,7 @@ plotters = { version = "0.3.0", optional = true } [dependencies.halo2] git = "https://github.com/zcash/halo2.git" -rev = "d8e4f24df44da94ab5cacbc531517e2b63fe45ee" +rev = "d04b532368d05b505e622f8cac4c0693574fbd93" [dependencies.reddsa] git = "https://github.com/str4d/redjubjub.git" diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs index 31d252e3..6e26971c 100644 --- a/src/circuit/gadget/ecc.rs +++ b/src/circuit/gadget/ecc.rs @@ -9,6 +9,8 @@ use halo2::{ plonk::Error, }; +pub mod chip; + /// The set of circuit instructions required to use the ECC gadgets. pub trait EccInstructions: Chip { /// Variable representing an element of the elliptic curve's base field, that @@ -36,16 +38,18 @@ pub trait EccInstructions: Chip { /// Variable representing the affine short Weierstrass x-coordinate of an /// elliptic curve point. type X: Clone + Debug; - /// Variable representing the set of fixed bases in the circuit. + /// Enumeration of the set of fixed bases to be used in full-width scalar mul. type FixedPoints: Clone + Debug; - /// Variable representing the set of fixed bases to be used in scalar - /// multiplication with a short signed exponent. + /// Enumeration of the set of fixed bases to be used in short signed scalar mul. type FixedPointsShort: Clone + Debug; - /// Variable representing a fixed elliptic curve point (constant in the circuit). - type FixedPoint: Clone + Debug; - /// Variable representing a fixed elliptic curve point (constant in the circuit) - /// to be used in scalar multiplication with a short signed exponent. - type FixedPointShort: Clone + Debug; + + /// Constrains point `a` to be equal in value to point `b`. + fn constrain_equal( + &self, + layouter: &mut impl Layouter, + a: &Self::Point, + b: &Self::Point, + ) -> Result<(), Error>; /// Witnesses the given base field element as a private input to the circuit /// for variable-base scalar mul. @@ -72,6 +76,7 @@ pub trait EccInstructions: Chip { ) -> Result; /// Witnesses the given point as a private input to the circuit. + /// This maps the identity to (0, 0) in affine coordinates. fn witness_point( &self, layouter: &mut impl Layouter, @@ -81,18 +86,6 @@ pub trait EccInstructions: Chip { /// Extracts the x-coordinate of a point. fn extract_p(point: &Self::Point) -> &Self::X; - /// Returns a fixed point that had been previously loaded into the circuit. - /// The pre-loaded cells are used to set up equality constraints in other - /// parts of the circuit where the fixed base is used. - fn get_fixed(&self, fixed_points: Self::FixedPoints) -> Result; - - /// Returns a fixed point to be used in scalar multiplication with a signed - /// short exponent. - fn get_fixed_short( - &self, - fixed_points: Self::FixedPointsShort, - ) -> Result; - /// Performs incomplete point addition, returning `a + b`. /// /// This returns an error in exceptional cases. @@ -111,14 +104,8 @@ pub trait EccInstructions: Chip { b: &Self::Point, ) -> Result; - /// Performs point doubling, returning `[2] a`. - fn double( - &self, - layouter: &mut impl Layouter, - a: &Self::Point, - ) -> Result; - /// Performs variable-base scalar multiplication, returning `[scalar] base`. + /// Multiplication of the identity `[scalar] π’ͺ ` returns an error. fn mul( &self, layouter: &mut impl Layouter, @@ -131,7 +118,7 @@ pub trait EccInstructions: Chip { &self, layouter: &mut impl Layouter, scalar: &Self::ScalarFixed, - base: &Self::FixedPoint, + base: &Self::FixedPoints, ) -> Result; /// Performs fixed-base scalar multiplication using a short signed scalar, returning `[scalar] base`. @@ -139,7 +126,7 @@ pub trait EccInstructions: Chip { &self, layouter: &mut impl Layouter, scalar: &Self::ScalarFixedShort, - base: &Self::FixedPointShort, + base: &Self::FixedPointsShort, ) -> Result; } @@ -174,12 +161,18 @@ impl + Clone + Debug + Eq> ScalarVar /// A full-width element of the given elliptic curve's scalar field, to be used for fixed-base scalar mul. #[derive(Debug)] -pub struct ScalarFixed + Clone + Debug + Eq> { +pub struct ScalarFixed +where + EccChip: EccInstructions + Clone + Debug + Eq, +{ chip: EccChip, inner: EccChip::ScalarFixed, } -impl + Clone + Debug + Eq> ScalarFixed { +impl ScalarFixed +where + EccChip: EccInstructions + Clone + Debug + Eq, +{ /// Constructs a new ScalarFixed with the given value. pub fn new( chip: EccChip, @@ -193,13 +186,17 @@ impl + Clone + Debug + Eq> ScalarFix /// A signed short element of the given elliptic curve's scalar field, to be used for fixed-base scalar mul. #[derive(Debug)] -pub struct ScalarFixedShort + Clone + Debug + Eq> { +pub struct ScalarFixedShort +where + EccChip: EccInstructions + Clone + Debug + Eq, +{ chip: EccChip, inner: EccChip::ScalarFixedShort, } -impl + Clone + Debug + Eq> - ScalarFixedShort +impl ScalarFixedShort +where + EccChip: EccInstructions + Clone + Debug + Eq, { /// Constructs a new ScalarFixedShort with the given value. /// @@ -231,7 +228,7 @@ impl + Clone + Debug + Eq> } /// An elliptic curve point over the given curve. -#[derive(Debug)] +#[derive(Copy, Clone, Debug)] pub struct Point + Clone + Debug + Eq> { chip: EccChip, inner: EccChip::Point, @@ -248,6 +245,16 @@ impl + Clone + Debug + Eq> Point, + other: &Self, + ) -> Result<(), Error> { + self.chip + .constrain_equal(&mut layouter, &self.inner, &other.inner) + } + /// Extracts the x-coordinate of a point. pub fn extract_p(&self) -> X { X::from_inner(self.chip.clone(), EccChip::extract_p(&self.inner).clone()) @@ -318,18 +325,18 @@ impl + Clone + Debug + Eq> X + Clone + Debug + Eq> { +pub struct FixedPoint +where + EccChip: EccInstructions + Clone + Debug + Eq, +{ chip: EccChip, - inner: EccChip::FixedPoint, + inner: EccChip::FixedPoints, } -impl + Clone + Debug + Eq> FixedPoint { - /// Gets a reference to the specified fixed point in the circuit. - pub fn get(chip: EccChip, point: EccChip::FixedPoints) -> Result { - chip.get_fixed(point) - .map(|inner| FixedPoint { chip, inner }) - } - +impl FixedPoint +where + EccChip: EccInstructions + Clone + Debug + Eq, +{ /// Returns `[by] self`. pub fn mul( &self, @@ -344,23 +351,28 @@ impl + Clone + Debug + Eq> FixedPoin inner, }) } + + /// Wraps the given fixed base (obtained directly from an instruction) in a gadget. + pub fn from_inner(chip: EccChip, inner: EccChip::FixedPoints) -> Self { + FixedPoint { chip, inner } + } } /// A constant elliptic curve point over the given curve, used in scalar multiplication /// with a short signed exponent #[derive(Clone, Debug)] -pub struct FixedPointShort + Clone + Debug + Eq> { +pub struct FixedPointShort +where + EccChip: EccInstructions + Clone + Debug + Eq, +{ chip: EccChip, - inner: EccChip::FixedPointShort, + inner: EccChip::FixedPointsShort, } -impl + Clone + Debug + Eq> FixedPointShort { - /// Gets a reference to the specified fixed point in the circuit. - pub fn get(chip: EccChip, point: EccChip::FixedPointsShort) -> Result { - chip.get_fixed_short(point) - .map(|inner| FixedPointShort { chip, inner }) - } - +impl FixedPointShort +where + EccChip: EccInstructions + Clone + Debug + Eq, +{ /// Returns `[by] self`. pub fn mul( &self, @@ -375,4 +387,123 @@ impl + Clone + Debug + Eq> FixedPoin inner, }) } + + /// Wraps the given fixed base (obtained directly from an instruction) in a gadget. + pub fn from_inner(chip: EccChip, inner: EccChip::FixedPointsShort) -> Self { + FixedPointShort { chip, inner } + } +} + +#[cfg(test)] +mod tests { + use group::{prime::PrimeCurveAffine, Curve, Group}; + + use halo2::{ + circuit::{layouter::SingleChipLayouter, Layouter}, + dev::MockProver, + plonk::{Assignment, Circuit, ConstraintSystem, Error}, + }; + use pasta_curves::pallas; + + use super::chip::{EccChip, EccConfig}; + + struct MyCircuit {} + + #[allow(non_snake_case)] + impl Circuit for MyCircuit { + type Config = EccConfig; + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let advices = [ + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + meta.advice_column(), + ]; + + let perm = meta.permutation( + &advices + .iter() + .map(|advice| (*advice).into()) + .collect::>(), + ); + + EccChip::configure(meta, advices, perm) + } + + fn synthesize( + &self, + cs: &mut impl Assignment, + config: Self::Config, + ) -> Result<(), Error> { + let mut layouter = SingleChipLayouter::new(cs)?; + let chip = EccChip::construct(config); + + // Generate a random point P + let p_val = pallas::Point::random(rand::rngs::OsRng).to_affine(); // P + let p = super::Point::new(chip.clone(), layouter.namespace(|| "P"), Some(p_val))?; + let p_neg = -p_val; + let p_neg = super::Point::new(chip.clone(), layouter.namespace(|| "-P"), Some(p_neg))?; + + // Generate a random point Q + let q_val = pallas::Point::random(rand::rngs::OsRng).to_affine(); // Q + let q = super::Point::new(chip.clone(), layouter.namespace(|| "Q"), Some(q_val))?; + + // Make sure P and Q are not the same point. + assert_ne!(p_val, q_val); + + // Generate a (0,0) point to be used in other tests. + let zero = { + super::Point::new( + chip.clone(), + layouter.namespace(|| "identity"), + Some(pallas::Affine::identity()), + )? + }; + + // Test complete addition + { + super::chip::add::tests::test_add( + chip.clone(), + layouter.namespace(|| "complete addition"), + &zero, + p_val, + &p, + q_val, + &q, + &p_neg, + )?; + } + + // Test incomplete addition + { + super::chip::add_incomplete::tests::test_add_incomplete( + chip, + layouter.namespace(|| "incomplete addition"), + &zero, + p_val, + &p, + q_val, + &q, + &p_neg, + )?; + } + + Ok(()) + } + } + + #[test] + fn ecc() { + let k = 6; + let circuit = MyCircuit {}; + let prover = MockProver::run(k, &circuit, vec![]).unwrap(); + assert_eq!(prover.verify(), Ok(())) + } } diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs new file mode 100644 index 00000000..e398547c --- /dev/null +++ b/src/circuit/gadget/ecc/chip.rs @@ -0,0 +1,291 @@ +use super::EccInstructions; +use crate::circuit::gadget::utilities::{copy, CellValue, Var}; +use crate::constants; + +use group::prime::PrimeCurveAffine; +use halo2::{ + circuit::{Chip, Layouter}, + plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation, Selector}, +}; +use pasta_curves::{arithmetic::CurveAffine, pallas}; + +pub(super) mod add; +pub(super) mod add_incomplete; +// pub(super) mod mul; +// pub(super) mod mul_fixed; +pub(super) mod witness_point; +// pub(super) mod witness_scalar_fixed; + +/// A curve point represented in affine (x, y) coordinates. Each coordinate is +/// assigned to a cell. +#[derive(Clone, Debug)] +pub struct EccPoint { + /// x-coordinate + x: CellValue, + /// y-coordinate + y: CellValue, +} + +impl EccPoint { + /// Returns the value of this curve point, if known. + pub fn point(&self) -> Option { + match (self.x.value(), self.y.value()) { + (Some(x), Some(y)) => { + if x == pallas::Base::zero() && y == pallas::Base::zero() { + Some(pallas::Affine::identity()) + } else { + Some(pallas::Affine::from_xy(x, y).unwrap()) + } + } + _ => None, + } + } + /// The cell containing the affine short-Weierstrass x-coordinate, + /// or 0 for the zero point. + pub fn x(&self) -> CellValue { + self.x + } + /// The cell containing the affine short-Weierstrass y-coordinate, + /// or 0 for the zero point. + pub fn y(&self) -> CellValue { + self.y + } +} + +/// Configuration for the ECC chip +#[derive(Clone, Debug, Eq, PartialEq)] +#[allow(non_snake_case)] +pub struct EccConfig { + /// Advice columns needed by instructions in the ECC chip. + pub advices: [Column; 10], + + /// Coefficients of interpolation polynomials for x-coordinates (used in fixed-base scalar multiplication) + pub lagrange_coeffs: [Column; constants::H], + /// Fixed z such that y + z = u^2 some square, and -y + z is a non-square. (Used in fixed-base scalar multiplication) + pub fixed_z: Column, + + /// Incomplete addition + pub q_add_incomplete: Selector, + /// Complete addition + pub q_add: Selector, + /// Variable-base scalar multiplication (hi half) + pub q_mul_hi: Selector, + /// Variable-base scalar multiplication (lo half) + pub q_mul_lo: Selector, + /// Selector used in scalar decomposition for variable-base scalar mul + pub q_mul_decompose_var: Selector, + /// Variable-base scalar multiplication (final scalar) + pub q_mul_complete: Selector, + /// Fixed-base full-width scalar multiplication + pub q_mul_fixed: Selector, + /// Fixed-base signed short scalar multiplication + pub q_mul_fixed_short: Selector, + /// Witness point + pub q_point: Selector, + /// Witness full-width scalar for fixed-base scalar mul + pub q_scalar_fixed: Selector, + /// Witness signed short scalar for full-width fixed-base scalar mul + pub q_scalar_fixed_short: Selector, + /// Permutation + pub perm: Permutation, +} + +/// A chip implementing EccInstructions +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct EccChip { + config: EccConfig, +} + +impl Chip for EccChip { + type Config = EccConfig; + type Loaded = (); + + fn config(&self) -> &Self::Config { + &self.config + } + + fn loaded(&self) -> &Self::Loaded { + &() + } +} + +impl EccChip { + pub fn construct(config: >::Config) -> Self { + Self { config } + } + + #[allow(non_snake_case)] + pub fn configure( + meta: &mut ConstraintSystem, + advices: [Column; 10], + perm: Permutation, + ) -> >::Config { + let config = EccConfig { + advices, + lagrange_coeffs: [ + meta.fixed_column(), + meta.fixed_column(), + meta.fixed_column(), + meta.fixed_column(), + meta.fixed_column(), + meta.fixed_column(), + meta.fixed_column(), + meta.fixed_column(), + ], + fixed_z: meta.fixed_column(), + q_add_incomplete: meta.selector(), + q_add: meta.selector(), + q_mul_hi: meta.selector(), + q_mul_lo: meta.selector(), + q_mul_decompose_var: meta.selector(), + q_mul_complete: meta.selector(), + q_mul_fixed: meta.selector(), + q_mul_fixed_short: meta.selector(), + q_point: meta.selector(), + q_scalar_fixed: meta.selector(), + q_scalar_fixed_short: meta.selector(), + perm, + }; + + // Create witness point gate + { + let config: witness_point::Config = (&config).into(); + config.create_gate(meta); + } + + // Create incomplete point addition gate + { + let config: add_incomplete::Config = (&config).into(); + config.create_gate(meta); + } + + // Create complete point addition gate + { + let add_config: add::Config = (&config).into(); + add_config.create_gate(meta); + } + + config + } +} + +impl EccInstructions for EccChip { + type ScalarFixed = (); // TODO + type ScalarFixedShort = (); // TODO + type ScalarVar = (); // TODO + type Point = EccPoint; + type X = CellValue; + type FixedPoints = (); // TODO + type FixedPointsShort = (); // TODO + + fn constrain_equal( + &self, + layouter: &mut impl Layouter, + a: &Self::Point, + b: &Self::Point, + ) -> Result<(), Error> { + let config = self.config().clone(); + layouter.assign_region( + || "constrain equal", + |mut region| { + // Constrain x-coordinates + region.constrain_equal(&config.perm, a.x().cell(), b.x().cell())?; + // Constrain x-coordinates + region.constrain_equal(&config.perm, a.y().cell(), b.y().cell()) + }, + ) + } + + fn witness_scalar_var( + &self, + _layouter: &mut impl Layouter, + _value: Option, + ) -> Result { + todo!() + } + + fn witness_scalar_fixed( + &self, + _layouter: &mut impl Layouter, + _value: Option, + ) -> Result { + todo!() + } + + fn witness_scalar_fixed_short( + &self, + _layouter: &mut impl Layouter, + _value: Option, + ) -> Result { + todo!() + } + + fn witness_point( + &self, + layouter: &mut impl Layouter, + value: Option, + ) -> Result { + let config: witness_point::Config = self.config().into(); + layouter.assign_region( + || "witness point", + |mut region| config.assign_region(value, 0, &mut region), + ) + } + + fn extract_p(point: &Self::Point) -> &Self::X { + &point.x + } + + fn add_incomplete( + &self, + layouter: &mut impl Layouter, + a: &Self::Point, + b: &Self::Point, + ) -> Result { + let config: add_incomplete::Config = self.config().into(); + layouter.assign_region( + || "incomplete point addition", + |mut region| config.assign_region(a, b, 0, &mut region), + ) + } + + fn add( + &self, + layouter: &mut impl Layouter, + a: &Self::Point, + b: &Self::Point, + ) -> Result { + let config: add::Config = self.config().into(); + layouter.assign_region( + || "complete point addition", + |mut region| config.assign_region(a, b, 0, &mut region), + ) + } + + fn mul( + &self, + _layouter: &mut impl Layouter, + _scalar: &Self::ScalarVar, + _base: &Self::Point, + ) -> Result { + todo!() + } + + fn mul_fixed( + &self, + _layouter: &mut impl Layouter, + _scalar: &Self::ScalarFixed, + _base: &Self::FixedPoints, + ) -> Result { + todo!() + } + + fn mul_fixed_short( + &self, + _layouter: &mut impl Layouter, + _scalar: &Self::ScalarFixedShort, + _base: &Self::FixedPointsShort, + ) -> Result { + todo!() + } +} diff --git a/src/circuit/gadget/ecc/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs new file mode 100644 index 00000000..0ae7f094 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/add.rs @@ -0,0 +1,493 @@ +use std::array; + +use super::{copy, CellValue, EccConfig, EccPoint, Var}; +use ff::Field; +use halo2::{ + arithmetic::BatchInvert, + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector}, + poly::Rotation, +}; +use pasta_curves::{arithmetic::FieldExt, pallas}; +use std::collections::HashSet; + +#[derive(Clone, Debug)] +pub struct Config { + q_add: Selector, + // lambda + lambda: Column, + // x-coordinate of P in P + Q = R + pub x_p: Column, + // y-coordinate of P in P + Q = R + pub y_p: Column, + // x-coordinate of Q or R in P + Q = R + pub x_qr: Column, + // y-coordinate of Q or R in P + Q = R + pub y_qr: Column, + // Ξ± = inv0(x_q - x_p) + alpha: Column, + // Ξ² = inv0(x_p) + beta: Column, + // Ξ³ = inv0(x_q) + gamma: Column, + // Ξ΄ = inv0(y_p + y_q) if x_q = x_p, 0 otherwise + delta: Column, + // Permutation + perm: Permutation, +} + +impl From<&EccConfig> for Config { + fn from(ecc_config: &EccConfig) -> Self { + Self { + q_add: ecc_config.q_add, + x_p: ecc_config.advices[0], + y_p: ecc_config.advices[1], + x_qr: ecc_config.advices[2], + y_qr: ecc_config.advices[3], + lambda: ecc_config.advices[4], + alpha: ecc_config.advices[5], + beta: ecc_config.advices[6], + gamma: ecc_config.advices[7], + delta: ecc_config.advices[8], + perm: ecc_config.perm.clone(), + } + } +} + +impl Config { + pub(crate) fn advice_columns(&self) -> HashSet> { + core::array::IntoIter::new([ + self.x_p, + self.y_p, + self.x_qr, + self.y_qr, + self.lambda, + self.alpha, + self.beta, + self.gamma, + self.delta, + ]) + .collect() + } + + pub(crate) fn create_gate(&self, meta: &mut ConstraintSystem) { + meta.create_gate("complete addition gates", |meta| { + let q_add = meta.query_selector(self.q_add); + let x_p = meta.query_advice(self.x_p, Rotation::cur()); + let y_p = meta.query_advice(self.y_p, Rotation::cur()); + let x_q = meta.query_advice(self.x_qr, Rotation::cur()); + let y_q = meta.query_advice(self.y_qr, Rotation::cur()); + let x_r = meta.query_advice(self.x_qr, Rotation::next()); + let y_r = meta.query_advice(self.y_qr, Rotation::next()); + let lambda = meta.query_advice(self.lambda, Rotation::cur()); + + // Ξ± = inv0(x_q - x_p) + let alpha = meta.query_advice(self.alpha, Rotation::cur()); + // Ξ² = inv0(x_p) + let beta = meta.query_advice(self.beta, Rotation::cur()); + // Ξ³ = inv0(x_q) + let gamma = meta.query_advice(self.gamma, Rotation::cur()); + // Ξ΄ = inv0(y_p + y_q) if x_q = x_p, 0 otherwise + let delta = meta.query_advice(self.delta, Rotation::cur()); + + // Useful composite expressions + // Ξ± β‹…(x_q - x_p) + let if_alpha = (x_q.clone() - x_p.clone()) * alpha; + // Ξ² β‹… x_p + let if_beta = x_p.clone() * beta; + // Ξ³ β‹… x_q + let if_gamma = x_q.clone() * gamma; + // Ξ΄ β‹…(y_p + y_q) + let if_delta = (y_q.clone() + y_p.clone()) * delta; + + // Useful constants + let one = Expression::Constant(pallas::Base::one()); + let two = Expression::Constant(pallas::Base::from_u64(2)); + let three = Expression::Constant(pallas::Base::from_u64(3)); + + // (x_q βˆ’ x_p)β‹…((x_q βˆ’ x_p)β‹…Ξ» βˆ’ (y_qβˆ’y_p)) = 0 + let poly1 = { + let x_q_minus_x_p = x_q.clone() - x_p.clone(); // (x_q βˆ’ x_p) + + let y_q_minus_y_p = y_q.clone() - y_p.clone(); // (y_q βˆ’ y_p) + let incomplete = x_q_minus_x_p.clone() * lambda.clone() - y_q_minus_y_p; // (x_q βˆ’ x_p)β‹…Ξ» βˆ’ (y_qβˆ’y_p) + + // q_add β‹…(x_q βˆ’ x_p)β‹…((x_q βˆ’ x_p)β‹…Ξ» βˆ’ (y_qβˆ’y_p)) + x_q_minus_x_p * incomplete + }; + + // (1 - (x_q - x_p)β‹…Ξ±)β‹…(2y_p β‹…Ξ» - 3x_p^2) = 0 + let poly2 = { + let three_x_p_sq = three * x_p.clone().square(); // 3x_p^2 + let two_y_p = two * y_p.clone(); // 2y_p + let tangent_line = two_y_p * lambda.clone() - three_x_p_sq; // (2y_p β‹…Ξ» - 3x_p^2) + + // q_add β‹…(1 - (x_q - x_p)β‹…Ξ±)β‹…(2y_p β‹…Ξ» - 3x_p^2) + (one.clone() - if_alpha.clone()) * tangent_line + }; + + // x_pβ‹…x_qβ‹…(x_q - x_p)β‹…(Ξ»^2 - x_p - x_q - x_r) = 0 + let secant_line = lambda.clone().square() - x_p.clone() - x_q.clone() - x_r.clone(); // (Ξ»^2 - x_p - x_q - x_r) + let poly3 = { + let x_q_minus_x_p = x_q.clone() - x_p.clone(); // (x_q - x_p) + + // x_pβ‹…x_qβ‹…(x_q - x_p)β‹…(Ξ»^2 - x_p - x_q - x_r) + x_p.clone() * x_q.clone() * x_q_minus_x_p * secant_line.clone() + }; + + // x_pβ‹…x_qβ‹…(x_q - x_p)β‹…(Ξ» β‹…(x_p - x_r) - y_p - y_r) = 0 + let poly4 = { + let x_q_minus_x_p = x_q.clone() - x_p.clone(); // (x_q - x_p) + let x_p_minus_x_r = x_p.clone() - x_r.clone(); // (x_p - x_r) + + // x_pβ‹…x_qβ‹…(x_q - x_p)β‹…(Ξ» β‹…(x_p - x_r) - y_p - y_r) + x_p.clone() + * x_q.clone() + * x_q_minus_x_p + * (lambda.clone() * x_p_minus_x_r - y_p.clone() - y_r.clone()) + }; + + // x_pβ‹…x_qβ‹…(y_q + y_p)β‹…(Ξ»^2 - x_p - x_q - x_r) = 0 + let poly5 = { + let y_q_plus_y_p = y_q.clone() + y_p.clone(); // (y_q + y_p) + + // x_pβ‹…x_qβ‹…(y_q + y_p)β‹…(Ξ»^2 - x_p - x_q - x_r) + x_p.clone() * x_q.clone() * y_q_plus_y_p * secant_line + }; + + // x_pβ‹…x_qβ‹…(y_q + y_p)β‹…(Ξ» β‹…(x_p - x_r) - y_p - y_r) = 0 + let poly6 = { + let y_q_plus_y_p = y_q.clone() + y_p.clone(); // (y_q + y_p) + let x_p_minus_x_r = x_p.clone() - x_r.clone(); // (x_p - x_r) + + // x_pβ‹…x_qβ‹…(y_q + y_p)β‹…(Ξ» β‹…(x_p - x_r) - y_p - y_r) + x_p.clone() + * x_q.clone() + * y_q_plus_y_p + * (lambda * x_p_minus_x_r - y_p.clone() - y_r.clone()) + }; + + // (1 - x_p * Ξ²) * (x_r - x_q) = 0 + let poly7 = (one.clone() - if_beta.clone()) * (x_r.clone() - x_q); + + // (1 - x_p * Ξ²) * (y_r - y_q) = 0 + let poly8 = (one.clone() - if_beta) * (y_r.clone() - y_q); + + // (1 - x_q * Ξ³) * (x_r - x_p) = 0 + let poly9 = (one.clone() - if_gamma.clone()) * (x_r.clone() - x_p); + + // (1 - x_q * Ξ³) * (y_r - y_p) = 0 + let poly10 = (one.clone() - if_gamma) * (y_r.clone() - y_p); + + // ((1 - (x_q - x_p) * Ξ± - (y_q + y_p) * Ξ΄)) * x_r + let poly11 = (one.clone() - if_alpha.clone() - if_delta.clone()) * x_r; + + // ((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) + }); + } + + pub(super) fn assign_region( + &self, + p: &EccPoint, + q: &EccPoint, + offset: usize, + region: &mut Region<'_, pallas::Base>, + ) -> Result { + // Enable `q_add` selector + self.q_add.enable(region, offset)?; + + // Copy point `p` into `x_p`, `y_p` columns + copy(region, || "x_p", self.x_p, offset, &p.x, &self.perm)?; + copy(region, || "y_p", self.y_p, offset, &p.y, &self.perm)?; + + // Copy point `q` into `x_qr`, `y_qr` columns + copy(region, || "x_q", self.x_qr, offset, &q.x, &self.perm)?; + copy(region, || "y_q", self.y_qr, offset, &q.y, &self.perm)?; + + let (x_p, y_p) = (p.x.value(), p.y.value()); + let (x_q, y_q) = (q.x.value(), q.y.value()); + + // [alpha, beta, gamma, delta] + // = [inv0(x_q - x_p), inv0(x_p), inv0(x_q), inv0(y_q + y_p)] + // where inv0(x) = 0 if x = 0, 1/x otherwise. + // + let (alpha, beta, gamma, delta) = { + let inverses = x_p + .zip(x_q) + .zip(y_p) + .zip(y_q) + .map(|(((x_p, x_q), y_p), y_q)| { + let alpha = x_q - x_p; + let beta = x_p; + let gamma = x_q; + let delta = y_q + y_p; + + let mut inverses = [alpha, beta, gamma, delta]; + inverses.batch_invert(); + inverses + }); + + if let Some([alpha, beta, gamma, delta]) = inverses { + (Some(alpha), Some(beta), Some(gamma), Some(delta)) + } else { + (None, None, None, None) + } + }; + + // Assign Ξ± = inv0(x_q - x_p) + region.assign_advice( + || "Ξ±", + self.alpha, + offset, + || alpha.ok_or(Error::SynthesisError), + )?; + + // Assign Ξ² = inv0(x_p) + region.assign_advice( + || "Ξ²", + self.beta, + offset, + || beta.ok_or(Error::SynthesisError), + )?; + + // Assign Ξ³ = inv0(x_q) + region.assign_advice( + || "Ξ³", + self.gamma, + offset, + || gamma.ok_or(Error::SynthesisError), + )?; + + // Assign Ξ΄ = inv0(y_q + y_p) if x_q = x_p, 0 otherwise + region.assign_advice( + || "Ξ΄", + self.delta, + offset, + || { + let x_p = x_p.ok_or(Error::SynthesisError)?; + let x_q = x_q.ok_or(Error::SynthesisError)?; + + if x_q == x_p { + delta.ok_or(Error::SynthesisError) + } else { + Ok(pallas::Base::zero()) + } + }, + )?; + + #[allow(clippy::collapsible_else_if)] + // Assign lambda + let lambda = + x_p.zip(y_p) + .zip(x_q) + .zip(y_q) + .zip(alpha) + .map(|((((x_p, y_p), x_q), y_q), alpha)| { + if x_q != x_p { + // Ξ» = (y_q - y_p)/(x_q - x_p) + // Here, alpha = inv0(x_q - x_p), which suffices since we + // know that x_q != x_p in this branch. + (y_q - y_p) * alpha + } else { + if y_p != pallas::Base::zero() { + // 3(x_p)^2 + let three_x_p_sq = pallas::Base::from_u64(3) * x_p.square(); + // 1 / 2(y_p) + let inv_two_y_p = y_p.invert().unwrap() * pallas::Base::TWO_INV; + // Ξ» = 3(x_p)^2 / 2(y_p) + three_x_p_sq * inv_two_y_p + } else { + pallas::Base::zero() + } + } + }); + region.assign_advice( + || "Ξ»", + self.lambda, + offset, + || lambda.ok_or(Error::SynthesisError), + )?; + + // Calculate (x_r, y_r) + let r = + x_p.zip(y_p) + .zip(x_q) + .zip(y_q) + .zip(lambda) + .map(|((((x_p, y_p), x_q), y_q), lambda)| { + { + if x_p == pallas::Base::zero() { + // 0 + Q = Q + (x_q, y_q) + } else if x_q == pallas::Base::zero() { + // P + 0 = P + (x_p, y_p) + } else if (x_q == x_p) && (y_q == -y_p) { + // P + (-P) maps to (0,0) + (pallas::Base::zero(), pallas::Base::zero()) + } else { + // x_r = Ξ»^2 - x_p - x_q + let x_r = lambda.square() - x_p - x_q; + // y_r = Ξ»(x_p - x_r) - y_p + let y_r = lambda * (x_p - x_r) - y_p; + (x_r, y_r) + } + } + }); + + // Assign x_r + let x_r = r.map(|r| r.0); + let x_r_cell = region.assign_advice( + || "x_r", + self.x_qr, + offset + 1, + || x_r.ok_or(Error::SynthesisError), + )?; + + // Assign y_r + let y_r = r.map(|r| r.1); + let y_r_cell = region.assign_advice( + || "y_r", + self.y_qr, + offset + 1, + || y_r.ok_or(Error::SynthesisError), + )?; + + let result = EccPoint { + x: CellValue::::new(x_r_cell, x_r), + y: CellValue::::new(y_r_cell, y_r), + }; + + #[cfg(test)] + // Check that the correct sum is obtained. + { + use group::Curve; + + let p = p.point(); + let q = q.point(); + let real_sum = p.zip(q).map(|(p, q)| p + q); + let result = result.point(); + + if let (Some(real_sum), Some(result)) = (real_sum, result) { + assert_eq!(real_sum.to_affine(), result); + } + } + + Ok(result) + } +} + +#[cfg(test)] +pub mod tests { + use group::{prime::PrimeCurveAffine, Curve}; + use halo2::{circuit::Layouter, plonk::Error}; + use pasta_curves::{arithmetic::CurveExt, pallas}; + + use crate::circuit::gadget::ecc::{EccInstructions, Point}; + + #[allow(clippy::too_many_arguments)] + pub fn test_add + Clone + Eq + std::fmt::Debug>( + chip: EccChip, + mut layouter: impl Layouter, + zero: &Point, + p_val: pallas::Affine, + p: &Point, + q_val: pallas::Affine, + q: &Point, + p_neg: &Point, + ) -> Result<(), Error> { + // Make sure P and Q are not the same point. + assert_ne!(p_val, q_val); + + // Check complete addition P + (-P) + { + let result = p.add(layouter.namespace(|| "P + (-P)"), p_neg)?; + result.constrain_equal(layouter.namespace(|| "P + (-P) = π’ͺ"), zero)?; + } + + // Check complete addition π’ͺ + π’ͺ + { + let result = zero.add(layouter.namespace(|| "π’ͺ + π’ͺ"), zero)?; + result.constrain_equal(layouter.namespace(|| "π’ͺ + π’ͺ = π’ͺ"), zero)?; + } + + // Check P + Q + { + let result = p.add(layouter.namespace(|| "P + Q"), q)?; + let witnessed_result = Point::new( + chip.clone(), + layouter.namespace(|| "witnessed P + Q"), + Some((p_val + q_val).to_affine()), + )?; + result.constrain_equal(layouter.namespace(|| "constrain P + Q"), &witnessed_result)?; + } + + // P + P + { + let result = p.add(layouter.namespace(|| "P + P"), p)?; + let witnessed_result = Point::new( + chip.clone(), + layouter.namespace(|| "witnessed P + P"), + Some((p_val + p_val).to_affine()), + )?; + result.constrain_equal(layouter.namespace(|| "constrain P + P"), &witnessed_result)?; + } + + // P + π’ͺ + { + let result = p.add(layouter.namespace(|| "P + π’ͺ"), zero)?; + result.constrain_equal(layouter.namespace(|| "P + π’ͺ = P"), p)?; + } + + // π’ͺ + P + { + let result = zero.add(layouter.namespace(|| "π’ͺ + P"), p)?; + result.constrain_equal(layouter.namespace(|| "π’ͺ + P = P"), p)?; + } + + // (x, y) + (ΞΆx, y) should behave like normal P + Q. + let endo_p = p_val.to_curve().endo(); + let endo_p = Point::new( + chip.clone(), + layouter.namespace(|| "endo(P)"), + Some(endo_p.to_affine()), + )?; + p.add(layouter.namespace(|| "P + endo(P)"), &endo_p)?; + + // (x, y) + (ΞΆx, -y) should also behave like normal P + Q. + let endo_p_neg = (-p_val).to_curve().endo(); + let endo_p_neg = Point::new( + chip.clone(), + layouter.namespace(|| "endo(-P)"), + Some(endo_p_neg.to_affine()), + )?; + p.add(layouter.namespace(|| "P + endo(-P)"), &endo_p_neg)?; + + // (x, y) + ((ΞΆ^2)x, y) + let endo_2_p = p_val.to_curve().endo().endo(); + let endo_2_p = Point::new( + chip.clone(), + layouter.namespace(|| "endo^2(P)"), + Some(endo_2_p.to_affine()), + )?; + p.add(layouter.namespace(|| "P + endo^2(P)"), &endo_2_p)?; + + // (x, y) + ((ΞΆ^2)x, -y) + let endo_2_p_neg = (-p_val).to_curve().endo().endo(); + let endo_2_p_neg = Point::new( + chip, + layouter.namespace(|| "endo^2(-P)"), + Some(endo_2_p_neg.to_affine()), + )?; + p.add(layouter.namespace(|| "P + endo^2(-P)"), &endo_2_p_neg)?; + + Ok(()) + } +} diff --git a/src/circuit/gadget/ecc/chip/add_incomplete.rs b/src/circuit/gadget/ecc/chip/add_incomplete.rs new file mode 100644 index 00000000..8877bba8 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs @@ -0,0 +1,198 @@ +use std::array; + +use super::{copy, CellValue, EccConfig, EccPoint, Var}; +use group::Curve; +use halo2::{ + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Permutation, Selector}, + poly::Rotation, +}; +use pasta_curves::{arithmetic::CurveAffine, pallas}; + +#[derive(Clone, Debug)] +pub struct Config { + q_add_incomplete: Selector, + // x-coordinate of P in P + Q = R + pub x_p: Column, + // y-coordinate of P in P + Q = R + pub y_p: Column, + // x-coordinate of Q or R in P + Q = R + pub x_qr: Column, + // y-coordinate of Q or R in P + Q = R + pub y_qr: Column, + // Permutation + perm: Permutation, +} + +impl From<&EccConfig> for Config { + fn from(ecc_config: &EccConfig) -> Self { + Self { + q_add_incomplete: ecc_config.q_add_incomplete, + x_p: ecc_config.advices[0], + y_p: ecc_config.advices[1], + x_qr: ecc_config.advices[2], + y_qr: ecc_config.advices[3], + perm: ecc_config.perm.clone(), + } + } +} + +impl Config { + pub(super) fn create_gate(&self, meta: &mut ConstraintSystem) { + meta.create_gate("incomplete addition gates", |meta| { + let q_add_incomplete = meta.query_selector(self.q_add_incomplete); + let x_p = meta.query_advice(self.x_p, Rotation::cur()); + let y_p = meta.query_advice(self.y_p, Rotation::cur()); + let x_q = meta.query_advice(self.x_qr, Rotation::cur()); + let y_q = meta.query_advice(self.y_qr, Rotation::cur()); + let x_r = meta.query_advice(self.x_qr, Rotation::next()); + let y_r = meta.query_advice(self.y_qr, Rotation::next()); + + // (x_r + x_q + x_p)β‹…(x_p βˆ’ x_q)^2 βˆ’ (y_p βˆ’ y_q)^2 = 0 + let poly1 = { + (x_r.clone() + x_q.clone() + x_p.clone()) + * (x_p.clone() - x_q.clone()) + * (x_p.clone() - x_q.clone()) + - (y_p.clone() - y_q.clone()).square() + }; + + // (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) + }); + } + + pub(super) fn assign_region( + &self, + p: &EccPoint, + q: &EccPoint, + offset: usize, + region: &mut Region<'_, pallas::Base>, + ) -> Result { + // Enable `q_add_incomplete` selector + self.q_add_incomplete.enable(region, offset)?; + + // Handle exceptional cases + let (x_p, y_p) = (p.x.value(), p.y.value()); + let (x_q, y_q) = (q.x.value(), q.y.value()); + x_p.zip(y_p) + .zip(x_q) + .zip(y_q) + .map(|(((x_p, y_p), x_q), y_q)| { + // P is point at infinity + if (x_p == pallas::Base::zero() && y_p == pallas::Base::zero()) + // Q is point at infinity + || (x_q == pallas::Base::zero() && y_q == pallas::Base::zero()) + // x_p = x_q + || (x_p == x_q) + { + Err(Error::SynthesisError) + } else { + Ok(()) + } + }) + .transpose()?; + + // Copy point `p` into `x_p`, `y_p` columns + copy(region, || "x_p", self.x_p, offset, &p.x, &self.perm)?; + copy(region, || "y_p", self.y_p, offset, &p.y, &self.perm)?; + + // Copy point `q` into `x_qr`, `y_qr` columns + copy(region, || "x_q", self.x_qr, offset, &q.x, &self.perm)?; + copy(region, || "y_q", self.y_qr, offset, &q.y, &self.perm)?; + + // Compute the sum `P + Q = R` + let r = { + let p = p.point(); + let q = q.point(); + let r = p + .zip(q) + .map(|(p, q)| (p + q).to_affine().coordinates().unwrap()); + let r_x = r.map(|r| *r.x()); + let r_y = r.map(|r| *r.y()); + + (r_x, r_y) + }; + + // Assign the sum to `x_qr`, `y_qr` columns in the next row + let x_r = r.0; + let x_r_var = region.assign_advice( + || "x_r", + self.x_qr, + offset + 1, + || x_r.ok_or(Error::SynthesisError), + )?; + + let y_r = r.1; + let y_r_var = region.assign_advice( + || "y_r", + self.y_qr, + offset + 1, + || y_r.ok_or(Error::SynthesisError), + )?; + + let result = EccPoint { + x: CellValue::::new(x_r_var, x_r), + y: CellValue::::new(y_r_var, y_r), + }; + + Ok(result) + } +} + +#[cfg(test)] +pub mod tests { + use group::Curve; + use halo2::{circuit::Layouter, plonk::Error}; + use pasta_curves::pallas; + + use crate::circuit::gadget::ecc::{EccInstructions, Point}; + + #[allow(clippy::too_many_arguments)] + pub fn test_add_incomplete< + EccChip: EccInstructions + Clone + Eq + std::fmt::Debug, + >( + chip: EccChip, + mut layouter: impl Layouter, + zero: &Point, + p_val: pallas::Affine, + p: &Point, + q_val: pallas::Affine, + q: &Point, + p_neg: &Point, + ) -> Result<(), Error> { + // P + Q + { + let result = p.add_incomplete(layouter.namespace(|| "P + Q"), q)?; + let witnessed_result = Point::new( + chip, + layouter.namespace(|| "witnessed P + Q"), + Some((p_val + q_val).to_affine()), + )?; + result.constrain_equal(layouter.namespace(|| "constrain P + Q"), &witnessed_result)?; + } + + // P + P should return an error + p.add_incomplete(layouter.namespace(|| "P + P"), p) + .expect_err("P + P should return an error"); + + // P + (-P) should return an error + p.add_incomplete(layouter.namespace(|| "P + (-P)"), p_neg) + .expect_err("P + (-P) should return an error"); + + // P + π’ͺ should return an error + p.add_incomplete(layouter.namespace(|| "P + π’ͺ"), zero) + .expect_err("P + 0 should return an error"); + + // π’ͺ + P should return an error + zero.add_incomplete(layouter.namespace(|| "π’ͺ + P"), p) + .expect_err("0 + P should return an error"); + + // π’ͺ + π’ͺ should return an error + zero.add_incomplete(layouter.namespace(|| "π’ͺ + π’ͺ"), zero) + .expect_err("π’ͺ + π’ͺ should return an error"); + + Ok(()) + } +} diff --git a/src/circuit/gadget/ecc/chip/witness_point.rs b/src/circuit/gadget/ecc/chip/witness_point.rs new file mode 100644 index 00000000..c9267963 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/witness_point.rs @@ -0,0 +1,96 @@ +use super::{CellValue, EccConfig, EccPoint, Var}; + +use group::prime::PrimeCurveAffine; + +use halo2::{ + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector}, + poly::Rotation, +}; +use pasta_curves::{arithmetic::CurveAffine, pallas}; + +#[derive(Clone, Debug)] +pub struct Config { + q_point: Selector, + // x-coordinate + pub x: Column, + // y-coordinate + pub y: Column, +} + +impl From<&EccConfig> for Config { + fn from(ecc_config: &EccConfig) -> Self { + Self { + q_point: ecc_config.q_point, + x: ecc_config.advices[0], + y: ecc_config.advices[1], + } + } +} + +impl Config { + pub(super) fn create_gate(&self, meta: &mut ConstraintSystem) { + meta.create_gate("witness point", |meta| { + // Check that either the point being witness is either: + // - the identity, which is mapped to (0, 0) in affine coordinates; or + // - a valid curve point y^2 = x^3 + b, where b = 5 in the Pallas equation + + let q_point = meta.query_selector(self.q_point); + let x = meta.query_advice(self.x, Rotation::cur()); + let y = meta.query_advice(self.y, Rotation::cur()); + + // y^2 = x^3 + b + let curve_eqn = y.clone().square() + - (x.clone().square() * x.clone()) + - Expression::Constant(pallas::Affine::b()); + + vec![ + q_point.clone() * x * curve_eqn.clone(), + q_point * y * curve_eqn, + ] + }); + } + + pub(super) fn assign_region( + &self, + value: Option, + offset: usize, + region: &mut Region<'_, pallas::Base>, + ) -> Result { + // Enable `q_point` selector + self.q_point.enable(region, offset)?; + + let value = value.map(|value| { + // Map the identity to (0, 0). + if value == pallas::Affine::identity() { + (pallas::Base::zero(), pallas::Base::zero()) + } else { + let value = value.coordinates().unwrap(); + (*value.x(), *value.y()) + } + }); + + // Assign `x` value + let x_val = value.map(|value| value.0); + let x_var = region.assign_advice( + || "x", + self.x, + offset, + || x_val.ok_or(Error::SynthesisError), + )?; + + // Assign `y` value + let y_val = value.map(|value| value.1); + let y_var = region.assign_advice( + || "y", + self.y, + offset, + || y_val.ok_or(Error::SynthesisError), + )?; + + Ok(EccPoint { + x: CellValue::::new(x_var, x_val), + y: CellValue::::new(y_var, y_val), + }) + } +}