From e15648cb67cc30b2c6fb6325d380ee1b10cf7676 Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 5 Jun 2021 13:59:48 +0800
Subject: [PATCH 01/17] gadget::ecc: Remove representations of fixed points in
 the circuit

Fixed points are represented by precomputed window tables. These
are not "initialized" in the circuit at any single point, but are
loaded into fixed columns at the offsets where the fixed points
are used.

Thus, we don't need FixedPoint and get_fixed() in the circuit.
Similarly, we can remove FixedPointShort and get_fixed_short().
---
 src/circuit/gadget/ecc.rs | 102 ++++++++++++++++++--------------------
 1 file changed, 49 insertions(+), 53 deletions(-)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index 31d252e3..07e6eff7 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -36,16 +36,10 @@ pub trait EccInstructions<C: CurveAffine>: Chip<C::Base> {
     /// 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;
 
     /// Witnesses the given base field element as a private input to the circuit
     /// for variable-base scalar mul.
@@ -81,18 +75,6 @@ pub trait EccInstructions<C: CurveAffine>: Chip<C::Base> {
     /// 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<Self::FixedPoint, Error>;
-
-    /// 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<Self::FixedPointShort, Error>;
-
     /// Performs incomplete point addition, returning `a + b`.
     ///
     /// This returns an error in exceptional cases.
@@ -111,14 +93,8 @@ pub trait EccInstructions<C: CurveAffine>: Chip<C::Base> {
         b: &Self::Point,
     ) -> Result<Self::Point, Error>;
 
-    /// Performs point doubling, returning `[2] a`.
-    fn double(
-        &self,
-        layouter: &mut impl Layouter<C::Base>,
-        a: &Self::Point,
-    ) -> Result<Self::Point, Error>;
-
     /// Performs variable-base scalar multiplication, returning `[scalar] base`.
+    /// Multiplication of the identity `[scalar] 𝒪 ` returns an error.
     fn mul(
         &self,
         layouter: &mut impl Layouter<C::Base>,
@@ -131,7 +107,7 @@ pub trait EccInstructions<C: CurveAffine>: Chip<C::Base> {
         &self,
         layouter: &mut impl Layouter<C::Base>,
         scalar: &Self::ScalarFixed,
-        base: &Self::FixedPoint,
+        base: &Self::FixedPoints,
     ) -> Result<Self::Point, Error>;
 
     /// Performs fixed-base scalar multiplication using a short signed scalar, returning `[scalar] base`.
@@ -139,7 +115,7 @@ pub trait EccInstructions<C: CurveAffine>: Chip<C::Base> {
         &self,
         layouter: &mut impl Layouter<C::Base>,
         scalar: &Self::ScalarFixedShort,
-        base: &Self::FixedPointShort,
+        base: &Self::FixedPointsShort,
     ) -> Result<Self::Point, Error>;
 }
 
@@ -174,12 +150,18 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + 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<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> {
+pub struct ScalarFixed<C: CurveAffine, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
+{
     chip: EccChip,
     inner: EccChip::ScalarFixed,
 }
 
-impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> ScalarFixed<C, EccChip> {
+impl<C: CurveAffine, EccChip> ScalarFixed<C, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
+{
     /// Constructs a new ScalarFixed with the given value.
     pub fn new(
         chip: EccChip,
@@ -193,13 +175,17 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + 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<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> {
+pub struct ScalarFixedShort<C: CurveAffine, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
+{
     chip: EccChip,
     inner: EccChip::ScalarFixedShort,
 }
 
-impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq>
-    ScalarFixedShort<C, EccChip>
+impl<C: CurveAffine, EccChip> ScalarFixedShort<C, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
 {
     /// Constructs a new ScalarFixedShort with the given value.
     ///
@@ -231,7 +217,7 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq>
 }
 
 /// An elliptic curve point over the given curve.
-#[derive(Debug)]
+#[derive(Copy, Clone, Debug)]
 pub struct Point<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> {
     chip: EccChip,
     inner: EccChip::Point,
@@ -318,18 +304,18 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> X<C, EccC
 /// A constant elliptic curve point over the given curve, for which window tables have
 /// been provided to make scalar multiplication more efficient.
 #[derive(Clone, Debug)]
-pub struct FixedPoint<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> {
+pub struct FixedPoint<C: CurveAffine, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
+{
     chip: EccChip,
-    inner: EccChip::FixedPoint,
+    inner: EccChip::FixedPoints,
 }
 
-impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> FixedPoint<C, EccChip> {
-    /// Gets a reference to the specified fixed point in the circuit.
-    pub fn get(chip: EccChip, point: EccChip::FixedPoints) -> Result<Self, Error> {
-        chip.get_fixed(point)
-            .map(|inner| FixedPoint { chip, inner })
-    }
-
+impl<C: CurveAffine, EccChip> FixedPoint<C, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
+{
     /// Returns `[by] self`.
     pub fn mul(
         &self,
@@ -344,23 +330,28 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + 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<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> {
+pub struct FixedPointShort<C: CurveAffine, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
+{
     chip: EccChip,
-    inner: EccChip::FixedPointShort,
+    inner: EccChip::FixedPointsShort,
 }
 
-impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> FixedPointShort<C, EccChip> {
-    /// Gets a reference to the specified fixed point in the circuit.
-    pub fn get(chip: EccChip, point: EccChip::FixedPointsShort) -> Result<Self, Error> {
-        chip.get_fixed_short(point)
-            .map(|inner| FixedPointShort { chip, inner })
-    }
-
+impl<C: CurveAffine, EccChip> FixedPointShort<C, EccChip>
+where
+    EccChip: EccInstructions<C> + Clone + Debug + Eq,
+{
     /// Returns `[by] self`.
     pub fn mul(
         &self,
@@ -375,4 +366,9 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + 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 }
+    }
 }

From 6627b2258f6c0df366c5b3dfd973d5993638070e Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 5 Jun 2021 14:05:58 +0800
Subject: [PATCH 02/17] ecc::chip.rs: Add ECC chip.

Implement witness_scalar_var() and extract_p() instructions inline.
---
 src/circuit/gadget/ecc.rs      |   2 +
 src/circuit/gadget/ecc/chip.rs | 280 +++++++++++++++++++++++++++++++++
 2 files changed, 282 insertions(+)
 create mode 100644 src/circuit/gadget/ecc/chip.rs

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index 07e6eff7..268e33c2 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<C: CurveAffine>: Chip<C::Base> {
     /// Variable representing an element of the elliptic curve's base field, that
diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs
new file mode 100644
index 00000000..12cef95e
--- /dev/null
+++ b/src/circuit/gadget/ecc/chip.rs
@@ -0,0 +1,280 @@
+use super::EccInstructions;
+use crate::circuit::gadget::utilities::{copy, CellValue, Var};
+use crate::constants::{self, OrchardFixedBasesFull, ValueCommitV};
+use arrayvec::ArrayVec;
+use ff::{Field, PrimeFieldBits};
+use halo2::{
+    arithmetic::CurveAffine,
+    circuit::{Chip, Layouter},
+    plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation, Selector},
+};
+use std::marker::PhantomData;
+
+// 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<C: CurveAffine> {
+    /// x-coordinate
+    pub x: CellValue<C::Base>,
+    /// y-coordinate
+    pub y: CellValue<C::Base>,
+}
+
+impl<C: CurveAffine> EccPoint<C> {
+    /// Returns the value of this curve point, if known.
+    pub fn point(&self) -> Option<C> {
+        match (self.x.value(), self.y.value()) {
+            (Some(x), Some(y)) => {
+                if x == C::Base::zero() && y == C::Base::zero() {
+                    Some(C::identity())
+                } else {
+                    Some(C::from_xy(x, y).unwrap())
+                }
+            }
+            _ => None,
+        }
+    }
+}
+
+/// 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<Advice>; 10],
+
+    /// Coefficients of interpolation polynomials for x-coordinates (used in fixed-base scalar multiplication)
+    pub lagrange_coeffs: [Column<Fixed>; 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<Fixed>,
+
+    /// 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<C: CurveAffine> {
+    config: EccConfig,
+    _marker: PhantomData<C>,
+}
+
+impl<C: CurveAffine> Chip<C::Base> for EccChip<C> {
+    type Config = EccConfig;
+    type Loaded = ();
+
+    fn config(&self) -> &Self::Config {
+        &self.config
+    }
+
+    fn loaded(&self) -> &Self::Loaded {
+        &()
+    }
+}
+
+impl<C: CurveAffine> EccChip<C>
+where
+    C::Scalar: PrimeFieldBits,
+{
+    pub fn construct(config: <Self as Chip<C::Base>>::Config) -> Self {
+        Self {
+            config,
+            _marker: PhantomData,
+        }
+    }
+
+    #[allow(non_snake_case)]
+    pub fn configure(
+        meta: &mut ConstraintSystem<C::Base>,
+        advices: [Column<Advice>; 10],
+        perm: Permutation,
+    ) -> <Self as Chip<C::Base>>::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,
+        };
+
+        // TODO: create gates
+
+        config
+    }
+}
+
+/// A full-width scalar used for fixed-base scalar multiplication.
+/// This is decomposed in chunks of `window_width` bits in little-endian order.
+/// For example, if `window_width` = 3, we will have [k_0, k_1, ..., k_n]
+/// where `scalar = k_0 + k_1 * (2^3) + ... + k_n * (2^3)^n` and each `k_i` is
+/// in the range [0..2^3).
+#[derive(Clone, Debug)]
+pub struct EccScalarFixed<C: CurveAffine> {
+    value: Option<C::Scalar>,
+    windows: ArrayVec<CellValue<C::Base>, { constants::NUM_WINDOWS }>,
+}
+
+/// A signed short scalar used for fixed-base scalar multiplication.
+/// This is decomposed in chunks of `window_width` bits in little-endian order.
+/// For example, if `window_width` = 3, we will have [k_0, k_1, ..., k_n]
+/// where `scalar = k_0 + k_1 * (2^3) + ... + k_n * (2^3)^n` and each `k_i` is
+/// in the range [0..2^3).
+#[derive(Clone, Debug)]
+pub struct EccScalarFixedShort<C: CurveAffine> {
+    magnitude: Option<C::Scalar>,
+    sign: CellValue<C::Base>,
+    windows: ArrayVec<CellValue<C::Base>, { constants::NUM_WINDOWS_SHORT }>,
+}
+
+impl<C: CurveAffine> EccInstructions<C> for EccChip<C>
+where
+    C::Scalar: PrimeFieldBits,
+{
+    type ScalarFixed = EccScalarFixed<C>;
+    type ScalarFixedShort = EccScalarFixedShort<C>;
+    type ScalarVar = CellValue<C::Base>;
+    type Point = EccPoint<C>;
+    type X = CellValue<C::Base>;
+    type FixedPoints = OrchardFixedBasesFull<C>;
+    type FixedPointsShort = ValueCommitV<C>;
+
+    fn witness_scalar_var(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        value: Option<C::Base>,
+    ) -> Result<Self::ScalarVar, Error> {
+        layouter.assign_region(
+            || "Witness scalar for variable-base mul",
+            |mut region| {
+                let cell = region.assign_advice(
+                    || "Scalar var",
+                    self.config().advices[0],
+                    0,
+                    || value.ok_or(Error::SynthesisError),
+                )?;
+                Ok(CellValue::new(cell, value))
+            },
+        )
+    }
+
+    fn witness_scalar_fixed(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        value: Option<C::Scalar>,
+    ) -> Result<Self::ScalarFixed, Error> {
+        todo!()
+    }
+
+    fn witness_scalar_fixed_short(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        value: Option<C::Scalar>,
+    ) -> Result<Self::ScalarFixedShort, Error> {
+        todo!()
+    }
+
+    fn witness_point(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        value: Option<C>,
+    ) -> Result<Self::Point, Error> {
+        todo!()
+    }
+
+    fn extract_p(point: &Self::Point) -> &Self::X {
+        &point.x
+    }
+
+    fn add_incomplete(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        a: &Self::Point,
+        b: &Self::Point,
+    ) -> Result<Self::Point, Error> {
+        todo!()
+    }
+
+    fn add(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        a: &Self::Point,
+        b: &Self::Point,
+    ) -> Result<Self::Point, Error> {
+        todo!()
+    }
+
+    fn mul(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        scalar: &Self::ScalarVar,
+        base: &Self::Point,
+    ) -> Result<Self::Point, Error> {
+        todo!()
+    }
+
+    fn mul_fixed(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        scalar: &Self::ScalarFixed,
+        base: &Self::FixedPoints,
+    ) -> Result<Self::Point, Error> {
+        todo!()
+    }
+
+    fn mul_fixed_short(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        scalar: &Self::ScalarFixedShort,
+        base: &Self::FixedPointsShort,
+    ) -> Result<Self::Point, Error> {
+        todo!()
+    }
+}

From 7eb86eb0c2c0970eed26d2a1d5dc05115f95e50d Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 5 Jun 2021 14:08:51 +0800
Subject: [PATCH 03/17] chip::witness_point.rs: Implement witness_point()
 instruction.

---
 src/circuit/gadget/ecc/chip.rs               | 14 +++-
 src/circuit/gadget/ecc/chip/witness_point.rs | 78 ++++++++++++++++++++
 2 files changed, 89 insertions(+), 3 deletions(-)
 create mode 100644 src/circuit/gadget/ecc/chip/witness_point.rs

diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs
index 12cef95e..a6f46136 100644
--- a/src/circuit/gadget/ecc/chip.rs
+++ b/src/circuit/gadget/ecc/chip.rs
@@ -14,7 +14,7 @@ use std::marker::PhantomData;
 // pub(super) mod add_incomplete;
 // pub(super) mod mul;
 // pub(super) mod mul_fixed;
-// pub(super) mod witness_point;
+pub(super) mod witness_point;
 // pub(super) mod witness_scalar_fixed;
 
 /// A curve point represented in affine (x, y) coordinates. Each coordinate is
@@ -145,7 +145,11 @@ where
             perm,
         };
 
-        // TODO: create gates
+        // Create witness point gate
+        {
+            let config: witness_point::Config = (&config).into();
+            config.create_gate::<C>(meta);
+        }
 
         config
     }
@@ -226,7 +230,11 @@ where
         layouter: &mut impl Layouter<C::Base>,
         value: Option<C>,
     ) -> Result<Self::Point, Error> {
-        todo!()
+        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 {
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..9b4d8888
--- /dev/null
+++ b/src/circuit/gadget/ecc/chip/witness_point.rs
@@ -0,0 +1,78 @@
+use super::{CellValue, EccConfig, EccPoint, Var};
+
+use halo2::{
+    arithmetic::CurveAffine,
+    circuit::Region,
+    plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
+    poly::Rotation,
+};
+
+#[derive(Clone, Debug)]
+pub struct Config {
+    q_point: Selector,
+    // x-coordinate
+    pub x: Column<Advice>,
+    // y-coordinate
+    pub y: Column<Advice>,
+}
+
+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<C: CurveAffine>(&self, meta: &mut ConstraintSystem<C::Base>) {
+        meta.create_gate("witness point", |meta| {
+            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());
+
+            // Check that y^2 = x^3 + b, where b = 5 in the Pallas equation
+            vec![
+                q_point
+                    * (y.clone() * y - (x.clone() * x.clone() * x) - Expression::Constant(C::b())),
+            ]
+        });
+    }
+
+    pub(super) fn assign_region<C: CurveAffine>(
+        &self,
+        value: Option<C>,
+        offset: usize,
+        region: &mut Region<'_, C::Base>,
+    ) -> Result<EccPoint<C>, Error> {
+        // Enable `q_point` selector
+        self.q_point.enable(region, offset)?;
+
+        let value = value.map(|value| value.coordinates().unwrap());
+
+        // Assign `x` value
+        let x_val = value.map(|value| *value.x());
+        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.y());
+        let y_var = region.assign_advice(
+            || "y",
+            self.y,
+            offset,
+            || y_val.ok_or(Error::SynthesisError),
+        )?;
+
+        Ok(EccPoint {
+            x: CellValue::<C::Base>::new(x_var, x_val),
+            y: CellValue::<C::Base>::new(y_var, y_val),
+        })
+    }
+}

From 7dc11b95d29a81e0847c9f471158a7a154e651b8 Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 5 Jun 2021 14:11:40 +0800
Subject: [PATCH 04/17] 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::<C>(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<Self::Point, Error> {
-        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<Advice>,
+    // y-coordinate of P in P + Q = R
+    pub y_p: Column<Advice>,
+    // x-coordinate of Q or R in P + Q = R
+    pub x_qr: Column<Advice>,
+    // y-coordinate of Q or R in P + Q = R
+    pub y_qr: Column<Advice>,
+    // 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<F: FieldExt>(&self, meta: &mut ConstraintSystem<F>) {
+        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<C: CurveAffine>(
+        &self,
+        p: &EccPoint<C>,
+        q: &EccPoint<C>,
+        offset: usize,
+        region: &mut Region<'_, C::Base>,
+    ) -> Result<EccPoint<C>, 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::<C> {
+            x: CellValue::<C::Base>::new(x_r_var, x_r),
+            y: CellValue::<C::Base>::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<C> + Clone + Eq + std::fmt::Debug,
+    >(
+        mut layouter: impl Layouter<C::Base>,
+        zero: &Point<C, EccChip>,
+        p: &Point<C, EccChip>,
+        q: &Point<C, EccChip>,
+        p_neg: &Point<C, EccChip>,
+    ) -> 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(())
+    }
+}

From e802e2917ae3e05ac703e6912b3569d65eec09ea Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 5 Jun 2021 14:13:56 +0800
Subject: [PATCH 05/17] chip::add.rs: Implement complete addition instruction.

---
 src/circuit/gadget/ecc/chip.rs     |  14 +-
 src/circuit/gadget/ecc/chip/add.rs | 469 +++++++++++++++++++++++++++++
 2 files changed, 481 insertions(+), 2 deletions(-)
 create mode 100644 src/circuit/gadget/ecc/chip/add.rs

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<Self::Point, Error> {
-        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<Advice>,
+    // x-coordinate of P in P + Q = R
+    pub x_p: Column<Advice>,
+    // y-coordinate of P in P + Q = R
+    pub y_p: Column<Advice>,
+    // x-coordinate of Q or R in P + Q = R
+    pub x_qr: Column<Advice>,
+    // y-coordinate of Q or R in P + Q = R
+    pub y_qr: Column<Advice>,
+    // α = inv0(x_q - x_p)
+    alpha: Column<Advice>,
+    // β = inv0(x_p)
+    beta: Column<Advice>,
+    // γ = inv0(x_q)
+    gamma: Column<Advice>,
+    // δ = inv0(y_p + y_q) if x_q = x_p, 0 otherwise
+    delta: Column<Advice>,
+    // 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<Column<Advice>> {
+        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<F: FieldExt>(&self, meta: &mut ConstraintSystem<F>) {
+        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<C: CurveAffine>(
+        &self,
+        p: &EccPoint<C>,
+        q: &EccPoint<C>,
+        offset: usize,
+        region: &mut Region<'_, C::Base>,
+    ) -> Result<EccPoint<C>, 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::<C> {
+            x: CellValue::<C::Base>::new(x_r_cell, x_r),
+            y: CellValue::<C::Base>::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<F: FieldExt>(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<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Eq + std::fmt::Debug>(
+        chip: EccChip,
+        mut layouter: impl Layouter<C::Base>,
+        zero: &Point<C, EccChip>,
+        p_val: C,
+        p: &Point<C, EccChip>,
+        q_val: C,
+        q: &Point<C, EccChip>,
+        p_neg: &Point<C, EccChip>,
+    ) -> 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(())
+    }
+}

From 6491ea90ddd8e3dd9be77b7f5859b0517db602fc Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Fri, 11 Jun 2021 01:09:04 +0800
Subject: [PATCH 06/17] ecc::chip.rs: Bound EccConfig on <C: CurveAffine>.

---
 src/circuit/gadget/ecc/chip.rs                | 73 ++++++++-----------
 src/circuit/gadget/ecc/chip/add.rs            | 22 +++---
 src/circuit/gadget/ecc/chip/add_incomplete.rs | 18 +++--
 src/circuit/gadget/ecc/chip/witness_point.rs  | 16 ++--
 4 files changed, 62 insertions(+), 67 deletions(-)

diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs
index 09f8ed21..c7d702ea 100644
--- a/src/circuit/gadget/ecc/chip.rs
+++ b/src/circuit/gadget/ecc/chip.rs
@@ -46,7 +46,7 @@ impl<C: CurveAffine> EccPoint<C> {
 /// Configuration for the ECC chip
 #[derive(Clone, Debug, Eq, PartialEq)]
 #[allow(non_snake_case)]
-pub struct EccConfig {
+pub struct EccConfig<C: CurveAffine> {
     /// Advice columns needed by instructions in the ECC chip.
     pub advices: [Column<Advice>; 10],
 
@@ -79,17 +79,17 @@ pub struct EccConfig {
     pub q_scalar_fixed_short: Selector,
     /// Permutation
     pub perm: Permutation,
+    _marker: PhantomData<C>,
 }
 
 /// A chip implementing EccInstructions
 #[derive(Clone, Debug, Eq, PartialEq)]
 pub struct EccChip<C: CurveAffine> {
-    config: EccConfig,
-    _marker: PhantomData<C>,
+    config: EccConfig<C>,
 }
 
 impl<C: CurveAffine> Chip<C::Base> for EccChip<C> {
-    type Config = EccConfig;
+    type Config = EccConfig<C>;
     type Loaded = ();
 
     fn config(&self) -> &Self::Config {
@@ -106,10 +106,7 @@ where
     C::Scalar: PrimeFieldBits,
 {
     pub fn construct(config: <Self as Chip<C::Base>>::Config) -> Self {
-        Self {
-            config,
-            _marker: PhantomData,
-        }
+        Self { config }
     }
 
     #[allow(non_snake_case)]
@@ -118,7 +115,7 @@ where
         advices: [Column<Advice>; 10],
         perm: Permutation,
     ) -> <Self as Chip<C::Base>>::Config {
-        let config = EccConfig {
+        let config = EccConfig::<C> {
             advices,
             lagrange_coeffs: [
                 meta.fixed_column(),
@@ -143,23 +140,24 @@ where
             q_scalar_fixed: meta.selector(),
             q_scalar_fixed_short: meta.selector(),
             perm,
+            _marker: PhantomData,
         };
 
         // Create witness point gate
         {
-            let config: witness_point::Config = (&config).into();
-            config.create_gate::<C>(meta);
+            let config: witness_point::Config<C> = (&config).into();
+            config.create_gate(meta);
         }
 
         // Create incomplete point addition gate
         {
-            let config: add_incomplete::Config = (&config).into();
+            let config: add_incomplete::Config<C> = (&config).into();
             config.create_gate(meta);
         }
 
         // Create complete point addition gate
         {
-            let add_config: add::Config = (&config).into();
+            let add_config: add::Config<C> = (&config).into();
             add_config.create_gate(meta);
         }
 
@@ -204,35 +202,24 @@ where
 
     fn witness_scalar_var(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
-        value: Option<C::Base>,
+        _layouter: &mut impl Layouter<C::Base>,
+        _value: Option<C::Base>,
     ) -> Result<Self::ScalarVar, Error> {
-        layouter.assign_region(
-            || "Witness scalar for variable-base mul",
-            |mut region| {
-                let cell = region.assign_advice(
-                    || "Scalar var",
-                    self.config().advices[0],
-                    0,
-                    || value.ok_or(Error::SynthesisError),
-                )?;
-                Ok(CellValue::new(cell, value))
-            },
-        )
+        todo!()
     }
 
     fn witness_scalar_fixed(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
-        value: Option<C::Scalar>,
+        _layouter: &mut impl Layouter<C::Base>,
+        _value: Option<C::Scalar>,
     ) -> Result<Self::ScalarFixed, Error> {
         todo!()
     }
 
     fn witness_scalar_fixed_short(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
-        value: Option<C::Scalar>,
+        _layouter: &mut impl Layouter<C::Base>,
+        _value: Option<C::Scalar>,
     ) -> Result<Self::ScalarFixedShort, Error> {
         todo!()
     }
@@ -242,7 +229,7 @@ where
         layouter: &mut impl Layouter<C::Base>,
         value: Option<C>,
     ) -> Result<Self::Point, Error> {
-        let config: witness_point::Config = self.config().into();
+        let config: witness_point::Config<C> = self.config().into();
         layouter.assign_region(
             || "witness point",
             |mut region| config.assign_region(value, 0, &mut region),
@@ -259,7 +246,7 @@ where
         a: &Self::Point,
         b: &Self::Point,
     ) -> Result<Self::Point, Error> {
-        let config: add_incomplete::Config = self.config().into();
+        let config: add_incomplete::Config<C> = self.config().into();
         layouter.assign_region(
             || "incomplete point addition",
             |mut region| config.assign_region(a, b, 0, &mut region),
@@ -272,7 +259,7 @@ where
         a: &Self::Point,
         b: &Self::Point,
     ) -> Result<Self::Point, Error> {
-        let config: add::Config = self.config().into();
+        let config: add::Config<C> = self.config().into();
         layouter.assign_region(
             || "complete point addition",
             |mut region| config.assign_region(a, b, 0, &mut region),
@@ -281,27 +268,27 @@ where
 
     fn mul(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
-        scalar: &Self::ScalarVar,
-        base: &Self::Point,
+        _layouter: &mut impl Layouter<C::Base>,
+        _scalar: &Self::ScalarVar,
+        _base: &Self::Point,
     ) -> Result<Self::Point, Error> {
         todo!()
     }
 
     fn mul_fixed(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
-        scalar: &Self::ScalarFixed,
-        base: &Self::FixedPoints,
+        _layouter: &mut impl Layouter<C::Base>,
+        _scalar: &Self::ScalarFixed,
+        _base: &Self::FixedPoints,
     ) -> Result<Self::Point, Error> {
         todo!()
     }
 
     fn mul_fixed_short(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
-        scalar: &Self::ScalarFixedShort,
-        base: &Self::FixedPointsShort,
+        _layouter: &mut impl Layouter<C::Base>,
+        _scalar: &Self::ScalarFixedShort,
+        _base: &Self::FixedPointsShort,
     ) -> Result<Self::Point, Error> {
         todo!()
     }
diff --git a/src/circuit/gadget/ecc/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs
index 00a875ab..f27ac9dc 100644
--- a/src/circuit/gadget/ecc/chip/add.rs
+++ b/src/circuit/gadget/ecc/chip/add.rs
@@ -8,10 +8,10 @@ use halo2::{
     plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
     poly::Rotation,
 };
-use std::collections::HashSet;
+use std::{collections::HashSet, marker::PhantomData};
 
 #[derive(Clone, Debug)]
-pub struct Config {
+pub struct Config<C: CurveAffine> {
     q_add: Selector,
     // lambda
     lambda: Column<Advice>,
@@ -33,10 +33,11 @@ pub struct Config {
     delta: Column<Advice>,
     // Permutation
     perm: Permutation,
+    _marker: PhantomData<C>,
 }
 
-impl From<&EccConfig> for Config {
-    fn from(ecc_config: &EccConfig) -> Self {
+impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
+    fn from(ecc_config: &EccConfig<C>) -> Self {
         Self {
             q_add: ecc_config.q_add,
             x_p: ecc_config.advices[0],
@@ -49,11 +50,12 @@ impl From<&EccConfig> for Config {
             gamma: ecc_config.advices[7],
             delta: ecc_config.advices[8],
             perm: ecc_config.perm.clone(),
+            _marker: PhantomData,
         }
     }
 }
 
-impl Config {
+impl<C: CurveAffine> Config<C> {
     pub(crate) fn advice_columns(&self) -> HashSet<Column<Advice>> {
         core::array::IntoIter::new([
             self.x_p,
@@ -69,7 +71,7 @@ impl Config {
         .collect()
     }
 
-    pub(crate) fn create_gate<F: FieldExt>(&self, meta: &mut ConstraintSystem<F>) {
+    pub(crate) fn create_gate(&self, meta: &mut ConstraintSystem<C::Base>) {
         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());
@@ -100,9 +102,9 @@ impl Config {
             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));
+            let one = Expression::Constant(C::Base::one());
+            let two = Expression::Constant(C::Base::from_u64(2));
+            let three = Expression::Constant(C::Base::from_u64(3));
 
             // (x_q − x_p)⋅((x_q − x_p)⋅λ − (y_q−y_p)) = 0
             let poly1 = {
@@ -195,7 +197,7 @@ impl Config {
         });
     }
 
-    pub(super) fn assign_region<C: CurveAffine>(
+    pub(super) fn assign_region(
         &self,
         p: &EccPoint<C>,
         q: &EccPoint<C>,
diff --git a/src/circuit/gadget/ecc/chip/add_incomplete.rs b/src/circuit/gadget/ecc/chip/add_incomplete.rs
index 95414041..b1b5b0c1 100644
--- a/src/circuit/gadget/ecc/chip/add_incomplete.rs
+++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs
@@ -1,17 +1,17 @@
-use std::array;
+use std::{array, marker::PhantomData};
 
 use super::{copy, CellValue, EccConfig, EccPoint, Var};
 use ff::Field;
 use group::Curve;
 use halo2::{
-    arithmetic::{CurveAffine, FieldExt},
+    arithmetic::CurveAffine,
     circuit::Region,
     plonk::{Advice, Column, ConstraintSystem, Error, Permutation, Selector},
     poly::Rotation,
 };
 
 #[derive(Clone, Debug)]
-pub struct Config {
+pub struct Config<C: CurveAffine> {
     q_add_incomplete: Selector,
     // x-coordinate of P in P + Q = R
     pub x_p: Column<Advice>,
@@ -23,10 +23,11 @@ pub struct Config {
     pub y_qr: Column<Advice>,
     // Permutation
     perm: Permutation,
+    _marker: PhantomData<C>,
 }
 
-impl From<&EccConfig> for Config {
-    fn from(ecc_config: &EccConfig) -> Self {
+impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
+    fn from(ecc_config: &EccConfig<C>) -> Self {
         Self {
             q_add_incomplete: ecc_config.q_add_incomplete,
             x_p: ecc_config.advices[0],
@@ -34,12 +35,13 @@ impl From<&EccConfig> for Config {
             x_qr: ecc_config.advices[2],
             y_qr: ecc_config.advices[3],
             perm: ecc_config.perm.clone(),
+            _marker: PhantomData,
         }
     }
 }
 
-impl Config {
-    pub(super) fn create_gate<F: FieldExt>(&self, meta: &mut ConstraintSystem<F>) {
+impl<C: CurveAffine> Config<C> {
+    pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<C::Base>) {
         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());
@@ -64,7 +66,7 @@ impl Config {
         });
     }
 
-    pub(super) fn assign_region<C: CurveAffine>(
+    pub(super) fn assign_region(
         &self,
         p: &EccPoint<C>,
         q: &EccPoint<C>,
diff --git a/src/circuit/gadget/ecc/chip/witness_point.rs b/src/circuit/gadget/ecc/chip/witness_point.rs
index 9b4d8888..1d1377b0 100644
--- a/src/circuit/gadget/ecc/chip/witness_point.rs
+++ b/src/circuit/gadget/ecc/chip/witness_point.rs
@@ -7,27 +7,31 @@ use halo2::{
     poly::Rotation,
 };
 
+use std::marker::PhantomData;
+
 #[derive(Clone, Debug)]
-pub struct Config {
+pub struct Config<C: CurveAffine> {
     q_point: Selector,
     // x-coordinate
     pub x: Column<Advice>,
     // y-coordinate
     pub y: Column<Advice>,
+    _marker: PhantomData<C>,
 }
 
-impl From<&EccConfig> for Config {
-    fn from(ecc_config: &EccConfig) -> Self {
+impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
+    fn from(ecc_config: &EccConfig<C>) -> Self {
         Self {
             q_point: ecc_config.q_point,
             x: ecc_config.advices[0],
             y: ecc_config.advices[1],
+            _marker: PhantomData,
         }
     }
 }
 
-impl Config {
-    pub(super) fn create_gate<C: CurveAffine>(&self, meta: &mut ConstraintSystem<C::Base>) {
+impl<C: CurveAffine> Config<C> {
+    pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<C::Base>) {
         meta.create_gate("witness point", |meta| {
             let q_point = meta.query_selector(self.q_point);
             let x = meta.query_advice(self.x, Rotation::cur());
@@ -41,7 +45,7 @@ impl Config {
         });
     }
 
-    pub(super) fn assign_region<C: CurveAffine>(
+    pub(super) fn assign_region(
         &self,
         value: Option<C>,
         offset: usize,

From 36d7888c1c957a6a5767e58388d033b5b042587a Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Fri, 11 Jun 2021 01:07:56 +0800
Subject: [PATCH 07/17] ecc.rs: Add tests for complete and incomplete addition.

---
 src/circuit/gadget/ecc.rs | 114 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 114 insertions(+)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index 268e33c2..7c41f579 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -374,3 +374,117 @@ where
         FixedPointShort { chip, inner }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use ff::PrimeFieldBits;
+    use group::{Curve, Group};
+    use halo2::{
+        arithmetic::CurveAffine,
+        circuit::{layouter::SingleChipLayouter, Layouter},
+        dev::MockProver,
+        pasta::pallas,
+        plonk::{Assignment, Circuit, ConstraintSystem, Error},
+    };
+
+    use super::chip::{EccChip, EccConfig};
+
+    struct MyCircuit<C: CurveAffine> {
+        _marker: std::marker::PhantomData<C>,
+    }
+
+    #[allow(non_snake_case)]
+    impl<C: CurveAffine> Circuit<C::Base> for MyCircuit<C>
+    where
+        C::Scalar: PrimeFieldBits,
+    {
+        type Config = EccConfig<C>;
+
+        fn configure(meta: &mut ConstraintSystem<C::Base>) -> 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::<Vec<_>>(),
+            );
+
+            EccChip::<C>::configure(meta, advices, perm)
+        }
+
+        fn synthesize(
+            &self,
+            cs: &mut impl Assignment<C::Base>,
+            config: Self::Config,
+        ) -> Result<(), Error> {
+            let mut layouter = SingleChipLayouter::new(cs)?;
+            let chip = EccChip::construct(config);
+
+            // Generate a random point P
+            let p_val = C::CurveExt::random(rand::rngs::OsRng).to_affine(); // P
+            let p = super::Point::new(chip.clone(), layouter.namespace(|| "point"), Some(p_val))?;
+            let p_neg = -p_val;
+            let p_neg =
+                super::Point::new(chip.clone(), layouter.namespace(|| "point"), Some(p_neg))?;
+
+            // Generate a random point Q
+            let q_val = C::CurveExt::random(rand::rngs::OsRng).to_affine(); // P
+            let q = super::Point::new(chip.clone(), layouter.namespace(|| "point"), 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 = p.add(layouter.namespace(|| "P + (-P)"), &p_neg)?;
+
+            // 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(
+                    layouter.namespace(|| "incomplete addition"),
+                    &zero,
+                    &p,
+                    &q,
+                    &p_neg,
+                )?;
+            }
+
+            Ok(())
+        }
+    }
+
+    #[test]
+    fn ecc() {
+        let k = 5;
+        let circuit = MyCircuit::<pallas::Affine> {
+            _marker: std::marker::PhantomData,
+        };
+        let prover = MockProver::run(k, &circuit, vec![]).unwrap();
+        assert_eq!(prover.verify(), Ok(()))
+    }
+}

From 433791fcb02d5fb81549063d7e1165808275da4d Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Fri, 11 Jun 2021 11:18:52 +0800
Subject: [PATCH 08/17] chip::witness_point.rs: Allow witnessing the identity.

---
 src/circuit/gadget/ecc.rs                    |  9 +++++-
 src/circuit/gadget/ecc/chip/witness_point.rs | 29 ++++++++++++++++----
 2 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index 7c41f579..23efe03f 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -68,6 +68,7 @@ pub trait EccInstructions<C: CurveAffine>: Chip<C::Base> {
     ) -> Result<Self::ScalarFixedShort, Error>;
 
     /// 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<C::Base>,
@@ -447,7 +448,13 @@ mod tests {
             assert_ne!(p_val, q_val);
 
             // Generate a (0,0) point to be used in other tests.
-            let zero = p.add(layouter.namespace(|| "P + (-P)"), &p_neg)?;
+            let zero = {
+                super::Point::new(
+                    chip.clone(),
+                    layouter.namespace(|| "identity"),
+                    Some(C::identity()),
+                )?
+            };
 
             // Test complete addition
             {
diff --git a/src/circuit/gadget/ecc/chip/witness_point.rs b/src/circuit/gadget/ecc/chip/witness_point.rs
index 1d1377b0..c582e9cd 100644
--- a/src/circuit/gadget/ecc/chip/witness_point.rs
+++ b/src/circuit/gadget/ecc/chip/witness_point.rs
@@ -1,5 +1,6 @@
 use super::{CellValue, EccConfig, EccPoint, Var};
 
+use ff::Field;
 use halo2::{
     arithmetic::CurveAffine,
     circuit::Region,
@@ -33,14 +34,22 @@ impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
 impl<C: CurveAffine> Config<C> {
     pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<C::Base>) {
         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());
 
-            // Check that y^2 = x^3 + b, where b = 5 in the Pallas equation
+            // y^2 = x^3 + b
+            let curve_eqn = y.clone() * y.clone()
+                - (x.clone() * x.clone() * x.clone())
+                - Expression::Constant(C::b());
+
             vec![
-                q_point
-                    * (y.clone() * y - (x.clone() * x.clone() * x) - Expression::Constant(C::b())),
+                q_point.clone() * x * curve_eqn.clone(),
+                q_point * y * curve_eqn,
             ]
         });
     }
@@ -54,10 +63,18 @@ impl<C: CurveAffine> Config<C> {
         // Enable `q_point` selector
         self.q_point.enable(region, offset)?;
 
-        let value = value.map(|value| value.coordinates().unwrap());
+        let value = value.map(|value| {
+            // Map the identity to (0, 0).
+            if value == C::identity() {
+                (C::Base::zero(), C::Base::zero())
+            } else {
+                let value = value.coordinates().unwrap();
+                (*value.x(), *value.y())
+            }
+        });
 
         // Assign `x` value
-        let x_val = value.map(|value| *value.x());
+        let x_val = value.map(|value| value.0);
         let x_var = region.assign_advice(
             || "x",
             self.x,
@@ -66,7 +83,7 @@ impl<C: CurveAffine> Config<C> {
         )?;
 
         // Assign `y` value
-        let y_val = value.map(|value| *value.y());
+        let y_val = value.map(|value| value.1);
         let y_var = region.assign_advice(
             || "y",
             self.y,

From aff56e67639094a3c15fe5e1e5515cceba8fe68a Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Fri, 11 Jun 2021 11:24:12 +0800
Subject: [PATCH 09/17] ecc::chip.rs: Make EccPoint.x, EccPoint.y private
 fields

Also add public getters x() and y().

Co-authored-by: Jack Grigg <jack@electriccoin.co>
Co-authored-by: Daira Hopwood <daira@jacaranda.org>
---
 src/circuit/gadget/ecc.rs      |  2 +-
 src/circuit/gadget/ecc/chip.rs | 14 ++++++++++++--
 2 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index 23efe03f..d20ac5c2 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -459,7 +459,7 @@ mod tests {
             // Test complete addition
             {
                 super::chip::add::tests::test_add(
-                    chip.clone(),
+                    chip,
                     layouter.namespace(|| "complete addition"),
                     &zero,
                     p_val,
diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs
index c7d702ea..5d95a272 100644
--- a/src/circuit/gadget/ecc/chip.rs
+++ b/src/circuit/gadget/ecc/chip.rs
@@ -22,9 +22,9 @@ pub(super) mod witness_point;
 #[derive(Clone, Debug)]
 pub struct EccPoint<C: CurveAffine> {
     /// x-coordinate
-    pub x: CellValue<C::Base>,
+    x: CellValue<C::Base>,
     /// y-coordinate
-    pub y: CellValue<C::Base>,
+    y: CellValue<C::Base>,
 }
 
 impl<C: CurveAffine> EccPoint<C> {
@@ -41,6 +41,16 @@ impl<C: CurveAffine> EccPoint<C> {
             _ => None,
         }
     }
+    /// The cell containing the affine short-Weierstrass x-coordinate,
+    /// or 0 for the zero point.
+    pub fn x(&self) -> CellValue<C::Base> {
+        self.x
+    }
+    /// The cell containing the affine short-Weierstrass y-coordinate,
+    /// or 0 for the zero point.
+    pub fn y(&self) -> CellValue<C::Base> {
+        self.y
+    }
 }
 
 /// Configuration for the ECC chip

From f655e38e3e46089879abc6ea320fa8bcababa44c Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Fri, 11 Jun 2021 11:27:23 +0800
Subject: [PATCH 10/17] chip::add_incomplete.rs: Remove superfluous check.

Co-authored-by: Jack Grigg <jack@electriccoin.co>
---
 src/circuit/gadget/ecc/chip/add_incomplete.rs | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/src/circuit/gadget/ecc/chip/add_incomplete.rs b/src/circuit/gadget/ecc/chip/add_incomplete.rs
index b1b5b0c1..9b658dde 100644
--- a/src/circuit/gadget/ecc/chip/add_incomplete.rs
+++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs
@@ -140,19 +140,6 @@ impl<C: CurveAffine> Config<C> {
             y: CellValue::<C::Base>::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)
     }
 }

From 6dabb16edc3d0cf549f4e32f8f58387b6653fc33 Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Fri, 11 Jun 2021 12:05:21 +0800
Subject: [PATCH 11/17] chip::add.rs: Use batch inversion for alpha, beta,
 gamma, delta

---
 src/circuit/gadget/ecc/chip/add.rs | 105 ++++++++++++++++-------------
 1 file changed, 60 insertions(+), 45 deletions(-)

diff --git a/src/circuit/gadget/ecc/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs
index f27ac9dc..3d31d9a0 100644
--- a/src/circuit/gadget/ecc/chip/add.rs
+++ b/src/circuit/gadget/ecc/chip/add.rs
@@ -3,7 +3,7 @@ use std::array;
 use super::{copy, CellValue, EccConfig, EccPoint, Var};
 use ff::Field;
 use halo2::{
-    arithmetic::{CurveAffine, FieldExt},
+    arithmetic::{BatchInvert, CurveAffine, FieldExt},
     circuit::Region,
     plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
     poly::Rotation,
@@ -218,8 +218,39 @@ impl<C: CurveAffine> Config<C> {
         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 = vec![alpha, beta, gamma, delta];
+                    inverses.batch_invert();
+                    inverses
+                });
+
+            if let Some(inverses) = inverses {
+                (
+                    Some(inverses[0]),
+                    Some(inverses[1]),
+                    Some(inverses[2]),
+                    Some(inverses[3]),
+                )
+            } else {
+                (None, None, None, None)
+            }
+        };
+
         // 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,
@@ -232,10 +263,7 @@ impl<C: CurveAffine> Config<C> {
             || "β",
             self.beta,
             offset,
-            || {
-                let beta = x_p.map(inv0);
-                beta.ok_or(Error::SynthesisError)
-            },
+            || beta.ok_or(Error::SynthesisError),
         )?;
 
         // Assign γ = inv0(x_q)
@@ -243,10 +271,7 @@ impl<C: CurveAffine> Config<C> {
             || "γ",
             self.gamma,
             offset,
-            || {
-                let gamma = x_q.map(inv0);
-                gamma.ok_or(Error::SynthesisError)
-            },
+            || gamma.ok_or(Error::SynthesisError),
         )?;
 
         // Assign δ = inv0(y_q + y_p) if x_q = x_p, 0 otherwise
@@ -257,43 +282,42 @@ impl<C: CurveAffine> Config<C> {
             || {
                 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)
+                    delta
                 } else {
-                    C::Base::zero()
+                    Some(C::Base::zero())
                 };
-                Ok(delta)
+                delta.ok_or(Error::SynthesisError)
             },
         )?;
 
         #[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()
+        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 {
-                        C::Base::zero()
+                        if y_p != C::Base::zero() {
+                            // 3(x_p)^2
+                            let three_x_p_sq = C::Base::from_u64(3) * x_p * x_p;
+                            // 1 / 2(y_p)
+                            let inv_two_y_p = y_p.invert().unwrap() * C::Base::TWO_INV;
+                            // λ = 3(x_p)^2 / 2(y_p)
+                            three_x_p_sq * inv_two_y_p
+                        } else {
+                            C::Base::zero()
+                        }
                     }
-                }
-            });
+                });
         region.assign_advice(
             || "λ",
             self.lambda,
@@ -378,15 +402,6 @@ impl<C: CurveAffine> Config<C> {
     }
 }
 
-// inv0(x) is 0 if x = 0, 1/x otherwise.
-fn inv0<F: FieldExt>(x: F) -> F {
-    if x == F::zero() {
-        F::zero()
-    } else {
-        x.invert().unwrap()
-    }
-}
-
 #[cfg(test)]
 pub mod tests {
     use group::Curve;

From e1779dab703f932ed252f3049a0404396871ba4f Mon Sep 17 00:00:00 2001
From: ying tong <yingtong@z.cash>
Date: Sat, 12 Jun 2021 06:36:26 +0800
Subject: [PATCH 12/17] Docfixes and minor refactors.

Co-authored-by: str4d <jack@electriccoin.co>
---
 src/circuit/gadget/ecc.rs                     |  9 ++--
 src/circuit/gadget/ecc/chip/add.rs            | 44 ++++++++-----------
 src/circuit/gadget/ecc/chip/add_incomplete.rs | 12 ++---
 3 files changed, 29 insertions(+), 36 deletions(-)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index d20ac5c2..55bdc42d 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -435,14 +435,13 @@ mod tests {
 
             // Generate a random point P
             let p_val = C::CurveExt::random(rand::rngs::OsRng).to_affine(); // P
-            let p = super::Point::new(chip.clone(), layouter.namespace(|| "point"), Some(p_val))?;
+            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(|| "point"), Some(p_neg))?;
+            let p_neg = super::Point::new(chip.clone(), layouter.namespace(|| "-P"), Some(p_neg))?;
 
             // Generate a random point Q
-            let q_val = C::CurveExt::random(rand::rngs::OsRng).to_affine(); // P
-            let q = super::Point::new(chip.clone(), layouter.namespace(|| "point"), Some(q_val))?;
+            let q_val = C::CurveExt::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);
diff --git a/src/circuit/gadget/ecc/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs
index 3d31d9a0..24064133 100644
--- a/src/circuit/gadget/ecc/chip/add.rs
+++ b/src/circuit/gadget/ecc/chip/add.rs
@@ -233,18 +233,13 @@ impl<C: CurveAffine> Config<C> {
                     let gamma = x_q;
                     let delta = y_q + y_p;
 
-                    let mut inverses = vec![alpha, beta, gamma, delta];
+                    let mut inverses = [alpha, beta, gamma, delta];
                     inverses.batch_invert();
                     inverses
                 });
 
-            if let Some(inverses) = inverses {
-                (
-                    Some(inverses[0]),
-                    Some(inverses[1]),
-                    Some(inverses[2]),
-                    Some(inverses[3]),
-                )
+            if let Some([alpha, beta, gamma, delta]) = inverses {
+                (Some(alpha), Some(beta), Some(gamma), Some(delta))
             } else {
                 (None, None, None, None)
             }
@@ -283,12 +278,11 @@ impl<C: CurveAffine> Config<C> {
                 let x_p = x_p.ok_or(Error::SynthesisError)?;
                 let x_q = x_q.ok_or(Error::SynthesisError)?;
 
-                let delta = if x_q == x_p {
-                    delta
+                if x_q == x_p {
+                    delta.ok_or(Error::SynthesisError)
                 } else {
-                    Some(C::Base::zero())
-                };
-                delta.ok_or(Error::SynthesisError)
+                    Ok(C::Base::zero())
+                }
             },
         )?;
 
@@ -428,28 +422,28 @@ pub mod tests {
         assert_ne!(p_val, q_val);
 
         // Check complete addition P + (-P)
-        p.add(layouter.namespace(|| "P + (-P)"), &p_neg)?;
+        p.add(layouter.namespace(|| "P + (-P)"), p_neg)?;
 
         // Check complete addition 𝒪 + 𝒪
-        zero.add(layouter.namespace(|| "𝒪 + 𝒪"), &zero)?;
+        zero.add(layouter.namespace(|| "𝒪 + 𝒪"), zero)?;
 
         // Check P + Q
-        p.add(layouter.namespace(|| "P + Q"), &q)?;
+        p.add(layouter.namespace(|| "P + Q"), q)?;
 
         // P + P
-        p.add(layouter.namespace(|| "P + P"), &p)?;
+        p.add(layouter.namespace(|| "P + P"), p)?;
 
         // P + 𝒪
-        p.add(layouter.namespace(|| "P + 𝒪"), &zero)?;
+        p.add(layouter.namespace(|| "P + 𝒪"), zero)?;
 
         // 𝒪 + P
-        zero.add(layouter.namespace(|| "𝒪 + P"), &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"),
+            layouter.namespace(|| "endo(P)"),
             Some(endo_p.to_affine()),
         )?;
         p.add(layouter.namespace(|| "P + endo(P)"), &endo_p)?;
@@ -458,7 +452,7 @@ pub mod tests {
         let endo_p_neg = (-p_val).to_curve().endo();
         let endo_p_neg = Point::new(
             chip.clone(),
-            layouter.namespace(|| "point"),
+            layouter.namespace(|| "endo(-P)"),
             Some(endo_p_neg.to_affine()),
         )?;
         p.add(layouter.namespace(|| "P + endo(-P)"), &endo_p_neg)?;
@@ -467,19 +461,19 @@ pub mod tests {
         let endo_2_p = p_val.to_curve().endo().endo();
         let endo_2_p = Point::new(
             chip.clone(),
-            layouter.namespace(|| "point"),
+            layouter.namespace(|| "endo^2(P)"),
             Some(endo_2_p.to_affine()),
         )?;
-        p.add(layouter.namespace(|| "P + endo(P)"), &endo_2_p)?;
+        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(|| "point"),
+            layouter.namespace(|| "endo^2(-P)"),
             Some(endo_2_p_neg.to_affine()),
         )?;
-        p.add(layouter.namespace(|| "P + endo(P)"), &endo_2_p_neg)?;
+        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
index 9b658dde..692525db 100644
--- a/src/circuit/gadget/ecc/chip/add_incomplete.rs
+++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs
@@ -161,26 +161,26 @@ pub mod tests {
         p_neg: &Point<C, EccChip>,
     ) -> Result<(), Error> {
         // P + Q
-        p.add_incomplete(layouter.namespace(|| "P + Q"), &q)?;
+        p.add_incomplete(layouter.namespace(|| "P + Q"), q)?;
 
         // P + P should return an error
-        p.add_incomplete(layouter.namespace(|| "P + P"), &p)
+        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)
+        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)
+        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)
+        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)
+        zero.add_incomplete(layouter.namespace(|| "𝒪 + 𝒪"), zero)
             .expect_err("𝒪 + 𝒪 should return an error");
 
         Ok(())

From aec7a7f850aaacc4b9ce1a6af25034699519198a Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 12 Jun 2021 06:09:15 +0800
Subject: [PATCH 13/17] ecc::chip.rs: Stub out scalar-mul-related structs and
 types.

These will be updated or restored in #111.
---
 src/circuit/gadget/ecc/chip.rs | 36 ++++++----------------------------
 1 file changed, 6 insertions(+), 30 deletions(-)

diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs
index 5d95a272..8335efc2 100644
--- a/src/circuit/gadget/ecc/chip.rs
+++ b/src/circuit/gadget/ecc/chip.rs
@@ -1,7 +1,6 @@
 use super::EccInstructions;
 use crate::circuit::gadget::utilities::{copy, CellValue, Var};
-use crate::constants::{self, OrchardFixedBasesFull, ValueCommitV};
-use arrayvec::ArrayVec;
+use crate::constants;
 use ff::{Field, PrimeFieldBits};
 use halo2::{
     arithmetic::CurveAffine,
@@ -175,40 +174,17 @@ where
     }
 }
 
-/// A full-width scalar used for fixed-base scalar multiplication.
-/// This is decomposed in chunks of `window_width` bits in little-endian order.
-/// For example, if `window_width` = 3, we will have [k_0, k_1, ..., k_n]
-/// where `scalar = k_0 + k_1 * (2^3) + ... + k_n * (2^3)^n` and each `k_i` is
-/// in the range [0..2^3).
-#[derive(Clone, Debug)]
-pub struct EccScalarFixed<C: CurveAffine> {
-    value: Option<C::Scalar>,
-    windows: ArrayVec<CellValue<C::Base>, { constants::NUM_WINDOWS }>,
-}
-
-/// A signed short scalar used for fixed-base scalar multiplication.
-/// This is decomposed in chunks of `window_width` bits in little-endian order.
-/// For example, if `window_width` = 3, we will have [k_0, k_1, ..., k_n]
-/// where `scalar = k_0 + k_1 * (2^3) + ... + k_n * (2^3)^n` and each `k_i` is
-/// in the range [0..2^3).
-#[derive(Clone, Debug)]
-pub struct EccScalarFixedShort<C: CurveAffine> {
-    magnitude: Option<C::Scalar>,
-    sign: CellValue<C::Base>,
-    windows: ArrayVec<CellValue<C::Base>, { constants::NUM_WINDOWS_SHORT }>,
-}
-
 impl<C: CurveAffine> EccInstructions<C> for EccChip<C>
 where
     C::Scalar: PrimeFieldBits,
 {
-    type ScalarFixed = EccScalarFixed<C>;
-    type ScalarFixedShort = EccScalarFixedShort<C>;
-    type ScalarVar = CellValue<C::Base>;
+    type ScalarFixed = (); // TODO
+    type ScalarFixedShort = (); // TODO
+    type ScalarVar = (); // TODO
     type Point = EccPoint<C>;
     type X = CellValue<C::Base>;
-    type FixedPoints = OrchardFixedBasesFull<C>;
-    type FixedPointsShort = ValueCommitV<C>;
+    type FixedPoints = (); // TODO
+    type FixedPointsShort = (); // TODO
 
     fn witness_scalar_var(
         &self,

From e259bb3846c4e0ed96cd7e72fe81422150d735cb Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 12 Jun 2021 06:29:05 +0800
Subject: [PATCH 14/17] ecc::chip.rs: Use concrete pallas::Affine for Chip
 impl.

The EccInstructions trait is still generic over C: CurveAffine;
however, the EccChip implementation is specific to the pasta
curves.
---
 src/circuit/gadget/ecc.rs                     | 34 +++----
 src/circuit/gadget/ecc/chip.rs                | 98 +++++++++----------
 src/circuit/gadget/ecc/chip/add.rs            | 84 ++++++++--------
 src/circuit/gadget/ecc/chip/add_incomplete.rs | 35 +++----
 src/circuit/gadget/ecc/chip/witness_point.rs  | 35 +++----
 5 files changed, 130 insertions(+), 156 deletions(-)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index 55bdc42d..813a0aec 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -378,30 +378,24 @@ where
 
 #[cfg(test)]
 mod tests {
-    use ff::PrimeFieldBits;
-    use group::{Curve, Group};
+    use group::{prime::PrimeCurveAffine, Curve, Group};
+
     use halo2::{
-        arithmetic::CurveAffine,
         circuit::{layouter::SingleChipLayouter, Layouter},
         dev::MockProver,
-        pasta::pallas,
         plonk::{Assignment, Circuit, ConstraintSystem, Error},
     };
+    use pasta_curves::pallas;
 
     use super::chip::{EccChip, EccConfig};
 
-    struct MyCircuit<C: CurveAffine> {
-        _marker: std::marker::PhantomData<C>,
-    }
+    struct MyCircuit {}
 
     #[allow(non_snake_case)]
-    impl<C: CurveAffine> Circuit<C::Base> for MyCircuit<C>
-    where
-        C::Scalar: PrimeFieldBits,
-    {
-        type Config = EccConfig<C>;
+    impl Circuit<pallas::Base> for MyCircuit {
+        type Config = EccConfig;
 
-        fn configure(meta: &mut ConstraintSystem<C::Base>) -> Self::Config {
+        fn configure(meta: &mut ConstraintSystem<pallas::Base>) -> Self::Config {
             let advices = [
                 meta.advice_column(),
                 meta.advice_column(),
@@ -422,25 +416,25 @@ mod tests {
                     .collect::<Vec<_>>(),
             );
 
-            EccChip::<C>::configure(meta, advices, perm)
+            EccChip::configure(meta, advices, perm)
         }
 
         fn synthesize(
             &self,
-            cs: &mut impl Assignment<C::Base>,
+            cs: &mut impl Assignment<pallas::Base>,
             config: Self::Config,
         ) -> Result<(), Error> {
             let mut layouter = SingleChipLayouter::new(cs)?;
             let chip = EccChip::construct(config);
 
             // Generate a random point P
-            let p_val = C::CurveExt::random(rand::rngs::OsRng).to_affine(); // 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 = C::CurveExt::random(rand::rngs::OsRng).to_affine(); // 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.
@@ -451,7 +445,7 @@ mod tests {
                 super::Point::new(
                     chip.clone(),
                     layouter.namespace(|| "identity"),
-                    Some(C::identity()),
+                    Some(pallas::Affine::identity()),
                 )?
             };
 
@@ -487,9 +481,7 @@ mod tests {
     #[test]
     fn ecc() {
         let k = 5;
-        let circuit = MyCircuit::<pallas::Affine> {
-            _marker: std::marker::PhantomData,
-        };
+        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
index 8335efc2..fda8f793 100644
--- a/src/circuit/gadget/ecc/chip.rs
+++ b/src/circuit/gadget/ecc/chip.rs
@@ -1,13 +1,13 @@
 use super::EccInstructions;
 use crate::circuit::gadget::utilities::{copy, CellValue, Var};
 use crate::constants;
-use ff::{Field, PrimeFieldBits};
+
+use group::prime::PrimeCurveAffine;
 use halo2::{
-    arithmetic::CurveAffine,
     circuit::{Chip, Layouter},
     plonk::{Advice, Column, ConstraintSystem, Error, Fixed, Permutation, Selector},
 };
-use std::marker::PhantomData;
+use pasta_curves::{arithmetic::CurveAffine, pallas};
 
 pub(super) mod add;
 pub(super) mod add_incomplete;
@@ -19,22 +19,22 @@ pub(super) mod witness_point;
 /// A curve point represented in affine (x, y) coordinates. Each coordinate is
 /// assigned to a cell.
 #[derive(Clone, Debug)]
-pub struct EccPoint<C: CurveAffine> {
+pub struct EccPoint {
     /// x-coordinate
-    x: CellValue<C::Base>,
+    x: CellValue<pallas::Base>,
     /// y-coordinate
-    y: CellValue<C::Base>,
+    y: CellValue<pallas::Base>,
 }
 
-impl<C: CurveAffine> EccPoint<C> {
+impl EccPoint {
     /// Returns the value of this curve point, if known.
-    pub fn point(&self) -> Option<C> {
+    pub fn point(&self) -> Option<pallas::Affine> {
         match (self.x.value(), self.y.value()) {
             (Some(x), Some(y)) => {
-                if x == C::Base::zero() && y == C::Base::zero() {
-                    Some(C::identity())
+                if x == pallas::Base::zero() && y == pallas::Base::zero() {
+                    Some(pallas::Affine::identity())
                 } else {
-                    Some(C::from_xy(x, y).unwrap())
+                    Some(pallas::Affine::from_xy(x, y).unwrap())
                 }
             }
             _ => None,
@@ -42,12 +42,12 @@ impl<C: CurveAffine> EccPoint<C> {
     }
     /// The cell containing the affine short-Weierstrass x-coordinate,
     /// or 0 for the zero point.
-    pub fn x(&self) -> CellValue<C::Base> {
+    pub fn x(&self) -> CellValue<pallas::Base> {
         self.x
     }
     /// The cell containing the affine short-Weierstrass y-coordinate,
     /// or 0 for the zero point.
-    pub fn y(&self) -> CellValue<C::Base> {
+    pub fn y(&self) -> CellValue<pallas::Base> {
         self.y
     }
 }
@@ -55,7 +55,7 @@ impl<C: CurveAffine> EccPoint<C> {
 /// Configuration for the ECC chip
 #[derive(Clone, Debug, Eq, PartialEq)]
 #[allow(non_snake_case)]
-pub struct EccConfig<C: CurveAffine> {
+pub struct EccConfig {
     /// Advice columns needed by instructions in the ECC chip.
     pub advices: [Column<Advice>; 10],
 
@@ -88,17 +88,16 @@ pub struct EccConfig<C: CurveAffine> {
     pub q_scalar_fixed_short: Selector,
     /// Permutation
     pub perm: Permutation,
-    _marker: PhantomData<C>,
 }
 
 /// A chip implementing EccInstructions
 #[derive(Clone, Debug, Eq, PartialEq)]
-pub struct EccChip<C: CurveAffine> {
-    config: EccConfig<C>,
+pub struct EccChip {
+    config: EccConfig,
 }
 
-impl<C: CurveAffine> Chip<C::Base> for EccChip<C> {
-    type Config = EccConfig<C>;
+impl Chip<pallas::Base> for EccChip {
+    type Config = EccConfig;
     type Loaded = ();
 
     fn config(&self) -> &Self::Config {
@@ -110,21 +109,18 @@ impl<C: CurveAffine> Chip<C::Base> for EccChip<C> {
     }
 }
 
-impl<C: CurveAffine> EccChip<C>
-where
-    C::Scalar: PrimeFieldBits,
-{
-    pub fn construct(config: <Self as Chip<C::Base>>::Config) -> Self {
+impl EccChip {
+    pub fn construct(config: <Self as Chip<pallas::Base>>::Config) -> Self {
         Self { config }
     }
 
     #[allow(non_snake_case)]
     pub fn configure(
-        meta: &mut ConstraintSystem<C::Base>,
+        meta: &mut ConstraintSystem<pallas::Base>,
         advices: [Column<Advice>; 10],
         perm: Permutation,
-    ) -> <Self as Chip<C::Base>>::Config {
-        let config = EccConfig::<C> {
+    ) -> <Self as Chip<pallas::Base>>::Config {
+        let config = EccConfig {
             advices,
             lagrange_coeffs: [
                 meta.fixed_column(),
@@ -149,24 +145,23 @@ where
             q_scalar_fixed: meta.selector(),
             q_scalar_fixed_short: meta.selector(),
             perm,
-            _marker: PhantomData,
         };
 
         // Create witness point gate
         {
-            let config: witness_point::Config<C> = (&config).into();
+            let config: witness_point::Config = (&config).into();
             config.create_gate(meta);
         }
 
         // Create incomplete point addition gate
         {
-            let config: add_incomplete::Config<C> = (&config).into();
+            let config: add_incomplete::Config = (&config).into();
             config.create_gate(meta);
         }
 
         // Create complete point addition gate
         {
-            let add_config: add::Config<C> = (&config).into();
+            let add_config: add::Config = (&config).into();
             add_config.create_gate(meta);
         }
 
@@ -174,48 +169,45 @@ where
     }
 }
 
-impl<C: CurveAffine> EccInstructions<C> for EccChip<C>
-where
-    C::Scalar: PrimeFieldBits,
-{
+impl EccInstructions<pallas::Affine> for EccChip {
     type ScalarFixed = (); // TODO
     type ScalarFixedShort = (); // TODO
     type ScalarVar = (); // TODO
-    type Point = EccPoint<C>;
-    type X = CellValue<C::Base>;
+    type Point = EccPoint;
+    type X = CellValue<pallas::Base>;
     type FixedPoints = (); // TODO
     type FixedPointsShort = (); // TODO
 
     fn witness_scalar_var(
         &self,
-        _layouter: &mut impl Layouter<C::Base>,
-        _value: Option<C::Base>,
+        _layouter: &mut impl Layouter<pallas::Base>,
+        _value: Option<pallas::Base>,
     ) -> Result<Self::ScalarVar, Error> {
         todo!()
     }
 
     fn witness_scalar_fixed(
         &self,
-        _layouter: &mut impl Layouter<C::Base>,
-        _value: Option<C::Scalar>,
+        _layouter: &mut impl Layouter<pallas::Base>,
+        _value: Option<pallas::Scalar>,
     ) -> Result<Self::ScalarFixed, Error> {
         todo!()
     }
 
     fn witness_scalar_fixed_short(
         &self,
-        _layouter: &mut impl Layouter<C::Base>,
-        _value: Option<C::Scalar>,
+        _layouter: &mut impl Layouter<pallas::Base>,
+        _value: Option<pallas::Scalar>,
     ) -> Result<Self::ScalarFixedShort, Error> {
         todo!()
     }
 
     fn witness_point(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
-        value: Option<C>,
+        layouter: &mut impl Layouter<pallas::Base>,
+        value: Option<pallas::Affine>,
     ) -> Result<Self::Point, Error> {
-        let config: witness_point::Config<C> = self.config().into();
+        let config: witness_point::Config = self.config().into();
         layouter.assign_region(
             || "witness point",
             |mut region| config.assign_region(value, 0, &mut region),
@@ -228,11 +220,11 @@ where
 
     fn add_incomplete(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
+        layouter: &mut impl Layouter<pallas::Base>,
         a: &Self::Point,
         b: &Self::Point,
     ) -> Result<Self::Point, Error> {
-        let config: add_incomplete::Config<C> = self.config().into();
+        let config: add_incomplete::Config = self.config().into();
         layouter.assign_region(
             || "incomplete point addition",
             |mut region| config.assign_region(a, b, 0, &mut region),
@@ -241,11 +233,11 @@ where
 
     fn add(
         &self,
-        layouter: &mut impl Layouter<C::Base>,
+        layouter: &mut impl Layouter<pallas::Base>,
         a: &Self::Point,
         b: &Self::Point,
     ) -> Result<Self::Point, Error> {
-        let config: add::Config<C> = self.config().into();
+        let config: add::Config = self.config().into();
         layouter.assign_region(
             || "complete point addition",
             |mut region| config.assign_region(a, b, 0, &mut region),
@@ -254,7 +246,7 @@ where
 
     fn mul(
         &self,
-        _layouter: &mut impl Layouter<C::Base>,
+        _layouter: &mut impl Layouter<pallas::Base>,
         _scalar: &Self::ScalarVar,
         _base: &Self::Point,
     ) -> Result<Self::Point, Error> {
@@ -263,7 +255,7 @@ where
 
     fn mul_fixed(
         &self,
-        _layouter: &mut impl Layouter<C::Base>,
+        _layouter: &mut impl Layouter<pallas::Base>,
         _scalar: &Self::ScalarFixed,
         _base: &Self::FixedPoints,
     ) -> Result<Self::Point, Error> {
@@ -272,7 +264,7 @@ where
 
     fn mul_fixed_short(
         &self,
-        _layouter: &mut impl Layouter<C::Base>,
+        _layouter: &mut impl Layouter<pallas::Base>,
         _scalar: &Self::ScalarFixedShort,
         _base: &Self::FixedPointsShort,
     ) -> Result<Self::Point, Error> {
diff --git a/src/circuit/gadget/ecc/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs
index 24064133..2e821774 100644
--- a/src/circuit/gadget/ecc/chip/add.rs
+++ b/src/circuit/gadget/ecc/chip/add.rs
@@ -3,15 +3,16 @@ use std::array;
 use super::{copy, CellValue, EccConfig, EccPoint, Var};
 use ff::Field;
 use halo2::{
-    arithmetic::{BatchInvert, CurveAffine, FieldExt},
+    arithmetic::BatchInvert,
     circuit::Region,
     plonk::{Advice, Column, ConstraintSystem, Error, Expression, Permutation, Selector},
     poly::Rotation,
 };
-use std::{collections::HashSet, marker::PhantomData};
+use pasta_curves::{arithmetic::FieldExt, pallas};
+use std::collections::HashSet;
 
 #[derive(Clone, Debug)]
-pub struct Config<C: CurveAffine> {
+pub struct Config {
     q_add: Selector,
     // lambda
     lambda: Column<Advice>,
@@ -33,11 +34,10 @@ pub struct Config<C: CurveAffine> {
     delta: Column<Advice>,
     // Permutation
     perm: Permutation,
-    _marker: PhantomData<C>,
 }
 
-impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
-    fn from(ecc_config: &EccConfig<C>) -> Self {
+impl From<&EccConfig> for Config {
+    fn from(ecc_config: &EccConfig) -> Self {
         Self {
             q_add: ecc_config.q_add,
             x_p: ecc_config.advices[0],
@@ -50,12 +50,11 @@ impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
             gamma: ecc_config.advices[7],
             delta: ecc_config.advices[8],
             perm: ecc_config.perm.clone(),
-            _marker: PhantomData,
         }
     }
 }
 
-impl<C: CurveAffine> Config<C> {
+impl Config {
     pub(crate) fn advice_columns(&self) -> HashSet<Column<Advice>> {
         core::array::IntoIter::new([
             self.x_p,
@@ -71,7 +70,7 @@ impl<C: CurveAffine> Config<C> {
         .collect()
     }
 
-    pub(crate) fn create_gate(&self, meta: &mut ConstraintSystem<C::Base>) {
+    pub(crate) fn create_gate(&self, meta: &mut ConstraintSystem<pallas::Base>) {
         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());
@@ -102,9 +101,9 @@ impl<C: CurveAffine> Config<C> {
             let if_delta = (y_q.clone() + y_p.clone()) * delta;
 
             // Useful constants
-            let one = Expression::Constant(C::Base::one());
-            let two = Expression::Constant(C::Base::from_u64(2));
-            let three = Expression::Constant(C::Base::from_u64(3));
+            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 = {
@@ -199,11 +198,11 @@ impl<C: CurveAffine> Config<C> {
 
     pub(super) fn assign_region(
         &self,
-        p: &EccPoint<C>,
-        q: &EccPoint<C>,
+        p: &EccPoint,
+        q: &EccPoint,
         offset: usize,
-        region: &mut Region<'_, C::Base>,
-    ) -> Result<EccPoint<C>, Error> {
+        region: &mut Region<'_, pallas::Base>,
+    ) -> Result<EccPoint, Error> {
         // Enable `q_add` selector
         self.q_add.enable(region, offset)?;
 
@@ -281,7 +280,7 @@ impl<C: CurveAffine> Config<C> {
                 if x_q == x_p {
                     delta.ok_or(Error::SynthesisError)
                 } else {
-                    Ok(C::Base::zero())
+                    Ok(pallas::Base::zero())
                 }
             },
         )?;
@@ -300,15 +299,15 @@ impl<C: CurveAffine> Config<C> {
                         // know that x_q != x_p in this branch.
                         (y_q - y_p) * alpha
                     } else {
-                        if y_p != C::Base::zero() {
+                        if y_p != pallas::Base::zero() {
                             // 3(x_p)^2
-                            let three_x_p_sq = C::Base::from_u64(3) * x_p * x_p;
+                            let three_x_p_sq = pallas::Base::from_u64(3) * x_p * x_p;
                             // 1 / 2(y_p)
-                            let inv_two_y_p = y_p.invert().unwrap() * C::Base::TWO_INV;
+                            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 {
-                            C::Base::zero()
+                            pallas::Base::zero()
                         }
                     }
                 });
@@ -326,15 +325,15 @@ impl<C: CurveAffine> Config<C> {
                 .zip(y_q)
                 .zip(lambda)
                 .map(|((((x_p, y_p), x_q), y_q), lambda)| {
-                    if x_p == C::Base::zero() {
+                    if x_p == pallas::Base::zero() {
                         // 0 + Q = Q
                         x_q
-                    } else if x_q == C::Base::zero() {
+                    } else if x_q == pallas::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()
+                        pallas::Base::zero()
                     } else {
                         // x_r = λ^2 - x_p - x_q
                         lambda * lambda - x_p - x_q
@@ -350,15 +349,15 @@ impl<C: CurveAffine> Config<C> {
         // 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() {
+                if x_p == pallas::Base::zero() {
                     // 0 + Q = Q
                     y_q
-                } else if x_q == C::Base::zero() {
+                } else if x_q == pallas::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()
+                    pallas::Base::zero()
                 } else {
                     // y_r = λ(x_p - x_r) - y_p
                     lambda * (x_p - x_r) - y_p
@@ -372,9 +371,9 @@ impl<C: CurveAffine> Config<C> {
             || y_r.ok_or(Error::SynthesisError),
         )?;
 
-        let result = EccPoint::<C> {
-            x: CellValue::<C::Base>::new(x_r_cell, x_r),
-            y: CellValue::<C::Base>::new(y_r_cell, y_r),
+        let result = EccPoint {
+            x: CellValue::<pallas::Base>::new(x_r_cell, x_r),
+            y: CellValue::<pallas::Base>::new(y_r_cell, y_r),
         };
 
         #[cfg(test)]
@@ -398,25 +397,22 @@ impl<C: CurveAffine> Config<C> {
 
 #[cfg(test)]
 pub mod tests {
-    use group::Curve;
-    use halo2::{
-        arithmetic::{CurveAffine, CurveExt},
-        circuit::Layouter,
-        plonk::Error,
-    };
+    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<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Eq + std::fmt::Debug>(
+    pub fn test_add<EccChip: EccInstructions<pallas::Affine> + Clone + Eq + std::fmt::Debug>(
         chip: EccChip,
-        mut layouter: impl Layouter<C::Base>,
-        zero: &Point<C, EccChip>,
-        p_val: C,
-        p: &Point<C, EccChip>,
-        q_val: C,
-        q: &Point<C, EccChip>,
-        p_neg: &Point<C, EccChip>,
+        mut layouter: impl Layouter<pallas::Base>,
+        zero: &Point<pallas::Affine, EccChip>,
+        p_val: pallas::Affine,
+        p: &Point<pallas::Affine, EccChip>,
+        q_val: pallas::Affine,
+        q: &Point<pallas::Affine, EccChip>,
+        p_neg: &Point<pallas::Affine, EccChip>,
     ) -> Result<(), Error> {
         // Make sure P and Q are not the same point.
         assert_ne!(p_val, q_val);
diff --git a/src/circuit/gadget/ecc/chip/add_incomplete.rs b/src/circuit/gadget/ecc/chip/add_incomplete.rs
index 692525db..bfeae528 100644
--- a/src/circuit/gadget/ecc/chip/add_incomplete.rs
+++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs
@@ -1,17 +1,16 @@
-use std::{array, marker::PhantomData};
+use std::array;
 
 use super::{copy, CellValue, EccConfig, EccPoint, Var};
-use ff::Field;
 use group::Curve;
 use halo2::{
-    arithmetic::CurveAffine,
     circuit::Region,
     plonk::{Advice, Column, ConstraintSystem, Error, Permutation, Selector},
     poly::Rotation,
 };
+use pasta_curves::{arithmetic::CurveAffine, pallas};
 
 #[derive(Clone, Debug)]
-pub struct Config<C: CurveAffine> {
+pub struct Config {
     q_add_incomplete: Selector,
     // x-coordinate of P in P + Q = R
     pub x_p: Column<Advice>,
@@ -23,11 +22,10 @@ pub struct Config<C: CurveAffine> {
     pub y_qr: Column<Advice>,
     // Permutation
     perm: Permutation,
-    _marker: PhantomData<C>,
 }
 
-impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
-    fn from(ecc_config: &EccConfig<C>) -> Self {
+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],
@@ -35,13 +33,12 @@ impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
             x_qr: ecc_config.advices[2],
             y_qr: ecc_config.advices[3],
             perm: ecc_config.perm.clone(),
-            _marker: PhantomData,
         }
     }
 }
 
-impl<C: CurveAffine> Config<C> {
-    pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<C::Base>) {
+impl Config {
+    pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<pallas::Base>) {
         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());
@@ -68,11 +65,11 @@ impl<C: CurveAffine> Config<C> {
 
     pub(super) fn assign_region(
         &self,
-        p: &EccPoint<C>,
-        q: &EccPoint<C>,
+        p: &EccPoint,
+        q: &EccPoint,
         offset: usize,
-        region: &mut Region<'_, C::Base>,
-    ) -> Result<EccPoint<C>, Error> {
+        region: &mut Region<'_, pallas::Base>,
+    ) -> Result<EccPoint, Error> {
         // Enable `q_add_incomplete` selector
         self.q_add_incomplete.enable(region, offset)?;
 
@@ -84,9 +81,9 @@ impl<C: CurveAffine> Config<C> {
             .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())
+                if (x_p == pallas::Base::zero() && y_p == pallas::Base::zero())
                 // Q is point at infinity
-                || (x_q == C::Base::zero() && y_q == C::Base::zero())
+                || (x_q == pallas::Base::zero() && y_q == pallas::Base::zero())
                 // x_p = x_q
                 || (x_p == x_q)
                 {
@@ -135,9 +132,9 @@ impl<C: CurveAffine> Config<C> {
             || y_r.ok_or(Error::SynthesisError),
         )?;
 
-        let result = EccPoint::<C> {
-            x: CellValue::<C::Base>::new(x_r_var, x_r),
-            y: CellValue::<C::Base>::new(y_r_var, y_r),
+        let result = EccPoint {
+            x: CellValue::<pallas::Base>::new(x_r_var, x_r),
+            y: CellValue::<pallas::Base>::new(y_r_var, y_r),
         };
 
         Ok(result)
diff --git a/src/circuit/gadget/ecc/chip/witness_point.rs b/src/circuit/gadget/ecc/chip/witness_point.rs
index c582e9cd..33bef835 100644
--- a/src/circuit/gadget/ecc/chip/witness_point.rs
+++ b/src/circuit/gadget/ecc/chip/witness_point.rs
@@ -1,38 +1,35 @@
 use super::{CellValue, EccConfig, EccPoint, Var};
 
-use ff::Field;
+use group::prime::PrimeCurveAffine;
+
 use halo2::{
-    arithmetic::CurveAffine,
     circuit::Region,
     plonk::{Advice, Column, ConstraintSystem, Error, Expression, Selector},
     poly::Rotation,
 };
-
-use std::marker::PhantomData;
+use pasta_curves::{arithmetic::CurveAffine, pallas};
 
 #[derive(Clone, Debug)]
-pub struct Config<C: CurveAffine> {
+pub struct Config {
     q_point: Selector,
     // x-coordinate
     pub x: Column<Advice>,
     // y-coordinate
     pub y: Column<Advice>,
-    _marker: PhantomData<C>,
 }
 
-impl<C: CurveAffine> From<&EccConfig<C>> for Config<C> {
-    fn from(ecc_config: &EccConfig<C>) -> Self {
+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],
-            _marker: PhantomData,
         }
     }
 }
 
-impl<C: CurveAffine> Config<C> {
-    pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<C::Base>) {
+impl Config {
+    pub(super) fn create_gate(&self, meta: &mut ConstraintSystem<pallas::Base>) {
         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
@@ -45,7 +42,7 @@ impl<C: CurveAffine> Config<C> {
             // y^2 = x^3 + b
             let curve_eqn = y.clone() * y.clone()
                 - (x.clone() * x.clone() * x.clone())
-                - Expression::Constant(C::b());
+                - Expression::Constant(pallas::Affine::b());
 
             vec![
                 q_point.clone() * x * curve_eqn.clone(),
@@ -56,17 +53,17 @@ impl<C: CurveAffine> Config<C> {
 
     pub(super) fn assign_region(
         &self,
-        value: Option<C>,
+        value: Option<pallas::Affine>,
         offset: usize,
-        region: &mut Region<'_, C::Base>,
-    ) -> Result<EccPoint<C>, Error> {
+        region: &mut Region<'_, pallas::Base>,
+    ) -> Result<EccPoint, Error> {
         // Enable `q_point` selector
         self.q_point.enable(region, offset)?;
 
         let value = value.map(|value| {
             // Map the identity to (0, 0).
-            if value == C::identity() {
-                (C::Base::zero(), C::Base::zero())
+            if value == pallas::Affine::identity() {
+                (pallas::Base::zero(), pallas::Base::zero())
             } else {
                 let value = value.coordinates().unwrap();
                 (*value.x(), *value.y())
@@ -92,8 +89,8 @@ impl<C: CurveAffine> Config<C> {
         )?;
 
         Ok(EccPoint {
-            x: CellValue::<C::Base>::new(x_var, x_val),
-            y: CellValue::<C::Base>::new(y_var, y_val),
+            x: CellValue::<pallas::Base>::new(x_var, x_val),
+            y: CellValue::<pallas::Base>::new(y_var, y_val),
         })
     }
 }

From a11c2066efea1d136e738c15d40e140316c16f3c Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sat, 12 Jun 2021 06:59:02 +0800
Subject: [PATCH 15/17] chip::add.rs: Use Expression::square() + other minor
 refactors

Co-authored-by: Jack Grigg <jack@electriccoin.co>
---
 Cargo.toml                         |  2 +-
 src/circuit/gadget/ecc/chip/add.rs | 67 +++++++++++++-----------------
 2 files changed, 29 insertions(+), 40 deletions(-)

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/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs
index 2e821774..8f06a8c6 100644
--- a/src/circuit/gadget/ecc/chip/add.rs
+++ b/src/circuit/gadget/ecc/chip/add.rs
@@ -118,7 +118,7 @@ impl Config {
 
             // (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 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)
 
@@ -127,13 +127,12 @@ impl Config {
             };
 
             // 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)
-                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.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
@@ -151,11 +150,9 @@ impl Config {
             // 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.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
@@ -301,7 +298,7 @@ impl Config {
                     } else {
                         if y_p != pallas::Base::zero() {
                             // 3(x_p)^2
-                            let three_x_p_sq = pallas::Base::from_u64(3) * x_p * x_p;
+                            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)
@@ -318,27 +315,35 @@ impl Config {
             || lambda.ok_or(Error::SynthesisError),
         )?;
 
-        // Assign x_r
-        let x_r =
+        // 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
-                    } else if x_q == pallas::Base::zero() {
-                        // P + 0 = P
-                        x_p
-                    } else if (x_q == x_p) && (y_q == -y_p) {
-                        // P + (-P) maps to (0,0)
-                        pallas::Base::zero()
-                    } else {
-                        // x_r = λ^2 - x_p - x_q
-                        lambda * lambda - x_p - x_q
+                    {
+                        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,
@@ -347,23 +352,7 @@ impl Config {
         )?;
 
         // 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 == pallas::Base::zero() {
-                    // 0 + Q = Q
-                    y_q
-                } else if x_q == pallas::Base::zero() {
-                    // P + 0 = P
-                    y_p
-                } else if (x_q == x_p) && (y_q == -y_p) {
-                    // P + (-P) maps to (0,0)
-                    pallas::Base::zero()
-                } else {
-                    // y_r = λ(x_p - x_r) - y_p
-                    lambda * (x_p - x_r) - y_p
-                }
-            },
-        );
+        let y_r = r.map(|r| r.1);
         let y_r_cell = region.assign_advice(
             || "y_r",
             self.y_qr,

From 7341996d2ce0d6a12c417f4f3385bc192d86b88c Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Sun, 13 Jun 2021 21:26:30 +0800
Subject: [PATCH 16/17] gadget::ecc.rs: Add EccInstructions::constrain_equal()
 instruction.

This allows us to constrain two points to be equal in value at the
gadget level.

Co-authored-by: Jack Grigg <jack@electriccoin.co>
---
 src/circuit/gadget/ecc.rs          | 18 ++++++++++++++
 src/circuit/gadget/ecc/chip.rs     | 18 ++++++++++++++
 src/circuit/gadget/ecc/chip/add.rs | 40 +++++++++++++++++++++++++-----
 3 files changed, 70 insertions(+), 6 deletions(-)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index 813a0aec..d5700381 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -43,6 +43,14 @@ pub trait EccInstructions<C: CurveAffine>: Chip<C::Base> {
     /// Enumeration of the set of fixed bases to be used in short signed scalar mul.
     type FixedPointsShort: Clone + Debug;
 
+    /// Constrains point `a` to be equal in value to point `b`.
+    fn constrain_equal(
+        &self,
+        layouter: &mut impl Layouter<C::Base>,
+        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.
     fn witness_scalar_var(
@@ -237,6 +245,16 @@ impl<C: CurveAffine, EccChip: EccInstructions<C> + Clone + Debug + Eq> Point<C,
         point.map(|inner| Point { chip, inner })
     }
 
+    /// Constrains this point to be equal in value to another point.
+    pub fn constrain_equal(
+        &self,
+        mut layouter: impl Layouter<C::Base>,
+        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<C, EccChip> {
         X::from_inner(self.chip.clone(), EccChip::extract_p(&self.inner).clone())
diff --git a/src/circuit/gadget/ecc/chip.rs b/src/circuit/gadget/ecc/chip.rs
index fda8f793..e398547c 100644
--- a/src/circuit/gadget/ecc/chip.rs
+++ b/src/circuit/gadget/ecc/chip.rs
@@ -178,6 +178,24 @@ impl EccInstructions<pallas::Affine> for EccChip {
     type FixedPoints = (); // TODO
     type FixedPointsShort = (); // TODO
 
+    fn constrain_equal(
+        &self,
+        layouter: &mut impl Layouter<pallas::Base>,
+        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<pallas::Base>,
diff --git a/src/circuit/gadget/ecc/chip/add.rs b/src/circuit/gadget/ecc/chip/add.rs
index 8f06a8c6..555645b6 100644
--- a/src/circuit/gadget/ecc/chip/add.rs
+++ b/src/circuit/gadget/ecc/chip/add.rs
@@ -407,22 +407,50 @@ pub mod tests {
         assert_ne!(p_val, q_val);
 
         // Check complete addition P + (-P)
-        p.add(layouter.namespace(|| "P + (-P)"), p_neg)?;
+        {
+            let result = p.add(layouter.namespace(|| "P + (-P)"), p_neg)?;
+            result.constrain_equal(layouter.namespace(|| "P + (-P) = 0"), zero)?;
+        }
 
         // Check complete addition 𝒪 + 𝒪
-        zero.add(layouter.namespace(|| "𝒪 + 𝒪"), zero)?;
+        {
+            let result = zero.add(layouter.namespace(|| "𝒪 + 𝒪"), zero)?;
+            result.constrain_equal(layouter.namespace(|| "P + (-P) = 0"), zero)?;
+        }
 
         // Check P + Q
-        p.add(layouter.namespace(|| "P + Q"), 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
-        p.add(layouter.namespace(|| "P + 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 + 𝒪
-        p.add(layouter.namespace(|| "P + 𝒪"), zero)?;
+        {
+            let result = p.add(layouter.namespace(|| "P + 𝒪"), zero)?;
+            result.constrain_equal(layouter.namespace(|| "P + 𝒪 = P"), p)?;
+        }
 
         // 𝒪 + P
-        zero.add(layouter.namespace(|| "𝒪 + 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();

From 8a8df98a5094e7300dcaf5a32295e325965c2288 Mon Sep 17 00:00:00 2001
From: therealyingtong <yingtong@z.cash>
Date: Mon, 14 Jun 2021 00:19:21 +0800
Subject: [PATCH 17/17] add_incomplete::tests: Constrain output of `P + Q`
 test.

Also minor docfixes and refactors.

Co-authored-by: Jack Grigg <jack@electriccoin.co>
---
 src/circuit/gadget/ecc.rs                     |  7 ++--
 src/circuit/gadget/ecc/chip/add.rs            |  4 +--
 src/circuit/gadget/ecc/chip/add_incomplete.rs | 33 +++++++++++++------
 src/circuit/gadget/ecc/chip/witness_point.rs  |  4 +--
 4 files changed, 32 insertions(+), 16 deletions(-)

diff --git a/src/circuit/gadget/ecc.rs b/src/circuit/gadget/ecc.rs
index d5700381..6e26971c 100644
--- a/src/circuit/gadget/ecc.rs
+++ b/src/circuit/gadget/ecc.rs
@@ -470,7 +470,7 @@ mod tests {
             // Test complete addition
             {
                 super::chip::add::tests::test_add(
-                    chip,
+                    chip.clone(),
                     layouter.namespace(|| "complete addition"),
                     &zero,
                     p_val,
@@ -484,9 +484,12 @@ mod tests {
             // 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,
                 )?;
@@ -498,7 +501,7 @@ mod tests {
 
     #[test]
     fn ecc() {
-        let k = 5;
+        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/add.rs b/src/circuit/gadget/ecc/chip/add.rs
index 555645b6..0ae7f094 100644
--- a/src/circuit/gadget/ecc/chip/add.rs
+++ b/src/circuit/gadget/ecc/chip/add.rs
@@ -409,13 +409,13 @@ pub mod tests {
         // Check complete addition P + (-P)
         {
             let result = p.add(layouter.namespace(|| "P + (-P)"), p_neg)?;
-            result.constrain_equal(layouter.namespace(|| "P + (-P) = 0"), zero)?;
+            result.constrain_equal(layouter.namespace(|| "P + (-P) = 𝒪"), zero)?;
         }
 
         // Check complete addition 𝒪 + 𝒪
         {
             let result = zero.add(layouter.namespace(|| "𝒪 + 𝒪"), zero)?;
-            result.constrain_equal(layouter.namespace(|| "P + (-P) = 0"), zero)?;
+            result.constrain_equal(layouter.namespace(|| "𝒪 + 𝒪 = 𝒪"), zero)?;
         }
 
         // Check P + Q
diff --git a/src/circuit/gadget/ecc/chip/add_incomplete.rs b/src/circuit/gadget/ecc/chip/add_incomplete.rs
index bfeae528..8877bba8 100644
--- a/src/circuit/gadget/ecc/chip/add_incomplete.rs
+++ b/src/circuit/gadget/ecc/chip/add_incomplete.rs
@@ -53,7 +53,7 @@ impl Config {
                 (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_p.clone() - y_q.clone()).square()
             };
 
             // (y_r + y_q)(x_p − x_q) − (y_p − y_q)(x_q − x_r) = 0
@@ -143,22 +143,35 @@ impl Config {
 
 #[cfg(test)]
 pub mod tests {
-    use halo2::{arithmetic::CurveAffine, circuit::Layouter, plonk::Error};
+    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<
-        C: CurveAffine,
-        EccChip: EccInstructions<C> + Clone + Eq + std::fmt::Debug,
+        EccChip: EccInstructions<pallas::Affine> + Clone + Eq + std::fmt::Debug,
     >(
-        mut layouter: impl Layouter<C::Base>,
-        zero: &Point<C, EccChip>,
-        p: &Point<C, EccChip>,
-        q: &Point<C, EccChip>,
-        p_neg: &Point<C, EccChip>,
+        chip: EccChip,
+        mut layouter: impl Layouter<pallas::Base>,
+        zero: &Point<pallas::Affine, EccChip>,
+        p_val: pallas::Affine,
+        p: &Point<pallas::Affine, EccChip>,
+        q_val: pallas::Affine,
+        q: &Point<pallas::Affine, EccChip>,
+        p_neg: &Point<pallas::Affine, EccChip>,
     ) -> Result<(), Error> {
         // P + Q
-        p.add_incomplete(layouter.namespace(|| "P + Q"), 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)
diff --git a/src/circuit/gadget/ecc/chip/witness_point.rs b/src/circuit/gadget/ecc/chip/witness_point.rs
index 33bef835..c9267963 100644
--- a/src/circuit/gadget/ecc/chip/witness_point.rs
+++ b/src/circuit/gadget/ecc/chip/witness_point.rs
@@ -40,8 +40,8 @@ impl Config {
             let y = meta.query_advice(self.y, Rotation::cur());
 
             // y^2 = x^3 + b
-            let curve_eqn = y.clone() * y.clone()
-                - (x.clone() * x.clone() * x.clone())
+            let curve_eqn = y.clone().square()
+                - (x.clone().square() * x.clone())
                 - Expression::Constant(pallas::Affine::b());
 
             vec![