fix(avm)!: pre-audit review of context.pil#19549
Conversation
Flakey Tests🤖 says: This CI run detected 5 tests that failed, but were tolerated due to a .test_patterns.yml entry. |
| // Selectors related to exiting a nested context | ||
| pol commit nested_return; // @boolean (by definition) | ||
| nested_return = has_parent_ctx * sel_execute_return; | ||
| pol commit nested_failure; // @boolean (by definition) | ||
| nested_failure = has_parent_ctx * sel_failure; | ||
| // Since `sel_exit_call = sel_failure + sel_execute_return`, we can define the following alias | ||
| // to characterize exiting from a nested context. | ||
| pol NESTED_EXIT_CALL = nested_failure + nested_return; // = has_parent_ctx * sel_exit_call; |
There was a problem hiding this comment.
Is it true that sel_execute_return can only be 1 if there has been no failure? The opcode cannot fail during its execution?
There was a problem hiding this comment.
Exactly, this comes from #[INFALLIBLE_OPCODES_SUCCESS] and this explanation is present before the definition of sel_exit_call.
We use this property a lot. Basically, when an opcode selector is turned on in execution, it means that the only error which might occur is an opcode error. #[INFALLIBLE_OPCODES_SUCCESS] prevents to turn on this error for those we know will not fail such as RETURN.
| // Initialization: enqueued_call_start = 1 ==> parent_calldata_addr = 0; | ||
| // Propagation: | ||
| // NESTED_EXIT_CALL = 1 ==> constraints come from lookups (#[CTX_STACK_ROLLBACK] and #[CTX_STACK_RETURN]) | ||
| // sel_enter_call = 1 ==> parent_calldata_addr' = rop[4] (resolved operand 5 from execution trace) |
There was a problem hiding this comment.
just confirming that rop[4] does indeed correspond to resolved operand 5, or is this a typo?
There was a problem hiding this comment.
These comments were already present and are all "incrementing the index by one" because humans like to start by index one. I think it is misleading and will remove such indices in the comment and just keep "from execution trace".
| // RETRIEVED BYTECODES TREE | ||
| // ============================= | ||
|
|
||
| // Here, we constrain the transition `retrieved_bytecodes_tree_root` to `prev_retrieved_bytecodes_tree_size` |
There was a problem hiding this comment.
This confuses me. Why would retrieved_*root transition to prev_*root? And i think you have a typo here because you say *root to *size
There was a problem hiding this comment.
Oh we're not really transitioning? We're saying "on the next row, make sure that prev_*root points to this row's root? I'd reword to make clearer.
| // The state of the retrieved bytecodes tree should be continuous unless we have finished an enqueued call. | ||
| // `prev_retrieved_bytecodes_tree_root` and `prev_retrieved_bytecodes_tree_size` are initialized | ||
| // on `enqueued_call_start == 1` as part of the permutation (#[DISPATCH_EXEC_START] in tx.pil). | ||
| // The final values at the end of an enqueued call are sent back to the tx trace in the lookup #[DISPATCH_EXEC_END]. |
There was a problem hiding this comment.
What does it mean for the bytecodes tree to be continuous? I'd clarify that it can evolve during an enqueued call as bytecodes are retrieved. And then we don't actually constrain that it propagates in context.pil at enqueued-call boundaries because it is sent-back and initialized like you say. Maybe just clarify the meaning of continuous.
There was a problem hiding this comment.
I added clarifications on what we mean by continuous.
| pol commit transaction_fee; | ||
| // Constrained boolean by tx trace for enqueued call, #[IS_STATIC_NEXT_ROW] during normal execution, | ||
| // IS_STATIC_IF_STATIC_CALL+IS_STATIC_IF_CALL_FROM_STATIC_CONTEXT for nested calls, | ||
| // and CTX_STACK_CALL for returns or failures. | ||
| pol commit is_static; |
There was a problem hiding this comment.
Why remove comment? Is it made clear elsewhere?
There was a problem hiding this comment.
I see that you add @boolean with a note later, although it doesn't specify exactly how is_static is constrained to be bool
There was a problem hiding this comment.
Added some explanations.
576d813 to
ad16c1c
Compare
ad16c1c to
81a7651
Compare
BEGIN_COMMIT_OVERRIDE fix(avm): Fix relative addressing in fuzzer (#19550) feat(avm): avm fuzzer bytecode mutation (#19378) chore(avm): there is automatic conversion from uint128_t to FF chore(avm): ECC pre-audit - normalise infinity points (#19462) feat(bb-pilcom): single-component graph check (#19578) feat(avm): contract class mutation (#19498) chore: support uint128_t in uint256_t construction (#19581) fix!: remove unused column in update_check.pil (#19557) fix(avm)!: pre-audit review of context.pil (#19549) fix(avm): Relax fuzzer memory manager asserts (#19591) fix!: sha256.pil missing input propagation constraints (#19590) END_COMMIT_OVERRIDE
Linear issue: AVM-44