Fixes for Allen's Issue 3

core/src/alu/divrem/mod.rs

@@ -181,6 +181,18 @@ pub struct DivRemCols<T> {
     /// Flag to indicate whether `c` is negative.
     pub c_neg: T,
 
+    /// Flag to indicate whether `c` is a multiple of 256.
+    pub c_neg_mult_256: T,
+
+    /// Flag to indicate whether `rem` is a multiple of -256.
+    pub rem_neg_mult_256: T,
+
+    /// Flag to indicate whether `c` is min value
+    pub is_c_min: IsEqualWordOperation<T>,
+
+    /// Flag to indicate whether `rem` is min value
+    pub is_rem_min: IsEqualWordOperation<T>,
+
     /// Selector to know whether this row is enabled.
     pub is_real: T,
 
@@ -255,6 +267,13 @@ impl<F: PrimeField> MachineAir<F> for DivRemChip {
                     cols.max_abs_c_or_1 = Word::from(u32::max(1, event.c));
                 }
 
+                //Flags for absolute value special cases.
+                cols.is_c_min.populate(event.c, i32::MIN as u32);
+                cols.is_rem_min.populate(remainder, i32::MIN as u32);
+
+                cols.rem_neg_mult_256 = F::from_bool(remainder % 256 == 0) * cols.rem_neg;
+                cols.c_neg_mult_256 = F::from_bool(event.c % 256 == 0) * cols.c_neg;
+
                 // Insert the MSB lookup events.
                 {
                     let words = [event.b, event.c, remainder];
@@ -644,18 +663,47 @@ where
 
         // Range check remainder. (i.e., |remainder| < |c| when not is_c_0)
         {
+            // Calculate the extra flags for absolute value special cases.
+            IsEqualWordOperation::<AB::F>::eval(
+                builder,
+                local.c.map(|x| x.into()),
+                Word::from(i32::MIN as u32).map(|x: AB::F| x.into()),
+                local.is_c_min,
+                local.is_real.into(),
+            );
+
+            IsEqualWordOperation::<AB::F>::eval(
+                builder,
+                local.remainder.map(|x| x.into()),
+                Word::from(i32::MIN as u32).map(|x: AB::F| x.into()),
+                local.is_rem_min,
+                local.is_real.into(),
+            );
+
+            builder.assert_bool(local.c_neg_mult_256);
+            builder.assert_bool(local.rem_neg_mult_256);
+
+            builder.when(local.c_neg_mult_256).assert_zero(local.c[0]);
+            builder
+                .when(local.rem_neg_mult_256)
+                .assert_zero(local.remainder[0]);
+
             eval_abs_value(
                 builder,
                 local.remainder.borrow(),
                 local.abs_remainder.borrow(),
                 local.rem_neg.borrow(),
+                local.is_rem_min.is_diff_zero.result.borrow(),
+                local.rem_neg_mult_256.borrow(),
             );
 
             eval_abs_value(
                 builder,
                 local.c.borrow(),
                 local.abs_c.borrow(),
                 local.c_neg.borrow(),
+                local.is_c_min.is_diff_zero.result.borrow(),
+                local.c_neg_mult_256.borrow(),
             );
 
             // max(abs(c), 1) = abs(c) * (1 - is_c_0) + 1 * is_c_0
@@ -856,6 +904,7 @@ mod tests {
             (Opcode::DIV, neg(1), 0, 0),
             (Opcode::DIV, 1 << 31, 1 << 31, neg(1)),
             (Opcode::REM, 0, 1 << 31, neg(1)),
+            (Opcode::REM, 0, 1 << 8, neg(256)),
         ];
         for t in divrems.iter() {
             divrem_events.push(AluEvent::new(0, 0, t.0, t.1, t.2, t.3));

core/src/alu/divrem/utils.rs

@@ -2,6 +2,7 @@ use p3_air::AirBuilder;
 use p3_field::AbstractField;
 
 use crate::air::{SP1AirBuilder, Word, WORD_SIZE};
+use crate::operations::IsEqualWordOperation;
 use crate::runtime::Opcode;
 
 /// Returns `true` if the given `opcode` is a signed operation.
@@ -55,6 +56,8 @@ pub fn eval_abs_value<AB>(
     value: &Word<AB::Var>,
     abs_value: &Word<AB::Var>,
     is_negative: &AB::Var,
+    is_min: &AB::Var,
+    is_neg_mult_256: &AB::Var,
 ) where
     AB: SP1AirBuilder,
 {
@@ -67,12 +70,32 @@ pub fn eval_abs_value<AB>(
             }
         });
 
+        // Excluding the special case when value is a negative multiple of 256, we check that the sum of the limbs is `exp_sum_if_negative` if `is_negative` and otherwise check that the limbs are equal.
         builder
+            .when_not(*is_neg_mult_256)
             .when(*is_negative)
             .assert_eq(value[i] + abs_value[i], exp_sum_if_negative.clone());
 
         builder
             .when_not(*is_negative)
             .assert_eq(value[i], abs_value[i]);
     }
+
+    // In the special case that the value is a negative multiple of 256, we check that the first byte of the absolute value is 9.
+    builder
+        .when(*is_neg_mult_256)
+        .when(*is_negative)
+        .assert_eq(abs_value[0], AB::Expr::from_canonical_u32(0));
+
+    // In the further special case that the value is the minimum i32 value, we further need to check that the absolute value is again the minimum i32 value.
+    for i in 0..WORD_SIZE - 1 {
+        builder
+            .when(*is_min)
+            .when(*is_negative)
+            .assert_eq(abs_value[i], AB::Expr::from_canonical_u32(0));
+    }
+    builder
+        .when(*is_min)
+        .when(*is_negative)
+        .assert_eq(abs_value[WORD_SIZE - 1], AB::Expr::from_canonical_u32(1));
 }

core/src/runtime/mod.rs

@@ -1513,6 +1513,12 @@ pub mod tests {
         u32::MAX - a + 1
     }
 
+    #[test]
+    fn just_run_div() {
+        println!("{}", u32::MAX - 1 + 1);
+        println!("{}", 1 << 31);
+        println!("{}", (u32::MAX - 1 + 1) / (1 << 31));
+    }
     #[test]
     fn division_tests() {
         simple_op_code_test(Opcode::DIVU, 3, 20, 6);
@@ -1521,6 +1527,7 @@ pub mod tests {
         simple_op_code_test(Opcode::DIVU, 0, u32::MAX - 20 + 1, u32::MAX - 6 + 1);
 
         simple_op_code_test(Opcode::DIVU, 1 << 31, 1 << 31, 1);
+        // println!("{} {} {}", u32::MAX, 1 << 31, u32::MAX - 1 + 1);
         simple_op_code_test(Opcode::DIVU, 0, 1 << 31, u32::MAX - 1 + 1);
 
         simple_op_code_test(Opcode::DIVU, u32::MAX, 1 << 31, 0);