Implementing BLOBHASH Opcode

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

@@ -105,6 +105,7 @@ Operator `#revOps` can be used to reverse a program.
     rule #asmOpCode( GASLIMIT       ) =>  69
     rule #asmOpCode( CHAINID        ) =>  70
     rule #asmOpCode( SELFBALANCE    ) =>  71
+    rule #asmOpCode( BLOBHASH       ) =>  73
     rule #asmOpCode( POP            ) =>  80
     rule #asmOpCode( MLOAD          ) =>  81
     rule #asmOpCode( MSTORE         ) =>  82

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

@@ -597,7 +597,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 +627,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.

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
 ```

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

@@ -168,7 +168,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>
 
@@ -915,11 +915,19 @@ Some operators don't calculate anything, they just push the stack around a bit.
 These operations are getters/setters of the local execution memory.
 
 ```k
-    syntax UnStackOp ::= "MLOAD"
- // ----------------------------
+    syntax UnStackOp ::= "MLOAD" | "BLOBHASH"
+ // -----------------------------------------
     rule <k> MLOAD INDEX => #asWord(#range(LM, INDEX, 32)) ~> #push ... </k>
          <localMem> LM </localMem>
 
+   rule <k> BLOBHASH INDEX => PUSHZERO ~> #push ... </k>
+        <txVersionedHashes> HASHES </txVersionedHashes>
+      requires INDEX >=Int size(HASHES)
+
+   rule <k> BLOBHASH INDEX => #asWord( {HASHES[INDEX]}:>Bytes ) ~> #push ... </k>
+        <txVersionedHashes> HASHES </txVersionedHashes>
+      requires INDEX <Int size(HASHES)
+
     syntax BinStackOp ::= "MSTORE" | "MSTORE8"
  // ------------------------------------------
     rule <k> MSTORE INDEX VALUE => .K ... </k>
@@ -2289,6 +2297,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>
@@ -2453,6 +2462,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(  80,     _ ) => POP
     rule #dasmOpCode(  81,     _ ) => MLOAD
     rule #dasmOpCode(  82,     _ ) => MSTORE

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

@@ -29,7 +29,7 @@ module SCHEDULE
                           | "Ghassstorestipend"       | "Ghaschainid"      | "Ghasaccesslist"      | "Ghasbasefee"
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
                           | "Ghaswarmcoinbase"        | "Ghastransient"    | "Ghasmcopy"           | "Ghasbeaconroot"
-                          | "Ghaseip6780"
+                          | "Ghaseip6780"             | "Ghasblobhash"
  // -------------------------------------
 ```
 
@@ -151,6 +151,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
@@ -393,11 +394,13 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghasmcopy      << CANCUN >> => true
     rule Ghasbeaconroot << CANCUN >> => true
     rule Ghaseip6780    << CANCUN >> => true
+    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 Ghasblobhash
                        )
 ```
 ```k

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]
  // ---------------------------------------------------------------------------------------------

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

@@ -189,6 +189,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
@@ -378,7 +386,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
@@ -479,6 +487,7 @@ The `"rlp"` key loads the block information.
          => #if ( notBool Ghasbasefee << SCHED >> )
                 orBool TXTYPE ==K Legacy
                 orBool TXTYPE ==K AccessList
+                orBool TXTYPE ==K Blob
               #then GPRICE
               #else BFEE +Int minInt(TPF, TM -Int BFEE)
             #fi