EIP-4788: Beacon Roots contract (#2546)

* implement eip-4788 * Set Version: 1.0.662 * Set Version: 1.0.663 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]>
runtimeverification · Aug 2, 2024 · 14c9d29 · 14c9d29
1 parent 394c1ec
commit 14c9d29
Show file tree

Hide file tree

Showing 8 changed files with 54 additions and 31 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.662"
+version = "1.0.663"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.662'
+VERSION: Final = '1.0.663'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -397,10 +397,6 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
     rule <k> check TESTID : { "post" : (POST:String) } => check "blockHeader" : {  "stateRoot" : #parseWord(POST) } ~> failure TESTID ... </k>
     rule <k> check TESTID : { "post" : { POST } } => check "account" : { POST } ~> failure TESTID ... </k>
 
-    // Temp rule to skip Beacon Roots contract checks.
-    // To be removed after EIP-4788
-    rule <k> check "account" : { 339909022928299415537769066420252604268194818 : _ } => .K ... </k>
-
     rule <k> check "account" : { ACCTID:Int : { KEY : VALUE , REST } } => check "account" : { ACCTID : { KEY : VALUE } } ~> check "account" : { ACCTID : { REST } } ... </k>
       requires REST =/=K .JSONs
 

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -657,7 +657,7 @@ After executing a transaction, it's necessary to have the effect of the substate
 ```k
     syntax EthereumCommand ::= "#startBlock"
  // ----------------------------------------
-    rule <k> #startBlock => .K ... </k>
+    rule <k> #startBlock => #executeBeaconRoots ... </k>
          <gasUsed> _ => 0 </gasUsed>
          <log> _ => .List </log>
          <logsBloom> _ => #padToWidth(256, .Bytes) </logsBloom>
@@ -728,6 +728,31 @@ After executing a transaction, it's necessary to have the effect of the substate
     rule getBloomFilterBit(X, I) => #asInteger(#range(X, I, 2)) %Int 2048
 ```
 
+If `block.timestamp >= CANCUN_FORK_TIMESTAMP`:
+Before executing any transaction, the `BEACON_ROOTS_ADDRESS` (`0x000F3df6D732807Ef1319fB7B8bB8522d0Beac02`) storage is modified as following:
+ - Set the storage value at `header.timestamp % HISTORY_BUFFER_LENGTH` to be `header.timestamp`
+ - Set the storage value at `header.timestamp % HISTORY_BUFFER_LENGTH + HISTORY_BUFFER_LENGTH` to be `header.parent_beacon_root_hash`
+where `HISTORY_BUFFER_LENGTH == 8191`.
+
+Read more about EIP-4788 here [https://eips.ethereum.org/EIPS/eip-4788](https://eips.ethereum.org/EIPS/eip-4788).
+
+```k
+    syntax EthereumCommand ::= "#executeBeaconRoots" [symbol(#executeBeaconRoots)]
+ // ------------------------------------------------------------------------------
+    rule <k> #executeBeaconRoots => .K ... </k>
+         <schedule> SCHED </schedule>
+         <timestamp> TS </timestamp>
+         <beaconRoot> BR </beaconRoot>
+         <account>
+           <acctID> 339909022928299415537769066420252604268194818 </acctID>
+           <storage> M:Map => M [(TS modInt 8191) <- TS] [(TS modInt 8191 +Int 8191) <- BR] </storage>
+           ...
+         </account>
+      requires Ghasbeaconroot << SCHED >>
+
+    rule <k> #executeBeaconRoots => .K ... </k> [owise]
+```
+
 EVM Programs
 ============
 

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
@@ -28,8 +28,8 @@ module SCHEDULE
                           | "Ghasdirtysstore"         | "Ghascreate2"      | "Ghasextcodehash"     | "Ghasselfbalance"
                           | "Ghassstorestipend"       | "Ghaschainid"      | "Ghasaccesslist"      | "Ghasbasefee"
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
-                          | "Ghaswarmcoinbase"        | "Ghastransient"    | "Ghasmcopy"
- // ------------------------------------------------------------------------------------
+                          | "Ghaswarmcoinbase"        | "Ghastransient"    | "Ghasmcopy"           | "Ghasbeaconroot"
+ // -----------------------------------------------------------------------------------------------------------------
 ```
 
 ### Schedule Constants
@@ -148,6 +148,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghaswarmcoinbase        << DEFAULT >> => false
     rule Ghastransient           << DEFAULT >> => false
     rule Ghasmcopy               << DEFAULT >> => false
+    rule Ghasbeaconroot          << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -386,11 +387,13 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule SCHEDCONST             < CANCUN > => SCHEDCONST < SHANGHAI >
       requires notBool (SCHEDCONST ==K Gwarmstoragedirtystore)
 
-    rule Ghastransient << CANCUN >> => true
-    rule Ghasmcopy     << CANCUN >> => true
+    rule Ghastransient  << CANCUN >> => true
+    rule Ghasmcopy      << CANCUN >> => true
+    rule Ghasbeaconroot << CANCUN >> => true
     rule SCHEDFLAG     << CANCUN >> => SCHEDFLAG << SHANGHAI >>
       requires notBool ( SCHEDFLAG ==K Ghastransient
                   orBool SCHEDFLAG ==K Ghasmcopy
+                  orBool SCHEDFLAG ==K Ghasbeaconroot
                        )
 ```
 ```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
@@ -171,20 +171,21 @@ The `"network"` key allows setting the fee schedule inside the test.
 
     syntax Schedule ::= #asScheduleString ( String ) [symbol(#asScheduleString), function]
  // --------------------------------------------------------------------------------------
-    rule #asScheduleString("Frontier")          => FRONTIER
-    rule #asScheduleString("Homestead")         => HOMESTEAD
-    rule #asScheduleString("EIP150")            => TANGERINE_WHISTLE
-    rule #asScheduleString("EIP158")            => SPURIOUS_DRAGON
-    rule #asScheduleString("Byzantium")         => BYZANTIUM
-    rule #asScheduleString("Constantinople")    => CONSTANTINOPLE
-    rule #asScheduleString("ConstantinopleFix") => PETERSBURG
-    rule #asScheduleString("Istanbul")          => ISTANBUL
-    rule #asScheduleString("Berlin")            => BERLIN
-    rule #asScheduleString("London")            => LONDON
-    rule #asScheduleString("Merge")             => MERGE
-    rule #asScheduleString("Paris")             => MERGE
-    rule #asScheduleString("Shanghai")          => SHANGHAI
-    rule #asScheduleString("Cancun")            => CANCUN
+    rule #asScheduleString("Frontier")                  => FRONTIER
+    rule #asScheduleString("Homestead")                 => HOMESTEAD
+    rule #asScheduleString("EIP150")                    => TANGERINE_WHISTLE
+    rule #asScheduleString("EIP158")                    => SPURIOUS_DRAGON
+    rule #asScheduleString("Byzantium")                 => BYZANTIUM
+    rule #asScheduleString("Constantinople")            => CONSTANTINOPLE
+    rule #asScheduleString("ConstantinopleFix")         => PETERSBURG
+    rule #asScheduleString("Istanbul")                  => ISTANBUL
+    rule #asScheduleString("Berlin")                    => BERLIN
+    rule #asScheduleString("London")                    => LONDON
+    rule #asScheduleString("Merge")                     => MERGE
+    rule #asScheduleString("Paris")                     => MERGE
+    rule #asScheduleString("Shanghai")                  => SHANGHAI
+    rule #asScheduleString("Cancun")                    => CANCUN
+    rule #asScheduleString("ShanghaiToCancunAtTime15k") => CANCUN
 ```
 
 The `"rlp"` key loads the block information.

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.662
+1.0.663
diff --git a/tests/failing.llvm b/tests/failing.llvm
@@ -3,13 +3,11 @@ BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d1g0v0_Ca
 BlockchainTests/GeneralStateTests/VMTests/vmTests/suicide.json,suicide_d2g0v0_Cancun
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/reentrant_selfdestructing_call.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/multi_block_beacon_root_timestamp_calls.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_contract_timestamps.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_contract_deploy.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_equal_to_timestamp.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_selfdestruct.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/tx_to_beacon_root_contract.json,*
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_contract_deploy.json,*
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/tx_to_beacon_root_contract.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4788_beacon_root/test_beacon_root_contract.py::test_tx_to_beacon_root_contract[fork_Cancun-tx_type_3-blockchain_test-call_beacon_root_contract_True-auto_access_list_False]
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/tx_to_beacon_root_contract.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4788_beacon_root/test_beacon_root_contract.py::test_tx_to_beacon_root_contract[fork_Cancun-tx_type_3-blockchain_test-call_beacon_root_contract_True-auto_access_list_True]
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_transition.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_contract_calls.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/no_beacon_root_contract_at_transition.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/delegatecall_from_pre_existing_contract_to_new_contract.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_created_same_block_different_tx.json,*