-
Notifications
You must be signed in to change notification settings - Fork 613
feat: constrain call #13758
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: constrain call #13758
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,17 +1,79 @@ | ||
| // This is a virtual gadget, which is part of the execution trace. | ||
| namespace execution; | ||
|
|
||
| // Useful to define some opcodes within this pil file | ||
| // Constrained to be boolean by execution instruction spec table | ||
| pol commit call_sel; | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. didn't we just discuss maybe we want
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. hmm ok i get confused by our naming conventions..i dont have a strong opinion outside of it being easy for me to remember the convention 😅 . We have some that are
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'd say we use
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. BTW when I say they all start with sel, I mean in PIL. Of course in tracegen etc you'll have them all prefixed by namespace.
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Won't you also have this in the execution trace eventually?
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this is actually the one from the execution trace..but you are right that perhaps i should move this to the execution.pil rather than this virtual trace. I had it in here because my intuition is that most of the relations involving |
||
| pol commit static_call_sel; | ||
| pol CALL = call_sel + static_call_sel; // Guaranteed to be mutually exclusive | ||
| // CALL & precomputed.first_row are NAND | ||
| CALL * precomputed.first_row = 0; | ||
|
fcarreiro marked this conversation as resolved.
|
||
|
|
||
| // Context columns | ||
| pol commit context_id; | ||
| pol commit parent_id; | ||
| pol commit pc; | ||
| pol commit next_pc; | ||
| pol commit msg_sender; | ||
| pol commit contract_address; | ||
|
|
||
| pol commit is_static; | ||
| is_static * (1 - is_static) = 0; | ||
| pol commit is_static; // Constrained boolean by tx trace | ||
|
IlyasRidhuan marked this conversation as resolved.
Outdated
|
||
|
|
||
| pol commit parent_calldata_offset_addr; | ||
| pol commit parent_calldata_size_addr; | ||
|
|
||
| pol commit last_child_returndata_offset_addr; | ||
| pol commit last_child_returndata_size_addr; | ||
| pol commit last_child_success; // Careful with this for now... | ||
|
|
||
| // ==== Helper columns ==== | ||
| // TODO: These context modifiers also need to factor in when a new enqueued call occurs | ||
| // REPLACE prefixed precomputed.first_row in relations with actual phase / enqueued call change | ||
|
|
||
| // next_context_id increments with each invocation of an external call or new enqueued call | ||
| pol commit next_context_id; // Can be replaced by clk | ||
| // The initial next_context_id = 2, in row = 1 | ||
| #[INCR_CONTEXT_ID] | ||
| (1- precomputed.first_row) * sel' * (next_context_id' - (next_context_id + CALL)) = 0; | ||
|
IlyasRidhuan marked this conversation as resolved.
Outdated
|
||
|
|
||
| // CALL = 1 <==> context_id' = next_context_id | ||
| // CALL = 0 <==> context_id' = context_id | ||
|
IlyasRidhuan marked this conversation as resolved.
|
||
| #[NEXT_CONTEXT_ID] | ||
| (1- precomputed.first_row) * sel' * ((next_context_id - context_id) * CALL + context_id + precomputed.first_row - context_id') = 0; | ||
|
|
||
| // CALL = 1 <==> parent_id' = context_id | ||
| // CALL = 0 <==> parent_id' = parent_id | ||
|
IlyasRidhuan marked this conversation as resolved.
|
||
| #[NEXT_PARENT_ID] | ||
| (1- precomputed.first_row) * sel' * ((context_id - parent_id) * (CALL + precomputed.first_row) + parent_id - parent_id') = 0; | ||
|
|
||
| // CALL = 1 <==> pc' = 0 | ||
| // CALL = 0 <==> pc' = next_pc | ||
| #[NEXT_PC] | ||
| (1- precomputed.first_row) * sel' * (pc' - ((1 - CALL) * next_pc)) = 0; | ||
|
|
||
| // CALL = 1 <==> msg_sender' = contract_address | ||
| // CALL = 0 <==> msg_sender' = msg_sender | ||
| #[NEXT_MSG_SENDER] | ||
| (1- precomputed.first_row) * sel' * ((contract_address - msg_sender) * CALL + msg_sender - msg_sender') = 0; | ||
|
|
||
| // CALL = 1 <==> contract_address' = reg3 (intermediate register 3 from execution trace) | ||
| // CALL = 0 <==> contract_address' = contract_address | ||
| #[NEXT_CONTRACT_ADDR] | ||
| (1- precomputed.first_row) * sel' * ((reg3 - contract_address) * CALL + contract_address - contract_address') = 0; | ||
|
|
||
| // CALL = 1 && static_call = 1 <==> is_static' = 1 | ||
| // CALL = 1 && static_call = 0 <==> is_static' = 0 | ||
| // CALL = 0 && static_call = 0 <==> is_static' = is_static | ||
| #[NEXT_IS_STATIC] | ||
| (1- precomputed.first_row) * sel' * (is_static' - (static_call_sel + (1 - CALL) * is_static)) = 0; | ||
|
|
||
| // CALL = 1 <==> parent_calldata_offset_addr' = rop4 (resolved operand 4 from execution trace) | ||
| // CALL = 0 <==> parent_calldata_offset_addr' = parent_calldata_offset_addr | ||
| #[NEXT_CD_OFFSET] | ||
| (1- precomputed.first_row) * sel' * ((rop4 - parent_calldata_offset_addr) * CALL + parent_calldata_offset_addr - parent_calldata_offset_addr') = 0; | ||
|
|
||
| // CALL = 1 <==> parent_calldata_size_addr' = rop5 (resolved operand 5 from execution trace) | ||
| // CALL = 0 <==> parent_calldata_size_addr' = parent_calldata_size_addr | ||
| #[NEXT_CD_SIZE] | ||
| (1- precomputed.first_row) * sel' * ((rop5 - parent_calldata_size_addr) * CALL + parent_calldata_size_addr - parent_calldata_size_addr') = 0; | ||
|
|
||
|
|
||
Large diffs are not rendered by default.
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -30,7 +30,6 @@ class ContextInterface { | |
| virtual void set_next_pc(uint32_t new_next_pc) = 0; | ||
| virtual bool halted() const = 0; | ||
| virtual void halt() = 0; | ||
|
|
||
| virtual uint32_t get_context_id() const = 0; | ||
|
|
||
| // Environment. | ||
|
|
@@ -166,16 +165,20 @@ class EnqueuedCallContext : public BaseContext { | |
| // Event Emitting | ||
| ContextEvent serialize_context_event() override | ||
| { | ||
| return { .id = get_context_id(), | ||
| .pc = get_pc(), | ||
| .msg_sender = get_msg_sender(), | ||
| .contract_addr = get_address(), | ||
| .is_static = get_is_static(), | ||
| .parent_cd_addr = 0, | ||
| .parent_cd_size_addr = 0, | ||
| .last_child_rd_addr = get_last_rd_offset(), | ||
| .last_child_rd_size_addr = get_last_rd_size(), | ||
| .last_child_success = get_last_success() }; | ||
| return { | ||
| .id = get_context_id(), | ||
| .parent_id = 0, | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. this is the main thing that changed (besides formatting) |
||
| .pc = get_pc(), | ||
| .next_pc = get_next_pc(), | ||
| .msg_sender = get_msg_sender(), | ||
| .contract_addr = get_address(), | ||
| .is_static = get_is_static(), | ||
| .parent_cd_addr = 0, | ||
| .parent_cd_size_addr = 0, | ||
| .last_child_rd_addr = get_last_rd_offset(), | ||
| .last_child_rd_size_addr = get_last_rd_size(), | ||
| .last_child_success = get_last_success(), | ||
| }; | ||
| }; | ||
|
|
||
| // Input / Output | ||
|
|
@@ -220,13 +223,20 @@ class NestedContext : public BaseContext { | |
| // Event Emitting | ||
| ContextEvent serialize_context_event() override | ||
| { | ||
| return { .id = get_context_id(), | ||
| .pc = get_pc(), | ||
| .msg_sender = get_msg_sender(), | ||
| .contract_addr = get_address(), | ||
| .is_static = get_is_static(), | ||
| .parent_cd_addr = parent_cd_offset, | ||
| .parent_cd_size_addr = parent_cd_size }; | ||
| return { | ||
| .id = get_context_id(), | ||
| .parent_id = parent_context.get_context_id(), | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. same here |
||
| .pc = get_pc(), | ||
| .next_pc = get_next_pc(), | ||
| .msg_sender = get_msg_sender(), | ||
| .contract_addr = get_address(), | ||
| .is_static = get_is_static(), | ||
| .parent_cd_addr = parent_cd_offset, | ||
| .parent_cd_size_addr = parent_cd_size, | ||
| .last_child_rd_addr = get_last_rd_offset(), | ||
| .last_child_rd_size_addr = get_last_rd_size(), | ||
| .last_child_success = get_last_success(), | ||
| }; | ||
| }; | ||
|
|
||
| // Input / Output | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -28,6 +28,9 @@ struct ExecutionEvent { | |
| // todo(ilyas): this is a vector because GETCONTRACTINSTANCE has 2 outputs, we should change this to 1 | ||
| std::vector<TaggedValue> output; | ||
|
|
||
| // Context Id for the next context. | ||
| uint32_t next_context_id; | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why do we need, for every event, the NEXT context id? Why not the current and why an id at all? (I'm not asking for a change, but an explanation :) )
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Ah good question (this holds for enqueued calls but it's easier just to consider nested calls for now). The current id is stored within the context event - it's needed to uniquely identify a context when interacting with the stack AND it is used as the space_id for memory (we should really deprecate the use of space_id IMO). When we encounter a call we need to assign a new unique id to the new context. We cannot just increment the current id because we could have hit a
If we just incremented the current ID = 1, we would get a duplicate context with ID = 2. In order to know that we the next ID is 3 we have to track it at a global level (which is why this doesnt live in context) and this was the easiest way i could think of - maybe we could do some trick with the stack?
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. ah I get it, it's the "next available context id". I thought it was something weird like "ok this is the context id of the call i'm about to go in to". Consider name change (or comment) but not needed. |
||
|
|
||
| // Sub-events. | ||
| AddressingEvent addressing_event; | ||
| ContextEvent context_event; | ||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.