Set field to to be not nil in Blob transactions

From the EIP specification: "The field `to` deviates slightly from the semantics with the exception that it *MUST NOT* be `nil` and therefore must always represent a 20-byte address. This means that blob transactions cannot have the form of a create transaction."

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
@@ -466,7 +472,7 @@ Productions related to transactions
                           | 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: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: Bytes ) [symbol(BlobTxData)]
+    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/serialization.md

@@ -229,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)
@@ -352,7 +355,7 @@ Encoding
       => #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), TV, DATA, [TA], TB, TVH ] )
+      => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytesNotNil(TT), TV, DATA, [TA], TB, TVH ] )
 
     syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function]
  // ---------------------------------------------------------------------------------------------