EIP-6780: SELFDESTRUCT only in same transaction

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.670'
+VERSION: Final = '1.0.671'

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

@@ -82,6 +82,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
               <refund>           0     </refund>                  // A_r
               <accessedAccounts> .Set  </accessedAccounts>
               <accessedStorage>  .Map  </accessedStorage>
+              <createdAccounts>  .Set  </createdAccounts>
             </substate>
 
             // Immutable during a single transaction
@@ -554,9 +555,10 @@ After executing a transaction, it's necessary to have the effect of the substate
     rule <k> #finalizeTx(true) => #finalizeStorage(Set2List(SetItem(MINER) |Set ACCTS)) ... </k>
          <selfDestruct> .Set </selfDestruct>
          <coinbase> MINER </coinbase>
-         <touchedAccounts> ACCTS </touchedAccounts>
+         <touchedAccounts> ACCTS => .Set </touchedAccounts>
          <accessedAccounts> _ => .Set </accessedAccounts>
          <accessedStorage> _ => .Map </accessedStorage>
+         <createdAccounts> _ => .Set </createdAccounts>
 
     rule <k> #finalizeTx(false) ... </k>
          <useGas> true </useGas>
@@ -1617,6 +1619,7 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
            <nonce> NONCE => #if Gemptyisnonexistent << SCHED >> #then NONCE +Int 1 #else NONCE #fi </nonce>
            ...
          </account>
+         <createdAccounts> ACCTS => ACCTS |Set SetItem(ACCTTO) </createdAccounts>
 
     rule <k> #incrementNonce ACCT => .K ... </k>
          <account>
@@ -1748,6 +1751,7 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in
     syntax UnStackOp ::= "SELFDESTRUCT"
  // -----------------------------------
     rule <k> SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... </k>
+         <schedule> SCHED </schedule>
          <id> ACCT </id>
          <selfDestruct> SDS => SDS |Set SetItem(ACCT) </selfDestruct>
          <account>
@@ -1756,9 +1760,12 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in
            ...
          </account>
          <output> _ => .Bytes </output>
-      requires ACCT =/=Int ACCTTO
+         <createdAccounts> CA </createdAccounts>
+      requires ((notBool Ghaseip6780 << SCHED >>) orBool ACCT in CA)
+       andBool ACCT =/=Int ACCTTO
 
     rule <k> SELFDESTRUCT ACCT => #touchAccounts ACCT ~> #accessAccounts ACCT ~> #end EVMC_SUCCESS ... </k>
+         <schedule> SCHED </schedule>
          <id> ACCT </id>
          <selfDestruct> SDS => SDS |Set SetItem(ACCT) </selfDestruct>
          <account>
@@ -1767,6 +1774,28 @@ Self destructing to yourself, unlike a regular transfer, destroys the balance in
            ...
          </account>
          <output> _ => .Bytes </output>
+         <createdAccounts> CA </createdAccounts>
+      requires ((notBool Ghaseip6780 << SCHED >>) orBool ACCT in CA)
+
+    rule <k> SELFDESTRUCT ACCTTO => #touchAccounts ACCT ACCTTO ~> #accessAccounts ACCTTO ~> #transferFunds ACCT ACCTTO BALFROM ~> #end EVMC_SUCCESS ... </k>
+         <schedule> SCHED </schedule>
+         <id> ACCT </id>
+         <account>
+           <acctID> ACCT </acctID>
+           <balance> BALFROM </balance>
+           ...
+         </account>
+         <output> _ => .Bytes </output>
+         <createdAccounts> CA </createdAccounts>
+      requires Ghaseip6780 << SCHED >> andBool (notBool ACCT in CA)
+       andBool ACCT =/=Int ACCTTO
+
+    rule <k> SELFDESTRUCT ACCT => #touchAccounts ACCT ~> #accessAccounts ACCT ~> #end EVMC_SUCCESS ... </k>
+         <schedule> SCHED </schedule>
+         <id> ACCT </id>
+         <output> _ => .Bytes </output>
+         <createdAccounts> CA </createdAccounts>
+      requires Ghaseip6780 << SCHED >> andBool (notBool ACCT in CA)
 ```
 
 Precompiled Contracts

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

@@ -29,7 +29,8 @@ module SCHEDULE
                           | "Ghassstorestipend"       | "Ghaschainid"      | "Ghasaccesslist"      | "Ghasbasefee"
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
                           | "Ghaswarmcoinbase"        | "Ghastransient"    | "Ghasmcopy"           | "Ghasbeaconroot"
- // -----------------------------------------------------------------------------------------------------------------
+                          | "Ghaseip6780"
+ // -------------------------------------
 ```
 
 ### Schedule Constants
@@ -149,6 +150,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghastransient           << DEFAULT >> => false
     rule Ghasmcopy               << DEFAULT >> => false
     rule Ghasbeaconroot          << DEFAULT >> => false
+    rule Ghaseip6780             << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -390,10 +392,12 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghastransient  << CANCUN >> => true
     rule Ghasmcopy      << CANCUN >> => true
     rule Ghasbeaconroot << CANCUN >> => true
+    rule Ghaseip6780     << CANCUN >> => true
     rule SCHEDFLAG     << CANCUN >> => SCHEDFLAG << SHANGHAI >>
       requires notBool ( SCHEDFLAG ==K Ghastransient
                   orBool SCHEDFLAG ==K Ghasmcopy
                   orBool SCHEDFLAG ==K Ghasbeaconroot
+                  orBool SCHEDFLAG ==K Ghaseip6780
                        )
 ```
 ```k

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

@@ -50,6 +50,7 @@ module STATE-UTILS
          <origin>           _ => .Account   </origin>
          <touchedAccounts>  _ => .Set       </touchedAccounts>
          <accessedAccounts> _ => .Set       </accessedAccounts>
+         <createdAccounts>  _ => .Set       </createdAccounts>
 
     syntax EthereumCommand ::= "clearBLOCK"
  // ---------------------------------------

kevm-pyk/src/tests/integration/test_conformance.py

@@ -31,13 +31,16 @@
 
 TEST_DIR: Final = REPO_ROOT / 'tests/ethereum-tests'
 GOLDEN: Final = (REPO_ROOT / 'tests/templates/output-success-llvm.json').read_text().rstrip()
+TEST_FILES_WITH_CID_0: Final = (REPO_ROOT / 'tests/bchain.0.chainId').read_text().splitlines()
 
 
-def _test(gst_file: Path, schedule: str, mode: str, chainid: int, usegas: bool) -> None:
+def _test(gst_file: Path, schedule: str, mode: str, usegas: bool) -> None:
     skipped_gst_tests = SKIPPED_TESTS.get(gst_file, [])
     if '*' in skipped_gst_tests:
         pytest.skip()
 
+    chainid = 0 if str(gst_file.relative_to(TEST_DIR)) in TEST_FILES_WITH_CID_0 else 1
+
     with gst_file.open() as f:
         gst_data = json.load(f)
 
@@ -93,7 +96,7 @@ def read_csv_file(csv_file: Path) -> tuple[tuple[Path, str], ...]:
     ids=[str(test_file.relative_to(VM_TEST_DIR)) for test_file in VM_TESTS],
 )
 def test_vm(test_file: Path) -> None:
-    _test(test_file, 'DEFAULT', 'VMTESTS', 1, True)
+    _test(test_file, 'DEFAULT', 'VMTESTS', True)
 
 
 @pytest.mark.skip(reason='failing / slow VM tests')
@@ -103,7 +106,7 @@ def test_vm(test_file: Path) -> None:
     ids=[str(test_file.relative_to(VM_TEST_DIR)) for test_file in SKIPPED_VM_TESTS],
 )
 def test_rest_vm(test_file: Path) -> None:
-    _test(test_file, 'DEFAULT', 'VMTESTS', 1, True)
+    _test(test_file, 'DEFAULT', 'VMTESTS', True)
 
 
 ALL_TEST_DIR: Final = TEST_DIR / 'BlockchainTests/GeneralStateTests'
@@ -118,7 +121,7 @@ def test_rest_vm(test_file: Path) -> None:
     ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in BCHAIN_TESTS],
 )
 def test_bchain(test_file: Path) -> None:
-    _test(test_file, 'CANCUN', 'NORMAL', 1, True)
+    _test(test_file, 'CANCUN', 'NORMAL', True)
 
 
 @pytest.mark.skip(reason='failing / slow blockchain tests')
@@ -128,4 +131,4 @@ def test_bchain(test_file: Path) -> None:
     ids=[str(test_file.relative_to(ALL_TEST_DIR)) for test_file in SKIPPED_BCHAIN_TESTS],
 )
 def test_rest_bchain(test_file: Path) -> None:
-    _test(test_file, 'CANCUN', 'NORMAL', 1, True)
+    _test(test_file, 'CANCUN', 'NORMAL', True)

package/version

@@ -1 +1 @@
-1.0.670
+1.0.671

tests/bchain.0.chainId

@@ -0,0 +1,14 @@
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/create_selfdestruct_same_tx.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/delegatecall_from_new_contract_to_pre_existing_contract.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/delegatecall_from_pre_existing_contract_to_new_contract.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collision_multi_tx.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collision_two_different_transactions.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collision.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/recreate_self_destructed_contract_different_txs.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/reentrancy_selfdestruct_revert.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/self_destructing_initcode_create_tx.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/self_destructing_initcode.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_created_in_same_tx_with_revert.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_created_same_block_different_tx.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_not_created_in_same_tx_with_revert.json
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_pre_existing.json