From 0265d8f1dc5f8deaf80542b30b4baf048ae8ac75 Mon Sep 17 00:00:00 2001 From: Pratyush Mishra Date: Thu, 21 Dec 2023 18:03:19 -0800 Subject: [PATCH] Add explanation for why booleanity check can be avoided --- src/fields/fp/mod.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/fields/fp/mod.rs b/src/fields/fp/mod.rs index 6dfe427e..bd955bd7 100644 --- a/src/fields/fp/mod.rs +++ b/src/fields/fp/mod.rs @@ -332,7 +332,8 @@ impl AllocatedFp { /// This requires two constraints. #[tracing::instrument(target = "r1cs")] pub fn is_neq(&self, other: &Self) -> Result, SynthesisError> { - // We don't need to enforce `is_not_equal` to be boolean here + // 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()?), @@ -384,6 +385,11 @@ impl AllocatedFp { // constraint 1: // (self - other) * multiplier = is_not_equal // 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,