Skip to content

Commit

Permalink
fix: apply range constraints to return values from unconstrained func…
Browse files Browse the repository at this point in the history
…tions (#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.
  • Loading branch information
TomAFrench authored Jan 31, 2024
1 parent 26e9618 commit 3af2a89
Showing 1 changed file with 43 additions and 13 deletions.
56 changes: 43 additions & 13 deletions compiler/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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))
}
})?;

Expand Down Expand Up @@ -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)
}

Expand Down

0 comments on commit 3af2a89

Please sign in to comment.