Check exception

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
 
@@ -20,20 +21,11 @@ section Model
 
 open Lean
 
-abbrev AddrMap (α : Type) [Inhabited α] := Batteries.RBMap AccountAddress α compare
-abbrev Storage := Batteries.RBMap UInt256 UInt256 compare
-
-def Storage.toFinmap (self : Storage) : Finmap (λ _ : UInt256 ↦ UInt256) :=
-  self.foldl (init := ∅) λ acc k v ↦ acc.insert (UInt256.ofNat k.1) v
-
-def Storage.toEvmYulStorage (self : Storage) : EvmYul.Storage :=
-  self.foldl (init := ∅) λ acc k v ↦ acc.insert (UInt256.ofNat k.1) v
-
 def AddrMap.keys {α : Type} [Inhabited α] (self : AddrMap α) : Multiset AccountAddress :=
   .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
@@ -69,16 +61,9 @@ instance : DecidableRel (α := (_ : UInt256) × UInt256) (· ≤ ·) :=
 
 abbrev Code := ByteArray
 
-structure AccountEntry :=
-  nonce   : UInt256
-  balance : UInt256
-  storage : Storage
-  code    : ByteArray
-  deriving Inhabited, Repr, BEq
-
-abbrev Pre := AddrMap AccountEntry
+abbrev Pre := AddrMap PersistentAccountState
 
-abbrev PostEntry := AccountEntry
+abbrev PostEntry := PersistentAccountState
 
 abbrev Post := AddrMap PostEntry
 
@@ -91,17 +76,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`.
@@ -110,24 +95,39 @@ This would be ever so slightly cleaner, but before we understand the exact corre
 between all of the test file entires and the states, we sometimes keep a 'parsing model' *and*
 an EVM model and write translations between them where convenient.
 -/
-structure TestEntry :=
+
+inductive PostState :=
+  | Hash : ByteArray → PostState
+  | Map : Post → PostState
+  deriving Inhabited
+
+structure RawTestEntry :=
   info               : Json := ""
-  blocks             : Blocks
-  genesisBlockHeader : Json := ""
+  blocks             : RawBlocks
+  genesisBlockHeader : BlockHeader
   genesisRLP         : Json := ""
   lastblockhash      : Json := ""
-  network            : Json := ""
-  postState          : Post
+  network            : String
+  postState          : PostState
   pre                : Pre
   sealEngine         : Json := ""
   deriving Inhabited
 
-abbrev Test := Batteries.RBMap String TestEntry compare
+abbrev RawTestMap := Batteries.RBMap String RawTestEntry compare
+
+structure DeserializedTestEntry :=
+  info               : Json := ""
+  blocks             : DeserializedBlocks
+  genesisBlockHeader : BlockHeader
+  genesisRLP         : Json := ""
+  network            : String
+  postState          : PostState
+  pre                : Pre
+  deriving Inhabited
+
+abbrev DeserializedTestMap := Batteries.RBMap String DeserializedTestEntry compare
 
-structure AccessListEntry :=
-  address     : AccountAddress
-  storageKeys : Array UInt256
-  deriving Inhabited, Repr
+abbrev AccessListEntry := AccountAddress × Array UInt256
 
 abbrev AccessList := Array AccessListEntry
 

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'
@@ -72,7 +73,7 @@ This is also applicable for `FromJson Code`, as this is an abbrev for `ByteArray
 -/
 instance : FromJson ByteArray := fromBlobString (ByteArray.ofBlob)
 
-instance : FromJson AccountEntry where
+instance : FromJson PersistentAccountState where
   fromJson? json := do
     pure {
       balance := ← json.getObjValAs? UInt256 "balance"
@@ -82,7 +83,7 @@ instance : FromJson AccountEntry where
     }
 
 instance : FromJson Pre where
-  fromJson? json := json.getObjVals? AccountAddress AccountEntry
+  fromJson? json := json.getObjVals? AccountAddress PersistentAccountState
 
 instance : FromJson Post where
   fromJson? json := json.getObjVals? AccountAddress PostEntry
@@ -95,35 +96,34 @@ instance : FromJson BlockHeader where
     try
       pure {
         parentHash    := ← json.getObjValAsD! UInt256   "parentHash"
-        ommersHash    := TODO -- TODO - Set to whatever the KEC(RLP()) evaluates to.
+        ommersHash    := ← json.getObjValAsD! UInt256   "uncleHash"
         beneficiary   := ← json.getObjValAsD! AccountAddress   "coinbase"
         stateRoot     := ← json.getObjValAsD! UInt256   "stateRoot"
-        transRoot     := TODO -- TODO - Does not seem to be used in Υ?
-        receiptRoot   := TODO -- TODO - Does not seem to be used in Υ?
+        transRoot     := ← json.getObjValAsD! UInt256   "transactionsTrie"
+        receiptRoot   := ← json.getObjValAsD! UInt256   "receiptTrie"
         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
+        difficulty    := ← json.getObjValAsD! ℕ         "difficulty"
+        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)
         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
 
 instance : FromJson AccessListEntry where
   fromJson? json := do
-    pure {
-      address     := ← json.getObjValAs? AccountAddress         "address"
-      storageKeys := ← json.getObjValAs? (Array UInt256) "storageKeys"
-    }
+    let address     := ← json.getObjValAs? AccountAddress "address"
+    let storageKeys := ← json.getObjValAs? (Array UInt256) "storageKeys"
+    pure (address, storageKeys)
 
 instance : FromJson Withdrawal where
   fromJson? json := do
@@ -140,17 +140,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,8 +160,8 @@ instance : FromJson Transaction where
         -- Any other transaction now necessarily has an access list.
         let accessListTransaction : Transaction.WithAccessList :=
           {
-            chainId    := let mainnet : Nat := 1; mainnet
-            accessList := ← FromJson.fromJson? accessList <&> accessListToRBMap
+            chainId    := ← json.getObjValAsD UInt256 "chainId" ⟨1⟩
+            accessList := ← FromJson.fromJson? accessList
             yParity    := ← json.getObjValAsD! UInt256 "v"
           }
 
@@ -170,16 +170,25 @@ 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
 
 -- #eval DebuggingAndProfiling.testJsonParser Transaction r#"
 --                     {
@@ -198,47 +207,82 @@ instance : FromJson Transaction where
 /--
 - Format₀: `EthereumTests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add.json`
 - Format₁: `EthereumTests/BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_static_excess_blob_gas.json`
-
-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 RawBlock := 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"
+  let rlp ← json.getObjValAsD! ByteArray "rlp"
   -- Descend to `rlp_decoded` - Format₁ if exists, Format₀ otherwise.
-  let json ← json.getObjValAsD Json "rlp_decoded" json
+  -- let json ← json.getObjValAsD Json "rlp_decoded" json
+  -- let blockHeader  ← json.getObjValAsD! (Option BlockHeader) "blockHeader"
+  -- let transactions ← json.getObjValAsD! (Option Transactions) "transactions"
+  -- let withdrawals  ← json.getObjValAsD! (Option Withdrawals) "withdrawals"
+
+  -- if blockHeader == none then
+  --   dbg_trace "blockHeader is none"
+  -- if transactions == none then
+  --   dbg_trace "transactions is none"
+  -- if withdrawals == none then
+  --   dbg_trace "withdrawals is none"
+
   pure {
-    blockHeader  := ← json.getObjValAsD! BlockHeader  "blockHeader"
-    rlp          := ← json.getObjValAsD! Json         "rlp"
-    transactions := ← json.getObjValAsD! Transactions "transactions"
-    uncleHeaders := ← json.getObjValAsD! Json         "uncleHeaders"
-    withdrawals  := ← json.getObjValAsD! Withdrawals  "withdrawals"
-    blocknumber  := ← json.getObjValAsD  _            "blocknumber" "1" >>= tryParseBlocknumber
-    exception    := exception
+    rlp
+    blockHeader := none -- := ← json.getObjValAsD! (Option BlockHeader) "blockHeader"
+    transactions := none -- := ← json.getObjValAsD! (Option Transactions) "transactions"
+    withdrawals := none --  := ← json.getObjValAsD! (Option Withdrawals) "withdrawals"
+    exception --    := exception
   }
   where
     tryParseBlocknumber (s : String) : Except String Nat :=
       s.toNat?.elim (.error "Cannot parse `blocknumber`.") .ok
 
-instance : FromJson BlockEntry := ⟨blockEntryOfJson⟩
-
-deriving instance FromJson for TestEntry
+instance : FromJson RawBlock := ⟨blockOfJson⟩
+
+-- instance : FromJson PostState where
+--   fromJson? json := do
+--     let hash ← json.getObjValAsD! (Option ByteArray) "postStateHash"
+--     match hash with
+--       | some hash =>
+--         dbg_trace s!"Read postStateHash: {hash}"
+--         .ok <| PostState.Hash hash
+--       | none =>
+--         let map ← json.getObjValAsD! Post "postState"
+--         dbg_trace s!"Read post state map of size {map.size}"
+--         .ok <| PostState.Map map
+
+instance : FromJson RawTestEntry where
+  fromJson? json := do
+    let post : PostState ←
+      match json.getObjVal? "postStateHash" with
+        | .error _ =>
+          -- dbg_trace s!"Read post state map"
+          .Map <$> json.getObjValAsD! PersistentAccountMap "postState"
+        | .ok postStateHash =>
+          -- dbg_trace s!"Read postStateHash: {postStateHash}"
+          .Hash <$> FromJson.fromJson? postStateHash
+    pure {
+      info               := ← json.getObjValAs? Json "info"
+      blocks             := ← json.getObjValAs? RawBlocks "blocks"
+      genesisBlockHeader := ← json.getObjValAs? BlockHeader "genesisBlockHeader"
+      genesisRLP         := ← json.getObjValAs? Json "genesisRLP"
+      lastblockhash      := ← json.getObjValAs? Json "lastblockhash"
+      network            := ← json.getObjValAs? String "network"
+      postState          := post
+      pre                := ← json.getObjValAs? Pre "pre"
+      sealEngine         := ← json.getObjValAs? Json "sealEngine"
+    }
 
-instance : FromJson Test where
-  fromJson? json := json.getObjVals? String TestEntry
+instance : FromJson RawTestMap where
+  fromJson? json := json.getObjVals? String RawTestEntry
 
 end FromJson
 
 def testNamesOfTest (test : Lean.Json) : Except String (Array String) :=
   test.getObj? <&> (·.toArray.map Sigma.fst)
 
-namespace Test
-
-end Test
-
 section PrettyPrinter
 
-instance : ToString AccountEntry := ⟨ToString.toString ∘ repr⟩
+instance : ToString PersistentAccountState := ⟨ToString.toString ∘ repr⟩
 
 instance : ToString Pre := ⟨ToString.toString ∘ repr⟩