[#1793] Fix ff_higest range check

o1-labs · Mar 21, 2024 · 605ae08 · 605ae08
1 parent d5c4820
commit 605ae08
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/msm/src/fec/interpreter.rs b/msm/src/fec/interpreter.rs
@@ -29,7 +29,7 @@ pub trait FECInterpreterEnv<F: PrimeField> {
     /// Checks |x| = 1, that is x ∈ {-1,1}
     fn range_check_abs1(&mut self, value: &Self::Variable);
 
-    /// Checks x ∈ [0, f - 2^{15*16})
+    /// Checks x ∈ [0, f >> 15*16)
     fn range_check_ff_highest<Ff: PrimeField>(&mut self, value: &Self::Variable);
 
     /// Checks input x ∈ [0,2^15)
@@ -312,7 +312,7 @@ pub fn constrain_ec_addition<F: PrimeField, Ff: PrimeField, Env: FECInterpreterE
         .chain(yr_limbs_small.iter())
         .enumerate()
     {
-        if i % N_LIMBS_LARGE == N_LIMBS_LARGE - 1 {
+        if i % N_LIMBS_SMALL == N_LIMBS_SMALL - 1 {
             // If it's the highest limb, we need to check that it's representing a field element.
             env.range_check_ff_highest::<Ff>(x);
         } else {

diff --git a/msm/src/fec/witness.rs b/msm/src/fec/witness.rs
@@ -63,8 +63,11 @@ impl<F: PrimeField> FECInterpreterEnv<F> for WitnessBuilderEnv<F> {
 
     fn range_check_ff_highest<Ff: PrimeField>(&mut self, value: &Self::Variable) {
         let f_bui: BigUint = TryFrom::try_from(Ff::Params::MODULUS).unwrap();
-        let big_limb: BigUint = BigUint::from(1u64) << ((N_LIMBS - 1) * LIMB_BITSIZE);
-        let top_modulus: BigUint = f_bui - big_limb;
+        // N_LIMBS * LIMB_BITSIZE = 17*15 = 255
+        // (N_LIMBS-1) * LIMB_BITSIZE = 16*15 = 240
+        // So we only want to check that the highest 15 bits of our number is
+        // less than the highest bits of f after dropping 240 of the lowest ones.
+        let top_modulus: BigUint = f_bui >> ((N_LIMBS - 1) * LIMB_BITSIZE);
         let top_modulus_f: F = F::from_biguint(&top_modulus).unwrap();
         assert!(*value < top_modulus_f);
     }