Implement Deposit Requests

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

@@ -524,7 +524,7 @@ Here we check the other post-conditions associated with an EVM test.
                         SetItem("mixHash") SetItem("nonce") SetItem("number") SetItem("parentHash")
                         SetItem("receiptTrie") SetItem("stateRoot") SetItem("timestamp")
                         SetItem("transactionsTrie") SetItem("uncleHash") SetItem("baseFeePerGas") SetItem("withdrawalsRoot")
-                        SetItem("blobGasUsed") SetItem("excessBlobGas") SetItem("parentBeaconBlockRoot")
+                        SetItem("blobGasUsed") SetItem("excessBlobGas") SetItem("parentBeaconBlockRoot") SetItem("requestsHash")
                       )
 
     rule <k> check "blockHeader" : { "bloom"                : VALUE } => .K ... </k> <logsBloom>        VALUE </logsBloom>
@@ -547,6 +547,8 @@ Here we check the other post-conditions associated with an EVM test.
     rule <k> check "blockHeader" : { "blobGasUsed"          : VALUE } => .K ... </k> <blobGasUsed>      VALUE </blobGasUsed>
     rule <k> check "blockHeader" : { "excessBlobGas"        : VALUE } => .K ... </k> <excessBlobGas>    VALUE </excessBlobGas>
     rule <k> check "blockHeader" : { "parentBeaconBlockRoot": VALUE } => .K ... </k> <beaconRoot>       VALUE </beaconRoot>
+    rule <k> check "blockHeader" : { "requestsHash"         : VALUE } => .K ... </k> <requestsRoot>     VALUE </requestsRoot>
+
 
 
     rule <k> check "blockHeader" : { "hash": HASH:Bytes } => .K ...</k>
@@ -570,10 +572,12 @@ Here we check the other post-conditions associated with an EVM test.
          <blobGasUsed>      UB </blobGasUsed>
          <excessBlobGas>    EB </excessBlobGas>
          <beaconRoot>       BR </beaconRoot>
-      requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)                     ==Int #asWord(HASH)
-        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF)                 ==Int #asWord(HASH)
-        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR)             ==Int #asWord(HASH)
-        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR) ==Int #asWord(HASH)
+         <requestsRoot>     RR </requestsRoot>
+      requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN)                         ==Int #asWord(HASH)
+        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF)                     ==Int #asWord(HASH)
+        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR)                 ==Int #asWord(HASH)
+        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR)     ==Int #asWord(HASH)
+        orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, RR) ==Int #asWord(HASH)
 
     rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID
  // ------------------------------------------------------------------------------------------------------------------------

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

@@ -11,12 +11,14 @@ This file only defines the local execution operations, the file `driver.md` will
 requires "data.md"
 requires "network.md"
 requires "gas.md"
+requires "requests.md"
 
 module EVM
     imports STRING
     imports EVM-DATA
     imports NETWORK
     imports GAS
+    imports EVM-REQUESTS
 ```
 
 Configuration
@@ -116,6 +118,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
               <blobGasUsed>      0      </blobGasUsed>
               <excessBlobGas>    0      </excessBlobGas>
               <beaconRoot>       0      </beaconRoot>
+              <requestsRoot>     0      </requestsRoot>
 
               <ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
             </block>
@@ -190,6 +193,11 @@ In the comments next to each cell, we've marked which component of the YellowPap
               </withdrawal>
             </withdrawals>
 
+            <requests>
+              <depositRequests> .List </depositRequests>
+              //other request types come here
+            </requests>
+
           </network>
 
         </ethereum>
@@ -762,6 +770,53 @@ After executing a transaction, it's necessary to have the effect of the substate
     rule <k> #deleteAccounts(.List) => .K ... </k>
 ```
 
+### Fetching requests from event logs
+
+While processing a block, multiple requests objects with different `request_types` will be produced by the system, and accumulated in the block requests list.
+
+```k
+    syntax KItem ::= "#filterLogs" Int [symbol(#filterLogs)]
+ // --------------------------------------------------------
+    rule <k> #filterLogs _ => .K ... </k> <schedule> SCHED </schedule> requires notBool Ghasrequests << SCHED >>
+
+    rule <k> #filterLogs IDX => .K ... </k>
+         <schedule> SCHED </schedule>
+         <log> LOGS </log>
+         // <depositRequests> DRQSTS </depositRequests>
+         // <requestsRoot> _ => #computeRequestsHash(DRQSTS) </requestsRoot>
+      requires Ghasrequests << SCHED >> andBool IDX >=Int size(LOGS)
+
+    rule <k> #filterLogs IDX
+          => #parseDepositRequest {LOGS[IDX]}:>SubstateLogEntry
+          // parse other request types
+          ~> #filterLogs IDX +Int 1
+         ...
+         </k>
+         <log> LOGS </log>
+         <schedule> SCHED </schedule>
+      requires IDX <Int size(LOGS) andBool Ghasrequests << SCHED >>
+```
+
+Rules for parsing Deposit Requests according to EIP-6110.
+
+```k
+    syntax KItem ::= "#parseDepositRequest" SubstateLogEntry [symbol(#parseDepositRequest)]
+ // ---------------------------------------------------------------------------------------
+    rule <k> #parseDepositRequest { ADDR | TOPICS | DATA } => .K ... </k>
+         <depositRequests> RS => RS ListItem(Int2Bytes(1, DEPOSIT_REQUEST_TYPE, BE) +Bytes #extractDepositData(DATA)) </depositRequests>
+      requires ADDR ==K DEPOSIT_CONTRACT_ADDRESS
+       andBool size(TOPICS) >Int 0
+       andBool {TOPICS[0]}:>Int ==Int DEPOSIT_EVENT_SIGNATURE_HASH
+       andBool #isValidDepositEventData(DATA)
+
+    rule <k> #parseDepositRequest { ADDR | TOPICS | DATA } => #end EVMC_INVALID_BLOCK ... </k>
+      requires ADDR ==K DEPOSIT_CONTRACT_ADDRESS
+       andBool size(TOPICS) >Int 0
+       andBool {TOPICS[0]}:>Int ==Int DEPOSIT_EVENT_SIGNATURE_HASH
+       andBool notBool #isValidDepositEventData(DATA)
+
+    rule <k> #parseDepositRequest _ => .K ... </k> [owise]
+```
 ### Block processing
 
 -   `#startBlock` is used to signal that we are about to start mining a block and block initialization should take place (before transactions are executed).
@@ -779,7 +834,12 @@ After executing a transaction, it's necessary to have the effect of the substate
     syntax EthereumCommand ::= "#finalizeBlock"
                              | #rewardOmmers ( JSONs ) [symbol(#rewardOmmers)]
  // --------------------------------------------------------------------------
-    rule <k> #finalizeBlock => #if Ghaswithdrawals << SCHED >> #then #finalizeWithdrawals #else .K #fi ~> #rewardOmmers(OMMERS) ... </k>
+    rule <k> #finalizeBlock
+          => #if Ghaswithdrawals << SCHED >> #then #finalizeWithdrawals #else .K #fi
+          ~> #rewardOmmers(OMMERS)
+          ~> #filterLogs 0
+         ...
+         </k>
          <schedule> SCHED </schedule>
          <ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
          <coinbase> MINER </coinbase>

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

@@ -46,6 +46,7 @@ The following codes all indicate that the VM ended execution with an exception,
                                    | "EVMC_STATIC_MODE_VIOLATION"
                                    | "EVMC_PRECOMPILE_FAILURE"
                                    | "EVMC_NONCE_EXCEEDED"
+                                   | "EVMC_INVALID_BLOCK"
  // -------------------------------------------------------------
     rule StatusCode2String(EVMC_FAILURE)               => "EVMC_FAILURE"
     rule StatusCode2String(EVMC_INVALID_INSTRUCTION)   => "EVMC_INVALID_INSTRUCTION"
@@ -59,6 +60,7 @@ The following codes all indicate that the VM ended execution with an exception,
     rule StatusCode2String(EVMC_STATIC_MODE_VIOLATION) => "EVMC_STATIC_MODE_VIOLATION"
     rule StatusCode2String(EVMC_PRECOMPILE_FAILURE)    => "EVMC_PRECOMPILE_FAILURE"
     rule StatusCode2String(EVMC_NONCE_EXCEEDED)        => "EVMC_NONCE_EXCEEDED"
+    rule StatusCode2String(EVMC_INVALID_BLOCK)         => "EVMC_INVALID_BLOCK"
 ```
 
 ### Ending Codes

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

@@ -0,0 +1,113 @@
+Implementation of Execution Layer Requests
+------------------------------------------
+```k
+requires "serialization.md"
+```
+
+```k
+module EVM-REQUESTS
+    imports SERIALIZATION
+```
+
+A `requests` object consists of a `request_type` byte prepended to an opaque byte array `request_data`.
+The `request_data` contains zero or more encoded request objects.
+```
+requests = request_type ++ request_data
+```
+Each request type will define its own requests object with its own `request_data` format.
+
+In order to compute the commitment, an intermediate hash list is first built by hashing all non-empty requests elements of the block requests list.
+Items with empty `request_data` are excluded, i.e. the intermediate list skips requests items which contain only the `request_type` (1 byte) and nothing else.
+
+```k
+    syntax Int ::= #computeRequestsHash(List) [function, symbol(#computeRequestsHash)]
+ // ----------------------------------------------------------------------------------
+    rule #computeRequestsHash(RS) => keccak(#computeRequestsHashIntermediate(RS))
+
+    syntax Bytes ::= #computeRequestsHashIntermediate(List)        [function, symbol(#computeRequestsHashIntermediate)]
+                   | #computeRequestsHashIntermediate(List, Bytes) [function, symbol(#computeRequestsHashIntermediateAux)]
+ // ----------------------------------------------------------------------------------------------------------------------
+    rule #computeRequestsHashIntermediate(RS) => #computeRequestsHashIntermediate(RS, .Bytes)
+    rule #computeRequestsHashIntermediate(.List, ACC) => ACC
+    rule #computeRequestsHashIntermediate(ListItem(R) RS, ACC) => #computeRequestsHashIntermediate(RS, ACC)
+      requires lengthBytes(R) <=Int 1
+    rule #computeRequestsHashIntermediate(ListItem(R) RS, ACC) => #computeRequestsHashIntermediate(RS, ACC +Bytes Keccak256raw(R))
+      requires lengthBytes(R) >Int 1
+```
+
+Deposit Requests
+----------------
+The structure denoting the new deposit request consists of the following fields:
+
+1. `pubkey: Bytes48`
+2. `withdrawal_credentials: Bytes32`
+3. `amount: uint64`
+4. `signature: Bytes96`
+5. `index: uint64`
+
+```k
+    syntax Int ::= "DEPOSIT_REQUEST_TYPE"         [macro]
+                 | "DEPOSIT_EVENT_LENGTH"         [macro]
+                 | "DEPOSIT_CONTRACT_ADDRESS"     [alias]
+                 | "DEPOSIT_EVENT_SIGNATURE_HASH" [alias]
+ // -----------------------------------------------------
+    rule DEPOSIT_REQUEST_TYPE => 0
+    rule DEPOSIT_CONTRACT_ADDRESS => #parseAddr("0x00000000219ab540356cbb839cbe05303d7705fa")
+    rule DEPOSIT_EVENT_SIGNATURE_HASH => #parseWord("0x649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c5")
+    rule DEPOSIT_EVENT_LENGTH => 576
+
+    syntax Int ::= "PUBKEY_OFFSET"                [macro]
+                 | "WITHDRAWAL_CREDENTIALS_OFFSET"[macro]
+                 | "AMOUNT_OFFSET"                [macro]
+                 | "SIGNATURE_OFFSET"             [macro]
+                 | "INDEX_OFFSET"                 [macro]
+                 | "PUBKEY_SIZE"                  [macro]
+                 | "WITHDRAWAL_CREDENTIALS_SIZE"  [macro]
+                 | "AMOUNT_SIZE"                  [macro]
+                 | "SIGNATURE_SIZE"               [macro]
+                 | "INDEX_SIZE"                   [macro]
+ // -----------------------------------------------------
+    rule PUBKEY_OFFSET                 => 160
+    rule WITHDRAWAL_CREDENTIALS_OFFSET => 256
+    rule AMOUNT_OFFSET                 => 320
+    rule SIGNATURE_OFFSET              => 384
+    rule INDEX_OFFSET                  => 512
+    rule PUBKEY_SIZE                   => 48
+    rule WITHDRAWAL_CREDENTIALS_SIZE   => 32
+    rule AMOUNT_SIZE                   => 8
+    rule SIGNATURE_SIZE                => 96
+    rule INDEX_SIZE                    => 8
+```
+
+
+
+```k
+    syntax Bytes ::= #extractDepositData ( Bytes ) [function, symbol(#extractDepositData)]
+ // --------------------------------------------------------------------------------------
+    rule #extractDepositData(DATA) => substrBytes(DATA, PUBKEY_OFFSET +Int 32, PUBKEY_OFFSET +Int 32 +Int PUBKEY_SIZE)
+                               +Bytes substrBytes(DATA, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32 +Int WITHDRAWAL_CREDENTIALS_SIZE)
+                               +Bytes substrBytes(DATA, AMOUNT_OFFSET +Int 32, AMOUNT_OFFSET +Int 32 +Int AMOUNT_SIZE)
+                               +Bytes substrBytes(DATA, SIGNATURE_OFFSET +Int 32, SIGNATURE_OFFSET +Int 32 +Int SIGNATURE_SIZE)
+                               +Bytes substrBytes(DATA, INDEX_OFFSET +Int 32, INDEX_OFFSET +Int 32 +Int INDEX_SIZE)
+
+    syntax Bool ::= #isValidDepositEventData ( Bytes ) [function, symbol(#isValidDepositEventData), total]
+ // ------------------------------------------------------------------------------------------------------
+    rule #isValidDepositEventData(DATA) => true
+      requires lengthBytes(DATA) ==Int DEPOSIT_EVENT_LENGTH
+       andBool Bytes2Int(substrBytes(DATA, 0, 32), BE, Unsigned) ==Int PUBKEY_OFFSET
+       andBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) ==Int WITHDRAWAL_CREDENTIALS_OFFSET
+       andBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) ==Int AMOUNT_OFFSET
+       andBool Bytes2Int(substrBytes(DATA, 96, 128), BE, Unsigned) ==Int SIGNATURE_OFFSET
+       andBool Bytes2Int(substrBytes(DATA, 128, 160), BE, Unsigned) ==Int INDEX_OFFSET
+       andBool Bytes2Int(substrBytes(DATA, PUBKEY_OFFSET, PUBKEY_OFFSET +Int 32), BE, Unsigned) ==Int PUBKEY_SIZE
+       andBool Bytes2Int(substrBytes(DATA, WITHDRAWAL_CREDENTIALS_OFFSET, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32), BE, Unsigned) ==Int WITHDRAWAL_CREDENTIALS_SIZE
+       andBool Bytes2Int(substrBytes(DATA, AMOUNT_OFFSET, AMOUNT_OFFSET +Int 32), BE, Unsigned) ==Int AMOUNT_SIZE
+       andBool Bytes2Int(substrBytes(DATA, SIGNATURE_OFFSET, SIGNATURE_OFFSET +Int 32), BE, Unsigned) ==Int SIGNATURE_SIZE
+       andBool Bytes2Int(substrBytes(DATA, INDEX_OFFSET, INDEX_OFFSET +Int 32), BE, Unsigned) ==Int INDEX_SIZE
+
+    rule #isValidDepositEventData(_) => false [owise]
+```
+
+```k
+endmodule
+```

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

@@ -30,6 +30,8 @@ module SCHEDULE
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
                           | "Ghaswarmcoinbase"        | "Ghaswithdrawals"  | "Ghastransient"       | "Ghasmcopy"
                           | "Ghasbeaconroot"          | "Ghaseip6780"      | "Ghasblobbasefee"     | "Ghasblobhash"
+                          | "Ghasrequests"
+ // --------------------------------------
 ```
 
 ### Schedule Constants
@@ -156,6 +158,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule [GhasbeaconrootDefault]:          Ghasbeaconroot          << DEFAULT >> => false
     rule [Ghaseip6780Default]:             Ghaseip6780             << DEFAULT >> => false
     rule [GhasblobhashDefault]:            Ghasblobhash            << DEFAULT >> => false
+    rule [GhasrequestsDefault]:            Ghasrequests            << DEFAULT >> => false
 ```
 
 ### Frontier Schedule
@@ -423,8 +426,9 @@ A `ScheduleConst` is a constant determined by the fee schedule.
  // --------------------------------------------------------------------------
     rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
 
-    rule [SCHEDFLAGPrague]: SCHEDFLAG  << PRAGUE >> => SCHEDFLAG << CANCUN >>
-
+    rule [GhasrequestsPrague]: Ghasrequests << PRAGUE >> => true
+    rule [SCHEDFLAGPrague]:    SCHEDFLAG    << PRAGUE >> => SCHEDFLAG << CANCUN >>
+      requires notBool ( SCHEDFLAG ==K Ghasrequests )
 ```
 
 ```k