Balance check

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
 
@@ -33,7 +34,7 @@ def AddrMap.keys {α : Type} [Inhabited α] (self : AddrMap α) : Multiset Accou
   .ofList <| self.toList.map Prod.fst
 
 instance : LE ((_ : UInt256) × UInt256) where
-  le lhs rhs := if lhs.1 = rhs.1 then lhs.2 ≤ rhs.2 else lhs.1 ≤ rhs.1
+  le lhs rhs := if lhs.1.val = rhs.1.val then lhs.2.val ≤ rhs.2.val else lhs.1.val ≤ rhs.1.val
 
 instance : IsTrans ((_ : UInt256) × UInt256) (· ≤ ·) where
   trans a b c h₁ h₂ := by
@@ -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

@@ -31,6 +31,7 @@ private def fromBlobString {α} (f : Blob → Except String α) : FromJson α :=
   }
 
 instance : FromJson UInt256 := fromBlobString UInt256.fromBlob?
+instance : FromJson ℕ := fromBlobString Nat.fromBlob?
 
 instance : FromJson AccountAddress := fromBlobString AccountAddress.fromBlob?
 
@@ -55,11 +56,11 @@ Why is there no handy `unfold` - because of termination issues?
 -/
 def decodeMany (code : ByteArray) : Except String Code' := do
   let mut result : Code' := #[]
-  let mut pc := 0
-  while pc < code.size do
-    let (instr, arg) ← (EVM.decode code pc |>.toExceptWith s!"Cannot decode the instruction: {code.data.get! pc}")
+  let mut pc : UInt256 := ⟨0⟩
+  while pc.toNat < code.size do
+    let (instr, arg) ← (EVM.decode code pc |>.toExceptWith s!"Cannot decode the instruction: {code.data.get! pc.toNat}")
     result := result.push (instr, Prod.fst <$> arg)
-    pc := pc + 1 + arg.option 0 Prod.snd
+    pc := pc + .ofNat (1 + arg.option 0 Prod.snd)
   pure result
 
 end _Code'
@@ -94,6 +95,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"
@@ -102,18 +104,20 @@ instance : FromJson BlockHeader where
         receiptRoot   := TODO -- TODO - Does not seem to be used in Υ?
         logsBloom     := ← json.getObjValAsD! ByteArray "bloom"
         difficulty    := 0  -- [deprecated] 0.
-        number        := ← json.getObjValAsD! _         "number"        <&> UInt256.toNat
-        gasLimit      := ← json.getObjValAsD! _         "gasLimit"      <&> UInt256.toNat
-        gasUsed       := ← json.getObjValAsD! _         "gasUsed"       <&> UInt256.toNat
-        timestamp     := ← json.getObjValAsD! _         "timestamp"     <&> UInt256.toNat
+        number        := ← json.getObjValAsD! ℕ         "number"
+        gasLimit      := ← json.getObjValAsD! ℕ         "gasLimit"
+        gasUsed       := ← json.getObjValAsD! ℕ         "gasUsed"
+        timestamp     := ← json.getObjValAsD! ℕ         "timestamp"
         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
+        baseFeePerGas := ← json.getObjValAsD! ℕ         "baseFeePerGas"
         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 UInt64) "blobGasUsed"
+        excessBlobGas    := ← json.getObjValAsD! (Option UInt64) "excessBlobGas"
       }
     catch exct => dbg_trace s!"OOOOPSIE: {exct}\n json: {json}"
                   default
@@ -140,17 +144,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
@@ -160,7 +164,7 @@ instance : FromJson Transaction where
         -- Any other transaction now necessarily has an access list.
         let accessListTransaction : Transaction.WithAccessList :=
           {
-            chainId    := let mainnet : Nat := 1; mainnet
+            chainId    := ← json.getObjValAsD UInt256 "chainId" ⟨1⟩
             accessList := ← FromJson.fromJson? accessList <&> accessListToRBMap
             yParity    := ← json.getObjValAsD! UInt256 "v"
           }
@@ -170,13 +174,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 +217,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