From 7dc11b95d29a81e0847c9f471158a7a154e651b8 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Sat, 5 Jun 2021 14:11:40 +0800 Subject: [PATCH] chip::add_incomplete.rs: Implement add_incomplete() instruction --- src/circuit/gadget/ecc/chip.rs | 14 +- src/circuit/gadget/ecc/chip/add_incomplete.rs | 199 ++++++++++++++++++ 2 files changed, 211 insertions(+), 2 deletions(-) create mode 100644 src/circuit/gadget/ecc/chip/add_incomplete.rs diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs index a6f46136..7f7337d3 100644 --- a/src/circuit/gadget/ecc/chip.rs +++ b/src/circuit/gadget/ecc/chip.rs @@ -11,7 +11,7 @@ use halo2::{ use std::marker::PhantomData; // pub(super) mod add; -// pub(super) mod add_incomplete; +pub(super) mod add_incomplete; // pub(super) mod mul; // pub(super) mod mul_fixed; pub(super) mod witness_point; @@ -151,6 +151,12 @@ where config.create_gate::(meta); } + // Create incomplete point addition gate + { + let config: add_incomplete::Config = (&config).into(); + config.create_gate(meta); + } + config } } @@ -247,7 +253,11 @@ where a: &Self::Point, b: &Self::Point, ) -> Result { - todo!() + 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( 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..95414041 --- /dev/null +++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs @@ -0,0 +1,199 @@ +use std::array; + +use super::{copy, CellValue, EccConfig, EccPoint, Var}; +use ff::Field; +use group::Curve; +use halo2::{ + arithmetic::{CurveAffine, FieldExt}, + circuit::Region, + plonk::{Advice, Column, ConstraintSystem, Error, Permutation, Selector}, + poly::Rotation, +}; + +#[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()) * (y_p.clone() - y_q.clone()) + }; + + // (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<'_, C::Base>, + ) -> Result, Error> { + // 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 == C::Base::zero() && y_p == C::Base::zero()) + // Q is point at infinity + || (x_q == C::Base::zero() && y_q == C::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), + }; + + #[cfg(test)] + // Check that the correct sum is obtained. + { + 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 halo2::{arithmetic::CurveAffine, circuit::Layouter, plonk::Error}; + + use crate::circuit::gadget::ecc::{EccInstructions, Point}; + + pub fn test_add_incomplete< + C: CurveAffine, + EccChip: EccInstructions + Clone + Eq + std::fmt::Debug, + >( + mut layouter: impl Layouter, + zero: &Point, + p: &Point, + q: &Point, + p_neg: &Point, + ) -> Result<(), Error> { + // P + Q + p.add_incomplete(layouter.namespace(|| "P + Q"), &q)?; + + // 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(()) + } +}