EIP-4844: Add Blob transaction type

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

@@ -397,6 +397,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
     rule <k> loadTransaction _ { "s"                    : (TS:Bytes => #padToWidth(32, TS)), _ } ... </k> requires lengthBytes(TS) <Int 32
     rule <k> loadTransaction _ { "maxPriorityFeePerGas" : (V:Bytes  => #asWord(V)), _          } ... </k>
     rule <k> loadTransaction _ { "maxFeePerGas"         : (V:Bytes  => #asWord(V)), _          } ... </k>
+    rule <k> loadTransaction _ { "maxFeePerBlobGas"     : (V:Bytes  => #asWord(V)), _          } ... </k>
 ```
 
 ### Checking State
@@ -582,7 +583,7 @@ Here we check the other post-conditions associated with an EVM test.
     rule <k> check "transactions" : (_KEY     : (VALUE:String => #parseByteStack(VALUE))) ... </k>
     rule <k> check "transactions" : ("to"     : (VALUE:Bytes  => #asAccount(VALUE)))      ... </k>
     rule <k> check "transactions" : ( KEY     : (VALUE:Bytes  => #padToWidth(32, VALUE))) ... </k> requires KEY in (SetItem("r") SetItem("s")) andBool lengthBytes(VALUE) <Int 32
-    rule <k> check "transactions" : ( KEY     : (VALUE:Bytes  => #asWord(VALUE)))         ... </k> requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas"))
+    rule <k> check "transactions" : ( KEY     : (VALUE:Bytes  => #asWord(VALUE)))         ... </k> requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas") SetItem("maxFeePerBlobGas"))
     rule <k> check "transactions" : ("type"   : (VALUE:Int    => #asmTxPrefix(VALUE)))    ... </k>
 
     rule <k> check "transactions" : "accessList" : [ ACCESSLIST , REST ] => check "transactions" : "accessList" : ACCESSLIST  ~> check "transactions" : "accessList" : [ REST ] ... </k>
@@ -593,6 +594,11 @@ Here we check the other post-conditions associated with an EVM test.
     rule <k> check "transactions" : "accessList" : [ .JSONs ] => .K ... </k>
 
     rule <k> check "transactions" : "accessList" : "address" : ADDR : "storageKeys" : KEY        => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txAccess> TA </txAccess> ... </message> requires isInAccessList(ADDR, KEY, TA)
+
+    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" : ("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>
     rule <k> check "transactions" : ("gasPrice"             : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txGasPrice>    VALUE </txGasPrice>     ... </message>
@@ -606,6 +612,7 @@ Here we check the other post-conditions associated with an EVM test.
     rule <k> check "transactions" : ("type"                 : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txType>        VALUE </txType>         ... </message>
     rule <k> check "transactions" : ("maxFeePerGas"         : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxFee>      VALUE </txMaxFee>       ... </message>
     rule <k> check "transactions" : ("maxPriorityFeePerGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txPriorityFee> VALUE </txPriorityFee>  ... </message>
+    rule <k> check "transactions" : ("maxFeePerBlobGas"     : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxBlobFee>  VALUE </txMaxBlobFee>   ... </message>
     rule <k> check "transactions" : ("sender"               : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <sigV> TW </sigV> <sigR> TR </sigR> <sigS> TS </sigS> ... </message> <chainID> B </chainID> requires #sender( #getTxData(TXID), TW, TR, TS, B ) ==K VALUE
 
     syntax Bool ::= isInAccessListStorage ( Int , JSON )    [symbol(isInAccessListStorage), function]
@@ -620,6 +627,14 @@ 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

@@ -337,6 +337,8 @@ Bytes helper functions
 -   `#asInteger` will interpret a stack of bytes as a single arbitrary-precision integer (with MSB first).
 -   `#asAccount` will interpret a stack of bytes as a single account id (with MSB first).
     Differs from `#asWord` only in that an empty stack represents the empty account, not account zero.
+-   `asAccountNotNil` will interpret a stack of bytes as a single account id (with MSB first), but will fail if the
+    stack is empty.
 -   `#asByteStack` will split a single word up into a `Bytes`.
 -   `#range(WS, N, W)` access the range of `WS` beginning with `N` of width `W`.
 -   `#padToWidth(N, WS)` and `#padRightToWidth` make sure that a `Bytes` is the correct size.
@@ -350,11 +352,14 @@ Bytes helper functions
  // -------------------------------------------------------------------------
     rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete]
 
-    syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function]
- // ----------------------------------------------------------------------
+    syntax Account ::= #asAccount ( Bytes )             [symbol(#asAccount), function]
+    syntax AccountNotNil ::= #asAccountNotNil ( Bytes ) [symbol(#asAccountNotNil), function]
+ // ----------------------------------------------------------------------------------------
     rule #asAccount(BS) => .Account    requires lengthBytes(BS) ==Int 0
     rule #asAccount(BS) => #asWord(BS) [owise]
 
+    rule #asAccountNotNil(BS) => #asWord(BS) requires lengthBytes(BS) >Int 0
+
     syntax Bytes ::= #asByteStack ( Int ) [symbol(#asByteStack), function, total]
  // -----------------------------------------------------------------------------
     rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned) [concrete]
@@ -385,7 +390,8 @@ Accounts
 
 ```k
     syntax Account ::= ".Account" | Int
- // -----------------------------------
+    syntax AccountNotNil = Int
+ // --------------------------
 
     syntax AccountCode ::= Bytes
  // ----------------------------
@@ -442,28 +448,32 @@ Productions related to transactions
                     | "Legacy"
                     | "AccessList"
                     | "DynamicFee"
- // ------------------------------
+                    | "Blob"
+ // ------------------------
 
     syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function]
  // -------------------------------------------------------------------------
     rule #dasmTxPrefix (Legacy)     => 0
     rule #dasmTxPrefix (AccessList) => 1
     rule #dasmTxPrefix (DynamicFee) => 2
+    rule #dasmTxPrefix (Blob)       => 3
 
     syntax TxType ::= #asmTxPrefix ( Int ) [symbol(#asmTxPrefix), function]
  // -----------------------------------------------------------------------
     rule #asmTxPrefix (0) => Legacy
     rule #asmTxPrefix (1) => AccessList
     rule #asmTxPrefix (2) => DynamicFee
+    rule #asmTxPrefix (3) => Blob
 
-    syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx
- // --------------------------------------------------------
+    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 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)]
+ // ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 
 endmodule
 ```

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

@@ -167,6 +167,8 @@ In the comments next to each cell, we've marked which component of the YellowPap
                 <txPriorityFee> 0          </txPriorityFee> // T_f
                 <txMaxFee>      0          </txMaxFee>      // T_m
                 <txType>        .TxType    </txType>        // T_x
+                <txMaxBlobFee>  0          </txMaxBlobFee>
+                <txVersionedHashes> [ .JSONs ] </txVersionedHashes>
               </message>
             </messages>
 

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

@@ -141,7 +141,8 @@ The encoding schemes are applied in `#rlpEcondeTxData`.
     rule #hashTxData( TXDATA ) => Keccak256raw(                #rlpEncodeTxData(TXDATA) ) requires isLegacyTx    (TXDATA)
     rule #hashTxData( TXDATA ) => Keccak256raw( b"\x01" +Bytes #rlpEncodeTxData(TXDATA) ) requires isAccessListTx(TXDATA)
     rule #hashTxData( TXDATA ) => Keccak256raw( b"\x02" +Bytes #rlpEncodeTxData(TXDATA) ) requires isDynamicFeeTx(TXDATA)
-```
+    rule #hashTxData( TXDATA ) => Keccak256raw( b"\x03" +Bytes #rlpEncodeTxData(TXDATA) ) requires isBlobTx      (TXDATA)
+``` 
 
 The EVM test-sets are represented in JSON format with hex-encoding of the data and programs.
 Here we provide some standard parser/unparser functions for that format.
@@ -228,15 +229,16 @@ 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
 
 ```k
     syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function]
                    | #wordBytes ( Int )     [symbol(#wordBytes), function]
- // ----------------------------------------------------------------------
+ // ----------------------------------------------------------------------------------------
     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)
+    rule #addrBytes(ACCT)     => #padToWidth(20, #asByteStack(ACCT))   requires #rangeAddress(ACCT)
+    rule #wordBytes(WORD)     => #padToWidth(32, #asByteStack(WORD))   requires #rangeUInt(256, WORD)
 ```
 
 Recursive Length Prefix (RLP)
@@ -349,6 +351,9 @@ 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] ] )
 
     syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function]
  // ---------------------------------------------------------------------------------------------