More explicit R1CS tests/examples (#358)

Author: mmagician

relations/src/r1cs/constraint_system.rs

@@ -639,7 +639,7 @@ impl<F: Field> ConstraintSystem<F> {
                     self.lc_assignment_cache.borrow_mut().insert(idx, value);
                     Some(value)
                 }
-            }
+            },
         }
     }
 }
@@ -1053,4 +1053,119 @@ mod tests {
         assert_eq!(matrices.c[2], vec![(two, 1), (two, 2)]);
         Ok(())
     }
+
+    #[test]
+    fn matrix_generation_outlined() -> crate::r1cs::Result<()> {
+        let cs = ConstraintSystem::<Fr>::new_ref();
+        cs.set_optimization_goal(OptimizationGoal::Weight);
+        let two = Fr::one() + Fr::one();
+        let a = cs.new_input_variable(|| Ok(Fr::one()))?;
+        let b = cs.new_witness_variable(|| Ok(Fr::one()))?;
+        let c = cs.new_witness_variable(|| Ok(two))?;
+        cs.enforce_constraint(lc!() + a, lc!() + (two, b), lc!() + c)?;
+
+        let d = cs.new_lc(lc!() + a + b)?;
+        cs.enforce_constraint(lc!() + a, lc!() + d, lc!() + d)?;
+
+        let e = cs.new_lc(lc!() + d + d)?;
+        cs.enforce_constraint(lc!() + Variable::One, lc!() + e, lc!() + e)?;
+
+        cs.finalize();
+        assert!(cs.is_satisfied().is_ok());
+        let matrices = cs.to_matrices().unwrap();
+        assert_eq!(matrices.a[0], vec![(Fr::one(), 1)]);
+        assert_eq!(matrices.b[0], vec![(two, 2)]);
+        assert_eq!(matrices.c[0], vec![(Fr::one(), 3)]);
+
+        assert_eq!(matrices.a[1], vec![(Fr::one(), 1)]);
+        // Notice here how the variable allocated for d is outlined
+        // compared to the example in previous test case.
+        // We are optimising for weight: there are less non-zero elements.
+        assert_eq!(matrices.b[1], vec![(Fr::one(), 4)]);
+        assert_eq!(matrices.c[1], vec![(Fr::one(), 4)]);
+
+        assert_eq!(matrices.a[2], vec![(Fr::one(), 0)]);
+        assert_eq!(matrices.b[2], vec![(two, 4)]);
+        assert_eq!(matrices.c[2], vec![(two, 4)]);
+        Ok(())
+    }
+
+    /// Example meant to follow as closely as possible the excellent R1CS
+    /// write-up by [Vitalik Buterin](https://vitalik.ca/general/2016/12/10/qap.html)
+    /// and demonstrate how to construct such matrices in arkworks.
+    #[test]
+    fn matrix_generation_example() -> crate::r1cs::Result<()> {
+        let cs = ConstraintSystem::<Fr>::new_ref();
+        // helper definitions
+        let three = Fr::from(3u8);
+        let five = Fr::from(5u8);
+        let nine = Fr::from(9u8);
+        // There will be six variables in the system, in the order governed by adding
+        // them to the constraint system (Note that the CS is initialised with
+        // `Variable::One` in the first position implicitly).
+        // Note also that the all public variables will always be placed before all witnesses
+        //
+        // Variable::One
+        // Variable::Instance(5)
+        // Variable::Witness(3) ( == x )
+        // Variable::Witness(9) ( == sym_1 )
+        // Variable::Witness(27) ( == y )
+        // Variable::Witness(30) ( == y )
+
+        // let one = Variable::One; // public input, implicitly defined
+        let out = cs.new_input_variable(|| Ok(nine * three + three + five))?; // public input
+        let x = cs.new_witness_variable(|| Ok(three))?; // explicit witness
+        let sym_1 = cs.new_witness_variable(|| Ok(nine))?; // intermediate witness variable
+        let y = cs.new_witness_variable(|| Ok(nine * three))?; // intermediate witness variable
+        let sym_2 = cs.new_witness_variable(|| Ok(nine * three + three))?; // intermediate witness variable
+
+        cs.enforce_constraint(lc!() + x, lc!() + x, lc!() + sym_1)?;
+        cs.enforce_constraint(lc!() + sym_1, lc!() + x, lc!() + y)?;
+        cs.enforce_constraint(lc!() + y + x, lc!() + Variable::One, lc!() + sym_2)?;
+        cs.enforce_constraint(
+            lc!() + sym_2 + (five, Variable::One),
+            lc!() + Variable::One,
+            lc!() + out,
+        )?;
+
+        cs.finalize();
+        assert!(cs.is_satisfied().is_ok());
+        let matrices = cs.to_matrices().unwrap();
+        // There are four gates(constraints), each generating a row.
+        // Resulting matrices:
+        // (Note how 2nd & 3rd columns are swapped compared to the online example.
+        // This results from an implementation detail of placing all Variable::Instances(_) first.
+        //
+        // A
+        // [0, 0, 1, 0, 0, 0]
+        // [0, 0, 0, 1, 0, 0]
+        // [0, 0, 1, 0, 1, 0]
+        // [5, 0, 0, 0, 0, 1]
+        // B
+        // [0, 0, 1, 0, 0, 0]
+        // [0, 0, 1, 0, 0, 0]
+        // [1, 0, 0, 0, 0, 0]
+        // [1, 0, 0, 0, 0, 0]
+        // C
+        // [0, 0, 0, 1, 0, 0]
+        // [0, 0, 0, 0, 1, 0]
+        // [0, 0, 0, 0, 0, 1]
+        // [0, 1, 0, 0, 0, 0]
+        assert_eq!(matrices.a[0], vec![(Fr::one(), 2)]);
+        assert_eq!(matrices.b[0], vec![(Fr::one(), 2)]);
+        assert_eq!(matrices.c[0], vec![(Fr::one(), 3)]);
+
+        assert_eq!(matrices.a[1], vec![(Fr::one(), 3)]);
+        assert_eq!(matrices.b[1], vec![(Fr::one(), 2)]);
+        assert_eq!(matrices.c[1], vec![(Fr::one(), 4)]);
+
+        assert_eq!(matrices.a[2], vec![(Fr::one(), 2), (Fr::one(), 4)]);
+        assert_eq!(matrices.b[2], vec![(Fr::one(), 0)]);
+        assert_eq!(matrices.c[2], vec![(Fr::one(), 5)]);
+
+        assert_eq!(matrices.a[3], vec![(five, 0), (Fr::one(), 5)]);
+        assert_eq!(matrices.b[3], vec![(Fr::one(), 0)]);
+        assert_eq!(matrices.c[3], vec![(Fr::one(), 1)]);
+        Ok(())
+    }
 }

relations/src/r1cs/error.rs

@@ -31,17 +31,17 @@ impl fmt::Display for SynthesisError {
             SynthesisError::MissingCS => write!(f, "the constraint system was `None`"),
             SynthesisError::AssignmentMissing => {
                 write!(f, "an assignment for a variable could not be computed")
-            }
+            },
             SynthesisError::DivisionByZero => write!(f, "division by zero"),
             SynthesisError::Unsatisfiable => write!(f, "unsatisfiable constraint system"),
             SynthesisError::PolynomialDegreeTooLarge => write!(f, "polynomial degree is too large"),
             SynthesisError::UnexpectedIdentity => {
                 write!(f, "encountered an identity element in the CRS")
-            }
+            },
             SynthesisError::MalformedVerifyingKey => write!(f, "malformed verifying key"),
             SynthesisError::UnconstrainedVariable => {
                 write!(f, "auxiliary variable was unconstrained")
-            }
+            },
         }
     }
 }

relations/src/r1cs/impl_lc.rs

@@ -228,16 +228,16 @@ where
             Ordering::Greater => {
                 new_vec.push((push_fn(other[j].0), other[j].1));
                 j += 1;
-            }
+            },
             Ordering::Less => {
                 new_vec.push(*self_cur);
                 i += 1;
-            }
+            },
             Ordering::Equal => {
                 new_vec.push((combine_fn(self_cur.0, other_cur.0), self_cur.1));
                 i += 1;
                 j += 1;
-            }
+            },
         };
     }
     new_vec.extend_from_slice(&cur[i..]);

relations/src/r1cs/trace.rs

@@ -68,7 +68,7 @@ where
             id if id == TypeId::of::<Self>() => Some(self as *const _ as *const ()),
             id if id == TypeId::of::<WithContext>() => {
                 Some(&self.get_context as *const _ as *const ())
-            }
+            },
             _ => None,
         }
     }