From 43f1d82b80f18f2d3a878fa8b4a4e00ad0bf50df Mon Sep 17 00:00:00 2001 From: Frantisek Silvasi Date: Wed, 19 Jun 2024 15:11:12 +0200 Subject: [PATCH] Initial commit --- .github/workflows/build-project.yml | 61 +++ .gitignore | 3 + .gitmodules | 3 + Conform/Exception.lean | 23 + Conform/Main.lean | 29 ++ Conform/Model.lean | 133 +++++ Conform/TestParser.lean | 176 +++++++ Conform/TestRunner.lean | 88 ++++ Conform/Wheels.lean | 128 +++++ EthereumTests | 1 + EvmYul.lean | 42 ++ EvmYul/Data/Stack.lean | 86 ++++ EvmYul/EVM/Exception.lean | 34 ++ EvmYul/EVM/Instr.lean | 564 ++++++++++++++++++++ EvmYul/EVM/PrimOps.lean | 167 ++++++ EvmYul/EVM/Semantics.lean | 688 +++++++++++++++++++++++++ EvmYul/EVM/State.lean | 22 + EvmYul/EVM/StateOps.lean | 49 ++ EvmYul/MachineState.lean | 35 ++ EvmYul/MachineStateOps.lean | 113 ++++ EvmYul/Operations.lean | 765 ++++++++++++++++++++++++++++ EvmYul/Semantics.lean | 422 +++++++++++++++ EvmYul/SharedState.lean | 9 + EvmYul/SharedStateOps.lean | 64 +++ EvmYul/SpongeHash/Keccak256.lean | 206 ++++++++ EvmYul/SpongeHash/Wheels.lean | 52 ++ EvmYul/State.lean | 38 ++ EvmYul/State/Account.lean | 31 ++ EvmYul/State/AccountOps.lean | 40 ++ EvmYul/State/Block.lean | 22 + EvmYul/State/BlockHeader.lean | 51 ++ EvmYul/State/ExecutionEnv.lean | 33 ++ EvmYul/State/Substate.lean | 26 + EvmYul/State/SubstateOps.lean | 15 + EvmYul/State/Transaction.lean | 88 ++++ EvmYul/StateOps.lean | 154 ++++++ EvmYul/UInt256.lean | 346 +++++++++++++ EvmYul/Wheels.lean | 96 ++++ EvmYul/Yul/Ast.lean | 81 +++ EvmYul/Yul/Exception.lean | 13 + EvmYul/Yul/Interpreter.lean | 228 +++++++++ EvmYul/Yul/MachineState.lean | 17 + EvmYul/Yul/PrimOps.lean | 150 ++++++ EvmYul/Yul/SizeLemmas.lean | 133 +++++ EvmYul/Yul/State.lean | 50 ++ EvmYul/Yul/StateOps.lean | 161 ++++++ EvmYul/Yul/Wheels.lean | 13 + EvmYul/Yul/YulNotation.lean | 477 +++++++++++++++++ README.md | 44 ++ SpongeHash.lean | 4 + lake-manifest.json | 68 +++ lakefile.lean | 18 + lean-toolchain | 1 + license.txt | 201 ++++++++ 54 files changed, 6562 insertions(+) create mode 100644 .github/workflows/build-project.yml create mode 100644 .gitignore create mode 100644 .gitmodules create mode 100644 Conform/Exception.lean create mode 100644 Conform/Main.lean create mode 100644 Conform/Model.lean create mode 100644 Conform/TestParser.lean create mode 100644 Conform/TestRunner.lean create mode 100644 Conform/Wheels.lean create mode 160000 EthereumTests create mode 100644 EvmYul.lean create mode 100644 EvmYul/Data/Stack.lean create mode 100644 EvmYul/EVM/Exception.lean create mode 100644 EvmYul/EVM/Instr.lean create mode 100644 EvmYul/EVM/PrimOps.lean create mode 100644 EvmYul/EVM/Semantics.lean create mode 100644 EvmYul/EVM/State.lean create mode 100644 EvmYul/EVM/StateOps.lean create mode 100644 EvmYul/MachineState.lean create mode 100644 EvmYul/MachineStateOps.lean create mode 100644 EvmYul/Operations.lean create mode 100644 EvmYul/Semantics.lean create mode 100644 EvmYul/SharedState.lean create mode 100644 EvmYul/SharedStateOps.lean create mode 100644 EvmYul/SpongeHash/Keccak256.lean create mode 100644 EvmYul/SpongeHash/Wheels.lean create mode 100644 EvmYul/State.lean create mode 100644 EvmYul/State/Account.lean create mode 100644 EvmYul/State/AccountOps.lean create mode 100644 EvmYul/State/Block.lean create mode 100644 EvmYul/State/BlockHeader.lean create mode 100644 EvmYul/State/ExecutionEnv.lean create mode 100644 EvmYul/State/Substate.lean create mode 100644 EvmYul/State/SubstateOps.lean create mode 100644 EvmYul/State/Transaction.lean create mode 100644 EvmYul/StateOps.lean create mode 100644 EvmYul/UInt256.lean create mode 100644 EvmYul/Wheels.lean create mode 100644 EvmYul/Yul/Ast.lean create mode 100644 EvmYul/Yul/Exception.lean create mode 100644 EvmYul/Yul/Interpreter.lean create mode 100644 EvmYul/Yul/MachineState.lean create mode 100644 EvmYul/Yul/PrimOps.lean create mode 100644 EvmYul/Yul/SizeLemmas.lean create mode 100644 EvmYul/Yul/State.lean create mode 100644 EvmYul/Yul/StateOps.lean create mode 100644 EvmYul/Yul/Wheels.lean create mode 100644 EvmYul/Yul/YulNotation.lean create mode 100644 README.md create mode 100644 SpongeHash.lean create mode 100644 lake-manifest.json create mode 100644 lakefile.lean create mode 100644 lean-toolchain create mode 100644 license.txt diff --git a/.github/workflows/build-project.yml b/.github/workflows/build-project.yml new file mode 100644 index 0000000..a975385 --- /dev/null +++ b/.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 + \ No newline at end of file diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..37c1270 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +*.olean +.lake/ +vc/.stack-work/* \ No newline at end of file diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..67f01f4 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "EthereumTests"] + path = EthereumTests + url = https://github.com/ethereum/tests diff --git a/Conform/Exception.lean b/Conform/Exception.lean new file mode 100644 index 0000000..265a5d5 --- /dev/null +++ b/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 diff --git a/Conform/Main.lean b/Conform/Main.lean new file mode 100644 index 0000000..83bef99 --- /dev/null +++ b/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 "; 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"] diff --git a/Conform/Model.lean b/Conform/Model.lean new file mode 100644 index 0000000..92d3003 --- /dev/null +++ b/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 diff --git a/Conform/TestParser.lean b/Conform/TestParser.lean new file mode 100644 index 0000000..74f26f2 --- /dev/null +++ b/Conform/TestParser.lean @@ -0,0 +1,176 @@ +import Lean.Data.Json + +import EvmYul.Wheels +import EvmYul.Operations +import EvmYul.EVM.Semantics + +import Conform.Model +import Conform.Wheels + +namespace EvmYul + +namespace Conform + +namespace Parser + +section FromJson + +open Lean (FromJson Json) + +/-- +Sorries are often +-/ +@[deprecated] +scoped notation "TODO" => default + +private def fromBlobString {α} (f : Blob → Except String α) : FromJson α := + { + fromJson? := λ json ↦ json.getStr? >>= (getBlob? · >>= f) + } + +instance : FromJson UInt256 := fromBlobString UInt256.fromBlob? + +instance : FromJson Address := fromBlobString Address.fromBlob? + +instance : FromJson Storage where + fromJson? json := json.getObjVals? Address UInt256 + +section _Code' +-- The `_Code'` section is auxiliary and the functionality inside is currently unused. + +/-- +We probably want to fetch/decode on demand, as such, `Conform.Code` can be a `ByteArray`. +Keep this around for potential convenience. +-/ +abbrev Code' := Array (Operation .EVM × Option UInt256) + +/-- +Decode `ByteArray` to an array of `Operation`s. Considering we do decoding on demand, +this is only kept around for potential conveninece. + +TODO: This is essentially `unfold` with `f := EVM.decode code`. +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}") + result := result.push (instr, Prod.fst <$> arg) + pc := pc + 1 + arg.option 0 Prod.snd + pure result + +end _Code' + + +/-- +TODO - Is this right for both `Code` and general `ByteArray`s? + +This is also applicable for `FromJson Code`, as this is an abbrev for `ByteArray`. +-/ +instance : FromJson ByteArray := fromBlobString (ByteArray.ofBlob) + +instance : FromJson AccountEntry where + fromJson? json := do + pure { + balance := ← json.getObjValAs? UInt256 "balance" + nonce := ← json.getObjValAs? UInt256 "nonce" + code := ← json.getObjValAs? Code "code" + storage := ← json.getObjValAs? Storage "storage" + } + +instance : FromJson Pre where + fromJson? json := json.getObjVals? Address AccountEntry + +instance : FromJson Post where + fromJson? json := json.getObjVals? Address PostEntry + +/-- +TODO: We parse ℕ-valued scalars as though they were at most UInt256; could need changing. +-/ +instance : FromJson BlockHeader where + fromJson? json := do + try + pure { + parentHash := ← json.getObjValAsOrInit? UInt256 "parentHash" + ommersHash := TODO -- TODO - Set to whatever the KEC(RLP()) evaluates to. + beneficiary := TODO + stateRoot := ← json.getObjValAsOrInit? UInt256 "stateRoot" + transRoot := TODO + receiptRoot := TODO + logsBloom := ← json.getObjValAsOrInit? ByteArray "bloom" + difficulty := 0 -- [deprecated] 0. + number := ← json.getObjValAsOrInit? _ "number" <&> UInt256.toNat + gasLimit := ← json.getObjValAsOrInit? _ "gasLimit" <&> UInt256.toNat + gasUsed := ← json.getObjValAsOrInit? _ "gasUsed" <&> UInt256.toNat + timestamp := ← json.getObjValAsOrInit? _ "timestamp" <&> UInt256.toNat + extraData := ← json.getObjValAsOrInit? ByteArray "extraData" + minHash := TODO + chainId := TODO + nonce := 0 -- [deprecated] 0. + baseFeePerGas := ← json.getObjValAsOrInit? _ "baseFeePerGas" <&> UInt256.toNat + } + catch exct => dbg_trace s!"OOOOPSIE: {exct}\n json: {json}" + default + +/-- +TODO - Currently we return `AccessListTransaction`. No idea if this is what we want. +-/ +instance : FromJson Transaction where + fromJson? json := do + pure <| .access { + nonce := ← json.getObjValAs? UInt256 "nonce" + gasLimit := ← json.getObjValAs? UInt256 "gasLimit" + recipient := ← json.getObjValAs? (Option Address) "to" -- TODO - How do test represent no 'to' - just missing field? Refine this. + value := ← json.getObjValAs? UInt256 "value" + r := ← json.getObjValAs? ByteArray "r" + s := ← json.getObjValAs? ByteArray "s" + data := ← json.getObjValAs? ByteArray "data" + gasPrice := ← json.getObjValAs? UInt256 "gasPrice" + chainId := TODO + accessList := TODO -- TODO - Not sure this needs initialising in tests. + } + +instance : FromJson BlockEntry where + fromJson? json := do + pure { + blockHeader := ← json.getObjValAs? BlockHeader "blockHeader" + rlp := ← json.getObjValAs? Json "rlp" + transactions := ← json.getObjValAs? Transactions "transactions" + uncleHeaders := ← json.getObjValAs? Json "uncleHeaders" + withdrawals := ← json.getObjValAs? Json "withdrawals" + } + +deriving instance FromJson for TestEntry + +instance : FromJson Test where + fromJson? json := json.getObjVals? String TestEntry + +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 Pre := ⟨ToString.toString ∘ repr⟩ + +instance : ToString PostEntry := ⟨ToString.toString ∘ repr⟩ + +instance : ToString Post := ⟨ToString.toString ∘ repr⟩ + +instance : ToString Transaction := ⟨λ _ ↦ "Some transaction."⟩ + +end PrettyPrinter + +end Parser + +end Conform + +end EvmYul diff --git a/Conform/TestRunner.lean b/Conform/TestRunner.lean new file mode 100644 index 0000000..71ccfac --- /dev/null +++ b/Conform/TestRunner.lean @@ -0,0 +1,88 @@ +import EvmYul.EVM.State +import EvmYul.EVM.Semantics +import EvmYul.Wheels + +import Conform.Exception +import Conform.Model +import Conform.TestParser + +namespace EvmYul + +namespace Conform + +def Pre.toEVMState (self : Pre) : EVM.State := + self.fold addAccount default + where addAccount s addr acc := + let account : Account := + { + nonce := acc.nonce + balance := acc.balance + code := acc.code + codeHash := 0 -- TODO - We can of course compute this but we probably do not need this. + storage := acc.storage.toFinmap + } + { s with toState := s.setAccount addr account } + +def Test.toTests (self : Test) : List (String × TestEntry) := self.toList + +def Post.toEVMState : Post → EVM.State := Pre.toEVMState + +def run : EVM.Transformer := EVM.step 5000 -- TODO - Replace with Xi or some such. + +local instance : Inhabited EVM.Transformer where + default := λ _ ↦ default + +partial def runUntilStop : EVM.Transformer := λ s ↦ + match EvmYul.Conform.run s with + | .error (.StopInvoked s) => pure s + | .error e => .error e + | .ok s => runUntilStop s + +private def compareWithEVMdefaults (s₁ s₂ : EvmYul.Storage) : Bool := + withDefault s₁ == withDefault s₂ + where + withDefault (s : EvmYul.Storage) : EvmYul.Storage := if 0 ∈ s then s else s.insert 0 0 + +private def somewhatShoddyAccEq (acc₁ acc₂ : Account) : Bool := acc₁ == acc₂ + +/-- +TODO - Of course fix this later on. Potentially in some `Except Err` monad to report +precisely on why this failed. +-/ +private def somewhatShoddyStateEq (s₁ s₂ : EVM.State) : Bool := + s₁.accountMap == s₂.accountMap + +/-- +TODO - This MUST use the transaction to initialise the `ExecutionEnv` of the `s`... somehow :). + +This is marked `deprecated` to emit an error to make it clear that the implementation is placeholder. +-/ +@[deprecated] +def executeTransaction (transaction : Transaction) (s : EVM.State) : Except EVM.Exception EVM.State := + runUntilStop s + +/-- +This assumes that the `transactions` are ordered. +-/ +def preImpliesPost (pre : Pre) (post : Post) (transactions : Transactions) : Except EVM.Exception Bool := + somewhatShoddyStateEq post.toEVMState <$> + transactions.foldlM (flip executeTransaction) pre.toEVMState + +local instance : MonadLift (Except EVM.Exception) (Except Conform.Exception) := ⟨Except.mapError .EVMError⟩ + +def processTest (entry : TestEntry) : Except Exception TestResult := do + -- From the tests eyeballed, there is a single block in 'blocks', so currently we assume this. + let transactions := entry.blocks[0]!.transactions + pure <| TestResult.ofBool (← preImpliesPost entry.pre entry.postState transactions) + +local instance : MonadLift (Except String) (Except Conform.Exception) := ⟨Except.mapError .CannotParse⟩ + +def processTestsOfFile (file : System.FilePath) : ExceptT Exception IO (Lean.RBMap String TestResult compare) := do + let file ← Lean.Json.fromFile file + let test ← Lean.FromJson.fromJson? (α := Test) file + test.toTests.foldlM (init := ∅) λ acc (testname, test) ↦ + processTest test >>= pure ∘ acc.insert testname + +end Conform + +end EvmYul diff --git a/Conform/Wheels.lean b/Conform/Wheels.lean new file mode 100644 index 0000000..c5ea297 --- /dev/null +++ b/Conform/Wheels.lean @@ -0,0 +1,128 @@ +import Lean.Data.Json +import EvmYul.UInt256 +import EvmYul.Wheels + +import Mathlib.Data.Multiset.Sort + +namespace Lean.Json + +def getObjValAs! + (self : Json) (α : Type) (key : String) [Inhabited α] [FromJson α] : α := + match self.getObjValAs? α key with + | .error _ => panic! s!"Expected the key {key} in the map." + | .ok pre => pre + +/-- +Turn non-existance of the key into default initialisation. + +This silences ONLY the `property not found:` error. +If the parsing of an existing value fails, we propagate the error. +-/ +def getObjValAsOrInitWith? (j : Json) (α : Type) [FromJson α] (k : String) (default : α) : Except String α := + match j.getObjVal? k with + | .error _ => pure default + | .ok val => fromJson? val + +/-- +`getObjValAsOrInit = getObjValAsOrInitWith default` for inhabited types. +-/ +def getObjValAsOrInit? (j : Json) (α : Type) [FromJson α] [Inhabited α] (k : String) : Except String α := + getObjValAsOrInitWith? j α k default + +open Batteries (RBMap) in +def getObjVals? + (self : Json) (α β : Type) [Ord α] [FromJson α] [FromJson β] : Except String (RBMap α β compare) := do + let keys ← Array.map Sigma.fst <$> RBNode.toArray <$> self.getObj? + let mut result : RBMap α β compare := ∅ + for k in keys do + if let .ok key := FromJson.fromJson? k then + result := result.insert key (← self.getObjValAs? β k) + pure result + +def fromFile (path : System.FilePath) : IO Json := do + let .ok json ← Json.parse <$> IO.FS.readFile path | panic! s!"Failed to parse Json at: {path}" + pure json + +end Lean.Json + +namespace EvmYul + +namespace Conform + +def TargetSchedule := "Cancun" + +def isHexDigitChar (c : Char) : Bool := + '0' <= c && c <= '9' || 'a' <= c.toLower && c.toLower <= 'f' + +def Blob := String + +instance : Inhabited Blob := inferInstanceAs (Inhabited String) + +def Blob.toString : Blob → String := λ blob ↦ blob + +instance : ToString Blob := ⟨Blob.toString⟩ + +def getBlob? (s : String) : Except String Blob := + if isHex s then + let rest := s.drop Hex.length + if rest.any (not ∘ isHexDigitChar) + then .error "Blobs must consist of valid hex digits." + else .ok rest.toLower + else .error "Input does not begin with 0x." + where + Hex := "0x" + isHex (s : String) := s.startsWith Hex + +def getBlob! (s : String) : Blob := getBlob? s |>.toOption.get! + +def toHex (c : Char) : Except String Nat := + if '0' ≤ c ∧ c ≤ '9' + then .ok <| c.toString.toNat! + else if 'a' ≤ c.toLower ∧ c.toLower ≤ 'f' + then let Δ := c.toLower.toNat - 'a'.toNat + .ok <| 10 + Δ + else .error s!"Not a hex digit: {c}" + +end Conform + + +section WithConform + +open Conform + +namespace UInt256 + +def fromBlob? (blob : Blob) : Except String UInt256 := + Fin.ofNat <$> ((·.1) <| blob.foldr (init := (.ok 0, 0)) λ digit (acc, exp) ↦ + (do pure <| (←acc) + (16 ^ exp) * (←toHex digit), exp + 1)) + +def fromBlob! (blob : Blob) : UInt256 := fromBlob? blob |>.toOption.get! + +end UInt256 + +namespace Address + +def fromBlob? (s : Blob) : Except String Address := (Fin.ofNat ·.toNat) <$> UInt256.fromBlob? s + +def fromBlob! (blob : Blob) : Address := fromBlob? blob |>.toOption.get! + +end Address + +end WithConform + +end EvmYul + +open EvmYul.Conform (toHex) in +def UInt8.ofHex? : List Char → Except String UInt8 + | [] => pure 0 + | [msb, lsb] => do pure ∘ UInt8.ofNat <| (← toHex msb) * 16 + (← toHex lsb) + | _ => throw "Need two hex digits for every byte." + +def ByteArray.ofBlob (self : EvmYul.Conform.Blob) : Except String ByteArray := do + let chunks ← self.toList.toChunks 2 |>.mapM UInt8.ofHex? + pure ⟨chunks.toArray⟩ + +def computeToList! {α} + [LE α] [IsTrans α (· ≤ ·)] [IsAntisymm α (· ≤ ·)] [IsTotal α (· ≤ ·)] + [DecidableRel (α := α) (· ≤ ·)] (m : Multiset α) : List α := + m.sort (· ≤ ·) diff --git a/EthereumTests b/EthereumTests new file mode 160000 index 0000000..08839f5 --- /dev/null +++ b/EthereumTests @@ -0,0 +1 @@ +Subproject commit 08839f54ebdeb808ff4171a7ddb8803dfa8963a8 diff --git a/EvmYul.lean b/EvmYul.lean new file mode 100644 index 0000000..694aaa6 --- /dev/null +++ b/EvmYul.lean @@ -0,0 +1,42 @@ +import EvmYul.MachineState +import EvmYul.MachineStateOps +import EvmYul.Operations +import EvmYul.Semantics +import EvmYul.SharedState +import EvmYul.SharedStateOps +import EvmYul.State +import EvmYul.StateOps +import EvmYul.UInt256 +import EvmYul.Wheels + +import EvmYul.Data.Stack + +import EvmYul.EVM.Exception +import EvmYul.EVM.Instr +import EvmYul.EVM.PrimOps +import EvmYul.EVM.Semantics +import EvmYul.EVM.State +import EvmYul.EVM.StateOps + +import EvmYul.State.Account +import EvmYul.State.AccountOps +import EvmYul.State.Block +import EvmYul.State.BlockHeader +import EvmYul.State.ExecutionEnv +import EvmYul.State.Substate +import EvmYul.State.SubstateOps +import EvmYul.State.Transaction + +import EvmYul.Yul.Ast +import EvmYul.Yul.Exception +import EvmYul.Yul.Interpreter +import EvmYul.Yul.MachineState +import EvmYul.Yul.PrimOps +import EvmYul.Yul.SizeLemmas +import EvmYul.Yul.State +import EvmYul.Yul.StateOps +import EvmYul.Yul.Wheels +import EvmYul.Yul.YulNotation + +import EvmYul.SpongeHash.Wheels +import EvmYul.SpongeHash.Keccak256 diff --git a/EvmYul/Data/Stack.lean b/EvmYul/Data/Stack.lean new file mode 100644 index 0000000..5119c13 --- /dev/null +++ b/EvmYul/Data/Stack.lean @@ -0,0 +1,86 @@ +namespace EvmYul + +abbrev Stack (α : Type) := List α + +namespace Stack + +variable {α : Type} + +def new : Stack α := [] + +def isEmpty (s : Stack α) := List.isEmpty s + +def size (s : Stack α) : Nat := List.length s +def push (s : Stack α) (v : α) : Stack α := v :: s + +def pop : Stack α → Option (Stack α × α) + | hd :: tl => .some (tl, hd) + | [] => .none + +def pop2 : Stack α → Option (Stack α × α × α) + | hd :: hd₁ :: tl => .some (tl, hd, hd₁) + | _ => .none + +def pop3 : Stack α → Option (Stack α × α × α × α) + | hd :: hd₁ :: hd₂ :: tl => .some (tl, hd, hd₁, hd₂) + | _ => .none + +def pop4 : Stack α → Option (Stack α × α × α × α × α) + | hd :: hd₁ :: hd₂ :: hd₃ :: tl => .some (tl, hd, hd₁, hd₂, hd₃) + | _ => .none + +def pop5 : Stack α → Option (Stack α × α × α × α × α × α) + | hd :: hd₁ :: hd₂ :: hd₃ :: hd₄ :: tl => .some (tl, hd, hd₁, hd₂, hd₃, hd₄) + | _ => .none + +def pop6 : Stack α → Option (Stack α × α × α × α × α × α × α) + | hd :: hd₁ :: hd₂ :: hd₃ :: hd₄ :: hd₅ :: tl => .some (tl, hd, hd₁, hd₂, hd₃, hd₄, hd₅) + | _ => .none + +def pop7 : Stack α → Option (Stack α × α × α × α × α × α × α × α) + | hd :: hd₁ :: hd₂ :: hd₃ :: hd₄ :: hd₅ :: hd₆ :: tl => + .some (tl, hd, hd₁, hd₂, hd₃, hd₄, hd₅, hd₆) + | _ => .none + +section StackLemmas + +variable {x : α} {s : Stack α} + +@[simp] +theorem isEmpty_push_false : (s.push x).isEmpty = false := rfl + +@[simp] +theorem isEmpty_nil : Stack.isEmpty (α := α) [] := rfl + +@[simp] +theorem isEmpty_cons_false : Stack.isEmpty (α := α) (x :: s) = false := rfl + +@[simp] +theorem size_nil : Stack.size (α := α) [] = 0 := rfl + +@[simp] +theorem size_new : Stack.new.size (α := α) = 0 := rfl + +@[simp] +theorem size_cons : Stack.size (α := α) (x :: s) = Stack.size s + 1 := rfl + +theorem size_zero_iff_isEmpty_eq_true : s.size = 0 ↔ s.isEmpty = true := by + cases s <;> simp + +@[simp] +theorem size_push : (s.push x).size = s.size + 1 := rfl + +@[simp] +theorem pop_push : (s.push x).pop = some (s, x) := rfl + +end StackLemmas + +instance {α} : Inhabited (Stack α) := ⟨Stack.new⟩ +instance {α} [DecidableEq α] : DecidableEq (Stack α) := inferInstanceAs (DecidableEq (List α)) +instance {α} : EmptyCollection (Stack α) := ⟨Stack.new⟩ + +end Stack + +instance {α : Type} [ToString α] : ToString (Stack α) := inferInstanceAs (ToString (List α)) + +end EvmYul diff --git a/EvmYul/EVM/Exception.lean b/EvmYul/EVM/Exception.lean new file mode 100644 index 0000000..0c63c17 --- /dev/null +++ b/EvmYul/EVM/Exception.lean @@ -0,0 +1,34 @@ +import EvmYul.EVM.State + +namespace EvmYul + +namespace EVM + +inductive Exception where + | InvalidStackSizeException : Exception + | InvalidPC : Exception + | OutOfBounds : Exception + | NotEncodableRLP : Exception + | InvalidInstruction : Exception + | SenderMustExist : Exception + | ReceiverMustExistWithNonZeroValue : Exception + | Underflow : Exception + | Overflow : Exception + | StopInvoked (s : EVM.State) : Exception + +instance : Repr Exception where + reprPrec s _ := match s with + | .InvalidStackSizeException => "InvalidStackSizeException" + | .InvalidPC => "InvalidPC" + | .OutOfBounds => "OutOfBounds" + | .NotEncodableRLP => "NotEncodableRLP" + | .InvalidInstruction => "InvalidInstruction" + | .SenderMustExist => "SenderMustExist" + | .ReceiverMustExistWithNonZeroValue => "ReceiverMustExistWithNonZeroValue" + | .Underflow => "Underflow" + | .Overflow => "Overflow" + | .StopInvoked _ => "Execution halted by STOP." + +end EVM + +end EvmYul diff --git a/EvmYul/EVM/Instr.lean b/EvmYul/EVM/Instr.lean new file mode 100644 index 0000000..1d4903e --- /dev/null +++ b/EvmYul/EVM/Instr.lean @@ -0,0 +1,564 @@ +import EvmYul.Operations + +namespace EvmYul + +namespace EVM + +open Operation + +def serializeStopArithInstr : SAOp .EVM → UInt8 + | .STOP => 0 + | .ADD => 1 + | .MUL => 2 + | .SUB => 3 + | .DIV => 4 + | .SDIV => 5 + | .MOD => 6 + | .SMOD => 7 + | .ADDMOD => 8 + | .MULMOD => 9 + | .EXP => 10 + | .SIGNEXTEND => 11 + +def serializeCompBitInstr : CBLOp .EVM → UInt8 + | .LT => 16 + | .GT => 17 + | .SLT => 18 + | .SGT => 19 + | .EQ => 20 + | .ISZERO => 21 + | .AND => 22 + | .OR => 23 + | .XOR => 24 + | .NOT => 25 + | .BYTE => 26 + | .SHL => 27 + | .SHR => 28 + | .SAR => 29 + +def serializeKeccakInstr : KOp .EVM → UInt8 + | .KECCAK256 => 32 + +def serializeEnvInstr : EOp .EVM → UInt8 + | .ADDRESS => 48 + | .BALANCE => 49 + | .ORIGIN => 50 + | .CALLER => 51 + | .CALLVALUE => 52 + | .CALLDATALOAD => 53 + | .CALLDATASIZE => 54 + | .CALLDATACOPY => 55 + | .CODESIZE => 56 + | .CODECOPY => 57 + | .GASPRICE => 58 + | .EXTCODESIZE => 59 + | .EXTCODECOPY => 60 + | .RETURNDATASIZE => 61 + | .RETURNDATACOPY => 62 + | .EXTCODEHASH => 63 + +def serializeBlockInstr : BOp .EVM → UInt8 + | .BLOCKHASH => 64 + | .COINBASE => 65 + | .TIMESTAMP => 66 + | .NUMBER => 67 + | .PREVRANDAO => 68 + | .DIFFICULTY => 68 + | .GASLIMIT => 69 + | .CHAINID => 70 + | .SELFBALANCE => 71 + | .BASEFEE => 72 + +def serializeStackMemFlowInstr : SMSFOp .EVM → UInt8 + | .POP => 80 + | .MLOAD => 81 + | .MSTORE => 82 + | .MSTORE8 => 83 + | .SLOAD => 84 + | .SSTORE => 85 + | .PC => 88 + | .MSIZE => 89 + | .GAS => 90 + | .JUMP => 86 + | .JUMPI => 87 + | .JUMPDEST => 91 + +def serializePushInstr : POp → UInt8 + | .PUSH0 => 95 + | .PUSH1 => 96 + | .PUSH2 => 97 + | .PUSH3 => 98 + | .PUSH4 => 99 + | .PUSH5 => 100 + | .PUSH6 => 101 + | .PUSH7 => 102 + | .PUSH8 => 103 + | .PUSH9 => 104 + | .PUSH10 => 105 + | .PUSH11 => 106 + | .PUSH12 => 107 + | .PUSH13 => 108 + | .PUSH14 => 109 + | .PUSH15 => 110 + | .PUSH16 => 111 + | .PUSH17 => 112 + | .PUSH18 => 113 + | .PUSH19 => 114 + | .PUSH20 => 115 + | .PUSH21 => 116 + | .PUSH22 => 117 + | .PUSH23 => 118 + | .PUSH24 => 119 + | .PUSH25 => 120 + | .PUSH26 => 121 + | .PUSH27 => 122 + | .PUSH28 => 123 + | .PUSH29 => 124 + | .PUSH30 => 125 + | .PUSH31 => 126 + | .PUSH32 => 127 + +def serializeDupInstr : DOp → UInt8 + | .DUP1 => 128 + | .DUP2 => 129 + | .DUP3 => 130 + | .DUP4 => 131 + | .DUP5 => 132 + | .DUP6 => 133 + | .DUP7 => 134 + | .DUP8 => 135 + | .DUP9 => 136 + | .DUP10 => 137 + | .DUP11 => 138 + | .DUP12 => 139 + | .DUP13 => 140 + | .DUP14 => 141 + | .DUP15 => 142 + | .DUP16 => 143 + +def serializeSwapInstr : ExOp → UInt8 + | .SWAP1 => 144 + | .SWAP2 => 145 + | .SWAP3 => 146 + | .SWAP4 => 147 + | .SWAP5 => 148 + | .SWAP6 => 149 + | .SWAP7 => 150 + | .SWAP8 => 151 + | .SWAP9 => 152 + | .SWAP10 => 153 + | .SWAP11 => 154 + | .SWAP12 => 155 + | .SWAP13 => 156 + | .SWAP14 => 157 + | .SWAP15 => 158 + | .SWAP16 => 159 + +def serializeLogInstr : LOp .EVM → UInt8 + | .LOG0 => 160 + | .LOG1 => 161 + | .LOG2 => 162 + | .LOG3 => 163 + | .LOG4 => 164 + +def serializeSysInstr : SOp .EVM → UInt8 + | .CREATE => 240 + | .CALL => 241 + | .CALLCODE => 242 + | .RETURN => 243 + | .DELEGATECALL => 244 + | .CREATE2 => 245 + | .STATICCALL => 250 + | .REVERT => 253 + | .INVALID => 254 + | .SELFDESTRUCT => 255 + +def serializeInstr : Operation .EVM → UInt8 + | .StopArith a => serializeStopArithInstr a + | .CompBit e => serializeCompBitInstr e + | .Keccak k => serializeKeccakInstr k + | .Env e => serializeEnvInstr e + | .Block b => serializeBlockInstr b + | .StackMemFlow m => serializeStackMemFlowInstr m + | .Push p => serializePushInstr p + | .Dup d => serializeDupInstr d + | .Exchange e => serializeSwapInstr e + | .Log l => serializeLogInstr l + | .System s => serializeSysInstr s + + def δ : Operation .EVM → Option ℕ + | .STOP => some 0 + | .ADD => some 2 + | .MUL => some 2 + | .SUB => some 2 + | .DIV => some 2 + | .SDIV => some 2 + | .MOD => some 2 + | .SMOD => some 2 + | .ADDMOD => some 3 + | .MULMOD => some 3 + | .EXP => some 2 + | .SIGNEXTEND => some 2 + | .LT => some 2 + | .GT => some 2 + | .SLT => some 2 + | .SGT => some 2 + | .EQ => some 2 + | .ISZERO => some 1 + | .AND => some 2 + | .OR => some 2 + | .XOR => some 2 + | .NOT => some 1 + | .BYTE => some 2 + | .SHL => some 2 + | .SHR => some 2 + | .SAR => some 2 + | .KECCAK256 => some 2 + | .ADDRESS => some 0 + | .BALANCE => some 1 + | .ORIGIN => some 0 + | .CALLER => some 0 + | .CALLVALUE => some 0 + | .CALLDATALOAD => some 1 + | .CALLDATASIZE => some 0 + | .CALLDATACOPY => some 3 + | .CODESIZE => some 0 + | .CODECOPY => some 3 + | .GASPRICE => some 0 + | .EXTCODESIZE => some 4 + | .EXTCODECOPY => some 4 + | .RETURNDATASIZE => some 0 + | .RETURNDATACOPY => some 3 + | .EXTCODEHASH => some 1 + | .BLOCKHASH => some 1 + | .COINBASE => some 0 + | .TIMESTAMP => some 0 + | .NUMBER => some 0 + | .PREVRANDAO => some 0 + | .DIFFICULTY => some 0 + | .GASLIMIT => some 0 + | .CHAINID => some 0 + | .SELFBALANCE => some 0 + | .BASEFEE => some 0 + | .POP => some 1 + | .MLOAD => some 2 + | .MSTORE => some 2 + | .MSTORE8 => some 1 + | .SLOAD => some 2 + | .SSTORE => some 2 + | .PC => some 0 + | .MSIZE => some 0 + | .GAS => some 0 + | .Push _ => some 0 + | .DUP1 => some 1 + | .DUP2 => some 2 + | .DUP3 => some 3 + | .DUP4 => some 4 + | .DUP5 => some 5 + | .DUP6 => some 6 + | .DUP7 => some 7 + | .DUP8 => some 8 + | .DUP9 => some 9 + | .DUP10 => some 10 + | .DUP11 => some 11 + | .DUP12 => some 12 + | .DUP13 => some 13 + | .DUP14 => some 14 + | .DUP15 => some 15 + | .DUP16 => some 16 + | .SWAP1 => some 2 + | .SWAP2 => some 3 + | .SWAP3 => some 4 + | .SWAP4 => some 5 + | .SWAP5 => some 6 + | .SWAP6 => some 7 + | .SWAP7 => some 8 + | .SWAP8 => some 9 + | .SWAP9 => some 10 + | .SWAP10 => some 11 + | .SWAP11 => some 12 + | .SWAP12 => some 13 + | .SWAP13 => some 14 + | .SWAP14 => some 15 + | .SWAP15 => some 16 + | .SWAP16 => some 17 + | .LOG0 => some 2 + | .LOG1 => some 3 + | .LOG2 => some 4 + | .LOG3 => some 5 + | .LOG4 => some 6 + | .JUMP => some 1 + | .JUMPI => some 2 + | .JUMPDEST => some 0 + | .CREATE => some 3 + | .CALL => some 7 + | .CALLCODE => some 7 + | .RETURN => some 2 + | .DELEGATECALL => some 6 + | .CREATE2 => some 6 + | .STATICCALL => some 6 + | .REVERT => some 2 + | .INVALID => none + | .SELFDESTRUCT => some 1 + + def α : Operation .EVM → Option ℕ + | .STOP => some 0 + | .ADD => some 1 + | .MUL => some 1 + | .SUB => some 1 + | .DIV => some 1 + | .SDIV => some 1 + | .MOD => some 1 + | .SMOD => some 1 + | .ADDMOD => some 1 + | .MULMOD => some 1 + | .EXP => some 1 + | .SIGNEXTEND => some 1 + | .LT => some 1 + | .GT => some 1 + | .SLT => some 1 + | .SGT => some 1 + | .EQ => some 1 + | .ISZERO => some 1 + | .AND => some 1 + | .OR => some 1 + | .XOR => some 1 + | .NOT => some 1 + | .BYTE => some 1 + | .SHL => some 1 + | .SHR => some 1 + | .SAR => some 1 + | .KECCAK256 => some 1 + | .ADDRESS => some 1 + | .BALANCE => some 1 + | .ORIGIN => some 1 + | .CALLER => some 1 + | .CALLVALUE => some 1 + | .CALLDATALOAD => some 1 + | .CALLDATASIZE => some 1 + | .CALLDATACOPY => some 0 + | .CODESIZE => some 1 + | .CODECOPY => some 0 + | .GASPRICE => some 1 + | .EXTCODESIZE => some 1 + | .EXTCODECOPY => some 0 + | .RETURNDATASIZE => some 1 + | .RETURNDATACOPY => some 0 + | .EXTCODEHASH => some 1 + | .BLOCKHASH => some 1 + | .COINBASE => some 1 + | .TIMESTAMP => some 1 + | .NUMBER => some 1 + | .PREVRANDAO => some 1 + | .DIFFICULTY => some 1 + | .GASLIMIT => some 1 + | .CHAINID => some 1 + | .SELFBALANCE => some 1 + | .BASEFEE => some 1 + | .POP => some 0 + | .MLOAD => some 1 + | .MSTORE => some 0 + | .MSTORE8 => some 0 + | .SLOAD => some 1 + | .SSTORE => some 0 + | .PC => some 1 + | .MSIZE => some 1 + | .GAS => some 1 + | .JUMP => some 0 + | .JUMPI => some 0 + | .JUMPDEST => some 0 + | .Push _ => some 1 + | .DUP1 => some 2 + | .DUP2 => some 3 + | .DUP3 => some 4 + | .DUP4 => some 5 + | .DUP5 => some 6 + | .DUP6 => some 7 + | .DUP7 => some 8 + | .DUP8 => some 9 + | .DUP9 => some 10 + | .DUP10 => some 11 + | .DUP11 => some 12 + | .DUP12 => some 13 + | .DUP13 => some 14 + | .DUP14 => some 15 + | .DUP15 => some 16 + | .DUP16 => some 16 + | .SWAP1 => some 2 + | .SWAP2 => some 3 + | .SWAP3 => some 4 + | .SWAP4 => some 5 + | .SWAP5 => some 6 + | .SWAP6 => some 7 + | .SWAP7 => some 8 + | .SWAP8 => some 9 + | .SWAP9 => some 10 + | .SWAP10 => some 11 + | .SWAP11 => some 12 + | .SWAP12 => some 13 + | .SWAP13 => some 14 + | .SWAP14 => some 15 + | .SWAP15 => some 16 + | .SWAP16 => some 17 + | .Log _ => some 0 + | .CREATE => some 1 + | .CALL => some 1 + | .CALLCODE => some 1 + | .RETURN => some 0 + | .DELEGATECALL => some 1 + | .CREATE2 => some 1 + | .STATICCALL => some 0 + | .REVERT => some 0 + | .INVALID => none + | .SELFDESTRUCT => some 0 + +def parseInstr : UInt8 → Option (Operation .EVM) + | 0 => some .STOP + | 1 => some .ADD + | 2 => some .MUL + | 3 => some .SUB + | 4 => some .DIV + | 5 => some .SDIV + | 6 => some .MOD + | 7 => some .SMOD + | 8 => some .ADDMOD + | 9 => some .MULMOD + | 10 => some .EXP + | 11 => some .SIGNEXTEND + | 16 => some .LT + | 17 => some .GT + | 18 => some .SLT + | 19 => some .SGT + | 20 => some .EQ + | 21 => some .ISZERO + | 22 => some .AND + | 23 => some .OR + | 24 => some .XOR + | 25 => some .NOT + | 26 => some .BYTE + | 27 => some .SHL + | 28 => some .SHR + | 29 => some .SAR + | 32 => some .KECCAK256 + | 48 => some .ADDRESS + | 49 => some .BALANCE + | 50 => some .ORIGIN + | 51 => some .CALLER + | 52 => some .CALLVALUE + | 53 => some .CALLDATALOAD + | 54 => some .CALLDATASIZE + | 55 => some .CALLDATACOPY + | 56 => some .CODESIZE + | 57 => some .CODECOPY + | 58 => some .GASPRICE + | 59 => some .EXTCODESIZE + | 60 => some .EXTCODECOPY + | 61 => some .RETURNDATASIZE + | 62 => some .RETURNDATACOPY + | 63 => some .EXTCODEHASH + | 64 => some .BLOCKHASH + | 65 => some .COINBASE + | 66 => some .TIMESTAMP + | 67 => some .NUMBER + | 68 => some .DIFFICULTY + | 69 => some .GASLIMIT + | 70 => some .CHAINID + | 71 => some .SELFBALANCE + | 72 => some .BASEFEE + | 80 => some .POP + | 81 => some .MLOAD + | 82 => some .MSTORE + | 83 => some .MSTORE8 + | 84 => some .SLOAD + | 85 => some .SSTORE + | 86 => some .JUMP + | 87 => some .JUMPI + | 88 => some .PC + | 89 => some .MSIZE + | 90 => some .GAS + | 91 => some .JUMPDEST + | 95 => some .PUSH0 + | 96 => some .PUSH1 + | 97 => some .PUSH2 + | 98 => some .PUSH3 + | 99 => some .PUSH4 + | 100 => some .PUSH5 + | 101 => some .PUSH6 + | 102 => some .PUSH7 + | 103 => some .PUSH8 + | 104 => some .PUSH9 + | 105 => some .PUSH10 + | 106 => some .PUSH11 + | 107 => some .PUSH12 + | 108 => some .PUSH13 + | 109 => some .PUSH14 + | 110 => some .PUSH15 + | 111 => some .PUSH16 + | 112 => some .PUSH17 + | 113 => some .PUSH18 + | 114 => some .PUSH19 + | 115 => some .PUSH20 + | 116 => some .PUSH21 + | 117 => some .PUSH22 + | 118 => some .PUSH23 + | 119 => some .PUSH24 + | 120 => some .PUSH25 + | 121 => some .PUSH26 + | 122 => some .PUSH27 + | 123 => some .PUSH28 + | 124 => some .PUSH29 + | 125 => some .PUSH30 + | 126 => some .PUSH31 + | 127 => some .PUSH32 + | 128 => some .DUP1 + | 129 => some .DUP2 + | 130 => some .DUP3 + | 131 => some .DUP4 + | 132 => some .DUP5 + | 133 => some .DUP6 + | 134 => some .DUP7 + | 135 => some .DUP8 + | 136 => some .DUP9 + | 137 => some .DUP10 + | 138 => some .DUP11 + | 139 => some .DUP12 + | 140 => some .DUP13 + | 141 => some .DUP14 + | 142 => some .DUP15 + | 143 => some .DUP16 + | 144 => some .SWAP1 + | 145 => some .SWAP2 + | 146 => some .SWAP3 + | 147 => some .SWAP4 + | 148 => some .SWAP5 + | 149 => some .SWAP6 + | 150 => some .SWAP7 + | 151 => some .SWAP8 + | 152 => some .SWAP9 + | 153 => some .SWAP10 + | 154 => some .SWAP11 + | 155 => some .SWAP12 + | 156 => some .SWAP13 + | 157 => some .SWAP14 + | 158 => some .SWAP15 + | 159 => some .SWAP16 + | 160 => some .LOG0 + | 161 => some .LOG1 + | 162 => some .LOG2 + | 163 => some .LOG3 + | 164 => some .LOG4 + | 240 => some .CREATE + | 241 => some .CALL + | 242 => some .CALLCODE + | 243 => some .RETURN + | 244 => some .DELEGATECALL + | 245 => some .CREATE2 + | 250 => some .STATICCALL + | 253 => some .REVERT + | 254 => some .INVALID + | 255 => some .SELFDESTRUCT + | _ => none + +end EVM + +end EvmYul diff --git a/EvmYul/EVM/PrimOps.lean b/EvmYul/EVM/PrimOps.lean new file mode 100644 index 0000000..1f29a36 --- /dev/null +++ b/EvmYul/EVM/PrimOps.lean @@ -0,0 +1,167 @@ +import EvmYul.Data.Stack + +import EvmYul.EVM.State +import EvmYul.EVM.Exception +import EvmYul.EVM.StateOps +import EvmYul.SharedStateOps + +namespace EvmYul + +namespace EVM + +def Transformer := EVM.State → Except EVM.Exception EVM.State + +def execUnOp (f : Primop.Unary) : Transformer := + λ s ↦ + match s.stack.pop with + | some ⟨stack, μ₀⟩ => + .ok <| s.replaceStackAndIncrPC (stack.push <| f μ₀) + | _ => + .error .InvalidStackSizeException + +def execBinOp (f : Primop.Binary) : Transformer := + λ s ↦ + match s.stack.pop2 with + | some ⟨stack, μ₀, μ₁⟩ => + .ok <| s.replaceStackAndIncrPC (stack.push <| f μ₀ μ₁) + | _ => + .error .InvalidStackSizeException + +def execTriOp (f : Primop.Ternary) : Transformer := + λ s ↦ + match s.stack.pop3 with + | some ⟨stack, μ₀, μ₁, μ₂⟩ => + .ok <| s.replaceStackAndIncrPC (stack.push <| f μ₀ μ₁ μ₂) + | _ => + .error .InvalidStackSizeException + +def execQuadOp (f : Primop.Quaternary) : Transformer := + λ s ↦ + match s.stack.pop4 with + | some ⟨ stack , μ₀ , μ₁ , μ₂, μ₃ ⟩ => + .ok <| s.replaceStackAndIncrPC (stack.push <| f μ₀ μ₁ μ₂ μ₃) + | _ => + .error .InvalidStackSizeException + +def executionEnvOp (op : ExecutionEnv → UInt256) : Transformer := + λ evmState ↦ + .ok <| + evmState.replaceStackAndIncrPC (evmState.stack.push <| op evmState.executionEnv) + +def machineStateOp (op : MachineState → UInt256) : Transformer := + λ evmState ↦ + .ok <| + evmState.replaceStackAndIncrPC (evmState.stack.push <| op evmState.toMachineState) + +def binaryMachineStateOp + (op : MachineState → UInt256 → UInt256 → MachineState) : Transformer +:= λ evmState ↦ + match evmState.stack.pop2 with + | some ⟨ s , μ₀, μ₁ ⟩ => + let mState' := op evmState.toMachineState μ₀ μ₁ + let evmState' := {evmState with toMachineState := mState'} + .ok <| evmState'.replaceStackAndIncrPC s + | _ => .error EVM.Exception.InvalidStackSizeException + +def binaryMachineStateOp' + (op : MachineState → UInt256 → UInt256 → UInt256 × MachineState) : Transformer +:= λ evmState ↦ + match evmState.stack.pop2 with + | some ⟨ s , μ₀, μ₁ ⟩ => + let (val, mState') := op evmState.toMachineState μ₀ μ₁ + let evmState' := {evmState with toMachineState := mState'} + .ok <| evmState'.replaceStackAndIncrPC (s.push val) + | _ => .error EVM.Exception.InvalidStackSizeException + +def binaryStateOp + (op : EvmYul.State → UInt256 → UInt256 → EvmYul.State) : Transformer +:= λ evmState ↦ + match evmState.stack.pop2 with + | some ⟨ s , μ₀, μ₁ ⟩ => + let state' := op evmState.toState μ₀ μ₁ + let evmState' := {evmState with toState := state'} + .ok <| evmState'.replaceStackAndIncrPC s + | _ => .error EVM.Exception.InvalidStackSizeException + +def stateOp (op : EvmYul.State → UInt256) : Transformer := + λ evmState ↦ + .ok <| + evmState.replaceStackAndIncrPC (evmState.stack.push <| op evmState.toState) + +def unaryStateOp (op : EvmYul.State → UInt256 → EvmYul.State × UInt256) : Transformer := + λ evmState ↦ + match evmState.stack.pop with + | some ⟨stack' , μ₀ ⟩ => + let (state', b) := op evmState.toState μ₀ + let evmState' := {evmState with toState := state'} + .ok <| evmState'.replaceStackAndIncrPC (stack'.push b) + | _ => .error EVM.Exception.InvalidStackSizeException + +def ternaryCopyOp (op : SharedState → UInt256 → UInt256 → UInt256 → SharedState) : + Transformer +:= λ evmState ↦ + match evmState.stack.pop3 with + | some ⟨ stack' , μ₀, μ₁, μ₂⟩ => + let sState' := op evmState.toSharedState μ₀ μ₁ μ₂ + let evmState' := { evmState with toSharedState := sState'} + .ok <| evmState'.replaceStackAndIncrPC stack' + | _ => .error EVM.Exception.InvalidStackSizeException + +def quaternaryCopyOp + (op : SharedState → UInt256 → UInt256 → UInt256 → UInt256 → SharedState) : + Transformer +:= λ evmState ↦ + match evmState.stack.pop4 with + | some ⟨ stack' , μ₀, μ₁, μ₂, μ₃⟩ => + let sState' := op evmState.toSharedState μ₀ μ₁ μ₂ μ₃ + let evmState' := { evmState with toSharedState := sState'} + .ok <| evmState'.replaceStackAndIncrPC stack' + | _ => .error EVM.Exception.InvalidStackSizeException + +private def evmLogOp (evmState : State) (μ₀ μ₁ : UInt256) (t : List UInt256) : State := + let (substate', μᵢ') := SharedState.logOp μ₀ μ₁ t evmState.toSharedState + { evmState with substate := substate', maxAddress := μᵢ' } + +def log0Op : Transformer := + λ evmState ↦ + match evmState.stack.pop2 with + | some ⟨stack', μ₀, μ₁⟩ => + let evmState' := evmLogOp evmState μ₀ μ₁ [] + .ok <| evmState'.replaceStackAndIncrPC stack' + | _ => .error EVM.Exception.InvalidStackSizeException + +def log1Op : Transformer := + λ evmState ↦ + match evmState.stack.pop3 with + | some ⟨stack', μ₀, μ₁, μ₂⟩ => + let evmState' := evmLogOp evmState μ₀ μ₁ [μ₂] + .ok <| evmState'.replaceStackAndIncrPC stack' + | _ => .error EVM.Exception.InvalidStackSizeException + +def log2Op : Transformer := + λ evmState ↦ + match evmState.stack.pop4 with + | some ⟨stack', μ₀, μ₁, μ₂, μ₃⟩ => + let evmState' := evmLogOp evmState μ₀ μ₁ [μ₂, μ₃] + .ok <| evmState'.replaceStackAndIncrPC stack' + | _ => .error EVM.Exception.InvalidStackSizeException + +def log3Op : Transformer := + λ evmState ↦ + match evmState.stack.pop5 with + | some ⟨stack', μ₀, μ₁, μ₂, μ₃, μ₄⟩ => + let evmState' := evmLogOp evmState μ₀ μ₁ [μ₂, μ₃, μ₄] + .ok <| evmState'.replaceStackAndIncrPC stack' + | _ => .error EVM.Exception.InvalidStackSizeException + +def log4Op : Transformer := + λ evmState ↦ + match evmState.stack.pop6 with + | some ⟨stack', μ₀, μ₁, μ₂, μ₃, μ₄, μ₅⟩ => + let evmState' := evmLogOp evmState μ₀ μ₁ [μ₂, μ₃, μ₄, μ₅] + .ok <| evmState'.replaceStackAndIncrPC stack' + | _ => .error EVM.Exception.InvalidStackSizeException + +end EVM + +end EvmYul diff --git a/EvmYul/EVM/Semantics.lean b/EvmYul/EVM/Semantics.lean new file mode 100644 index 0000000..44bef1a --- /dev/null +++ b/EvmYul/EVM/Semantics.lean @@ -0,0 +1,688 @@ +import Mathlib.Data.BitVec +import Mathlib.Data.Array.Defs +import Mathlib.Data.List.Defs + +import EvmYul.Data.Stack +import EvmYul.Operations +import EvmYul.UInt256 +import EvmYul.Wheels +import EvmYul.State.ExecutionEnv +import EvmYul.EVM.State +import EvmYul.EVM.StateOps +import EvmYul.SharedStateOps +import EvmYul.EVM.Exception +import EvmYul.EVM.Instr +import EvmYul.Semantics +import EvmYul.Wheels + +namespace EvmYul + +namespace EVM + +def argOnNBytesOfInstr : Operation .EVM → ℕ + -- | .Push .PUSH0 => 0 is handled as default. + | .Push .PUSH1 => 1 + | .Push .PUSH2 => 2 + | .Push .PUSH3 => 3 + | .Push .PUSH4 => 4 + | .Push .PUSH5 => 5 + | .Push .PUSH6 => 6 + | .Push .PUSH7 => 7 + | .Push .PUSH8 => 8 + | .Push .PUSH9 => 9 + | .Push .PUSH10 => 10 + | .Push .PUSH11 => 11 + | .Push .PUSH12 => 12 + | .Push .PUSH13 => 13 + | .Push .PUSH14 => 14 + | .Push .PUSH15 => 15 + | .Push .PUSH16 => 16 + | .Push .PUSH17 => 17 + | .Push .PUSH18 => 18 + | .Push .PUSH19 => 19 + | .Push .PUSH20 => 20 + | .Push .PUSH21 => 21 + | .Push .PUSH22 => 22 + | .Push .PUSH23 => 23 + | .Push .PUSH24 => 24 + | .Push .PUSH25 => 25 + | .Push .PUSH26 => 26 + | .Push .PUSH27 => 27 + | .Push .PUSH28 => 28 + | .Push .PUSH29 => 29 + | .Push .PUSH30 => 30 + | .Push .PUSH31 => 31 + | .Push .PUSH32 => 32 + | _ => 0 + +def N (pc : Nat) (instr : Operation .EVM) := pc.succ + argOnNBytesOfInstr instr + +/-- +Returns the instruction from `arr` at `pc` assuming it is valid. + +The `Push` instruction also returns the argument as an EVM word along with the width of the instruction. +-/ +def decode (arr : ByteArray) (pc : Nat) : + Option (Operation .EVM × Option (UInt256 × Nat)) := do + let instr ← arr.get? pc >>= EvmYul.EVM.parseInstr + let argWidth := argOnNBytesOfInstr instr + .some ( + instr, + if argWidth == 0 + then .none + else .some (EvmYul.uInt256OfByteArray (arr.extract pc.succ (pc.succ + argWidth)), argWidth) + ) + +def fetchInstr (I : EvmYul.ExecutionEnv) (pc : UInt256) : + Except EVM.Exception (Operation .EVM × Option (UInt256 × Nat)) := + decode I.code pc |>.option (.error .InvalidStackSizeException) Except.ok + +private def BitVec.ofFn {k} (x : Fin k → Bool) : BitVec k := + BitVec.ofNat k (natOfBools (Vector.ofFn x)) + where natOfBools (vec : Vector Bool k) : Nat := + (·.1) <| vec.toList.foldl (init := (0, 0)) λ (res, i) bit ↦ (res + 2^i * bit.toNat, i + 1) + +def byteAt (μ₀ μ₁ : UInt256) : UInt256 := + let v₁ : BitVec 256 := BitVec.ofNat 256 μ₁.1 + let vᵣ : BitVec 256 := BitVec.ofFn (λ i => if i >= 248 && μ₀ < 32 + then v₁.getLsb i + else false) + EvmYul.UInt256.ofNat (BitVec.toNat vᵣ) + +def dup (n : ℕ) : Transformer := + λ s ↦ + let top := s.stack.take n + if top.length = n then + .ok <| s.replaceStackAndIncrPC (top.getLast! :: s.stack) + else + .error EVM.Exception.InvalidStackSizeException + +#check List.getLast + +def swap (n : ℕ) : Transformer := + λ s ↦ + let top := s.stack.take (n + 1) + let bottom := s.stack.drop (n + 1) + if List.length top = (n + 1) then + .ok <| s.replaceStackAndIncrPC (top.getLast! :: top.tail!.dropLast ++ [top.head!] ++ bottom) + else + .error EVM.Exception.InvalidStackSizeException + +-- def callDataLoad (μ₀ : UInt256)(Id : ByteArray) : UInt256 := +-- open Array in +-- let vs : Array UInt256 := (Array.range 32).map (λ v => EvmYul.UInt256.ofNat v + μ₀) +-- sorry + +-- def keccak256 : EVM.State → Except EVM.Exception EVM.State := sorry + +local instance : MonadLift Option (Except EVM.Exception) := + ⟨Option.option (.error .InvalidStackSizeException) .ok⟩ + +mutual + +def step (fuel : ℕ) : EVM.Transformer := + match fuel with + | 0 => .ok + | .succ f => + λ (evmState : EVM.State) ↦ do + let (instr, arg) ← fetchInstr evmState.toState.executionEnv evmState.pc + -- @Andrei: Of course not all can be shared, so based on `instr` this might not be `EvmYul.step`. + match instr with + | .Push _ => do + let some (arg, argWidth) := arg | .error EVM.Exception.InvalidStackSizeException + .ok <| evmState.replaceStackAndIncrPC (evmState.stack.push arg) (pcΔ := argWidth) + | .JUMP => + match evmState.stack.pop with + | some ⟨stack , μ₀⟩ => + let newPc := μ₀ + match fetchInstr evmState.toState.executionEnv newPc with + | .ok (.JUMPDEST, _) => + let evmState' := {evmState with pc := newPc} + .ok <| evmState'.replaceStackAndIncrPC stack + | _ => .error EVM.Exception.InvalidPC + | _ => .error EVM.Exception.InvalidStackSizeException + | .JUMPI => + match evmState.stack.pop2 with + | some ⟨stack , μ₀, μ₁⟩ => + let newPc := if μ₁ = 0 then evmState.pc + 1 else μ₀ + match fetchInstr evmState.toState.executionEnv newPc with + | .ok (.JUMPDEST, _) => + let evmState' := {evmState with pc := newPc} + .ok <| evmState'.replaceStackAndIncrPC stack + | _ => .error EVM.Exception.InvalidPC + | _ => .error EVM.Exception.InvalidStackSizeException + | .PC => + .ok <| evmState.replaceStackAndIncrPC (evmState.stack.push evmState.pc) + | .JUMPDEST => .ok evmState + + | .DUP1 => dup 1 evmState + | .DUP2 => dup 2 evmState + | .DUP3 => dup 3 evmState + | .DUP4 => dup 4 evmState + | .DUP5 => dup 5 evmState + | .DUP6 => dup 6 evmState + | .DUP7 => dup 7 evmState + | .DUP8 => dup 8 evmState + | .DUP9 => dup 9 evmState + | .DUP10 => dup 10 evmState + | .DUP11 => dup 11 evmState + | .DUP12 => dup 12 evmState + | .DUP13 => dup 13 evmState + | .DUP14 => dup 14 evmState + | .DUP15 => dup 15 evmState + | .DUP16 => dup 16 evmState + + | .SWAP1 => swap 1 evmState + | .SWAP2 => swap 2 evmState + | .SWAP3 => swap 3 evmState + | .SWAP4 => swap 4 evmState + | .SWAP5 => swap 5 evmState + | .SWAP6 => swap 6 evmState + | .SWAP7 => swap 7 evmState + | .SWAP8 => swap 8 evmState + | .SWAP9 => swap 9 evmState + | .SWAP10 => swap 10 evmState + | .SWAP11 => swap 11 evmState + | .SWAP12 => swap 12 evmState + | .SWAP13 => swap 13 evmState + | .SWAP14 => swap 14 evmState + | .SWAP15 => swap 15 evmState + | .SWAP16 => swap 16 evmState + + | .CREATE => + match evmState.stack.pop3 with + | some ⟨stack, μ₀, μ₁, μ₂⟩ => do + let i : ByteArray := evmState.toMachineState.lookupMemoryRange μ₁ μ₂ + let ζ := none + let I := evmState.executionEnv + let Iₐ := evmState.executionEnv.codeOwner + let Iₒ := evmState.executionEnv.sender + let Iₑ := evmState.executionEnv.depth + let Λ := Lambda f evmState.accountMap evmState.toState.substate Iₐ Iₒ I.gasPrice μ₀ i (Iₑ + 1) ζ I.header + let (a, evmState', z, o) : (Address × EVM.State × Bool × ByteArray) := + if μ₀ ≤ (evmState.accountMap.lookup Iₐ |>.option 0 Account.balance) ∧ Iₑ < 1024 then + match Λ with + | some (a, σ', A', z, o) => + (a, {evmState with accountMap := σ', substate := A'}, z, o) + | none => (0, evmState, False, .empty) + else + (0, evmState, False, .empty) + let x := + let balance := evmState.accountMap.lookup a |>.option 0 Account.balance + if z = false ∨ Iₑ = 1024 ∨ μ₀ < balance then 0 else a + let newReturnData : ByteArray := if z = false then .empty else o + let μᵢ' := MachineState.M evmState.maxAddress μ₁ μ₂ + let evmState' := + {evmState' with + toMachineState := + {evmState.toMachineState with + returnData := newReturnData + maxAddress := μᵢ' + } + } + .ok <| evmState'.replaceStackAndIncrPC (evmState.stack.push x) + | _ => + .error .InvalidStackSizeException + | .CREATE2 => + -- Exactly equivalent to CREATE except ζ ≡ μₛ[3] + match evmState.stack.pop4 with + | some ⟨stack, μ₀, μ₁, μ₂, μ₃⟩ => do + let i : ByteArray := evmState.toMachineState.lookupMemoryRange μ₁ μ₂ + let ζ := some ⟨⟨toBytesBigEndian μ₃.val⟩⟩ + let I := evmState.executionEnv + let Iₐ := evmState.executionEnv.codeOwner + let Iₒ := evmState.executionEnv.sender + let Iₑ := evmState.executionEnv.depth + let Λ := Lambda f evmState.accountMap evmState.toState.substate Iₐ Iₒ I.gasPrice μ₀ i (Iₑ + 1) ζ I.header + let (a, evmState', z, o) : (Address × EVM.State × Bool × ByteArray) := + if μ₀ ≤ (evmState.accountMap.lookup Iₐ |>.option 0 Account.balance) ∧ Iₑ < 1024 then + match Λ with + | some (a, σ', A', z, o) => + (a, {evmState with accountMap := σ', substate := A'}, z, o) + | none => (0, evmState, False, .empty) + else + (0, evmState, False, .empty) + let x := + let balance := evmState.accountMap.lookup a |>.option 0 Account.balance + if z = false ∨ Iₑ = 1024 ∨ μ₀ < balance then 0 else a + let newReturnData : ByteArray := if z = false then .empty else o + let μᵢ' := MachineState.M evmState.maxAddress μ₁ μ₂ + let evmState' := + {evmState' with + toMachineState := + {evmState.toMachineState with + returnData := newReturnData + maxAddress := μᵢ' + } + } + .ok <| evmState'.replaceStackAndIncrPC (evmState.stack.push x) + | _ => + .error .InvalidStackSizeException + | .CALL => do + -- Names are from the YP, these are: + -- μ₀ - gas + -- μ₁ - to + -- μ₂ - value + -- μ₃ - inOffset + -- μ₄ - inSize + -- μ₅ - outOffsize + -- μ₆ - outSize + let (stack, μ₀, μ₁, μ₂, μ₃, μ₄, μ₅, μ₆) ← evmState.stack.pop7 + let (σ', g', A', z, o) ← do + -- TODO - Refactor condition and possibly share with CREATE + if μ₂ ≤ (evmState.accountMap.lookup evmState.executionEnv.codeOwner |>.option 0 Account.balance) ∧ evmState.executionEnv.depth < 1024 then + let t : Address := Address.ofUInt256 μ₁ -- t ≡ μs[1] mod 2^160 + let A' := evmState.addAccessedAccount t |>.substate -- A' ≡ A except A'ₐ ≡ Aₐ ∪ {t} + let tDirect := evmState.accountMap.lookup t |>.get!.code -- We use the code directly without an indirection a'la `codeMap[t]`. + let i := evmState.toMachineState.lookupMemoryRange μ₃ μ₄ -- m[μs[3] . . . (μs[3] + μs[4] − 1)] + Θ (σ := evmState) -- σ in Θ(σ, ..) + (A := A') -- A* in Θ(.., A*, ..) + (s := evmState.executionEnv.codeOwner) -- Iₐ in Θ(.., Iₐ, ..) + (o := evmState.executionEnv.sender) -- Iₒ in Θ(.., Iₒ, ..) + (r := t) -- t in Θ(.., t, ..) + (c := tDirect) -- t in Θ(.., t, ..) except 'dereferenced' + (g := μ₀) -- TODO gas - CCALLGAS(σ, μ, A) + (p := evmState.executionEnv.gasPrice) -- Iₚ in Θ(.., Iₚ, ..) + (v := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) + (v' := μ₂) -- μₛ[2] in Θ(.., μₛ[2], ..) + (d := i) -- i in Θ(.., i, ..) + (e := evmState.executionEnv.depth + 1) -- Iₑ + 1 in Θ(.., Iₑ + 1, ..) + (w := evmState.executionEnv.perm) -- I_W in Θ(.., I_W) + -- TODO gas - CCALLGAS(σ, μ, A) + else .ok (evmState, μ₀, evmState.toState.substate, false, ByteArray.empty) + let n : UInt256 := min μ₆ o.size -- n ≡ min({μs[6], ‖o‖}) -- TODO - Why is this using... set??? { } brackets ??? + -- TODO I am assuming here that μ' is μ with the updates mentioned in the CALL section. Check. + + -- TODO - Note to self. Check how updateMemory/copyMemory is implemented. By a cursory look, we play loose with UInt8 -> UInt256 (c.f. e.g. `calldatacopy`) and then the interplay with the WordSize parameter. + let μ'ₘ := List.range (n - 1) |>.foldl (init := evmState.toMachineState) + λ μ addr ↦ μ.copyMemory o μ₅ μ₆ -- μ′_m[μs[5] ... (μs[5] + n − 1)] = o[0 ... (n − 1)] + + let μ'ₒ := o -- μ′o = o + let μ'_g := g' -- TODO gas - μ′g ≡ μg − CCALLGAS(σ, μ, A) + g + + let codeExecutionFailed : Bool := z -- TODO - This is likely wrong. + let notEnoughFunds : Bool := μ₂ > (evmState.accountMap.lookup evmState.executionEnv.codeOwner |>.elim 0 Account.balance) -- TODO - Unify condition with CREATE. + let callDepthLimitReached : Bool := evmState.executionEnv.depth == 1024 + let x : UInt256 := if codeExecutionFailed || notEnoughFunds || callDepthLimitReached then 0 else 1 -- where x = 0 if the code execution for this operation failed, or if μs[2] > σ[Ia]b (not enough funds) or Ie = 1024 (call depth limit reached); x = 1 otherwise. + + let μ'ₛ := stack.push x -- μ′s[0] ≡ x + let μ'ᵢ := MachineState.M (MachineState.M evmState.maxAddress μ₃ μ₄) μ₅ μ₆ -- μ′i ≡ M (M (μi, μs[3], μs[4]), μs[5], μs[6]) + + -- NB. `MachineState` here does not contain the `Stack` nor the `PC`, thus incomplete. + let μ'incomplete : MachineState := + { μ'ₘ with + returnData := μ'ₒ + gasAvailable := μ'_g + maxAddress := μ'ᵢ } + + let σ' : EVM.State := { + σ' with toMachineState := μ'incomplete + }.replaceStackAndIncrPC μ'ₛ + + .ok σ' + | instr => EvmYul.step instr evmState + +def multistep (fuel : ℕ) (evmState : State) : Except EVM.Exception (State × ByteArray) := do + match fuel with + | 0 => .ok (evmState, .empty) + | .succ f => + let (instr, _) ← fetchInstr evmState.toState.executionEnv evmState.pc + let evmState' ← step f evmState + match instr with + | .RETURN | .REVERT => .ok <| (evmState', evmState'.returnData) + | .STOP | .SELFDESTRUCT => .ok (evmState', .empty) + | _ => multistep f evmState' + +def Lambda + (fuel : ℕ) + (σ : Finmap (λ _ : Address ↦ Account)) + (A : Substate) + (s : Address) -- sender + (o : Address) -- original transactor + (p : UInt256) -- gas price + (v : UInt256) -- endowment + (i : ByteArray) -- the initialisation EVM code + (e : UInt256) -- depth of the message-call/contract-creation stack + (ζ : Option ByteArray) -- the salt + (H : BlockHeader) + : + Option (Address × Finmap (λ _ : Address ↦ Account) × Substate × Bool × ByteArray) +:= + match fuel with + | 0 => .none + | .succ f => do + let n : UInt256 := (σ.lookup s |>.option 0 Account.nonce) - 1 + let lₐ ← L_A s n ζ i + let a : Address := + (KEC lₐ).extract 96 265 |>.data.toList.reverse |> fromBytes' |> Fin.ofNat + -- A* + let AStar := A.addAccessedAccount a + -- σ* + let v' := + match σ.lookup a with + | none => 0 + | some ac => ac.balance + + let newAccount : Account := + ⟨1, v + v', .empty, fromBytes' (KEC default).data.data, default⟩ + + let σStar := + match σ.lookup s with + | none => σ + | some ac => + σ.insert s {ac with balance := ac.balance - v} + |>.insert a newAccount + -- I + let exEnv : ExecutionEnv := + { codeOwner := a + , sender := o + , source := s + , weiValue := v + , inputData := default + , code := i + , gasPrice := p + , header := H + , depth := e + 1 + , perm := sorry -- TODO(Andrei) + } + let defState : EVM.State := default + let freshEvmState : EVM.State := + { defState with + accountMap := σStar + executionEnv := exEnv + substate := AStar + } + match multistep f freshEvmState with + | .error _ => .none + | .ok (evmState', returnedData) => + let F₀ : Bool := + match σ.lookup a with + | .some ac => ac.code ≠ .empty ∨ ac.nonce ≠ 0 + | .none => false + let σStarStar := evmState'.accountMap + let F : Bool := + F₀ ∨ σStarStar ≠ ∅ ∨ returnedData.size > 24576 + ∨ returnedData = ByteArray.mk ⟨0xef :: returnedData.data.toList.tail⟩ + let fail := F ∨ σStarStar = ∅ + let σ' := + if fail then σ + else if evmState'.dead a then (σStarStar.extract a).2 + else σStarStar.insert a {newAccount with code := returnedData} + let A' := if fail then AStar else evmState'.substate + let z := not fail + .some (a, σ', A', z, returnedData) + where + L_A (s : Address) (n : UInt256) (ζ : Option ByteArray) (i : ByteArray) : + Option ByteArray + := + let s := (toBytesBigEndian s).toByteArray + let n := (toBytesBigEndian n).toByteArray + match ζ with + | none => + match RLP <| .𝕃 [.𝔹 s, .𝔹 n] with + | none => .none + | some L_A => .some L_A + | some ζ => + .some <| (toBytesBigEndian 255).toByteArray ++ s ++ ζ ++ KEC i + +/-- +This invokes precompiled contracts based on the hash of the code. +Of course, we store the code directly. + +TODO - Link to precompiles, investigate the return value. +Should this return the sender somehow ::thinking::? +-/ +def Ξ (σ₁ : EVM.State) (g : UInt256) (A : Substate) (I : ExecutionEnv) : + EVM.State × UInt256 × Substate × ByteArray := sorry -- TODO - Wiat for this to exist. + +/-- +`σ` - evm state +`A` - accrued substate +`s` - sender +`o` - transaction originator +`r` - recipient +`c` - the account whose code is to be called, usually the same as `r` +`g` - available gas +`p` - effective gas price +`v` - value +`v'` - value in the execution context +`d` - input data of the call +`e` - depth of the message-call / contract-creation stack +`w` - permissions to make modifications to the stack + +TODO check - UInt256 vs Nat for some of the arguments. +-/ +def Θ (σ : EVM.State) + (A : Substate) + (s : Address) + (o : Address) + (r : Address) + (c : ByteArray) + (g : UInt256) + (p : UInt256) + (v : UInt256) + (v' : UInt256) + (d : ByteArray) + (e : Nat) + (w : Bool) : Except EVM.Exception (EVM.State × UInt256 × Substate × Bool × ByteArray) := do + -- Equation (117) + let σ₁sender ← + if !σ.accountExists s && v == 0 + then throw .SenderMustExist -- TODO - YP explains the semantics of undefined receiver; what about sender? Cf. between (115) and (116). + else σ.accountMap.lookup s |>.get!.subBalance v |>.elim (.error .Underflow) .ok -- Equation (118) TODO - What do we do on underflow? + + -- Equation (120) + let σ₁receiver ← + if !σ.accountExists s && v != 0 + then default else + if !σ.accountExists s && v == 0 + then throw .ReceiverMustExistWithNonZeroValue else -- TODO - It seems that we must only initialise the account if v != 0. Otherwise the same question as with the non-existant sender. + σ.accountMap.lookup r |>.get!.addBalance v |>.elim (.error .Overflow) .ok -- Equation (121) TODO - What do we do on overflow? + + -- (117) and (120) is `let σ₁ ← σ.transferBalance s r v` with some account updates. + let σ₁ := σ.updateAccount s σ₁sender |>.updateAccount r σ₁receiver + + -- Equation (126) + -- Note that the `c` used here is the actual code, not the address. TODO - Handle precompiled contracts. + let (σ'', g'', A'', out) := Ξ σ₁ g A σ.toState.executionEnv + + -- Equation (122) + let σ' := if σ''.isEmpty then σ else σ'' + + -- Equation (123) + let g' := if σ''.isEmpty && out.isEmpty then 0 else g'' + + -- Equation (124) + let A' := if σ''.isEmpty then A else A'' + + -- Equation (125) + let z := if σ''.isEmpty then false else true + + let I : ExecutionEnv := + { + codeOwner := r -- Equation (127) + sender := o -- Equation (128) + source := s -- Equation (131) + weiValue := v' -- Equation (132) + inputData := d -- Equation (130) + code := c -- Note that we don't use an address, but the actual code. Equation (136)-ish. + gasPrice := p -- Equation (129) + header := default -- TODO - ? + depth := e -- Equation (133) + perm := w -- Equation (134) + } + + -- TODO - Not sure if I should be set here, or somehow pre-set for Xi. + .ok ({ σ' with toState.executionEnv := I }, g', A', z, out) + +end +-- open EvmYul.UInt256 +-- def step : EvmYul.EVM.State → Except EVM.Exception EvmYul.EVM.State +-- | evmState@⟨sState@⟨state, mState⟩, pc, stack⟩ => do +-- match fetchInstr sState.toState.executionEnv pc with +-- | .error ex => .error ex +-- | .ok (i, pushArg?) => +-- match i with +-- | .StopArith .STOP => .ok evmState +-- | .StopArith .ADD => execBinOp UInt256.add evmState +-- | .StopArith .MUL => execBinOp UInt256.mul evmState +-- | .StopArith .SUB => execBinOp UInt256.sub evmState +-- | .StopArith .DIV => execBinOp UInt256.div evmState +-- | .StopArith .SDIV => execBinOp UInt256.sdiv evmState +-- | .StopArith .MOD => execBinOp UInt256.mod evmState +-- | .StopArith .SMOD => execBinOp UInt256.smod evmState +-- | .StopArith .ADDMOD => execTriOp addMod evmState +-- | .StopArith .MULMOD => execTriOp mulMod evmState +-- | .StopArith .EXP => execBinOp exp evmState +-- | .CompBit .LT => execBinOp lt evmState +-- | .CompBit .GT => execBinOp gt evmState +-- | .CompBit .SLT => execBinOp slt evmState +-- | .CompBit .SGT => execBinOp sgt evmState +-- | .CompBit .EQ => execBinOp eq evmState +-- | .CompBit .ISZERO => execUnOp isZero evmState +-- | .CompBit .AND => execBinOp UInt256.land evmState +-- | .CompBit .OR => execBinOp UInt256.lor evmState +-- | .CompBit .XOR => execBinOp UInt256.xor evmState +-- | .CompBit .NOT => execUnOp UInt256.lnot evmState +-- | .CompBit .BYTE => execBinOp UInt256.byteAt evmState +-- | .CompBit .SHL => execBinOp UInt256.shiftLeft evmState +-- | .CompBit .SHR => execBinOp UInt256.shiftRight evmState +-- | .CompBit .SAR => execBinOp UInt256.sar evmState +-- | .Keccak .KECCAK256 => sorry +-- | .StopArith .SIGNEXTEND => +-- execBinOp +-- UInt256.signextend +-- -- (λ μ₀ μ₁ => +-- -- let v₁ : BitVec 256 := BitVec.ofNat 256 μ₁.1 +-- -- let t : Fin 256 := (256 - 8 * (μ₀ - 1)).1 +-- -- let v₂ : BitVec 256 := BitVec.ofFn λ i => +-- -- if i <= t then BitVec.getLsb v₁ t else BitVec.getLsb v₁ i +-- -- UInt256.ofNat (BitVec.toNat v₂)) +-- evmState +-- | .Env .ADDRESS => .ok <| evmState.replaceStackAndIncrPC (stack.push sState.toState.executionEnv.codeOwner) +-- | .Env .BALANCE => +-- match Stack.pop stack with +-- | some ⟨ s , μ₀ ⟩ => +-- let (state', a') := EvmYul.State.balance evmState.toSharedState.toState μ₀ +-- let evmState' := {evmState with toSharedState.toState := state'} +-- -- let addr : _root_.Address := Fin.ofNat (Nat.mod μ₀.1 (2 ^ 160)) +-- -- let σ₁ : EvmYul.EVMState := EvmYul.EVMState.addAccessedAccount addr σ +-- -- match Finmap.lookup addr σ.account_map with +-- -- | some v => inr (σ₁ , pushAndIncrPC v.balance s μ) +-- -- | _ => inr (σ₁ , pushAndIncrPC 0 s μ) +-- .ok <| evmState'.replaceStackAndIncrPC (s.push a') +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Env .ORIGIN => .ok <| evmState.replaceStackAndIncrPC (stack.push sState.toState.executionEnv.sender) +-- | .Env .CALLER => .ok <| evmState.replaceStackAndIncrPC (stack.push sState.toState.executionEnv.source) +-- | .Env .CALLVALUE => .ok <| evmState.replaceStackAndIncrPC (stack.push sState.toState.executionEnv.weiValue) +-- | .Env .CALLDATALOAD => +-- match Stack.pop stack with +-- | some ⟨ _ , μ₀ ⟩ => +-- let v : UInt256 := EvmYul.State.calldataload evmState.toSharedState.toState μ₀ +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Env .CALLDATASIZE => +-- let v : UInt256 := UInt256.ofNat sState.toState.executionEnv.inputData.size +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Env .CALLDATACOPY => +-- match Stack.pop3 stack with +-- | some ⟨ s , μ₀ , μ₁ , μ₂ ⟩ => +-- -- TODO: doublecheck calldatacopy +-- let sState' := evmState.calldatacopy μ₀ μ₁ μ₂ +-- let evmState' := { evmState with toSharedState := sState'} +-- -- maxAddress handled by updateMemory +-- -- let maxAddress' := M evmState'.maxAddress μ₀ μ₂ +-- -- let evmState'' := { evmState' with maxAddress := maxAddress' } +-- .ok evmState' +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Env .CODESIZE => .ok <| evmState.replaceStackAndIncrPC (stack.push sState.toState.executionEnv.code.size) +-- | .Env .CODECOPY => +-- match Stack.pop3 stack with +-- | some ⟨ s , μ₀ , μ₁ , μ₂ ⟩ => +-- -- TODO: doublecheck codecopy +-- let sState' := sState.codeCopy μ₀ μ₁ μ₂ +-- let evmState' := { evmState with toSharedState := sState'} +-- -- maxAddress handled by updateMemory? +-- -- let maxAddress' := M evmState'.maxAddress μ₀ μ₂ +-- -- let evmState'' := { evmState' with maxAddress := maxAddress' } +-- .ok <| evmState' +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Env .GASPRICE => +-- let v : UInt256 := UInt256.ofNat sState.toState.executionEnv.gasPrice +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Env .EXTCODESIZE => +-- match Stack.pop stack with +-- | some ⟨ s , μ₀ ⟩ => +-- let addr : Address := Fin.ofNat (Nat.mod μ₀.1 (2 ^ 160)) +-- let state' : EvmYul.State := EvmYul.State.addAccessedAccount sState.toState addr +-- let evmState' := {evmState with toSharedState.toState := state'} +-- match Finmap.lookup addr evmState'.accountMap with +-- | some act => .ok <| evmState'.replaceStackAndIncrPC (stack.push act.code.size) +-- | _ => .ok <| evmState'.replaceStackAndIncrPC (stack.push 0) +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Env .EXTCODECOPY => +-- match Stack.pop4 stack with +-- | some ⟨s, μ₀, μ₁, μ₂, μ₃⟩ => +-- let addr : Address := Fin.ofNat (Nat.mod μ₀.1 (2 ^ 160)) +-- let sState' := sState.extCodeCopy addr μ₁ μ₂ μ₃ +-- let evmState' := {evmState with toSharedState := sState'} +-- -- maxAddress handled by updateMemory? +-- -- let maxAddress' := M mState.maxAddress μ₁ μ₃ +-- -- let evmState'' := {evmState' with maxAddress := maxAddress'} +-- let state' : EvmYul.State := EvmYul.State.addAccessedAccount sState.toState addr +-- let evmState'' := {evmState' with toState := state'} +-- .ok evmState'' +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Env .RETURNDATASIZE => +-- let v := mState.returndatasize +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Env .RETURNDATACOPY => +-- match Stack.pop3 stack with +-- | some ⟨ s , μ₀ , μ₁ , μ₂ ⟩ => +-- let some mState' := evmState.toMachineState.returndatacopy μ₀ μ₁ μ₂ | .error EVM.Exception.OutOfBounds +-- .ok <| {evmState with toMachineState := mState'} +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Env .EXTCODEHASH => sorry +-- | .Block .BLOCKHASH => +-- match Stack.pop stack with +-- | some ⟨ s , μ₀ ⟩ => +-- -- State.blockHash seems correct +-- let v : UInt256 := state.blockHash μ₀ +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Block .COINBASE => +-- let v : UInt256 := sState.toState.executionEnv.header.beneficiary +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Block .TIMESTAMP => +-- let v : UInt256 := UInt256.ofNat (sState.toState.executionEnv.header.timestamp) +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Block .NUMBER => +-- let v : UInt256 := UInt256.ofNat (sState.toState.executionEnv.header.number) +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Block .DIFFICULTY => +-- let v : UInt256 := UInt256.ofNat (sState.toState.executionEnv.header.difficulty) +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Block .GASLIMIT => +-- let v : UInt256 := UInt256_returnedData.ofNat (sState.toState.executionEnv.header.gasLimit) +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Block .CHAINID => +-- -- XXX The chainid β seem to be associated in transactions. +-- -- question: How transactions are denoted in the evm state? +-- let v : UInt256 := sState.toState.chainId +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Block .SELFBALANCE => +-- let v : UInt256 := sState.toState.executionEnv.codeOwner +-- .ok <| evmState.replaceStackAndIncrPC (stack.push v) +-- | .Block .BASEFEE => sorry +-- | .Log _ => sorry -- How to model substate’s log series? +-- | .StackMemFlow .POP => +-- match Stack.pop stack with +-- | some ⟨ s , _ ⟩ => .ok <| evmState.replaceStackAndIncrPC s +-- | _ => .error EVM.Exception.InvalidStackSizeException +-- | .Push _ => do let some (arg, argWidth) := pushArg? | .error EVM.Exception.InvalidStackSizeException +-- .ok <| evmState.replaceStackAndIncrPC (stack.push arg) (pcΔ := argWidth) +-- | _ => .ok evmState + +end EVM + +end EvmYul diff --git a/EvmYul/EVM/State.lean b/EvmYul/EVM/State.lean new file mode 100644 index 0000000..0a96a11 --- /dev/null +++ b/EvmYul/EVM/State.lean @@ -0,0 +1,22 @@ +import EvmYul.Data.Stack + +import EvmYul.State +import EvmYul.SharedState + +namespace EvmYul + +namespace EVM + +/-- +The EVM `State` (extends EvmYul.SharedState). +- `pc` `pc`- The program counter. +- `stack` `s` +-/ +structure State extends EvmYul.SharedState := + pc : UInt256 + stack : Stack UInt256 + deriving Inhabited, DecidableEq + +end EVM + +end EvmYul diff --git a/EvmYul/EVM/StateOps.lean b/EvmYul/EVM/StateOps.lean new file mode 100644 index 0000000..88fdd8a --- /dev/null +++ b/EvmYul/EVM/StateOps.lean @@ -0,0 +1,49 @@ +import Mathlib.Data.List.Intervals + +import EvmYul.UInt256 +import EvmYul.EVM.State +import EvmYul.State.AccountOps +import EvmYul.StateOps + +namespace EvmYul + +namespace EVM + +namespace State + +section Instructions + +def incrPC (I : EVM.State) (pcΔ : ℕ := 1) : EVM.State := + { I with pc := I.pc + pcΔ } + +def replaceStackAndIncrPC (I : EVM.State) (s : Stack UInt256) (pcΔ : ℕ := 1) : EVM.State := + incrPC { I with stack := s } pcΔ + +end Instructions + +def liftMState {m} [Monad m] (f : EvmYul.State → m EvmYul.State) : EVM.State → m EVM.State := + λ s ↦ do pure { s with toState := ← f s.toState } + +instance {m} [Monad m] : CoeFun (EvmYul.State → m EvmYul.State) (λ _ ↦ EVM.State → m EVM.State) := ⟨liftMState⟩ + +def liftState (f : EvmYul.State → EvmYul.State) : EVM.State → EVM.State := + liftMState (m := Id) f + +instance : CoeFun (EvmYul.State → EvmYul.State) (λ _ ↦ EVM.State → EVM.State) := ⟨liftState⟩ + +def transferBalance (sender : Address) (recipient : Address) (balance : UInt256) : EVM.State → Option EVM.State := + EvmYul.State.transferBalance sender recipient balance + +def initialiseAccount (addr : Address) : EVM.State → EVM.State := + EvmYul.State.initialiseAccount addr + +def updateAccount (addr : Address) (act : Account) : EVM.State → EVM.State := + EvmYul.State.updateAccount addr act + +def isEmpty (self : EVM.State) : Bool := self.toState.accountMap = ∅ + +end State + +end EVM + +end EvmYul diff --git a/EvmYul/MachineState.lean b/EvmYul/MachineState.lean new file mode 100644 index 0000000..82b7c56 --- /dev/null +++ b/EvmYul/MachineState.lean @@ -0,0 +1,35 @@ +import Mathlib.Data.Finmap + +import EvmYul.UInt256 + +namespace EvmYul + +instance : DecidableEq ByteArray + | a, b => match decEq a.data b.data with + | isTrue h₁ => isTrue <| congrArg ByteArray.mk h₁ + | isFalse h₂ => isFalse <| λ h ↦ by cases h; exact (h₂ rfl) + +/-- +The partial shared `MachineState` `μ`. Section 9.4.1. +- `gasAvailable` `g` +- `memory` `m` +- `maxAddress` `i` - # active words (modelled as the highest accessed address). +- `returnData` `o` - Data from the previous call from the current environment. +-/ +structure MachineState where + gasAvailable : UInt256 + maxAddress : UInt256 + memory : Finmap (λ _ : UInt256 => UInt8) + returnData : ByteArray + deriving DecidableEq, Inhabited + +inductive WordSize := | Standard | Single + +def WordSize.toNat (this : WordSize) : ℕ := + match this with + | WordSize.Standard => 32 + | WordSize.Single => 1 + +instance : Coe WordSize Nat := ⟨WordSize.toNat⟩ + +end EvmYul diff --git a/EvmYul/MachineStateOps.lean b/EvmYul/MachineStateOps.lean new file mode 100644 index 0000000..3b17ebf --- /dev/null +++ b/EvmYul/MachineStateOps.lean @@ -0,0 +1,113 @@ +import EvmYul.MachineState + +import EvmYul.SpongeHash.Keccak256 + +namespace EvmYul + +namespace MachineState + +section Memory + +def new_max (self : MachineState) (addr : UInt256) (numOctets : WordSize) : ℕ := + max self.maxAddress (Rat.ceil ((addr.1 + numOctets) / 32)).toNat + +def updateMemory (self : MachineState) (addr v : UInt256) (numOctets : WordSize := WordSize.Standard) : MachineState := + { self with memory := let addrs := List.range 32 |>.map (·+addr) + let inserts := addrs.zipWith Finmap.insert (toBytes! v) + inserts.foldl (init := self.memory) (flip id) + maxAddress := self.new_max addr numOctets } + +def copyMemory (self : MachineState) (source : ByteArray) (s n : Nat) : MachineState := + { self with memory := (List.range n).map (UInt256.ofNat) |>.foldl (init := self.memory) + λ mem addr ↦ mem.insert (addr+s) (source.get! addr) + maxAddress := self.new_max (s + n) WordSize.Standard + } + +def lookupMemory (self : MachineState) (addr : UInt256) : UInt256 := + fromBytes! (List.map (λ i ↦ (self.memory.lookup (addr + i)).get!) (List.range 32)) + +def lookupMemoryRange (self : MachineState) (addr size : UInt256) : ByteArray := + ⟨⟨List.map (λ i ↦ (self.memory.lookup (addr + i)).get!) (List.range size)⟩⟩ + +def msize (self : MachineState) : UInt256 := + self.maxAddress + +def mload (self : MachineState) (spos : UInt256) : UInt256 × MachineState := + let val := self.lookupMemory spos + let rem := (spos + 32) % 32 + let divided := (spos + 32) / 32 + let maxAddress' := max self.maxAddress (if rem == 0 then divided else divided + 1) + (val, {self with maxAddress := maxAddress'}) + +def mstore (self : MachineState) (spos sval : UInt256) : MachineState := + self.updateMemory spos sval + +def mstore8 (self : MachineState) (spos sval : UInt256) : MachineState := + self.updateMemory spos (Fin.ofNat (sval.val % (2^8))) + +-- Apendix H, (320) +def M (s f l : UInt256) : UInt256 := + match l with + | 0 => s + | l => + -- ⌈ (f + l) ÷ 32 ⌉ + let rem := (f + l) % 32 + let divided := (f + l) / 32 + max s (if rem == 0 then divided else divided + 1) + +end Memory + +section ReturnData + +def setReturnData (self : MachineState) (r : ByteArray) : MachineState := + { self with returnData := r } + +def returndatasize (self : MachineState) : UInt256 := + self.returnData.size + +def returndataat (self : MachineState) (pos : UInt256) : UInt8 := + self.returnData.data.getD pos.val 0 + +def returndatacopy (self : MachineState) (mstart rstart s : UInt256) : Option MachineState := + let pos := rstart.val + s.val + -- TODO: + -- "The additions in μₛ[1]+i are not subject to the 2^256 modulo" + if UInt256.size ≤ pos || self.returndatasize.val ≤ pos then .none + else + let arr := self.returnData + let rdata := arr.extract rstart.val (rstart.val + s.val - 1) + let s := rdata.data.foldr (init := (self , mstart)) + λ v (ac, p) ↦ (ac.updateMemory p v.val, p +1) + .some s.1 + +def evmReturn (self : MachineState) (mstart s : UInt256) : MachineState := + let vals := self.returnData.extract mstart.val s.val + let maxAddress' := M self.maxAddress mstart s + {self with maxAddress := maxAddress'}.setReturnData vals + +def evmRevert (self : MachineState) (mstart s : UInt256) : MachineState := + self.evmReturn mstart s + +end ReturnData + +def keccak256 (self : MachineState) (mstart s : UInt256) : UInt256 × MachineState := + let vals := self.lookupMemoryRange mstart.val s.val + let kec := KEC vals + let maxAddress' := M self.maxAddress mstart s + (fromBytesBigEndian kec.data.data, {self with maxAddress := maxAddress'}) + +section Gas + +def mkNewWithGas (gas : ℕ) : MachineState := + let init : MachineState := default + { init with gasAvailable := gas } + +end Gas + +section Storage + +end Storage + +end MachineState + +end EvmYul diff --git a/EvmYul/Operations.lean b/EvmYul/Operations.lean new file mode 100644 index 0000000..b6dadd9 --- /dev/null +++ b/EvmYul/Operations.lean @@ -0,0 +1,765 @@ +import EvmYul.UInt256 +import EvmYul.MachineStateOps +import EvmYul.MachineState + +import Mathlib.Data.Finmap + +namespace EvmYul + +set_option autoImplicit true + +inductive OperationType where + | Yul + | EVM + deriving DecidableEq, Repr + +namespace Operation + +section Operation + +/-- + Stop and Arithmetic Operations +-/ +inductive SAOp (τ : OperationType) : Type where + /-- + Stop: halts program execution + δ: 0 ; α : 0 + -/ + | protected STOP : SAOp τ + /-- + ADD: adds two stack values. + δ: 2 ; α : 1 + -/ + | protected ADD : SAOp τ + /-- + MUL: multiplies two stack values. + δ: 2 ; α : 1 + -/ + | protected MUL : SAOp τ + /-- + SUB: subtracts two stack values. + δ: 2 ; α : 1 + -/ + | protected SUB : SAOp τ + /-- + DIV: divides two stack values. + δ: 2 ; α: 1 + -/ + | protected DIV : SAOp τ + /-- + SDIV: signed integer division + δ: 2 ; α: 1 + -/ + | protected SDIV : SAOp τ + /-- + MOD: Modulo remainder operation + δ: 2 ; α: 1 + -/ + | protected MOD : SAOp τ + /-- + SMOD: signed integer remainder + δ: 2 ; α: 1 + -/ + | protected SMOD : SAOp τ + /-- + ADDMOD: addition modulo operation + δ: 3 ; α: 1 + -/ + | protected ADDMOD : SAOp τ + /-- + MULMOD: multiplication modulo operation + δ: 3 ; α: 1 + -/ + | protected MULMOD : SAOp τ + /-- + EXP: Exponential operation + δ:2 ; α: 1 + -/ + | protected EXP : SAOp τ + /-- + SIGNEXTEND: Extend length of two's complement signed integer + δ: 2 ; α: 1 + -/ + | protected SIGNEXTEND : SAOp τ + deriving DecidableEq, Repr + +/-- + Comparison & Bitwise Logic Operations +-/ +inductive CBLOp (τ : OperationType) : Type where + /-- + LT: less than comparison + δ: 2 ; α: 1 + -/ + | protected LT : CBLOp τ + /-- + GT: greater than comparison + δ: 2 ; α: 1 + -/ + | protected GT : CBLOp τ + /-- + SLT: signed less-than comparison + δ:2 ; α: 1 + -/ + | protected SLT : CBLOp τ + /-- + SGT: signed greater-than comparison + δ: 2 ; α: 1 + -/ + | protected SGT : CBLOp τ + /-- + EQ: equality test + δ:2 ; α : 1 + -/ + | protected EQ : CBLOp τ + /-- + ISZERO: simple not operation + δ: 1 ; α : 1 + -/ + | protected ISZERO : CBLOp τ + /-- + AND: bitwise and + δ:2 ; α: 1 + -/ + | protected AND : CBLOp τ + /-- + OR: bitwise or + δ: 2 ; α: 1 + -/ + | protected OR : CBLOp τ + /-- + XOR: bitwise xor + δ: 2 ; α: 1 + -/ + | protected XOR : CBLOp τ + /-- + NOT: bitwise not + δ:1 ; α: 1 + -/ + | protected NOT : CBLOp τ + /-- + BYTE: retrieve single byte from a word + δ:2 ; α:1 + -/ + | protected BYTE : CBLOp τ + /-- + SHL: shift left operation + δ:2 ; α: 1 + -/ + | protected SHL : CBLOp τ + /-- + SHR: logical shift right operation + δ:2 ; α:1 + -/ + | protected SHR : CBLOp τ + /-- + SAR: arithmetical shift right operation + δ:2 ; α:1 + -/ + | protected SAR : CBLOp τ + deriving DecidableEq, Repr + +/-- + Keccak operation. +-/ +inductive KOp : OperationType → Type where + /-- + KECCAK256: compute KECCAK256 hash + δ:2 ; α: 1 + -/ + | protected KECCAK256 : KOp τ + deriving DecidableEq, Repr + +/-- + Environment Information. +-/ +inductive EOp : OperationType → Type where + /-- + ADDRESS: get the address of current executing account + δ:0 ; α: 1 + -/ + | protected ADDRESS : EOp τ + /-- + BALANCE: get the balance of an input account + δ:1 ; α: 1 + -/ + | protected BALANCE : EOp τ + /-- + ORIGIN: get execution origination address + δ:0 ; α: 1 + -/ + | protected ORIGIN : EOp τ + /-- + CALLER: returns the caller address + δ: 0 ; α: 1 + -/ + | protected CALLER : EOp τ + /-- + CALLVALUE: get deposited value by the instruction / transaction + responsible for this execution. + δ: 0 ; α: 1 + -/ + | protected CALLVALUE : EOp τ + /-- + CALLDATALOAD: get input data of current environment + δ: 1 ; α: 1 + -/ + | protected CALLDATALOAD : EOp τ + /-- + CALLDATASIZE: get size of input data in current environment + δ: 0 ; α: 1 + -/ + | protected CALLDATASIZE : EOp τ + /-- + CALLDATACOPY: copy input data from environment to memory + δ: 3 ; α: 0 + -/ + | protected CALLDATACOPY : EOp τ + /-- + CODESIZE: get the size of code running in current environment + δ:0 ; α: 1 + -/ + | protected GASPRICE : EOp τ + /-- + CODECOPY: Copy code running in current environment to memory + δ: 3 ; α: 0 + -/ + | protected CODESIZE : EOp τ + /-- + GASPRICE: Gas price in current execution environment + δ: 0 ; α: 1 + -/ + | protected CODECOPY : EOp τ + /-- + EXTCODESIZE: get the size of an account's code + δ:1 ; α: 1 + -/ + | protected EXTCODESIZE : EOp τ + /-- + EXTCODECOPY: copy an account's code to memory + δ: 4 ; α: 0 + -/ + | protected EXTCODECOPY : EOp τ + /-- + RETURNDATASIZE: get the size of output data from the previous call + from the current environment. + δ: 0 ; α: 1 + -/ + | protected RETURNDATASIZE : EOp τ + /-- + RETURNDATACOPY: copy output data from previous call to memory + δ: 3 ; α: 0 + -/ + | protected RETURNDATACOPY : EOp τ + /-- + EXTCODEHASH: get hash of an account's code + δ: 1 ; α: 1 + -/ + | protected EXTCODEHASH : EOp τ + deriving DecidableEq, Repr + +/-- + Block Information. +-/ +inductive BOp : OperationType → Type where + /-- + BLOCKHASH: get the hash of one of the 256 most recent blocks + δ:1 ; α: 1 + -/ + | protected BLOCKHASH : BOp τ + /-- + COINBASE: get current's block beneficiary address + δ: 0 ; α: 1 + -/ + | protected COINBASE : BOp τ + /-- + TIMESTAMP: get current block's timestamp + δ: 0 ; α: 1 + -/ + | protected TIMESTAMP : BOp τ + /-- + NUMBER: get current block's number + δ: 0 ; α: 1 + -/ + | protected NUMBER : BOp τ + | protected PREVRANDAO : BOp τ + /-- + DIFFICULTY: get current block's difficulty + δ: 0 ; α: 1 + -/ + | protected DIFFICULTY : BOp τ + /-- + GASLIMIT: get the gas limit for the current block + δ: 0 ; α: 1 + -/ + | protected GASLIMIT : BOp τ + /-- + CHAINID: returns the chainid, β + δ: 0 ; α: 1 + -/ + | protected CHAINID : BOp τ + /-- + SELFBALANCE: get the balance of the current executing account + δ: 0 ; α: 1 + -/ + | protected SELFBALANCE : BOp τ + | protected BASEFEE : BOp τ + deriving DecidableEq, Repr + +/-- + Stack, Memory, Storage and Flow Operations +-/ +inductive SMSFOp : OperationType → Type where + /-- + POP: remove an item from the stack + δ: 1 ; α: 0 + -/ + | protected POP : SMSFOp τ + /-- + MLOAD: load word from memory + δ: 1 ; α: 1 + -/ + | protected MLOAD : SMSFOp τ + /-- + MSTORE: save word in memory + δ: 2 ; α: 0 + -/ + | protected MSTORE : SMSFOp τ + /-- + SLOAD: load word from storage + δ: 1 ; α: 1 + -/ + | protected SLOAD : SMSFOp τ + /-- + SSTORE: Save word to storage + δ:2 ; α: 0 + -/ + | protected SSTORE : SMSFOp τ + /-- + MSTORE8: save byte in memory + δ: 2 ; α: 0 + -/ + | protected MSTORE8 : SMSFOp τ + /-- + JUMP: modify program counter + δ:1 ; α: 0 + -/ + | protected JUMP : SMSFOp .EVM + /-- + JUMPI: conditionally modify program counter + δ: 2 ; α: 0 + -/ + | protected JUMPI : SMSFOp .EVM + /-- + PC: get program counter before increment + δ: 0 ; α: 1 + -/ + | protected PC : SMSFOp τ + /-- + MSIZE: get the size of active memory in bytes + δ: 0 ; α: 1 + -/ + | protected MSIZE : SMSFOp τ + /-- + GAS: get the amount of available gas + δ: 0 ; α: 1 + -/ + | protected GAS : SMSFOp τ + /-- + JUMPDEST: mark a valid destination for jumps + δ: 0 ; α: 0 + -/ + | protected JUMPDEST : SMSFOp .EVM + deriving DecidableEq, Repr + +/-- + Push operations. + + PUSHn : pushes n bytes to stack. + δ: 0 ; α: 1 +-/ +inductive POp : Type where + | protected PUSH0 : POp + | protected PUSH1 : POp + | protected PUSH2 : POp + | protected PUSH3 : POp + | protected PUSH4 : POp + | protected PUSH5 : POp + | protected PUSH6 : POp + | protected PUSH7 : POp + | protected PUSH8 : POp + | protected PUSH9 : POp + | protected PUSH10 : POp + | protected PUSH11 : POp + | protected PUSH12 : POp + | protected PUSH13 : POp + | protected PUSH14 : POp + | protected PUSH15 : POp + | protected PUSH16 : POp + | protected PUSH17 : POp + | protected PUSH18 : POp + | protected PUSH19 : POp + | protected PUSH20 : POp + | protected PUSH21 : POp + | protected PUSH22 : POp + | protected PUSH23 : POp + | protected PUSH24 : POp + | protected PUSH25 : POp + | protected PUSH26 : POp + | protected PUSH27 : POp + | protected PUSH28 : POp + | protected PUSH29 : POp + | protected PUSH30 : POp + | protected PUSH31 : POp + | protected PUSH32 : POp + deriving DecidableEq, Repr + +/-- + Duplicate Operations. + + DUPn: duplicates the nth item on the stack. + δ: n ; α: n + 1 +-/ +inductive DOp : Type where + | protected DUP1 + | protected DUP2 + | protected DUP3 + | protected DUP4 + | protected DUP5 + | protected DUP6 + | protected DUP7 + | protected DUP8 + | protected DUP9 + | protected DUP10 + | protected DUP11 + | protected DUP12 + | protected DUP13 + | protected DUP14 + | protected DUP15 + | protected DUP16 + deriving DecidableEq, Repr + +/-- + Exchange Operations. + + SWAPn: swaps the 1st and nth element of the stack. + δ: n + 1 ; α: n + 1 + +-/ +inductive ExOp : Type where + | protected SWAP1 : ExOp + | protected SWAP2 : ExOp + | protected SWAP3 : ExOp + | protected SWAP4 : ExOp + | protected SWAP5 : ExOp + | protected SWAP6 : ExOp + | protected SWAP7 : ExOp + | protected SWAP8 : ExOp + | protected SWAP9 : ExOp + | protected SWAP10 : ExOp + | protected SWAP11 : ExOp + | protected SWAP12 : ExOp + | protected SWAP13 : ExOp + | protected SWAP14 : ExOp + | protected SWAP15 : ExOp + | protected SWAP16 : ExOp + deriving DecidableEq, Repr + +/-- + Logging Operations. + + LOGn: append log record with n topics. + δ: n + 2 ; α : 0 +-/ +inductive LOp : OperationType → Type where + | protected LOG0 : LOp τ + | protected LOG1 : LOp τ + | protected LOG2 : LOp τ + | protected LOG3 : LOp τ + | protected LOG4 : LOp τ + deriving DecidableEq, Repr + +/-- + System Operations. +-/ +inductive SOp : OperationType → Type where + /-- + CREATE: create a new account with associated code + δ: 3 ; α: 1 + -/ + | protected CREATE : SOp τ + /-- + CALL: message call into an account + δ: 7 ; α: 1 + -/ + | protected CALL : SOp τ + /-- + CALLCODE: message call into this account with an alternative account's code + δ: 7 ; α: 1 + -/ + | protected CALLCODE : SOp τ + /-- + RETURN: Halt execution returning output data + δ: 2 ; α: 0 + -/ + | protected RETURN : SOp τ + /-- + DELEGATECALL: message call into this account with an alternative account's code + but persisting the current values for sender and value + δ: 6 ; α: 1 + -/ + | protected DELEGATECALL : SOp τ + /-- + CREATE2: create a new account with associated code + δ: 4 ; α: 1 + -/ + | protected CREATE2 : SOp τ + /-- + STATICCALL: static message call into an account + δ: 6 ; α: 1 + -/ + | protected STATICCALL : SOp τ + /-- + REVERT: halt execution reverting state changes but returning data and remaining gas + δ: 2 ; α: 0 + -/ + | protected REVERT : SOp τ + /-- + INVALID: invalid opcode + δ: ∅ ; α: ∅ + -/ + | protected INVALID : SOp τ + /-- + SELFDESTRUCT: halt and mark account for later deletion. + δ: 1 ; α: 0 + -/ + | protected SELFDESTRUCT : SOp τ + deriving DecidableEq, Repr + +end Operation + +end Operation + +open Operation + +inductive Operation : OperationType → Type where + | protected StopArith : SAOp τ → Operation τ + | protected CompBit : CBLOp τ → Operation τ + | protected Keccak : KOp τ → Operation τ + | protected Env : EOp τ → Operation τ + | protected Block : BOp τ → Operation τ + | protected StackMemFlow : SMSFOp τ → Operation τ + | protected Push : POp → Operation .EVM + | protected Dup : DOp → Operation .EVM + | protected Exchange : ExOp → Operation .EVM + | protected Log : LOp τ → Operation τ + | protected System : SOp τ → Operation τ + deriving DecidableEq, Repr + +namespace Operation + +@[match_pattern] +abbrev STOP {τ : OperationType} : Operation τ := .StopArith .STOP +abbrev ADD {τ : OperationType} : Operation τ := .StopArith .ADD +abbrev MUL {τ : OperationType} : Operation τ := .StopArith .MUL +abbrev SUB {τ : OperationType} : Operation τ := .StopArith .SUB +abbrev DIV {τ : OperationType} : Operation τ := .StopArith .DIV +abbrev SDIV {τ : OperationType} : Operation τ := .StopArith .SDIV +abbrev MOD {τ : OperationType} : Operation τ := .StopArith .MOD +abbrev SMOD {τ : OperationType} : Operation τ := .StopArith .SMOD +abbrev ADDMOD {τ : OperationType} : Operation τ := .StopArith .ADDMOD +abbrev MULMOD {τ : OperationType} : Operation τ := .StopArith .MULMOD +abbrev EXP {τ : OperationType} : Operation τ := .StopArith .EXP +abbrev SIGNEXTEND {τ : OperationType} : Operation τ := .StopArith .SIGNEXTEND + +abbrev LT {τ : OperationType} : Operation τ := .CompBit .LT +abbrev GT {τ : OperationType} : Operation τ := .CompBit .GT +abbrev SLT {τ : OperationType} : Operation τ := .CompBit .SLT +abbrev SGT {τ : OperationType} : Operation τ := .CompBit .SGT +abbrev EQ {τ : OperationType} : Operation τ := .CompBit .EQ +abbrev ISZERO {τ : OperationType} : Operation τ := .CompBit .ISZERO +abbrev AND {τ : OperationType} : Operation τ := .CompBit .AND +abbrev OR {τ : OperationType} : Operation τ := .CompBit .OR +abbrev XOR {τ : OperationType} : Operation τ := .CompBit .XOR +abbrev NOT {τ : OperationType} : Operation τ := .CompBit .NOT +abbrev BYTE {τ : OperationType} : Operation τ := .CompBit .BYTE +abbrev SHL {τ : OperationType} : Operation τ := .CompBit .SHL +abbrev SHR {τ : OperationType} : Operation τ := .CompBit .SHR +abbrev SAR {τ : OperationType} : Operation τ := .CompBit .SAR + +abbrev KECCAK256 {τ : OperationType} : Operation τ := .Keccak .KECCAK256 + +abbrev ADDRESS {τ : OperationType} : Operation τ := .Env .ADDRESS +abbrev BALANCE {τ : OperationType} : Operation τ := .Env .BALANCE +abbrev ORIGIN {τ : OperationType} : Operation τ := .Env .ORIGIN +abbrev CALLER {τ : OperationType} : Operation τ := .Env .CALLER +abbrev CALLVALUE {τ : OperationType} : Operation τ := .Env .CALLVALUE +abbrev CALLDATALOAD {τ : OperationType} : Operation τ := .Env .CALLDATALOAD +abbrev CALLDATASIZE {τ : OperationType} : Operation τ := .Env .CALLDATASIZE +abbrev CALLDATACOPY {τ : OperationType} : Operation τ := .Env .CALLDATACOPY +abbrev CODESIZE {τ : OperationType} : Operation τ := .Env .CODESIZE +abbrev GASPRICE {τ : OperationType} : Operation τ := .Env .GASPRICE +abbrev CODECOPY {τ : OperationType} : Operation τ := .Env .CODECOPY +abbrev EXTCODECOPY {τ : OperationType} : Operation τ := .Env .EXTCODECOPY +abbrev EXTCODESIZE {τ : OperationType} : Operation τ := .Env .EXTCODESIZE +abbrev RETURNDATASIZE {τ : OperationType} : Operation τ := .Env .RETURNDATASIZE +abbrev RETURNDATACOPY {τ : OperationType} : Operation τ := .Env .RETURNDATACOPY +abbrev EXTCODEHASH {τ : OperationType} : Operation τ := .Env .EXTCODEHASH + +abbrev BLOCKHASH {τ : OperationType} : Operation τ := .Block .BLOCKHASH +abbrev COINBASE {τ : OperationType} : Operation τ := .Block .COINBASE +abbrev TIMESTAMP {τ : OperationType} : Operation τ := .Block .TIMESTAMP +abbrev NUMBER {τ : OperationType} : Operation τ := .Block .NUMBER +abbrev PREVRANDAO {τ : OperationType} : Operation τ := .Block .PREVRANDAO +abbrev DIFFICULTY {τ : OperationType} : Operation τ := .Block .DIFFICULTY +abbrev GASLIMIT {τ : OperationType} : Operation τ := .Block .GASLIMIT +abbrev CHAINID {τ : OperationType} : Operation τ := .Block .CHAINID +abbrev SELFBALANCE {τ : OperationType} : Operation τ := .Block .SELFBALANCE +abbrev BASEFEE {τ : OperationType} : Operation τ := .Block .BASEFEE + +abbrev POP {τ : OperationType} : Operation τ := .StackMemFlow .POP +abbrev MLOAD {τ : OperationType} : Operation τ := .StackMemFlow .MLOAD +abbrev MSTORE {τ : OperationType} : Operation τ := .StackMemFlow .MSTORE +abbrev SLOAD {τ : OperationType} : Operation τ := .StackMemFlow .SLOAD +abbrev SSTORE {τ : OperationType} : Operation τ := .StackMemFlow .SSTORE +abbrev MSTORE8 {τ : OperationType} : Operation τ := .StackMemFlow .MSTORE8 +abbrev JUMP : Operation .EVM := .StackMemFlow .JUMP +abbrev JUMPI : Operation .EVM := .StackMemFlow .JUMPI +abbrev PC {τ : OperationType} : Operation τ := .StackMemFlow .PC +abbrev MSIZE {τ : OperationType} : Operation τ := .StackMemFlow .MSIZE +abbrev GAS {τ : OperationType} : Operation τ := .StackMemFlow .GAS +abbrev JUMPDEST : Operation .EVM := .StackMemFlow .JUMPDEST + +abbrev PUSH0 : Operation .EVM := .Push .PUSH0 +abbrev PUSH1 : Operation .EVM := .Push .PUSH1 +abbrev PUSH2 : Operation .EVM := .Push .PUSH2 +abbrev PUSH3 : Operation .EVM := .Push .PUSH3 +abbrev PUSH4 : Operation .EVM := .Push .PUSH4 +abbrev PUSH5 : Operation .EVM := .Push .PUSH5 +abbrev PUSH6 : Operation .EVM := .Push .PUSH6 +abbrev PUSH7 : Operation .EVM := .Push .PUSH7 +abbrev PUSH8 : Operation .EVM := .Push .PUSH8 +abbrev PUSH9 : Operation .EVM := .Push .PUSH9 +abbrev PUSH10 : Operation .EVM := .Push .PUSH10 +abbrev PUSH11 : Operation .EVM := .Push .PUSH11 +abbrev PUSH12 : Operation .EVM := .Push .PUSH12 +abbrev PUSH13 : Operation .EVM := .Push .PUSH13 +abbrev PUSH14 : Operation .EVM := .Push .PUSH14 +abbrev PUSH15 : Operation .EVM := .Push .PUSH15 +abbrev PUSH16 : Operation .EVM := .Push .PUSH16 +abbrev PUSH17 : Operation .EVM := .Push .PUSH17 +abbrev PUSH18 : Operation .EVM := .Push .PUSH18 +abbrev PUSH19 : Operation .EVM := .Push .PUSH19 +abbrev PUSH20 : Operation .EVM := .Push .PUSH20 +abbrev PUSH21 : Operation .EVM := .Push .PUSH21 +abbrev PUSH22 : Operation .EVM := .Push .PUSH22 +abbrev PUSH23 : Operation .EVM := .Push .PUSH23 +abbrev PUSH24 : Operation .EVM := .Push .PUSH24 +abbrev PUSH25 : Operation .EVM := .Push .PUSH25 +abbrev PUSH26 : Operation .EVM := .Push .PUSH26 +abbrev PUSH27 : Operation .EVM := .Push .PUSH27 +abbrev PUSH28 : Operation .EVM := .Push .PUSH28 +abbrev PUSH29 : Operation .EVM := .Push .PUSH29 +abbrev PUSH30 : Operation .EVM := .Push .PUSH30 +abbrev PUSH31 : Operation .EVM := .Push .PUSH31 +abbrev PUSH32 : Operation .EVM := .Push .PUSH32 + +abbrev DUP1 : Operation .EVM := .Dup .DUP1 +abbrev DUP2 : Operation .EVM := .Dup .DUP2 +abbrev DUP3 : Operation .EVM := .Dup .DUP3 +abbrev DUP4 : Operation .EVM := .Dup .DUP4 +abbrev DUP5 : Operation .EVM := .Dup .DUP5 +abbrev DUP6 : Operation .EVM := .Dup .DUP6 +abbrev DUP7 : Operation .EVM := .Dup .DUP7 +abbrev DUP8 : Operation .EVM := .Dup .DUP8 +abbrev DUP9 : Operation .EVM := .Dup .DUP9 +abbrev DUP10 : Operation .EVM := .Dup .DUP10 +abbrev DUP11 : Operation .EVM := .Dup .DUP11 +abbrev DUP12 : Operation .EVM := .Dup .DUP12 +abbrev DUP13 : Operation .EVM := .Dup .DUP13 +abbrev DUP14 : Operation .EVM := .Dup .DUP14 +abbrev DUP15 : Operation .EVM := .Dup .DUP15 +abbrev DUP16 : Operation .EVM := .Dup .DUP16 + +abbrev SWAP1 : Operation .EVM := .Exchange .SWAP1 +abbrev SWAP2 : Operation .EVM := .Exchange .SWAP2 +abbrev SWAP3 : Operation .EVM := .Exchange .SWAP3 +abbrev SWAP4 : Operation .EVM := .Exchange .SWAP4 +abbrev SWAP5 : Operation .EVM := .Exchange .SWAP5 +abbrev SWAP6 : Operation .EVM := .Exchange .SWAP6 +abbrev SWAP7 : Operation .EVM := .Exchange .SWAP7 +abbrev SWAP8 : Operation .EVM := .Exchange .SWAP8 +abbrev SWAP9 : Operation .EVM := .Exchange .SWAP9 +abbrev SWAP10 : Operation .EVM := .Exchange .SWAP10 +abbrev SWAP11 : Operation .EVM := .Exchange .SWAP11 +abbrev SWAP12 : Operation .EVM := .Exchange .SWAP12 +abbrev SWAP13 : Operation .EVM := .Exchange .SWAP13 +abbrev SWAP14 : Operation .EVM := .Exchange .SWAP14 +abbrev SWAP15 : Operation .EVM := .Exchange .SWAP15 +abbrev SWAP16 : Operation .EVM := .Exchange .SWAP16 + +abbrev LOG0 {τ : OperationType} : Operation τ := .Log .LOG0 +abbrev LOG1 {τ : OperationType} : Operation τ := .Log .LOG1 +abbrev LOG2 {τ : OperationType} : Operation τ := .Log .LOG2 +abbrev LOG3 {τ : OperationType} : Operation τ := .Log .LOG3 +abbrev LOG4 {τ : OperationType} : Operation τ := .Log .LOG4 + +abbrev CREATE {τ : OperationType} : Operation τ := .System .CREATE +abbrev CALL {τ : OperationType} : Operation τ := .System .CALL +abbrev CALLCODE {τ : OperationType} : Operation τ := .System .CALLCODE +abbrev RETURN {τ : OperationType} : Operation τ := .System .RETURN +abbrev DELEGATECALL {τ : OperationType} : Operation τ := .System .DELEGATECALL +abbrev CREATE2 {τ : OperationType} : Operation τ := .System .CREATE2 +abbrev STATICCALL {τ : OperationType} : Operation τ := .System .STATICCALL +abbrev REVERT {τ : OperationType} : Operation τ := .System .REVERT +abbrev INVALID {τ : OperationType} : Operation τ := .System .INVALID +abbrev SELFDESTRUCT {τ : OperationType} : Operation τ := .System .SELFDESTRUCT + +end Operation + +open EvmYul.UInt256 + +def addMod (a b c : UInt256) : UInt256 := + if c = 0 then 0 else + Fin.mod (a + b) c + +def mulMod (a b c : UInt256) : UInt256 := + if c = 0 then 0 else + Fin.mod (a * b) c + +def exp (a b : UInt256) : UInt256 := + a ^ b.val + +abbrev fromBool := Bool.toUInt256 + +def lt (a b : UInt256) := + fromBool (a < b) + +def gt (a b : UInt256) := + fromBool (a > b) + +-- def slt (a b : UInt256) := +-- fromBool (EvmYul.UInt256.slt a b) + +-- def sgt (a b : UInt256) := +-- fromBool (EvmYul.UInt256.sgt a b) + +def eq (a b : UInt256) := + fromBool (a = b) + +def isZero (a : UInt256) := + fromBool (a = 0) + +end EvmYul + +open EvmYul + +-- Apendix H, (320) +def M (s f l : UInt256) : UInt256 := + match l with + | 0 => s + | l => + -- ⌈ (f + l) ÷ 32 ⌉ + let rem := (f + l) % 32 + let divided := (f + l) / 32 + max s (if rem == 0 then divided else divided + 1) diff --git a/EvmYul/Semantics.lean b/EvmYul/Semantics.lean new file mode 100644 index 0000000..39fc570 --- /dev/null +++ b/EvmYul/Semantics.lean @@ -0,0 +1,422 @@ +import EvmYul.Operations + +import EvmYul.Yul.State +import EvmYul.Yul.Ast +import EvmYul.Yul.Exception +import EvmYul.Yul.PrimOps +import EvmYul.Yul.StateOps + +import EvmYul.EVM.State +import EvmYul.EVM.Exception +import EvmYul.EVM.PrimOps +import EvmYul.EVM.StateOps +import EvmYul.Wheels + +import EvmYul.UInt256 +import EvmYul.StateOps +import EvmYul.SharedStateOps +import EvmYul.MachineStateOps + +import EvmYul.SpongeHash.Keccak256 + +namespace EvmYul + +section Semantics + +/-- +`Transformer` is the primop-evaluating semantic function type for `Yul` and `EVM`. + +- `EVM` is `EVM.State → EVM.State` because the arguments are already contained in `EVM.State.stack`. +- `Yul` is `Yul.State × List Literal → Yul.State × Option Literal` because the evaluation of primops in Yul + does *not* store results within the state. + +Both operations happen in their respecitve `.Exception` error monad. +-/ +private abbrev Transformer : OperationType → Type + | .EVM => EVM.Transformer + | .Yul => Yul.Transformer + +private def dispatchInvalid (τ : OperationType) : Transformer τ := + match τ with + | .EVM => λ _ ↦ .error EVM.Exception.InvalidInstruction + | .Yul => λ _ _ ↦ .error Yul.Exception.InvalidInstruction + +private def dispatchUnary (τ : OperationType) : Primop.Unary → Transformer τ := + match τ with + | .EVM => EVM.execUnOp + | .Yul => Yul.execUnOp + +private def dispatchBinary (τ : OperationType) : Primop.Binary → Transformer τ := + match τ with + | .EVM => EVM.execBinOp + | .Yul => Yul.execBinOp + +private def dispatchTernary (τ : OperationType) : Primop.Ternary → Transformer τ := + match τ with + | .EVM => EVM.execTriOp + | .Yul => Yul.execTriOp + +private def dispatchQuartiary (τ : OperationType) : Primop.Quaternary → Transformer τ := + match τ with + | .EVM => EVM.execQuadOp + | .Yul => Yul.execQuadOp + +private def dispatchExecutionEnvOp (τ : OperationType) (op : ExecutionEnv → UInt256) : Transformer τ := + match τ with + | .EVM => EVM.executionEnvOp op + | .Yul => Yul.executionEnvOp op + +private def dispatchMachineStateOp (τ : OperationType) (op : MachineState → UInt256) : Transformer τ := + match τ with + | .EVM => EVM.machineStateOp op + | .Yul => Yul.machineStateOp op + +private def dispatchUnaryStateOp (τ : OperationType) (op : State → UInt256 → State × UInt256) : Transformer τ := + match τ with + | .EVM => EVM.unaryStateOp op + | .Yul => Yul.unaryStateOp op + +private def dispatchTernaryCopyOp + (τ : OperationType) (op : SharedState → UInt256 → UInt256 → UInt256 → SharedState) : + Transformer τ +:= + match τ with + | .EVM => EVM.ternaryCopyOp op + | .Yul => Yul.ternaryCopyOp op + +private def dispatchQuaternaryCopyOp + (τ : OperationType) (op : SharedState → UInt256 → UInt256 → UInt256 → UInt256 → SharedState) : + Transformer τ +:= + match τ with + | .EVM => EVM.quaternaryCopyOp op + | .Yul => Yul.quaternaryCopyOp op + +private def dispatchBinaryMachineStateOp + (τ : OperationType) (op : MachineState → UInt256 → UInt256 → MachineState) : + Transformer τ +:= + match τ with + | .EVM => EVM.binaryMachineStateOp op + | .Yul => Yul.binaryMachineStateOp op + + +private def dispatchBinaryMachineStateOp' + (τ : OperationType) (op : MachineState → UInt256 → UInt256 → UInt256 × MachineState) : + Transformer τ +:= + match τ with + | .EVM => EVM.binaryMachineStateOp' op + | .Yul => Yul.binaryMachineStateOp' op + +private def dispatchBinaryStateOp + (τ : OperationType) (op : State → UInt256 → UInt256 → State) : + Transformer τ +:= + match τ with + | .EVM => EVM.binaryStateOp op + | .Yul => Yul.binaryStateOp op + +private def dispatchStateOp (τ : OperationType) (op : State → UInt256) : Transformer τ := + match τ with + | .EVM => EVM.stateOp op + | .Yul => Yul.stateOp op + +private def dispatchLog0 (τ : OperationType) : Transformer τ := + match τ with + | .EVM => EVM.log0Op + | .Yul => Yul.log0Op + +private def dispatchLog1 (τ : OperationType) : Transformer τ := + match τ with + | .EVM => EVM.log1Op + | .Yul => Yul.log1Op + +private def dispatchLog2 (τ : OperationType) : Transformer τ := + match τ with + | .EVM => EVM.log2Op + | .Yul => Yul.log2Op + +private def dispatchLog3 (τ : OperationType) : Transformer τ := + match τ with + | .EVM => EVM.log3Op + | .Yul => Yul.log3Op + +private def dispatchLog4 (τ : OperationType) : Transformer τ := + match τ with + | .EVM => EVM.log4Op + | .Yul => Yul.log4Op + +private def L (n : ℕ) := n - n / 64 + + +def toHex (bytes : ByteArray) : String := + bytes.foldl (init := "") λ acc byte ↦ acc ++ hexOfByte byte + +def shortInput := "01aHHABLA" +def longInput := "Lean 4 is a reimplementation of the Lean theorem prover in Lean itself. The new compiler produces C code, and users can now implement efficient proof automation in Lean, compile it into efficient C code, and load it as a plugin. In Lean 4, users can access all internal data structures used to implement Lean by merely importing the Lean package." +-- Look ok 596cfd6c2f8f76b8f480f5c2fc582db9089486792435f397f8286aff64d42646 +#eval toHex $ KEC shortInput.toUTF8 +#eval toHex $ KEC longInput.toUTF8 +-- Appendix B. Recursive Length Prefix + +inductive 𝕋 := + | 𝔹 : ByteArray → 𝕋 + | 𝕃 : (List 𝕋) → 𝕋 + +private def R_b (x : ByteArray) : Option ByteArray := + if x.size = 1 ∧ x.get! 0 < 128 then some x + else + if x.size < 56 then some <| [⟨128 + x.size⟩].toByteArray ++ x + else + if x.size < 2^64 then + let BE : ByteArray := (toBytesBigEndian x.size).toByteArray + some <| [⟨183 + BE.size⟩].toByteArray ++ BE ++ x + else none + +mutual + +private def s (l : List 𝕋) : Option ByteArray := + match l with + | [] => some .empty + | t :: ts => + match RLP t, s ts with + | none , _ => none + | _ , none => none + | some rlpₗ, some rlpᵣ => rlpₗ ++ rlpᵣ + +def R_l (l : List 𝕋) : Option ByteArray := + match s l with + | none => none + | some s_x => + if s_x.size < 65 then + some <| [⟨192 + s_x.size⟩].toByteArray ++ s_x + else + if s_x.size < 2^64 then + let BE : ByteArray := (toBytesBigEndian s_x.size).toByteArray + some <| [⟨183 + BE.size⟩].toByteArray ++ BE ++ s_x + else none + +def RLP (t : 𝕋) : Option ByteArray := + match t with + | .𝔹 ba => R_b ba + | .𝕃 l => R_l l + +def step {τ : OperationType} (op : Operation τ) : Transformer τ := + match τ, op with + -- TODO: Revisit STOP, this is likely not the best way to do it and the Yul version is WIP. + | τ, .STOP => + match τ with + | .EVM => λ evmState ↦ .ok <| {evmState with toMachineState := evmState.toMachineState.setReturnData .empty} + | .Yul => λ yulState _ ↦ .ok (yulState, none) + | τ, .ADD => dispatchBinary τ UInt256.add + | τ, .MUL => dispatchBinary τ UInt256.mul + | τ, .SUB => dispatchBinary τ UInt256.add + | τ, .DIV => dispatchBinary τ UInt256.div + | τ, .SDIV => dispatchBinary τ UInt256.sdiv + | τ, .MOD => dispatchBinary τ UInt256.mod + | τ, .SMOD => dispatchBinary τ UInt256.smod + | τ, .ADDMOD => dispatchTernary τ UInt256.addMod + | τ, .MULMOD => dispatchTernary τ UInt256.mulMod + | τ, .EXP => dispatchBinary τ UInt256.exp + | τ, .SIGNEXTEND => dispatchBinary τ UInt256.signextend + + | τ, .LT => dispatchBinary τ UInt256.lt + | τ, .GT => dispatchBinary τ UInt256.gt + | τ, .SLT => dispatchBinary τ UInt256.slt + | τ, .SGT => dispatchBinary τ UInt256.sgt + | τ, .EQ => dispatchBinary τ UInt256.eq + | τ, .ISZERO => dispatchUnary τ UInt256.isZero + | τ, .AND => dispatchBinary τ UInt256.land + | τ, .OR => dispatchBinary τ UInt256.lor + | τ, .XOR => dispatchBinary τ UInt256.xor + | τ, .NOT => dispatchUnary τ UInt256.lnot + | τ, .BYTE => dispatchBinary τ UInt256.byteAt + | τ, .SHL => dispatchBinary τ UInt256.shiftLeft + | τ, .SHR => dispatchBinary τ UInt256.shiftRight + | τ, .SAR => dispatchBinary τ UInt256.sar + + | τ, .KECCAK256 => dispatchBinaryMachineStateOp' τ MachineState.keccak256 + + | τ, .ADDRESS => dispatchExecutionEnvOp τ (Fin.ofNat ∘ Fin.val ∘ ExecutionEnv.codeOwner) + | τ, .BALANCE => dispatchUnaryStateOp τ EvmYul.State.balance + | τ, .ORIGIN => dispatchExecutionEnvOp τ (Fin.ofNat ∘ Fin.val ∘ ExecutionEnv.sender) + | τ, .CALLER => dispatchExecutionEnvOp τ (Fin.ofNat ∘ Fin.val ∘ ExecutionEnv.source) + | τ, .CALLVALUE => dispatchExecutionEnvOp τ (Fin.ofNat ∘ Fin.val ∘ ExecutionEnv.weiValue) + | τ, .CALLDATALOAD => dispatchUnaryStateOp τ (λ s v ↦ (s, EvmYul.State.calldataload s v)) + | τ, .CALLDATASIZE => dispatchExecutionEnvOp τ (.size ∘ ExecutionEnv.inputData) + | τ, .CALLDATACOPY => dispatchTernaryCopyOp τ .calldatacopy + | τ, .CODESIZE => dispatchExecutionEnvOp τ (.size ∘ ExecutionEnv.code) + | τ, .CODECOPY => dispatchTernaryCopyOp τ .codeCopy + | τ, .GASPRICE => dispatchExecutionEnvOp τ (.ofNat ∘ ExecutionEnv.gasPrice) + | τ, .EXTCODESIZE => dispatchUnaryStateOp τ EvmYul.State.extCodeSize + | τ, .EXTCODECOPY => dispatchQuaternaryCopyOp τ EvmYul.SharedState.extCodeCopy + | τ, .RETURNDATASIZE => dispatchMachineStateOp τ EvmYul.MachineState.returndatasize + | .EVM, .RETURNDATACOPY => + λ evmState ↦ + match evmState.stack.pop3 with + | some ⟨stack', μ₀, μ₁, μ₂⟩ => do + let .some mState' := evmState.toMachineState.returndatacopy μ₀ μ₁ μ₂ + | .error EVM.Exception.OutOfBounds + .ok <| {evmState with toMachineState := mState'} + | _ => .error EVM.Exception.InvalidStackSizeException + | .Yul, .RETURNDATACOPY => + λ yulState lits ↦ + match lits with + | [a, b, c] => do + let .some mState' := yulState.toSharedState.toMachineState.returndatacopy a b c + | .error .InvalidArguments + .ok <| (yulState.setMachineState mState', .none) + | _ => .error .InvalidArguments + | τ, .EXTCODEHASH => dispatchUnaryStateOp τ (λ s v ↦ (s, EvmYul.State.extCodeHash s v)) + + | τ, .BLOCKHASH => dispatchUnaryStateOp τ (λ s v ↦ (s, EvmYul.State.blockHash s v)) + | τ, .COINBASE => dispatchStateOp τ (Fin.ofNat ∘ Fin.val ∘ EvmYul.State.coinBase) + | τ, .TIMESTAMP => dispatchStateOp τ EvmYul.State.timeStamp + | τ, .NUMBER => dispatchStateOp τ EvmYul.State.number + -- "RANDAO is a pseudorandom value generated by validators on the Ethereum consensus layer" + -- "the details of generating the RANDAO value on the Beacon Chain is beyond the scope of this paper" + | τ, .PREVRANDAO => sorry + | τ, .DIFFICULTY => dispatchStateOp τ EvmYul.State.difficulty + | τ, .GASLIMIT => dispatchStateOp τ EvmYul.State.gasLimit + | τ, .CHAINID => dispatchStateOp τ EvmYul.State.chainId + | τ, .SELFBALANCE => dispatchStateOp τ EvmYul.State.selfbalance + + | .EVM, .POP => + λ evmState ↦ + match evmState.stack.pop with + | some ⟨ s , _ ⟩ => .ok <| evmState.replaceStackAndIncrPC s + | _ => .error EVM.Exception.InvalidStackSizeException + + | .EVM, .MLOAD => λ evmState ↦ + match evmState.stack.pop with + | some ⟨ s , μ₀ ⟩ => + let (v, mState') := evmState.toMachineState.mload μ₀ + let evmState' := {evmState with toMachineState := mState'} + .ok <| evmState'.replaceStackAndIncrPC (s.push v) + | _ => .error EVM.Exception.InvalidStackSizeException + | .Yul, .MLOAD => λ yulState lits ↦ + match lits with + | [a] => + let (v, mState') := yulState.toSharedState.toMachineState.mload a + let yulState' := yulState.setMachineState mState' + .ok <| (yulState', some v) + | _ => .error .InvalidArguments + | τ, .MSTORE => dispatchBinaryMachineStateOp τ MachineState.mstore + | τ, .MSTORE8 => dispatchBinaryMachineStateOp τ MachineState.mstore8 + | τ, .SLOAD => dispatchUnaryStateOp τ EvmYul.State.sload + | τ, .SSTORE => dispatchBinaryStateOp τ EvmYul.State.sstore + | τ, .MSIZE => dispatchMachineStateOp τ MachineState.msize + + | τ, .LOG0 => dispatchLog0 τ + | τ, .LOG1 => dispatchLog1 τ + | τ, .LOG2 => dispatchLog2 τ + | τ, .LOG3 => dispatchLog3 τ + | τ, .LOG4 => dispatchLog4 τ + + | .Yul, .CREATE => λ yulState lits ↦ + match lits with + | [v, poz, len] => + let Iₐ := yulState.executionEnv.codeOwner + let nonce' : UInt256 := yulState.toState.accountMap.lookup Iₐ |>.option 0 Account.nonce + let s : 𝕋 := .𝔹 (toBytesBigEndian Iₐ.val).toByteArray + let n : 𝕋 := .𝔹 (toBytesBigEndian nonce').toByteArray + let L_A := RLP <| .𝕃 [s, n] + match L_A with + | none => .error .NotEncodableRLP + | some L_A => + let addr : Address := + (KEC L_A).extract 96 265 |>.data.data |> fromBytesBigEndian |> Fin.ofNat + let code : ByteArray := yulState.toMachineState.lookupMemoryRange poz len + -- σ* + let accountMapStar := + match yulState.toState.accountMap.lookup Iₐ with + | none => yulState.toState.accountMap + | some ac => + yulState.toState.accountMap.insert + Iₐ + {ac with balance := ac.balance - v, nonce := ac.nonce + 1} + let v' := + match yulState.toState.accountMap.lookup addr with + | none => 0 + | some ac => ac.balance + let newAccount : Account := + ⟨1, v + v', code, fromBytesBigEndian (KEC code).data.data, default⟩ + let yulState' := yulState.setState (yulState.toState.updateAccount addr newAccount) + + .ok <| (yulState', some addr) + | _ => .error .InvalidArguments + | τ, .RETURN => dispatchBinaryMachineStateOp τ MachineState.evmReturn + | τ, .REVERT => dispatchBinaryMachineStateOp τ MachineState.evmRevert + | .EVM, .SELFDESTRUCT => + λ evmState ↦ + match evmState.stack.pop with + | some ⟨ s , μ₁ ⟩ => + let Iₐ := evmState.executionEnv.codeOwner + let r : Address := Address.ofUInt256 μ₁ + let A' : Substate := + { evmState.substate with + selfDestructSet := + evmState.substate.selfDestructSet ∪ {Iₐ} + accessedAccounts := + evmState.substate.accessedAccounts ∪ {r} + } + let accountMap' := + match evmState.lookupAccount r, evmState.lookupAccount Iₐ with + | some σ_r, some σ_Iₐ => + if r ≠ Iₐ then + evmState.accountMap.insert r + {σ_r with balance := σ_r.balance + σ_Iₐ.balance} + |>.insert Iₐ {σ_Iₐ with balance := 0} + else + evmState.accountMap.insert r {σ_r with balance := 0} + |>.insert Iₐ {σ_Iₐ with balance := 0} + | _, _ => evmState.accountMap + let evmState' := {evmState with accountMap := accountMap'} + .ok <| evmState.replaceStackAndIncrPC s + | _ => .error EVM.Exception.InvalidStackSizeException + | .EVM, .CALL => λ evmState ↦ + match evmState.stack.pop7 with + | some ⟨stack', μ₀, μ₁, μ₂, μ₃, μ₄, μ₅, μ₆⟩ => + .ok <| sorry + | _ => .error EVM.Exception.InvalidStackSizeException + | τ, .INVALID => dispatchInvalid τ + + | .Yul, .CREATE2 => λ yulState lits ↦ + match lits with + | [v, poz, len, ζ] => + let Iₐ := yulState.executionEnv.codeOwner + let this₀ := toBytesBigEndian Iₐ.val + let this : List UInt8 := List.replicate (20 - this₀.length) 0 ++ this₀ + let code : ByteArray := yulState.toMachineState.lookupMemoryRange poz len + let s : List UInt8 := toBytesBigEndian ζ + let a₀ : List UInt8 := [0xff] + let addr₀ := KEC <| ⟨⟨a₀ ++ this ++ s⟩⟩ ++ KEC code + let addr : Address := Fin.ofNat <| fromBytesBigEndian addr₀.data.data + let accountMapStar := + match yulState.toState.accountMap.lookup Iₐ with + | none => yulState.toState.accountMap + | some ac => + yulState.toState.accountMap.insert + Iₐ + {ac with balance := ac.balance - v, nonce := ac.nonce + 1} + let v' := + match yulState.toState.accountMap.lookup addr with + | none => 0 + | some ac => ac.balance + let newAccount : Account := + ⟨1, v + v', code, fromBytesBigEndian (KEC code).data.data, default⟩ + let yulState' := yulState.setState (yulState.toState.updateAccount addr newAccount) + .ok <| (yulState', some addr) + | _ => .error .InvalidArguments + + | _, _ => sorry + +end + +#eval toBytesBigEndian 0 +#eval RLP (.𝔹 (toBytesBigEndian 123456789).toByteArray) |>.option "" toHex + +end Semantics + +end EvmYul diff --git a/EvmYul/SharedState.lean b/EvmYul/SharedState.lean new file mode 100644 index 0000000..23f486e --- /dev/null +++ b/EvmYul/SharedState.lean @@ -0,0 +1,9 @@ +import EvmYul.State +import EvmYul.MachineState + +namespace EvmYul + +structure SharedState extends EvmYul.State, EvmYul.MachineState + deriving DecidableEq, Inhabited + +end EvmYul diff --git a/EvmYul/SharedStateOps.lean b/EvmYul/SharedStateOps.lean new file mode 100644 index 0000000..a7b2c1c --- /dev/null +++ b/EvmYul/SharedStateOps.lean @@ -0,0 +1,64 @@ +import EvmYul.SharedState +import EvmYul.StateOps +import EvmYul.MachineStateOps +import EvmYul.Operations +import Mathlib.Data.List.Intervals + +namespace EvmYul + +namespace SharedState + +section Keccak + +def keccak256 (s : SharedState) (p n : UInt256) : Option (UInt256 × SharedState) := + let interval : List UInt256 := mkInterval s.toMachineState p n + match s.keccakMap.lookup interval with + | .some val => .some (val, s) + | .none => + match s.toState.keccakRange.partition (λ x ↦ x ∈ s.toState.usedRange) with + | (_,(r :: rs)) => + .some (r, { s with toState.keccakMap := s.toState.keccakMap.insert interval r, + toState.keccakRange := rs, + toState.usedRange := {r} ∪ s.toState.usedRange }) + | (_, []) => .none + where mkInterval (ms : MachineState) (p n : UInt256) : List UInt256 := + (List.Ico p (p + n)).map ms.lookupMemory + +end Keccak + +section Memory + +def updateMemory (self : SharedState) (addr v : UInt256) (numOctets : WordSize := WordSize.Standard) : SharedState := + { self with toMachineState := self.toMachineState.updateMemory addr v numOctets } + +def calldatacopy (self : SharedState) (mstart datastart s : UInt256) : SharedState := + let arr := self.toState.executionEnv.inputData.extract datastart.val s.val + (·.1) <| arr.foldl (init := (self, mstart)) λ (sa , j) i ↦ (sa.updateMemory j i.val, j + 1) + +def codeCopy (self : SharedState) (mstart cstart s : UInt256) : SharedState := + let Ib := self.toState.executionEnv.code.extract cstart.val s.val -- TODO(double check, changed in a fast-and-loose manner) + (·.1) <| Ib.foldl (init := (self, mstart)) λ (sa, j) i ↦ (sa.updateMemory j i.toUInt256, j + 1) + +def extCodeCopy (self : SharedState) (acc mstart cstart s : UInt256) : SharedState := + let addr := Address.ofUInt256 acc + let sState' : SharedState := + match self.toState.lookupAccount addr with + | .some act1 => + let Ib := act1.code.extract cstart.val s.val + (·.1) <| Ib.foldl (init := (self, mstart)) λ (sa, j) i ↦ (sa.updateMemory j i.toUInt256, j + 1) + | _ => + (·.1) <| s.val.fold (init := (self, mstart)) λ _ (sa , j) ↦ (sa.updateMemory j 0, j + 1) + {sState' with toState.substate := .addAccessedAccount self.toState.substate addr} + +end Memory + +def logOp (μ₀ μ₁ : UInt256) (t : List UInt256) (sState : SharedState) : Substate × UInt256 := + let Iₐ := sState.executionEnv.codeOwner + let mem := sState.toMachineState.lookupMemoryRange μ₀ μ₁ + let logSeries' := sState.toState.substate.logSeries.push (Iₐ, t, mem) + let μᵢ' := MachineState.M sState.maxAddress μ₀ μ₁ + ({sState.substate with logSeries := logSeries'}, μᵢ') + +end SharedState + +end EvmYul diff --git a/EvmYul/SpongeHash/Keccak256.lean b/EvmYul/SpongeHash/Keccak256.lean new file mode 100644 index 0000000..cef8391 --- /dev/null +++ b/EvmYul/SpongeHash/Keccak256.lean @@ -0,0 +1,206 @@ +import Mathlib.Tactic + +import EvmYul.SpongeHash.Wheels + +open BigOperators +open Vector + +abbrev SHA3SR : Type := Array UInt64 + +instance : Coe Bool (Fin 2) := ⟨(if · then 1 else 0)⟩ +instance : Coe (Fin 2) Bool := ⟨(·.1 == 1)⟩ + +def Rounds : Nat := 24 + +def NumLanes : Nat := 25 + +def LaneWidth : Nat := 64 + +def RoundConstants : Array UInt64 := + #[ 0x0000000000000001, 0x0000000000008082, 0x800000000000808A + , 0x8000000080008000, 0x000000000000808B, 0x0000000080000001 + , 0x8000000080008081, 0x8000000000008009, 0x000000000000008A + , 0x0000000000000088, 0x0000000080008009, 0x000000008000000A + , 0x000000008000808B, 0x800000000000008B, 0x8000000000008089 + , 0x8000000000008003, 0x8000000000008002, 0x8000000000000080 + , 0x000000000000800A, 0x800000008000000A, 0x8000000080008081 + , 0x8000000000008080, 0x0000000080000001, 0x8000000080008008 ] + +def rotationConstants : Array Nat := + #[ 0, 36, 3, 41, 18 + , 1, 44, 10, 45, 2 + , 62, 6, 43, 15, 61 + , 28, 55, 25, 21, 56 + , 27, 20, 39, 8, 14 ] + +def piConstants : Array Nat := + #[ 0, 15, 5, 20, 10 + , 6, 21, 11, 1, 16 + , 12, 2, 17, 7, 22 + , 18, 8, 23, 13, 3 + , 24, 14, 4, 19, 9 ] + +def rotateL (a : UInt64) (n : Nat) : UInt64 := UInt64.ofNat (BitVec.ofNat 64 a.toNat |>.rotateLeft n).toNat + +def complement (a : UInt64) : UInt64 := UInt64.ofNat (Complement.complement <| BitVec.ofNat 64 a.toNat).toNat + +def Array.foldl1 {β : Type} [Inhabited β] (f : β → β → β) (as : Array β) : β := + Array.foldl f (as[0]!) ⟨as.data.drop 1⟩ + +def θ (state : SHA3SR) : SHA3SR := + let indexed := Array.zip (Array.range 25) d + indexed.concatMap λ (i, e) ↦ Array.map (· ^^^ e) (state.extract (i * 5) (i * 5 + 5)) + where c : SHA3SR := Array.range 5 |>.map λ i ↦ (state.extract (i * 5) (i * 5 + 5)).foldl1 (·^^^·) + d : SHA3SR := Array.range 5 |>.map λ i ↦ c[(Int.ofNat i - 1) % 5 |>.toNat]! ^^^ rotateL (c[(Int.ofNat i + 1) % 5 |>.toNat]!) 1 + +def ρ (state : SHA3SR) : SHA3SR := Array.zipWith rotationConstants state (flip rotateL) + +def Array.backpermute {α} [Inhabited α] : Array α → Array Nat → Array α := λ xs ↦ Array.map (xs[·]!) + +def π (state : SHA3SR) : SHA3SR := state.backpermute piConstants + +def Array.imap {α β} (f : ℕ → α → β) (arr : Array α) : Array β := + let indexed := Array.zip (Array.range arr.size) arr + indexed.map (Function.uncurry f) + +def χ (b : SHA3SR) : SHA3SR := Array.imap subChi b + where subChi z el := el ^^^ (complement (b[(z + 5) % 25]!) &&& (b[(z + 10) % 25]!)) + +def ι (roundNumber : Nat) (state : SHA3SR) : SHA3SR := state.setD 0 (RoundConstants[roundNumber]! ^^^ (state[0]!)) + +def keccak_round (r : ℕ) : SHA3SR → SHA3SR := ι r ∘ χ ∘ π ∘ ρ ∘ θ + +def keccakF'' (s : SHA3SR) : SHA3SR := + let f : ℕ × SHA3SR → ℕ × SHA3SR := λ (r, s) => (.succ r, keccak_round r $ s) + (List.foldl Function.comp id (List.replicate 24 f) (0, s)).2 + +def keccakF (state : SHA3SR) : SHA3SR := + (·.2) <| Array.foldl1 (·∘·) (⟨List.replicate Rounds f⟩) (0, state) + where f : Nat × SHA3SR → Nat × SHA3SR := λ (r, s) ↦ (r.succ, ι r ∘ χ ∘ π ∘ ρ <| θ s) + +def bytesOfList (l : List (Fin 2)) : List UInt8 := + l.toChunks 8 |>.map λ bits ↦ bits.zip (List.iota 8 |>.map Nat.pred) |>.foldl (init := 0) + λ acc (bit, exp) ↦ acc + (UInt8.ofNat <| bit.val * 2^exp) + +def hexOfByte (byte : UInt8) : String := + hexDigitRepr (byte.toNat >>> 4 &&& 0b00001111) ++ + hexDigitRepr (byte.toNat &&& 0b00001111) + +namespace Absorb + +partial def unfoldr {α β} (f : β → Option (α × β)) (b0 : β) : Array α := + build λ c n ↦ + let rec go b := match f b with + | .some (a, new_b) => c a <| go new_b + | .none => n + go b0 + where build g := g push_front #[] + push_front (elem : α) (arr : Array α) : Array α := ⟨elem :: arr.toList⟩ + +partial def unfoldrN {α β} (m : Nat) (f : β → Option (α × β)) (b0 : β) : Array α := + build λ c n ↦ + let rec go b i := if i == 0 then n else + match f b with + | .some (a, new_b) => c a <| go new_b (i - 1) + | .none => n + go b0 m + where build g := g push_front #[] + push_front {α} (elem : α) (arr : Array α) : Array α := ⟨elem :: arr.toList⟩ + +def ifoldl {α β : Type} (f : α → Nat → β → α) (init : α) (as : Array β) : α := + Array.range as.size |>.zip as |>.foldl (λ acc (i, elem) ↦ f acc i elem) init + +def toBlocks : ByteArray → Array UInt64 := + unfoldr toLane + where toLane (input : ByteArray) : Option (UInt64 × ByteArray) := + if input.isEmpty then .none + else let (h, t) := input.data.splitAt 8 + .some (ifoldl createWord64 0 h, ⟨t⟩) + createWord64 acc offset octet := acc ^^^ (octet.toUInt64 <<< (UInt64.ofNat offset * 8)) + +partial def absorbBlock (rate : Nat) (state : Array UInt64) (input : Array UInt64) : Array UInt64 := + if input.size == 0 then state + else -- dbg_trace s!"initial state: {state} | istream: {input}" + -- dbg_trace s!"applying keccak to: {state'} to get: {keccakF state'}" + absorbBlock rate (keccakF state') (input.drop (rate / 64)) + where state' : SHA3SR := Array.imap (λ z el ↦ if z / 5 + 5 * (z % 5) < rate / 64 + then el ^^^ (input[z / 5 + 5 * (z % 5)]!) + else el) state + +def absorb (rate : Nat) : ByteArray → Array UInt64 := absorbBlock rate ⟨List.replicate 25 0⟩ ∘ toBlocks +end Absorb + +def multiratePadding (bitrateBytes : Nat) (padByte : UInt8) (input : ByteArray) : ByteArray := + ByteArray.mk <| Array.range totalLength |>.map λ i ↦ process i + where msglen := input.size + padlen := bitrateBytes - (msglen % bitrateBytes) + totalLength := padlen + msglen + process x := if x < msglen then input[x]! else + if x == (totalLength - 1) && padlen == 1 then 0x80 ||| padByte else + if x == (totalLength - 1) then 0x80 else + if x == msglen then padByte + else 0x00 + +def byteArrayOfSHA3SR (arr : SHA3SR) : ByteArray := + arr.foldl (init := ByteArray.empty) + λ acc word ↦ + acc.push (word >>> UInt64.ofNat 56).toUInt8 + |>.push (word >>> UInt64.ofNat 48).toUInt8 + |>.push (word >>> UInt64.ofNat 40).toUInt8 + |>.push (word >>> UInt64.ofNat 32).toUInt8 + |>.push (word >>> UInt64.ofNat 24).toUInt8 + |>.push (word >>> UInt64.ofNat 16).toUInt8 + |>.push (word >>> UInt64.ofNat 8).toUInt8 + |>.push (word >>> UInt64.ofNat 0).toUInt8 + +def SHA3SRofByteArray (arr : ByteArray) : SHA3SR := + let arr : ByteArray := ⟨Array.mkArray ((8 - arr.size % 8) % 8) 0⟩ ++ arr + (·.1) <| arr.foldl (init := (#[], 0, 7)) + λ (res, word, i) byte ↦ + let byteVal : UInt64 := (2^(8 * i)).toUInt64 * byte.toUInt64 + if i == 0 + then (res.push (word + byteVal), 0, 7) + else (res, word + byteVal, i - 1) + +def paddingKeccak (bitrateBytes : Nat) : ByteArray → SHA3SR := + SHA3SRofByteArray ∘ multiratePadding bitrateBytes 0x01 + +partial def squeeze' (rate : Nat) (l : Nat) (state : SHA3SR) : ByteArray := + ByteArray.extract (b := 0) (e := l) ∘ toLittleEndian <| stateToBytes state + where lanesToExtract := Int.toNat ∘ Rat.ceil <| l / (64 / 8) + threshold := rate / 64 + extract := λ (x, s) ↦ + if x < threshold + then Option.some (s[x / 5 + x % 5 * 5]!, (x.succ, s)) + else extract (0, keccakF s) + stateToBytes (s : Array UInt64) : Array UInt64 := Absorb.unfoldrN lanesToExtract extract (0, s) + toLittleEndian (arr : Array UInt64) : ByteArray := + arr.foldl (init := ByteArray.empty) λ acc elem ↦ + let res := + acc.push (elem >>> UInt64.ofNat 0).toUInt8 + |>.push (elem >>> UInt64.ofNat 8).toUInt8 + |>.push (elem >>> UInt64.ofNat 16).toUInt8 + |>.push (elem >>> UInt64.ofNat 24).toUInt8 + |>.push (elem >>> UInt64.ofNat 32).toUInt8 + |>.push (elem >>> UInt64.ofNat 40).toUInt8 + |>.push (elem >>> UInt64.ofNat 48).toUInt8 + |>.push (elem >>> UInt64.ofNat 56).toUInt8 + res + +open Absorb + +def hashFunction (paddingFunction : Nat → ByteArray → SHA3SR) (rate : Nat) (inp : ByteArray) : ByteArray := + -- dbg_trace s!"padded result': {paddingFunction (rate / 8) $ inp}" + -- dbg_trace s!"absorbed result': {Absorb.absorb rate ∘ byteArrayOfSHA3SR ∘ paddingFunction (rate / 8) $ inp}" + squeeze' rate outputBytes ∘ Absorb.absorb rate ∘ byteArrayOfSHA3SR ∘ paddingFunction (rate / 8) $ inp + where outputBytes := (1600 - rate) / 16 + +def KEC : ByteArray → ByteArray := hashFunction paddingKeccak 1088 + +instance : Coe UInt8 (Fin (2^8)) := ⟨(·.val)⟩ +instance : Coe (Fin (2^8)) UInt8 := ⟨(⟨·⟩)⟩ +instance : Coe UInt64 (Fin (2^64)) := ⟨(·.val)⟩ +instance : Coe (Fin (2^64)) UInt64 := ⟨(⟨·⟩)⟩ + +instance : Fintype UInt64 := ⟨⟨List.finRange (2^64) |>.map UInt64.mk, sorry⟩, sorry⟩ +instance : Fintype UInt8 := ⟨⟨List.finRange (2^8) |>.map UInt8.mk, sorry⟩, sorry⟩ diff --git a/EvmYul/SpongeHash/Wheels.lean b/EvmYul/SpongeHash/Wheels.lean new file mode 100644 index 0000000..4d7d6ba --- /dev/null +++ b/EvmYul/SpongeHash/Wheels.lean @@ -0,0 +1,52 @@ +import Batteries.Data.Array.Lemmas + +import Mathlib.Tactic.Linarith + +namespace Array + +section Array + +variable {α : Type} + +def splitAt (n : Nat) (l : Array α) : Array α × Array α := + (l.extract 0 n, l.extract n l.size) + +section splitAt + +variable {l : Array α} {n : Nat} + +@[simp] +theorem splitAt_size_lt_lt : (l.splitAt n).2.size = l.size - n := by simp [splitAt] + +end splitAt + +def take (n : Nat) (l : Array α) : Array α := l.extract 0 n + +section take + +variable {l : Array α} {n : Nat} + +theorem size_take_of_le (h : n ≤ l.size) : (l.take n).size = n := by simp [take]; linarith + +@[simp] +theorem splitAt_1_eq_take : (l.splitAt n).1 = l.take n := by simp [take, splitAt] + +end take + +def drop (n : Nat) (l : Array α) : Array α := l.extract n l.size + +section drop + +variable {l : Array α} {n : Nat} {i : Nat} + +@[simp] +theorem size_drop : (l.drop i).size = l.size - i := by simp [drop] + +@[simp] +theorem splitAt_2_eq_drop : (l.splitAt n).2 = l.drop n := by simp [drop, splitAt] + +end drop + +end Array + +end Array diff --git a/EvmYul/State.lean b/EvmYul/State.lean new file mode 100644 index 0000000..e3b893b --- /dev/null +++ b/EvmYul/State.lean @@ -0,0 +1,38 @@ +import Mathlib.Data.Finmap +import Mathlib.Data.Finset.Basic + +import EvmYul.State.ExecutionEnv +import EvmYul.State.Substate +import EvmYul.State.Account +import EvmYul.State.Block + +import EvmYul.UInt256 +import EvmYul.Wheels + +namespace EvmYul + +/-- +The `State`. Section 9.3. + +- `accountMap` `σ` +- `substate` `A` +- `executionEnv` `I` +- `remainingGas` `g` +-/ +structure State where + accountMap : Finmap (λ _ : Address ↦ Account) + remainingGas : ℕ + substate : Substate + executionEnv : ExecutionEnv + + -- Instead of keeping a map from `parentHash` to `Block`, we instead store the blocks we need. + blocks : List Block + + -- TODO(Keccak Stuff) + keccakMap : Finmap (λ _ : List UInt256 ↦ UInt256) + keccakRange : List UInt256 + usedRange : Finset UInt256 + hashCollision : Bool +deriving DecidableEq, Inhabited + +end EvmYul diff --git a/EvmYul/State/Account.lean b/EvmYul/State/Account.lean new file mode 100644 index 0000000..025e9c5 --- /dev/null +++ b/EvmYul/State/Account.lean @@ -0,0 +1,31 @@ +import Mathlib.Data.Finmap +import EvmYul.UInt256 +import EvmYul.Wheels + +namespace EvmYul + +/-- +The `Account` data. Section 4.1. + +Suppose `a` is some address. + +- `nonce` -- σ[a]ₙ. +- `balance` -- σ[a]_b. + +In the yellow paper it is supposed to be a 256-bit hash of the root node of +a Merkle Tree. KEVM implemets it as just an key/value map. +- `storage` -- σ[a]_s. +- `codeHash` -- σ[a]_c. + +For now, we assume no global map `GM` with which `GM[code_hash] ≡ code`. +- `code` +-/ +structure Account := + nonce : UInt256 + balance : UInt256 + code : ByteArray + codeHash : UInt256 -- TODO - Probably not needed. + storage : Storage +deriving DecidableEq, Inhabited + +end EvmYul diff --git a/EvmYul/State/AccountOps.lean b/EvmYul/State/AccountOps.lean new file mode 100644 index 0000000..eb4dd9c --- /dev/null +++ b/EvmYul/State/AccountOps.lean @@ -0,0 +1,40 @@ +import EvmYul.State.Account + +namespace EvmYul + +namespace Account + +def lookupStorage (self : Account) (k : UInt256) : UInt256 := + self.storage.lookup k |>.getD 0 + +def updateStorage (self : Account) (k v : UInt256) : Account := + { self with storage := self.storage.insert k v } + +/-- +EMPTY(σ, a). Section 4.1., equation 14. +-/ +def emptyAccount (self : Account) : Bool := + self.code.isEmpty ∧ self.nonce = 0 ∧ self.balance = 0 + +def transferBalanceTo (self : Account) (balance : UInt256) (recipient : Account) : Option (Account × Account) := + let underflow : Bool := self.balance < balance + let overflow : Bool := recipient.balance + balance < recipient.balance + if underflow || overflow then .none + else .some ( + {self with balance := self.balance - balance}, + {recipient with balance := recipient.balance + balance} + ) + +def addBalance (self : Account) (balance : UInt256) : Option Account := + let overflow : Bool := self.balance + balance < self.balance + if overflow then .none + else .some { self with balance := self.balance + balance } + +def subBalance (self : Account) (balance : UInt256) : Option Account := + let underflow : Bool := self.balance < balance + if underflow then .none + else .some { self with balance := self.balance - balance } + +end Account + +end EvmYul diff --git a/EvmYul/State/Block.lean b/EvmYul/State/Block.lean new file mode 100644 index 0000000..e9e4a59 --- /dev/null +++ b/EvmYul/State/Block.lean @@ -0,0 +1,22 @@ +import Mathlib.Data.Finset.Basic + +import EvmYul.State.BlockHeader +import EvmYul.State.Transaction + +namespace EvmYul + +/-- +`Block`. `B`. Section 4.3. +`blockHeader` `H` +`transactions` `T` +`ommers` `U` [deprecated] +-/ +structure Block where + blockHeader : BlockHeader + transactions : List Transaction + ommers : Finset BlockHeader := ∅ + deriving Inhabited, DecidableEq + +attribute [deprecated] Block.ommers + +end EvmYul diff --git a/EvmYul/State/BlockHeader.lean b/EvmYul/State/BlockHeader.lean new file mode 100644 index 0000000..70aaf1e --- /dev/null +++ b/EvmYul/State/BlockHeader.lean @@ -0,0 +1,51 @@ +import EvmYul.UInt256 +import EvmYul.Wheels + +namespace EvmYul + +/-- +`BlockHeader`. `H_`. Section 4.3. + +`parentHash` `p` +`ommersHash` `o` +`beneficiary` `c` +`stateRoot` `r` +`transRoot` `t` +`receiptRoot` `e` +`logsBloom` `b` +`difficulty` `d` [deprecated] +`number` `i` +`gasLimit` `l` +`gasUsed` `g` +`timestamp` `s` +`extraData` `x` +`minHash` `m` +`chainId` `n` TODO ???? +`nonce` `n` [deprecated] +`baseFeePerGas` `f` +-/ +structure BlockHeader where + parentHash : UInt256 + ommersHash : UInt256 + beneficiary : Address + stateRoot : UInt256 + transRoot : UInt256 + receiptRoot : UInt256 + logsBloom : ByteArray + difficulty : ℕ + number : ℕ + gasLimit : ℕ + gasUsed : ℕ + timestamp : ℕ + extraData : ByteArray + minHash : UInt256 + chainId : UInt256 -- TODO(Why is this here?) + nonce : UInt64 + -- prevRandao -- TODO + baseFeePerGas : ℕ +deriving DecidableEq, Inhabited + +attribute [deprecated] BlockHeader.difficulty +attribute [deprecated] BlockHeader.nonce + +end EvmYul diff --git a/EvmYul/State/ExecutionEnv.lean b/EvmYul/State/ExecutionEnv.lean new file mode 100644 index 0000000..f0b043e --- /dev/null +++ b/EvmYul/State/ExecutionEnv.lean @@ -0,0 +1,33 @@ +import EvmYul.Wheels +import EvmYul.UInt256 +import EvmYul.State.BlockHeader + +namespace EvmYul + +/-- +The execution envorinment `I` `ExecutionEnv`. Section 9.3. +- `codeOwner` `Iₐ` +- `sender` `I₀` +- `source` `Iₛ` +- `weiValue` `Iᵥ` +- `inputData` `I_d` +- `code` `I_b` +- `gasPrice` `Iₚ` +- `header` `I_H` +- `depth` `Iₑ` +- `perm` `I_w` +-/ +structure ExecutionEnv := + codeOwner : Address + sender : Address + source : Address + weiValue : UInt256 + inputData : ByteArray + code : ByteArray + gasPrice : ℕ + header : BlockHeader + depth : ℕ + perm : Bool + deriving DecidableEq, Inhabited + +end EvmYul diff --git a/EvmYul/State/Substate.lean b/EvmYul/State/Substate.lean new file mode 100644 index 0000000..9173db6 --- /dev/null +++ b/EvmYul/State/Substate.lean @@ -0,0 +1,26 @@ +import Mathlib.Data.Finset.Basic +import EvmYul.UInt256 +import EvmYul.Wheels +import EvmYul.State.Account + +namespace EvmYul + +/-- +The `Substate` `A`. Section 6.1. +- `selfDestructSet` `Aₛ` +- `touchedAccounts` `Aₜ` +- `refundBalance` `Aᵣ` +- `accessedAccounts` `Aₐ` +- `accessedStorageKey` `Aₖ` +- `logSeries` `Aₗ` +-/ +structure Substate := + selfDestructSet : Finset Address + touchedAccounts : Finset Account + refundBalance : UInt256 + accessedAccounts : Finset Address + accessedStorageKeys : Finset (Address × UInt256) + logSeries : Array (Address × List UInt256 × ByteArray) + deriving DecidableEq, Inhabited + +end EvmYul diff --git a/EvmYul/State/SubstateOps.lean b/EvmYul/State/SubstateOps.lean new file mode 100644 index 0000000..79a20eb --- /dev/null +++ b/EvmYul/State/SubstateOps.lean @@ -0,0 +1,15 @@ +import EvmYul.State.Substate + +namespace EvmYul + +namespace Substate + +def addAccessedAccount (self : Substate) (addr : Address) : Substate := + { self with accessedAccounts := {addr} ∪ self.accessedAccounts } + +def addAccessedStorageKey (self : Substate) (sk : Address × UInt256) : Substate := + { self with accessedStorageKeys := {sk} ∪ self.accessedStorageKeys } + +end Substate + +end EvmYul diff --git a/EvmYul/State/Transaction.lean b/EvmYul/State/Transaction.lean new file mode 100644 index 0000000..890cce3 --- /dev/null +++ b/EvmYul/State/Transaction.lean @@ -0,0 +1,88 @@ +import Mathlib.Data.List.AList + +import EvmYul.UInt256 +import EvmYul.Wheels + +namespace EvmYul + +/-- +`BaseTransaction`. `T`. Section 4.3. + +`nonce` `x` +`gasLimit` `a` +`recipinet` `g` +`value` `t` +`r` `s` +`s` `r` +`data` `d/i` +TODO: In case of recipient = none, it means contract creation and data should be treated as init? +-/ +structure BaseTransaction where + nonce : UInt256 + gasLimit : UInt256 + recipient : Option Address + value : UInt256 + r : ByteArray + s : ByteArray + data : ByteArray + deriving DecidableEq + +/-- +`WithGasPriceTransaction`. `T`. Section 4.3. +`gasPrice` `p` +-/ +structure WithGasPriceTransaction extends BaseTransaction where + gasPrice : UInt256 + deriving DecidableEq + +/-- +`LegacyTransaction`. `T`. Section 4.3. +`w` `w` +-/ +structure LegacyTransaction extends WithGasPriceTransaction where + w: UInt256 + deriving DecidableEq +/-- +`LegacyProtectedTransaction`. `T`. Section 4.3. +`chainId` `c` +-/ +structure LegacyProtectedTransaction extends LegacyTransaction where + chainId : ℕ + +/-- +`AccessListTransaction`. `T`. EIP-2930. +`chainId` `c` +`accessList` `A` +-/ +structure AccessListTransaction extends WithGasPriceTransaction where + chainId : ChainID + accessList : AList (λ _ : Address ↦ List UInt256) + deriving DecidableEq + +/-- +`DynamicFeeTransaction`. `T`. EIP-1559. + +`priorityGasFee` +`maxGasFee` +`chainId` `c` +`accessList` `A` +-/ +structure DynamicFeeTransaction extends BaseTransaction where + priorityGasFee : UInt256 + maxGasFee : UInt256 + chainId : ChainID + accessList : AList (λ _ : Address ↦ List UInt256) + deriving DecidableEq + +inductive Transaction where + | legacy : LegacyTransaction → Transaction + | access : AccessListTransaction → Transaction + | dynamic : DynamicFeeTransaction → Transaction + deriving DecidableEq + +def Transaction.type : Transaction → Nat + | .legacy _ => 0 + | .access _ => 1 + | .dynamic _ => 2 + +end EvmYul diff --git a/EvmYul/StateOps.lean b/EvmYul/StateOps.lean new file mode 100644 index 0000000..7e5040d --- /dev/null +++ b/EvmYul/StateOps.lean @@ -0,0 +1,154 @@ +import EvmYul.State.SubstateOps +import EvmYul.State.AccountOps + +import EvmYul.State + +namespace EvmYul + +namespace State + +def addAccessedAccount (self : State) (addr : Address) : State := + { self with substate := self.substate.addAccessedAccount addr } + +def addAccessedStorageKey (self : State) (sk : Address × UInt256) : State := + { self with substate := self.substate.addAccessedStorageKey sk } + +/-- +DEAD(σ, a). Section 4.1., equation 15. +-/ +def dead (s : State) (addr : Address) : Bool := + s.accountMap.lookup addr |>.option True Account.emptyAccount + +def addHashCollision (self : State) : State := { self with hashCollision := true } + +def accountExists (self : State) (addr : Address) : Bool := self.accountMap.lookup addr |>.isSome + +def lookupAccount (self : State) (addr : Address) : Option Account := + self.accountMap.lookup addr + +def updateAccount (addr : Address) (act : Account) (self : State) : State := + { self with accountMap := self.accountMap.insert addr act } +def setAccount (self : State) (addr : Address) (acc : Account) : State := + { self with accountMap := self.accountMap.insert addr acc } + +def setSelfAccount (self : State) (acc : Account := default) : State := + self.setAccount self.executionEnv.codeOwner acc + +def updateAccount! (self : State) (addr : Address) (f : Account → Account) : State := + let acc! := self.lookupAccount addr |>.getD default + self.setAccount addr (f acc!) + +def updateSelfAccount! (self : State) : (Account → Account) → State := + self.updateAccount! self.executionEnv.codeOwner + +def balance (self : State) (k : UInt256) : State × UInt256 := + let addr := Address.ofUInt256 k + (self.addAccessedAccount addr, self.accountMap.lookup addr |>.option 0 Account.balance) + +def transferBalance (sender : Address) (recipient : Address) (balance : UInt256) (self : State) : Option State := + if sender == recipient then .some self -- NB this check renders `balance` validity irrelevant + else do + let senderAcc ← self.accountMap.lookup sender + let recipientAcc ← self.accountMap.lookup recipient + let (senderAcc, recipientAcc) ← senderAcc.transferBalanceTo balance recipientAcc + self.updateAccount sender senderAcc + |>.updateAccount recipient recipientAcc + +def initialiseAccount (addr : Address) (self : State) : State := + if self.accountExists addr then self else self.updateAccount addr default +def setBalance! (self : State) (addr : Address) (balance : UInt256) : State := + self.updateAccount! addr (λ acc ↦ { acc with balance := balance }) + +def setSelfBalance! (self : State) : UInt256 → State := + self.setBalance! self.executionEnv.codeOwner + +def calldataload (self : State) (v : UInt256) : UInt256 := + uInt256OfByteArray <| self.executionEnv.inputData.extract v (v + 32) + +def setNonce! (self : State) (addr : Address) (nonce : UInt256) : State := + self.updateAccount! addr (λ acc ↦ { acc with nonce := nonce }) + +def setSelfNonce! (self : State) (nonce : UInt256) : State := + self.setNonce! self.executionEnv.codeOwner nonce + +def selfStorage! (self : State) : Finmap (λ _ : UInt256 ↦ UInt256) := + self.lookupAccount self.executionEnv.codeOwner |>.getD default |>.storage + +section CodeCopy + +def extCodeSize (self : State) (a : UInt256) : State × UInt256 := + let addr := Address.ofUInt256 a + let s := self.lookupAccount addr |>.option 0 (Fin.ofNat ∘ ByteArray.size ∘ Account.code) + (self.addAccessedAccount addr, s) + +def extCodeHash (self : State) (v : UInt256) : UInt256 := + self.lookupAccount (Address.ofUInt256 v) |>.option 0 Account.codeHash + +end CodeCopy + +section Blocks + +def blockHash (self : State) (blockNumber : UInt256) : UInt256 := + let v := self.executionEnv.header.number + if v ≤ blockNumber || blockNumber + 256 < v then 0 + else + let bs := self.blocks.map λ b ↦ b.blockHeader.parentHash + bs.getD (v - blockNumber) 0 + +def coinBase (self : State) : Address := + self.executionEnv.header.beneficiary + +def timeStamp (self : State) : UInt256 := + self.executionEnv.header.timestamp + +def number (self : State) : UInt256 := + self.executionEnv.header.number + +def difficulty (self : State) : UInt256 := + self.executionEnv.header.difficulty + +def gasLimit (self : State) : UInt256 := + self.executionEnv.header.gasLimit + +def chainId (self : State) : UInt256 := + self.executionEnv.header.chainId + +def selfbalance (self : State) : UInt256 := + Finmap.lookup self.executionEnv.codeOwner self.accountMap |>.option 0 Account.balance + +/-- +TODO: `Account` also has `code`. Recheck. +-/ +def setCode (self : State) (code : ByteArray) : State := + { self with executionEnv.code := code } + +end Blocks + +section Storage + +def setStorage! (self : State) (addr : Address) (strg : Finmap (λ _ : UInt256 ↦ UInt256)) : State := + self.updateAccount! addr (λ acc ↦ { acc with storage := strg }) + +def setSelfStorage! (self : State) : Finmap (λ _ : UInt256 ↦ UInt256) → State := + self.setStorage! self.executionEnv.codeOwner + +def sload (self : State) (spos : UInt256) : State × UInt256 := + let Iₐ := self.executionEnv.codeOwner + let v := self.lookupAccount Iₐ |>.option 0 (Account.lookupStorage (k := spos)) + let state' := self.addAccessedStorageKey (Iₐ, spos) + (state', v) + +def sstore (self : State) (spos sval : UInt256) : State := + let Iₐ := self.executionEnv.codeOwner + self.lookupAccount Iₐ |>.option self λ acc ↦ + let self' := self.setAccount Iₐ (acc.updateStorage spos sval) + { self' with + usedRange := {spos} ∪ self'.usedRange -- not sure what this is + substate := self.substate.addAccessedStorageKey (Iₐ, spos) + } + +end Storage + +end State + +end EvmYul diff --git a/EvmYul/UInt256.lean b/EvmYul/UInt256.lean new file mode 100644 index 0000000..082c56c --- /dev/null +++ b/EvmYul/UInt256.lean @@ -0,0 +1,346 @@ +import Init.Data.Nat.Div +import Mathlib.Data.Nat.Defs +import Mathlib.Data.Fin.Basic +import Mathlib.Data.Vector.Basic +import Mathlib.Algebra.Group.Defs +import Mathlib.Algebra.GroupWithZero.Defs +import Mathlib.Algebra.Ring.Basic +import Mathlib.Algebra.Order.Floor +import Mathlib.Data.ZMod.Defs +import Mathlib.Tactic.Ring + +namespace EvmYul + +open Std + +def UInt256.size : ℕ := 115792089237316195423570985008687907853269984665640564039457584007913129639936 + +instance : NeZero UInt256.size := ⟨by decide⟩ + +abbrev UInt256 := Fin UInt256.size + +instance : SizeOf UInt256 where sizeOf := 1 + +namespace UInt256 + +def ofNat (n : ℕ) : UInt256 := Fin.ofNat n +instance {n : ℕ} : OfNat UInt256 n := ⟨UInt256.ofNat n⟩ +instance : Inhabited UInt256 := ⟨0⟩ + +end UInt256 + +end EvmYul + +section CastUtils + +open EvmYul UInt256 + +abbrev Nat.toUInt256 : ℕ → UInt256 := ofNat +abbrev UInt8.toUInt256 (a : UInt8) : UInt256 := ⟨a.1, Nat.lt_trans a.1.2 (by decide)⟩ +def Bool.toUInt256 (b : Bool) : UInt256 := if b then 1 else 0 + +@[simp] +lemma Bool.toUInt256_true : true.toUInt256 = 1 := rfl + +@[simp] +lemma Bool.toUInt256_false : false.toUInt256 = 0 := rfl + +end CastUtils + +namespace EvmYul + +namespace UInt256 + +def add (a b : UInt256) : UInt256 := a.1 + b.1 +def sub (a b : UInt256) : UInt256 := a.1 - b.1 +def mul (a b : UInt256) : UInt256 := a.1 * b.1 +def div (a b : UInt256) : UInt256 := a.1 / b.1 +def mod (a b : UInt256) : UInt256 := a.1 % b.1 +def modn (a : UInt256) (n : ℕ) : UInt256 := Fin.modn a.1 n +def land (a b : UInt256) : UInt256 := Fin.land a.1 b.1 +def lor (a b : UInt256) : UInt256 := Fin.lor a.1 b.1 +def xor (a b : UInt256) : UInt256 := Fin.xor a.1 b.1 +def shiftLeft (a b : UInt256) : UInt256 := a.1 <<< (modn b 256).1 +def shiftRight (a b : UInt256) : UInt256 := a.1 >>> (modn b 256).1 +-- def lt (a b : UInt256) : Prop := a.1 < b.1 +-- def le (a b : UInt256) : Prop := a.1 ≤ b.1 +def log2 (a : UInt256) : UInt256 := Fin.log2 a.1 +def floor (a : UInt256) : UInt256 := Fin.ofNat (Nat.floor a.1) + +instance : Add UInt256 := ⟨UInt256.add⟩ +instance : Sub UInt256 := ⟨UInt256.sub⟩ +instance : Mul UInt256 := ⟨UInt256.mul⟩ +instance : Div UInt256 := ⟨UInt256.div⟩ +instance : Mod UInt256 := ⟨UInt256.mod⟩ +instance : HMod UInt256 ℕ UInt256 := ⟨UInt256.modn⟩ +-- instance : LT UInt256 := ⟨UInt256.lt⟩ +-- instance : LE UInt256 := ⟨UInt256.le⟩ + +def complement (a : UInt256) : UInt256 := 0-(a + 1) + +instance : Complement UInt256 := ⟨EvmYul.UInt256.complement⟩ +instance : HPow UInt256 UInt256 UInt256 where + hPow a n := a ^ n.val +instance : AndOp UInt256 := ⟨UInt256.land⟩ +instance : OrOp UInt256 := ⟨UInt256.lor⟩ +instance : Xor UInt256 := ⟨UInt256.xor⟩ +instance : ShiftLeft UInt256 := ⟨UInt256.shiftLeft⟩ +instance : ShiftRight UInt256 := ⟨UInt256.shiftRight⟩ +instance : DecidableEq UInt256 := decEq + +def decLt (a b : UInt256) : Decidable (a < b) := + match a, b with + | n, m => inferInstanceAs (Decidable (n < m)) + +def decLe (a b : UInt256) : Decidable (a ≤ b) := + match a, b with + | n, m => inferInstanceAs (Decidable (n <= m)) + +instance (a b : UInt256) : Decidable (a < b) := decLt _ _ +instance (a b : UInt256) : Decidable (a ≤ b) := UInt256.decLe a b +instance : Max UInt256 := maxOfLe +instance : Min UInt256 := minOfLe + +def toNat (n : UInt256) : ℕ := n.1 +def eq0 (a : UInt256) : Bool := a = 0 +def lnot (a : UInt256) : UInt256 := (UInt256.size - 1) - a + +def byteAt (a b : UInt256) : UInt256 := + b >>> (UInt256.ofNat ((31 - a.toNat) * 8)) &&& 0xFF + +def sgn (a : UInt256) : UInt256 := + if 2 ^ 255 <= a + then -1 + else + if a = 0 + then 0 + else 1 + +def abs (a : UInt256) : UInt256 := + if 2 ^ 255 <= a + then a * -1 + else a + +def sdiv (a b : UInt256) : UInt256 := + if 2 ^ 255 <= a then + if 2 ^ 255 <= b then + abs a / abs b + else (abs a / b) * -1 + else + if 2 ^ 255 <= b then + (a / abs b) * -1 + else a / b + +def smod (a b : UInt256) : UInt256 := + if 2 ^ 255 <= a + then if 2 ^ 255 <= b + then (abs a) % (abs b) + else -1 * (abs a) % b + else if 2 ^ 255 <= b + then -1 * a % (abs b) + else a % b + +def sltBool (a b : UInt256) : Bool := + if a ≥ 2 ^ 255 then + if b ≥ 2 ^ 255 then + a < b + else true + else + if b ≥ 2 ^ 255 then false + else a < b + +def sgtBool (a b : UInt256) : Bool := + if a ≥ 2 ^ 255 then + if b ≥ 2 ^ 255 then + a > b + else false + else + if b ≥ 2 ^ 255 then true + else a > b + +abbrev fromBool := Bool.toUInt256 + +def slt (a b : UInt256) := + fromBool (sltBool a b) + +def sgt (a b : UInt256) := + fromBool (sgtBool a b) + +def sar (a b : UInt256) : UInt256 := + if sltBool a 0 + then UInt256.complement (UInt256.complement a >>> b) + else a >>> b + +private partial def dbg_toHex (n : Nat) : String := + if n < 16 + then hexDigitRepr n + else (dbg_toHex (n / 16)) ++ hexDigitRepr (n % 16) + +def signextend (a b : UInt256) : UInt256 := + if a ≤ 31 then + let test_bit := a * 8 + 7 + let sign_bit := 1 <<< test_bit + if b &&& sign_bit ≠ 0 then + b ||| (UInt256.size.toUInt256 - sign_bit) + else b &&& (sign_bit - 1) + else b + +def addMod (a b c : UInt256) : UInt256 := + if c = 0 then 0 else + Fin.mod (a + b) c + +def mulMod (a b c : UInt256) : UInt256 := + if c = 0 then 0 else + Fin.mod (a * b) c + +def exp (a b : UInt256) : UInt256 := + a ^ b.val + +def lt (a b : UInt256) := + fromBool (a < b) + +def gt (a b : UInt256) := + fromBool (a > b) + +def eq (a b : UInt256) := + fromBool (a = b) + +def isZero (a : UInt256) := + fromBool (a = 0) + +end UInt256 + +-- | Convert from a list of little-endian bytes to a natural number. +def fromBytes' : List UInt8 → ℕ +| [] => 0 +| b :: bs => b.val.val + 2^8 * fromBytes' bs + +def fromBytesBigEndian : List UInt8 → ℕ := fromBytes' ∘ List.reverse + +variable {bs : List UInt8} + {n : ℕ} + +-- | A bound for the natural number value of a list of bytes. +private lemma fromBytes'_le : fromBytes' bs < 2^(8 * bs.length) := by + induction bs with + | nil => unfold fromBytes'; simp + | cons b bs ih => + unfold fromBytes' + have h := b.val.isLt + simp only [List.length_cons, Nat.mul_succ, Nat.add_comm, Nat.pow_add] + have _ := + Nat.add_le_of_le_sub + (Nat.one_le_pow _ _ (by decide)) + (Nat.le_sub_one_of_lt ih) + linarith + +-- | The natural number value of a length 32 list of bytes is < 2^256. +private lemma fromBytes'_UInt256_le (h : bs.length = 32) : fromBytes' bs < 2^256 := by + have h' := @fromBytes'_le bs + rw [h] at h' + exact h' + +-- | Convert a natural number into a list of bytes. +private def toBytes' : ℕ → List UInt8 + | 0 => [] + | n@(.succ n') => + let byte : UInt8 := ⟨Nat.mod n UInt8.size, Nat.mod_lt _ (by linarith)⟩ + have : n / UInt8.size < n' + 1 := by + rename_i h + rw [h] + apply Nat.div_lt_self <;> simp + byte :: toBytes' (n / UInt8.size) + +def toBytesBigEndian : ℕ → List UInt8 := List.reverse ∘ toBytes' + +-- | If n < 2⁸ᵏ, then (toBytes' n).length ≤ k. +private lemma toBytes'_le {k : ℕ} (h : n < 2 ^ (8 * k)) : (toBytes' n).length ≤ k := by + induction k generalizing n with + | zero => + simp at h + rw [h] + simp [toBytes'] + | succ e ih => + match n with + | .zero => simp [toBytes'] + | .succ n => + unfold toBytes' + simp [Nat.succ_le_succ_iff] + apply ih (Nat.div_lt_of_lt_mul _) + rw [Nat.mul_succ, Nat.pow_add] at h + linarith + +-- | If n < 2²⁵⁶, then (toBytes' n).length ≤ 32. +private lemma toBytes'_UInt256_le (h : n < UInt256.size) : (toBytes' n).length ≤ 32 := toBytes'_le h + +-- | Zero-pad a list of bytes up to some length, adding the zeroes on the right. +private def zeroPadBytes (n : ℕ) (bs : List UInt8) : List UInt8 := + bs ++ (List.replicate (n - bs.length)) 0 + +-- | The length of a `zeroPadBytes` call is its first argument. +lemma zeroPadBytes_len (h : bs.length ≤ n) : (zeroPadBytes n bs).length = n := by + unfold zeroPadBytes + aesop + +-- | Appending a bunch of zeroes to a little-endian list of bytes doesn't change its value. +@[simp] +private lemma extend_bytes_zero : fromBytes' (bs ++ List.replicate n 0) = fromBytes' bs := by + induction bs with + | nil => + simp [fromBytes'] + induction n with + | zero => simp [List.replicate, fromBytes'] + | succ _ ih => simp [List.replicate, fromBytes']; norm_cast + | cons _ _ ih => simp [fromBytes', ih] + +-- | The ℕ value of a little-endian list of bytes is invariant under right zero-padding up to length 32. +@[simp] +private lemma fromBytes'_zeroPadBytes_32_eq : fromBytes' (zeroPadBytes 32 bs) = fromBytes' bs := extend_bytes_zero + +-- | Casting a natural number to a list of bytes and back is the identity. +@[simp] +private lemma fromBytes'_toBytes' {x : ℕ} : fromBytes' (toBytes' x) = x := by + match x with + | .zero => simp [toBytes', fromBytes'] + | .succ n => + unfold toBytes' fromBytes' + simp only + have := Nat.div_lt_self (Nat.zero_lt_succ n) (by decide : 1 < UInt8.size) + rw [fromBytes'_toBytes'] + simp [UInt8.size, add_comm] + apply Nat.div_add_mod + +def fromBytes! (bs : List UInt8) : ℕ := fromBytes' (bs.take 32) + +private lemma fromBytes_was_good_all_year_long + (h : bs.length ≤ 32) : fromBytes' bs < 2^256 := by + have h' := @fromBytes'_le bs + rw [pow_mul] at h' + refine lt_of_lt_of_le (b := (2 ^ 8) ^ List.length bs) h' ?lenBs + case lenBs => rw [←pow_mul]; exact pow_le_pow_right (by decide) (by linarith) + +@[simp] +lemma fromBytes_wasnt_naughty : fromBytes! bs < 2^256 := fromBytes_was_good_all_year_long (by simp) + +-- Convenience function for spooning into UInt256. +-- Given that I 'accept' UInt8, might as well live with UInt256. +def fromBytes_if_you_really_must? (bs : List UInt8) : UInt256 := + ⟨fromBytes! bs, fromBytes_wasnt_naughty⟩ + +def toBytes! (n : UInt256) : List UInt8 := zeroPadBytes 32 (toBytes' n.1) + +@[simp] +lemma length_toBytes! {n : UInt256} : (toBytes! n).length = 32 := zeroPadBytes_len (toBytes'_UInt256_le n.2) + +def uInt256OfByteArray' (arr : ByteArray) : UInt256 := Id.run do + let mut acc : ℕ := 0 + let mut exp : ℕ := arr.size - 1 + for byte in arr do + acc := acc + byte.toNat * 2 ^ (8 * exp) + exp := exp - 1 + return acc + +def uInt256OfByteArray (arr : ByteArray) : UInt256 := + fromBytes' arr.data.toList.reverse + +end EvmYul diff --git a/EvmYul/Wheels.lean b/EvmYul/Wheels.lean new file mode 100644 index 0000000..4d36337 --- /dev/null +++ b/EvmYul/Wheels.lean @@ -0,0 +1,96 @@ +import EvmYul.UInt256 + +import Mathlib.Data.Finmap + +namespace EvmYul + +abbrev Literal := UInt256 + +-- 2^160 https://www.wolframalpha.com/input?i=2%5E160 +def Address.size : Nat := 1461501637330902918203684832716283019655932542976 + +abbrev Address : Type := Fin Address.size + +abbrev Storage : Type := Finmap (λ _ : UInt256 ↦ UInt256) + +instance : Inhabited Address := ⟨Fin.ofNat 0⟩ + +namespace Address + +def ofNat {n : ℕ} : Address := Fin.ofNat n +def ofUInt256 (v : UInt256) : Address := Fin.ofNat (v.val % Address.size) +instance {n : Nat} : OfNat Address n := ⟨Fin.ofNat n⟩ + +end Address + +/-- + Is an enumerate type, but nat is okay for now TODO(model properly) +-/ +def ChainID : Type := Nat + +deriving instance DecidableEq for ChainID +deriving instance Inhabited for ChainID + +def Identifier := String +instance : ToString Identifier := inferInstanceAs (ToString String) +instance : Inhabited Identifier := inferInstanceAs (Inhabited String) +instance : DecidableEq Identifier := inferInstanceAs (DecidableEq String) +instance : Repr Identifier := inferInstanceAs (Repr String) + +namespace NaryNotation + +scoped syntax "!nary[" ident "^" num "]" : term + +open Lean in +scoped macro_rules + | `(!nary[ $idn:ident ^ $nat:num ]) => + let rec go (n : ℕ) : MacroM Term := + match n with + | 0 => `($idn) + | n + 1 => do `($idn → $(←go n)) + go nat.getNat + +end NaryNotation + +namespace Primop + +section + +open NaryNotation + +def Nullary := !nary[UInt256 ^ 0] +def Unary := !nary[UInt256 ^ 1] +def Binary := !nary[UInt256 ^ 2] +def Ternary := !nary[UInt256 ^ 3] +def Quaternary := !nary[UInt256 ^ 4] + +end + +end Primop + +end EvmYul + +/-- +TODO(rework later to a sane version) +-/ +instance : DecidableEq ByteArray := by + rintro ⟨a⟩ ⟨b⟩ + rw [ByteArray.mk.injEq] + apply decEq + +def Option.option {α β : Type} (dflt : β) (f : α -> β) : Option α → β + | .none => dflt + | .some x => f x + +def Option.toExceptWith {α β : Type} (dflt : β) (x : Option α) : Except β α := + x.option (.error dflt) Except.ok + +def ByteArray.get? (self : ByteArray) (n : Nat) : Option UInt8 := + if h : n < self.size + then self.get ⟨n, h⟩ + else .none + +partial def Nat.toHex (n : Nat) : String := + if n < 16 + then hexDigitRepr n + else (toHex (n / 16)) ++ hexDigitRepr (n % 16) diff --git a/EvmYul/Yul/Ast.lean b/EvmYul/Yul/Ast.lean new file mode 100644 index 0000000..39c14cb --- /dev/null +++ b/EvmYul/Yul/Ast.lean @@ -0,0 +1,81 @@ +/- Yul specification: +https://docs.soliditylang.org/en/v0.8.9/yul.html +-/ + +import EvmYul.UInt256 +import EvmYul.Operations +import EvmYul.Wheels + +namespace EvmYul + +namespace Yul + +namespace Ast + +open EvmYul UInt256 + +abbrev Literal := UInt256 +-- def Identifier := String + +instance : ToString Identifier := inferInstanceAs (ToString String) + +instance : Inhabited Identifier := ⟨""⟩ +instance : DecidableEq Identifier := String.decEq + +abbrev PrimOp := Operation .Yul + +def stringOfPrimOp : PrimOp → String := toString ∘ repr + +instance : ToString PrimOp := ⟨stringOfPrimOp⟩ + +-- https://docs.soliditylang.org/en/latest/yul.html#informal-description-of-yul + +mutual + inductive FunctionDefinition where + | Def : List Identifier → List Identifier → List Stmt → FunctionDefinition + + inductive Expr where + | PrimCall : PrimOp → List Expr → Expr + | Call : FunctionDefinition → List Expr → Expr + | Var : Identifier → Expr + | Lit : Literal → Expr + + -- | The loop constructor 'Stmt.For' has no initialiser because of + -- https://docs.soliditylang.org/en/latest/internals/optimizer.html#forloopinitrewriter + inductive Stmt where + | Block : List Stmt → Stmt + | Let : List Identifier → Stmt + | LetEq : Identifier → Expr → Stmt + | LetCall : List Identifier → FunctionDefinition → List Expr → Stmt + | LetPrimCall : List Identifier → PrimOp → List Expr → Stmt + | Assign : Identifier → Expr → Stmt + | AssignCall : List Identifier → FunctionDefinition → List Expr → Stmt + | AssignPrimCall : List Identifier → PrimOp → List Expr → Stmt + | ExprStmtCall : FunctionDefinition → List Expr -> Stmt + | ExprStmtPrimCall : PrimOp → List Expr -> Stmt + | Switch : Expr → List (Literal × List Stmt) → List Stmt → Stmt + | For : Expr → List Stmt → List Stmt → Stmt + | If : Expr → List Stmt → Stmt + | Continue : Stmt + | Break : Stmt + | Leave : Stmt +end + +namespace FunctionDefinition + +def params : FunctionDefinition → List Identifier + | Def params _ _ => params + +def rets : FunctionDefinition → List Identifier + | Def _ rets _ => rets + +def body : FunctionDefinition → List Stmt + | Def _ _ body => body + +end FunctionDefinition + +end Ast + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/Exception.lean b/EvmYul/Yul/Exception.lean new file mode 100644 index 0000000..b548473 --- /dev/null +++ b/EvmYul/Yul/Exception.lean @@ -0,0 +1,13 @@ +namespace EvmYul + +namespace Yul + +inductive Exception where + | InvalidArguments : Exception + | NotEncodableRLP : Exception + | InvalidInstruction : Exception + | StopInvoked : Exception + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/Interpreter.lean b/EvmYul/Yul/Interpreter.lean new file mode 100644 index 0000000..cd27e33 --- /dev/null +++ b/EvmYul/Yul/Interpreter.lean @@ -0,0 +1,228 @@ +import Mathlib.Data.Finmap +import Mathlib.Init.Data.List.Lemmas + +import EvmYul.Yul.Ast +import EvmYul.Yul.State +import EvmYul.Yul.PrimOps +import EvmYul.Yul.StateOps +import EvmYul.Yul.SizeLemmas +import EvmYul.Yul.Exception + +import EvmYul.Semantics + +namespace EvmYul + +namespace Yul + +open Ast SizeLemmas + +-- ============================================================================ +-- INTERPRETER +-- ============================================================================ + +def head' : Yul.State × List Literal → Yul.State × Literal + | (s, rets) => (s, List.head! rets) + +def cons' (arg : Literal) : Yul.State × List Literal → Yul.State × List Literal + | (s, args) => (s, arg :: args) + +def reverse' : Yul.State × List Literal → Yul.State × List Literal + | (s, args) => (s, args.reverse) + +def multifill' (vars : List Identifier) : Yul.State × List Literal → Yul.State + | (s, rets) => s.multifill vars rets + +/-- +TODO: Temporary EvmYul artefact with separate primop implementations. +-/ +abbrev primCall (s : Yul.State) (prim : Operation .Yul) (args : List Literal) := + step prim s args |>.toOption.map (λ (s, lit) ↦ (s, lit.toList)) |>.getD default + +mutual + def evalTail (fuel : Nat) (args : List Expr) : Yul.State × Literal → Yul.State × List Literal + | (s, arg) => cons' arg (evalArgs fuel args s) + termination_by _ => 1 + fuel + sizeOf args + + /-- + `evalArgs` evaluates a list of arguments. + -/ + def evalArgs (fuel : Nat) (args : List Expr) (s : Yul.State) : Yul.State × List Literal := + match args with + | [] => (s, []) + | arg :: args => + evalTail fuel args (eval fuel arg s) + termination_by fuel + sizeOf args + decreasing_by + all_goals simp_wf; try simp_arith + try apply Expr.zero_lt_sizeOf + + /-- + `call` executes a call of a user-defined function. + -/ + def call (fuel : Nat) (args : List Literal) (f : FunctionDefinition) (s : Yul.State) : Yul.State × List Literal := + let s₁ := 👌 s.initcall f.params args + let s₂ := exec fuel (.Block f.body) s₁ + let s₃ := s₂.reviveJump.overwrite? s |>.setStore s + (s₃, List.map s₂.lookup! f.rets) + termination_by fuel + sizeOf f + decreasing_by + all_goals simp_wf + simp_arith + apply FunctionDefinition.sizeOf_body_succ_lt_sizeOf + + -- Safe to call `List.head!` on return values, because the compiler throws an + -- error when coarity is > 0 in (1) and when coarity is > 1 in all other + -- cases. + + def evalPrimCall (prim : PrimOp) : Yul.State × List Literal → Yul.State × Literal + | (s, args) => head' (primCall s prim args) + + def evalCall (fuel : Nat) (f : FunctionDefinition) : Yul.State × List Literal → Yul.State × Literal + | (s, args) => head' (call fuel args f s) + termination_by _ => 1 + fuel + sizeOf f + + def execPrimCall (prim : PrimOp) (vars : List Identifier) : Yul.State × List Literal → Yul.State + | (s, args) => multifill' vars (primCall s prim args) + + def execCall (fuel : Nat) (f : FunctionDefinition) (vars : List Identifier) : Yul.State × List Literal → Yul.State + | (s, args) => multifill' vars (call fuel args f s) + termination_by _ => 1 + fuel + sizeOf f + + /-- + `execSwitchCases` executes each case of a `switch` statement. + -/ + def execSwitchCases (fuel : Nat) (s : Yul.State) : List (Literal × List Stmt) → List (Literal × Yul.State) + | [] => [] + | ((val, stmts) :: cases') => (val, exec fuel (.Block stmts) s) :: execSwitchCases fuel s cases' + termination_by x => fuel + sizeOf x + + /-- + `eval` evaluates an expression. + + - calls evaluated here are assumed to have coarity 1 + -/ + def eval (fuel : Nat) (expr : Expr) (s : Yul.State) : Yul.State × Literal := + match expr with + + -- We hit these two cases (`PrimCall` and `Call`) when evaluating: + -- + -- 1. f() (expression statements) + -- 2. g(f()) (calls in function arguments) + -- 3. if f() {...} (if conditions) + -- 4. for {...} f() ... (for conditions) + -- 5. switch f() ... (switch conditions) + + | .PrimCall prim args => evalPrimCall prim (reverse' (evalArgs fuel args.reverse s)) + | .Call f args => evalCall fuel f (reverse' (evalArgs fuel args.reverse s)) + | .Var id => (s, s[id]!) + | .Lit val => (s, val) + termination_by fuel + sizeOf expr + decreasing_by + all_goals + simp_wf + try simp_arith + try apply Expr.zero_lt_sizeOf_List + + /-- + `exec` executs a single statement. + -/ + def exec (fuel : Nat) (stmt : Stmt) (s : Yul.State) : Yul.State := + match stmt with + | .Block [] => s + | .Block (stmt :: stmts) => + let s₁ := exec fuel stmt s + exec fuel (.Block stmts) s₁ + + | .Let vars => List.foldr (λ var s ↦ s.insert var 0) s vars + + | .LetEq var rhs => + let (s, val) := eval fuel rhs s + s.insert var val + + | .LetCall vars f args => execCall fuel f vars (reverse' (evalArgs fuel args.reverse s)) + + | .LetPrimCall vars prim args => execPrimCall prim vars (reverse' (evalArgs fuel args.reverse s)) + + | .Assign var rhs => + let (s, x) := eval fuel rhs s + s.insert var x + + | .AssignCall vars f args => execCall fuel f vars (reverse' (evalArgs fuel args.reverse s)) + + | .AssignPrimCall vars prim args => execPrimCall prim vars (reverse' (evalArgs fuel args.reverse s)) + + | .If cond body => + let (s, cond) := eval fuel cond s + if cond ≠ 0 then exec fuel (.Block body) s else s + + -- "Expressions that are also statements (i.e. at the block level) have + -- to evaluate to zero values." + -- + -- (https://docs.soliditylang.org/en/latest/yul.html#restrictions-on-the-grammar) + -- + -- Thus, we cannot have literals or variables on the RHS. + | .ExprStmtCall f args => execCall fuel f [] (reverse' (evalArgs fuel args.reverse s)) + | .ExprStmtPrimCall prim args => execPrimCall prim [] (reverse' (evalArgs fuel args.reverse s)) + + | .Switch cond cases' default' => + + let (s₁, cond) := eval fuel cond s + let branches := execSwitchCases fuel s₁ cases' + let s₂ := exec fuel (.Block default') s₁ + List.foldr (λ (valᵢ, sᵢ) s ↦ if valᵢ = cond then sᵢ else s) s₂ branches + + -- A `Break` or `Continue` in the pre or post is a compiler error, + -- so we assume it can't happen and don't modify the state in these + -- cases. (https://docs.soliditylang.org/en/v0.8.23/yul.html#loops) + | .For cond post body => loop fuel cond post body s + | .Continue => 🔁 s + | .Break => 💔 s + | .Leave => 🚪 s + termination_by fuel + sizeOf stmt + decreasing_by + all_goals + simp_wf + try simp_arith + try apply le_add_right + try apply List.zero_lt_sizeOf + try apply Expr.zero_lt_sizeOf + try apply Expr.zero_lt_sizeOf_List + + /-- + `loop` executes a for-loop. + -/ + def loop (fuel : Nat) (cond : Expr) (post body : List Stmt) (s : Yul.State) : Yul.State := + match fuel with + | 0 => s.diverge + | 1 => s.diverge + | fuel + 1 + 1 => + let (s₁, x) := eval fuel cond (👌s) + if x = 0 + then s₁✏️⟦s⟧? + else + let s₂ := exec fuel (.Block body) s₁ + match s₂ with + | .OutOfFuel => s₂✏️⟦s⟧? + | .Checkpoint (.Break _ _) => 🧟s₂✏️⟦s⟧? + | .Checkpoint (.Leave _ _) => s₂✏️⟦s⟧? + | .Checkpoint (.Continue _ _) + | _ => + let s₃ := exec fuel (.Block post) (🧟 s₂) + let s₄ := s₃✏️⟦s⟧? + let s₅ := exec fuel (.For cond post body) s₄ + let s₆ := s₅✏️⟦s⟧? + s₆ + termination_by fuel + sizeOf cond + sizeOf post + sizeOf body + decreasing_by + all_goals + simp_wf + simp_arith + +end + +notation "🍄" => exec +notation "🌸" => eval + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/MachineState.lean b/EvmYul/Yul/MachineState.lean new file mode 100644 index 0000000..2822166 --- /dev/null +++ b/EvmYul/Yul/MachineState.lean @@ -0,0 +1,17 @@ +import EvmYul.MachineState +import EvmYul.Yul.Wheels + +namespace EvmYul + +namespace Yul + +/-- +The partial Yul `MachineState` `μ`. +-/ +structure MachineState extends EvmYul.MachineState := + varStore : VarStore +deriving DecidableEq, Inhabited + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/PrimOps.lean b/EvmYul/Yul/PrimOps.lean new file mode 100644 index 0000000..7567393 --- /dev/null +++ b/EvmYul/Yul/PrimOps.lean @@ -0,0 +1,150 @@ +import EvmYul.Yul.State +import EvmYul.Yul.Exception +import EvmYul.Yul.StateOps +import EvmYul.SharedStateOps + +import EvmYul.UInt256 + +import EvmYul.Wheels + +namespace EvmYul + +namespace Yul + +open Lean Parser + +set_option autoImplicit true + +def Transformer := Yul.State → List Literal → Except Yul.Exception (Yul.State × Option Literal) + +def execUnOp (f : Primop.Unary) : Transformer + | s, [a] => .ok (s, f a) + | _, _ => throw .InvalidArguments + +def execBinOp (f : Primop.Binary) : Transformer + | s, [a, b] => .ok (s, f a b) + | _, _ => throw .InvalidArguments + +def execTriOp (f : Primop.Ternary) : Transformer + | s, [a, b, c] => .ok (s, f a b c) + | _, _ => throw .InvalidArguments + +def execQuadOp (f : Primop.Quaternary) : Transformer + | s, [a, b, c, d] => .ok (s, f a b c d) + | _, _ => throw .InvalidArguments + +def executionEnvOp (op : ExecutionEnv → UInt256) : Transformer := + λ yulState _ ↦ .ok (yulState, .some <| op yulState.executionEnv) + +def machineStateOp (op : MachineState → UInt256) : Transformer := + λ yulState _ ↦ .ok (yulState, .some <| op yulState.toMachineState) + +def binaryMachineStateOp + (op : MachineState → UInt256 → UInt256 → MachineState) : Transformer +:= λ yulState lits ↦ + match lits with + | [a, b] => + let mState' := op yulState.toMachineState a b + let yulState' := yulState.setMachineState mState' + .ok <| (yulState', none) + | _ => .error .InvalidArguments + +def binaryMachineStateOp' + (op : MachineState → UInt256 → UInt256 → UInt256 × MachineState) : Transformer +:= λ yulState lits ↦ + match lits with + | [a, b] => + let (val, mState') := op yulState.toMachineState a b + let yulState' := yulState.setMachineState mState' + .ok <| (yulState', some val) + | _ => .error .InvalidArguments + +def binaryStateOp + (op : EvmYul.State → UInt256 → UInt256 → EvmYul.State) : Transformer +:= λ yulState lits ↦ + match lits with + | [a, b] => + let state' := op yulState.toState a b + let yulState' := yulState.setState state' + .ok <| (yulState', none) + | _ => .error .InvalidArguments + +def stateOp (op : EvmYul.State → UInt256) : Transformer := + λ yulState _ ↦ .ok (yulState, .some <| op yulState.toState) + +def unaryStateOp (op : EvmYul.State → UInt256 → EvmYul.State × UInt256) : Transformer := + λ yulState lits ↦ + match lits with + | [lit] => + let (state', b) := op yulState.toState lit + let yulState' := + yulState.setSharedState { yulState.toSharedState with toState := state' } + .ok (yulState', some b) + | _ => .error .InvalidArguments + +def ternaryCopyOp (op : SharedState → UInt256 → UInt256 → UInt256 → SharedState) : + Transformer +:= λ yulState lits ↦ + match lits with + | [a, b, c] => + let sState' := op yulState.toSharedState a b c + let yulState' := yulState.setSharedState sState' + .ok (yulState', none) + | _ => .error .InvalidArguments + +def quaternaryCopyOp + (op : SharedState → UInt256 → UInt256 → UInt256 → UInt256 → SharedState) : + Transformer +:= λ yulState lits ↦ + match lits with + | [a, b, c, d] => + let sState' := op yulState.toSharedState a b c d + let yulState' := yulState.setSharedState sState' + .ok (yulState', none) + | _ => .error .InvalidArguments + +private def yulLogOp (yulState : State) (a b : UInt256) (t : List UInt256) : State × Option Literal := + let (substate', μᵢ') := SharedState.logOp a b t yulState.toSharedState + ( yulState.setSharedState + { yulState.sharedState with substate := substate', maxAddress := μᵢ'} + , none + ) + +def log0Op : Transformer := + λ yulState lits ↦ + match lits with + | [a, b] => + .ok <| yulLogOp yulState a b [] + | _ => .ok (yulState, none) + +def log1Op : Transformer := + λ yulState lits ↦ + match lits with + | [a, b, c] => + .ok <| yulLogOp yulState a b [c] + | _ => .ok (yulState, none) + +def log2Op : Transformer := + λ yulState lits ↦ + match lits with + | [a, b, c, d] => + .ok <| yulLogOp yulState a b [c, d] + | _ => .ok (yulState, none) + +def log3Op : Transformer := + λ yulState lits ↦ + match lits with + | [a, b, c, d, e] => + .ok <| yulLogOp yulState a b [c, d, e] + | _ => .ok (yulState, none) + +def log4Op : Transformer := + λ yulState lits ↦ + match lits with + | [a, b, c, d, e, f] => + .ok <| yulLogOp yulState a b [c, d, e, f] + | _ => .ok (yulState, none) + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/SizeLemmas.lean b/EvmYul/Yul/SizeLemmas.lean new file mode 100644 index 0000000..2141030 --- /dev/null +++ b/EvmYul/Yul/SizeLemmas.lean @@ -0,0 +1,133 @@ +import EvmYul.Yul.Ast + +namespace EvmYul + +namespace Yul + +namespace SizeLemmas + +section + +open EvmYul Ast Expr Stmt FunctionDefinition + +variable {expr arg : Expr} + {stmt : Stmt} + {exprs args args' : List Expr} + {stmts : List Stmt} + {f : FunctionDefinition} + {prim : PrimOp} + {α : Type} + {xs ys : List α} + +-- ============================================================================ +-- SIZEOF LEMMAS +-- ============================================================================ + +@[simp] +lemma Zero.zero_le {n : ℕ} : Zero.zero ≤ n := by ring_nf; exact Nat.zero_le _ + +@[simp] +lemma List.zero_lt_sizeOf : 0 < sizeOf xs +:= by + rcases xs <;> simp_arith + +@[simp] +lemma List.reverseAux_size : sizeOf (List.reverseAux args args') = sizeOf args + sizeOf args' - 1 := by + induction args generalizing args' with + | nil => simp_arith + | cons z zs ih => + aesop (config := {warnOnNonterminal := false}); omega + +@[simp] +lemma List.reverse_size : sizeOf (args.reverse) = sizeOf args := by + unfold List.reverse + rw [List.reverseAux_size] + simp_arith + +/-- + Expressions have positive size. +-/ +@[simp] +lemma Expr.zero_lt_sizeOf : 0 < sizeOf expr := by + rcases expr <;> simp_arith + +@[simp] +lemma Stmt.sizeOf_stmt_ne_0 : sizeOf stmt ≠ 0 := by cases stmt <;> aesop + +/-- + Statements have positive size. +-/ +@[simp] +lemma Stmt.zero_lt_sizeOf : 0 < sizeOf stmt := by + have : sizeOf stmt ≠ 0 := by simp + omega + +/-- + Lists of expressions have positive size. +-/ +@[simp] +lemma Expr.zero_lt_sizeOf_List : 0 < sizeOf exprs := by + have : sizeOf exprs ≠ 0 := by cases exprs <;> aesop + omega + +@[simp] +lemma Expr.sizeOf_head_lt_sizeOf_List : sizeOf expr < sizeOf (expr :: exprs) := by + simp_arith + +@[simp] +lemma Expr.sizeOf_tail_lt_sizeOf_List : sizeOf exprs < sizeOf (expr :: exprs) := by + simp_arith + +/-- + Lists of statements have positive size. +-/ +@[simp] +lemma Stmt.zero_lt_sizeOf_List : 0 < sizeOf stmts := by cases stmts <;> aesop + +/-- + Function definitions have positive size. +-/ +@[simp] +lemma FunctionDefinition.zero_lt_sizeOf : 0 < sizeOf f := by cases f; aesop + +@[simp] +lemma Expr.sizeOf_args_lt_sizeOf_Call : sizeOf args < sizeOf (Call f args) := by + simp_arith + +@[simp] +lemma Expr.sizeOf_args_lt_sizeOf_PrimCall : sizeOf args < sizeOf (PrimCall prim args) := by + simp_arith + +/-- + The size of the body of a function is less than the size of the function itself. +-/ +@[simp] +lemma FunctionDefinition.sizeOf_body_lt_sizeOf : sizeOf (body f) < sizeOf f := by unfold body; aesop + +lemma FunctionDefinition.sizeOf_body_succ_lt_sizeOf : sizeOf (FunctionDefinition.body f) + 1 < sizeOf f := by + cases f + unfold body + simp_arith + exact le_add_right List.zero_lt_sizeOf + +/-- + The size of the head of a list of statements is less than the size of a block containing the whole list. +-/ +@[simp] +lemma Stmt.sizeOf_head_lt_sizeOf : sizeOf stmt < sizeOf (Block (stmt :: stmts)) := by + simp only [Block.sizeOf_spec, List.cons.sizeOf_spec] + linarith + +/-- + The size of the head of a list of statements is less than the size of a block containing the whole list. +-/ +@[simp] +lemma Stmt.sizeOf_head_lt_sizeOf_tail : sizeOf (Block stmts) < sizeOf (Block (stmt :: stmts)) := by simp + +end + +end SizeLemmas + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/State.lean b/EvmYul/Yul/State.lean new file mode 100644 index 0000000..d12218b --- /dev/null +++ b/EvmYul/Yul/State.lean @@ -0,0 +1,50 @@ +import Mathlib.Data.Finmap + +import EvmYul.Wheels +import EvmYul.Yul.Wheels +import EvmYul.SharedState + +namespace EvmYul + +namespace Yul + +/-- +A jump in control flow containing a checkpoint of the state at jump-time. +- `Continue`: yul `continue` was encountered +- `Break` : yul `break` was encountered +- `Leave` : evm `return` was encountered +-/ +inductive Jump where + | Continue : EvmYul.SharedState → VarStore → Jump + | Break : EvmYul.SharedState → VarStore → Jump + | Leave : EvmYul.SharedState → VarStore → Jump +deriving DecidableEq + +/-- +The Yul `State`. +- `Ok state varstore` : The underlying `EvmYul.State` `state` along with `varstore`. +- `OutOfFuel` : No state. +- `Checkpoint` : Restore a previous state due to control flow. + +The definition is ever so slightly off due to historical reasons. +-/ +inductive State where + | Ok : EvmYul.SharedState → VarStore → State + | OutOfFuel : State + | Checkpoint : Jump → State +deriving DecidableEq + +instance : Inhabited State where + default := .Ok default default + +namespace State + +def sharedState : State → EvmYul.SharedState + | Ok sharedState _ => sharedState + | _ => default + +end State + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/StateOps.lean b/EvmYul/Yul/StateOps.lean new file mode 100644 index 0000000..78abbbf --- /dev/null +++ b/EvmYul/Yul/StateOps.lean @@ -0,0 +1,161 @@ +import EvmYul.Yul.State + +namespace EvmYul + +namespace Yul + +namespace State + +-- | Insert an (identifier, literal) pair into the varstore. +def insert (var : Identifier) (val : Literal) : Yul.State → Yul.State + | (Ok sharedState store) => Ok sharedState (store.insert var val) + | s => s + +-- | Zip a list of variables with a list of literals and insert right-to-left. +def multifill (vars : List Identifier) (vals : List Literal) : Yul.State → Yul.State + | s@(Ok _ _) => (List.zip vars vals).foldr (λ (var, val) s ↦ s.insert var val) s + | s => s + +-- | Overwrite the EvmYul.Yul.State state of some state. +def setSharedState (sharedState : EvmYul.SharedState) : Yul.State → Yul.State + | Ok _ store => Ok sharedState store + | s => s + +def setMachineState (mstate : EvmYul.MachineState) : Yul.State → Yul.State + | Ok sstate store => Ok {sstate with toMachineState := mstate} store + | s => s + +def setState (state : EvmYul.State) : Yul.State → Yul.State + | Ok sstate store => Ok {sstate with toState := state} store + | s => s + +-- | Overwrite the varstore of some state. +def setStore (s s' : Yul.State) : Yul.State := + match s, s' with + | (Ok sharedState _), (Ok _ store) => Ok sharedState store + | s, _ => s + +def setContinue : Yul.State → Yul.State + | Ok sharedState store => Checkpoint (.Continue sharedState store) + | s => s + +def setBreak : Yul.State → Yul.State + | Ok sharedState store => Checkpoint (.Break sharedState store) + | s => s + +def setLeave : Yul.State → Yul.State + | Ok sharedState store => Checkpoint (.Leave sharedState store) + | s => s + +-- | Indicate that we've hit an infinite loop/ran out of fuel. +def diverge : Yul.State → Yul.State + | Ok _ _ => .OutOfFuel + | s => s + +-- | Initialize function parameters and return values in varstore. +def initcall (params : List Identifier) (args : List Literal) : Yul.State → Yul.State + | s@(Ok _ _) => + let s₁ := s.setStore default + s₁.multifill params args + | s => s + +-- | Since it literally does not matter what happens if the state is non-Ok, we just use the default. +def mkOk : Yul.State → Yul.State + | Checkpoint _ => default + | s => s + +-- | Helper function for `reviveJump`. +def revive : Jump → Yul.State + | .Continue sharedState store => Ok sharedState store + | .Break sharedState store => Ok sharedState store + | .Leave sharedState store => Ok sharedState store + +-- | Revive a saved state (sharedState, varstore), discarding top-level (sharedState, varstore). +-- +-- Called after we've finished executing: +-- * A loop +-- * A function call +-- +-- The compiler disallows top-level `Continue`s or `Break`s in function bodies, +-- thus it is safe to assume the state we're reviving is a checkpoint from the +-- expected flavor of `Jump`. +def reviveJump : Yul.State → Yul.State + | Checkpoint c => revive c + | s => s + +-- | If s' is non-Ok, overwrite s with s'. +def overwrite? (s s' : Yul.State) : Yul.State := + match s' with + | Ok _ _ => s + | _ => s' + +-- ============================================================================ +-- STATE QUERIES +-- ============================================================================ + +-- | Lookup the literal associated with an variable in the varstore, returning 0 if not found. +def lookup! (var : Identifier) : Yul.State → Literal + | Ok _ store => (store.lookup var).get! + | Checkpoint (.Continue _ store) => (store.lookup var).get! + | Checkpoint (.Break _ store) => (store.lookup var).get! + | Checkpoint (.Leave _ store) => (store.lookup var).get! + | _ => 0 + +-- ============================================================================ +-- STATE NOTATION +-- ============================================================================ + +def toSharedState : State → EvmYul.SharedState + | Ok s _ => s + | _ => default + +def executionEnv : State → EvmYul.ExecutionEnv + | Ok s _ => s.executionEnv + | _ => default + +def toMachineState : State → EvmYul.MachineState + | Ok s _ => s.toMachineState + | _ => default + +def toState : State → EvmYul.State + | Ok s _ => s.toState + | _ => default + +def store : State → VarStore + | Ok _ store => store + | _ => default + +-- | All state-related functions should be prefix operators so they can be read right-to-left. + +-- Yul.State queries +-- notation:65 s:64"[" var "]!" => Yul.State.lookup! var s + +/-- +TODO - The notation is a bit of a remnant from EvmYul and it is unnecessarily overzaelous. +This should have been an instance of GetElem in the first place. + +N.B. We also ignore the validity condition altogether for the time being. +-/ +instance : GetElem Yul.State Identifier Literal (λ s idx ↦ idx ∈ s.store) where + getElem s ident _ := s.lookup! ident + +notation "❓" => Yul.State.isOutOfFuel + +-- Yul.State transformers +notation:65 s:64 "⟦" var "↦" lit "⟧" => Yul.State.insert var lit s +notation:65 "🔁" s:64 => Yul.State.setContinue s +notation:65 "💔" s:64 => Yul.State.setBreak s +notation:65 "🚪" s:64 => Yul.State.setLeave s +notation:65 s:64 "🏪⟦" s' "⟧" => Yul.State.setStore s s' +notation:65 s:64 "🇪⟦" sharedState "⟧" => Yul.State.setSharedState sharedState s +notation:65 "🪫" s:64 => Yul.State.diverge s +notation:65 "👌" s:64 => Yul.State.mkOk s +notation:65 s:64 "☎️⟦" params "," args "⟧" => Yul.State.initcall params args s +notation:65 s:64 "✏️⟦" s' "⟧?" => Yul.State.overwrite? s s' +notation:64 (priority := high) "🧟" s:max => Yul.State.reviveJump s + +end State + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/Wheels.lean b/EvmYul/Yul/Wheels.lean new file mode 100644 index 0000000..c2c9c76 --- /dev/null +++ b/EvmYul/Yul/Wheels.lean @@ -0,0 +1,13 @@ +import Mathlib.Data.Finmap + +import EvmYul.Wheels + +namespace EvmYul + +namespace Yul + +abbrev VarStore := Finmap (λ _ : Identifier ↦ Literal) + +end Yul + +end EvmYul diff --git a/EvmYul/Yul/YulNotation.lean b/EvmYul/Yul/YulNotation.lean new file mode 100644 index 0000000..171f6a2 --- /dev/null +++ b/EvmYul/Yul/YulNotation.lean @@ -0,0 +1,477 @@ +import EvmYul.Yul.Ast +import Lean.Parser +import EvmYul.Operations + +namespace EvmYul + +namespace Yul + +namespace Notation + +open Ast Lean Parser Elab Term + +def yulKeywords := ["let", "if", "default", "switch", "case"] + +def idFirstChar : Array Char := Id.run <| do + let mut arr := #[] + for i in [0:26] do + arr := arr.push (Char.ofNat ('a'.toNat + i)) + for i in [0:26] do + arr := arr.push (Char.ofNat ('A'.toNat + i)) + arr := (arr.push '_').push '$' + return arr + +def idSubsequentChar : Array Char := Id.run <| do + let mut arr := idFirstChar + for i in [0:10] do + arr := arr.push (Char.ofNat ('0'.toNat + i)) + return arr.push '.' + +def idFn : ParserFn := fun c s => Id.run do + let input := c.input + let start := s.pos + if h : input.atEnd start then + s.mkEOIError + else + let fst := input.get' start h + if not (idFirstChar.contains fst) then + return s.mkError "yul identifier" + let s := takeWhileFn idSubsequentChar.contains c (s.next input start) + let stop := s.pos + let name := .str .anonymous (input.extract start stop) + if yulKeywords.contains name.lastComponentAsString then + return s.mkError "yul identifier" + mkIdResult start none name c s + +def idNoAntiquot : Parser := { fn := idFn } + +section +open PrettyPrinter Parenthesizer Syntax.MonadTraverser Formatter + +@[combinator_formatter idNoAntiquot] +def idNoAntiquot.formatter : Formatter := do + Formatter.checkKind identKind + let Syntax.ident info _ idn _ ← getCur + | throwError m!"not an ident: {← getCur}" + Formatter.pushToken info idn.toString + goLeft + +@[combinator_parenthesizer idNoAntiquot] +def idNoAntiquot.parenthesizer := Parenthesizer.visitToken +end + +@[run_parser_attribute_hooks] +def ident : Parser := withAntiquot (mkAntiquot "ident" identKind) idNoAntiquot + +declare_syntax_cat expr +declare_syntax_cat stmt + +syntax identifier_list := ident,* +syntax typed_identifier_list := ident,* +syntax function_call := ident "(" expr,* ")" +syntax block := "{" stmt* "}" +syntax if' := "if" expr block +syntax function_definition := + "function" ident "(" typed_identifier_list ")" + ("->" typed_identifier_list)? + block +syntax params_list := "[" typed_identifier_list "]" +syntax variable_declaration := "let" ident (":=" expr)? +-- syntax let_str_literal := "let" ident ":=" str -- TODO(fix) +syntax variable_declarations := "let" typed_identifier_list (":=" expr)? +syntax for_loop := "for" block expr block block +syntax assignment := identifier_list ":=" expr + +syntax stmtlist := stmt* + +syntax block : stmt +syntax if' : stmt +syntax function_definition : stmt +syntax variable_declarations : stmt +syntax assignment : stmt +syntax expr : stmt +-- syntax let_str_literal : stmt -- TODO(fix) +syntax for_loop : stmt +syntax "break" : stmt +syntax "continue" : stmt +syntax "leave" : stmt + +syntax ident : expr +syntax numLit : expr +syntax function_call: expr + +syntax default := "default" "{" stmt* "}" +syntax case := "case" expr "{" stmt* "}" +syntax switch := "switch" expr case+ (default)? +syntax switch_default := "switch" expr default + +syntax switch : stmt +syntax switch_default : stmt + +scoped syntax:max "<<" expr ">>" : term +scoped syntax:max "" : term +scoped syntax:max "" : term +scoped syntax:max "" : term +scoped syntax:max "" : term + +partial def translatePrimOp (primOp : PrimOp) : TermElabM Term := do + let (family, instr) ← familyAndInstr primOp + PrettyPrinter.delab ( + ←Lean.Meta.mkAppM + family.toName + #[←Lean.Meta.mkAppOptM instr.toName #[mkConst YulTag]] + ) + where + familyAndInstr (primOp : PrimOp) : TermElabM (String × String) := do + let family :: instr :: [] := toString primOp |>.splitOn | throwError s!"{primOp} shape not " + pure (family, instr.drop 1 |>.dropRight 1) + YulTag : Name := "EvmYul.OperationType.Yul".toName + +partial def translateIdent (idn : TSyntax `ident) : TSyntax `term := + Syntax.mkStrLit idn.getId.lastComponentAsString + +def parseFunction : String → PrimOp ⊕ Identifier + | "add" => .inl .ADD + | "sub" => .inl .SUB + | "mul" => .inl .MUL + | "div" => .inl .DIV + | "sdiv" => .inl .SDIV + | "mod" => .inl .MOD + | "smod" => .inl .SMOD + | "addmod" => .inl .ADDMOD + | "mulmod" => .inl .MULMOD + | "exp" => .inl .EXP + | "signextend" => .inl .SIGNEXTEND + | "lt" => .inl .LT + | "gt" => .inl .GT + | "slt" => .inl .SLT + | "sgt" => .inl .SGT + | "eq" => .inl .EQ + | "iszero" => .inl .ISZERO + | "and" => .inl .AND + | "or" => .inl .OR + | "xor" => .inl .XOR + | "not" => .inl .NOT + | "byte" => .inl .BYTE + | "shl" => .inl .SHL + | "shr" => .inl .SHR + | "sar" => .inl .SAR + | "keccak256" => .inl .KECCAK256 + | "address" => .inl .ADDRESS + | "balance" => .inl .BALANCE + | "origin" => .inl .ORIGIN + | "caller" => .inl .CALLER + | "callvalue" => .inl .CALLVALUE + | "calldataload" => .inl .CALLDATALOAD + | "calldatacopy" => .inl .CALLDATACOPY + | "calldatasize" => .inl .CALLDATASIZE + | "codesize" => .inl .CODESIZE + | "codecopy" => .inl .CODECOPY + | "gasprice" => .inl .GASPRICE + | "extcodesize" => .inl .EXTCODESIZE + | "extcodecopy" => .inl .EXTCODECOPY + | "extcodehash" => .inl .EXTCODEHASH + | "returndatasize" => .inl .RETURNDATASIZE + | "returndatacopy" => .inl .RETURNDATACOPY + | "blockhash" => .inl .BLOCKHASH + | "coinbase" => .inl .COINBASE + | "timestamp" => .inl .TIMESTAMP + | "gaslimit" => .inl .GASLIMIT + | "chainid" => .inl .CHAINID + | "selfbalance" => .inl .SELFBALANCE + | "mload" => .inl .MLOAD + | "mstore" => .inl .MSTORE + | "sload" => .inl .SLOAD + | "sstore" => .inl .SSTORE + | "msize" => .inl .MSIZE + | "gas" => .inl .GAS + | "pop" => .inl .POP + | "revert" => .inl .REVERT + | "return" => .inl .RETURN + | "call" => .inl .CALL + | "staticcall" => .inl .STATICCALL + | "delegatecall" => .inl .DELEGATECALL + -- | "loadimmutable" => .inl .LOADI + -- | "log0" => .inl .LOG0 + | "log1" => .inl .LOG1 + | "log2" => .inl .LOG2 + | "log3" => .inl .LOG3 + | "log4" => .inl .LOG4 + | "number" => .inl .NUMBER + | userF => .inr userF + +partial def translateExpr (expr : TSyntax `expr) : TermElabM Term := + match expr with + | `(expr| $idn:ident) => `(Expr.Var $(translateIdent idn)) + | `(expr| $num:num) => `(Expr.Lit $num) + | `(expr| $name:ident($args:expr,*)) => do + let args' ← (args : TSyntaxArray `expr).mapM translateExpr + let f' := parseFunction (TSyntax.getId name).lastComponentAsString + match f' with + | .inl primOp => + let primOp ← translatePrimOp primOp + `(Expr.PrimCall $primOp [$args',*]) + | .inr _ => + `(Expr.Call $name [$args',*]) + | _ => throwError "unknown expr" + +partial def translateExpr' (expr : TSyntax `expr) : TermElabM Term := + match expr with + | `(expr| $num:num) => `($num) + | exp => translateExpr exp + +partial def translateParamsList + (params : TSyntax `EvmYul.Yul.Notation.params_list) +: TermElabM Term := + match params with + | `(params_list| [ $args:ident,* ]) => do + let args' := (args : TSyntaxArray _).map translateIdent + `([$args',*]) + | _ => throwError (toString params.raw) + +mutual +partial def translateFdef + (fdef : TSyntax `EvmYul.Yul.Notation.function_definition) +: TermElabM Term := + match fdef with + | `(function_definition| function $_:ident($args:ident,*) {$body:stmt*}) => do + let args' := (args : TSyntaxArray _).map translateIdent + let body' ← body.mapM translateStmt + `(EvmYul.Yul.Ast.FunctionDefinition.Def [$args',*] [] [$body',*]) + | `(function_definition| function $_:ident($args:ident,*) -> $rets,* {$body:stmt*}) => do + let args' := (args : TSyntaxArray _).map translateIdent + let rets' := (rets : TSyntaxArray _).map translateIdent + let body' ← body.mapM translateStmt + `(EvmYul.Yul.Ast.FunctionDefinition.Def [$args',*] [$rets',*] [$body',*]) + | _ => throwError (toString fdef.raw) + +partial def translateStmt (stmt : TSyntax `stmt) : TermElabM Term := + match stmt with + + -- Block + | `(stmt| {$stmts:stmt*}) => do + let stmts' ← stmts.mapM translateStmt + `(Stmt.Block ([$stmts',*])) + + -- If + | `(stmt| if $cond:expr {$body:stmt*}) => do + let cond' ← translateExpr cond + let body' ← body.mapM translateStmt + `(Stmt.If $cond' [$body',*]) + + -- Function Definition + | `(stmt| $fdef:function_definition) => do + let fdef' ← translateFdef fdef + `(Stmt.FunctionDefinition $fdef') + + -- Switch + | `(stmt| switch $expr:expr $[case $lits { $cs:stmt* }]* $[default { $dflts:stmt* }]?) => do + let expr ← translateExpr expr + let lits ← lits.mapM translateExpr' + let cases ← cs.mapM (λ cc ↦ cc.mapM translateStmt) + let f (litCase : TSyntax `term × Array Term) : TermElabM Term := do + let (lit, cs) := litCase; `(($lit, [$cs,*])) + let switchCases ← lits.zip cases |>.mapM f + let dflt ← match dflts with + | .none => `([.Break]) + | .some dflts => `([$(←dflts.mapM translateStmt),*]) + `(Stmt.Switch $expr [$switchCases,*] $dflt) + + -- Switch + | `(stmt| switch $expr:expr default {$dflts:stmt*}) => do + let expr ← translateExpr expr + let dflt ← dflts.mapM translateStmt + `(Stmt.Switch $expr [] ([$dflt,*])) + + -- LetCall + | `(stmt| let $ids:ident,* := $f:ident ( $es:expr,* )) => do + let ids' := (ids : TSyntaxArray _).map translateIdent + let f' := parseFunction (TSyntax.getId f).lastComponentAsString + let es' ← (es : TSyntaxArray _).mapM translateExpr + match f' with + | .inl primOp => + let primOp ← translatePrimOp primOp + `(Stmt.LetPrimCall [$ids',*] $primOp [$es',*]) + | .inr _ => + `(Stmt.LetCall [$ids',*] $f [$es',*]) + + -- LetEq + | `(stmt| let $idn:ident := $init:expr) => do + let idn' := translateIdent idn + let expr' ← translateExpr init + `(Stmt.LetEq $idn' $expr') + + -- TODO(fix) + -- | `(stmt| let $idn:ident := $s:str) => do + -- let idn' := translateIdent idn + -- `(Stmt.LetEq $idn' _) + + -- Let + | `(stmt| let $ids:ident,*) => do + let ids' := (ids : TSyntaxArray _).map translateIdent + `(Stmt.Let [$ids',*]) + + -- AssignCall + | `(stmt| $ids:ident,* := $f:ident ( $es:expr,* )) => do + let ids' := (ids : TSyntaxArray _).map translateIdent + let f' := parseFunction (TSyntax.getId f).lastComponentAsString + let es' ← (es : TSyntaxArray _).mapM translateExpr + match f' with + | .inl primOp => + let primOp ← translatePrimOp primOp + `(Stmt.AssignPrimCall [$ids',*] $primOp [$es',*]) + | .inr _ => + `(Stmt.AssignCall [$ids',*] $f [$es',*]) + + -- Assign + | `(stmt| $idn:ident := $init:expr) => do + let idn' := translateIdent idn + let expr' ← translateExpr init + `(Stmt.Assign $idn' $expr') + + -- ExprStmt + | `(stmt| $f:ident ( $es:expr,* )) => do + let f' := parseFunction (TSyntax.getId f).lastComponentAsString + let es' ← (es : TSyntaxArray _).mapM translateExpr + match f' with + | .inl primOp => + let primOp ← translatePrimOp primOp + `(Stmt.ExprStmtPrimCall $primOp [$es',*]) + | .inr _ => + `(Stmt.ExprStmtCall $f [$es',*]) + + -- For + | `(stmt| for {} $cond:expr {$post:stmt*} {$body:stmt*}) => do + let cond' ← translateExpr cond + let post' ← post.mapM translateStmt + let body' ← body.mapM translateStmt + `(Stmt.For $cond' [$post',*] [$body',*]) + + -- Break + | `(stmt| break) => `(Stmt.Break) + + -- Continue + | `(stmt| continue) => `(Stmt.Continue) + + -- Leave + | `(stmt| leave) => `(Stmt.Leave) + + -- Anything else + | _ => throwError (toString stmt.raw) +end + +partial def translateStmtList (stmt : TSyntax `stmt) : TermElabM Term := + match stmt with + | `(stmt| {$stmts:stmt*}) => do + let stmts' ← stmts.mapM translateStmt + `([$stmts',*]) + | _ => throwError (toString stmt.raw) + +private def elabWith {β : SyntaxNodeKinds} + (x : Syntax) (translator : TSyntax β → TermElabM Term) : TermElabM Lean.Expr := do + elabTerm (←translator (TSyntax.mk (ks := β) x)) .none + +elab "<<" e:expr ">>" : term => elabWith e translateExpr +elab "" : term => elabWith f translateFdef +elab "" : term => elabWith s translateStmt +elab "" : term => elabWith ss translateStmtList +elab "" : term => elabWith p translateParamsList + +def f : FunctionDefinition := x, y { + if lt(a, b) { + x := a + y := b + leave + } + x := b + y := a + } +> + +example : = ["a", "b", "c"] := rfl +example : << bar >> = Expr.Var "bar" := rfl +example : << 42 >> = Expr.Lit 42 := rfl +example : = Stmt.Break := rfl +example : = Stmt.LetCall ["a", "b"] f [Expr.Lit 42] := rfl +example : = Stmt.Let ["a"] := rfl +example : = Stmt.LetEq "a" (.Lit 5) := rfl +example : = Stmt.AssignCall ["a", "b"] f [Expr.Lit 42] := rfl +example : = Stmt.Assign "a" (.Lit 42) := rfl + +example : = Stmt.AssignPrimCall ["c"] (Operation.StopArith Operation.SAOp.ADD) [Expr.Var "a", Expr.Var "b"] := rfl +example : = Stmt.LetPrimCall ["c"] (Operation.StopArith Operation.SAOp.SUB) [Expr.Var "a", Expr.Var "b"] := rfl +example : = Stmt.LetEq "a" (.Lit 5) := rfl +example : + = Stmt.Block [] := rfl +example : = Stmt.Block [, , ] := rfl +example : = Stmt.If <> [, ] := rfl + +example : = [, , ] := rfl + +example : = Stmt.For (.Lit 0) [] [] := by rfl + +example : << + add(1, 1) + >> = Expr.PrimCall (Operation.StopArith Operation.SAOp.ADD) [Expr.Lit 1, Expr.Lit 1] := rfl + +example : = Stmt.For <> [] + [] := rfl + +def sort2 : FunctionDefinition := x, y { + if lt(a, b) { + x := a + y := b + leave + } + x := b + y := a + } +> + +def no_rets : FunctionDefinition := + +example : = Stmt.Switch (Expr.Var "a") [(42, [.Continue])] [.Break] := rfl + +example : = Stmt.Let ["a", "b", "c"] := rfl +example : = Stmt.ExprStmtPrimCall (.System (.REVERT)) [(Expr.Lit 0), (Expr.Lit 0)] := rfl +example : = Stmt.If (.Lit 1) [Stmt.Leave] := rfl +example : = Stmt.Block [Stmt.If (.Lit 1) [.Leave], .Leave] := rfl + +end Notation + +end Yul + +end EvmYul diff --git a/README.md b/README.md new file mode 100644 index 0000000..47c5544 --- /dev/null +++ b/README.md @@ -0,0 +1,44 @@ +This repository contains a formal model of the EVM and Yul in Lean 4. +Where applicable, the underlying EVM primops are used directly by the Yul model. + +Everything here is work in progress and is subject to change therefore. + +# Project structure + +## Primops +The `Operation` describing all of the primitive operations: +``` +EvmYul/Operations.lean +``` + +The semantic function `primCall` associated with the ADT: +``` +EvmYul/Yul/PrimOps.lean +``` + +## EVM +The model of the EVM state `EVM.State`: +``` +EvmYul/EVM/State.lean +``` + +The semantic function `step`: +``` +EvmYul/EVM/Semantics.lean +``` + +## Yul +The ADT `Stmt` mutually defined with `Expr` and `FunctionDefinition` describing Yul: +``` +EvmYul/Yul/Ast.lean +``` + +The model of the Yul state `YUL.State`: +``` +EvmYul/Yul/State.lean +``` + +The semantic function `exec` mutually defined with `eval` (and some misc. functions): +``` +EvmYul/Yul/Interpreter.lean +``` diff --git a/SpongeHash.lean b/SpongeHash.lean new file mode 100644 index 0000000..570460b --- /dev/null +++ b/SpongeHash.lean @@ -0,0 +1,4 @@ +-- This module serves as the root of the `SpongeHash` library. +-- Import modules here that should be built as part of the library. +import «SpongeHash».Basic +import «SpongeHash».Keccak256 diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..1b1b892 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,68 @@ +{"version": "1.0.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.38", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph.git", + "type": "git", + "subDir": null, + "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "f0957a7575317490107578ebaee9efaf8e62a4ab", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "evmyul", + "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..6bb6b4c --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,18 @@ +import Lake +open Lake DSL + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git"@"f0957a7575317490107578ebaee9efaf8e62a4ab" + +package «evmyul» { + moreLeanArgs := #["-DautoImplicit=false"] + moreServerOptions := #[⟨`DautoImplicit, false⟩] +} + +@[default_target] +lean_lib «EvmYul» + +lean_lib «Conform» + +lean_exe «conform» where + root := `Conform.Main diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..4ef27c4 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.9.0 diff --git a/license.txt b/license.txt new file mode 100644 index 0000000..8d70572 --- /dev/null +++ b/license.txt @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright 2024 Demerzel Solutions Limited (t/a Nethermind) + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License.