Skip to content

Commit

Permalink
feat: static_assert builtin (noir-lang#5342)
Browse files Browse the repository at this point in the history
# Description

## Problem\*

Resolves noir-lang#5182

## Summary\*

1. New builtin that behaves almost exactly like `assert_constant`, but
also checks that the input is `true`
2. Add recursion to `assert_constant` so that `[dynamic_var]` is no
longer treated as constant

## Additional Context



## Documentation\*

Check one:
- [ ] No documentation needed.
- [ ] Documentation included in this PR.
- [ ] **[For Experimental Features]** 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.

---------

Co-authored-by: Maxim Vezenov <[email protected]>
  • Loading branch information
michaeljklein and vezenovm authored Jun 27, 2024
1 parent 47b621f commit ef44270
Show file tree
Hide file tree
Showing 39 changed files with 410 additions and 28 deletions.
6 changes: 6 additions & 0 deletions compiler/noirc_evaluator/src/errors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,10 @@ pub enum RuntimeError {
UnknownLoopBound { call_stack: CallStack },
#[error("Argument is not constant")]
AssertConstantFailed { call_stack: CallStack },
#[error("The static_assert message is not constant")]
StaticAssertDynamicMessage { call_stack: CallStack },
#[error("Nested slices are not supported")]
StaticAssertFailed { call_stack: CallStack },
#[error("Nested slices are not supported")]
NestedSlice { call_stack: CallStack },
#[error("Big Integer modulus do no match")]
Expand Down Expand Up @@ -120,6 +124,8 @@ impl RuntimeError {
| RuntimeError::UnInitialized { call_stack, .. }
| RuntimeError::UnknownLoopBound { call_stack }
| RuntimeError::AssertConstantFailed { call_stack }
| RuntimeError::StaticAssertFailed { call_stack }
| RuntimeError::StaticAssertDynamicMessage { call_stack }
| RuntimeError::IntegerOutOfBounds { call_stack, .. }
| RuntimeError::UnsupportedIntegerSize { call_stack, .. }
| RuntimeError::NestedSlice { call_stack, .. }
Expand Down
5 changes: 4 additions & 1 deletion compiler/noirc_evaluator/src/ssa.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,10 @@ pub(crate) fn optimize_into_acir(
// Run mem2reg with the CFG separated into blocks
.run_pass(Ssa::mem2reg, "After Mem2Reg:")
.run_pass(Ssa::as_slice_optimization, "After `as_slice` optimization")
.try_run_pass(Ssa::evaluate_assert_constant, "After Assert Constant:")?
.try_run_pass(
Ssa::evaluate_static_assert_and_assert_constant,
"After `static_assert` and `assert_constant`:",
)?
.try_run_pass(Ssa::unroll_loops_iteratively, "After Unrolling:")?
.run_pass(Ssa::simplify_cfg, "After Simplifying:")
.run_pass(Ssa::flatten_cfg, "After Flattening:")
Expand Down
17 changes: 15 additions & 2 deletions compiler/noirc_evaluator/src/ssa/ir/dfg.rs
Original file line number Diff line number Diff line change
Expand Up @@ -497,9 +497,22 @@ impl DataFlowGraph {
}
}

/// True if the given ValueId refers to a constant value
/// True if the given ValueId refers to a (recursively) constant value
pub(crate) fn is_constant(&self, argument: ValueId) -> bool {
!matches!(&self[self.resolve(argument)], Value::Instruction { .. } | Value::Param { .. })
match &self[self.resolve(argument)] {
Value::Instruction { .. } | Value::Param { .. } => false,
Value::Array { array, .. } => array.iter().all(|element| self.is_constant(*element)),
_ => true,
}
}

/// True that the input is a non-zero `Value::NumericConstant`
pub(crate) fn is_constant_true(&self, argument: ValueId) -> bool {
if let Some(constant) = self.get_numeric_constant(argument) {
!constant.is_zero()
} else {
false
}
}
}

Expand Down
10 changes: 7 additions & 3 deletions compiler/noirc_evaluator/src/ssa/ir/instruction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ pub(crate) enum Intrinsic {
ArrayLen,
AsSlice,
AssertConstant,
StaticAssert,
SlicePushBack,
SlicePushFront,
SlicePopBack,
Expand All @@ -76,6 +77,7 @@ impl std::fmt::Display for Intrinsic {
Intrinsic::ArrayLen => write!(f, "array_len"),
Intrinsic::AsSlice => write!(f, "as_slice"),
Intrinsic::AssertConstant => write!(f, "assert_constant"),
Intrinsic::StaticAssert => write!(f, "static_assert"),
Intrinsic::SlicePushBack => write!(f, "slice_push_back"),
Intrinsic::SlicePushFront => write!(f, "slice_push_front"),
Intrinsic::SlicePopBack => write!(f, "slice_pop_back"),
Expand Down Expand Up @@ -104,9 +106,10 @@ impl Intrinsic {
/// If there are no side effects then the `Intrinsic` can be removed if the result is unused.
pub(crate) fn has_side_effects(&self) -> bool {
match self {
Intrinsic::AssertConstant | Intrinsic::ApplyRangeConstraint | Intrinsic::AsWitness => {
true
}
Intrinsic::AssertConstant
| Intrinsic::StaticAssert
| Intrinsic::ApplyRangeConstraint
| Intrinsic::AsWitness => true,

// These apply a constraint that the input must fit into a specified number of limbs.
Intrinsic::ToBits(_) | Intrinsic::ToRadix(_) => true,
Expand Down Expand Up @@ -142,6 +145,7 @@ impl Intrinsic {
"array_len" => Some(Intrinsic::ArrayLen),
"as_slice" => Some(Intrinsic::AsSlice),
"assert_constant" => Some(Intrinsic::AssertConstant),
"static_assert" => Some(Intrinsic::StaticAssert),
"apply_range_constraint" => Some(Intrinsic::ApplyRangeConstraint),
"slice_push_back" => Some(Intrinsic::SlicePushBack),
"slice_push_front" => Some(Intrinsic::SlicePushFront),
Expand Down
15 changes: 15 additions & 0 deletions compiler/noirc_evaluator/src/ssa/ir/instruction/call.rs
Original file line number Diff line number Diff line change
Expand Up @@ -246,6 +246,21 @@ pub(super) fn simplify_call(
SimplifyResult::None
}
}
Intrinsic::StaticAssert => {
if arguments.len() != 2 {
panic!("ICE: static_assert called with wrong number of arguments")
}

if !dfg.is_constant(arguments[1]) {
return SimplifyResult::None;
}

if dfg.is_constant_true(arguments[0]) {
SimplifyResult::Remove
} else {
SimplifyResult::None
}
}
Intrinsic::ApplyRangeConstraint => {
let value = arguments[0];
let max_bit_size = dfg.get_numeric_constant(arguments[1]);
Expand Down
35 changes: 34 additions & 1 deletion compiler/noirc_evaluator/src/ssa/opt/assert_constant.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,9 @@ impl Ssa {
/// since we must go through every instruction to find all references to `assert_constant`
/// while loop unrolling only touches blocks with loops in them.
#[tracing::instrument(level = "trace", skip(self))]
pub(crate) fn evaluate_assert_constant(mut self) -> Result<Ssa, RuntimeError> {
pub(crate) fn evaluate_static_assert_and_assert_constant(
mut self,
) -> Result<Ssa, RuntimeError> {
for function in self.functions.values_mut() {
for block in function.reachable_blocks() {
// Unfortunately we can't just use instructions.retain(...) here since
Expand Down Expand Up @@ -54,10 +56,13 @@ fn check_instruction(
instruction: InstructionId,
) -> Result<bool, RuntimeError> {
let assert_constant_id = function.dfg.import_intrinsic(Intrinsic::AssertConstant);
let static_assert_id = function.dfg.import_intrinsic(Intrinsic::StaticAssert);
match &function.dfg[instruction] {
Instruction::Call { func, arguments } => {
if *func == assert_constant_id {
evaluate_assert_constant(function, instruction, arguments)
} else if *func == static_assert_id {
evaluate_static_assert(function, instruction, arguments)
} else {
Ok(true)
}
Expand All @@ -82,3 +87,31 @@ fn evaluate_assert_constant(
Err(RuntimeError::AssertConstantFailed { call_stack })
}
}

/// Evaluate a call to `static_assert`, returning an error if the value is false
/// or not constant (see assert_constant).
///
/// When it passes, Ok(false) is returned. This signifies a
/// success but also that the instruction need not be reinserted into the block being unrolled
/// since it has already been evaluated.
fn evaluate_static_assert(
function: &Function,
instruction: InstructionId,
arguments: &[ValueId],
) -> Result<bool, RuntimeError> {
if arguments.len() != 2 {
panic!("ICE: static_assert called with wrong number of arguments")
}

if !function.dfg.is_constant(arguments[1]) {
let call_stack = function.dfg.get_call_stack(instruction);
return Err(RuntimeError::StaticAssertDynamicMessage { call_stack });
}

if function.dfg.is_constant_true(arguments[0]) {
Ok(false)
} else {
let call_stack = function.dfg.get_call_stack(instruction);
Err(RuntimeError::StaticAssertFailed { call_stack })
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,7 @@ impl Context {

Intrinsic::ArrayLen
| Intrinsic::AssertConstant
| Intrinsic::StaticAssert
| Intrinsic::ApplyRangeConstraint
| Intrinsic::StrAsBytes
| Intrinsic::ToBits(_)
Expand Down
1 change: 1 addition & 0 deletions compiler/noirc_evaluator/src/ssa/opt/remove_if_else.rs
Original file line number Diff line number Diff line change
Expand Up @@ -226,6 +226,7 @@ fn slice_capacity_change(

// These cases don't affect slice capacities
Intrinsic::AssertConstant
| Intrinsic::StaticAssert
| Intrinsic::ApplyRangeConstraint
| Intrinsic::ArrayLen
| Intrinsic::StrAsBytes
Expand Down
17 changes: 0 additions & 17 deletions compiler/noirc_frontend/src/ast/expression.rs
Original file line number Diff line number Diff line change
Expand Up @@ -189,23 +189,6 @@ impl ExpressionKind {
struct_type: None,
}))
}

/// Returns true if the expression is a literal integer
pub fn is_integer(&self) -> bool {
self.as_integer().is_some()
}

fn as_integer(&self) -> Option<FieldElement> {
let literal = match self {
ExpressionKind::Literal(literal) => literal,
_ => return None,
};

match literal {
Literal::Integer(integer, _) => Some(*integer),
_ => None,
}
}
}

impl Recoverable for ExpressionKind {
Expand Down
1 change: 1 addition & 0 deletions compiler/noirc_frontend/src/monomorphization/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -610,6 +610,7 @@ impl<'interner> Monomorphizer<'interner> {
})
.transpose()?
.map(Box::new);

Ok(ast::Expression::Constrain(Box::new(expr), location, assert_message))
}
HirStatement::Assign(assign) => self.assign(assign),
Expand Down
39 changes: 36 additions & 3 deletions docs/docs/noir/concepts/assert.md
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
---
title: Assert Function
description:
Learn about the assert function in Noir, which can be used to explicitly constrain the predicate or
comparison expression that follows to be true, and what happens if the expression is false at
runtime.
Learn about the `assert` and `static_assert` functions in Noir, which can be used to explicitly
constrain the predicate or comparison expression that follows to be true, and what happens if
the expression is false at runtime or compile-time, respectively.
keywords: [Noir programming language, assert statement, predicate expression, comparison expression]
sidebar_position: 4
---
Expand Down Expand Up @@ -43,3 +43,36 @@ let s = myStruct { myField: y };
assert(s.myField == x, s);
```

There is also a special `static_assert` function that behaves like `assert`,
but that runs at compile-time.

```rust
fn main(xs: [Field; 3]) {
let x = 2 + 2;
let y = 4;
static_assert(x == y, "expected 2 + 2 to equal 4");

// This passes since the length of `xs` is known at compile-time
static_assert(xs.len() == 3, "expected the input to have 3 elements");
}
```

This function fails when passed a dynamic (run-time) argument:

```rust
fn main(x : Field, y : Field) {
// this fails because `x` is not known at compile-time
static_assert(x == 2, "expected x to be known at compile-time and equal to 2");

let mut example_slice = &[];
if y == 4 {
example_slice = example_slice.push_back(0);
}

// This fails because the length of `example_slice` is not known at
// compile-time
let error_message = "expected an empty slice, known at compile-time";
static_assert(example_slice.len() == 0, error_message);
}
```

5 changes: 5 additions & 0 deletions noir_stdlib/src/lib.nr
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,11 @@ pub fn verify_proof<N>(verification_key: [Field], proof: [Field], public_inputs:
// Useful for debugging for-loop bounds.
#[builtin(assert_constant)]
pub fn assert_constant<T>(x: T) {}

// Asserts that the given value is both true and known at compile-time
#[builtin(static_assert)]
pub fn static_assert<N>(predicate: bool, message: str<N>) {}

// from_field and as_field are private since they are not valid for every type.
// `as` should be the default for users to cast between primitive types, and in the future
// traits can be used to work with generic types.
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "assert_constant_dynamic_array"
type = "bin"
authors = [""]
compiler_version = ">=0.31.0"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
fn main(
dynamic_one: Field, // == 1
) {
assert_constant([dynamic_one]);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "assert_constant_dynamic_plus"
type = "bin"
authors = [""]
compiler_version = ">=0.31.0"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
fn main(
dynamic_one: Field, // == 1
) {
assert_constant(dynamic_one + 1 == 3);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "assert_constant_dynamic_slice"
type = "bin"
authors = [""]
compiler_version = ">=0.31.0"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
fn main(
dynamic_one: Field, // == 1
) {
assert_constant(&[dynamic_one]);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "assert_constant_dynamic_struct_array"
type = "bin"
authors = [""]
compiler_version = ">=0.31.0"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
struct Foo {
field: Field,
array: [Field; 3],
slice: [Field],
}

fn main(
dynamic_one: Field, // == 1
) {
let foo_dynamic_array = Foo { field: 0, array: [dynamic_one, 2, 3], slice: &[] };
assert_constant(foo_dynamic_array);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "assert_constant_dynamic_struct_field"
type = "bin"
authors = [""]
compiler_version = ">=0.31.0"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
struct Foo {
field: Field,
array: [Field; 3],
slice: [Field],
}

fn main(
dynamic_one: Field, // == 1
) {
let foo_dynamic = Foo { field: dynamic_one, array: [1, 2, 3], slice: &[] };
assert_constant(foo_dynamic);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
[package]
name = "assert_constant_dynamic_struct_slice"
type = "bin"
authors = [""]
compiler_version = ">=0.31.0"

[dependencies]
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
struct Foo {
field: Field,
array: [Field; 3],
slice: [Field],
}

fn main(
dynamic_one: Field, // == 1
) {
let foo_dynamic_slice = Foo { field: 0, array: [1, 2, 3], slice: &[dynamic_one] };
assert_constant(foo_dynamic_slice);
}
Loading

0 comments on commit ef44270

Please sign in to comment.