From 3af2a89826f7d9b6dcd1782b8b38417c64065293 Mon Sep 17 00:00:00 2001
From: Tom French <15848336+TomAFrench@users.noreply.github.com>
Date: Wed, 31 Jan 2024 14:48:06 +0000
Subject: [PATCH] fix: apply range constraints to return values from
 unconstrained functions (#4217)

# Description

## Problem\*

Resolves <!-- Link to GitHub Issue -->

## Summary\*

Consider the program

```rust
unconstrained fn identity(x: u8) -> u8 {
    x
}

fn main(x: u8, y: pub Field) {
    assert(identity(x) as Field == 1000);
}
```

From looking at the type information, this program should be
unsatisfiable. A `u8` should not be able to contain the value `1000` so
the assertion should always fail. If we look at the generated ACIR
however we see that the return value of `identity()` doesn't need to be
a valid `u8` and so can be set by the prover to be `1000`.

```
BLACKBOX::RANGE [(_0, num_bits: 8)] [ ]
BRILLIG: inputs: [Single(Expression { mul_terms: [], linear_combinations: [(1, Witness(0))], q_c: 0 })]
outputs: [Simple(Witness(2))]
[Mov { destination: RegisterIndex(2), source: RegisterIndex(0) }, Const { destination: RegisterIndex(0), value: Value { inner: 0 } }, Const { destination: RegisterIndex(1), value: Value { inner: 0 } }, Mov { destination: RegisterIndex(2), source: RegisterIndex(2) }, Call { location: 7 }, Mov { destination: RegisterIndex(0), source: RegisterIndex(2) }, Stop, Mov { destination: RegisterIndex(3), source: RegisterIndex(2) }, Mov { destination: RegisterIndex(2), source: RegisterIndex(3) }, Return]

EXPR [ (1, _2) -1000 ]
```

This PR modifies ACIR gen so that when inserting a call to a brillig
function, we apply range constraints to the return values to ensure that
the results provided by the prover must be valid for those types.

## Additional Context

Note that we cannot enforce safety for all types which have validity
conditions outside of the type system. e.g. If an unconstrained function
returns a `U128` then this will not be constrained as its limbs are made
up of `Field`s so no constraints will be applied allowing a potentially
invalid value to be returned.


## Documentation\*

Check one:
- [x] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[Exceptional Case]** Documentation to be submitted in a separate
PR.

# PR Checklist\*

- [x] I have tested the changes locally.
- [x] I have formatted the changes with [Prettier](https://prettier.io/)
and/or `cargo fmt` on default settings.
---
 .../src/ssa/acir_gen/acir_ir/acir_variable.rs | 56 ++++++++++++++-----
 1 file changed, 43 insertions(+), 13 deletions(-)

diff --git a/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs b/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs
index a419dac9d93..5cf70b098f9 100644
--- a/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs
+++ b/compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs
@@ -1441,20 +1441,22 @@ impl AcirContext {
         inputs: Vec<AcirValue>,
         outputs: Vec<AcirType>,
         attempt_execution: bool,
-    ) -> Result<Vec<AcirValue>, InternalError> {
-        let b_inputs = try_vecmap(inputs, |i| match i {
-            AcirValue::Var(var, _) => Ok(BrilligInputs::Single(self.var_to_expression(var)?)),
-            AcirValue::Array(vars) => {
-                let mut var_expressions: Vec<Expression> = Vec::new();
-                for var in vars {
-                    self.brillig_array_input(&mut var_expressions, var)?;
+    ) -> Result<Vec<AcirValue>, RuntimeError> {
+        let b_inputs = try_vecmap(inputs, |i| -> Result<_, InternalError> {
+            match i {
+                AcirValue::Var(var, _) => Ok(BrilligInputs::Single(self.var_to_expression(var)?)),
+                AcirValue::Array(vars) => {
+                    let mut var_expressions: Vec<Expression> = Vec::new();
+                    for var in vars {
+                        self.brillig_array_input(&mut var_expressions, var)?;
+                    }
+                    Ok(BrilligInputs::Array(var_expressions))
+                }
+                AcirValue::DynamicArray(_) => {
+                    let mut var_expressions = Vec::new();
+                    self.brillig_array_input(&mut var_expressions, i)?;
+                    Ok(BrilligInputs::Array(var_expressions))
                 }
-                Ok(BrilligInputs::Array(var_expressions))
-            }
-            AcirValue::DynamicArray(_) => {
-                let mut var_expressions = Vec::new();
-                self.brillig_array_input(&mut var_expressions, i)?;
-                Ok(BrilligInputs::Array(var_expressions))
             }
         })?;
 
@@ -1489,6 +1491,34 @@ impl AcirContext {
         let predicate = self.var_to_expression(predicate)?;
         self.acir_ir.brillig(Some(predicate), generated_brillig, b_inputs, b_outputs);
 
+        fn range_constraint_value(
+            context: &mut AcirContext,
+            value: &AcirValue,
+        ) -> Result<(), RuntimeError> {
+            match value {
+                AcirValue::Var(var, typ) => {
+                    let numeric_type = match typ {
+                        AcirType::NumericType(numeric_type) => numeric_type,
+                        _ => unreachable!("`AcirValue::Var` may only hold primitive values"),
+                    };
+                    context.range_constrain_var(*var, numeric_type, None)?;
+                }
+                AcirValue::Array(values) => {
+                    for value in values {
+                        range_constraint_value(context, value)?;
+                    }
+                }
+                AcirValue::DynamicArray(_) => {
+                    unreachable!("Brillig opcodes cannot return dynamic arrays")
+                }
+            }
+            Ok(())
+        }
+
+        for output_var in &outputs_var {
+            range_constraint_value(self, output_var)?;
+        }
+
         Ok(outputs_var)
     }