From 3cb9fdef00e4abf15df73ff35578f6671e568e9a Mon Sep 17 00:00:00 2001
From: winderica <winderica@gmail.com>
Date: Fri, 29 Dec 2023 02:40:12 +0800
Subject: [PATCH] `FpVar::{is_eq, is_neq}` only need two constraints (#133)

Co-authored-by: Pratyush Mishra <pratyush795@gmail.com>
---
 CHANGELOG.md         |  1 +
 src/bits/boolean.rs  |  2 +-
 src/fields/fp/mod.rs | 32 +++++++++++++++++++-------------
 3 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a31ffb83..2397f878 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,7 @@
 - [\#117](https://github.com/arkworks-rs/r1cs-std/pull/117) Fix result of `precomputed_base_scalar_mul_le` to not discard previous value.
 - [\#124](https://github.com/arkworks-rs/r1cs-std/pull/124) Fix `scalar_mul_le` constraints unsatisfiability when short Weierstrass point is zero.
 - [\#127](https://github.com/arkworks-rs/r1cs-std/pull/127) Convert `NonNativeFieldVar` constants to little-endian bytes instead of big-endian (`ToBytesGadget`).
+- [\#133](https://github.com/arkworks-rs/r1cs-std/pull/133) Save 1 constraint in `FpVar::{is_eq, is_neq}` by removing the unnecessary booleanity check.
 
 ### Breaking changes
 
diff --git a/src/bits/boolean.rs b/src/bits/boolean.rs
index a892aea0..9f0be047 100644
--- a/src/bits/boolean.rs
+++ b/src/bits/boolean.rs
@@ -46,7 +46,7 @@ impl<F: Field> AllocatedBool<F> {
     }
 
     /// Allocate a witness variable without a booleanity check.
-    fn new_witness_without_booleanity_check<T: Borrow<bool>>(
+    pub(crate) fn new_witness_without_booleanity_check<T: Borrow<bool>>(
         cs: ConstraintSystemRef<F>,
         f: impl FnOnce() -> Result<T, SynthesisError>,
     ) -> Result<Self, SynthesisError> {
diff --git a/src/fields/fp/mod.rs b/src/fields/fp/mod.rs
index 8241aa60..bd955bd7 100644
--- a/src/fields/fp/mod.rs
+++ b/src/fields/fp/mod.rs
@@ -6,6 +6,7 @@ use ark_relations::r1cs::{
 use core::borrow::Borrow;
 
 use crate::{
+    boolean::AllocatedBool,
     fields::{FieldOpsBounds, FieldVar},
     prelude::*,
     Assignment, ToConstraintFieldGadget, Vec,
@@ -320,7 +321,7 @@ impl<F: PrimeField> AllocatedFp<F> {
 
     /// Outputs the bit `self == other`.
     ///
-    /// This requires three constraints.
+    /// This requires two constraints.
     #[tracing::instrument(target = "r1cs")]
     pub fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
         Ok(self.is_neq(other)?.not())
@@ -328,12 +329,15 @@ impl<F: PrimeField> AllocatedFp<F> {
 
     /// Outputs the bit `self != other`.
     ///
-    /// This requires three constraints.
+    /// This requires two constraints.
     #[tracing::instrument(target = "r1cs")]
     pub fn is_neq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
-        let is_not_equal = Boolean::new_witness(self.cs.clone(), || {
-            Ok(self.value.get()? != other.value.get()?)
-        })?;
+        // We don't need to enforce `is_not_equal` to be boolean here;
+        // see the comments above the constraints below for why.
+        let is_not_equal = Boolean::from(AllocatedBool::new_witness_without_booleanity_check(
+            self.cs.clone(),
+            || Ok(self.value.get()? != other.value.get()?),
+        )?);
         let multiplier = self.cs.new_witness_variable(|| {
             if is_not_equal.value()? {
                 (self.value.get()? - other.value.get()?).inverse().get()
@@ -369,21 +373,23 @@ impl<F: PrimeField> AllocatedFp<F> {
         // --------------------------------------------------------------------
         //
         // Soundness:
-        // Case 1: self != other, but is_not_equal = 0.
+        // Case 1: self != other, but is_not_equal != 1.
         // --------------------------------------------
-        //   constraint 1:
-        //   (self - other) * multiplier = is_not_equal
-        //   => non_zero * multiplier = 0 (only satisfiable if multiplier == 0)
-        //
         //   constraint 2:
         //   (self - other) * not(is_not_equal) = 0
-        //   => (non_zero) * 1 = 0 (impossible)
+        //   => (non_zero) * (1 - is_not_equal) = 0
+        //   => non_zero = 0 (contradiction) || 1 - is_not_equal = 0 (contradiction)
         //
-        // Case 2: self == other, but is_not_equal = 1.
+        // Case 2: self == other, but is_not_equal != 0.
         // --------------------------------------------
         //   constraint 1:
         //   (self - other) * multiplier = is_not_equal
-        //   0 * multiplier = 1 (unsatisfiable)
+        //   0 * multiplier = is_not_equal != 0 (unsatisfiable)
+        //
+        // That is, constraint 1 enforces that if self == other, then `is_not_equal = 0`
+        // and constraint 2 enforces that if self != other, then `is_not_equal = 1`.
+        // Since these are the only possible two cases, `is_not_equal` is always
+        // constrained to 0 or 1.
         self.cs.enforce_constraint(
             lc!() + self.variable - other.variable,
             lc!() + multiplier,