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] 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();