diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs index 7f7337d3..09f8ed21 100644 --- a/src/circuit/gadget/ecc/chip.rs +++ b/src/circuit/gadget/ecc/chip.rs @@ -10,7 +10,7 @@ use halo2::{ }; use std::marker::PhantomData; -// pub(super) mod add; +pub(super) mod add; pub(super) mod add_incomplete; // pub(super) mod mul; // pub(super) mod mul_fixed; @@ -157,6 +157,12 @@ where config.create_gate(meta); } + // Create complete point addition gate + { + let add_config: add::Config = (&config).into(); + add_config.create_gate(meta); + } + config } } @@ -266,7 +272,11 @@ where a: &Self::Point, b: &Self::Point, ) -> Result { - todo!() + 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( diff --git a/src/circuit/gadget/ecc/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs new file mode 100644 index 00000000..00a875ab --- /dev/null +++ b/src/circuit/gadget/ecc/chip/add.rs @@ -0,0 +1,469 @@ +use std::array; + +use super::{copy, CellValue, EccConfig, EccPoint, Var}; +use ff::Field; +use halo2::{ + arithmetic::{CurveAffine, FieldExt}, + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector}, + poly::Rotation, +}; +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(F::one()); + let two = Expression::Constant(F::from_u64(2)); + let three = Expression::Constant(F::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() * x_p.clone(); // 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 poly3 = { + let x_q_minus_x_p = x_q.clone() - x_p.clone(); // (x_q - x_p) + let secant_line = + lambda.clone() * lambda.clone() - x_p.clone() - x_q.clone() - x_r.clone(); // (λ^2 - x_p - x_q - x_r) + + // 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 + }; + + // 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) + let output_line_x = + lambda.clone() * lambda.clone() - x_p.clone() - x_q.clone() - x_r.clone(); // (λ^2 - x_p - x_q - x_r) + + // 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 * output_line_x + }; + + // 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<'_, C::Base>, + ) -> Result, Error> { + // 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()); + + // Assign α = inv0(x_q - x_p) + let alpha = x_p.zip(x_q).map(|(x_p, x_q)| 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, + || { + let beta = x_p.map(inv0); + beta.ok_or(Error::SynthesisError) + }, + )?; + + // Assign γ = inv0(x_q) + region.assign_advice( + || "γ", + self.gamma, + offset, + || { + let gamma = x_q.map(inv0); + 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)?; + let y_p = y_p.ok_or(Error::SynthesisError)?; + let y_q = y_q.ok_or(Error::SynthesisError)?; + + let delta = if x_q == x_p { + inv0(y_q + y_p) + } else { + C::Base::zero() + }; + Ok(delta) + }, + )?; + + #[allow(clippy::collapsible_else_if)] + // Assign lambda + let lambda = x_p + .zip(y_p) + .zip(x_q) + .zip(y_q) + .map(|(((x_p, y_p), x_q), y_q)| { + 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.unwrap() + } else { + if y_p != C::Base::zero() { + // 3(x_p)^2 + let three_x_p_sq = C::Base::from_u64(3) * x_p * x_p; + // 2(y_p) + let two_y_p = C::Base::from_u64(2) * y_p; + // λ = 3(x_p)^2 / 2(y_p) + three_x_p_sq * two_y_p.invert().unwrap() + } else { + C::Base::zero() + } + } + }); + region.assign_advice( + || "λ", + self.lambda, + offset, + || lambda.ok_or(Error::SynthesisError), + )?; + + // Assign x_r + let x_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 == C::Base::zero() { + // 0 + Q = Q + x_q + } else if x_q == C::Base::zero() { + // P + 0 = P + x_p + } else if (x_q == x_p) && (y_q == -y_p) { + // P + (-P) maps to (0,0) + C::Base::zero() + } else { + // x_r = λ^2 - x_p - x_q + lambda * lambda - x_p - x_q + } + }); + 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 = x_p.zip(y_p).zip(x_q).zip(y_q).zip(x_r).zip(lambda).map( + |(((((x_p, y_p), x_q), y_q), x_r), lambda)| { + if x_p == C::Base::zero() { + // 0 + Q = Q + y_q + } else if x_q == C::Base::zero() { + // P + 0 = P + y_p + } else if (x_q == x_p) && (y_q == -y_p) { + // P + (-P) maps to (0,0) + C::Base::zero() + } else { + // y_r = λ(x_p - x_r) - y_p + lambda * (x_p - x_r) - y_p + } + }, + ); + 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) + } +} + +// inv0(x) is 0 if x = 0, 1/x otherwise. +fn inv0(x: F) -> F { + if x == F::zero() { + F::zero() + } else { + x.invert().unwrap() + } +} + +#[cfg(test)] +pub mod tests { + use group::Curve; + use halo2::{ + arithmetic::{CurveAffine, CurveExt}, + circuit::Layouter, + plonk::Error, + }; + + 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: C, + p: &Point, + q_val: C, + 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) + p.add(layouter.namespace(|| "P + (-P)"), &p_neg)?; + + // Check complete addition 𝒪 + 𝒪 + zero.add(layouter.namespace(|| "𝒪 + 𝒪"), &zero)?; + + // Check P + Q + p.add(layouter.namespace(|| "P + Q"), &q)?; + + // P + P + p.add(layouter.namespace(|| "P + P"), &p)?; + + // P + 𝒪 + p.add(layouter.namespace(|| "P + 𝒪"), &zero)?; + + // 𝒪 + P + zero.add(layouter.namespace(|| "𝒪 + 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(|| "point"), + 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(|| "point"), + 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(|| "point"), + Some(endo_2_p.to_affine()), + )?; + p.add(layouter.namespace(|| "P + endo(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(|| "point"), + Some(endo_2_p_neg.to_affine()), + )?; + p.add(layouter.namespace(|| "P + endo(P)"), &endo_2_p_neg)?; + + Ok(()) + } +}