Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for linear constraints #83

Open
adr1anh opened this issue Feb 14, 2024 · 1 comment
Open

Support for linear constraints #83

adr1anh opened this issue Feb 14, 2024 · 1 comment

Comments

@adr1anh
Copy link

adr1anh commented Feb 14, 2024

When folding an R1CS circuit, the cross-term computation
$$T = AZ_1 ◦ BZ_2 + AZ_2 ◦ BZ_1 − u_1CZ_2 − u_2CZ_1$$
can be computed more efficiently when the circuit takes advantage of linear constraints of the form:
$$0=\sum_i C_{i,j} \cdot z_i.$$
Specifically, this corresponds to a constraint where the linear combinations in the rows $A_j, B_j$ are equal to zero.
If this is the case, then the $j$-th component of $T$ will always be equal to zero, and the computation for the $j$-th constraint can be avoided entirely.
Moreover, the computation of the commitment to $T$ can also be optimized to skip the entries corresponding to linear constraints.

In order to encourage the use of linear constraints, I propose adding the two following methods to the ConstraintSystem trait.

 /// Enforce that `A` = 0. The `annotation` function is invoked in testing contexts
 /// in order to derive a unique name for the constraint in the current namespace.
 fn enforce_eq_zero<A, AR, LA>(&mut self, annotation: A, a: LA)
   where
       A: FnOnce() -> AR,
       AR: Into<String>,
       LA: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar> {
   self.enforce(annotation, |_| LinearCombination::zero(), |_| LinearCombination::zero(), a);
 }

 /// Enforce that `A` = `B`. The `annotation` function is invoked in testing contexts
 /// in order to derive a unique name for the constraint in the current namespace.
 fn enforce_eq<A, AR, LA, LB>(&mut self, annotation: A, a: LA, b: LB)
   where
       A: FnOnce() -> AR,
       AR: Into<String>,
       LA: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar>,
       LB: FnOnce(LinearCombination<Scalar>) -> LinearCombination<Scalar> {
   let zero = a(LinearCombination::zero()) - b(LinearCombination::zero());
   self.enforce_eq_zero(annotation, |_| zero);
 }

Both of these functions can have default implementation defined in terms of the existing enforce function definition, avoiding backwards-compatibility issues. However, it allows folding-specific ConstraintSystems to choose to handle linear constraints differently.

@Sh0g0-1758
Copy link

Hey, @adr1anh, I have been looking into Bellpepper recently and I would like to work on this If no one has started yet. Do you guys assign the issue or do I just link a patch here?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants