fix(ssa): Validate checked signed add/sub is followed by a truncate

EXTERNAL_NOIR_LIBRARIES.yml

@@ -112,7 +112,7 @@ libraries:
     repo: AztecProtocol/aztec-packages
     ref: *AZ_COMMIT
     path: noir-projects/noir-protocol-circuits/crates/types
-    timeout: 70
+    timeout: 75
     critical: false
   protocol_circuits_rollup_lib:
     repo: AztecProtocol/aztec-packages

compiler/noirc_evaluator/src/ssa/function_builder/mod.rs

@@ -155,6 +155,9 @@ impl FunctionBuilder {
     /// Consume the FunctionBuilder returning all the functions it has generated.
     pub fn finish(mut self) -> Ssa {
         self.finished_functions.push(self.current_function);
+
+        Self::validate_ssa(&self.finished_functions);
+
         Ssa::new(self.finished_functions, self.error_types)
     }
 
@@ -518,6 +521,66 @@ impl FunctionBuilder {
     pub fn record_error_type(&mut self, selector: ErrorSelector, typ: HirType) {
         self.error_types.insert(selector, typ);
     }
+
+    fn validate_ssa(functions: &[Function]) {
+        for function in functions {
+            Self::validate_function(function);
+        }
+    }
+
+    fn validate_function(function: &Function) {
+        // State for tracking the last signed binary addition/subtraction
+        let mut signed_binary_op = None;
+        for block in function.reachable_blocks() {
+            for instruction in function.dfg[block].instructions() {
+                match &function.dfg[*instruction] {
+                    Instruction::Binary(binary) => {
+                        signed_binary_op = None;
+
+                        match binary.operator {
+                            // We are only validating addition/subtraction
+                            BinaryOp::Add { unchecked: false }
+                            | BinaryOp::Sub { unchecked: false } => {}
+                            // Otherwise, move onto the next instruction
+                            _ => continue,
+                        }
+
+                        // Assume rhs_type is the same as lhs_type
+                        let lhs_type = function.dfg.type_of_value(binary.lhs);
+                        if let Type::Numeric(NumericType::Signed { bit_size }) = lhs_type {
+                            let results = function.dfg.instruction_results(*instruction);
+                            signed_binary_op = Some((bit_size, results[0]));
+                        }
+                    }
+                    Instruction::Truncate { value, bit_size, max_bit_size } => {
+                        let Some((signed_op_bit_size, signed_op_res)) = signed_binary_op.take()
+                        else {
+                            continue;
+                        };
+                        assert_eq!(
+                            *bit_size, signed_op_bit_size,
+                            "ICE: Correct truncate must follow the result of a checked signed add/sub"
+                        );
+                        assert_eq!(
+                            *max_bit_size,
+                            *bit_size + 1,
+                            "ICE: Correct truncate must follow the result of a checked signed add/sub"
+                        );
+                        assert_eq!(
+                            *value, signed_op_res,
+                            "ICE: Correct truncate must follow the result of a checked signed add/sub"
+                        );
+                    }
+                    _ => {
+                        signed_binary_op = None;
+                    }
+                }
+            }
+        }
+        if signed_binary_op.is_some() {
+            panic!("ICE: Truncate must follow the result of a checked signed add/sub");
+        }
+    }
 }
 
 impl std::ops::Index<ValueId> for FunctionBuilder {
@@ -572,10 +635,13 @@ mod tests {
 
     use acvm::{FieldElement, acir::AcirField};
 
-    use crate::ssa::ir::{
-        instruction::{Endian, Intrinsic},
-        map::Id,
-        types::{NumericType, Type},
+    use crate::ssa::{
+        ir::{
+            instruction::{Endian, Intrinsic},
+            map::Id,
+            types::{NumericType, Type},
+        },
+        ssa_gen::Ssa,
     };
 
     use super::FunctionBuilder;
@@ -603,4 +669,151 @@ mod tests {
         assert_eq!(slice[2], one);
         assert_eq!(slice[3], zero);
     }
+
+    #[test]
+    #[should_panic(expected = "ICE: Truncate must follow the result of a checked signed add/sub")]
+    fn lone_signed_sub_acir() {
+        let src = r"
+        acir(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = sub v0, v1
+            return v2
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    #[should_panic(expected = "ICE: Truncate must follow the result of a checked signed add/sub")]
+    fn lone_signed_sub_brillig() {
+        // This matches the test above we just want to make sure it holds in the Brillig runtime as well as ACIR
+        let src = r"
+        brillig(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = sub v0, v1
+            return v2
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    #[should_panic(expected = "ICE: Truncate must follow the result of a checked signed add/sub")]
+    fn lone_signed_add_acir() {
+        let src = r"
+        acir(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = add v0, v1
+            return v2
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    #[should_panic(expected = "ICE: Truncate must follow the result of a checked signed add/sub")]
+    fn lone_signed_add_brillig() {
+        let src = r"
+        brillig(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = add v0, v1
+            return v2
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    #[should_panic(
+        expected = "ICE: Correct truncate must follow the result of a checked signed add/sub"
+    )]
+    fn signed_sub_bad_truncate_bit_size() {
+        let src = r"
+        acir(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = sub v0, v1
+            v3 = truncate v2 to 32 bits, max_bit_size: 33
+            return v3
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    #[should_panic(
+        expected = "ICE: Correct truncate must follow the result of a checked signed add/sub"
+    )]
+    fn signed_sub_bad_truncate_max_bit_size() {
+        let src = r"
+        acir(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = sub v0, v1
+            v3 = truncate v2 to 16 bits, max_bit_size: 18
+            return v3
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    fn truncate_follows_signed_sub_acir() {
+        let src = r"
+        acir(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = sub v0, v1
+            v3 = truncate v2 to 16 bits, max_bit_size: 17
+            return v3
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    fn truncate_follows_signed_sub_brillig() {
+        let src = r"
+        brillig(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = sub v0, v1
+            v3 = truncate v2 to 16 bits, max_bit_size: 17
+            return v3
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    fn truncate_follows_signed_add_acir() {
+        let src = r"
+        acir(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = add v0, v1
+            v3 = truncate v2 to 16 bits, max_bit_size: 17
+            return v3
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
+
+    #[test]
+    fn truncate_follows_signed_add_brillig() {
+        let src = r"
+        brillig(inline) pure fn main f0 {
+          b0(v0: i16, v1: i16):
+            v2 = add v0, v1
+            v3 = truncate v2 to 16 bits, max_bit_size: 17
+            return v3
+        }
+        ";
+
+        let _ = Ssa::from_str(src);
+    }
 }

compiler/noirc_evaluator/src/ssa/interpreter/tests/instructions.rs

@@ -23,12 +23,12 @@ fn add() {
         "
         acir(inline) fn main f0 {
           b0():
-            v0 = add i32 2, i32 100
+            v0 = add u32 2, u32 100
             return v0
         }
     ",
     );
-    assert_eq!(value, Value::Numeric(NumericValue::I32(102)));
+    assert_eq!(value, Value::Numeric(NumericValue::U32(102)));
 }
 
 #[test]
@@ -64,12 +64,12 @@ fn sub() {
         "
         acir(inline) fn main f0 {
           b0():
-            v0 = sub i32 10101, i32 101
+            v0 = sub u32 10101, u32 101
             return v0
         }
     ",
     );
-    assert_eq!(value, Value::Numeric(NumericValue::I32(10000)));
+    assert_eq!(value, Value::Numeric(NumericValue::U32(10000)));
 }
 
 #[test]
@@ -79,7 +79,8 @@ fn sub_underflow() {
         acir(inline) fn main f0 {
           b0():
             v0 = sub i8 136, i8 10  // -120 - 10
-            return v0
+            v1 = truncate v0 to 8 bits, max_bit_size: 9
+            return v1
         }
     ",
     );

compiler/noirc_evaluator/src/ssa/opt/checked_to_unchecked.rs

@@ -292,7 +292,8 @@ mod tests {
             v2 = cast v0 as i32
             v3 = cast v1 as i32
             v4 = add v2, v3
-            return v4
+            v5 = truncate v4 to 32 bits, max_bit_size: 33
+            return v5
         }
         ";
         let ssa = Ssa::from_str(src).unwrap();
@@ -307,7 +308,8 @@ mod tests {
           b0(v0: i16):
             v1 = cast v0 as i32
             v2 = sub i32 65536, v1
-            return v2
+            v3 = truncate v2 to 32 bits, max_bit_size: 33
+            return v3
         }
         ";
         let ssa = Ssa::from_str(src).unwrap();

compiler/noirc_evaluator/src/ssa/opt/constant_folding.rs

@@ -1482,7 +1482,8 @@ mod test {
             brillig(inline) fn one f1 {
               b0(v0: i32, v1: i32):
                 v2 = add v0, v1
-                return v2
+                v3 = truncate v2 to 32 bits, max_bit_size: 33
+                return v3
             }
             ";
         let ssa = Ssa::from_str(src).unwrap();

compiler/noirc_evaluator/src/ssa/opt/loop_invariant.rs

@@ -1403,37 +1403,37 @@ mod test {
         // uses a checked add in `b3`.
         let src = "
         brillig(inline) fn main f0 {
-          b0(v0: i32, v1: i32):
-              jmp b1(i32 0)
-          b1(v2: i32):
-              v5 = lt v2, i32 4
+          b0(v0: u32, v1: u32):
+              jmp b1(u32 0)
+          b1(v2: u32):
+              v5 = lt v2, u32 4
               jmpif v5 then: b3, else: b2
           b2():
               return
           b3():
               v6 = mul v0, v1
-              constrain v6 == i32 6
-              v8 = add v2, i32 1
+              constrain v6 == u32 6
+              v8 = add v2, u32 1
               jmp b1(v8)
         }
         ";
 
         let ssa = Ssa::from_str(src).unwrap();
 
-        // `v8 = add v2, i32 1` in b3 should now be `v9 = unchecked_add v2, i32 1` in b3
+        // `v8 = add v2, u32 1` in b3 should now be `v9 = unchecked_add v2, u32 1` in b3
         let expected = "
         brillig(inline) fn main f0 {
-          b0(v0: i32, v1: i32):
+          b0(v0: u32, v1: u32):
             v3 = mul v0, v1
-            constrain v3 == i32 6
-            jmp b1(i32 0)
-          b1(v2: i32):
-            v7 = lt v2, i32 4
+            constrain v3 == u32 6
+            jmp b1(u32 0)
+          b1(v2: u32):
+            v7 = lt v2, u32 4
             jmpif v7 then: b3, else: b2
           b2():
             return
           b3():
-            v9 = unchecked_add v2, i32 1
+            v9 = unchecked_add v2, u32 1
             jmp b1(v9)
         }
         ";