Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Evaluation of dynamic assert messages #4101

Merged
merged 72 commits into from
Feb 1, 2024
Merged
Show file tree
Hide file tree
Changes from 22 commits
Commits
Show all changes
72 commits
Select commit Hold shift + click to select a range
a523278
initial updates to make assert_message not a string literal
vezenovm Jan 17, 2024
31b6e55
Merge branch 'master' into mv/assert-msg-fmtstr
vezenovm Jan 17, 2024
84ec1bc
working resolution of assert messages and runtime
vezenovm Jan 19, 2024
0a084c4
remove old impl
vezenovm Jan 19, 2024
c581cee
revert debugging changes for brillig inputs
vezenovm Jan 19, 2024
73e48fb
cargo fmt
vezenovm Jan 19, 2024
0c46345
remove old ocmment
vezenovm Jan 19, 2024
1cf135d
cargo clippy and cleanup
vezenovm Jan 19, 2024
3123241
cleanup old comments and initial debugging for brillig assert message
vezenovm Jan 19, 2024
08d8922
improved usage of From trait for ForeignCallResults
vezenovm Jan 19, 2024
3284b99
resolve merge conflicts
vezenovm Jan 19, 2024
83605d8
start switching order of evaluation of resolve_assert_message as to n…
vezenovm Jan 22, 2024
7fdf5be
Merge branch 'master' into mv/assert-msg-fmtstr
vezenovm Jan 22, 2024
f131b96
switch order of execution
vezenovm Jan 23, 2024
f253cd2
update parser tests and some cleanup
vezenovm Jan 23, 2024
e149ede
cargo clippy
vezenovm Jan 23, 2024
8eb77ad
add back debug logs lines that were removed
vezenovm Jan 23, 2024
d0234d2
added compile failure tests
vezenovm Jan 23, 2024
0f0cbe0
move transformation of call expression to resolution rather than have…
vezenovm Jan 23, 2024
845e269
Merge branch 'master' into mv/assert-msg-fmtstr
vezenovm Jan 23, 2024
85a40c4
handle parser rrs
vezenovm Jan 23, 2024
e42cb9c
fix create_mock
vezenovm Jan 23, 2024
ec87b69
move to non-optional expr
vezenovm Jan 23, 2024
bc317a0
clippy
vezenovm Jan 23, 2024
9284490
clear out circuits w/ only brillig
vezenovm Jan 23, 2024
4333637
update compile_empty_success test
vezenovm Jan 24, 2024
9bc00eb
fix format
vezenovm Jan 24, 2024
f3083c8
cleanup resolve assert message
vezenovm Jan 24, 2024
185aba1
update debugger handle_foreign_call
vezenovm Jan 24, 2024
27ea4d9
cargo fmt
vezenovm Jan 24, 2024
0c7ff78
fix frontend tests, but acvm_js tests still failing
vezenovm Jan 24, 2024
720e470
Update tooling/nargo/src/ops/execute.rs
vezenovm Jan 24, 2024
8698083
some initial switches to putting resolve_assert_message under a predi…
vezenovm Jan 30, 2024
8458f83
Merge remote-tracking branch 'origin/mv/assert-msg-fmtstr' into mv/as…
vezenovm Jan 30, 2024
1a3ea85
accept changes
vezenovm Jan 30, 2024
480297a
missing merge edit
vezenovm Jan 30, 2024
8de9539
remove unused imports
vezenovm Jan 30, 2024
86cab04
remove old dbg
vezenovm Jan 30, 2024
7afc317
switch assert_message call instruction to be atomic with SSA and add …
vezenovm Jan 31, 2024
55de71f
cleanup decompose_constrain
vezenovm Jan 31, 2024
3ebc34a
some comment cleanup
vezenovm Jan 31, 2024
c0d3403
remove old comments
vezenovm Jan 31, 2024
49e7118
resolve merge conflicts
vezenovm Jan 31, 2024
9944a83
cargo fmt
vezenovm Jan 31, 2024
282a7d7
reorganize codegen of constrain error
vezenovm Jan 31, 2024
4cd9255
defunc cleanup
vezenovm Jan 31, 2024
9796a1b
cleanup
vezenovm Jan 31, 2024
8579816
cleanup brillig assert message gen:
vezenovm Jan 31, 2024
5170bc1
Merge branch 'master' into mv/assert-msg-fmtstr
vezenovm Jan 31, 2024
ae06f9e
macro errs update
vezenovm Jan 31, 2024
4e4d273
add an expect func to option
vezenovm Jan 31, 2024
e516c27
leave option expect for separate branch
vezenovm Jan 31, 2024
0c77f8f
Update compiler/noirc_evaluator/src/ssa/opt/defunctionalize.rs
vezenovm Jan 31, 2024
5cd9335
fixup git suggestion
vezenovm Jan 31, 2024
c8170f3
use AssertMessageMacro when disable_macros is enabled
vezenovm Jan 31, 2024
ae23e5c
chore: reduce diff and fix clippy warnings
TomAFrench Jan 31, 2024
5e0e198
chore: reduce diff
TomAFrench Jan 31, 2024
fa6b50c
format constrain err better
vezenovm Jan 31, 2024
f5598fe
Update compiler/noirc_evaluator/src/ssa/ssa_gen/mod.rs
vezenovm Jan 31, 2024
d3c2f0e
cargo fmt
vezenovm Jan 31, 2024
bb34b45
fix old test updates
vezenovm Jan 31, 2024
819c95a
remove old comment
vezenovm Jan 31, 2024
c62bec8
reduce diff
vezenovm Jan 31, 2024
7f174dc
update assert docs
vezenovm Jan 31, 2024
dd056a1
chore: remove some indentation
TomAFrench Jan 31, 2024
757c740
noir js assert_lt test to show usage of resolve_assert_message
vezenovm Jan 31, 2024
545923e
Merge remote-tracking branch 'origin/mv/assert-msg-fmtstr' into mv/as…
vezenovm Jan 31, 2024
e002ba2
improve comment
vezenovm Jan 31, 2024
c6fe900
add assert_msg_runtime execution failure test to noirJS
vezenovm Jan 31, 2024
1d06de2
prettier
vezenovm Jan 31, 2024
a48f065
Apply suggestions from code review
TomAFrench Feb 1, 2024
6f27d40
chore: delete unnecessary files
TomAFrench Feb 1, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 3 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
[workspace]

members = [
# Macros crates for metaprogramming
"aztec_macros",
"noirc_macros",
# Compiler crates
"compiler/noirc_evaluator",
"compiler/noirc_frontend",
"compiler/noirc_errors",
Expand Down
4 changes: 4 additions & 0 deletions acvm-repo/acir/src/circuit/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,10 @@ pub struct Circuit {
// Note: This should be a BTreeMap, but serde-reflect is creating invalid
// c++ code at the moment when it is, due to OpcodeLocation needing a comparison
// implementation which is never generated.
//
// TODO: These are only used for constraints that are explicitly created during code generation (such as index out of bounds on slices)
// TODO: We should move towards having all the checks being evaluated in the same manner
// TODO: as runtime assert messages specified by the user. This will also be a breaking change as the `Circuit` structure will change.
pub assert_messages: Vec<(OpcodeLocation, String)>,
}

Expand Down
81 changes: 77 additions & 4 deletions acvm-repo/acvm/src/pwg/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
use std::collections::HashMap;

use acir::{
brillig::ForeignCallResult,
brillig::{ForeignCallParam, ForeignCallResult, Value},
circuit::{opcodes::BlockId, Opcode, OpcodeLocation},
native_types::{Expression, Witness, WitnessMap},
BlackBoxFunc, FieldElement,
Expand Down Expand Up @@ -140,6 +140,8 @@ pub struct ACVM<'a, B: BlackBoxFunctionSolver> {
witness_map: WitnessMap,

brillig_solver: Option<BrilligSolver<'a, B>>,

current_assert_message: Option<String>,
}

impl<'a, B: BlackBoxFunctionSolver> ACVM<'a, B> {
Expand All @@ -153,6 +155,7 @@ impl<'a, B: BlackBoxFunctionSolver> ACVM<'a, B> {
instruction_pointer: 0,
witness_map: initial_witness,
brillig_solver: None,
current_assert_message: None,
}
}

Expand Down Expand Up @@ -224,13 +227,25 @@ impl<'a, B: BlackBoxFunctionSolver> ACVM<'a, B> {
/// Resolves a foreign call's [result][acir::brillig_vm::ForeignCallResult] using a result calculated outside of the ACVM.
///
/// The ACVM can then be restarted to solve the remaining Brillig VM process as well as the remaining ACIR opcodes.
pub fn resolve_pending_foreign_call(&mut self, foreign_call_result: ForeignCallResult) {
pub fn resolve_pending_foreign_call(&mut self, foreign_call_result: ACVMForeignCallResult) {
if !matches!(self.status, ACVMStatus::RequiresForeignCall(_)) {
panic!("ACVM is not expecting a foreign call response as no call was made");
}

let brillig_solver = self.brillig_solver.as_mut().expect("No active Brillig solver");
brillig_solver.resolve_pending_foreign_call(foreign_call_result);
match foreign_call_result {
ACVMForeignCallResult::BrilligOutput(foreign_call_result) => {
brillig_solver.resolve_pending_foreign_call(foreign_call_result);
}
ACVMForeignCallResult::ResolvedAssertMessage(assert_message) => {
if assert_message.is_empty() {
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In order to reset the current assertion message I went with inserting a resolve_assert_message call before every constrain and in the case one isn't specified we simply have an empty string. However, I could change this to be a separate boolean flag or something but I didn't think it was very important people got to print empty strings.

self.current_assert_message = None;
} else {
self.current_assert_message = Some(assert_message);
}
brillig_solver.resolve_pending_foreign_call(ForeignCallResult::default());
}
}

// Now that the foreign call has been resolved then we can resume execution.
self.status(ACVMStatus::InProgress);
Expand All @@ -251,7 +266,6 @@ impl<'a, B: BlackBoxFunctionSolver> ACVM<'a, B> {

pub fn solve_opcode(&mut self) -> ACVMStatus {
let opcode = &self.opcodes[self.instruction_pointer];

let resolution = match opcode {
Opcode::AssertZero(expr) => ExpressionSolver::solve(&mut self.witness_map, expr),
Opcode::BlackBoxFuncCall(bb_func) => {
Expand Down Expand Up @@ -376,6 +390,10 @@ impl<'a, B: BlackBoxFunctionSolver> ACVM<'a, B> {
self.brillig_solver = Some(solver);
self.solve_opcode()
}

pub fn get_assert_message(&self) -> &Option<String> {
&self.current_assert_message
}
}

// Returns the concrete value for a particular witness
Expand Down Expand Up @@ -445,3 +463,58 @@ fn any_witness_from_expression(expr: &Expression) -> Option<Witness> {
Some(expr.linear_combinations[0].1)
}
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub enum ACVMForeignCallResult {
BrilligOutput(ForeignCallResult),
ResolvedAssertMessage(String),
}

impl ACVMForeignCallResult {
pub fn get_assert_message(self) -> Option<String> {
match self {
Self::ResolvedAssertMessage(msg) => Some(msg),
_ => None,
}
}

pub fn get_brillig_output(self) -> Option<ForeignCallResult> {
match self {
Self::BrilligOutput(foreign_call_result) => Some(foreign_call_result),
_ => None,
}
}
}

impl From<ForeignCallResult> for ACVMForeignCallResult {
fn from(value: ForeignCallResult) -> Self {
Self::BrilligOutput(value)
}
}

impl From<String> for ACVMForeignCallResult {
fn from(value: String) -> Self {
Self::ResolvedAssertMessage(value)
}
}

impl From<Value> for ACVMForeignCallResult {
fn from(value: Value) -> Self {
let foreign_call_result: ForeignCallResult = value.into();
foreign_call_result.into()
}
}

impl From<Vec<Value>> for ACVMForeignCallResult {
fn from(values: Vec<Value>) -> Self {
let foreign_call_result: ForeignCallResult = values.into();
foreign_call_result.into()
}
}

impl From<Vec<ForeignCallParam>> for ACVMForeignCallResult {
fn from(values: Vec<ForeignCallParam>) -> Self {
let foreign_call_result: ForeignCallResult = values.into();
foreign_call_result.into()
}
}
2 changes: 1 addition & 1 deletion acvm-repo/brillig/src/foreign_call.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ impl ForeignCallParam {
}

/// Represents the full output of a [foreign call][crate::Opcode::ForeignCall].
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Clone)]
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Clone, Default)]
pub struct ForeignCallResult {
/// Resolved output values of the foreign call.
pub values: Vec<ForeignCallParam>,
Expand Down
2 changes: 1 addition & 1 deletion acvm-repo/brillig_vm/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -242,7 +242,7 @@
self.registers.set(*value_index, *value);
}
_ => unreachable!(
"Function result size does not match brillig bytecode (expected 1 result)"
"Function result size does not match brillig bytecode. Expected 1 result but got {output:?}"
),
},
RegisterOrMemory::HeapArray(HeapArray { pointer: pointer_index, size }) => {
Expand Down Expand Up @@ -552,7 +552,7 @@
}

#[test]
fn jmpifnot_opcode() {

Check warning on line 555 in acvm-repo/brillig_vm/src/lib.rs

View workflow job for this annotation

GitHub Actions / Code

Unknown word (jmpifnot)
let input_registers =
Registers::load(vec![Value::from(1u128), Value::from(2u128), Value::from(0u128)]);

Expand Down
1 change: 1 addition & 0 deletions compiler/noirc_driver/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -25,3 +25,4 @@ rust-embed.workspace = true
tracing.workspace = true

aztec_macros = { path = "../../aztec_macros" }
noirc_macros = { path = "../../noirc_macros" }
5 changes: 4 additions & 1 deletion compiler/noirc_driver/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,10 @@ pub fn check_crate(
let macros: Vec<&dyn MacroProcessor> = if disable_macros {
vec![]
} else {
vec![&aztec_macros::AztecMacro as &dyn MacroProcessor]
vec![
&aztec_macros::AztecMacro as &dyn MacroProcessor,
&noirc_macros::AssertMessageMacro as &dyn MacroProcessor,
]
};

let mut errors = vec![];
Expand Down
4 changes: 3 additions & 1 deletion compiler/noirc_evaluator/src/ssa/ir/printer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,9 @@ pub(crate) fn display_instruction(
writeln!(f, "truncate {value} to {bit_size} bits, max_bit_size: {max_bit_size}",)
}
Instruction::Constrain(lhs, rhs, message) => match message {
Some(message) => writeln!(f, "constrain {} == {} '{message}'", show(*lhs), show(*rhs)),
Some(message) => {
writeln!(f, "constrain {} == {} '{message:?}'", show(*lhs), show(*rhs))
}
None => writeln!(f, "constrain {} == {}", show(*lhs), show(*rhs)),
},
Instruction::Call { func, arguments } => {
Expand Down
5 changes: 2 additions & 3 deletions compiler/noirc_evaluator/src/ssa/ssa_gen/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -435,7 +435,7 @@ impl<'a> FunctionContext<'a> {
self.builder.set_location(location).insert_constrain(
sign,
one,
Some("attempt to bit-shift with overflow".to_string()),
Some("attempt to bit-shift with overflow".to_owned()),
);
}

Expand Down Expand Up @@ -509,11 +509,10 @@ impl<'a> FunctionContext<'a> {
let rhs_abs = self.absolute_value_helper(rhs, rhs_sign, bit_size);
let product_field = self.builder.insert_binary(lhs_abs, BinaryOp::Mul, rhs_abs);
// It must not already overflow the bit_size
let message = "attempt to multiply with overflow".to_string();
self.builder.set_location(location).insert_range_check(
product_field,
bit_size,
Some(message.clone()),
Some("attempt to multiply with overflow".to_string()),
);
let product = self.builder.insert_cast(product_field, Type::unsigned(bit_size));

Expand Down
14 changes: 11 additions & 3 deletions compiler/noirc_evaluator/src/ssa/ssa_gen/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ impl<'a> FunctionContext<'a> {
Expression::Call(call) => self.codegen_call(call),
Expression::Let(let_expr) => self.codegen_let(let_expr),
Expression::Constrain(expr, location, assert_message) => {
self.codegen_constrain(expr, *location, assert_message.clone())
self.codegen_constrain(expr, *location, assert_message)
}
Expression::Assign(assign) => self.codegen_assign(assign),
Expression::Semi(semi) => self.codegen_semi(semi),
Expand Down Expand Up @@ -438,6 +438,7 @@ impl<'a> FunctionContext<'a> {

let is_offset_out_of_bounds = self.builder.insert_binary(index, BinaryOp::Lt, array_len);
let true_const = self.builder.numeric_constant(true, Type::bool());

self.builder.insert_constrain(
is_offset_out_of_bounds,
true_const,
Expand Down Expand Up @@ -665,11 +666,18 @@ impl<'a> FunctionContext<'a> {
&mut self,
expr: &Expression,
location: Location,
assert_message: Option<String>,
assert_message: &Option<Box<Expression>>,
) -> Result<Values, RuntimeError> {
let expr = self.codegen_non_tuple_expression(expr)?;
let true_literal = self.builder.numeric_constant(true, Type::bool());
self.builder.set_location(location).insert_constrain(expr, true_literal, assert_message);

assert_message
.as_ref()
.map(|assert_message_expr| self.codegen_expression(assert_message_expr.as_ref()));

// Assert messages from constrain statements specified by the user are codegen'd with a call expression,
// thus the assert_message field here should always be `None`
self.builder.set_location(location).insert_constrain(expr, true_literal, None);

Ok(Self::unit_value())
}
Expand Down
2 changes: 1 addition & 1 deletion compiler/noirc_frontend/src/ast/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -416,7 +416,7 @@ pub enum LValue {
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct ConstrainStatement(pub Expression, pub Option<String>, pub ConstrainKind);
pub struct ConstrainStatement(pub Expression, pub Option<Expression>, pub ConstrainKind);

#[derive(Debug, PartialEq, Eq, Clone, Copy)]
pub enum ConstrainKind {
Expand Down
1 change: 1 addition & 0 deletions compiler/noirc_frontend/src/hir/def_collector/dc_crate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -361,6 +361,7 @@ impl DefCollector {
for macro_processor in macro_processors {
macro_processor.process_typed_ast(&crate_id, context);
}

errors.extend(type_check_globals(&mut context.def_interner, resolved_globals.globals));

// Type check all of the functions in the crate
Expand Down
42 changes: 40 additions & 2 deletions compiler/noirc_frontend/src/hir/resolution/resolver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1119,8 +1119,46 @@ impl<'a> Resolver<'a> {
}
StatementKind::Constrain(constrain_stmt) => {
let expr_id = self.resolve_expression(constrain_stmt.0);
let assert_message = constrain_stmt.1;
HirStatement::Constrain(HirConstrainStatement(expr_id, self.file, assert_message))
let call_resolve_msg_expr = constrain_stmt.1.map(|assert_msg_expr| {
let span = assert_msg_expr.span;
let is_in_stdlib = self.path_resolver.module_id().krate.is_stdlib();
let call_expr = if is_in_stdlib {
Expression::call(
Expression {
kind: ExpressionKind::Variable(Path {
segments: vec![Ident::from("resolve_assert_message")],
kind: PathKind::Crate,
span,
}),
span,
},
vec![assert_msg_expr.clone()],
span,
)
} else {
Expression::call(
Expression {
kind: ExpressionKind::Variable(Path {
segments: vec![
Ident::from("std"),
Ident::from("resolve_assert_message"),
],
kind: PathKind::Dep,
span: Span::default(),
}),
span: Span::default(),
},
vec![assert_msg_expr.clone()],
Span::default(),
)
};
self.resolve_expression(call_expr)
});
HirStatement::Constrain(HirConstrainStatement(
expr_id,
self.file,
call_resolve_msg_expr,
))
}
StatementKind::Expression(expr) => {
HirStatement::Expression(self.resolve_expression(expr))
Expand Down
3 changes: 3 additions & 0 deletions compiler/noirc_frontend/src/hir/type_check/stmt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -305,6 +305,9 @@ impl<'interner> TypeChecker<'interner> {
let expr_type = self.check_expression(&stmt.0);
let expr_span = self.interner.expr_span(&stmt.0);

// Must type check the assertion message expression so that we instantiate bindings
stmt.2.map(|assert_msg_expr| self.check_expression(&assert_msg_expr));

self.unify(&expr_type, &Type::Bool, || TypeCheckError::TypeMismatch {
expr_typ: expr_type.to_string(),
expected_typ: Type::Bool.to_string(),
Expand Down
2 changes: 1 addition & 1 deletion compiler/noirc_frontend/src/hir_def/stmt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ pub struct HirAssignStatement {
/// originates from. This is used later in the SSA pass to issue
/// an error if a constrain is found to be always false.
#[derive(Debug, Clone)]
pub struct HirConstrainStatement(pub ExprId, pub FileId, pub Option<String>);
pub struct HirConstrainStatement(pub ExprId, pub FileId, pub Option<ExprId>);

#[derive(Debug, Clone, Hash)]
pub enum HirPattern {
Expand Down
2 changes: 1 addition & 1 deletion compiler/noirc_frontend/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ pub mod macros_api {
pub use crate::hir_def::expr::{HirExpression, HirLiteral};
pub use crate::hir_def::stmt::HirStatement;
pub use crate::node_interner::{NodeInterner, StructId};
pub use crate::parser::SortedModule;
pub use crate::parser::{parse_program, SortedModule};
pub use crate::token::SecondaryAttribute;

pub use crate::hir::def_map::ModuleDefId;
Expand Down
2 changes: 1 addition & 1 deletion compiler/noirc_frontend/src/monomorphization/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ pub enum Expression {
ExtractTupleField(Box<Expression>, usize),
Call(Call),
Let(Let),
Constrain(Box<Expression>, Location, Option<String>),
Constrain(Box<Expression>, Location, Option<Box<Expression>>),
Assign(Assign),
Semi(Box<Expression>),
}
Expand Down
Loading
Loading