From 41ebf1db3db6d98bc8d587b8baeaf736db71caf2 Mon Sep 17 00:00:00 2001 From: Alessandro Coglio Date: Sat, 7 Oct 2023 21:49:35 -0700 Subject: [PATCH] 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 | 7 ++++ circuit/types/field/src/equal.rs | 57 +++++++++++++++++--------------- 2 files changed, 37 insertions(+), 27 deletions(-) diff --git a/circuit/types/boolean/src/lib.rs b/circuit/types/boolean/src/lib.rs index 292698cd5e..f2e9a7814a 100644 --- a/circuit/types/boolean/src/lib.rs +++ b/circuit/types/boolean/src/lib.rs @@ -39,6 +39,13 @@ pub struct Boolean(LinearCombination); impl BooleanTrait for Boolean {} +impl Boolean { + /// Initializes a boolean from a variable. + pub fn from_variable(var: Variable) -> Self { + Boolean(var.into()) + } +} + #[cfg(console)] impl Inject for Boolean { type Primitive = bool; diff --git a/circuit/types/field/src/equal.rs b/circuit/types/field/src/equal.rs index 38693b7add..e463c07a8d 100644 --- a/circuit/types/field/src/equal.rs +++ b/circuit/types/field/src/equal.rs @@ -13,6 +13,7 @@ // limitations under the License. use super::*; +use snarkvm_circuit_environment::Private; impl Equal for Field { type Output = Boolean; @@ -20,7 +21,7 @@ impl Equal for Field { /// /// 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 Equal for Field { /// 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 = witness!(|self, other| self != other); - - // Assign the expected multiplier. - let multiplier: Field = 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 = 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 Equal for Field { // 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 Metrics, Output = Boolean>> 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), } } }