Update tests

Conform/Model.lean

@@ -5,6 +5,7 @@ import Lean.Data.Json
 import EvmYul.Operations
 import EvmYul.Wheels
 import EvmYul.State.Withdrawal
+import EvmYul.State.Block
 
 import EvmYul.EVM.State
 
@@ -91,17 +92,17 @@ TODO - Temporary.
 -/
 private local instance : Repr Json := ⟨λ s _ ↦ Json.pretty s⟩
 
-structure BlockEntry :=
-  blockHeader  : BlockHeader
-  rlp          : Json
-  transactions : Transactions
-  uncleHeaders : Json
-  withdrawals  : Withdrawals
-  exception    : String -- TODO - I am guessing there is a closed set of these to turn into a sum.
-  blocknumber  : Nat
-  deriving Inhabited, Repr
+-- structure BlockEntry :=
+--   blockHeader  : BlockHeader
+--   rlp          : ByteArray
+--   transactions : Transactions
+--   ommers       : Array BlockHeader
+--   withdrawals  : Withdrawals
+--   exception    : String -- TODO - I am guessing there is a closed set of these to turn into a sum.
+--   -- blocknumber  : Nat
+--   deriving Inhabited, Repr
 
-abbrev Blocks := Array BlockEntry
+-- abbrev Blocks := Array BlockEntry
 
 /--
 In theory, parts of the TestEntry could deserialise immediately into the underlying `EVM.State`.
@@ -113,10 +114,10 @@ an EVM model and write translations between them where convenient.
 structure TestEntry :=
   info               : Json := ""
   blocks             : Blocks
-  genesisBlockHeader : Json := ""
+  genesisBlockHeader : BlockHeader
   genesisRLP         : Json := ""
   lastblockhash      : Json := ""
-  network            : Json := ""
+  network            : String
   postState          : Post
   pre                : Pre
   sealEngine         : Json := ""

Conform/TestParser.lean

@@ -94,6 +94,7 @@ instance : FromJson BlockHeader where
   fromJson? json := do
     try
       pure {
+        hash          := ← json.getObjValAsD! UInt256   "hash"
         parentHash    := ← json.getObjValAsD! UInt256   "parentHash"
         ommersHash    := TODO -- TODO - Set to whatever the KEC(RLP()) evaluates to.
         beneficiary   := ← json.getObjValAsD! AccountAddress   "coinbase"
@@ -108,12 +109,14 @@ instance : FromJson BlockHeader where
         timestamp     := ← json.getObjValAsD! _         "timestamp"     <&> UInt256.toNat
         extraData     := ← json.getObjValAsD! ByteArray "extraData"
         minHash       := TODO -- TODO - Does not seem to be used in Υ?
-        chainId       := 1 -- (5)
+        chainId       := ← json.getObjValAsD UInt256 "chainId" 1 -- (5)
         nonce         := 0 -- [deprecated] 0.
         baseFeePerGas := ← json.getObjValAsD! _         "baseFeePerGas" <&> UInt256.toNat
         parentBeaconBlockRoot := ← json.getObjValAsD! ByteArray "parentBeaconBlockRoot"
         prevRandao    := ← json.getObjValAsD! UInt256 "mixHash"
-        withdrawalsRoot := ← json.getObjValAsD! ByteArray "withdrawalsRoot"
+        withdrawalsRoot := ← json.getObjValAsD! (Option ByteArray) "withdrawalsRoot"
+        blobGasUsed    := ← json.getObjValAsD! (Option UInt256) "blobGasUsed"
+        excessBlobGas    := ← json.getObjValAsD! (Option UInt256) "excessBlobGas"
       }
     catch exct => dbg_trace s!"OOOOPSIE: {exct}\n json: {json}"
                   default
@@ -140,17 +143,17 @@ TODO - Currently we return `AccessListTransaction`. No idea if this is what we w
 instance : FromJson Transaction where
   fromJson? json := do
     let baseTransaction : Transaction.Base := {
-      nonce     := ← json.getObjValAsD! UInt256        "nonce"
-      gasLimit  := ← json.getObjValAsD! UInt256        "gasLimit"
-      recipient := ← match json.getObjVal? "to" with
-                     | .error _ => .ok .none
-                     | .ok ok => do let str ← ok.getStr?
-                                    if str.isEmpty then .ok .none else FromJson.fromJson? str
-      value     := ← json.getObjValAsD! UInt256        "value"
-      r         := ← json.getObjValAsD! ByteArray      "r"
-      s         := ← json.getObjValAsD! ByteArray      "s"
-      data      := ← json.getObjValAsD! ByteArray      "data"
-      dbgSender := ← json.getObjValAsD! AccountAddress        "sender"
+      nonce          := ← json.getObjValAsD! UInt256        "nonce"
+      gasLimit       := ← json.getObjValAsD! UInt256        "gasLimit"
+      recipient      := ← match json.getObjVal? "to" with
+                          | .error _ => .ok .none
+                          | .ok ok => do let str ← ok.getStr?
+                                         if str.isEmpty then .ok .none else FromJson.fromJson? str
+      value          := ← json.getObjValAsD! UInt256        "value"
+      r              := ← json.getObjValAsD! ByteArray      "r"
+      s              := ← json.getObjValAsD! ByteArray      "s"
+      data           := ← json.getObjValAsD! ByteArray      "data"
+      expectedSender := ← json.getObjValAsD! AccountAddress "sender"
     }
 
     match json.getObjVal? "accessList" with
@@ -170,13 +173,24 @@ instance : FromJson Transaction where
             -- dbg_trace "Constructing an access transaction."
             return .access ⟨baseTransaction, accessListTransaction, ⟨← FromJson.fromJson? gasPrice⟩⟩
           | .error _ =>
-            -- dbg_trace "Constructing an dynamic transaction."
-            return .dynamic ⟨
-                     baseTransaction,
-                     accessListTransaction,
-                     ← json.getObjValAsD! UInt256 "maxFeePerGas",
-                     ← json.getObjValAsD! UInt256 "maxPriorityFeePerGas"
-                   ⟩
+            let dynamic : DynamicFeeTransaction :=
+              ⟨ baseTransaction
+              , accessListTransaction
+              , ← json.getObjValAsD! UInt256 "maxFeePerGas"
+              , ← json.getObjValAsD! UInt256 "maxPriorityFeePerGas"
+              ⟩
+            match json.getObjVal? "maxFeePerBlobGas" with
+            | .error _ =>
+              pure <| .dynamic dynamic
+            | .ok maxFeePerBlobGas =>
+              -- dbg_trace "Constructing a blob transaction."
+              pure <|
+                .blob
+                  ⟨ dynamic
+                  , ← FromJson.fromJson? maxFeePerBlobGas
+                  , ← json.getObjValAsD! (List ByteArray) "blobVersionedHashes"
+                  ⟩
+
 
   where accessListToRBMap (this : AccessList) : Batteries.RBMap AccountAddress (Array UInt256) compare :=
     this.foldl (init := ∅) λ m ⟨addr, list⟩ ↦ m.insert addr list
@@ -202,25 +216,26 @@ instance : FromJson Transaction where
 TODO -
 - `EthereumTests/BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_blob_tx_contract_creation.json` - ?????
 -/
-private def blockEntryOfJson (json : Json) : Except String BlockEntry := do
+private def blockOfJson (json : Json) : Except String Block := do
   -- The exception, if exists, is always in the outermost object regardless of the `<Format>` (see this function's docs).
   let exception ← json.getObjValAsD! String "expectException"
   -- Descend to `rlp_decoded` - Format₁ if exists, Format₀ otherwise.
   let json ← json.getObjValAsD Json "rlp_decoded" json
   pure {
-    blockHeader  := ← json.getObjValAsD! BlockHeader  "blockHeader"
-    rlp          := ← json.getObjValAsD! Json         "rlp"
+    blockHeader  := ← json.getObjValAsD! BlockHeader "blockHeader"
+    rlp          := ← json.getObjValAsD! ByteArray "rlp"
     transactions := ← json.getObjValAsD! Transactions "transactions"
-    uncleHeaders := ← json.getObjValAsD! Json         "uncleHeaders"
-    withdrawals  := ← json.getObjValAsD! Withdrawals  "withdrawals"
-    blocknumber  := ← json.getObjValAsD  _            "blocknumber" "1" >>= tryParseBlocknumber
+    ommers       := ← json.getObjValAsD! (Array BlockHeader) "uncleHeaders"
+    withdrawals  := ← json.getObjValAsD! Withdrawals "withdrawals"
+    -- The block's number should be in the header.
+    -- blocknumber  := ← json.getObjValAsD  _ "blocknumber" "1" >>= tryParseBlocknumber
     exception    := exception
   }
   where
     tryParseBlocknumber (s : String) : Except String Nat :=
       s.toNat?.elim (.error "Cannot parse `blocknumber`.") .ok
 
-instance : FromJson BlockEntry := ⟨blockEntryOfJson⟩
+instance : FromJson Block := ⟨blockOfJson⟩
 
 deriving instance FromJson for TestEntry