arnaucube/ark-r1cs-std
1
0
Fork 0
mirror of https://github.com/arnaucube/ark-r1cs-std.git synced 2026-01-08 15:01:29 +01:00
Code Issues Projects Releases Wiki Activity

FpVar::{is_eq, is_neq} only need two constraints (#133)

Browse Source 
Co-authored-by: Pratyush Mishra <pratyush795@gmail.com>
This commit is contained in:
winderica
2023-12-29 02:40:12 +08:00
committed by GitHub
parent ed2d55e6ff
commit 3cb9fdef00
3 changed files with 21 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
CHANGELOG.md
View File

@@ -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

2
src/bits/boolean.rs
View File

@@ -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> {

32
src/fields/fp/mod.rs
View File

@@ -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,