Support for linear constraints

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=\sumi 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.

argumentcomputer / bellpepper

Support for linear constraints #83