sirasistant
commented
6 months ago Dynamic assert payloads
Current state
Consider the following code containing a "dynamic" assert payload:
```rust
fn option_expect(opt: Option, err: Err) -> T {
assert(opt.is_some(), err);
opt.unwrap_unchecked()
}
fn main(option: Option) -> pub u8 {
option_expect(option, "option is none")
}
```
vs the static assert payload version of the code:
```rust
fn main(option: Option) -> pub u8 {
assert(option.is_some(), "option is none");
option.unwrap_unchecked()
}
```
This is the generated SSA for the static version:
```
Initial SSA:
acir(inline) fn main f0 {
b0(v0: u1, v1: u8):
v3 = call f1(v0, v1)
constrain v3 == u1 1 "option is none"
v6 = call f2(v0, v1)
return v6
}
```
And this one for the "dynamic" version:
```
Initial SSA:
acir(inline) fn main f0 {
b0(v0: u1, v1: u8):
v12 = call f1(v0, v1, [u8 111, u8 2⁴×7, u8 116, u8 105, u8 111, u8 110, u8 2⁵, u8 105, u8 115, u8 2⁵, u8 110, u8 111, u8 110, u8 101])
return v12
}
acir(inline) fn option_expect f1 {
b0(v0: u1, v1: u8, v2: [u8; 14]):
inc_rc v2
v4 = call f2(v0, v1)
v8 = call f2(v0, v1)
inc_rc v2
constrain v4 == u1 1 call f3(v2, v8)
v10 = call f4(v0, v1)
dec_rc v2
return v10
}
acir(inline) fn is_some f2 {
b0(v0: u1, v1: u8):
return v0
}
brillig fn resolve_assert_message f3 {
b0(v0: [u8; 14], v1: u1):
inc_rc v0
v2 = not v1
jmpif v2 then: b1, else: b2
b1():
call v3(v0, [u8 123, u8 34, u8 107, u8 105, u8 110, u8 100, u8 34, u8 58, u8 34, u8 115, u8 116, u8 114, u8 105, u8 110, u8 103, u8 34, u8 44, u8 34, u8 108, u8 101, u8 110, u8 103, u8 116, u8 104, u8 34, u8 58, u8 49, u8 52, u8 125], u1 0)
jmp b2()
b2():
dec_rc v0
return
}
acir(inline) fn unwrap_unchecked f4 {
b0(v0: u1, v1: u8):
return v1
}
```
The dynamic version has undergone some modifications before conversion to SSA. Let's explain what are those:
### Modifications at HIR
```rust
if matches!(
assert_message_expr,
Expression { kind: ExpressionKind::Literal(Literal::Str(..)), .. }
) {
return Some(self.resolve_expression(assert_message_expr));
}
let is_in_stdlib = self.path_resolver.module_id().krate.is_stdlib();
let assert_msg_call_path = if is_in_stdlib {
ExpressionKind::Variable(Path {
segments: vec![Ident::from("internal"), Ident::from("resolve_assert_message")],
kind: PathKind::Crate,
span,
})
} else {
ExpressionKind::Variable(Path {
segments: vec![
Ident::from("std"),
Ident::from("internal"),
Ident::from("resolve_assert_message"),
],
kind: PathKind::Dep,
span,
})
};
let assert_msg_call_args = vec![assert_message_expr.clone(), condition];
let assert_msg_call_expr = Expression::call(
Expression { kind: assert_msg_call_path, span },
assert_msg_call_args,
span,
);
Some(self.resolve_expression(assert_msg_call_expr))
```
At the HIR level, if the assert message is not a **literal** string, a call to `resolve_assert_message` is introduced. This is the implementation of `resolve_assert_message`:
```rust
#[oracle(assert_message)]
unconstrained fn assert_message_oracle(_input: T) {}
unconstrained pub fn resolve_assert_message(input: T, condition: bool) {
if !condition {
assert_message_oracle(input);
}
}
```
This explains this added function in the SSA:
```
...
constrain v4 == u1 1 call f3(v2, v8)
...
brillig fn resolve_assert_message f3 {
b0(v0: [u8; 14], v1: u1):
inc_rc v0
v2 = not v1
jmpif v2 then: b1, else: b2
b1():
call v3(v0, [u8 123, u8 34, u8 107, u8 105, u8 110, u8 100, u8 34, u8 58, u8 34, u8 115, u8 116, u8 114, u8 105, u8 110, u8 103, u8 34, u8 44, u8 34, u8 108, u8 101, u8 110, u8 103, u8 116, u8 104, u8 34, u8 58, u8 49, u8 52, u8 125], u1 0)
jmp b2()
b2():
dec_rc v0
return
}
```
### Modifications at monomorphization
After monomorphization, the assert_message oracle call is modified with metadata about the type it's being called with, in a similar way as the print opcode.
```rust
if let ast::Expression::Ident(ident) = original_func.as_ref() {
if let Definition::Oracle(name) = &ident.definition {
if name.as_str() == "print" {
// Oracle calls are required to be wrapped in an unconstrained function
// The first argument to the `print` oracle is a bool, indicating a newline to be inserted at the end of the input
// The second argument is expected to always be an ident
self.append_printable_type_info(&hir_arguments[1], &mut arguments);
} else if name.as_str() == "assert_message" {
// The first argument to the `assert_message` oracle is the expression passed as a message to an `assert` or `assert_eq` statement
self.append_printable_type_info(&hir_arguments[0], &mut arguments);
}
}
}
```
The metadata is the serialized ABI of the type:
```rust
fn append_printable_type_info_inner(typ: &Type, arguments: &mut Vec) {
// Disallow printing slices and mutable references for consistency,
// since they cannot be passed from ACIR into Brillig
if matches!(typ, HirType::MutableReference(_)) {
unreachable!("println and format strings do not support mutable references.");
}
let printable_type: PrintableType = typ.into();
let abi_as_string = serde_json::to_string(&printable_type)
.expect("ICE: expected PrintableType to serialize");
arguments.push(ast::Expression::Literal(ast::Literal::Str(abi_as_string)));
}
```
This explains the call to v3 (assert_message) in SSA:
```
brillig fn resolve_assert_message f3 {
b0(v0: [u8; 14], v1: u1):
inc_rc v0
v2 = not v1
jmpif v2 then: b1, else: b2
b1():
call v3(v0, [u8 123, u8 34, u8 107, u8 105, u8 110, u8 100, u8 34, u8 58, u8 34, u8 115, u8 116, u8 114, u8 105, u8 110, u8 103, u8 34, u8 44, u8 34, u8 108, u8 101, u8 110, u8 103, u8 116, u8 104, u8 34, u8 58, u8 49, u8 52, u8 125], u1 0)
jmp b2()
b2():
dec_rc v0
return
}
```
As can be seen here, the oracle call to assert_message includes not only the string v0 but also a literal byte array, that being the abi_as_string.
### Compilation and runtime
This strategy will make it so when evaluating this instruction `constrain v4 == u1 1 call f3(v2, v8)` (the assertion on is_some()) a brillig call will be issued to a resolve_assert_message with the string and the condition. Then the brillig function will conditionally call the assert_message oracle with the string + extra metadata if the condition is false.
But how is this assert_message oracle related with the original assertion?
The runtime (acvm_js and nargo) recognizes this special oracle, parses the type using the metadata, stores the parsed result, and when the circuit fails, it has in cache the last call to assert_message.
### Comparison with static assert messages
With static assert messages, no transformations happen on the frontend. The generated SSA
```
Initial SSA:
acir(inline) fn main f0 {
b0(v0: u1, v1: u8):
v3 = call f1(v0, v1)
constrain v3 == u1 1 "option is none"
v6 = call f2(v0, v1)
return v6
}
```
gets compiled to ACIR and in compilation to ACIR, the literal string is stored in a Map inside the circuit. So when the circuit fails, the runtime just picks what String is stored there for the failing opcode.
If the function is brillig, instead of being added to the Map the error string is directly returned as revert data.
Challenges with current state
This approach, altough a bit fragile (since modifications in SSA assertions need to account for dynamic assertions, or bugs like this one can happen) works fine for circuits. But it poses some challenges for public functions in aztec:
- The runtime is required to know about dynamic assertions, storing the error payload for a later error. This is quite problematic for the implementation of the VM, since it would need to emulate what acvm_js is doing right now.
- Metadata about the type is embedded in the bytecode. This would increase bytecode size and runtime cost for public functions, with this data only being relevant for tooling.
- There is a small extra cost of adding an extra function call for constrains, but it should be easily removed by inlining.
Alternative approach
Instead of using an entirely new approach for dynamic assertion messages, we can follow the same approach that we have for static assertion messages. The Map<OpcodeLocation, String> that the circuit struct holds could be extended to be a Map<OpcodeLocation, AssertionData> The type AssertionData would be:
struct AssertionData {
typing_metadata: PrintableType, // This is what is currently serialized into the bytecode.
payload: AssertionPayload
};
enum AssertionPayload {
Witness(Vec<Expression>),
MemoryArray(BlockId),
BrilligOutput, // The brillig VM returns the data directly in revert data
}So the example code:
fn option_expect<T, Err>(opt: Option<T>, err: Err) -> T {
assert(opt.is_some(), err);
opt.unwrap_unchecked()
}
fn main(option: Option<u8>) -> pub u8 {
option_expect(option, "option is none")
}would generate the following SSA:
Initial SSA:
acir(inline) fn main f0 {
b0(v0: u1, v1: u8):
v12 = call f1(v0, v1, [u8 111, u8 2⁴×7, u8 116, u8 105, u8 111, u8 110, u8 2⁵, u8 105, u8 115, u8 2⁵, u8 110, u8 111, u8 110, u8 101])
return v12
}
acir(inline) fn option_expect f1 {
b0(v0: u1, v1: u8, v2: [u8; 14]):
inc_rc v2
v4 = call f2(v0, v1)
inc_rc v2
constrain v4 == u1 1 v2 // Notice here constrain directly holds an SSA value
v10 = call f4(v0, v1)
dec_rc v2
return v10
}
acir(inline) fn is_some f2 {
b0(v0: u1, v1: u8):
return v0
}
acir(inline) fn unwrap_unchecked f4 {
b0(v0: u1, v1: u8):
return v1
}ACIR generation and Brillig generation need access to the PrintableType metadata that is generated from the HIR for all non-string assert payloads. It could be maintained in parallel or directly embedded in the constrain instruction in SSA, altough the latter sounds worse. This is necessary since we need to build the AssertionData defined above.
When an opcode fails, the ACVM immediately has enough data to:
- Extract the payload of the failing opcode
- Know the types of the failing opcode payload and how they could be printed for an user.
Advantages of this approach
- Supporting static non-string assertion payloads
- Removes any notion of PrintableType from the bytecode, maintaining metadata outside.
- No more need to cache oracle calls to figure out the payload for a failing assertion.
- The constrain instruction just holds a regular SSA value. No need to special case it for everything like we have to do with the call to resolve_assert_message that has a parallel version of the constrain condition, etc.
- The distinction of static constrain payload or dynamic constrain payload happens after SSA optimization. So any payload that can be determined static via optimization wouldn't end up in the bytecode, unlike now (in fact my example above should be determined constant at inlining!)
- AVM support would now be easy, since no extraneous oracles have been added. Brillig gen just has to properly serialize the passed in type (possibly using the same serialization strategy as oracle calls have).
Updates to the proposal:
No metadata in the circuit struct
We can avoid storing metadata about assertion payload types in the circuit struct if we put it in the ABI.
The circuit struct will have a map of Map<OpcodeLocation, AssertionPayload> instead of Map<OpcodeLocation, AssertionData>. The metadata about the type of the error payload will live in the ABI instead. Nargo and other runners are then responsible to properly format the error data.
TomAFrench
Problem
This TODO was added in https://github.com/noir-lang/noir/pull/4101. This is due to having two different strategies for resolving constrain instruction error messages which can be seen in this enum (https://github.com/noir-lang/noir/blob/afcb385daa572f990178eda51faf10dc20acd2d0/compiler/noirc_evaluator/src/ssa/ir/instruction.rs#L5730). We have two different strategies as sometimes when doing SSA codegen we want to include a constrain with a message, but we can't easily codegen a call to
resolve_assert_messagein the same way we do for user provided assertion messages. Thus, we have thisassert_messagesmap for resolving messages specified by the compiler and separate calls toresolve_assert_messagefor handling assert messages specified by the user.Happy Case
We should unify the strategy for specifying errors and error types. Ideally we would remove the
assert_messagesmap from theCircuittype. We most likely could instead store errors and their respective types on the ABI rather than on the circuit. Upon circuit failure we can then use the ABI for fetching the appropriate error.Some example pseudocode written by @TomAFrench from when we were originally planning #4101.
Unifying these constrain errors would essentially require full structured errors as part of the ABI. We could then have followup work to enable custom errors inside Noir similar to https://soliditylang.org/blog/2021/04/21/custom-errors/.
Alternatives Considered
No response
Additional Context
No response
Would you like to submit a PR for this Issue?
No
Support Needs
No response