Optimize field (in)equality circuit.

To calculate `z = x != y`, instead of
```
(z) (1 - z) = (0)
(x - y) (w) = (z)
(x - y) (1 - z) = (0)
```
(where `w` is an internal variable) we just need
```
(x - y) (w) = (z)
(x - y) (1 - z) = (0)
```
i.e. just the 2nd and 3rd constraints, because they imply the 1st one. So we
save one constraint for every field (in)equality.

This optimization has been already verified in the ACL2 theorem prover.

To avoid generating the boolean constraint, we need to avoid `Boolean::new`, and
instead generate the `Boolean` directly, as in boolean AND for example.
However, boolean AND has access to the private `LinearCombination` component of
`Boolean`, while field (in)equality does not. So I've added a `from_variable`
constructor to `Boolean`, but if there is a better or more desirable approach,
we can revise this part.

circuit/types/boolean/src/lib.rs

@@ -39,6 +39,13 @@ pub struct Boolean<E: Environment>(LinearCombination<E::BaseField>);
 
 impl<E: Environment> BooleanTrait for Boolean<E> {}
 
+impl<E: Environment> Boolean<E> {
+    /// Initializes a boolean from a variable.
+    pub fn from_variable(var: Variable<E::BaseField>) -> Self {
+        Boolean(var.into())
+    }
+}
+
 #[cfg(console)]
 impl<E: Environment> Inject for Boolean<E> {
     type Primitive = bool;

circuit/types/field/src/equal.rs

@@ -13,14 +13,15 @@
 // limitations under the License.
 
 use super::*;
+use snarkvm_circuit_environment::Private;
 
 impl<E: Environment> Equal<Self> for Field<E> {
     type Output = Boolean<E>;
 
     ///
     /// Returns `true` if `self` and `other` are equal.
     ///
-    /// This method costs 3 constraints.
+    /// This method costs 2 constraints.
     ///
     fn is_equal(&self, other: &Self) -> Self::Output {
         !self.is_not_equal(other)
@@ -32,24 +33,41 @@ impl<E: Environment> Equal<Self> for Field<E> {
     /// This method constructs a boolean that indicates if
     /// `self` and `other ` are *not* equal to each other.
     ///
-    /// This method costs 3 constraints.
+    /// This method costs 2 constraints.
     ///
     fn is_not_equal(&self, other: &Self) -> Self::Output {
+        // In all cases, the witness ("ejected") value is calculated from the ejected values.
+        let is_neq_ejected = self.eject_value() != other.eject_value();
+
         match (self.is_constant(), other.is_constant()) {
-            (true, true) => witness!(|self, other| self != other),
+            // If both operands are constant, the result is also constant.
+            (true, true) => Boolean::new(Mode::Constant, is_neq_ejected),
+
+            // Otherwise, we introduce a private field variable is_neq for the result,
+            // along with an auxiliary variable multiplier for the inverse of the difference between the operands,
+            // and enforce the following constraints:
+            //   (self - other) (multiplier) = (is_neq)
+            //   (self - other) (1 - is_neq) = (0)
+            // These constraints imply that is_neq is boolean, i.e. either 0 or 1;
+            // so we avoid creating is_neq as a Boolean, which would generate an unneeded boolean constraint.
+            // See the comments just after the code for more detailed explanations.
             _ => {
-                // Compute a boolean that is `true` if `this` and `that` are not equivalent.
-                let is_neq: Boolean<E> = witness!(|self, other| self != other);
-
-                // Assign the expected multiplier.
-                let multiplier: Field<E> = witness!(|self, other| {
-                    match (self - other).inverse() {
+                let is_neq = Boolean::from_variable(E::new_variable(Mode::Private, match is_neq_ejected {
+                    true => E::BaseField::one(),
+                    false => E::BaseField::zero(),
+                }));
+                let delta = self - other;
+                let multiplier: Field<E> = witness!(|delta| {
+                    match delta.inverse() {
                         Ok(inverse) => inverse,
-                        _ => console::Field::one(),
+                        _ => console::Field::one(), // exact value is irrelevant, because (0) (anything) = (0)
                     }
                 });
+                let is_eq = !is_neq.clone(); // 1 - is_neq
+                E::enforce(|| (&delta, &multiplier, &is_neq)); // 1st constraint
+                E::enforce(|| (delta, is_eq, E::zero())); // 2nd constraint
+                is_neq
 
-                //
                 // Inequality Enforcement
                 // ----------------------------------------------------------------
                 // Check 1:  (a - b) * multiplier = is_neq
@@ -110,21 +128,6 @@ impl<E: Environment> Equal<Self> for Field<E> {
                 // Check 2:  (a - b) * not(1) = 0
                 //                          0 = 0
                 // => is_neq is trivially correct.
-                //
-
-                // Compute `self` - `other`.
-                let delta = self - other;
-
-                // Negate `is_neq`.
-                let is_eq = !is_neq.clone();
-
-                // Check 1: (a - b) * multiplier = is_neq
-                E::enforce(|| (&delta, &multiplier, &is_neq));
-
-                // Check 2: (a - b) * not(is_neq) = 0
-                E::enforce(|| (delta, is_eq, E::zero()));
-
-                is_neq
             }
         }
     }
@@ -137,7 +140,7 @@ impl<E: Environment> Metrics<dyn Equal<Field<E>, Output = Boolean<E>>> for Field
     fn count(case: &Self::Case) -> Count {
         match case {
             (Mode::Constant, Mode::Constant) => Count::is(1, 0, 0, 0),
-            _ => Count::is(0, 0, 2, 3),
+            _ => Count::is(0, 0, 2, 2),
         }
     }
 }