EIP-6780: SELFDESTRUCT only in same transaction (#2545)

* tests with cid 0 * tests with cid 0 tweaks * implement eip-6780 * failing.llvm: update failing tests * Set Version: 1.0.662 * add new cell to k proofs * Set Version: 1.0.662 * update expected integration tests * update kontrol proofs * Set Version: 1.0.664 * draft: update kontrol specs * Set Version: 1.0.671 * add cell to mcd-structured claims * fix mcd proofs * Update dependency: deps/k_release (#2664) * deps/k_release: Set Version 7.1.187 * kevm-pyk/: sync poetry files pyk version 7.1.187 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <[email protected]> * Support for multimasks in slot updates (#2657) * support for multimasks * syntax correction * test correction * Update dependency: deps/k_release (#2665) * deps/k_release: Set Version 7.1.190 * kevm-pyk/: sync poetry files pyk version 7.1.190 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <[email protected]> * introducing the optimize_kcfg parameter (#2666) * Update dependency: deps/k_release (#2667) * deps/k_release: Set Version 7.1.191 * kevm-pyk/: sync poetry files pyk version 7.1.191 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops <[email protected]> * update kontrol claims * passing kontrol specs * update newer specs * add cell to remaining tests.. * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md Co-authored-by: Palina <[email protected]> --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: Petar Maksimović <[email protected]> Co-authored-by: Palina <[email protected]>
runtimeverification · Jan 13, 2025 · 496cb34 · 496cb34
1 parent f28dcd9
commit 496cb34
Show file tree

Hide file tree

Showing 164 changed files with 411 additions and 3,314 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/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>
@@ -1618,6 +1620,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>
@@ -1749,6 +1752,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>
@@ -1757,9 +1761,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>
@@ -1768,6 +1775,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

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/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

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/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"
  // ---------------------------------------

diff --git a/kevm-pyk/src/tests/integration/test_conformance.py b/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)
diff --git a/tests/bchain.0.chainId b/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