From c71c109df65730a5b153f35299847e7ffd8d1e20 Mon Sep 17 00:00:00 2001 From: cilinder Date: Thu, 11 Sep 2025 14:48:06 +0200 Subject: [PATCH] Replace s[var]!! notation with GetElem instance implement GetElem instance for state and identifier so we can use the standard `s[var]` notation instead of the double exclamation mark. Needed to add some lemmas, so that everything still compiles, for instance so that we can use string literals in place of identifiers and connecting lemmas between the two instances Also added the new lemmas to the clr_varstore tactic so it can handle the example case of peano. --- Clear/Interpreter.lean | 6 +- Clear/State.lean | 92 ++++++++++++++----- Clear/Wheels.lean | 5 +- .../Common/for_4806375509446804985_user.lean | 12 +-- .../Common/for_727972558926940900_user.lean | 14 +-- .../Common/for_84821961910748561_user.lean | 14 +-- .../Common/if_6183625948864629624_user.lean | 4 +- 7 files changed, 99 insertions(+), 48 deletions(-) diff --git a/Clear/Interpreter.lean b/Clear/Interpreter.lean index efad1b21..65a869e1 100644 --- a/Clear/Interpreter.lean +++ b/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. diff --git a/Clear/State.lean b/Clear/State.lean index 29d23ccc..29b9e868 100644 --- a/Clear/State.lean +++ b/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,18 +409,25 @@ 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 @@ -410,15 +435,38 @@ lemma insert_insert : insert var val (insert var val' s) = insert var val s 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,14 +636,14 @@ 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 @@ -603,7 +651,7 @@ lemma lookup_initcall_2 (ha : vb ≠ va) : (initcall (va :: vb :: vars) (a :: b 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 diff --git a/Clear/Wheels.lean b/Clear/Wheels.lean index de70965d..56ecf500 100644 --- a/Clear/Wheels.lean +++ b/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 * ) ) ) diff --git a/Generated/peano/Peano/Common/for_4806375509446804985_user.lean b/Generated/peano/Peano/Common/for_4806375509446804985_user.lean index 4955a57f..96496bba 100644 --- a/Generated/peano/Peano/Common/for_4806375509446804985_user.lean +++ b/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 diff --git a/Generated/peano/Peano/Common/for_727972558926940900_user.lean b/Generated/peano/Peano/Common/for_727972558926940900_user.lean index 714ec0c6..6e234878 100644 --- a/Generated/peano/Peano/Common/for_727972558926940900_user.lean +++ b/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 diff --git a/Generated/peano/Peano/Common/for_84821961910748561_user.lean b/Generated/peano/Peano/Common/for_84821961910748561_user.lean index 7e02a2cc..dad289b1 100644 --- a/Generated/peano/Peano/Common/for_84821961910748561_user.lean +++ b/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 diff --git a/Generated/peano/Peano/Common/if_6183625948864629624_user.lean b/Generated/peano/Peano/Common/if_6183625948864629624_user.lean index eb8d4946..3f706540 100644 --- a/Generated/peano/Peano/Common/if_6183625948864629624_user.lean +++ b/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₉ →