only check nonce on CREATE and CREATE2 (#2310)

* only check nonce on CREATE and CREATE2

* remove failing test

* Set Version: 1.0.459

* Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

Co-authored-by: Andrei Văcaru <[email protected]>

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.462"
+version = "1.0.463"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.462'
+VERSION: Final = '1.0.463'

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -1286,7 +1286,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
          </account>
       requires #rangeNonce(NONCE)
 
-    rule <k> #checkCall ACCT VALUE => #checkBalanceUnderflow ACCT VALUE ~> #checkDepthExceeded ~> #checkNonceExceeded ACCT ... </k>
+    rule <k> #checkCall ACCT VALUE => #checkBalanceUnderflow ACCT VALUE ~> #checkDepthExceeded ... </k>
 
     rule <k> #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC
           => #callWithCode ACCTFROM ACCTTO ACCTCODE CODE VALUE APPVALUE ARGS STATIC
@@ -1523,7 +1523,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
     syntax InternalOp ::= "#create"   Int Int Int Bytes
                         | "#mkCreate" Int Int Int Bytes
                         | "#incrementNonce" Int
- // -------------------------------------------
+                        | "#checkCreate" Int Int
+ // --------------------------------------------
     rule <k> #create ACCTFROM ACCTTO VALUE INITCODE
           => #incrementNonce ACCTFROM
           ~> #pushCallStack ~> #pushWorldState
@@ -1621,6 +1622,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
          <k> #halt ~> #finishCodeDeposit _ _ => #popCallStack ~> #popWorldState ~> 0 ~> #push ... </k>
          <schedule> SCHED </schedule>
       requires SCHED =/=K FRONTIER
+
+    rule <k> #checkCreate ACCT VALUE => #checkBalanceUnderflow ACCT VALUE ~> #checkDepthExceeded ~> #checkNonceExceeded ACCT ... </k>
 ```
 
 `CREATE` will attempt to `#create` the account using the initialization code and cleans up the result with `#codeDeposit`.
@@ -1631,7 +1634,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
     rule [create-valid]:
          <k> CREATE VALUE MEMSTART MEMWIDTH
           => #accessAccounts #newAddr(ACCT, NONCE)
-          ~> #checkCall ACCT VALUE
+          ~> #checkCreate ACCT VALUE
           ~> #create ACCT #newAddr(ACCT, NONCE) VALUE #range(LM, MEMSTART, MEMWIDTH)
           ~> #codeDeposit #newAddr(ACCT, NONCE)
          ...
@@ -1658,7 +1661,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
     rule [create2-valid]:
          <k> CREATE2 VALUE MEMSTART MEMWIDTH SALT
           => #accessAccounts #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
-          ~> #checkCall ACCT VALUE
+          ~> #checkCreate ACCT VALUE
           ~> #create ACCT #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH)) VALUE #range(LM, MEMSTART, MEMWIDTH)
           ~> #codeDeposit #newAddr(ACCT, SALT, #range(LM, MEMSTART, MEMWIDTH))
          ...

package/version

@@ -1 +1 @@
-1.0.462
+1.0.463

tests/failing.llvm

@@ -1 +0,0 @@
-tests/ethereum-tests/BlockchainTests/GeneralStateTests/stCreate2/CREATE2_HighNonceDelegatecall.json