Make the IR1CS optimizer more aggressive

Previously, we would eliminate only final-round witnesses. This is
obviously sound, but sub-optimal.

Anna has found some protocols (SHA with lookups) where the
sub-optimality matters, so I've made the optimizer a bit more
aggressive.

Author: alex-ozdemir

src/target/r1cs/mod.rs

@@ -370,6 +370,37 @@ impl R1cs {
         matches!(var.ty(), VarType::FinalWit)
     }
 
+    /// Can this variable be eliminated within this constraint?
+    ///
+    /// A witness variable can be eliminated iff it is in the *last* round of its constraint.
+    /// We only approximate this.
+    /// We elim if:
+    /// 1) this is a final wit or
+    /// 2) this is a wit with only other wits and insts and it is the last wit
+    ///
+    /// This is an approximation because we comparse witness numbers in (2) instead of witness
+    /// rounds. So, we under-approximate the set of eliminatable variables.
+    pub fn can_eliminate_in(&self, var: Var, constraint: &Lc) -> bool {
+        match var.ty() {
+            VarType::FinalWit => true,
+            VarType::Inst | VarType::Chall | VarType::CWit => false,
+            VarType::RoundWit => {
+                for v in constraint.monomials.keys() {
+                    match v.ty() {
+                        VarType::Inst | VarType::CWit => {}
+                        VarType::Chall | VarType::FinalWit => return false,
+                        VarType::RoundWit => {
+                            if v.number() > var.number() {
+                                return false;
+                            }
+                        }
+                    }
+                }
+                true
+            }
+        }
+    }
+
     /// Get a nice string represenation of the tuple.
     pub fn format_qeq(&self, (a, b, c): &(Lc, Lc, Lc)) -> String {
         format!(

src/target/r1cs/opt.rs

@@ -177,7 +177,7 @@ impl LinReducer {
 fn as_linear_sub((a, b, c): &(Lc, Lc, Lc), r1cs: &R1cs) -> Option<(Var, Lc)> {
     if a.is_zero() || b.is_zero() {
         for i in c.monomials.keys() {
-            if r1cs.can_eliminate(*i) {
+            if r1cs.can_eliminate_in(*i, c) {
                 let mut lc = c.clone();
                 let v = lc.monomials.remove(i).unwrap();
                 lc *= v.recip();