reasoning principle proof fix

NethermindEth · Mar 30, 2024 · 53993df · 53993df
1 parent 68a4916
commit 53993df
Showing 1 changed file with 10 additions and 12 deletions.
diff --git a/Aether/ReasoningPrinciple.lean b/Aether/ReasoningPrinciple.lean
@@ -186,18 +186,16 @@ lemma reasoning_principle_2
           <;> clear hs₉
           <;> rw [overwrite?_of_isOk (by rw [← hs₀]; simp)] at *
         · generalize hs₂ : Ok evm₂ store₂ = s₂ at *
-          sorry
-          -- rw [revive_of_ok (by rw[← hs₂]; simp only [isOk_Ok])] at hpost
-          -- unfold Spec at hpost
-          -- rw [←hs₂] at hpost
-          -- simp at hpost
-          -- rw [hs₂] at hpost
-          -- have herr₃ : ¬ ❓ s₃ := by rw [hs₄]; apply not_isInfLoop_Spec ih hfuel
-          -- specialize hpost herr₃
-          -- rw [hs₄] at herr₃
-          -- have hok₂ : isOk s₂ := by rw [← hs₂]; simp
-          -- rw [hs₄] at hpost
-          -- exact AOk s₀ s₂ s₄ s₅ hok hok₂ hfuel hcond hbody hpost ih
+          unfold Spec at hpost
+          rw [←hs₂] at hpost
+          simp at hpost
+          rw [hs₂] at hpost
+          have herr₃ : ¬ ❓ s₃ := by rw [hs₄]; apply not_isInfLoop_Spec ih hfuel
+          specialize hpost herr₃
+          rw [hs₄] at herr₃
+          have hok₂ : isOk s₂ := by rw [← hs₂]; simp
+          rw [hs₄] at hpost
+          exact AOk s₀ s₂ s₄ s₅ hok hok₂ hfuel hcond hbody hpost ih
         · exfalso; apply hfuel; simp only [isInfLoop_InfLoop]
         · rcases c₂ with ⟨evm, store⟩ <;> simp at * <;> try rw [overwrite?_of_isOk (by rw [←hs₀]; simp)] at * <;> rw [hs₄] at hpost
           · exact AContinue s₀ _ s₄ s₅ hok (by simp only [isContinue_Continue]) hcond hbody hpost ih