Initial commit

.github/workflows/build-project.yml

@@ -0,0 +1,61 @@
+name: CI
+
+on:
+  pull_request:
+    branches:
+      - main
+
+jobs:
+  build-model:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: cache elan and mathlib
+        id: cache-elan-mathlib
+
+        uses: actions/cache@v3
+
+        env:
+          cache-name: cache-elan-mathlib
+
+        with:
+          path: |
+            .lake/packages/**
+            ~/.elan
+            ~/.profile
+          key: ${{ runner.os }}-${{ env.cache-name }}-${{ hashFiles('**/lakefile.lean') }}
+
+      - if: ${{ steps.cache-elan-mathlib.outputs.cache-hit != 'true' }}
+
+        name: install elan
+        run: |
+          set -o pipefail
+          curl -sSfL https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+          ./elan-init -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "${GITHUB_PATH}"
+
+      - if: ${{ steps.cache-elan-mathlib.outputs.cache-hit != 'true' }}
+
+        name: get cache
+        id: get
+        run: |
+          lake exe cache clean
+          lake exe cache get
+
+      - name: cache build
+        id: cache-build
+        uses: actions/cache@v3
+        env:
+          cache-name: cache-build
+        with:
+          path: |
+            .lake/build
+          key: ${{ runner.os }}-${{ env.cache-name }}-${{ hashFiles('**/lakefile.lean') }}
+
+      - name: build
+        run: |
+          source ~/.profile
+          lake build
+      

.gitignore

@@ -0,0 +1,3 @@
+*.olean
+.lake/
+vc/.stack-work/*

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "EthereumTests"]
+	path = EthereumTests
+	url = https://github.com/ethereum/tests

Conform/Exception.lean

@@ -0,0 +1,23 @@
+import EvmYul.EVM.Exception
+
+namespace EvmYul
+
+namespace Conform
+
+/--
+`Exception` represents the class of conformance testing errors.
+- `CannotParse`          - The `Json` of a test is malformed. `why` is the reason. 
+- `EVMError`             - There was an EVM `exc` error running code associated with `addr`.
+- `InvalidTestStructure` - The structure of tests has been violated. `why` is the reason. 
+- `TestFailed`           - The postState associated with `addr` differs from the state we arrived at
+                           by executing the model of the EVM starting in the state obtained from 
+                           pre associated with `addr`.
+-/
+inductive Exception :=
+  | CannotParse (why : String)
+  | EVMError (exc : EVM.Exception)
+  | InvalidTestStructure (why : String)
+  deriving Repr
+end Conform
+
+end EvmYul

Conform/Main.lean

@@ -0,0 +1,29 @@
+import Conform.TestRunner
+
+-- def TestsSubdir := "BlockchainTests"
+-- def isTestFile (file : System.FilePath) : Bool := file.extension.option false (· == "json")
+
+def SimpleFile := "EthereumTests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add.json"
+
+def TestsSubdir := "BlockchainTests"
+def isTestFile (file : System.FilePath) : Bool := file.extension.option false (· == "json")
+
+def main (args : List String) : IO Unit := do
+  if args.length != 1 then IO.println "Usage: conform <path to 'EthereumTests'>"; return ()
+
+  let testFiles ← Array.filter isTestFile <$> System.FilePath.walkDir (args.head! / TestsSubdir)
+
+  let mut dbgCount := 1
+
+  for testFile in testFiles do
+    if dbgCount == 0 then break
+
+    IO.println s!"File under test: {testFile}"
+    let res ← ExceptT.run <| EvmYul.Conform.processTestsOfFile testFile
+    match res with
+      | .error err         => IO.println s!"Error: {repr err}"
+      | .ok    testresults => IO.println s!"{repr testresults}"
+
+    dbgCount := dbgCount - 1
+
+-- #eval main ["EthereumTests"]

Conform/Model.lean

@@ -0,0 +1,133 @@
+import Lean.Data.RBMap
+import Lean.Data.Json
+
+import EvmYul.Wheels
+import EvmYul.Operations
+import EvmYul.EVM.State
+
+import Conform.Wheels
+
+import Mathlib.Tactic
+
+namespace EvmYul
+
+namespace Conform
+
+section Model
+
+open Lean
+
+abbrev AddrMap (α : Type) [Inhabited α] := Lean.RBMap Address α compare
+abbrev Storage := AddrMap UInt256
+
+def Storage.toFinmap (self : Storage) : Finmap (λ _ : UInt256 ↦ UInt256) :=
+  self.fold (init := ∅) λ acc k v ↦ acc.insert (UInt256.ofNat k.1) v
+
+def AddrMap.keys {α : Type} [Inhabited α] (self : AddrMap α) : Multiset Address :=
+  .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
+
+instance : IsTrans ((_ : UInt256) × UInt256) (· ≤ ·) where
+  trans a b c h₁ h₂ := by
+    rcases a with ⟨⟨a, ha⟩, ⟨a', ha'⟩⟩
+    rcases b with ⟨⟨b, hb⟩, ⟨b', hb'⟩⟩
+    rcases c with ⟨⟨c, hc⟩, ⟨c', hc'⟩⟩
+    unfold LE.le instLESigmaUInt256_conform at h₁ h₂ ⊢; simp at *
+    aesop (config := {warnOnNonterminal := false}) <;> omega
+
+instance : IsAntisymm ((_ : UInt256) × UInt256) (· ≤ ·) where
+  antisymm a b h₁ h₂ := by
+    rcases a with ⟨⟨a, ha⟩, ⟨a', ha'⟩⟩
+    rcases b with ⟨⟨b, hb⟩, ⟨b', hb'⟩⟩
+    unfold LE.le instLESigmaUInt256_conform at h₁ h₂; simp at *
+    aesop (config := {warnOnNonterminal := false}) <;> omega
+
+instance : IsTotal ((_ : UInt256) × UInt256) (· ≤ ·) where
+  total a b := by
+    rcases a with ⟨⟨a, ha⟩, ⟨a', ha'⟩⟩
+    rcases b with ⟨⟨b, hb⟩, ⟨b', hb'⟩⟩
+    unfold LE.le instLESigmaUInt256_conform; simp
+    aesop (config := {warnOnNonterminal := false}) <;> omega
+
+instance : DecidableRel (α := (_ : UInt256) × UInt256) (· ≤ ·) :=
+  λ a b ↦ by
+    rcases a with ⟨⟨a, ha⟩, ⟨a', ha'⟩⟩
+    rcases b with ⟨⟨b, hb⟩, ⟨b', hb'⟩⟩
+    unfold LE.le instLESigmaUInt256_conform; simp
+    aesop (config := {warnOnNonterminal := false}) <;> exact inferInstance
+
+def Storage.ofFinmap (m : Finmap (λ _ : UInt256 ↦ UInt256)) : Storage :=
+  let asList := computeToList! m.entries
+  Lean.RBMap.ofList (asList.map λ ⟨k, v⟩ ↦ (Address.ofUInt256 k, v))
+
+abbrev Code := ByteArray
+
+deriving instance Repr for ByteArray
+
+structure AccountEntry :=
+  balance : UInt256
+  code    : ByteArray
+  nonce   : UInt256
+  storage : Storage
+  deriving Inhabited, Repr
+
+abbrev Pre := AddrMap AccountEntry
+
+abbrev PostEntry := AccountEntry
+
+abbrev Post := AddrMap PostEntry
+
+abbrev Transactions := Array Transaction
+
+structure BlockEntry :=
+  blockHeader  : BlockHeader
+  rlp          : Json
+  transactions : Transactions
+  uncleHeaders : Json
+  withdrawals  : Json
+  deriving Inhabited
+
+abbrev Blocks := Array BlockEntry
+
+/--
+In theory, parts of the TestEntry could deserialise immediately into the underlying `EVM.State`.
+
+This would be ever so slightly cleaner, but before we understand the exact correlation
+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 :=
+  info               : Json := ""
+  blocks             : Blocks
+  genesisBlockHeader : Json := ""
+  genesisRLP         : Json := ""
+  lastblockhash      : Json := ""
+  network            : Json := ""
+  postState          : Post
+  pre                : Pre
+  sealEngine         : Json := ""
+  deriving Inhabited
+
+abbrev Test := Lean.RBMap String TestEntry compare 
+
+def TestResult := Option String
+  deriving Repr
+
+namespace TestResult
+
+def isSuccess (self : TestResult) : Bool := self matches none
+
+def isFailure (self : TestResult) : Bool := !self.isSuccess
+
+def mkFailed (reason : String := "") : TestResult := .some reason
+
+def mkSuccess : TestResult := .none
+
+def ofBool (success : Bool) : TestResult :=
+  if success then mkSuccess else mkFailed
+
+end TestResult
+
+end Model