diff --git a/EvmYul/Semantics.lean b/EvmYul/Semantics.lean index 07e65a94..f14f9d21 100644 --- a/EvmYul/Semantics.lean +++ b/EvmYul/Semantics.lean @@ -215,7 +215,6 @@ def swap (n : ℕ) : Transformer .EVM := else .error .StackUnderflow --- TODO: Yul halting for `SELFDESTRUCT` def step {τ : OperationType} (op : Operation τ) (arg : Option (UInt256 × Nat) := .none) : Transformer τ := Id.run do let _ : Id Unit := -- For debug logging match τ with @@ -391,7 +390,7 @@ def step {τ : OperationType} (op : Operation τ) (arg : Option (UInt256 × Nat) | .Yul, .REVERT => λ yulState lits ↦ match (dispatchBinaryMachineStateOp .Yul MachineState.evmRevert) yulState lits with | .error e => .error e - | .ok (_, _) => .error (Yul.Exception.Revert) + | .ok (s, _) => .error (Yul.Exception.Revert s) | .EVM, .SELFDESTRUCT => λ evmState ↦ match evmState.stack.pop with @@ -510,7 +509,7 @@ def step {τ : OperationType} (op : Operation τ) (arg : Option (UInt256 × Nat) let yulState' := yulState.setState { yulState.toState with accountMap := accountMap', substate := A'} - .ok <| (yulState', none) + .error (Yul.Exception.YulHalt yulState' ⟨0⟩) | _ => .error .InvalidArguments | τ, .INVALID => dispatchInvalid τ | .EVM, .Push .PUSH0 => λ evmState => diff --git a/EvmYul/Yul/Ast.lean b/EvmYul/Yul/Ast.lean index 7f7c5136..99be310a 100644 --- a/EvmYul/Yul/Ast.lean +++ b/EvmYul/Yul/Ast.lean @@ -47,6 +47,7 @@ mutual inductive Stmt where | Block : List Stmt → Stmt | Let : List Identifier → Option Expr → Stmt + | Assign : List Identifier → Expr → Stmt | ExprStmtCall : Expr → Stmt | Switch : Expr → List (Literal × List Stmt) → List Stmt → Stmt | For : Expr → List Stmt → List Stmt → Stmt diff --git a/EvmYul/Yul/Exception.lean b/EvmYul/Yul/Exception.lean index fdd9b4b7..610a44ae 100644 --- a/EvmYul/Yul/Exception.lean +++ b/EvmYul/Yul/Exception.lean @@ -13,8 +13,10 @@ inductive Exception where | MissingContract (s : String) : Exception | MissingContractFunction (s : String) : Exception | InvalidExpression : Exception + | UnknownIdentifier (s : String) : Exception + | DuplicateDeclaration (s : String) : Exception | YulEXTCODESIZENotImplemented : Exception - | Revert : Exception + | Revert (state : Yul.State) : Exception | YulHalt (state : Yul.State) (value : UInt256) : Exception -- | StopInvoked : Exception @@ -29,8 +31,10 @@ instance : Repr Exception where | .MissingContract s => "MissingContract: " ++ s | .MissingContractFunction f => "MissingContractFunction: " ++ f | .InvalidExpression => "InvalidExpression" + | .UnknownIdentifier s => "UnknownIdentifier: " ++ s + | .DuplicateDeclaration s => "DuplicateDeclaration: " ++ s | .YulEXTCODESIZENotImplemented => "YulEXTCODESIZENotImplemented" - | .Revert => "Revert" + | .Revert _ => "Revert" | .YulHalt _ _ => "YulHalt: (holds a state and a value)" diff --git a/EvmYul/Yul/Interpreter.lean b/EvmYul/Yul/Interpreter.lean index 3e8adfce..7bacf69f 100644 --- a/EvmYul/Yul/Interpreter.lean +++ b/EvmYul/Yul/Interpreter.lean @@ -37,6 +37,51 @@ def multifill' (vars : List Identifier) : Except Yul.Exception (State × List Li | .ok (s, rets) => .ok (s.multifill vars rets) | .error e => .error e +def firstDuplicate? : List Identifier → Option Identifier + | [] => .none + | var :: vars => + if vars.contains var then .some var else firstDuplicate? vars + +def firstDeclared? (s : State) (vars : List Identifier) : Option Identifier := + vars.find? (fun var => (s.lookup? var).isSome) + +def firstUndeclared? (s : State) (vars : List Identifier) : Option Identifier := + vars.find? (fun var => (s.lookup? var).isNone) + +def checkDeclaration (s : State) (vars : List Identifier) : Except Yul.Exception Unit := + match firstDuplicate? vars with + | .some var => .error (.DuplicateDeclaration var) + | .none => + match firstDeclared? s vars with + | .some var => .error (.DuplicateDeclaration var) + | .none => .ok () + +def checkAssignment (s : State) (vars : List Identifier) : Except Yul.Exception Unit := + match firstDuplicate? vars with + | .some _ => .error .InvalidArguments + | .none => + match firstUndeclared? s vars with + | .some var => .error (.UnknownIdentifier var) + | .none => .ok () + +def restoreRevertedContractCallState (s₀ s₂ : State) (outOffset outSize : Literal) : + Except Yul.Exception (State × List Literal) := + match s₀ with + | .OutOfFuel => .error .OutOfFuel + | .Checkpoint j => .ok (.Checkpoint j, [⟨0⟩]) + | .Ok sharedState₀ varstore => + let returnData := s₂.toMachineState.H_return + let memory₃ := + returnData.copySlice 0 s₀.toMachineState.memory outOffset.toNat + (min outSize.toNat returnData.size) + let sharedState₃ := + { sharedState₀ with + memory := memory₃ + returnData := returnData + H_return := ByteArray.empty + } + .ok (.Ok sharedState₃ varstore, [⟨0⟩]) + def setStatic (s : State) (p : Bool) : State := match s with | .OutOfFuel => .OutOfFuel @@ -60,6 +105,19 @@ def buildContractCallEmptyReturnState (s₀ : State) (accountMap₁ : Option (Ac accountMap := accountMap₁.getD s₀.toSharedState.accountMap } .ok (.Ok sharedState₁ varstore, [v]) +/-- + `selectSwitchCase` returns the first switch case body whose literal matches + the evaluated switch condition, or the default body if no case matches. + + This matches Solidity/Yul switch control flow: non-selected case and default + bodies are not executed. +-/ +def selectSwitchCase (cond : Literal) (defaultBody : List Stmt) : + List (Literal × List Stmt) → List Stmt + | [] => defaultBody + | ((val, stmts) :: cases') => + if val = cond then stmts else selectSwitchCase cond defaultBody cases' + mutual def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Literal) : Except Yul.Exception (State × List Literal) := @@ -130,6 +188,8 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li H_return := ByteArray.empty } .ok (.Ok sharedState₃ varstore, [⟨1⟩]) + | .error (.Revert s₂) => + restoreRevertedContractCallState s₀ s₂ outOffset outSize | .error e => .error e | .ok (s₂, _) => @@ -222,6 +282,8 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li executionEnv := executionEnv₃ } .ok (setStatic (.Ok sharedState₃ varstore) s₀.executionEnv.perm, [⟨1⟩]) + | .error (.Revert s₂) => + restoreRevertedContractCallState s₀ s₂ outOffset outSize | .error e => .error e | .ok (s₂, _) => @@ -307,6 +369,8 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li } .ok (.Ok sharedState₃ varstore, [⟨1⟩]) + | .error (.Revert s₂) => + restoreRevertedContractCallState s₀ s₂ outOffset outSize | .error e => .error e | .ok (s₂, _) => let memory₃ := s₂.toMachineState.H_return.copySlice 0 s₀.toMachineState.memory outOffset.toNat (min outSize.toNat s₂.toMachineState.H_return.size) @@ -381,6 +445,8 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li executionEnv := executionEnv₃ } .ok (.Ok sharedState₃ varstore, [⟨1⟩]) + | .error (.Revert s₂) => + restoreRevertedContractCallState s₀ s₂ outOffset outSize | .error e => .error e | .ok (s₂, _) => let memory₃ := s₂.toMachineState.H_return.copySlice 0 s₀.toMachineState.memory outOffset.toNat (min outSize.toNat s₂.toMachineState.H_return.size) @@ -449,7 +515,7 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li match fOpt with | .none => .error (.MissingContractFunction (yulFunctionNameOption.getD ".none")) | .some f => - let s₁ := 👌 s.initcall f.params args + let s₁ := 👌 s.initcall f.params f.rets args match exec fuel' (.Block f.body) codeOverride s₁ with | .error e => .error e | .ok s₂ => @@ -466,7 +532,7 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li | 0 => .error .OutOfFuel | .succ fuel' => let f := FunctionDefinition.Def [] [] [s.executionEnv.code.dispatcher] - let s₁ := 👌 s.initcall f.params [] + let s₁ := 👌 s.initcall f.params f.rets [] match exec fuel' (.Block f.body) codeOverride s₁ with | .error e => .error e | .ok s₂ => @@ -499,31 +565,24 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li | .succ fuel' => multifill' vars (call fuel' args yulFunctionName codeOverride s) | .error e => .error e - /-- - `execSwitchCases` executes each case of a `switch` statement. - -/ - def execSwitchCases (fuel : Nat) (codeOverride : Option YulContract) (s : State) : List (Literal × List Stmt) → Except Yul.Exception (List (Literal × (Except Yul.Exception State))) - | [] => .ok [] - | ((val, stmts) :: cases') => - match fuel with - | 0 => .error .OutOfFuel - | .succ fuel' => - match exec fuel' (.Block stmts) codeOverride s with - | .error (.YulHalt s₂ v) => - match execSwitchCases fuel' codeOverride s cases' with - | .error e => .error e - | .ok s₃ => - .ok ((val, .error (.YulHalt s₂ v)) :: s₃) - | .error e => - match execSwitchCases fuel' codeOverride s cases' with - | .error e => .error e - | .ok s₃ => - .ok ((val, .error e) :: s₃) - | .ok s₂ => - match execSwitchCases fuel' codeOverride s cases' with - | .error e => .error e - | .ok s₃ => - .ok ((val, .ok s₂) :: s₃) + def evalValues (fuel : Nat) (expr : Expr) (codeOverride : Option YulContract) (s : State) : Except Yul.Exception (State × List Literal) := + match fuel with + | 0 => .error .OutOfFuel + | .succ fuel' => + match expr with + | .Call (Sum.inl prim) args => + match reverse' (evalArgs fuel' args.reverse codeOverride s) with + | .ok (s, args) => primCall fuel' s prim args + | .error e => .error e + | .Call (Sum.inr yulFunctionName) args => + match reverse' (evalArgs fuel' args.reverse codeOverride s) with + | .ok (s, args) => call fuel' args yulFunctionName codeOverride s + | .error e => .error e + | .Var id => + match s.lookup? id with + | .some val => .ok (s, [val]) + | .none => .error (.UnknownIdentifier id) + | .Lit val => .ok (s, [val]) /-- `eval` evaluates an expression. @@ -531,24 +590,22 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li - calls evaluated here are assumed to have coarity 1 -/ def eval (fuel : Nat) (expr : Expr) (codeOverride : Option YulContract) (s : State) : Except Yul.Exception (State × Literal) := + head' (evalValues fuel expr codeOverride s) + + def execSeq (fuel : Nat) (stmts : List Stmt) (codeOverride : Option YulContract) (s : State) : Except Yul.Exception State := match fuel with | 0 => .error .OutOfFuel | .succ fuel' => - 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) - - | .Call (Sum.inl prim) args => evalPrimCall fuel' prim (reverse' (evalArgs fuel' args.reverse codeOverride s)) - | .Call (Sum.inr yulFunctionName) args => - evalCall fuel' yulFunctionName codeOverride (reverse' (evalArgs fuel' args.reverse codeOverride s)) - | .Var id => .ok (s, s[id]!) - | .Lit val => .ok (s, val) + match stmts with + | [] => .ok s + | stmt :: stmts => + match exec fuel' stmt codeOverride s with + | .error e => .error e + | .ok s₁ => + match s₁ with + | .Ok _ _ => execSeq fuel' stmts codeOverride s₁ + | .OutOfFuel => .ok s₁ + | .Checkpoint _ => .ok s₁ /-- `exec` executs a single statement. @@ -558,24 +615,23 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li | 0 => .error .OutOfFuel | .succ fuel' => match stmt with - | .Block [] => .ok s - | .Block (stmt :: stmts) => - let s₁ := exec fuel' stmt codeOverride s - match s₁ with - | .error e => .error e - | .ok s₁ => exec fuel' (.Block stmts) codeOverride s₁ + | .Block stmts => + match execSeq fuel' stmts codeOverride s with + | .error e => .error e + | .ok s₁ => .ok (s₁.restrictStoreTo s.store) | .Let vars exprOption => + match checkDeclaration s vars with + | .error e => .error e + | .ok () => match exprOption with - | .none => .ok (List.foldr (λ var s ↦ s.insert var ⟨0⟩) s vars) - | .some expr => - match expr with - | .Call (Sum.inl prim) args => - execPrimCall fuel' prim vars (reverse' (evalArgs fuel' args.reverse codeOverride s)) - | .Call (Sum.inr yulFunctionName) args => - execCall fuel' yulFunctionName vars codeOverride (reverse' (evalArgs fuel' args.reverse codeOverride s)) - | .Var identifier => .ok (s.insert vars.head! s[identifier]!) -- It should be safe to call head! here if the Yul code is parsed correctly. - | .Lit literal => .ok (s.insert vars.head! literal) -- It should be safe to call head! here if the Yul code is parsed correctly. + | .none => .ok (s.zeroFill vars) + | .some expr => multifill' vars (evalValues fuel' expr codeOverride s) + + | .Assign vars expr => + match checkAssignment s vars with + | .error e => .error e + | .ok () => multifill' vars (evalValues fuel' expr codeOverride s) | .If cond body => match eval fuel' cond codeOverride s with @@ -599,13 +655,7 @@ def primCall (fuel : ℕ) (s₀ : State) (prim : Operation .Yul) (args : List Li match eval fuel' cond codeOverride s with | .error e => .error e | .ok (s₁, cond) => - match execSwitchCases fuel' codeOverride s₁ cases' with - | .error e => .error e - | .ok branches => - match exec fuel' (.Block default') codeOverride s₁ with - | .error e => .error e - | .ok s₂ => - (List.foldr (λ (valᵢ, sᵢ) s ↦ if valᵢ = cond then sᵢ else s) (.ok s₂) branches) + exec fuel' (.Block (selectSwitchCase cond default' cases')) codeOverride s₁ -- 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 @@ -659,8 +709,10 @@ def execTopLevel (fuel : Nat) (stmt : Stmt) (s : State) : State := | .error (.MissingContract _) => default | .error (.MissingContractFunction _) => default -- We do not model fallback functions | .error .InvalidExpression => default + | .error (.UnknownIdentifier _) => default + | .error (.DuplicateDeclaration _) => default | .error .YulEXTCODESIZENotImplemented => default - | .error .Revert => s + | .error (.Revert _) => s | .error (.YulHalt s _) => s | .ok s => s diff --git a/EvmYul/Yul/StateOps.lean b/EvmYul/Yul/StateOps.lean index 357d782c..a0d59249 100644 --- a/EvmYul/Yul/StateOps.lean +++ b/EvmYul/Yul/StateOps.lean @@ -16,6 +16,19 @@ def multifill (vars : List Identifier) (vals : List Literal) : Yul.State → Yul | s@(Ok _ _) => (List.zip vars vals).foldr (λ (var, val) s ↦ s.insert var val) s | s => s +def zeroFill (vars : List Identifier) : Yul.State → Yul.State := + vars.foldr (λ var s ↦ s.insert var ⟨0⟩) + +def restrictVarStore (store scope : VarStore) : VarStore := + store.sdiff (store.sdiff scope) + +def restrictStoreTo (scope : VarStore) : Yul.State → Yul.State + | Ok sharedState store => Ok sharedState (restrictVarStore store scope) + | Checkpoint (.Continue sharedState store) => Checkpoint (.Continue sharedState (restrictVarStore store scope)) + | Checkpoint (.Break sharedState store) => Checkpoint (.Break sharedState (restrictVarStore store scope)) + | Checkpoint (.Leave sharedState store) => Checkpoint (.Leave sharedState (restrictVarStore store scope)) + | s => s + -- | Overwrite the EvmYul.Yul.State state of some state. def setSharedState (sharedState : EvmYul.SharedState .Yul) : Yul.State → Yul.State | Ok _ store => Ok sharedState store @@ -53,10 +66,11 @@ def diverge : Yul.State → Yul.State | s => s -- | Initialize function parameters and return values in varstore. -def initcall (params : List Identifier) (args : List Literal) : Yul.State → Yul.State +def initcall (params rets : List Identifier) (args : List Literal) : Yul.State → Yul.State | s@(Ok _ _) => let s₁ := s.setStore default - s₁.multifill params args + let s₂ := s₁.zeroFill rets + 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. @@ -93,13 +107,16 @@ def overwrite? (s s' : Yul.State) : Yul.State := -- STATE QUERIES -- ============================================================================ --- | Lookup the literal associated with an variable in the varstore, returning 0 if not found. +def lookup? (var : Identifier) : Yul.State → Option Literal + | Ok _ store => store.lookup var + | Checkpoint (.Continue _ store) => store.lookup var + | Checkpoint (.Break _ store) => store.lookup var + | Checkpoint (.Leave _ store) => store.lookup var + | _ => .none + +-- | Lookup the literal associated with a 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⟩ + | s => (s.lookup? var).getD ⟨0⟩ -- ============================================================================ -- STATE NOTATION @@ -150,7 +167,7 @@ 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 "☎️⟦" params "," rets "," args "⟧" => Yul.State.initcall params rets args s notation:65 s:64 "✏️⟦" s' "⟧?" => Yul.State.overwrite? s s' notation:64 (priority := high) "🧟" s:max => Yul.State.reviveJump s diff --git a/EvmYul/Yul/YulNotation.lean b/EvmYul/Yul/YulNotation.lean index 5863ae67..65a30ea8 100644 --- a/EvmYul/Yul/YulNotation.lean +++ b/EvmYul/Yul/YulNotation.lean @@ -273,7 +273,7 @@ partial def translateStmt (stmt : TSyntax `stmt) : TermElabM Term := let (lit, cs) := litCase; `(($lit, [$cs,*])) let switchCases ← lits.zip cases |>.mapM f let dflt ← match dflts with - | .none => `([.Break]) + | .none => `([]) | .some dflts => `([$(←dflts.mapM translateStmt),*]) `(Stmt.Switch $expr [$switchCases,*] $dflt) @@ -309,7 +309,7 @@ partial def translateStmt (stmt : TSyntax `stmt) : TermElabM Term := | `(stmt| $ids:ident,* := $expr:expr) => do let ids' := (ids : TSyntaxArray _).map translateIdent let expr ← translateExpr expr - `(Stmt.Let [$ids',*] (.some $expr)) + `(Stmt.Assign [$ids',*] $expr) -- ExprStmt | `(stmt| $expr:expr) => do @@ -373,10 +373,10 @@ example : = Stmt.Break := rfl example : = Stmt.Let ["a", "b"] (.some (.Call (Sum.inr "f") [Expr.Lit ⟨42⟩])) := rfl example : = Stmt.Let ["a"] .none := rfl example : = Stmt.Let ["a"] (.some (.Lit ⟨5⟩)) := rfl -example : = Stmt.Let ["a", "b"] (.some (.Call (Sum.inr "f") [Expr.Lit ⟨42⟩])) := rfl -example : = Stmt.Let ["a"] (.some (.Lit ⟨42⟩)) := rfl +example : = Stmt.Assign ["a", "b"] (.Call (Sum.inr "f") [Expr.Lit ⟨42⟩]) := rfl +example : = Stmt.Assign ["a"] (.Lit ⟨42⟩) := rfl -example : = Stmt.Let ["c"] (.some (Expr.Call (Sum.inl (Operation.StopArith Operation.SAOp.ADD)) [Expr.Var "a", Expr.Var "b"])) := rfl +example : = Stmt.Assign ["c"] (Expr.Call (Sum.inl (Operation.StopArith Operation.SAOp.ADD)) [Expr.Var "a", Expr.Var "b"]) := rfl example : = Stmt.Let ["c"] (.some (Expr.Call (Sum.inl (Operation.StopArith Operation.SAOp.SUB)) [Expr.Var "a", Expr.Var "b"])) := rfl example : = Stmt.Let ["a"] (.some (.Lit ⟨5⟩)) := rfl example : @@ -438,6 +438,11 @@ example : = Stmt.Switch (Expr.Var "a") [(⟨42⟩, [.Continue])] [.Break] := rfl +example : = Stmt.Switch (.Lit ⟨1⟩) [(⟨2⟩, [])] [] := rfl + example : = Stmt.Let ["a", "b", "c"] .none := rfl example : = Stmt.ExprStmtCall (.Call (Sum.inl (.System (.REVERT))) [(Expr.Lit ⟨0⟩), (Expr.Lit ⟨0⟩)]) := rfl example : = Stmt.If (.Lit ⟨1⟩) [Stmt.Leave] := rfl diff --git a/EvmYul/Yul/YulSemanticsTests/Main.lean b/EvmYul/Yul/YulSemanticsTests/Main.lean index 6387de3f..90a07828 100644 --- a/EvmYul/Yul/YulSemanticsTests/Main.lean +++ b/EvmYul/Yul/YulSemanticsTests/Main.lean @@ -1244,6 +1244,177 @@ def test₅ := | .error e => repr e | .ok s => s!"{s.toSharedState.accountMap.toList.map (fun (a : AccountAddress × Account .Yul) => repr a.1 ++ " " ++ repr a.2.storage.toList)}" +def test₆ := + let stmt : Stmt := + .Switch (.Lit ⟨1⟩) + [(⟨1⟩, [])] + [.ExprStmtCall + (.Call (Sum.inl (.System (.REVERT))) [.Lit ⟨0⟩, .Lit ⟨0⟩])] + match exec 99 stmt .none stateEg₁ with + | .error e => repr e + | .ok _ => "selected" + +def showVar? (name : Identifier) : State → String + | .Ok _ store => + match store.lookup name with + | .some value => toString value.toNat + | .none => "none" + | .Checkpoint _ => "checkpoint" + | .OutOfFuel => "out-of-fuel" + +def showExecVar (name : Identifier) (stmt : Stmt) (s : State) : String := + match exec 99 stmt .none s with + | .error e => toString (repr e) + | .ok s => showVar? name s + +def showExecMode (stmt : Stmt) (s : State) : String := + match exec 99 stmt .none s with + | .error e => toString (repr e) + | .ok (.Ok _ _) => "regular" + | .ok (.Checkpoint (.Break _ _)) => "break" + | .ok (.Checkpoint (.Continue _ _)) => "continue" + | .ok (.Checkpoint (.Leave _ _)) => "leave" + | .ok .OutOfFuel => "out-of-fuel" + +def test₇ := + let stmt : Stmt := + .Block + [ .Block [.Let ["x"] (.some (.Lit ⟨1⟩))] + , .Let ["y"] (.some (.Var "x")) + ] + showExecVar "y" stmt stateEg₁ + +def test₈ := + let stmt : Stmt := + .Block + [ .Let ["x"] (.some (.Lit ⟨1⟩)) + , .Block [.Let ["x"] (.some (.Lit ⟨2⟩))] + , .Let ["y"] (.some (.Var "x")) + ] + showExecVar "y" stmt stateEg₁ + +def stateWithX : State := + .Ok stateEg₁.toSharedState ((∅ : VarStore).insert "x" ⟨1⟩) + +def test₉ := + showExecVar "x" (.Assign ["x"] (.Lit ⟨2⟩)) stateWithX + +def test₁₀ := + showExecVar "x" (.Assign ["x"] (.Lit ⟨2⟩)) stateEg₁ + +def auditAddressUInt256 : UInt256 := ⟨100⟩ +def auditCalleeAddressUInt256 : UInt256 := ⟨101⟩ +def auditAddress := AccountAddress.ofUInt256 auditAddressUInt256 +def auditCalleeAddress := AccountAddress.ofUInt256 auditCalleeAddressUInt256 + +def auditStateWithContract (code : YulContract) : State := + let account : Account .Yul := + { code := code + , balance := ⟨1000⟩ + , nonce := ⟨0⟩ + , storage := ∅ + , tstorage := ∅ + } + let accountMap : AccountMap .Yul := (∅ : AccountMap .Yul).insert auditAddress account + let sharedState : SharedState .Yul := + { (Inhabited.default : SharedState .Yul) with + accountMap := accountMap + executionEnv := + { (Inhabited.default : ExecutionEnv .Yul) with + codeOwner := auditAddress + code := code + perm := true + } + } + .Ok sharedState ∅ + +def returnInitContract : YulContract := + { dispatcher := .Block [] + , functions := + (∅ : Finmap (fun (_ : YulFunctionName) ↦ Yul.Ast.FunctionDefinition)) + |>.insert "f" (.Def [] ["r"] []) + } + +def test₁₁ := + let stmt : Stmt := .Let ["x"] (.some (.Call (Sum.inr "f") [])) + showExecVar "x" stmt (auditStateWithContract returnInitContract) + +def callRevertState : State := + let callerCode : YulContract := + { dispatcher := .Block [] + , functions := ∅ + } + let calleeCode : YulContract := + { dispatcher := + .ExprStmtCall + (.Call (Sum.inl (.System (.REVERT))) [.Lit ⟨0⟩, .Lit ⟨0⟩]) + , functions := ∅ + } + let callerAccount : Account .Yul := + { code := callerCode + , balance := ⟨1000⟩ + , nonce := ⟨0⟩ + , storage := ∅ + , tstorage := ∅ + } + let calleeAccount : Account .Yul := + { code := calleeCode + , balance := ⟨0⟩ + , nonce := ⟨0⟩ + , storage := ∅ + , tstorage := ∅ + } + let accountMap : AccountMap .Yul := + ((∅ : AccountMap .Yul).insert auditAddress callerAccount) + |>.insert auditCalleeAddress calleeAccount + let sharedState : SharedState .Yul := + { (Inhabited.default : SharedState .Yul) with + accountMap := accountMap + executionEnv := + { (Inhabited.default : ExecutionEnv .Yul) with + codeOwner := auditAddress + code := callerCode + perm := true + } + } + .Ok sharedState ∅ + +def test₁₂ := + let stmt : Stmt := + .Let ["ok"] + (.some + (.Call (Sum.inl (.System (.CALL))) + [ .Lit ⟨100000⟩ + , .Lit auditCalleeAddressUInt256 + , .Lit ⟨7⟩ + , .Lit ⟨0⟩ + , .Lit ⟨0⟩ + , .Lit ⟨0⟩ + , .Lit ⟨0⟩ + ])) + showExecVar "ok" stmt callRevertState + +def selfdestructState : State := + match callRevertState with + | .Ok sharedState _ => .Ok sharedState ((∅ : VarStore).insert "after" ⟨0⟩) + | s => s + +def test₁₃ := + let stmt : Stmt := + .Block + [ .ExprStmtCall + (.Call (Sum.inl (.System (.SELFDESTRUCT))) [.Lit auditCalleeAddressUInt256]) + , .Assign ["after"] (.Lit ⟨1⟩) + ] + showVar? "after" (execTopLevel 99 stmt selfdestructState) + +def test₁₄ := + let stmt : Stmt := + showExecMode stmt stateEg₁ + end Yul @@ -1259,3 +1430,12 @@ def main : IO Unit := do IO.println (s!"test₃: {test₃} -- " ++ (if s!"{test₃}" = "StaticModeViolation" then "Success" else "Failure")) IO.println (s!"test₄: {test₄} -- " ++ (if s!"{test₄}" = "[1 [], 2 [(0, 5)], 3 [], 4 []]" then "Success" else "Failure")) IO.println (s!"test₅: {test₅} -- " ++ (if s!"{test₅}" = "[1 [], 2 [(0, 5)], 3 [], 4 []]" then "Success" else "Failure")) + IO.println (s!"test₆: {test₆} -- " ++ (if s!"{test₆}" = "selected" then "Success" else "Failure")) + IO.println (s!"test₇: {test₇} -- " ++ (if s!"{test₇}" = "UnknownIdentifier: x" then "Success" else "Failure")) + IO.println (s!"test₈: {test₈} -- " ++ (if s!"{test₈}" = "DuplicateDeclaration: x" then "Success" else "Failure")) + IO.println (s!"test₉: {test₉} -- " ++ (if s!"{test₉}" = "2" then "Success" else "Failure")) + IO.println (s!"test₁₀: {test₁₀} -- " ++ (if s!"{test₁₀}" = "UnknownIdentifier: x" then "Success" else "Failure")) + IO.println (s!"test₁₁: {test₁₁} -- " ++ (if s!"{test₁₁}" = "0" then "Success" else "Failure")) + IO.println (s!"test₁₂: {test₁₂} -- " ++ (if s!"{test₁₂}" = "0" then "Success" else "Failure")) + IO.println (s!"test₁₃: {test₁₃} -- " ++ (if s!"{test₁₃}" = "0" then "Success" else "Failure")) + IO.println (s!"test₁₄: {test₁₄} -- " ++ (if s!"{test₁₄}" = "regular" then "Success" else "Failure")) diff --git a/README.md b/README.md index fbc60f00..72d3531d 100644 --- a/README.md +++ b/README.md @@ -99,4 +99,4 @@ These tests are defined in `EvmYul/Yul/YulSemanticsTests/Main.lean`. ## SELFDESTRUCT -- Halting for `SELFDESTRUCT` is not implemented and the semantics for `SELFDESTRUCT` have limitations, such as not triggering the fallback function in a contract that is the recipient of the ether from the contract the self-destructs. We may remove the semantics for `SELFDESTRUCT` once its status changes from deprecated to not being supported. \ No newline at end of file +- Yul `SELFDESTRUCT` halts execution after applying the modelled account and substate effects. The semantics for `SELFDESTRUCT` still have limitations, such as not triggering the fallback function in a contract that is the recipient of the ether from the contract the self-destructs. We may remove the semantics for `SELFDESTRUCT` once its status changes from deprecated to not being supported.