Refactoring eip-4844 (#2752)

* updates to the blob transaction

* update conformance failing.llvm

* add inline documentation

* remove AccountNotNil unused sort

* update failing.llvm files

* update expected output

* update expected output 2

* update proofs

Author: anvacaru

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

@@ -75,6 +75,28 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
 -   `finishTx` is a place-holder for performing necessary cleanup after a transaction.
 
 ```k
+    syntax InternalOp ::= "#deductBlobGas"
+ // --------------------------------------
+    rule <k> #deductBlobGas => .K ... </k>
+         <schedule> SCHED </schedule>
+         <excessBlobGas> EXCESS_BLOB_GAS </excessBlobGas>
+         <origin> ACCTFROM </origin>
+         <account>
+           <acctID> ACCTFROM </acctID>
+           <balance> BAL => BAL -Int Cblobfee(SCHED, EXCESS_BLOB_GAS, size(TVH)) </balance>
+           ...
+         </account>
+         <txPending> ListItem(TXID:Int) ... </txPending>
+         <message>
+           <msgID>             TXID         </msgID>
+           <txVersionedHashes> TVH          </txVersionedHashes>
+           <txType>            Blob         </txType>
+           ...
+         </message>
+      requires Ghasblobbasefee << SCHED >>
+
+    rule <k> #deductBlobGas => .K ... </k> [owise]
+
     syntax EthereumCommand ::= "startTx"
  // ------------------------------------
     rule <k> startTx => #finalizeBlock ... </k>
@@ -108,6 +130,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
 
     rule <k> loadTx(ACCTFROM)
           => #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
+          ~> #deductBlobGas
           ~> #loadAccessList(TA)
           ~> #checkCreate ACCTFROM VALUE
           ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
@@ -128,24 +151,23 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <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>
            <nonce> NONCE </nonce>
-           <code> ACCTCODE </code>
            ...
          </account>
          <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
       requires #hasValidInitCode(lengthBytes(CODE), SCHED)
-        andBool ACCTCODE ==K .Bytes
+       andBool #isValidTransaction(TXID, ACCTFROM)
+
 
     rule <k> loadTx(ACCTFROM)
           => #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
+          ~> #deductBlobGas
           ~> #loadAccessList(TA)
           ~> #checkCall ACCTFROM VALUE
           ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
@@ -174,16 +196,15 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <acctID> ACCTFROM </acctID>
            <balance> BAL => BAL -Int (GLIMIT *Int #effectiveGasPrice(TXID)) </balance>
            <nonce> NONCE => NONCE +Int 1 </nonce>
-           <code> ACCTCODE </code>
            ...
          </account>
          <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
       requires ACCTTO =/=K .Account
-        andBool ACCTCODE ==K .Bytes
+       andBool #isValidTransaction(TXID, ACCTFROM)
 
     rule <k> loadTx(ACCTFROM) => startTx ... </k>
-         <statusCode> _ => EVMC_FAILURE </statusCode>
+         <statusCode> _ => EVMC_INVALID_BLOCK </statusCode>
          <txPending> ListItem(_TXID:Int) REST => REST </txPending>
          <account>
            <acctID> ACCTFROM </acctID>

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

@@ -337,8 +337,6 @@ 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.
@@ -353,13 +351,10 @@ Bytes helper functions
     rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete]
 
     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]
@@ -390,8 +385,7 @@ Accounts
 
 ```k
     syntax Account ::= ".Account" | Int
-    syntax AccountNotNil = Int
- // --------------------------
+ // -----------------------------------
 
     syntax AccountCode ::= Bytes
  // ----------------------------
@@ -468,12 +462,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: List ) [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: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: List ) [symbol(BlobTxData)]
+ // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
 
 endmodule
 ```