Undo ULM changes to make CALL* and CREATE* opcodes execute in a single call frame#47
Undo ULM changes to make CALL* and CREATE* opcodes execute in a single call frame#47Robertorosmaninho wants to merge 28 commits intoulmfrom
Conversation
… modification needed to executed everything in a single call frame
Robertorosmaninho
force-pushed
the
moving-call-create-to-inner-execution
branch
from
52b622b to
f996f52
Compare
…eeded was already merged
Robertorosmaninho
force-pushed
the
moving-call-create-to-inner-execution
branch
from
007a9f3 to
f77decb
Compare
| rule [call.true]: | ||
| <k> #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC | ||
| => #callWithCode ACCTFROM ACCTTO ACCTCODE GetAndResolveCode(ACCTCODE) VALUE APPVALUE ARGS STATIC | ||
| ... | ||
| </k> | ||
|
|
||
| rule [call.false]: | ||
| <k> #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC | ||
| => #callWithCode ACCTFROM ACCTTO ACCTCODE .Bytes VALUE APPVALUE ARGS STATIC | ||
| ... | ||
| </k> [owise] |
There was a problem hiding this comment.
It seems to me that the LHS of the call.true and call.false rules have overlapping instances, since, in either case, it seems like the LHS is totally unconstrained.
It's just that, based on the names of these rules and the values of their RHS, I would expect that they do not overlap.
There was a problem hiding this comment.
I've added requires AccountExists(ACCTCODE) to differentiate them
| rule [call]: | ||
| <k> CALL _GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH | ||
| => #return RETSTART RETWIDTH Call(GCALL, ACCTTO, VALUE, #range(LM, ARGSTART, ARGWIDTH)) | ||
| => AccessAccount(ACCTTO) |
There was a problem hiding this comment.
The AccessAccount operation in the rules defining the CALL family of opcodes seems redundant because the #mkCall operation also seems to call AccessAccount.
| ```vlm | ||
| syntax InternalOp ::= "#newAccount" Int | ||
| // ------------------------------------- | ||
|
|
||
| rule <k> #create ACCTFROM ACCTTO VALUE INITCODE | ||
| => IncrementNonce(ACCTFROM) | ||
| ~> #pushCallStack ~> #pushWorldState | ||
| ~> #newAccount ACCTTO | ||
| ~> #transferFundsFrom ACCTFROM ACCTTO VALUE | ||
| ~> #mkCreate ACCTFROM ACCTTO VALUE INITCODE | ||
| ... | ||
| </k> | ||
|
|
||
| rule <k> #mkCreate ACCTFROM ACCTTO VALUE INITCODE | ||
| => AccessAccount(ACCTFROM) ~> AccessAccount(ACCTTO) ~> IncrementNonceOnCreate(ACCTTO, $SCHEDULE) ~> #loadProgram INITCODE ~> #initVM ~> #execute | ||
| ... | ||
| </k> | ||
| <id> _ => ACCTTO </id> | ||
| <gas> _GAVAIL => GCALL </gas> | ||
| <callGas> GCALL => 0 </callGas> | ||
| <caller> _ => ACCTFROM </caller> | ||
| <callDepth> CD => CD +Int 1 </callDepth> | ||
| <callData> _ => .Bytes </callData> | ||
| <callValue> _ => VALUE </callValue> | ||
|
|
||
| rule <k> #newAccount ACCT => #if NewAccount(ACCT) #then .K #else #end EVMC_ACCOUNT_ALREADY_EXISTS #fi ... </k> | ||
| ``` | ||
| ```reth | ||
| syntax InternalOp ::= "#newAccount" Int Int Int | ||
| // --------------------------------------------- | ||
|
|
||
| rule <k> #create ACCTFROM ACCTTO VALUE INITCODE | ||
| => IncrementNonce(ACCTFROM) | ||
| ~> #pushCallStack ~> #pushWorldState | ||
| ~> #newAccount ACCTFROM ACCTTO VALUE | ||
| ~> #mkCreate ACCTFROM ACCTTO VALUE INITCODE | ||
| ... | ||
| </k> | ||
|
|
||
| rule <k> #mkCreate ACCTFROM ACCTTO VALUE INITCODE => #loadProgram INITCODE ~> #initVM ~> #execute ... </k> | ||
| <id> _ => ACCTTO </id> | ||
| <gas> _GAVAIL => GCALL </gas> | ||
| <callGas> GCALL => 0 </callGas> | ||
| <caller> _ => ACCTFROM </caller> | ||
| <callDepth> CD => CD +Int 1 </callDepth> | ||
| <callData> _ => .Bytes </callData> | ||
| <callValue> _ => VALUE </callValue> |
There was a problem hiding this comment.
I'm not sure how much this matters since I think the vlm version will not be maintained much longer --- but if we do want to maintain both versions, we can isolate the difference in behaviors between these two versions in a single rule.
That is, we could have #create and #mkCreate have the same behavior in both versions and make the #newAccount operation contain all of the divergent behaviors including:
- the account accesses
- the nonce increment on ACCTTO
- the account existence check (which uses a different internal hook)
There was a problem hiding this comment.
I've simplified this a bit here. I didn't merge all the rules to maintain a minimal separation of responsibilities and to avoid clustering one single rule that does three different things. Let me know if you're happy with this version or want me to proceed with merging #NewAccount and #mkCreate
| ... | ||
| </k> | ||
| <callGas> GCALL </callGas> | ||
| <id> ACCT </id> |
There was a problem hiding this comment.
I'm a bit surprised that the create-invalid and create2-invalid cases return error EVMC_OUT_OF_GAS when the predicate #hasValidInitCode fails --- instead of some more specific error. I checked to see if Geth also follows this pattern but I wasn't able to deduce its behavior after a few minutes of checking.
I definitely don't know the expected behavior in this case, so if someone else could confirm this behavior, that would be helpful.
There was a problem hiding this comment.
Well, the EIP that introduced it doesn't mention a specific exception, but this feature was implemented with the gas limit as background: https://github.com/ethereum/EIPs/blob/master/EIPS/eip-3860.md
Robertorosmaninho
force-pushed
the
moving-call-create-to-inner-execution
branch
from
8347c4c to
cd87cd8
Compare
Adding `requires AccountExists` to `call.true`
sskeirik
left a comment
sskeirik
left a comment
There was a problem hiding this comment.
This looks good!
I just have one minor comment, but I'm approving now --- feel free to handle it as you like.
| => #transferFundsFrom ACCTFROM ACCTTO VALUE | ||
| ~> #if NewAccount(ACCTTO) #then .K #else #end EVMC_ACCOUNT_ALREADY_EXISTS #fi | ||
| ... |
There was a problem hiding this comment.
The order of operations seems strange here --- I would expect that we check for account existence before transferring funds --- since, in a CREATE context, the funds are intended to be transferred to a newly created account only (and not to an existing account that happens to have the same address).
The old code also had the order of these two operations switched.
However, in the end, it may not matter, for two reasons:
- The
#end EVMC_ACCOUNT_ALREADY_EXISTSmight induce a state revert which undoes this transfer; - More importantly, this codepath may never be used since we're moving to Reth.
Robertorosmaninho
force-pushed
the
moving-call-create-to-inner-execution
branch
5 times, most recently
from
51124be to
12a46fb
Compare
2 participants
No description provided.