Skip to content
Merged
Show file tree
Hide file tree
Changes from 5 commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ resolver = "2"
ark-ff = { version = "0.5.0", default-features = false }
ark-ec = { version = "0.5.0", default-features = false }
ark-std = { version = "0.5.0", default-features = false }
ark-relations = { version = "0.5.0", default-features = false }
ark-relations = { git = "https://github.com/arkworks-rs/snark.git", default-features = true }

educe = "0.6.0"
tracing = { version = "^0.1.0", default-features = false, features = ["attributes"] }
Expand Down Expand Up @@ -84,5 +84,8 @@ unexpected_cfgs = { level = "warn", check-cfg = ['cfg(ci)'] }


# patch
[patch.crates-io]
ark-relations = { git = "https://github.com/arkworks-rs/snark.git", default-features = true }
# [patch.crates-io]
# ark-relations = { path = "../snark/relations", default-features = true }

# [patch."https://github.com/arkworks-rs/snark.git"]
# ark-relations = { path = "../snark/relations", default-features = true }
Comment on lines 86 to +91

Copilot AI Jun 12, 2025

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[nitpick] There are commented-out [patch.crates-io] sections that look obsolete. Consider removing or updating these entries to keep the manifest clean and avoid confusion.

Copilot uses AI. Check for mistakes.
44 changes: 27 additions & 17 deletions src/boolean/allocated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ impl<F: Field> AllocatedBool<F> {
/// an `AllocatedBool`.
#[tracing::instrument(target = "gr1cs")]
pub fn not(&self) -> Result<Self, SynthesisError> {
let variable = self.cs.new_lc(lc!() + Variable::One - self.variable)?;
let variable = self.cs.new_lc(|| lc_diff![Variable::One, self.variable])?;
Ok(Self {
variable,
cs: self.cs.clone(),
Expand Down Expand Up @@ -90,9 +90,15 @@ impl<F: Field> AllocatedBool<F> {
// 2a * b = a + b - c
// (a + a) * b = a + b - c
self.cs.enforce_r1cs_constraint(
lc!() + self.variable + self.variable,
lc!() + b.variable,
lc!() + self.variable + b.variable - result.variable,
|| (F::ONE.double(), self.variable).into(),
|| b.variable.into(),
|| {
lc![
(F::ONE, self.variable),
(F::ONE, b.variable),
(-F::ONE, result.variable),
]
},
)?;

Ok(result)
Expand All @@ -109,9 +115,9 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (a) * (b) = (c), ensuring c is 1 iff
// a AND b are both 1.
self.cs.enforce_r1cs_constraint(
lc!() + self.variable,
lc!() + b.variable,
lc!() + result.variable,
|| self.variable.into(),
|| b.variable.into(),
|| result.variable.into(),
)?;

Ok(result)
Expand All @@ -128,9 +134,9 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (1 - a) * (1 - b) = (1 - c), ensuring c is 0 iff
// a and b are both false, and otherwise c is 1.
self.cs.enforce_r1cs_constraint(
lc!() + Variable::One - self.variable,
lc!() + Variable::One - b.variable,
lc!() + Variable::One - result.variable,
|| lc_diff![Variable::One, self.variable],
|| lc_diff![Variable::One, b.variable],
|| lc_diff![Variable::One, result.variable],
)?;

Ok(result)
Expand All @@ -146,9 +152,9 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (a) * (1 - b) = (c), ensuring c is 1 iff
// a is true and b is false, and otherwise c is 0.
self.cs.enforce_r1cs_constraint(
lc!() + self.variable,
lc!() + Variable::One - b.variable,
lc!() + result.variable,
|| lc!() + self.variable,
|| lc_diff![Variable::One, b.variable],
|| lc!() + result.variable,
)?;

Ok(result)
Expand All @@ -164,9 +170,9 @@ impl<F: Field> AllocatedBool<F> {
// Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
// a and b are both false, and otherwise c is 0.
self.cs.enforce_r1cs_constraint(
lc!() + Variable::One - self.variable,
lc!() + Variable::One - b.variable,
lc!() + result.variable,
|| lc_diff![Variable::One, self.variable],
|| lc_diff![Variable::One, b.variable],
|| result.variable.into(),
)?;

Ok(result)
Expand Down Expand Up @@ -210,7 +216,11 @@ impl<F: Field> AllocVar<bool, F> for AllocatedBool<F> {
// Constrain: (1 - a) * a = 0
// This constrains a to be either 0 or 1.

cs.enforce_r1cs_constraint(lc!() + Variable::One - variable, lc!() + variable, lc!())?;
cs.enforce_r1cs_constraint(
|| lc_diff![Variable::One, variable],
|| variable.into(),
|| lc!(),
)?;

Ok(Self {
variable,
Expand Down
77 changes: 48 additions & 29 deletions src/boolean/eq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,22 +27,32 @@ impl<F: Field> EqGadget<F> for Boolean<F> {
// We will use the following trick: a == b <=> a - b == 0
// This works because a - b == 0 if and only if a = 0 and b = 0, or a = 1 and b
// = 1, which is exactly the definition of a == b.
let difference = match (self, other) {
// 1 == 1; 0 == 0
(Constant(true), Constant(true)) | (Constant(false), Constant(false)) => return Ok(()),
// false != true
(Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
// 1 - a
(Constant(true), Var(a)) | (Var(a), Constant(true)) => lc!() + one - a.variable(),
// a - 0 = a
(Constant(false), Var(a)) | (Var(a), Constant(false)) => lc!() + a.variable(),
// b - a,
(Var(a), Var(b)) => lc!() + b.variable() - a.variable(),
};

if condition != &Constant(false) {
let cs = self.cs().or(other.cs()).or(condition.cs());
cs.enforce_r1cs_constraint(lc!() + difference, condition.lc(), lc!())?;
match (self, other) {
// 1 == 1; 0 == 0
(Constant(true), Constant(true)) | (Constant(false), Constant(false)) => {
return Ok(())
},
// false != true
(Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
// handled below
(_, _) => (),
};
let difference = || match (self, other) {
// 1 - a
(Constant(true), Var(a)) | (Var(a), Constant(true)) => {
lc_diff![one, a.variable()]
},
// a - 0 = a
(Constant(false), Var(a)) | (Var(a), Constant(false)) => a.variable().into(),
// b - a,
(Var(a), Var(b)) => lc_diff![b.variable(), a.variable()],
// handled above
(_, _) => unreachable!(),
};
cs.enforce_r1cs_constraint(difference, || condition.lc(), || lc!())?;
}
Ok(())
}
Expand All @@ -55,25 +65,34 @@ impl<F: Field> EqGadget<F> for Boolean<F> {
) -> Result<(), SynthesisError> {
use Boolean::*;
let one = Variable::One;
// We will use the following trick: a != b <=> a + b == 1
// This works because a + b == 1 if and only if a = 0 and b = 1, or a = 1 and b
// = 0, which is exactly the definition of a != b.
let sum = match (self, other) {
// 1 != 0; 0 != 1
(Constant(true), Constant(false)) | (Constant(false), Constant(true)) => return Ok(()),
// false == false and true == true
(Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
// 1 + a
(Constant(true), Var(a)) | (Var(a), Constant(true)) => lc!() + one + a.variable(),
// a + 0 = a
(Constant(false), Var(a)) | (Var(a), Constant(false)) => lc!() + a.variable(),
// b + a,
(Var(a), Var(b)) => lc!() + b.variable() + a.variable(),
};

if should_enforce != &Constant(false) {
let cs = self.cs().or(other.cs()).or(should_enforce.cs());
cs.enforce_r1cs_constraint(sum, should_enforce.lc(), lc!() + one)?;
// We will use the following trick: a != b <=> a + b == 1
// This works because a + b == 1 if and only if a = 0 and b = 1, or a = 1 and b
// = 0, which is exactly the definition of a != b.
match (self, other) {
// 1 != 0; 0 != 1
(Constant(true), Constant(false)) | (Constant(false), Constant(true)) => {
return Ok(())
},
// false == false and true == true
(Constant(_), Constant(_)) => return Err(SynthesisError::Unsatisfiable),
(_, _) => (),
}
let sum = || match (self, other) {
// 1 + a
(Constant(true), Var(a)) | (Var(a), Constant(true)) => {
lc![one, a.variable()]
},
// a + 0 = a
(Constant(false), Var(a)) | (Var(a), Constant(false)) => a.variable().into(),
// b + a,
(Var(a), Var(b)) => lc![b.variable(), a.variable()],
// handled above
(_, _) => unreachable!(),
};
cs.enforce_r1cs_constraint(sum, || should_enforce.lc(), || one.into())?;
}
Ok(())
}
Expand Down
16 changes: 15 additions & 1 deletion src/boolean/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -120,11 +120,25 @@ impl<F: Field> Boolean<F> {
pub fn lc(&self) -> LinearCombination<F> {
match self {
&Boolean::Constant(false) => lc!(),
&Boolean::Constant(true) => lc!() + Variable::One,
&Boolean::Constant(true) => Variable::One.into(),
Boolean::Var(v) => v.variable().into(),
}
}

/// Constructs a `Variable` from `Self`'s variables according
/// to the following map.
///
/// * `Boolean::TRUE => Variable::One`
/// * `Boolean::FALSE => Variable::Zero``
/// * `Boolean::Var(v) => v.variable()`
pub fn variable(&self) -> Variable {
match self {
&Boolean::Constant(false) => Variable::Zero,
&Boolean::Constant(true) => Variable::One,
Boolean::Var(v) => v.variable(),
}
}

/// Convert a little-endian bitwise representation of a field element to
/// `FpVar<F>`
///
Expand Down
6 changes: 3 additions & 3 deletions src/boolean/select.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,9 +79,9 @@ impl<F: PrimeField> CondSelectGadget<F> for Boolean<F> {
// 1 | 0 | 0 | 0
// 1 | 1 | 0 | 1
cs.enforce_r1cs_constraint(
cond.lc(),
lc!() + a.lc() - b.lc(),
lc!() + result.lc() - b.lc(),
|| cond.lc(),
|| lc_diff![a.variable(), b.variable()],
|| lc_diff![result.variable(), b.variable()],
)?;

Ok(result)
Expand Down
7 changes: 4 additions & 3 deletions src/eq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -124,10 +124,11 @@ impl<T: EqGadget<F> + GR1CSVar<F>, F: PrimeField> EqGadget<F> for [T] {
Ok(())
} else {
let cs = [&some_are_different, should_enforce].cs();
let should_enforce = cs.new_lc(|| should_enforce.lc())?;
Comment thread
Pratyush marked this conversation as resolved.
Outdated
cs.enforce_r1cs_constraint(
some_are_different.lc(),
should_enforce.lc(),
should_enforce.lc(),
|| some_are_different.lc(),
|| should_enforce.into(),
|| should_enforce.into(),
)
}
}
Expand Down
Loading