Merge pull request #21 from NethermindEth/fix-deep-recursion-error

Fix deep recursion error if `erc20` is merged with `main`

Clear/ExecLemmas.lean

@@ -23,19 +23,14 @@ variable {s s' : State}
 --  EXEC LEMMAS
 -- ============================================================================
 
-section
-unseal exec
-
 -- | Executing a continue is the same as setting the `jump` field to `Continue`.
-lemma Continue' : exec fuel .Continue s = 🔁 s := by rfl
+lemma Continue' : exec fuel .Continue s = 🔁 s := by unfold exec; rfl
 
 -- | Executing a break is the same as setting the `jump` field to `Break`.
-lemma Break' : exec fuel .Break s = 💔 s := by rfl
+lemma Break' : exec fuel .Break s = 💔 s := by unfold exec; rfl
 
 -- | Executing a `Leave` is the same as setting the `jump` field to `Leave`.
-lemma Leave' : exec fuel .Leave s = 🚪 s := by rfl
-
-end
+lemma Leave' : exec fuel .Leave s = 🚪 s := by unfold exec; rfl
 
 -- | Executing a `Let` binds the given variable names with value 0.
 lemma Let' : exec fuel (.Let vars) s = List.foldr (λ var s ↦ s.insert var 0) s vars := by unfold exec; rfl
@@ -96,13 +91,13 @@ lemma For' : exec fuel (.For cond post body) s =
             | .OutOfFuel                      => s₂✏️⟦s⟧?
             | .Checkpoint (.Break _ _)      => 🧟s₂✏️⟦s⟧?
             | .Checkpoint (.Leave _ _)      => s₂✏️⟦s⟧?
-            | .Checkpoint (.Continue _ _)
+            | .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₆ := by
+              s₆ := by            
   conv_lhs => unfold exec loop
   try rfl -- TODO(update Lean version): rfl is necessary in 4.8.0 because conv no longer does it
 

Clear/Interpreter.lean

@@ -194,7 +194,7 @@ mutual
               | .OutOfFuel                      => s₂✏️⟦s⟧?
               | .Checkpoint (.Break _ _)      => 🧟s₂✏️⟦s⟧?
               | .Checkpoint (.Leave _ _)      => s₂✏️⟦s⟧?
-              | .Checkpoint (.Continue _ _)
+              | .Checkpoint (.Continue _ _) 
               | _ =>
                 let s₃ := exec fuel (.Block post) (🧟 s₂)
                 let s₄ := s₃✏️⟦s⟧?
@@ -234,41 +234,31 @@ variable {s s₀ s₁ : State}
 --  TRAVERSE LEMMAS
 -- ============================================================================
 
-section
-unseal exec
-
 /-
   Traversing an empty list is the identity on states.
 -/
 @[simp]
-lemma nil : exec fuel (.Block []) s = s := by rfl
+lemma nil : exec fuel (.Block []) s = s := by unfold exec; rfl
 
 /--
   Traversing a nonempty list is the same traversing the tail from the state yielded from executing the head.
 -/
 lemma cons : exec fuel (.Block (stmt :: stmts)) s = exec fuel (.Block stmts) (exec fuel stmt s) := by
   conv_lhs => unfold exec
 
-end
-
 -- ============================================================================
 --  EVAL LEMMAS
 -- ============================================================================
 
-section
-unseal eval
-
 /--
   Evaluating a literal gives you back that literal and the state you started in.
 -/
-lemma Lit' : eval fuel (.Lit x) s = (s, x) := by rfl
+lemma Lit' : eval fuel (.Lit x) s = (s, x) := by unfold eval; rfl
 
 /--
   Evaluating a variable does a varstore lookup.
 -/
-lemma Var' : eval fuel (.Var var) s = (s, s[var]!!) := by rfl
-
-end
+lemma Var' : eval fuel (.Var var) s = (s, s[var]!!) := by unfold eval; rfl
 
 /--
   A call in an expression.

Clear/JumpLemmas.lean

@@ -214,7 +214,7 @@ lemma execPrimCall_Jump
 /--
   Evaluating arguments preserves jumps given inductive
   hypotheses that `exec` does so and `eval` does so.
--/
+-/ 
 @[aesop unsafe 10% apply]
 lemma mapAccumr_Jump_ih
   (h : isJump c s)
@@ -249,24 +249,19 @@ lemma evalTail_Jump_ih
   (ih : ∀ {s : State}, isJump c s → sizeOf args < sizeOf expr → isJump c (evalArgs fuel args s).1) :
   isJump c (evalTail fuel args inputs).1 := by unfold evalTail; aesop
 
-section
-unseal evalArgs
-
 lemma evalArgs_Jump_ih
   (h : isJump c s)
   (hsize : sizeOf args < sizeOf expr)
   (eval_ih : ∀ {s} {expr'}, isJump c s → sizeOf expr' < sizeOf expr → isJump c (eval fuel expr' s).1) :
   isJump c (evalArgs fuel args s).1 := by
   induction args generalizing s with
-    | nil => exact h
+    | nil => unfold evalArgs; exact h
     | cons x xs ih =>
       unfold evalArgs
       simp at hsize
       apply @evalTail_Jump_ih expr xs fuel _ _ (eval_ih h ?_) (by linarith) (by assumption)
       linarith
 
-end
-
 /--
   The `call` helper function for user-defined function calls preserves jumps.
 -/
@@ -313,7 +308,7 @@ lemma execPrimCall_evalArgs_Jump_ih
   isJump c (primCall (evalArgs fuel args s).1 prim (evalArgs fuel args s).2.reverse).1 := by
   apply execPrimCall_Jump (evalArgs_Jump_ih _ _ _) <;> aesop
 
-/--
+/-- 
   An `eval` preserves infinite loops.
 -/
 @[aesop unsafe 10% apply]
@@ -471,9 +466,6 @@ lemma If_Jump_ih
 lemma For_Jump (h : isJump c s) :
   isJump c (exec fuel (Stmt.For cond post body) s) := by rw [For']; aesop
 
-section
-unseal exec
-
 /--
   An `exec` preserves infinite loops.
 -/
@@ -509,11 +501,9 @@ lemma exec_Jump (h : isJump c s) : isJump c (exec fuel stmt s)
     · apply Switch_Jump (stmt := Switch cond cases' default') h (by simp_arith) _ (by aesop)
       rcases cases' <;> [aesop; (aesop (config := { warnOnNonterminal := false}); linarith)]
     · exact If_Jump_ih (stmt := If cond body) h (by simp_arith) (by rcases cond <;> aesop)
-    · exact isJump_setContinue h
-    · exact isJump_setBreak h
-    · exact isJump_setLeave h
-
-end
+    · unfold exec; exact isJump_setContinue h
+    · unfold exec; exact isJump_setBreak h
+    · unfold exec; exact isJump_setLeave h
 
 end
 

Clear/OutOfFuelLemmas.lean

@@ -14,7 +14,7 @@ lemma List.exists_append_singleton_of_nonempty {α : Type} {xs : List α}
     rcases h₁ with ⟨last, init, hrev⟩
     rw [←List.reverse_inj] at hrev
     aesop
-
+    
 @[simp]
 lemma List.mapAccumr_nil {α β σ : Type} {f : α → σ → σ × β} {s : σ} :
   List.mapAccumr f [] s = (s, []) := by
@@ -64,7 +64,7 @@ variable {s s₁ s₂ : State}
 @[simp]
 lemma isOutOfFuel_diverge_Ok : isOutOfFuel (diverge (Ok evm store)) := by
   simp [isOutOfFuel, diverge]
-
+  
 /--
   Varstore inserts preserve infinite loops.
 -/
@@ -220,7 +220,7 @@ lemma isOutOfFuel_diverge_mkOk : isOutOfFuel (diverge (mkOk s)) := by
   unfold mkOk diverge isOutOfFuel
   rcases s <;> aesop
 
-/--
+/-- 
   Helper lemma to show that `keccak256` primop preserves infinite loops.
 -/
 lemma isOutOfFuel_keccak256 (h : isOutOfFuel s) :
@@ -334,24 +334,19 @@ lemma evalTail_Inf_ih
   (ih : ∀ {s : State}, isOutOfFuel s → sizeOf args < sizeOf expr → isOutOfFuel (evalArgs fuel args s).1) :
   isOutOfFuel (evalTail fuel args inputs).1 := by unfold evalTail; aesop
 
-section
-unseal evalArgs
-
 lemma evalArgs_Inf_ih
   (h : isOutOfFuel s)
   (hsize : sizeOf args < sizeOf expr)
   (eval_ih : ∀ {s} {expr'}, isOutOfFuel s → sizeOf expr' < sizeOf expr → isOutOfFuel (eval fuel expr' s).1) :
   isOutOfFuel (evalArgs fuel args s).1 := by
   induction args generalizing s with
-    | nil => exact h
+    | nil => unfold evalArgs; exact h
     | cons x xs ih =>
       unfold evalArgs evalTail
       have : sizeOf x < sizeOf expr := by simp at hsize; linarith
       have : sizeOf xs < sizeOf expr := by simp at hsize; linarith
       aesop
 
-end
-
 /--
   The `call` helper function for user-defined function calls preserves infinite loops.
 -/
@@ -451,23 +446,18 @@ lemma evalTail_Inf_ih'
   apply cons'_Inf
   apply ih h
 
-section
-unseal evalArgs
-
 lemma evalArgs_Inf
   (h : isOutOfFuel s)
 : isOutOfFuel (evalArgs fuel args s).1
 := by
   induction args generalizing s with
-    | nil => exact h
+    | nil => unfold evalArgs; exact h
     | cons x xs ih =>
       unfold evalArgs
       apply evalTail_Inf_ih'
       apply eval_Inf h
       assumption
 
-end
-
 -- | Executing a call directly from `exec` preserves infinite loops.
 lemma Call_Inf
   (h : isOutOfFuel s)
@@ -683,9 +673,6 @@ lemma For_Inf
           · apply isOutOfFuel_overwrite?
             assumption
 
-section
-unseal exec
-
 -- | An `exec` preserves infinite loops.
 @[aesop unsafe 10% apply]
 lemma exec_Inf (h : isOutOfFuel s) : isOutOfFuel (exec fuel stmt s)
@@ -741,11 +728,9 @@ lemma exec_Inf (h : isOutOfFuel s) : isOutOfFuel (exec fuel stmt s)
     · apply @If_Inf_ih _ _ (If cond body) _ _ h
       simp_arith
       rcases cond <;> exact ih₁
-    · exact isOutOfFuel_setContinue h
-    · exact isOutOfFuel_setBreak h
-    · exact isOutOfFuel_setLeave h
-
-end
+    · unfold exec; exact isOutOfFuel_setContinue h
+    · unfold exec; exact isOutOfFuel_setBreak h
+    · unfold exec; exact isOutOfFuel_setLeave h
 
 -- ============================================================================
 --  TACTICS