Enforce ExecutionState transition#110
Conversation
| if self.next.execution_state == ExecutionState.BeginTx: | ||
| assert self.curr.execution_state == ExecutionState.EndTx | ||
| elif self.next.execution_state == ExecutionState.EndTx: | ||
| assert self.curr.execution_state.halts() or self.curr.execution_state == ExecutionState.BeginTx |
There was a problem hiding this comment.
what is the case of the BeginTx direct follows by EndTx ?
There was a problem hiding this comment.
When callee has empty code. But we could also remove this branch if we decide to always dive into call, even if code is empty.
han0110
force-pushed
the
feature/execution-state-transition
branch
from
ac5e5cf to
2a78c98
Compare
| for idx in range(len(steps) - 1): | ||
| curr, next = steps[idx], steps[idx + 1] |
There was a problem hiding this comment.
We could do something like
| for idx in range(len(steps) - 1): | |
| curr, next = steps[idx], steps[idx + 1] | |
| for curr, _next in zip(steps, steps[1:]): |
This works even if steps has 1 element.
There was a problem hiding this comment.
I just found we still need the idx, so I keep the current version. Also in #116, we can't extend the steps with a None, so iterating on range seems easier.
| return [ | ||
| (self, opcode, stack_pointer, 0) for opcode, stack_pointer in stack_overflow_pairs() | ||
| ] | ||
| else: |
There was a problem hiding this comment.
Since you remove these tags from the fixed table, what will be the strategy to prove that that an opcode can be "invalid", be a "state write" or cause a "stack overflow/underflow"?
Also, with this deletion the functions invalid_opcodes, state_write_opcodes, stack_underflow_pairs and stack_overflow_pairs are no longer used. Will they be used elsewhere? Or can they be removed?
There was a problem hiding this comment.
Since you remove these tags from the fixed table, what will be the strategy to prove that that an opcode can be "invalid", be a "state write" or cause a "stack overflow/underflow"?
I am thinking we can put all these stuff in Fixed::ResponsibleOpcode, and make use of the unused fourth column as auxiliary data. I was planning to add them in the following PR, but let me add them now to make it clear.
For invalid opcodes, the ExecutionState::ErrorInvalidOpcode should be responsible for them (weird but I think it somehow makes sense).
For state write opcodes, we only use them when ExecutionState::ErrorWriteProtection, so it's responsible for them.
For stack overflow/underflow, we can reduce to a single state ExecutionState::ErrorStack, with the stack_pointer in fourth column.
Also, with this deletion the functions
invalid_opcodes,state_write_opcodes,stack_underflow_pairsandstack_overflow_pairsare no longer used. Will they be used elsewhere? Or can they be removed?
I am going to add those pairs mentioned above into Fixed::ResponsibleOpcode sub-table, then these fns will be used.
There was a problem hiding this comment.
Markdown and table are fixed in 044f4f6.
han0110
force-pushed
the
feature/execution-state-transition
branch
from
044f4f6 to
2501f3f
Compare
|
A part from the possible typo mentioned in #110 (comment) the rest LGTM! |
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
4 participants
This PR aims to add missing
ExecutionStatetransition constraint. Currently there are 3 ofExecutionStates which need to be protected to avoid non-halting opcodes trying to halt unexpectedly. They are:BeginTx- Can only fromEndTxEndTx- Can only fromExecutionStatewhich halts orBeginTxEndBlock- Can only fromEndTxorEndBlockAlso it adds some missing
ErrorOutOfGascases and remove some unused information.