[#1793] Add range check interface + witness assertions

msm/src/fec/constraint.rs

@@ -51,4 +51,12 @@ impl<F: PrimeField> FECInterpreterEnv<F> for ConstraintBuilderEnv<F> {
     fn range_check_15bit(&mut self, _value: &Self::Variable) {
         // FIXME unimplemented
     }
+
+    fn range_check_abs15bit(&mut self, _value: &Self::Variable) {
+        // FIXME unimplemented
+    }
+
+    fn range_check_abs4bit(&mut self, _value: &Self::Variable) {
+        // FIXME unimplemented
+    }
 }

msm/src/fec/interpreter.rs

@@ -26,14 +26,17 @@ pub trait FECInterpreterEnv<F: PrimeField> {
 
     fn read_column(&self, ix: Column) -> Self::Variable;
 
-    /// Checks |x| = 1, that is x ∈ {-1,0,1}
+    /// Checks |x| = 1, that is x ∈ {-1,1}
     fn range_check_abs1(&mut self, value: &Self::Variable);
 
     /// Checks input x ∈ [0,2^15)
     fn range_check_15bit(&mut self, value: &Self::Variable);
 
-    ///// Checks input x ∈ [0,2^4)
-    //fn range_check_4bit(&mut self, value: &Self::Variable);
+    /// Checks input |x| ∈ [0,2^15)
+    fn range_check_abs15bit(&mut self, value: &Self::Variable);
+
+    /// Checks input |x| ∈ [0,2^4)
+    fn range_check_abs4bit(&mut self, value: &Self::Variable);
 }
 
 /// Alias for LIMB_BITSIZE, used for convenience.
@@ -306,6 +309,24 @@ pub fn constrain_ec_addition<F: PrimeField, Env: FECInterpreterEnv<F>>(
         env.range_check_15bit(x);
     }
 
+    for x in [&q1_sign, &q2_sign, &q3_sign] {
+        env.range_check_abs1(x);
+    }
+    for (i, x) in carry1_limbs_small
+        .iter()
+        .chain(carry2_limbs_small.iter())
+        .chain(carry3_limbs_small.iter())
+        .enumerate()
+    {
+        if i % 6 == 5 {
+            // This should be a diferent range check depending on which big-limb we're processing?
+            // So instead of one type of lookup we will have 5 different ones?
+            env.range_check_abs4bit(x);
+        } else {
+            env.range_check_abs15bit(x);
+        }
+    }
+
     // FIXME: Some of these /have/ to be in the [0,F), and carries have very specific ranges!
 
     let xr_limbs_large =

msm/src/fec/witness.rs

@@ -56,12 +56,20 @@ impl<F: PrimeField> FECInterpreterEnv<F> for WitnessBuilderEnv<F> {
         self.witness.last().unwrap().cols[i]
     }
 
-    fn range_check_abs1(&mut self, _value: &Self::Variable) {
-        // FIXME unimplemented
+    fn range_check_abs1(&mut self, value: &Self::Variable) {
+        assert!(*value == F::one() || *value == F::zero() - F::one());
     }
 
-    fn range_check_15bit(&mut self, _value: &Self::Variable) {
-        // FIXME unimplemented
+    fn range_check_15bit(&mut self, value: &Self::Variable) {
+        assert!(*value < F::from(1u64 << 15));
+    }
+
+    fn range_check_abs15bit(&mut self, value: &Self::Variable) {
+        assert!(*value < F::from(1u64 << 15) || *value >= F::zero() - F::from(1u64 << 15));
+    }
+
+    fn range_check_abs4bit(&mut self, value: &Self::Variable) {
+        assert!(*value < F::from(1u64 << 4) || *value >= F::zero() - F::from(1u64 << 4));
     }
 }