EIP-4844: Add Blob transaction type

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,6 +390,7 @@ Accounts
 
 ```k
     syntax Account ::= ".Account" | Int
+    syntax AccountNotNil ::= Int
  // -----------------------------------
 
     syntax AccountCode ::= Bytes
@@ -442,27 +448,31 @@ 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: Bytes ) [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> .Bytes </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,18 @@ 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]
+    syntax Bytes ::= #addrBytes ( Account )             [symbol(#addrBytes),       function]
+                   | #addrBytesNotNil ( AccountNotNil ) [symbol(#addrBytesNotNil), 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(.Account)     => .Bytes
+    rule #addrBytes(ACCT)         => #padToWidth(20, #asByteStack(ACCT))   requires #rangeAddress(ACCT)
+    rule #addrBytesNotNil(ACCTNN) => #padToWidth(20, #asByteStack(ACCTNN)) requires #rangeAddress(ACCTNN)
+    rule #wordBytes(WORD)         => #padToWidth(32, #asByteStack(WORD))   requires #rangeUInt(256, WORD)
 ```
 
 Recursive Length Prefix (RLP)
@@ -349,6 +353,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, #addrBytesNotNil(TT), TV, DATA, [TA], TB, TVH ] )
 
     syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function]
  // ---------------------------------------------------------------------------------------------

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

@@ -426,6 +426,25 @@ The `"rlp"` key loads the block information.
            <txType> DynamicFee </txType>
            ...
          </message>
+
+    rule [[ #getTxData( TXID ) => BlobTxData(TN, TP, TF, TG, TT, TV, DATA, CID, TA, TB, TVH) ]]
+         <message>
+           <msgID>             TXID </msgID>
+           <txNonce>           TN   </txNonce>
+           <txGasPrice>        TP   </txGasPrice>
+           <txGasLimit>        TG   </txGasLimit>
+           <to>                TT   </to>
+           <value>             TV   </value>
+           <data>              DATA </data>
+           <txChainID>         CID  </txChainID>
+           <txAccess>          TA   </txAccess>
+           <txPriorityFee>     TP   </txPriorityFee>
+           <txMaxFee>          TF  </txMaxFee>
+           <txMaxBlobFee>      TB  </txMaxBlobFee>
+           <txVersionedHashes> TVH </txVersionedHashes>
+           <txType> Blob </txType>
+           ...
+         </message>
 ```
 
 - `#effectiveGasPrice` will compute the gas price for TXID, as specified by EIP-1559

tests/failing/ContractCreationSpam_d0g0v0.json.expected

@@ -319,6 +319,12 @@
           <txType>
             Legacy
           </txType>
+          <txMaxBlobFee>
+            0
+          </txMaxBlobFee>
+          <txVersionedHashes>
+            b""
+          </txVersionedHashes>
         </message>
       </messages>
     </network>

tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected

@@ -365,6 +365,12 @@
           <txType>
             Legacy
           </txType>
+          <txMaxBlobFee>
+            0
+          </txMaxBlobFee>
+          <txVersionedHashes>
+            b""
+          </txVersionedHashes>
         </message>
       </messages>
     </network>