Implementing BLOBHASH Opcode (#2693)

* Introducing `BLOBHASH` OpCode as 73. * Modifying type of `txVersionedHashes` from `JSONs` to `List` to implement `BLOBHASH` operation * Implementing the operation of `BLOBHASH` * Adding `Blob` transaction to `effectiveGasPrice` * Updating integration tests with the new `txVersionedHashes` type * Updating `failing.llvm` list of tests * Fixing Opcode execution and transaction parsing * Addressing comments - Position of `BLOBHASH` on evm.md - Deleting invalid side condition in `$effectiveGasPrice` * Adding `versionedHashes` to evm's `callState` * Addressing comments * Updating failing tests * Filling `BENCHMARK_TESTS` * Filling `ERC20_TESTS` * Filling `EXAMPLES_TESTS` * Filling `MCD_TESTS` * Filling `MCD_STRUCTURED_TESTS` and `VAT_STRUCTURED_TESTS` * Filling `KONTROL_TESTS` * Updating `failing.llvm` * Fix dash size * Updating `failing.llvm` * Re-adding failing.llvm tests * Fix `kontrol` prove tests * Fix `mcd` prove tests * Fix `mcd-strutured` prove tests * Adding BASEFEE to #asmOpCode Co-authored-by: Andrei Văcaru <[email protected]> * Fixing `#parseList2JSONs` and updating `failing.llvm` * Changing back parseList2JSONs to avoid issues in rlp encoding * Fixing `BLOBBASEFEE` and Updating `failing.llvm` * Fixing `#rangeNegUInt64` --------- Co-authored-by: Andrei Văcaru <[email protected]>
runtimeverification · Jan 31, 2025 · 7c1de74 · 7c1de74
1 parent bfd9e29
commit 7c1de74
Show file tree

Hide file tree

Showing 171 changed files with 342 additions and 207 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/asm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/asm.md
@@ -105,6 +105,8 @@ Operator `#revOps` can be used to reverse a program.
     rule #asmOpCode( GASLIMIT       ) =>  69
     rule #asmOpCode( CHAINID        ) =>  70
     rule #asmOpCode( SELFBALANCE    ) =>  71
+    rule #asmOpCode( BASEFEE        ) =>  72
+    rule #asmOpCode( BLOBHASH       ) =>  73
     rule #asmOpCode( POP            ) =>  80
     rule #asmOpCode( MLOAD          ) =>  81
     rule #asmOpCode( MSTORE         ) =>  82

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -111,14 +111,16 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
          <txPending> ListItem(TXID:Int) ... </txPending>
          <coinbase> MINER </coinbase>
          <message>
-           <msgID>      TXID     </msgID>
-           <txGasLimit> GLIMIT   </txGasLimit>
-           <to>         .Account </to>
-           <value>      VALUE    </value>
-           <data>       CODE     </data>
-           <txAccess>   TA       </txAccess>
+           <msgID>             TXID     </msgID>
+           <txGasLimit>        GLIMIT   </txGasLimit>
+           <to>                .Account </to>
+           <value>             VALUE    </value>
+           <data>              CODE     </data>
+           <txAccess>          TA       </txAccess>
+           <txVersionedHashes> TVH      </txVersionedHashes>
            ...
          </message>
+         <versionedHashes> _ => TVH </versionedHashes>
          <account>
            <acctID> ACCTFROM </acctID>
            <balance> BAL => BAL -Int (GLIMIT *Int #effectiveGasPrice(TXID)) </balance>
@@ -147,14 +149,16 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
          <txPending> ListItem(TXID:Int) ... </txPending>
          <coinbase> MINER </coinbase>
          <message>
-           <msgID>      TXID   </msgID>
-           <txGasLimit> GLIMIT </txGasLimit>
-           <to>         ACCTTO </to>
-           <value>      VALUE  </value>
-           <data>       DATA   </data>
-           <txAccess>   TA     </txAccess>
+           <msgID>             TXID   </msgID>
+           <txGasLimit>        GLIMIT </txGasLimit>
+           <to>                ACCTTO </to>
+           <value>             VALUE  </value>
+           <data>              DATA   </data>
+           <txAccess>          TA     </txAccess>
+           <txVersionedHashes> TVH    </txVersionedHashes>
            ...
          </message>
+         <versionedHashes> _ => TVH </versionedHashes>
          <account>
            <acctID> ACCTFROM </acctID>
            <balance> BAL => BAL -Int (GLIMIT *Int #effectiveGasPrice(TXID)) </balance>
@@ -597,7 +601,7 @@ Here we check the other post-conditions associated with an EVM test.
     
     rule <k> check "transactions" : "blobVersionedHashes" : [ .JSONs ] => .K ... </k>
     rule <k> check "transactions" : "blobVersionedHashes" : [ VHASH, REST ] => check "transactions" : "blobVersionedHashes" : VHASH ~> check "transactions" : "blobVersionedHashes" : [ REST ] ... </k>
-    rule <k> check "transactions" : ("blobVersionedHashes" : VHASH ) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txVersionedHashes> VH </txVersionedHashes> ... </message> requires isInVersionedHashes(VHASH, VH)
+    rule <k> check "transactions" : ("blobVersionedHashes" : VHASH ) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txVersionedHashes> VH </txVersionedHashes> ... </message> requires VHASH in VH
 
     rule <k> check "transactions" : ("data"                 : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <data>          VALUE </data>           ... </message>
     rule <k> check "transactions" : ("gasLimit"             : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txGasLimit>    VALUE </txGasLimit>     ... </message>
@@ -627,14 +631,6 @@ Here we check the other post-conditions associated with an EVM test.
     rule isInAccessListStorage(KEY, [SKEY, REST]) => #if   KEY ==Int #asWord(SKEY)
                                                      #then true
                                                      #else isInAccessListStorage(KEY, [REST]) #fi
-
-   // Different from AccessList, Versioned Hashs doesn't contains a list of key-value jsons, but a list of strings finishing in .JSONs like [ "0x01...", "0x02", .JSONs]
-   syntax Bool ::= isInVersionedHashes(Bytes, JSON) [symbol(isInVersionedHashes), function]
- // ---------------------------------------------------------------------------------------
-   rule isInVersionedHashes(_, [.JSONs]) => false
-   rule isInVersionedHashes(KEY, [SKEY, REST]) => #if KEY ==K SKEY
-                                                  #then true
-                                                  #else isInVersionedHashes(KEY, [REST]) #fi
 ```
 
 TODO: case with nonzero ommers.

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
@@ -468,12 +468,12 @@ Productions related to transactions
     syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx
  // -----------------------------------------------------------------
 
-    syntax LegacyTx     ::= LegacyTxData       ( nonce: Int,                       gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes )                                                                                   [symbol(LegacyTxData)]
-                          | LegacySignedTxData ( nonce: Int,                       gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int )                                                              [symbol(LegacySignedTxData)]
-    syntax AccessListTx ::= AccessListTxData   ( nonce: Int,                       gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs )                                                 [symbol(AccessListTxData)]
-    syntax DynamicFeeTx ::= DynamicFeeTxData   ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs)                                                  [symbol(DynamicFeeTxData)]
-    syntax BlobTx       ::= BlobTxData         ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: JSONs ) [symbol(BlobTxData)]
- // ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+    syntax LegacyTx     ::= LegacyTxData       ( nonce: Int,                       gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes )                                                                                        [symbol(LegacyTxData)]
+                          | LegacySignedTxData ( nonce: Int,                       gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int )                                                                   [symbol(LegacySignedTxData)]
+    syntax AccessListTx ::= AccessListTxData   ( nonce: Int,                       gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs )                                                      [symbol(AccessListTxData)]
+    syntax DynamicFeeTx ::= DynamicFeeTxData   ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs)                                                       [symbol(DynamicFeeTxData)]
+    syntax BlobTx       ::= BlobTxData         ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: List ) [symbol(BlobTxData)]
+ // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 
 endmodule
 ```
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -75,6 +75,8 @@ In the comments next to each cell, we've marked which component of the YellowPap
               <callDepth> 0     </callDepth>
             </callState>
 
+            <versionedHashes> .List </versionedHashes>
+
             // A_* (execution substate)
             <substate>
               <selfDestruct>     .Set  </selfDestruct>            // A_s
@@ -168,7 +170,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
                 <txMaxFee>      0          </txMaxFee>      // T_m
                 <txType>        .TxType    </txType>        // T_x
                 <txMaxBlobFee>  0          </txMaxBlobFee>
-                <txVersionedHashes> [ .JSONs ] </txVersionedHashes>
+                <txVersionedHashes> .List  </txVersionedHashes>
               </message>
             </messages>
 
@@ -1081,7 +1083,7 @@ These operators make queries about the current execution state.
     rule <k> GASPRICE    => GPRICE                      ~> #push ... </k> <gasPrice> GPRICE </gasPrice>
     rule <k> GASLIMIT    => GLIMIT                      ~> #push ... </k> <gasLimit> GLIMIT </gasLimit>
     rule <k> BASEFEE     => BFEE                        ~> #push ... </k> <baseFee> BFEE </baseFee>
-    rule <k> BLOBBASEFEE => #baseFeePerBlobGas(BLOBGAS) ~> #push ... </k> <excessBlobGas> BLOBGAS </excessBlobGas>
+    rule <k> BLOBBASEFEE => #baseFeePerBlobGas(BLOBGAS) ~> #push ... </k> <excessBlobGas> BLOBGAS </excessBlobGas>  requires notBool #rangeNegUInt64(BLOBGAS)
 
     syntax NullStackOp ::= "COINBASE" | "TIMESTAMP" | "NUMBER" | "DIFFICULTY" | "PREVRANDAO"
  // ----------------------------------------------------------------------------------------
@@ -1137,6 +1139,19 @@ The blockhash is calculated here using the "shortcut" formula used for running t
     rule #blockhash(ListItem(_) L, N, HI, A) => #blockhash(L, N, HI -Int 1, A +Int 1) [owise]
 ```
 
+```k
+    syntax UnStackOp ::= "BLOBHASH"
+ // -------------------------------
+
+    rule <k> BLOBHASH INDEX => 0 ~> #push ... </k>
+         <versionedHashes> HASHES </versionedHashes>
+       requires INDEX >=Int size(HASHES)
+
+    rule <k> BLOBHASH INDEX => #asWord( {HASHES[INDEX]}:>Bytes ) ~> #push ... </k>
+         <versionedHashes> HASHES </versionedHashes>
+       requires INDEX <Int size(HASHES)
+```
+
 EVM OpCodes
 -----------
 
@@ -2361,6 +2376,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
     rule <k> #gasExec(SCHED, PUSH(_))        => Gverylow < SCHED > ... </k>
     rule <k> #gasExec(SCHED, DUP(_) _)       => Gverylow < SCHED > ... </k>
     rule <k> #gasExec(SCHED, SWAP(_) _)      => Gverylow < SCHED > ... </k>
+    rule <k> #gasExec(SCHED, BLOBHASH _)     => Gverylow < SCHED > ... </k>
 
     // Wlow
     rule <k> #gasExec(SCHED, MUL _ _)        => Glow < SCHED > ... </k>
@@ -2525,6 +2541,7 @@ After interpreting the strings representing programs as a `WordStack`, it should
     rule #dasmOpCode(  70, SCHED ) => CHAINID     requires Ghaschainid     << SCHED >>
     rule #dasmOpCode(  71, SCHED ) => SELFBALANCE requires Ghasselfbalance << SCHED >>
     rule #dasmOpCode(  72, SCHED ) => BASEFEE     requires Ghasbasefee     << SCHED >>
+    rule #dasmOpCode(  73, SCHED ) => BLOBHASH    requires Ghasblobhash    << SCHED >>
     rule #dasmOpCode(  74, SCHED ) => BLOBBASEFEE requires Ghasblobbasefee << SCHED >>
     rule #dasmOpCode(  80,     _ ) => POP
     rule #dasmOpCode(  81,     _ ) => MLOAD

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

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
@@ -231,6 +231,7 @@ Unparsing
 - `#addrBytes` Takes an Account and represents it as a 20-byte wide Bytes (or an empty Bytes for a null address)
 - `#addrBytesNotNil` Takes an Account and represents it as a 20-byte wide Bytes. It throws an error if the account is null.
 - `#wordBytes` Takes an Int and represents it as a 32-byte wide Bytes
+- `#parseList2JSONs` Takes a List of Bytes and represents it as a JSON array.
 
 ```k
     syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function]
@@ -239,6 +240,11 @@ Unparsing
     rule #addrBytes(.Account) => .Bytes
     rule #addrBytes(ACCT)     => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT)
     rule #wordBytes(WORD)     => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD)
+
+    syntax JSONs ::= #parseList2JSONs ( List ) [function]
+  // ----------------------------------------------------
+    rule #parseList2JSONs( .List ) => .JSONs
+    rule #parseList2JSONs( ListItem(X:Bytes) REST ) => X , #parseList2JSONs(REST)
 ```
 
 Recursive Length Prefix (RLP)
@@ -352,8 +358,8 @@ Encoding
     rule #rlpEncodeTxData( DynamicFeeTxData(TN, TF, TM, TG, TT, TV, DATA, TC, [TA]) )
       => #rlpEncode( [ TC, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA] ] )
    
-    rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, [TVH]) )
-      => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes({TT}:>Account), TV, DATA, [TA], TB, [TVH] ] )
+    rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) )
+      => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes({TT}:>Account), TV, DATA, [TA], TB, [#parseList2JSONs(TVH)] ] )
 
     syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function]
  // ---------------------------------------------------------------------------------------------

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
@@ -190,6 +190,14 @@ The `"network"` key allows setting the fee schedule inside the test.
     rule #asScheduleString("ShanghaiToCancunAtTime15k") => CANCUN
 ```
 
+- `#parseJSONs2List` parse a JSON object with string values into a list of value.
+```k
+   syntax List ::= "#parseJSONs2List" "(" JSONs ")" [function]
+ // ----------------------------------------------------------
+    rule #parseJSONs2List ( .JSONs ) => .List
+    rule #parseJSONs2List ( (VAL:Bytes) , REST ) => ListItem(VAL) #parseJSONs2List ( REST )
+```
+
 The `"rlp"` key loads the block information.
 
 ```k
@@ -353,7 +361,7 @@ The `"rlp"` key loads the block information.
          </k>
     requires #asWord(TYPE) ==Int #dasmTxPrefix(DynamicFee)
 
-     rule <k> load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, TY, TVH, TB, TR, TS ]] , REST ]
+     rule <k> load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, TB, TVH, TY, TR, TS ]] , REST ]
           => mkTX !ID:Int
           ~> loadTransaction !ID { "data"         : TI   ,   "gasLimit"         : TG   ,   "maxPriorityFeePerGas" : TP
                                  , "nonce"        : TN   ,   "r"                : TR   ,   "s"                    : TS
@@ -418,7 +426,7 @@ The `"rlp"` key loads the block information.
          <message> <msgID> TXID </msgID> <txMaxBlobFee> _ => TB </txMaxBlobFee> ... </message>
 
     rule <k> loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... </k>
-         <message> <msgID> TXID </msgID> <txVersionedHashes> _ =>  [TVH] </txVersionedHashes> ... </message>
+         <message> <msgID> TXID </msgID> <txVersionedHashes> _ =>  #parseJSONs2List(TVH) </txVersionedHashes> ... </message>
 ```
 
 ### Getting State