fix(acir): Div/mod for i1

compiler/noirc_evaluator/src/acir/acir_context/mod.rs

@@ -1029,6 +1029,30 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
         let zero = self.add_constant(F::zero());
         let one = self.add_constant(F::one());
 
+        // When dividing the twos complement lhs and rhs, we subtract one from the bit size
+        // to accurately represent the unsigned values we are dividing.
+        // We then internally constrain `q < 2^{max_q_bits}` during euclidean division.
+        // If we do not special case for binary types of one bit, we will range constrain the resulting
+        // quotient to be zero bits, which will cause inadvertent failures.
+        // We could theoretically still use this algorithm as is by incrementing the bit size by one,
+        // but the special case is very simple and then we don't mix the degenerate type
+        // into our general signed division algorithm.
+        //
+        // We know that a signed integer of bit size one can only be -1 or 0
+        // Thus, we know the only valid signed division can be 0 / -1.
+        // 0 / -1, valid as the quotient is 0
+        // -1 / -1, invalid as the quotient is 1, which cannot be represented in an i1
+        // All divisions by zero are invalid
+        if bit_size == 1 {
+            let lhs_is_zero = self.eq_var(lhs, zero)?;
+            // The value is represented internally as one with its sign stored separately
+            // As we are within signed division we can just check whether we have one here.
+            let rhs_is_one = self.eq_var(rhs, one)?;
+            let both_true = self.and_var(lhs_is_zero, rhs_is_one, AcirType::unsigned(1))?;
+            self.assert_neq_var(both_true, zero, predicate, None)?;
+            return Ok((zero, zero));
+        };
+
         // Get the sign bit of rhs by computing rhs / max_power_of_two
         let (rhs_leading, _) = self.euclidean_division_var(rhs, max_power_of_two, bit_size, one)?;
 
@@ -1080,7 +1104,32 @@ impl<F: AcirField, B: BlackBoxFunctionSolver<F>> AcirContext<F, B> {
 
         let (_, remainder_var) = match numeric_type {
             NumericType::Signed { bit_size } => {
-                self.signed_division_var(lhs, rhs, bit_size, predicate)?
+                // When dividing the twos complement lhs and rhs, we subtract one from the bit size
+                // to accurately represent the unsigned values we are dividing.
+                // We then internally constrain `q < 2^{max_q_bits}` during euclidean division.
+                // If we do not special case for binary types of one bit, we will range constrain the resulting
+                // quotient to be zero bits, which will cause inadvertent failures.
+                // We could theoretically still use `signed_division_var` here by incrementing the bit size by one,
+                // but the special case is very simple and then we don't mix the degenerate type
+                // into our general signed division algorithm.
+                //
+                // We know that a signed integer of bit size one can only be -1 or 0
+                // Thus, we know the only valid signed modulo can be 0 % -1 or -1 % -1
+                // 0 / -1, valid as the remainder is 0
+                // -1 / -1, valid as the remainder is 0
+                // All divisions by zero are invalid
+                if bit_size == 1 {
+                    // We only need to check that the rhs is not zero.
+                    // Otherwise the only valid result is zero.
+                    let zero = self.add_constant(F::zero());
+                    let rhs_is_zero = self.eq_var(rhs, zero)?;
+                    let rhs_is_zero_and_predicate_active = self.mul_var(rhs_is_zero, predicate)?;
+                    self.assert_eq_var(rhs_is_zero_and_predicate_active, zero, None)?;
+
+                    (zero, zero)
+                } else {
+                    self.signed_division_var(lhs, rhs, bit_size, predicate)?
+                }
             }
             _ => self.euclidean_division_var(lhs, rhs, bit_size, predicate)?,
         };

test_programs/execution_failure/div_by_zero_i1/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "div_by_zero_i1"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_failure/div_by_zero_i1/Prover.toml

@@ -0,0 +1,2 @@
+a = -1
+zero = 0

test_programs/execution_failure/div_by_zero_i1/src/main.nr

@@ -0,0 +1,3 @@
+fn main(a: i1, zero: i1) -> pub i1 {
+    a / zero
+}

test_programs/execution_failure/div_by_zero_modulo_i1/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "div_by_zero_modulo_i1"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_failure/div_by_zero_modulo_i1/Prover.toml

@@ -0,0 +1,2 @@
+a = -1
+zero = 0

test_programs/execution_failure/div_by_zero_modulo_i1/src/main.nr

@@ -0,0 +1,3 @@
+fn main(a: i1, zero: i1) -> pub i1 {
+    a % zero
+}

test_programs/execution_failure/i1_invalid_div_by_neg_one/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "i1_invalid_div_by_neg_one"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_failure/i1_invalid_div_by_neg_one/Prover.toml

@@ -0,0 +1 @@
+a = -1

test_programs/execution_failure/i1_invalid_div_by_neg_one/src/main.nr

@@ -0,0 +1,3 @@
+fn main(a: i1) -> pub i1 {
+    a / a
+}

test_programs/execution_success/i1_div_and_mod/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "i1_div_and_mod"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_success/i1_div_and_mod/Prover.toml

@@ -0,0 +1,2 @@
+a = -1
+zero = 0

test_programs/execution_success/i1_div_and_mod/src/main.nr

@@ -0,0 +1,12 @@
+fn main(a: i1, zero: i1) {
+    assert(0 / a == 0);
+    assert(a % a == 0);
+
+    // This if conditional is expected to be false
+    // We want to test the division appropriately does not error
+    // under an inactive predicate
+    if a == 0 {
+        assert(a / zero == 0);
+        assert(a % zero == 0);
+    }
+}