Replace s[var]!! notation with GetElem instance

Clear/Interpreter.lean

@@ -103,7 +103,7 @@ mutual
 
       | .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]!!)
+      | .Var id             => (s, s[id]!)
       | .Lit val            => (s, val)
   termination_by fuel + sizeOf expr
   decreasing_by
@@ -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⟧?
@@ -258,7 +258,7 @@ 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 unfold eval; rfl
+lemma Var' : eval fuel (.Var var) s = (s, s[var]!) := by unfold eval; rfl
 
 /--
   A call in an expression.

Clear/State.lean

@@ -25,8 +25,12 @@ inductive State where
   | Checkpoint : Jump → State
 deriving DecidableEq
 
+
+@[reducible]
+def defaultState : State := .Ok default default
+
 instance : Inhabited State where
-  default := .Ok default default
+  default := defaultState
 
 namespace State
 
@@ -158,6 +162,21 @@ def lookup! (var : Identifier) : State → Literal
   | Checkpoint (.Leave _ store) => (store.lookup var).get!
   | _ => 0
 
+instance instGetElemStateIdentifierLiteral : GetElem State Identifier Literal fun _ _ => True where
+  getElem s var _ := lookup! var s
+
+instance : LawfulGetElem State Identifier Literal fun _ _ => True where
+
+instance instGetElemStateStringLiteral : GetElem State String Literal fun _ _ => True where
+  getElem s var _ := lookup! var s
+
+instance : LawfulGetElem State String Literal fun _ _ => True where
+
+@[simp]
+lemma instGetElemStateEq : instGetElemStateIdentifierLiteral = instGetElemStateStringLiteral := by
+  rfl
+
+
 def mload (addr : Literal) : State → Literal
 | Ok e _ | Checkpoint (.Continue e _) | Checkpoint (.Break e _) | Checkpoint (.Leave e _) => EVMState.mload e addr
 | _ => 0
@@ -170,7 +189,6 @@ def mload (addr : Literal) : State → Literal
 
 -- State queries
 -- TODO: make this an GetElem instance
-notation:65 s:64"[" var "]!!" => State.lookup! var s
 notation "❓" => State.isOutOfFuel
 
 -- State transformers
@@ -391,34 +409,64 @@ lemma overwrite?_insert : (s.overwrite? (s'.insert var x)) = s.overwrite? s'
 
 -- | Looking up a variable you've just inserted gives you the value you inserted.
 @[simp]
-lemma lookup_insert : (Ok evm store)⟦var ↦ x⟧[var]!! = x
+lemma lookup_insert : (Ok evm store)⟦var ↦ x⟧[var]! = x
 := by
-  unfold insert lookup!
-  aesop
+  unfold insert instGetElemStateIdentifierLiteral lookup!
+  simp
+  rfl
 
 @[aesop norm simp]
-lemma lookup_insert' (h : isOk s) : s⟦var ↦ x⟧[var]!! = x
+lemma lookup_insert' (h : isOk s) : s⟦var ↦ x⟧[var]! = x
 := by
-  unfold insert lookup!
+  unfold insert instGetElemStateIdentifierLiteral lookup!
   rcases s <;> simp at *
   aesop
 
+-- | It seems in some cases, `s[var]!` is unfolded and then the simplifier is not able to figure it out on its own.
+@[simp]
+lemma lookup_insert'' {y : String} : lookup! y (Ok evm store⟦y↦val⟧) = val := by
+  apply lookup_insert
+
+
 -- | Inserting with the same key twice overwrites.
 @[simp]
 lemma insert_insert : insert var val (insert var val' s) = insert var val s
 := by
   unfold insert
   aesop
 
+-- | Looking up a variable (passed as a string literal) you've just inserted gives you the value you inserted.
+@[simp]
+lemma lookup_insert_string {var : String} : (Ok evm store)⟦var ↦ x⟧[var]! = x
+:= by
+  unfold insert getElem! instGetElemStateStringLiteral lookup!
+  simp
+  rfl
+
+-- | Looking up a variable (passed as a string literal) you've just inserted gives you the value you inserted.
+@[aesop norm simp]
+lemma lookup_insert_string' {var : String} (h : isOk s) : s⟦var ↦ x⟧[var]! = x
+:= by
+  unfold insert getElem! instGetElemStateStringLiteral lookup!
+  rcases s <;> simp at *
+  rfl
 -- | Looking up a variable in a default state returns 0.
 @[simp]
-lemma lookup_default : default[var]!! = 0 := by aesop
+lemma lookup_default : defaultState[var]! = 0 := by aesop
+
+-- | Inserts preserve lookups when the variable you're looking up is different from the one you inserted.
+-- @[aesop unsafe 3% apply (rule_sets := [Clear.aesop_varstore])]
+lemma lookup_insert_of_ne (h : var' ≠ var) : s⟦var ↦ x⟧[var']! = s[var']!
+:= by
+  unfold getElem! instGetElemStateIdentifierLiteral State.lookup! insert
+  rcases s with ⟨evm, store⟩ | _ | _ | _ <;> simp
+  aesop
 
 -- | Inserts preserve lookups when the variable you're looking up is different from the one you inserted.
 -- @[aesop unsafe 3% apply (rule_sets := [Clear.aesop_varstore])]
-lemma lookup_insert_of_ne (h : var' ≠ var) : s⟦var ↦ x⟧[var']!! = s[var']!!
+lemma lookup_insert_string_of_ne {var var' : String} (h : var' ≠ var) : s⟦var ↦ x⟧[var']! = s[var']!
 := by
-  unfold State.lookup! insert
+  unfold getElem! instGetElemStateStringLiteral State.lookup! insert
   rcases s with ⟨evm, store⟩ | _ | _ | _ <;> simp
   aesop
 
@@ -439,27 +487,27 @@ lemma revive_of_ok (h : isOk s) : 🧟s = s
     simp only at h
 
 -- | Revives are transparent to lookups when the state being revived is Ok.
-lemma lookup_revive_of_ok (h : isOk s) : (🧟s)[var]!! = s[var]!!
+lemma lookup_revive_of_ok (h : isOk s) : (🧟s)[var]! = s[var]!
 := by
   rw [revive_of_ok]
   assumption
 
 @[simp]
-lemma lookup_setContinue : (setContinue s)[var]!! = s[var]!!
+lemma lookup_setContinue : (setContinue s)[var]! = s[var]!
 := by
-  unfold lookup! setContinue
+  unfold instGetElemStateIdentifierLiteral lookup! setContinue
   rcases s <;> simp
 
 @[simp]
-lemma lookup_setBreak : (setBreak s)[var]!! = s[var]!!
+lemma lookup_setBreak : (setBreak s)[var]! = s[var]!
 := by
-  unfold lookup! setBreak
+  unfold instGetElemStateIdentifierLiteral lookup! setBreak
   rcases s <;> simp
 
 @[simp]
-lemma lookup_setLeave : (setLeave s)[var]!! = s[var]!!
+lemma lookup_setLeave : (setLeave s)[var]! = s[var]!
 := by
-  unfold lookup! setLeave
+  unfold instGetElemStateIdentifierLiteral lookup! setLeave
   rcases s <;> simp
 
 @[aesop unsafe 10% apply]
@@ -588,22 +636,22 @@ lemma setStore_same : s.setStore s = s
   rcases s <;> simp
 
 @[simp]
-lemma lookup_initcall_1 : (initcall (va :: vars) (a :: vals) (Ok evm store))[va]!! = a
+lemma lookup_initcall_1 : (initcall (va :: vars) (a :: vals) (Ok evm store))[va]! = a
 := by
   unfold initcall
   simp
   rw [lookup_insert']
   aesop
 
-lemma lookup_initcall_2 (ha : vb ≠ va) : (initcall (va :: vb :: vars) (a :: b :: vals) (Ok evm store))[vb]!! = b
+lemma lookup_initcall_2 (ha : vb ≠ va) : (initcall (va :: vb :: vars) (a :: b :: vals) (Ok evm store))[vb]! = b
 := by
   unfold initcall
   simp
   rw [lookup_insert_of_ne ha]
   rw [lookup_insert']
   aesop
 
-lemma lookup_initcall_3 (ha : vc ≠ va) (hb : vc ≠ vb) : (initcall (va :: vb :: vc :: vars) (a :: b :: c :: vals) (Ok evm store))[vc]!! = c
+lemma lookup_initcall_3 (ha : vc ≠ va) (hb : vc ≠ vb) : (initcall (va :: vb :: vc :: vars) (a :: b :: c :: vals) (Ok evm store))[vc]! = c
 := by
   unfold initcall
   simp
@@ -612,7 +660,7 @@ lemma lookup_initcall_3 (ha : vc ≠ va) (hb : vc ≠ vb) : (initcall (va :: vb
   rw [lookup_insert']
   aesop
 
-lemma lookup_initcall_4 (ha : vd ≠ va) (hb : vd ≠ vb) (hc : vd ≠ vc) : (initcall (va :: vb :: vc :: vd :: vars) (a :: b :: c :: d :: vals) (Ok evm store))[vd]!! = d
+lemma lookup_initcall_4 (ha : vd ≠ va) (hb : vd ≠ vb) (hc : vd ≠ vc) : (initcall (va :: vb :: vc :: vd :: vars) (a :: b :: c :: d :: vals) (Ok evm store))[vd]! = d
 := by
   unfold initcall
   simp
@@ -622,7 +670,7 @@ lemma lookup_initcall_4 (ha : vd ≠ va) (hb : vd ≠ vb) (hc : vd ≠ vc) : (in
   rw [lookup_insert']
   aesop
 
-lemma lookup_initcall_5 (ha : ve ≠ va) (hb : ve ≠ vb) (hc : ve ≠ vc) (hd : ve ≠ vd) : (initcall (va :: vb :: vc :: vd :: ve :: vars) (a :: b :: c :: d :: e :: vals) (Ok evm store))[ve]!! = e
+lemma lookup_initcall_5 (ha : ve ≠ va) (hb : ve ≠ vb) (hc : ve ≠ vc) (hd : ve ≠ vd) : (initcall (va :: vb :: vc :: vd :: ve :: vars) (a :: b :: c :: d :: e :: vals) (Ok evm store))[ve]! = e
 := by
   unfold initcall
   simp

Clear/Wheels.lean

@@ -45,7 +45,10 @@ elab "clr_varstore" : tactic => do
     repeat (
       first | rw [State.lookup_insert (by assumption)] at * |
               rw [State.lookup_insert' (by aesop_spec)] at * |
-              rw [State.lookup_insert_of_ne (by decide)] at *
+              rw [State.lookup_insert_of_ne (by decide)] at * |
+              rw [State.lookup_insert_string (by assumption)] at * |
+              rw [State.lookup_insert_string' (by aesop_spec)] at * |
+              rw [State.lookup_insert_string_of_ne (by decide)] at *
     )
   )
   )

Generated/peano/Peano/Common/for_4806375509446804985_user.lean

@@ -14,10 +14,10 @@ section
 
 open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities Peano.Common Generated.peano Peano
 
-def ACond_for_4806375509446804985 (s₀ : State) : Literal := 1 
-def APost_for_4806375509446804985 (s₀ s₉ : State) : Prop := s₉ = s₀⟦"k"↦(s₀["k"]!!) - 1⟧
-def ABody_for_4806375509446804985 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]!! = 0 then 💔 s₀ else s₀⟦"y"↦(s₀["y"]!!) + (s₀["x"]!!)⟧
-def AFor_for_4806375509446804985 (s₀ s₉ : State) : Prop := (s₉["y"]!!) = (s₀["y"]!!) + (s₀["x"]!!) * (s₀["k"]!!) ∧ isPure s₀ s₉ ∧ s₉.isOk
+def ACond_for_4806375509446804985 (s₀ : State) : Literal := 1
+def APost_for_4806375509446804985 (s₀ s₉ : State) : Prop := s₉ = s₀⟦"k"↦(s₀["k"]!) - 1⟧
+def ABody_for_4806375509446804985 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]! = 0 then 💔 s₀ else s₀⟦"y"↦(s₀["y"]!) + (s₀["x"]!)⟧
+def AFor_for_4806375509446804985 (s₀ s₉ : State) : Prop := (s₉["y"]!) = (s₀["y"]!) + (s₀["x"]!) * (s₀["k"]!) ∧ isPure s₀ s₉ ∧ s₉.isOk
 
 lemma for_4806375509446804985_cond_abs_of_code {s₀ fuel} : eval fuel for_4806375509446804985_cond (s₀) = (s₀, ACond_for_4806375509446804985 (s₀)) := by
   unfold eval ACond_for_4806375509446804985
@@ -36,7 +36,7 @@ lemma for_4806375509446804985_concrete_of_body_abs {s₀ s₉ : State} :
   aesop_spec
 
 lemma AZero_for_4806375509446804985 : ∀ s₀, isOk s₀ → ACond_for_4806375509446804985 (👌 s₀) = 0 → AFor_for_4806375509446804985 s₀ s₀ := by
-  unfold ACond_for_4806375509446804985 
+  unfold ACond_for_4806375509446804985
   aesop_spec
 
 lemma AOk_for_4806375509446804985 : ∀ s₀ s₂ s₄ s₅, isOk s₀ → isOk s₂ → ¬ ❓ s₅ → ¬ ACond_for_4806375509446804985 s₀ = 0 → ABody_for_4806375509446804985 s₀ s₂ → APost_for_4806375509446804985 s₂ s₄ → Spec AFor_for_4806375509446804985 s₄ s₅ → AFor_for_4806375509446804985 s₀ s₅
@@ -51,7 +51,7 @@ lemma AOk_for_4806375509446804985 : ∀ s₀ s₂ s₄ s₅, isOk s₀ → isOk
       · simp only [h₇, h₅] at *
         clr_varstore
         ring
-  · have : isOk (s₂⟦"k"↦s₂["k"]!! - 1⟧) := by aesop
+  · have : isOk (s₂⟦"k"↦s₂["k"]! - 1⟧) := by aesop
     simp [h₆.symm] at this
 
 lemma AContinue_for_4806375509446804985 : ∀ s₀ s₂ s₄ s₅, isOk s₀ → isContinue s₂ → ¬ ACond_for_4806375509446804985 s₀ = 0 → ABody_for_4806375509446804985 s₀ s₂ → Spec APost_for_4806375509446804985 (🧟s₂) s₄ → Spec AFor_for_4806375509446804985 s₄ s₅ → AFor_for_4806375509446804985 s₀ s₅ := by

Generated/peano/Peano/Common/for_727972558926940900_user.lean

@@ -15,9 +15,9 @@ section
 open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities Peano.Common Generated.peano Peano
 
 def ACond_for_727972558926940900 (s₀ : State) : Literal := 1
-def APost_for_727972558926940900 (s₀ s₉ : State) : Prop := s₉ = s₀⟦"k"↦(s₀["k"]!!) - 1⟧
-def ABody_for_727972558926940900 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]!! = 0 then 💔 s₀ else s₀⟦"y"↦(s₀["y"]!!) * (s₀["x"]!!)⟧
-def AFor_for_727972558926940900 (s₀ s₉ : State) : Prop := (s₉["y"]!!) =  (s₀["y"]!!) * (s₀["x"]!!) ^ (s₀["k"]!!) ∧ isPure s₀ s₉ ∧ s₉.isOk
+def APost_for_727972558926940900 (s₀ s₉ : State) : Prop := s₉ = s₀⟦"k"↦(s₀["k"]!) - 1⟧
+def ABody_for_727972558926940900 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]! = 0 then 💔 s₀ else s₀⟦"y"↦(s₀["y"]!) * (s₀["x"]!)⟧
+def AFor_for_727972558926940900 (s₀ s₉ : State) : Prop := (s₉["y"]!) =  (s₀["y"]!) * (s₀["x"]!) ^ (s₀["k"]!) ∧ isPure s₀ s₉ ∧ s₉.isOk
 
 lemma for_727972558926940900_cond_abs_of_code {s₀ fuel} : eval fuel for_727972558926940900_cond (s₀) = (s₀, ACond_for_727972558926940900 (s₀)) :=
   by unfold eval ACond_for_727972558926940900; aesop_spec
@@ -54,11 +54,11 @@ lemma AOk_for_727972558926940900 : ∀ s₀ s₂ s₄ s₅, isOk s₀ → isOk s
   rcases s₄ with _ | _ | _ <;> [skip; aesop_spec; skip]
   · clr_spec at h₇
     split_ands <;> [skip; aesop_spec; tauto]
-    by_cases eq : s₀["k"]!! = 0 <;> simp [eq] at h₅ <;> [simp [h₅] at h₂; skip]
+    by_cases eq : s₀["k"]! = 0 <;> simp [eq] at h₅ <;> [simp [h₅] at h₂; skip]
     rw [h₆] at h₇; rw [h₇.1, h₅]; clr_varstore
-    have : ↑(s₀["k"]!! - 1) + 1 < UInt256.size := by simp_arith [fin_eq_lem eq]; zify; omega
+    have : ↑(s₀["k"]! - 1) + 1 < UInt256.size := by simp_arith [fin_eq_lem eq]; zify; omega
     rw [mul_assoc, UInt256.UInt256_pow_succ this]; ring
-  · have h : isOk (s₂⟦"k"↦(s₂["k"]!!) - 1⟧) := by aesop
+  · have h : isOk (s₂⟦"k"↦(s₂["k"]!) - 1⟧) := by aesop
     simp [h₆.symm] at h
 
 lemma AContinue_for_727972558926940900 : ∀ s₀ s₂ s₄ s₅, isOk s₀ → isContinue s₂ → ¬ ACond_for_727972558926940900 s₀ = 0 → ABody_for_727972558926940900 s₀ s₂ → Spec APost_for_727972558926940900 (🧟s₂) s₄ → Spec AFor_for_727972558926940900 s₄ s₅ → AFor_for_727972558926940900 s₀ s₅ := by
@@ -69,7 +69,7 @@ lemma ABreak_for_727972558926940900 : ∀ s₀ s₂, isOk s₀ → isBreak s₂
   unfold ABody_for_727972558926940900 AFor_for_727972558926940900
   have {a : UInt256} : a ^ (0 : Literal) = 1 := rfl
   aesop_spec
-  
+
 lemma ALeave_for_727972558926940900 :  ∀ s₀ s₂, isOk s₀ → isLeave s₂ → ¬ ACond_for_727972558926940900 s₀ = 0 → ABody_for_727972558926940900 s₀ s₂ → AFor_for_727972558926940900 s₀ s₂ := by
   unfold ABody_for_727972558926940900
   aesop_spec

Generated/peano/Peano/Common/for_84821961910748561_user.lean

@@ -11,12 +11,12 @@ set_option autoImplicit false
 
 section
 
-open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities Peano.Common 
+open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities Peano.Common
 
-def ACond_for_84821961910748561 (s₀ : State) : Literal := 1 
-def APost_for_84821961910748561 (s₀ s₉ : State) : Prop := s₉ = s₀⟦"k"↦(s₀["k"]!!) - 1⟧
-def ABody_for_84821961910748561 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]!! = 0 then 💔 s₀ else s₀⟦"x"↦(s₀["x"]!!) + 1⟧
-def AFor_for_84821961910748561 (s₀ s₉ : State) : Prop := (s₀["x"]!!) + (s₀["k"]!!) = (s₉["x"]!!) ∧ isPure s₀ s₉ ∧ s₉.isOk
+def ACond_for_84821961910748561 (s₀ : State) : Literal := 1
+def APost_for_84821961910748561 (s₀ s₉ : State) : Prop := s₉ = s₀⟦"k"↦(s₀["k"]!) - 1⟧
+def ABody_for_84821961910748561 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]! = 0 then 💔 s₀ else s₀⟦"x"↦(s₀["x"]!) + 1⟧
+def AFor_for_84821961910748561 (s₀ s₉ : State) : Prop := (s₀["x"]!) + (s₀["k"]!) = (s₉["x"]!) ∧ isPure s₀ s₉ ∧ s₉.isOk
 
 lemma for_84821961910748561_cond_abs_of_code {s₀ fuel} : eval fuel for_84821961910748561_cond (s₀) = (s₀, ACond_for_84821961910748561 (s₀)) := by
   unfold eval ACond_for_84821961910748561
@@ -45,10 +45,10 @@ lemma AOk_for_84821961910748561 : ∀ s₀ s₂ s₄ s₅, isOk s₀ → isOk s
   rcases s₄ with _ | _ | _ <;> [skip; aesop_spec; skip]
   · clr_spec at h₇
     split_ands <;> [skip; aesop_spec; tauto]
-    by_cases eq : s₀["k"]!! = 0 <;> simp [eq] at h₅ <;> [simp [h₅] at h₂; skip]
+    by_cases eq : s₀["k"]! = 0 <;> simp [eq] at h₅ <;> [simp [h₅] at h₂; skip]
     rw [h₆] at h₇; rw [h₇.1.symm, h₅]; clr_varstore
     ring
-  · have h : isOk (s₂⟦"k"↦(s₂["k"]!!) - 1⟧) := by aesop
+  · have h : isOk (s₂⟦"k"↦(s₂["k"]!) - 1⟧) := by aesop
     simp [h₆.symm] at h
 
 lemma AContinue_for_84821961910748561 : ∀ s₀ s₂ s₄ s₅, isOk s₀ → isContinue s₂ → ¬ ACond_for_84821961910748561 s₀ = 0 → ABody_for_84821961910748561 s₀ s₂ → Spec APost_for_84821961910748561 (🧟s₂) s₄ → Spec AFor_for_84821961910748561 s₄ s₅ → AFor_for_84821961910748561 s₀ s₅ := by

Generated/peano/Peano/Common/if_6183625948864629624_user.lean

@@ -8,9 +8,9 @@ namespace Peano.Common
 
 section
 
-open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities 
+open Clear EVMState Ast Expr Stmt FunctionDefinition State Interpreter ExecLemmas OutOfFuelLemmas Abstraction YulNotation PrimOps ReasoningPrinciple Utilities
 
-def A_if_6183625948864629624 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]!! = 0 then 💔 s₀ else s₀
+def A_if_6183625948864629624 (s₀ s₉ : State) : Prop := s₉ = if s₀["k"]! = 0 then 💔 s₀ else s₀
 
 lemma if_6183625948864629624_abs_of_concrete {s₀ s₉ : State} :
   Spec if_6183625948864629624_concrete_of_code s₀ s₉ →