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₉ →