runtimeverification · anvacaru · Jul 26, 2024 · Jul 31, 2024 · Jul 31, 2024 · Jul 31, 2024
diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-7.1.186
+7.1.191
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -2,7 +2,7 @@
   description = "A flake for the KEVM Semantics";
 
   inputs = {
-    k-framework.url = "github:runtimeverification/k/v7.1.186";
+    k-framework.url = "github:runtimeverification/k/v7.1.191";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.follows = "k-framework/rv-utils";

diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.186"
+kframework = "7.1.191"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -365,6 +365,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 max_frontier_parallel=options.max_frontier_parallel,
                 force_sequential=options.force_sequential,
                 assume_defined=options.assume_defined,
+                optimize_kcfg=options.optimize_kcfg,
             )
             end_time = time.time()
             _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s')

diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py
@@ -381,6 +381,7 @@ class KProveOptions(Options):
     direct_subproof_rules: bool
     maintenance_rate: int
     assume_defined: bool
+    optimize_kcfg: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -390,6 +391,7 @@ def default() -> dict[str, Any]:
             'direct_subproof_rules': False,
             'maintenance_rate': 1,
             'assume_defined': False,
+            'optimize_kcfg': False,
         }
 
 
@@ -850,6 +852,13 @@ def kprove_args(self) -> ArgumentParser:
             action='store_true',
             help='Use the implication check of the Booster (experimental).',
         )
+        args.add_argument(
+            '--optimize-kcfg',
+            dest='optimize_kcfg',
+            default=None,
+            action='store_true',
+            help='Optimize the constructed KCFG on-the-fly.',
+        )
         return args
 
     @cached_property

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/lemmas/slot-updates.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/slot-updates.k
@@ -25,10 +25,12 @@ module SLOT-UPDATES [symbolic]
     // SHIFT appropriate, and in the latter case, the slot will appear on the LHS of the |Int.
 
     // 1. Slot masking using &Int
-    rule [mask-b-and]:
+    rule [multimask-b-and]:
       MASK:Int &Int SLOT:Int =>
+        ( MASK |Int ( 2 ^Int ( 8 *Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) ) -Int 1 ) )
+          &Int
         #asWord ( #buf ( 32, SLOT ) [ 32 -Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) := #buf ( #getMaskWidthBytes(MASK), 0 ) ] )
-        requires #isMask(MASK) andBool #rangeUInt(256, SLOT)
+        requires 0 <=Int #getMaskShiftBytes(MASK) andBool 0 <=Int #getMaskWidthBytes(MASK) andBool #rangeUInt(256, SLOT)
         [simplification, concrete(MASK), preserves-definedness]
 
     // 2a. |Int and +Bytes, update to be done in left

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/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -115,6 +115,7 @@ def run_prover(
     maintenance_rate: int = 1,
     assume_defined: bool = False,
     extra_module: KFlatModule | None = None,
+    optimize_kcfg: bool = False,
 ) -> bool:
     prover: APRProver | ImpliesProver
     try:
@@ -131,6 +132,7 @@ def create_prover() -> APRProver:
                     direct_subproof_rules=direct_subproof_rules,
                     assume_defined=assume_defined,
                     extra_module=extra_module,
+                    optimize_kcfg=optimize_kcfg,
                 )
 
             def update_status_bar(_proof: Proof) -> None:

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