From 8c409aca4101aa7d130c3118da5cd596ad9c4b76 Mon Sep 17 00:00:00 2001 From: Max Vistrup Date: Sat, 25 Jul 2026 14:01:05 +0200 Subject: [PATCH 1/2] Fix handling of observation list in definition of weakestpre. --- Iris/Iris/HeapLang/Completeness.lean | 28 +-- Iris/Iris/HeapLang/PrimitiveLaws.lean | 168 ++++++++---------- .../Iris/ProgramLogic/AbstractWeakestPre.lean | 12 +- Iris/Iris/ProgramLogic/Adequacy.lean | 7 +- Iris/Iris/ProgramLogic/EctxLifting.lean | 80 +++++---- Iris/Iris/ProgramLogic/Lifting.lean | 73 ++++---- Iris/Iris/ProgramLogic/WeakestPre.lean | 61 ++++--- 7 files changed, 223 insertions(+), 206 deletions(-) diff --git a/Iris/Iris/HeapLang/Completeness.lean b/Iris/Iris/HeapLang/Completeness.lean index d7fae5db0..0f7ad1a9c 100644 --- a/Iris/Iris/HeapLang/Completeness.lean +++ b/Iris/Iris/HeapLang/Completeness.lean @@ -111,8 +111,8 @@ theorem wp_base_atomic {e₁ : Exp} {v₂ : Val} (l : Loc) (vlive : Val) (vnew : icases (BigSepM.bigSepM_insert_acc (M := HeapF) (Φ := cellInv) hcell) $$ Hmap with ⟨⟨Hpt, Hmeta⟩, Hclose⟩ iapply wp_lift_atomic_step (EctxLanguage.val_stuck (hbase σ hcell)) - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %hcell1 : ⌜get? (M := HeapF) σ₁.heap l = some (some vlive)⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%hh itrivial @@ -121,7 +121,7 @@ theorem wp_base_atomic {e₁ : Exp} {v₂ : Val} (l : Loc) (vlive : Val) (vnew : simp only [Stuckness.MaybeReducible] exact EctxLanguage.primStep_reducible_of_baseStep_reducible ⟨[], _, _, [], hbase σ₁ hcell1⟩ - iintro !> %e₂ %σ₂ %eₜ %Hprim - + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hprim - obtain ⟨rfl, rfl, rfl, rfl⟩ := hdet hcell1 (EctxLanguage.baseStep_of_primStep_of_baseStep_reducible ⟨[], _, _, [], hbase σ₁ hcell1⟩ Hprim) @@ -130,7 +130,7 @@ theorem wp_base_atomic {e₁ : Exp} {v₂ : Val} (l : Loc) (vlive : Val) (vnew : · ipureintro exact EctxLanguage.primStep_of_baseStep (hbase σ hcell) imodintro - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit have hl0 : l + (0 : Int) = l := by cases l simp only [HAdd.hAdd, Loc.mk.injEq] @@ -305,8 +305,8 @@ theorem wp_baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset) iframe %hatom iintro %Φ Hstep iapply wp_lift_atomic_step (EctxLanguage.val_stuck (BaseStep.allocNS n v σ l hn hfresh)) - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ obtain ⟨lf, hlf⟩ := exists_fresh_block σ₁.heap n have Hred₁ : BaseStep.Reducible (Exp.allocN (.val (.lit (.int n))) (.val v), σ₁) := ⟨[], _, _, [], BaseStep.allocNS n v σ₁ lf hn hlf⟩ @@ -314,10 +314,10 @@ theorem wp_baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset) · ipureintro simp only [Stuckness.MaybeReducible] exact EctxLanguage.primStep_reducible_of_baseStep_reducible Hred₁ - iintro !> %e₂ %σ₂ %eₜ %Hprim - + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hprim - rcases EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred₁ Hprim rename_i l' Hpo Hi - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit icases Hinv with ⟨Hmap, Hproph_inv⟩ imod (genHeap_alloc_big (allocCells l' n.toNat (some v)) σ₁.heap (allocCells_disjoint Hi)) $$ Hσ with ⟨Hσ', Hnewpts, Hnewmeta⟩ @@ -361,8 +361,8 @@ theorem wp_baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset) exact base_step_to_val_atomic Atomicity.StronglyAtomic (BaseStep.newProphS σ p hp) iintro %Φ Hstep iapply wp_lift_atomic_step (EctxLanguage.val_stuck (BaseStep.newProphS σ p hp)) - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ obtain ⟨pf, Hpf⟩ := Std.List.fresh σ₁.usedProphId.toList have Hpf_contains : ¬ σ₁.usedProphId.contains pf := by intro hc; exact Hpf (Std.ExtTreeSet.mem_toList.mpr hc) @@ -372,13 +372,13 @@ theorem wp_baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset) · ipureintro simp only [Stuckness.MaybeReducible] exact EctxLanguage.primStep_reducible_of_baseStep_reducible Hred₁ - iintro !> %e₂ %σ₂ %eₜ %Hprim - + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hprim - cases EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred₁ Hprim rename_i p' Hp' - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit have Hp'_mem : p' ∉ σ₁.usedProphId := fun hmem => Hp' (Std.ExtTreeSet.mem_iff_contains.symm.mp hmem) - imod (ProphMap.new_proph p' σ₁.usedProphId obs' Hp'_mem) $$ Hproph + imod (ProphMap.new_proph p' σ₁.usedProphId obs Hp'_mem) $$ Hproph with ⟨Hproph', Htok⟩ icases Hinv with ⟨Hmap, Hproph_inv⟩ ihave %Hfresh_σ : ⌜p' ∉ σ.usedProphId⌝ $$ [Hproph_inv Htok] @@ -412,7 +412,7 @@ theorem wp_baseCompletenessGoal (e₁ : Exp) (σ : State) (E : CoPset) iapply (BigSepS.bigSepS_union hdisj).mpr iframe iapply BigSepS.bigSepS_singleton.mpr - iexists (prophListResolves obs' p') + iexists (prophListResolves obs p') iexact Htok | resolveS p v e σ w σ' κs ts hbase hp => have IH : heapInv (GF := GF) σ ⊢ iprop(|={E}=> baseCompletenessGoal e σ E) := diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index b696b2d27..724911fb4 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -147,20 +147,20 @@ theorem wp_fork {e : Exp} : WP hl(fork(&e)) @ s; E {{ Φ }} := by iintro HΦ Hwp iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ have Hred : BaseStep.Reducible (hl(fork(&e)), σ₁) := ⟨[], hl(#BaseLit.unit), σ₁, [e], by constructor⟩ isplitr · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact (primStep_reducible_of_baseStep_reducible Hred) - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit imodintro isplitl [Hσ Hproph] - · iapply (stateInterp_split σ₁ (ns + 1) obs' (nt + [e].length)).mpr + · iapply (stateInterp_split σ₁ (ns + 1) obs (nt + [e].length)).mpr iframe isplitr [Hwp] · iexists _ @@ -174,21 +174,21 @@ theorem wp_fork_fupd {e : Exp} : WP hl(fork(&e)) @ s; E {{ Φ }} := by iintro HeΦ iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ have Hred : BaseStep.Reducible (hl(fork(&e)), σ₁) := ⟨[], hl(#BaseLit.unit), σ₁, [e], by constructor⟩ isplitr · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit imod HeΦ with ⟨Hwp, HΦ⟩ imodintro isplitl [Hσ Hproph] - · iapply (stateInterp_split σ₁ (ns + 1) obs' (nt + [e].length)).mpr + · iapply (stateInterp_split σ₁ (ns + 1) obs (nt + [e].length)).mpr iframe Hσ Hproph isplitr [Hwp] · iexists _ @@ -202,8 +202,8 @@ theorem wp_alloc (v : Val) (Φ : Val → IProp GF ) : WP hl(ref(&v)) @ s; E {{ Φ }} := by iintro HΦ iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ let l := (List.fresh σ₁.heap.keys).choose have Hne : σ₁.get? l = .none := by simpa [State.get?, get?, getElem?_eq_none_iff, ←Std.ExtTreeMap.mem_keys] @@ -219,10 +219,10 @@ theorem wp_alloc (v : Val) (Φ : Val → IProp GF ) : · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr rcases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i l' Hpo Hi - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [stateInterp, Int.cast_ofNat_Int, Algebra.BigOpL.bigOpL_nil, Int.toNat_one, List.range_one, List.foldl_cons, List.foldl_nil] specialize Hi 0 (by simp) (by simp) @@ -241,8 +241,8 @@ theorem wp_load {l : Loc} {q} {v : Val} Φ : WP hl(!v(#l)) @ s; E {{ Φ }} := by iintro >Hpt HΦ iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = v⌝ $$ [Hσ Hpt] · ihave >%_ := genHeap_valid $$ [$Hσ $Hpt] itrivial @@ -254,13 +254,13 @@ theorem wp_load {l : Loc} {q} {v : Val} Φ : · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i v'' H rw [Hpt] at H; simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [stateInterp, Algebra.BigOpL.bigOpL_nil] iframe Hσ Hproph imodintro @@ -275,8 +275,8 @@ theorem wp_store {l : Loc} {v v' : Val} Φ : WP hl(v(#l) ← &v) @ s; E {{ Φ }} := by iintro >Hpt HΦ iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v')⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -288,13 +288,13 @@ theorem wp_store {l : Loc} {v v' : Val} Φ : · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i v'' H rw [Hpt] at H; simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, List.foldl_nil, Algebra.BigOpL.bigOpL_nil] rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] @@ -315,8 +315,8 @@ theorem wp_cmpXchg_fail {l : Loc} {q} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp {{ v'', ⌜v'' = hl_val((&v', #false))⌝ ∗ l ↦{q} some v' }}) := by iintro >Hpt iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v')⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -329,13 +329,13 @@ theorem wp_cmpXchg_fail {l : Loc} {q} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i Heq4 H rw [Hpt] at H simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [Algebra.BigOpL.bigOpL_nil] subst Heq4; simp only [toVal] at Heq1 Heq2 obtain ⟨rfl⟩ := Heq1 @@ -358,8 +358,8 @@ theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v {{ v'', ⌜v'' = hl_val((&v', #true))⌝ ∗ l ↦ some v2 }} := by iintro >Hpt iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v')⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -372,13 +372,13 @@ theorem wp_cmpXchg_true {l : Loc} {v' : Val} {e1 : Exp} {v1 : Val} {e2 : Exp} {v · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i v1' v2' vl' _ _ Heq4 H rw [Hpt] at H simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H subst H - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [stateInterp, Algebra.BigOpL.bigOpL_nil] subst Heq4; simp only [toVal] at Heq1 Heq2 obtain ⟨rfl⟩ := Heq1 @@ -399,8 +399,8 @@ theorem wp_free {l : Loc} {v : Val} : ▷ (l ↦ some v) ⊢ WP hl(free(#l)) @ s; E {{ v'', ⌜v'' = hl_val(#())⌝ ∗ l ↦ none }} := by iintro >Hpt iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v)⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -413,9 +413,9 @@ theorem wp_free {l : Loc} {v : Val} : · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr rcases baseStep_of_primStep_of_baseStep_reducible Hred Heq with ⟨v'', H⟩ - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, List.foldl_nil, Algebra.BigOpL.bigOpL_nil] rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] @@ -433,8 +433,8 @@ theorem wp_xchg {l : Loc} {v w : Val} : ▷ (l ↦ some v) ⊢ WP hl(xchg(#l, &w)) @ s; E {{ v'', ⌜v'' = v⌝ ∗ l ↦ some w }} := by iintro >Hpt iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some v)⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -446,13 +446,13 @@ theorem wp_xchg {l : Loc} {v w : Val} : · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr rcases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i v1' H obtain rfl : v = v1' := by simp only [Hpt, Option.pure_def, Option.bind_eq_bind, Option.bind_some, Option.some.injEq] at H exact H - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, List.foldl_nil, Algebra.BigOpL.bigOpL_nil] rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] @@ -469,8 +469,8 @@ theorem wp_faa {l : Loc} {i1 i2 : Int} : ⊢ WP hl(faa(#l, #i2)) @ s; E {{ v'', ⌜v'' = hl_val(#i1)⌝ ∗ l ↦ some hl_val(#(i1 + i2)) }} := by iintro >Hpt iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ ihave %Hpt : ⌜σ₁.get? l = .some (.some (Val.lit (.int i1)))⌝ $$ [Hσ Hpt] · icases genHeap_valid $$ [$Hσ $Hpt] with >%Heq' itrivial @@ -482,13 +482,13 @@ theorem wp_faa {l : Loc} {i1 i2 : Int} : · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i i1' H obtain rfl : i1 = i1' := by simp only [Hpt, Option.some.injEq, Val.lit.injEq, BaseLit.int.injEq] at H exact H - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit simp only [stateInterp, Int.toNat_one, List.range_one, List.foldl_cons, Int.cast_ofNat_Int, List.foldl_nil, Algebra.BigOpL.bigOpL_nil] rw [show l + (0 : Int) = l by cases l; simp only [HAdd.hAdd, Loc.mk.injEq]; grind] @@ -504,8 +504,8 @@ theorem wp_faa {l : Loc} {i1 i2 : Int} : theorem wp_new_proph : ⊢ WP hl(newProph()) @ s; E {{ v, ∃ p, ∃ pvs, ⌜v = .lit (.prophecy p)⌝ ∗ proph p pvs }} := by iapply wp_lift_atomic_step rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ !> - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ + iintro %σ₁ %ns %obs %nt Hσ !> + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hσ, Hproph⟩ obtain ⟨pf, Hpf⟩ := Iris.Std.List.fresh σ₁.usedProphId.toList have Hpf_contains : ¬ σ₁.usedProphId.contains pf := by intro hc; exact Hpf (Std.ExtTreeSet.mem_toList.mpr hc) @@ -515,13 +515,13 @@ theorem wp_new_proph : · ipureintro cases s <;> simp only [Stuckness.MaybeReducible] exact primStep_reducible_of_baseStep_reducible Hred - iintro !> %e₂ %σ₂ %eₜ %Heq Hcr + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Heq Hcr cases baseStep_of_primStep_of_baseStep_reducible Hred Heq rename_i p' Hp' - ihave Hproph := (prophMapInterp_nil_append obs' σ₁.usedProphId).mp $$ Hproph + subst Hsplit have Hp'_mem : p' ∉ σ₁.usedProphId := fun hmem => Hp' (Std.ExtTreeSet.mem_iff_contains.symm.mp hmem) - imod ProphMap.new_proph p' σ₁.usedProphId obs' Hp'_mem $$ Hproph with ⟨Hproph', Htok⟩ + imod ProphMap.new_proph p' σ₁.usedProphId obs Hp'_mem $$ Hproph with ⟨Hproph', Htok⟩ imodintro simp only [stateInterp] iframe Hσ @@ -546,9 +546,9 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × WP hl(resolve(&e, v(#p), v(&w))) @ s; E {{ Φ }} := by iintro Hp HWPe iapply wp_lift_step_fupdN rfl - iintro %σ₁ %ns %obs %obs' %nt Hσ - icases (stateInterp_split σ₁ ns (obs ++ obs') nt).mp $$ Hσ with ⟨Hheap, Hpmap⟩ - icases ProphMap.agree (obs ++ obs') σ₁.usedProphId p pvs $$ [$Hpmap $Hp] with %Hagree + iintro %σ₁ %ns %obs %nt Hσ + icases (stateInterp_split σ₁ ns obs nt).mp $$ Hσ with ⟨Hheap, Hpmap⟩ + icases ProphMap.agree obs σ₁.usedProphId p pvs $$ [$Hpmap $Hp] with %Hagree have hredR : Stuckness.MaybeReducible s (e, σ₁) → Stuckness.MaybeReducible s (hl(resolve(&e, v(#p), v(&w))), σ₁) := fun Hred_e => by cases s <;> simp only [Stuckness.MaybeReducible] at Hred_e ⊢ @@ -560,47 +560,33 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _ by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe - cases obs using List.reverseRec with - | nil => - ihave Hσ_e : iprop(stateInterp σ₁ ns ([] ++ obs') nt) $$ [Hheap Hpmap] - · iapply (stateInterp_split σ₁ ns ([] ++ obs') nt).mpr; iframe Hheap; iexact Hpmap - imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, _⟩ - imodintro - isplitr - · ipureintro; exact hredR Hred_e - iintro %e₂ %σ₂ %eₜ %Hstep _ - exfalso - obtain ⟨_, _, hκ_eq, _, _⟩ := step_resolve_decompose Hstep - exact List.cons_ne_nil _ _ (List.append_eq_nil_iff.mp hκ_eq.symm).2 - | append_singleton init lastObs ih => - clear ih - have hassoc : (init ++ [lastObs]) ++ obs' = init ++ (lastObs :: obs') := by simp - ihave Hσ_e : iprop(stateInterp σ₁ ns (init ++ (lastObs :: obs')) nt) $$ [Hheap Hpmap] - · iapply (stateInterp_split σ₁ ns (init ++ (lastObs :: obs')) nt).mpr - iframe Hheap; rw [← hassoc]; iexact Hpmap - imod HWPe $$ %_ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, HWPe⟩ - imodintro - isplitr - · ipureintro; exact hredR Hred_e - iintro %e₂ %σ₂ %eₜ %Hstep Hcred - obtain ⟨κ_inner, v_inner, hκ_eq, rfl, Hbase_e⟩ := step_resolve_decompose Hstep - obtain ⟨rfl, rfl⟩ := (by simpa using congrArg List.reverse hκ_eq : lastObs = _ ∧ init = κ_inner) - ispecialize HWPe $$ %_ %_ %_ %(EctxLanguage.primStep_of_baseStep Hbase_e) Hcred - iapply step_fupdN_wand $$ HWPe - iintro HWPe - imod HWPe with ⟨Hσ_post, HWPval, Hefs⟩ - icases (stateInterp_split σ₂ (ns + 1) ((p, (v_inner, w)) :: obs') (nt + eₜ.length)).mp - $$ Hσ_post with ⟨Hheap_e, Hpmap_e⟩ - imod wp_value_fupd'.mp $$ HWPval with ⟨%pvs', Hele, HΦ⟩ - icombine Hpmap_e Hele as Hcomb - imod (ProphMap.resolve_proph p (v_inner, w) obs' σ₂.usedProphId pvs') $$ Hcomb - with ⟨%pvs'', %hpvs'_eq, Hpmap_e, Hele⟩ - imodintro - iframe - isplitl [Hheap_e Hpmap_e] - · iapply (stateInterp_split σ₂ (ns + 1) obs' (nt + eₜ.length)).mpr $$ [$] - iapply wp_value' - iapply HΦ $$ %pvs'' %hpvs'_eq Hele + ihave Hσ_e : iprop(stateInterp σ₁ ns obs nt) $$ [Hheap Hpmap] + · iapply (stateInterp_split σ₁ ns obs nt).mpr; iframe Hheap; iexact Hpmap + imod HWPe $$ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, HWPe⟩ + imodintro + isplitr + · ipureintro; exact hredR Hred_e + iintro %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred + obtain ⟨κ_inner, v_inner, hκ_eq, rfl, Hbase_e⟩ := step_resolve_decompose Hstep + have Hsplit_e : obs = κ_inner ++ ((p, (v_inner, w)) :: obs') := by + rw [Hsplit, hκ_eq]; simp [List.append_assoc] + ispecialize HWPe $$ %_ %_ %_ %κ_inner %((p, (v_inner, w)) :: obs') %Hsplit_e + %(EctxLanguage.primStep_of_baseStep Hbase_e) Hcred + iapply step_fupdN_wand $$ HWPe + iintro HWPe + imod HWPe with ⟨Hσ_post, HWPval, Hefs⟩ + icases (stateInterp_split σ₂ (ns + 1) ((p, (v_inner, w)) :: obs') (nt + eₜ.length)).mp + $$ Hσ_post with ⟨Hheap_e, Hpmap_e⟩ + imod wp_value_fupd'.mp $$ HWPval with ⟨%pvs', Hele, HΦ⟩ + icombine Hpmap_e Hele as Hcomb + imod (ProphMap.resolve_proph p (v_inner, w) obs' σ₂.usedProphId pvs') $$ Hcomb + with ⟨%pvs'', %hpvs'_eq, Hpmap_e, Hele⟩ + imodintro + iframe + isplitl [Hheap_e Hpmap_e] + · iapply (stateInterp_split σ₂ (ns + 1) obs' (nt + eₜ.length)).mpr $$ [$] + iapply wp_value' + iapply HΦ $$ %pvs'' %hpvs'_eq Hele theorem wp_resolve {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × Val)} (hatom : Language.Atomic Language.Atomicity.StronglyAtomic e) (hne : toVal e = none) : diff --git a/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean b/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean index a32c0928b..36b83d44f 100644 --- a/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean +++ b/Iris/Iris/ProgramLogic/AbstractWeakestPre.lean @@ -168,14 +168,14 @@ theorem wp_inv_open_maybe_of_not_val {e : Expr} {E₁ E₂ : CoPset} {Φ : Val simp only [wp.pre, coe_of_toVal_eq_some He', Hnv] itrivial · dsimp only - iintro %σ %n %κ %κs %n₂ Hσ + iintro %σ %n %obs %n₂ Hσ imod Hwp $$ Hσ with ⟨%Hred, Hc⟩ imodintro have aux := Context.reducible_fill K Hred iframe %aux; clear aux - iintro %e₂ %σ₂ %efs %H Hlc + iintro %e₂ %σ₂ %efs %κ %obs' %Hsplit %H Hlc obtain ⟨e₂, rfl, Hprim⟩ := Context.primStep_fill_inv (toVal_none_of_reducible Hred) H - ispecialize Hc $$ %e₂ %σ₂ %efs %Hprim Hlc + ispecialize Hc $$ %e₂ %σ₂ %efs %κ %obs' %Hsplit %Hprim Hlc iapply step_fupdN_mono $$ Hc iintro Hc imod Hc with ⟨Hst, Hwp, $⟩ @@ -183,9 +183,9 @@ theorem wp_inv_open_maybe_of_not_val {e : Expr} {E₁ E₂ : CoPset} {Φ : Val icases wp_unfold $$ Hwp with Hwp unfold wp.pre rcases He₂' : toVal e₂ with (_|v₂) <;> dsimp only - · imod Hwp $$ %_ %_ %κs %.nil [Hst] with ⟨%Hredu, H⟩ - · rw [List.append_nil κs]; iframe - grind + · ispecialize Hwp $$ %σ₂ %(n + 1) %obs' %(n₂ + efs.length) + imod Hwp $$ Hst with ⟨%Hredu, _⟩ + exact (Language.not_reducible_iff_irreducible.mpr Hprim Hredu).elim · imod Hwp with >Hwp rw [coe_of_toVal_eq_some He₂'] iframe diff --git a/Iris/Iris/ProgramLogic/Adequacy.lean b/Iris/Iris/ProgramLogic/Adequacy.lean index 19b451411..ae2da3d94 100644 --- a/Iris/Iris/ProgramLogic/Adequacy.lean +++ b/Iris/Iris/ProgramLogic/Adequacy.lean @@ -47,9 +47,9 @@ theorem wp_step (s : Stuckness) (e1 : Expr) (σ1 : State) rw [wp_unfold.to_eq] simp only [wp.pre, Language.val_stuck Hstep] iintro Hσ Hcred Hwp - imod Hwp $$ %σ1 %ns %κ %κs %nt Hσ with ⟨%_, Hcont⟩ + imod Hwp $$ %σ1 %ns %(κ ++ κs) %nt Hσ with ⟨%_, Hcont⟩ imodintro - ihave Hcont := Hcont $$ %e2 %σ2 %efs %Hstep Hcred + ihave Hcont := Hcont $$ %e2 %σ2 %efs %κ %κs [//] %Hstep Hcred iapply step_fupdN_wand $$ Hcont iintro >⟨HSI, Hwp2, Hefs⟩ imodintro @@ -103,8 +103,7 @@ theorem wp_not_stuck (κs : List Obs) (nt : Nat) (e : Expr) (σ : State) | none => dsimp only iintro Hst Hcont - ispecialize Hcont $$ %σ %ns %([]) %κs %nt - rw [List.nil_append] + ispecialize Hcont $$ %σ %ns %κs %nt imod Hcont $$ Hst with ⟨%H, _⟩ imodintro ipureintro diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean index 20a498365..a91445f10 100644 --- a/Iris/Iris/ProgramLogic/EctxLifting.lean +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -20,50 +20,54 @@ variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} @[rocq_alias wp_lift_base_step_fupd] theorem wp_lift_base_step_fupd (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E,∅}=∗ ⌜BaseStep.Reducible (e₁,σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁,σ₁) -->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=> + ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁,σ₁) -<κ>->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=> stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro H iapply wp_lift_step_fupd h - iintro %σ₁ %ns %obs %obs' %nt Hσ + iintro %σ₁ %ns %obs %nt Hσ imod H $$ Hσ with ⟨%Hred, H⟩ imodintro isplit · ipureintro grind [primStep_reducible_of_baseStep_reducible] - iintro %e₂ %σ₂ %eₜ %Hstep - iapply H $$ %_ %_ %_ + iintro %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep + iapply H $$ %_ %_ %_ %_ %_ %Hsplit ipureintro exact baseStep_of_primStep_of_baseStep_reducible Hred Hstep @[rocq_alias wp_lift_base_step] theorem wp_lift_base_step (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E,∅}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ - ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅,E}=∗ + ▷ ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅,E}=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro H iapply wp_lift_base_step_fupd h - iintro %σ₁ %ns %obs %obs' %nt Hσ + iintro %σ₁ %ns %obs %nt Hσ imod H $$ [$] with ⟨$, H⟩ - iintro !> %e₂ %σ₂ %eₜ %Hbstep Hcred !> !> - iapply H $$ %_ %_ %_ %Hbstep Hcred + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hbstep Hcred !> !> + iapply H $$ %_ %_ %_ %_ %_ %Hsplit %Hbstep Hcred @[rocq_alias wp_lift_base_stuck] theorem wp_lift_base_stuck (h : toVal e = none) : SubredexesAreValues e → - (∀ σ ns obs' nt, stateInterp σ ns obs' nt ={E,∅}=∗ ⌜BaseStep.Stuck (e,σ)⌝) + (∀ σ ns obs nt, stateInterp σ ns obs nt ={E,∅}=∗ ⌜BaseStep.Stuck (e,σ)⌝) ⊢ WP e @ E ? {{ Φ }} := by iintro %sav_e H iapply wp_lift_stuck h - iintro %σ %ns %obs' %nt Hσ + iintro %σ %ns %obs %nt Hσ imod H $$ Hσ with %H ipureintro exact primStep_stuck_of_baseStep_stuck H sav_e @@ -75,7 +79,7 @@ theorem wp_lift_pure_base_stuck (h : toVal e = none) : ⊢ WP e @ E ?{{ Φ }} := by iintro %sav_e %Hstuck iapply wp_lift_base_stuck h sav_e - iintro %σ %ns %obs' %nt Hσ + iintro %σ %ns %obs %nt Hσ iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro - ipureintro @@ -83,61 +87,67 @@ theorem wp_lift_pure_base_stuck (h : toVal e = none) : @[rocq_alias wp_lift_atomic_base_step_fupd] theorem wp_lift_atomic_base_step_fupd (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E₁}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ + ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro H iapply wp_lift_atomic_step_fupd (E₂ := E₂) h - iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + iintro %σ₁ %ns %obs %nt Hσ₁ imod H $$ Hσ₁ with ⟨%Hbred, H⟩ imodintro isplit · ipureintro; grind only [primStep_reducible_of_baseStep_reducible] - iintro %_ %_ %_ %Hstep - iapply H + iintro %_ %_ %_ %κ %obs' %Hsplit %Hstep + iapply H $$ %_ %_ %_ %_ %_ %Hsplit ipureintro exact baseStep_of_primStep_of_baseStep_reducible Hbred Hstep @[rocq_alias wp_lift_atomic_base_step] theorem wp_lift_atomic_base_step (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ - ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + ▷ ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro H iapply wp_lift_atomic_step h - iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + iintro %σ₁ %ns %obs %nt Hσ₁ imod H $$ Hσ₁ with ⟨%Hbred, H⟩ imodintro isplit · ipureintro; grind only [primStep_reducible_of_baseStep_reducible] inext - iintro %e₂ %σ₂ %eₜ %Hstep Hcred - iapply H $$ %_ %_ %_ [] Hcred + iintro %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred + iapply H $$ %_ %_ %_ %_ %_ %Hsplit [] Hcred ipureintro exact baseStep_of_primStep_of_baseStep_reducible Hbred Hstep @[rocq_alias wp_lift_atomic_base_step_no_fork_fupd] theorem wp_lift_atomic_base_step_no_fork_fupd (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E₁}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ + ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v)) ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro H iapply wp_lift_atomic_base_step_fupd (E₂ := E₂) h - iintro %σ₁ %ns %obs %obs' %nt Hσ₁ - imod H $$ %_ %_ %_ %_ %_ Hσ₁ with ⟨$, H⟩ + iintro %σ₁ %ns %obs %nt Hσ₁ + imod H $$ %_ %_ %_ %_ Hσ₁ with ⟨$, H⟩ imodintro - iintro %_ %_ %_ %Hbstep Hcred - imod H $$ %_ %_ %_ %Hbstep Hcred with H + iintro %_ %_ %_ %κ %obs' %Hsplit %Hbstep Hcred + imod H $$ %_ %_ %_ %_ %_ %Hsplit %Hbstep Hcred with H iintro !> !> imod H with ⟨%h, _, _⟩ subst h @@ -147,19 +157,21 @@ theorem wp_lift_atomic_base_step_no_fork_fupd (h : toVal e₁ = none) : @[rocq_alias wp_lift_atomic_base_step_no_fork] theorem wp_lift_atomic_base_step_no_fork (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ - ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + ▷ ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v)) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro H iapply wp_lift_atomic_base_step h - iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + iintro %σ₁ %ns %obs %nt Hσ₁ imod H $$ Hσ₁ with ⟨$, H⟩ imodintro inext - iintro %v2 %σ₂ %eₜ %Hstep Hcred - imod H $$ %_ %_ %_ %Hstep Hcred with ⟨%h, _, _⟩ + iintro %v2 %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred + imod H $$ %_ %_ %_ %_ %_ %Hsplit %Hstep Hcred with ⟨%h, _, _⟩ subst h imodintro simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index 28ce47eba..efdc33b16 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -22,10 +22,12 @@ variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} @[rocq_alias wp_lift_step_fupdN] theorem wp_lift_step_fupdN (h : toVal e₁ = none) : - (∀ σ₁ ns (obs obs' : List Obs) nt, - stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + (∀ σ₁ ns (obs : List Obs) nt, + stateInterp σ₁ ns obs nt ={E,∅}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ + ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>-> (e₂,σ₂, eₜ)⌝ -∗ £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ WP e₂ @ s; E {{ Φ }} ∗ @@ -34,24 +36,26 @@ theorem wp_lift_step_fupdN (h : toVal e₁ = none) : @[rocq_alias wp_lift_step_fupd] theorem wp_lift_step_fupd (h : toVal e₁ = none) : - (∀ σ₁ ns (obs obs' : List Obs) nt, - stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + (∀ σ₁ ns (obs : List Obs) nt, + stateInterp σ₁ ns obs nt ={E,∅}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ + ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>-> (e₂,σ₂, eₜ)⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=> stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by refine .trans ?_ <| wp_lift_step_fupdN h - iintro Hwp %σ₁ %ns %obs %obs' %nt Hσ + iintro Hwp %σ₁ %ns %obs %nt Hσ imod Hwp $$ Hσ with ⟨$, Hwp⟩ - iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred ihave Hcred := lc_weaken 1 (Nat.le_add_left 1 (ι.numLatersPerStep ns)) $$ Hcred refine .trans ?_ <| step_fupd_mono <| (laterN_intro _).trans <| step_fupdN_intro Std.LawfulSet.empty_subset iintro ⟨Hwp, Hcred⟩ - imod Hwp $$ %_ %_ %_ %Hstep Hcred with Hwp + imod Hwp $$ %_ %_ %_ %_ %_ %Hsplit %Hstep Hcred with Hwp iapply step_fupd_intro Std.LawfulSet.empty_subset iassumption @@ -62,32 +66,34 @@ theorem wp_lift_stuck (h : toVal e = none) : iintro H rw [wp_unfold.to_eq] simp only [wp.pre, h] - iintro %σ₁ %ns %obs %obs' %nt Hσ + iintro %σ₁ %ns %obs %nt Hσ imod H $$ Hσ with %Hirr replace ⟨_, Hirr⟩ := Hirr imodintro isplit · ipureintro; simp [Stuckness.MaybeReducible] - iintro %e₂ %σ₂ %eₜ %Hstep - nomatch Hirr obs e₂ σ₂ eₜ Hstep + iintro %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep + nomatch Hirr κ e₂ σ₂ eₜ Hstep /-! ## Derived lifting lemmas -/ @[rocq_alias wp_lift_step] theorem wp_lift_step (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E,∅}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={∅,E}=∗ + ▷ ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={∅,E}=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro H iapply wp_lift_step_fupd h - iintro %σ₁ %ns %obs %obs' %nt Hσ - imod H $$ %_ %_ %_ %_ %_ Hσ with ⟨$, H⟩ - iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> - iapply H $$ %_ %_ %_ %Hstep Hcred + iintro %σ₁ %ns %obs %nt Hσ + imod H $$ %_ %_ %_ %_ Hσ with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred !> !> + iapply H $$ %_ %_ %_ %_ %_ %Hsplit %Hstep Hcred @[rocq_alias wp_lift_pure_step_no_fork] theorem wp_lift_pure_step_no_fork [Inhabited State] (E₂ : CoPset) : @@ -98,15 +104,16 @@ theorem wp_lift_pure_step_no_fork [Inhabited State] (E₂ : CoPset) : iintro %Hsafe %Hpure H have Hnone : toVal e₁ = none := by grind [Hsafe default] iapply wp_lift_step Hnone - iintro %σ₁ %ns %obs %obs' %nt Hσ + iintro %σ₁ %ns %obs %nt Hσ imod H iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro Hclose isplit · ipureintro; cases s <;> grind -- TODO: Why is `grind [cases S]` not enough? inext - iintro %e₂ %σ₂ %eₜ %Hstep Hcred + iintro %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred obtain ⟨rfl, rfl, rfl⟩ := Hpure _ _ _ _ _ Hstep + subst Hsplit dsimp only [List.nil_append, List.length_nil] imod ι.stateInterp_mono $$ Hσ with $ imod Hclose @@ -123,7 +130,7 @@ theorem wp_lift_pure_stuck [Inhabited State] : iintro %Hstuck - have ⟨toVal_e, _⟩ := Hstuck default iapply wp_lift_stuck toVal_e - iintro %σ %ns %obs' %nt - + iintro %σ %ns %obs %nt - iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro - ipureintro @@ -131,21 +138,23 @@ theorem wp_lift_pure_stuck [Inhabited State] : @[rocq_alias wp_lift_atomic_step_fupd] theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) (E₂ : CoPset) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E₁}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ + ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro H iapply wp_lift_step_fupd h - iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + iintro %σ₁ %ns %obs %nt Hσ₁ imod H $$ Hσ₁ with ⟨$, H⟩ iapply fupd_mask_intro Std.LawfulSet.empty_subset - iintro Hclose %e₂ %σ₂ %eₜ %Hstep Hcred + iintro Hclose %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred imod Hclose with - - imod H $$ %_ %_ %_ %Hstep Hcred with H + imod H $$ %_ %_ %_ %_ %_ %Hsplit %Hstep Hcred with H iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro Hclose !> imod Hclose with - @@ -154,19 +163,21 @@ theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) (E₂ : CoPset) : @[rocq_alias wp_lift_atomic_step] theorem wp_lift_atomic_step (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + (∀ σ₁ ns obs nt, stateInterp σ₁ ns obs nt ={E}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + ▷ ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro H iapply wp_lift_atomic_step_fupd (E₂ := E) h - iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + iintro %σ₁ %ns %obs %nt Hσ₁ imod H $$ [$] with ⟨$, H⟩ - iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> - iapply H $$ %_ %_ %_ %Hstep Hcred + iintro !> %e₂ %σ₂ %eₜ %κ %obs' %Hsplit %Hstep Hcred !> !> + iapply H $$ %_ %_ %_ %_ %_ %Hsplit %Hstep Hcred @[rocq_alias wp_lift_pure_det_step_no_fork] theorem wp_lift_pure_det_step_no_fork [Inhabited State] (E₂ : CoPset) diff --git a/Iris/Iris/ProgramLogic/WeakestPre.lean b/Iris/Iris/ProgramLogic/WeakestPre.lean index 958c75c39..927497600 100644 --- a/Iris/Iris/ProgramLogic/WeakestPre.lean +++ b/Iris/Iris/ProgramLogic/WeakestPre.lean @@ -70,10 +70,12 @@ def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF := match toVal e₁ with | some v => iprop(|={E}=> Φ v) - | none => iprop(∀ (σ₁ : State) (ns : Nat) (obs obs' : List Obs) (nt : Nat), - stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + | none => iprop(∀ (σ₁ : State) (ns : Nat) (obs : List Obs) (nt : Nat), + stateInterp σ₁ ns obs nt ={E,∅}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ + ∀ e₂ σ₂ eₜ κ obs', + ⌜obs = κ ++ obs'⌝ -∗ + ⌜(e₁, σ₁) -<κ>-> (e₂, σ₂, eₜ)⌝ -∗ £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost) @@ -90,7 +92,6 @@ instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where refine BI.forall_ne (fun σ₁ => ?_) refine BI.forall_ne (fun ns => ?_) refine BI.forall_ne (fun obs => ?_) - refine BI.forall_ne (fun obs' => ?_) refine BI.forall_ne (fun nt => ?_) refine BI.wand_ne.ne .rfl ?_ refine BIFUpdate.ne.ne ?_ @@ -98,6 +99,9 @@ instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where refine BI.forall_ne (fun e₂ => ?_) refine BI.forall_ne (fun σ₂ => ?_) refine BI.forall_ne (fun eₜ => ?_) + refine BI.forall_ne (fun κ => ?_) + refine BI.forall_ne (fun obs' => ?_) + refine BI.wand_ne.ne .rfl ?_ refine BI.wand_ne.ne .rfl ?_ refine BI.wand_ne.ne .rfl ?_ refine BIFUpdate.ne.ne ?_ @@ -139,7 +143,6 @@ instance wp_ne {s : Stuckness} {E} {e : Expr} : refine BI.forall_ne fun σ₁ => ?_ refine BI.forall_ne fun ns => ?_ refine BI.forall_ne fun obs => ?_ - refine BI.forall_ne fun obs' => ?_ refine BI.forall_ne fun nt => ?_ refine BI.wand_ne.ne .rfl ?_ refine BIFUpdate.ne.ne ?_ @@ -147,6 +150,9 @@ instance wp_ne {s : Stuckness} {E} {e : Expr} : refine BI.forall_ne fun e₂ => ?_ refine BI.forall_ne fun σ₂ => ?_ refine BI.forall_ne fun eₜ => ?_ + refine BI.forall_ne fun κ => ?_ + refine BI.forall_ne fun obs' => ?_ + refine BI.wand_ne.ne .rfl ?_ refine BI.wand_ne.ne .rfl ?_ refine BI.wand_ne.ne .rfl ?_ refine step_fupdN_contractive.distLater_dist fun m n_m => ?_ @@ -166,7 +172,6 @@ theorem wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) : refine BI.forall_ne fun σ₁ => ?_ refine BI.forall_ne fun ns => ?_ refine BI.forall_ne fun obs => ?_ - refine BI.forall_ne fun obs' => ?_ refine BI.forall_ne fun nt => ?_ refine BI.wand_ne.ne .rfl ?_ refine BIFUpdate.ne.ne ?_ @@ -174,6 +179,9 @@ theorem wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) : refine BI.forall_ne fun e₂ => ?_ refine BI.forall_ne fun σ₂ => ?_ refine BI.forall_ne fun eₜ => ?_ + refine BI.forall_ne fun κ => ?_ + refine BI.forall_ne fun obs' => ?_ + refine BI.wand_ne.ne .rfl ?_ refine BI.wand_ne.ne .rfl ?_ refine BI.wand_ne.ne .rfl ?_ refine step_fupdN_contractive.distLater_dist fun m n_m => ?_ @@ -199,7 +207,7 @@ theorem wp_strong_mono {s₁ s₂ : Stuckness} {E₁ E₂} {e : Expr} {Φ Ψ : V match toVal e with | none => dsimp only - iintro %σ₁ %ns %obs %obs' %nt Hσ + iintro %σ₁ %ns %obs %nt Hσ imod fupd_mask_subseteq hE with Hclose icases H $$ Hσ with >⟨%h, H⟩ imodintro @@ -207,9 +215,9 @@ theorem wp_strong_mono {s₁ s₂ : Stuckness} {E₁ E₂} {e : Expr} {Φ Ψ : V · simp only [LE.le] at hs ipureintro grind [cases Stuckness] - · iintro %e₂ %σ₂ %eₜ #hstep hc + · iintro %e₂ %σ₂ %eₜ %κ %obs' #hsplit #hstep hc dsimp only [Nat.repeat] - imod H $$ hstep hc with H + imod H $$ hsplit hstep hc with H iintro !> !>; imod H; iintro !> iapply step_fupdN_wand $$ H iintro >⟨aux, H, Hefs⟩ @@ -241,7 +249,7 @@ theorem fupd_wp {s : Stuckness}{E}{e : Expr} {Φ : Val → IProp GF} : iassumption | none => simp only [wp.pre, h] - iintro %σ₁ %ns %obs %obs' %nt + iintro %σ₁ %ns %obs %nt imod H with H iassumption @@ -273,12 +281,12 @@ theorem wp_atomic {s : Stuckness} {E1 E2 : CoPset} {e : Expr} {Φ : Val → IPro iassumption | none => simp only [wp.pre, He] - iintro %σ₁ %ns %obs %obs' %nt Hσ + iintro %σ₁ %ns %obs %nt Hσ imod H imod H $$ Hσ with ⟨$, H⟩ imodintro - iintro %e2 %σ2 %efs %Hstep Hcred - ihave aux := H $$ %e2 %σ2 %efs %Hstep Hcred + iintro %e2 %σ2 %efs %κ %obs' %Hsplit %Hstep Hcred + ihave aux := H $$ %e2 %σ2 %efs %κ %obs' %Hsplit %Hstep Hcred iapply step_fupdN_wand $$ aux iintro >(⟨Hσ,H,Hefs⟩) irevert %ι @@ -293,8 +301,8 @@ theorem wp_atomic {s : Stuckness} {E1 E2 : CoPset} {e : Expr} {Φ : Val → IPro iframe | none => iintro %ι - icases H $$ %σ2 %(ns +1) %([]) %_ %(nt + efs.length) [Hσ] with >⟨%h, _⟩ - · exact .rfl + ispecialize H $$ %σ2 %(ns + 1) %obs' %(nt + efs.length) + icases H $$ Hσ with >⟨%h, _⟩ exact ((Language.not_reducible_iff_irreducible.mpr (ι.atomic Hstep)) h).elim | .MaybeStuck => iintro %ι @@ -317,18 +325,18 @@ theorem wp_credit_access {s : Stuckness} {E : CoPset} {e : Expr} {Φ} {P: IProp simp only [wp_unfold.to_eq] iintro Hupd Hwp simp only [wp.pre, h] - iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + iintro %σ₁ %ns %obs %nt Hσ₁ imod Hupd $$ Hσ₁ with ⟨%k, %m, Hσ₁, %h, Hpost⟩; subst h imod Hwp $$ Hσ₁ with ⟨$,Hwp⟩ imodintro - iintro %e₂ %σ₂ %efs %Hstep Hc + iintro %e₂ %σ₂ %efs %κ %obs' %Hsplit %Hstep Hc simp only [lc_split.to_eq] icases Hc with ⟨Hc,Hone⟩ ihave Hc := lc_weaken _ (Htri m k) $$ Hc icases lc_split $$ Hc with ⟨Hm, Hk⟩ icombine Hm Hone as Hm dsimp only [Nat.repeat] - ihave Hwp := Hwp $$ [//] [Hm] + ihave Hwp := Hwp $$ %e₂ %σ₂ %efs %κ %obs' [//] [//] [Hm] · simp [lc_split.to_eq]; itrivial iapply step_fupd_wand $$ Hwp; iintro Hwp iapply step_fupdN_le (n := ι.numLatersPerStep m) (by grind only) LawfulSet.subset_refl @@ -358,14 +366,14 @@ theorem wp_step_fupdN_strong {s : Stuckness} {E1 E2 : CoPset} {e : Expr} {P : IP | n+1 => simp only [wp_unfold.to_eq] simp only [wp.pre, toVal_e] - iintro H %σ₁ %ns %obs %obs' %nt Hσ₁ + iintro H %σ₁ %ns %obs %nt Hσ₁ by_cases Hn : n ≤ ι.numLatersPerStep ns · icases H with ⟨-, ⟨Hp, Hwp⟩⟩ imod Hp dsimp only [Nat.repeat] imod Hwp $$ Hσ₁ with ⟨$, H⟩ - iintro !> %e₂ %σ₂ %efs %Hstep Hcred - icases H $$ %_ %_ %_ %Hstep Hcred with H + iintro !> %e₂ %σ₂ %efs %κ %obs' %Hsplit %Hstep Hcred + icases H $$ %_ %_ %_ %_ %_ %Hsplit %Hstep Hcred with H imod H; imod Hp iintro !> !> imod H; imod Hp @@ -412,16 +420,17 @@ theorem wp_bind_iff (K : Expr → Expr) [κ : Language.Context K] {s : Stuckness dsimp only simp only [wp.pre, κ.toVal_eq_none_fill h, Nat.repeat] isplit <;> - (iintro H %σ₁ %step %obs %obs' %n Hσ; imod H $$ [$] with ⟨%_, H⟩; imodintro; isplit) + (iintro H %σ₁ %step %obs %n Hσ; imod H $$ [$] with ⟨%_, H⟩; imodintro; isplit) · ipureintro; grind only [cases Stuckness, Language.Context.reducible_fill] - · iintro %e₂ %σ₂ %efs %HKstep Hcred + · iintro %e₂ %σ₂ %efs %κ' %obs' %Hsplit %HKstep Hcred obtain ⟨e₂', rfl, Hstep⟩ := κ.primStep_fill_inv h HKstep - icases H $$ %e₂' %σ₂ %efs %Hstep Hcred with >H; imodintro; imodintro + icases H $$ %e₂' %σ₂ %efs %κ' %obs' %Hsplit %Hstep Hcred with >H; imodintro; imodintro imod H; imodintro; iapply step_fupdN_wand $$ H; iintro H imod H with ⟨$, H, $⟩; imodintro; iapply IH $$ H · ipureintro; grind only [cases Stuckness, Language.Context.reducible_fill_inv] - · iintro %e₂ %σ₂ %efs %Hstep Hcred - icases H $$ %(K e₂) %σ₂ %efs %(κ.primStep_fill Hstep) Hcred with >H; imodintro; imodintro + · iintro %e₂ %σ₂ %efs %κ' %obs' %Hsplit %Hstep Hcred + icases H $$ %(K e₂) %σ₂ %efs %κ' %obs' %Hsplit %(κ.primStep_fill Hstep) Hcred with >H + imodintro; imodintro imod H; imodintro; iapply step_fupdN_wand $$ H; iintro H imod H with ⟨$, H, $⟩; imodintro; iapply IH $$ H From 37687aa172986d9c5b9bfb7c386c4cf3e623b8cc Mon Sep 17 00:00:00 2001 From: Max Vistrup Date: Sat, 25 Jul 2026 14:39:53 +0200 Subject: [PATCH 2/2] Fix build. --- Iris/Iris/HeapLang/PrimitiveLaws.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Iris/Iris/HeapLang/PrimitiveLaws.lean b/Iris/Iris/HeapLang/PrimitiveLaws.lean index 724911fb4..9698e4b84 100644 --- a/Iris/Iris/HeapLang/PrimitiveLaws.lean +++ b/Iris/Iris/HeapLang/PrimitiveLaws.lean @@ -557,9 +557,8 @@ theorem wp_resolve_strong {e : Exp} {p : ProphId} {w : Val} {pvs : List (Val × ihave HWPe : iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) $$ [Hp HWPe] · iapply HWPe; iexact Hp - ihave HWPe := (show iprop(WP e @ s; E {{ v_e, ∃ pvs', proph p pvs' ∗ - ∀ pvs'', ⌜pvs' = (v_e, w) :: pvs''⌝ -∗ proph p pvs'' -∗ Φ v_e }}) ⊢ _ - by rw [wp_unfold.to_eq]; simp only [wp.pre, hne]; exact .rfl) $$ HWPe + ihave HWPe := wp_unfold.mp $$ HWPe + isimp only [wp.pre, hne] in HWPe ihave Hσ_e : iprop(stateInterp σ₁ ns obs nt) $$ [Hheap Hpmap] · iapply (stateInterp_split σ₁ ns obs nt).mpr; iframe Hheap; iexact Hpmap imod HWPe $$ %_ %_ %_ %_ Hσ_e with ⟨%Hred_e, HWPe⟩