Fix undisclosed Yul semantics mismatches

danrobinson · danrobinson · commit 66633c59e388 · 2026-05-14T20:35:08.000-07:00
diff --git a/EvmYul/Semantics.lean b/EvmYul/Semantics.lean
@@ -391,7 +391,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
diff --git 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
@@ -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
@@ -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
@@ -143,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₂, _) =>
                             
@@ -235,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₂, _) =>
                         
@@ -320,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)
@@ -394,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)
@@ -462,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₂ =>
@@ -479,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₂ =>
@@ -512,30 +565,47 @@ 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
 
+  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.
 
     - 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.
@@ -545,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
@@ -640,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
@@ -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
@@ -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 : <s break > = Stmt.Break := rfl
 example : <s let a, b := f(42) > = Stmt.Let ["a", "b"] (.some (.Call (Sum.inr "f") [Expr.Lit ⟨42⟩])) := rfl
 example : <s let a > = Stmt.Let ["a"] .none := rfl
 example : <s let a := 5 > = Stmt.Let ["a"] (.some (.Lit ⟨5⟩)) := rfl
-example : <s a, b := f(42) > = Stmt.Let ["a", "b"] (.some (.Call (Sum.inr "f") [Expr.Lit ⟨42⟩])) := rfl
-example : <s a := 42 > = Stmt.Let ["a"] (.some (.Lit ⟨42⟩)) := rfl
+example : <s a, b := f(42) > = Stmt.Assign ["a", "b"] (.Call (Sum.inr "f") [Expr.Lit ⟨42⟩]) := rfl
+example : <s a := 42 > = Stmt.Assign ["a"] (.Lit ⟨42⟩) := rfl
 
-example : <s c := add(a, b) > = Stmt.Let ["c"] (.some (Expr.Call (Sum.inl (Operation.StopArith Operation.SAOp.ADD)) [Expr.Var "a", Expr.Var "b"])) := rfl
+example : <s c := add(a, b) > = Stmt.Assign ["c"] (Expr.Call (Sum.inl (Operation.StopArith Operation.SAOp.ADD)) [Expr.Var "a", Expr.Var "b"]) := rfl
 example : <s let c := sub(a, b) > = Stmt.Let ["c"] (.some (Expr.Call (Sum.inl (Operation.StopArith Operation.SAOp.SUB)) [Expr.Var "a", Expr.Var "b"])) := rfl
 example : <s let a := 5 > = Stmt.Let ["a"] (.some (.Lit ⟨5⟩)) := rfl
 example : <s {} >
diff --git a/EvmYul/Yul/YulSemanticsTests/Main.lean b/EvmYul/Yul/YulSemanticsTests/Main.lean
