From 4a3bf70a74c1098e535e868b6b8f7331a27a216c Mon Sep 17 00:00:00 2001 From: ayhon Date: Mon, 18 May 2026 23:21:23 +0200 Subject: [PATCH 01/10] feat: initial lifting and ectx-lifting port --- Iris/Iris/ProgramLogic/EctxLifting.lean | 190 +++++++++++++++++ Iris/Iris/ProgramLogic/Lifting.lean | 262 ++++++++++++++++++++++++ 2 files changed, 452 insertions(+) create mode 100644 Iris/Iris/ProgramLogic/EctxLifting.lean create mode 100644 Iris/Iris/ProgramLogic/Lifting.lean diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean new file mode 100644 index 00000000..d49d6d97 --- /dev/null +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -0,0 +1,190 @@ +module + +public import Iris.ProgramLogic.Lifting +public import Iris.ProgramLogic.EctxiLanguage + +namespace Iris.ProgramLogic + +open Language.Notation +open EctxLanguage.Notation + +variable {hlc : outParam Bool} +variable {Expr Ectx State Obs Val} +variable [Λ : EctxLanguage Expr Ectx State Obs Val] +variable {GF : BundledGFunctors} +variable [ι : IrisGS_gen hlc Expr GF] + +variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} +variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} + +theorem wp_lift_base_step_fupd : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜BaseStep.Reducible (e₁,σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(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 %toVal_e₁ H + iapply wp_lift_step_fupd toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ Hσ with ⟨%Hred, H⟩ + imodintro + isplit + · ipure_intro; cases s <;> simp only [Stuckness.MaybeReducible, Hred, EctxLanguage.primStep_reducible_of_baseStep_reducible] + iintro %e₂ %σ₂ %eₜ %Hstep + iapply H $$ %_ %_ %_ + ipure_intro + apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred Hstep + +theorem wp_lift_base_step : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(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 %toVal_e₁ H + iapply wp_lift_base_step_fupd toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ [$] with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %eₜ %Hbstep Hcred !> !> + iapply H $$ %_ %_ %_ %Hbstep Hcred + +theorem wp_lift_base_stuck : + toVal e = none → + EctxLanguage.SubredexesAreValues e → + (∀ σ ns obs' nt, stateInterp σ ns obs' nt ={E,∅}=∗ ⌜BaseStep.Stuck (e,σ)⌝) + ⊢ WP e @ E ? {{ Φ }} := by + iintro %toVal_e %sav_e H + iapply wp_lift_stuck toVal_e + iintro %σ %ns %obs' %nt Hσ + imod H $$ Hσ with %H + ipure_intro + apply EctxLanguage.primStep_stuck_of_baseStep_stuck H sav_e + +theorem wp_lift_pure_base_stuck : + toVal e = none → + EctxLanguage.SubredexesAreValues e → + (∀ σ, BaseStep.Stuck (e,σ)) → + ⊢ WP e @ E ?{{ Φ }} := by + iintro %toVal_e %sav_e %Hstuck + iapply wp_lift_base_stuck toVal_e sav_e + iintro %σ %ns %obs' %nt Hσ + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro _ + ipure_intro + apply Hstuck + +theorem wp_lift_atomic_base_step_fupd : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E1}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + (toVal e₂).rec iprop(False) Φ ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E1 {{ Φ }} := by + iintro %toVal_e₁ H + iapply wp_lift_atomic_step_fupd toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨%Hbred, H⟩ + imodintro + isplit + · ipure_intro; cases s <;> simp [Stuckness.MaybeReducible, EctxLanguage.primStep_reducible_of_baseStep_reducible, *] + iintro %_ %_ %_ %Hstep + iapply H + ipure_intro + apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hbred Hstep + +theorem wp_lift_atomic_base_step : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + (toVal e₂).rec iprop(False) Φ ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro %toVal_e H + iapply wp_lift_atomic_step toVal_e + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨%Hbred, H⟩ + imodintro + isplit + · ipure_intro; cases s <;> simp [Stuckness.MaybeReducible, EctxLanguage.primStep_reducible_of_baseStep_reducible, *] + inext + iintro %e₂ %σ₂ %eₜ %Hstep Hcred + iapply H $$ %_ %_ %_ [] Hcred + ipure_intro + apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hbred Hstep + +theorem wp_lift_atomic_base_step_no_fork_fupd : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E1}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ + ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (toVal e₂).rec iprop(False) Φ) + ⊢ WP e₁ @ s; E1 {{ Φ }} := by + iintro %toVal_e₁ H + iapply wp_lift_atomic_base_step_fupd toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ %_ %_ %_ %_ %_ Hσ₁ with ⟨$, H⟩ + imodintro + iintro %_ %_ %_ %Hbstep Hcred + imod H $$ %_ %_ %_ %Hbstep Hcred with H + iintro !> !> + imod H with ⟨%h, _, _⟩ + subst h + simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] + iframe + iapply fupd_mask_intro_discard Std.LawfulSet.subset_refl + exact .rfl + +theorem wp_lift_atomic_base_step_no_fork : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (toVal e₂).rec iprop(False) Φ ) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro %toVal_e₁ H + iapply wp_lift_atomic_base_step toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨$, H⟩ + imodintro + inext + iintro %v2 %σ₂ %eₜ %Hstep Hcred + imod H $$ %_ %_ %_ %Hstep Hcred with ⟨%h, _, _⟩ + subst h + imodintro + simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] + iframe + +#check wp_lift_pure_det_step_no_fork + +theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] : + toVal e₁ = none → + (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → + (∀ σ₁ obs e₂' σ₂ eₜ', + (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → + (|={E}[E']▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro %toVal_e₁ %Hbred %Hpure _ + apply wp_lift_pure_det_step_no_fork + · cases s <;> simp [EctxLanguage.primStep_reducible_of_baseStep_reducible, *] + · intro _ _ _ _ _ _ + apply Hpure + grind [EctxLanguage.baseStep_of_primStep_of_baseStep_reducible] + +theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] : + toVal e₁ = none → + (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → + (∀ σ₁ obs e₂' σ₂ eₜ', + (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → + ▷ (£ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro %toVal_e₁ %Hbred %Hpure _ + refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork (E' := E) toVal_e₁ Hbred Hpure + exact step_fupd_intro Std.LawfulSet.subset_refl diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean new file mode 100644 index 00000000..13ef425a --- /dev/null +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -0,0 +1,262 @@ +module + +public import Iris.ProofMode +public import Iris.ProgramLogic.WeakestPre + +public section + +namespace Iris.ProgramLogic + +open Language.Notation + +variable {hlc : outParam Bool} +variable {Expr State Obs Val} +variable [Λ : Language Expr State Obs Val] +variable {GF : BundledGFunctors} +variable [ι : IrisGS_gen hlc Expr GF] + +variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} +variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} + +attribute [local simp] Language.reducible_of_reducibleNoObs + +@[rocq_alias wp_lift_step_fupdN] +theorem wp_lift_step_fupdN : + toVal e₁ = none → + (∀ σ₁ ns (obs obs' : List Obs) nt, + stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ + £ (ι.numLatersPerStep ns + 1) + ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> + -- NOTE: Changed the order of `nt` and `eₜ.length` since in Lean + -- we have `n + 0 = n` and not `0 + n = n` + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + WP e₂ @ s; E {{ Φ }} ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + intro h + rw [rw_iProp wp_unfold] + simp only [wp.pre, h] + exact .rfl + +@[rocq_alias wp_lift_step_fupd] +theorem wp_lift_step_fupd : + toVal e₁ = none → + (∀ σ₁ ns (obs obs' : List Obs) nt, + stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ + £ 1 ={∅}=∗ ▷ |={∅,E}=> + -- NOTE: Changed the order of `nt` and `eₜ.length` since in Lean + -- we have `n + 0 = n` and not `0 + n = n` + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ + WP e₂ @ s; E {{ Φ }} ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + intro h + refine .trans ?_ <| wp_lift_step_fupdN h + iintro Hwp %σ₁ %ns %obs %obs' %nt Hσ + imod Hwp $$ Hσ with ⟨$, Hwp⟩ + iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred + ihave Hcred := lc_weaken 1 (Nat.le_add_left 1 (ι.numLatersPerStep ns)) $$ Hcred + -- simp only [Nat.repeat] + refine .trans ?_ <| BIFUpdate.mono <| BI.later_mono <| BIFUpdate.mono <| + (BI.laterN_intro _ |>.trans <| step_fupdN_intro Std.LawfulSet.empty_subset) + iintro ⟨Hwp, Hcred⟩ + imod Hwp $$ %_ %_ %_ %Hstep Hcred with Hwp + iapply step_fupd_intro Std.LawfulSet.empty_subset + iassumption + +theorem wp_lift_stuck : + toVal e = none → + (∀ σ ns obs nt, + stateInterp σ ns obs nt ={E,∅}=∗ ⌜PrimStep.Stuck (e,σ)⌝) + ⊢ WP e @ E ? {{ Φ }} := by + iintro %h H + simp only [rw_iProp wp_unfold] + simp only [wp.pre, h] + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ Hσ with %Hirr + replace ⟨_, Hirr⟩ := Hirr + imodintro + isplit + · ipure_intro; simp only [Stuckness.MaybeReducible] + iintro %e₂ %σ₂ %eₜ %Hstep + nomatch Hirr obs e₂ σ₂ eₜ Hstep + +/-! ## Derived lifting lemmas -/ + + +@[rocq_alias wp_lift_step] +theorem wp_lift_step : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(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 %toVal_e₁ H + iapply wp_lift_step_fupd toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H $$ %_ %_ %_ %_ %_ Hσ with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> + iapply H $$ %_ %_ %_ %Hstep Hcred + +@[rocq_alias wp_lift_pure_step_no_fork] +-- TODO: Why does `E₂` even appear here? +-- Probably shouldn't be inferring it... +theorem wp_lift_pure_step_no_fork [Inhabited State] : + (∀ σ₁, if s matches .NotStuck then PrimStep.Reducible (e₁,σ₁) else toVal e₁ = none) → + (∀ obs σ₁ e₂ σ₂ eₜ, (e₁, σ₁) --> (e₂, σ₂, eₜ) → obs = [] ∧ σ₂ = σ₁ ∧ eₜ = []) → + (|={E₁}[E₂]▷=> ∀ obs e₂ eₜ σ, ⌜(e₁, σ) --> (e₂, σ, eₜ)⌝ -∗ £ 1 -∗ WP e₂ @ s; E₁ {{ Φ }}) + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by + iintro %Hsafe %Hpure H + iapply wp_lift_step + { grind only [Language.toVal_none_of_reducible, Hsafe default] } + iintro %σ₁ %ns %obs %obs' %nt Hσ + imod H + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro Hclose + isplit + { ipure_intro; grind only } + inext + iintro %e₂ %σ₂ %eₜ %Hstep Hcred + obtain ⟨rfl, rfl, rfl⟩ := Hpure _ _ _ _ _ Hstep + dsimp only [List.nil_append, List.length_nil] + imod ι.stateInterp_mono $$ Hσ with $ + imod Hclose + imod H + imodintro + simp only [Algebra.BigOpL.bigOpL_nil] + ispecialize H $$ %_ %_ %_ %_ %Hstep Hcred + iframe + +@[rocq_alias wp_lift_pure_stuck] +theorem wp_lift_pure_stuck [Inhabited State] : + (∀ σ, PrimStep.Stuck (e,σ)) → + True ⊢ WP e @ E ?{{ Φ }} := by + iintro %Hstuck _ + have ⟨toVal_e, _⟩ := Hstuck default + iapply wp_lift_stuck toVal_e + iintro %σ %ns %obs' %nt _ + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro _ + ipure_intro + apply Hstuck + +theorem wp_lift_atomic_step_fupd : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E1}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ + (toVal e₂).rec iprop(False) Φ ∗ + -- NOTE: I tried something like this + -- (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ + -- but I can't destruct the exists in the IPM. Why was `.rec` chosen? + -- Is it related to this restriction on destructing `∃`? + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E1 {{ Φ }} := by + iintro %toVal_e₁ H + iapply wp_lift_step_fupd toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ Hσ₁ with ⟨$, H⟩ + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro Hclose %e₂ %σ₂ %eₜ %Hstep Hcred + imod Hclose + imod H $$ %_ %_ %_ %Hstep Hcred with H + iapply fupd_mask_intro Std.LawfulSet.empty_subset + iintro Hclose !> + imod Hclose + imod H with ⟨$, HQ, $⟩ + -- imod H with ⟨$, ⟨v, %_, _⟩, $⟩ + match h : toVal e₂ with + | some v => + iintro !> + iapply wp_value ⟨ToVal.coe_of_toVal_eq_some h⟩ $$ HQ + | none => + iexfalso; iassumption + + +theorem wp_lift_atomic_step : + toVal e₁ = none → + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ + stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ + (toVal e₂).rec iprop(False) Φ ∗ + [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) + ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro %toVal_e₁ H + iapply wp_lift_atomic_step_fupd toVal_e₁ + iintro %σ₁ %ns %obs %obs' %nt Hσ₁ + imod H $$ [$] with ⟨$, H⟩ + iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> + iapply H $$ %_ %_ %_ %Hstep Hcred + +theorem wp_lift_pure_det_step_no_fork [Inhabited State] : + (∀ σ₁, if s matches .NotStuck then PrimStep.Reducible (e₁,σ₁) else toVal e₁ = none) → + (∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) --> (e₂', σ₂, eₜ') → + obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → + (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro %Hsafe %Hpuredet H + iapply wp_lift_pure_step_no_fork Hsafe (by grind only) (E₂ := E₂) + iapply step_fupd_wand $$ H + iintro H + iintro %obs %e' %eₜ' %σ %aux + obtain ⟨rfl, _, rfl, rfl⟩:= Hpuredet _ _ _ _ _ aux + iassumption + +#check BIUpdate.intro + +theorem wp_pure_step_fupd [Inhabited State] : + Language.PureExec φ n e₁ e₂ → + φ → + (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro %Hexec %Hφ Hwp + replace Hexec := Hexec.pureExec Hφ + induction Hexec using Relation.Iterate.head_induction_on with + | rfl => + simp only [Nat.repeat] + rw (occs := [2]) [rw_iProp fupd_wp_iff] + icases lc_zero with >Hz + iapply Hwp $$ Hz + | @head n e₁ e₃ inicio fin IH => + obtain ⟨Hsafe, Hdet⟩ := inicio + iapply wp_lift_pure_det_step_no_fork (E₂ := E₂) (e₂ := e₃) (by + intro σ + cases s with + | NotStuck => grind + | MaybeStuck => + apply Language.toVal_none_of_reducible (σ := σ) + grind + ) (by grind) + simp only [Nat.repeat] + iapply step_fupd_wand $$ Hwp + iintro Hwp Hone + iapply IH + iapply step_fupdN_wand $$ Hwp + iintro Hwp Hc + iapply Hwp $$ [Hone Hc] + iapply lc_split + iframe + +theorem wp_pure_step_later [Inhabited State] : + Language.PureExec φ n e₁ e₂ → + φ → + ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + intro Hexec Hφ + refine .trans ?_ (@wp_pure_step_fupd hlc Expr State Obs Val Λ GF ι s E E e₁ e₂ Φ φ n _ Hexec Hφ) + suffices Hwp : ∀ (P : IProp GF), ▷^[n] P ⊢ |={E}▷=>^[n] P by iapply Hwp + intro P + clear Hexec + induction n with + | zero => exact .rfl + | succ n IH => + simp [Nat.repeat] + rw [rw_iProp <| BI.later_laterN n] + refine .trans (BI.later_mono IH) ?_ + apply step_fupd_intro (Std.LawfulSet.subset_refl) From d2842a1f8b872a69497c92dfa8dff79f4cc38cd5 Mon Sep 17 00:00:00 2001 From: ayhon Date: Wed, 20 May 2026 11:13:52 +0200 Subject: [PATCH 02/10] fix: add dangling lemmas --- Iris/Iris/BI/Updates.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean index 2187c2bc..8cc2796b 100644 --- a/Iris/Iris/BI/Updates.lean +++ b/Iris/Iris/BI/Updates.lean @@ -383,6 +383,18 @@ theorem step_fupd_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : _ ⊢ |={Ei}[Ei]▷=> P := mono <| later_mono fupd_intro _ ⊢ |={Eo}[Ei]▷=> P := step_fupd_mask_mono (subset_refl) Ei_Eo +@[rocq_alias step_fupdN_intro] +theorem step_fupdN_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : + ▷^[n] P ⊢ |={Eo}[Ei]▷=>^[n] P := + match n with + | 0 => .rfl + | n+1 => by + simp only [Nat.repeat] + refine .trans (later_laterN n).1 ?_ + refine .trans (step_fupd_intro Ei_Eo) ?_ + apply BIFUpdate.mono ∘ later_mono ∘ BIFUpdate.mono + exact (step_fupdN_intro (n := n) (P := P) Ei_Eo) + @[rocq_alias step_fupdN_le] theorem step_fupdN_le {n m : Nat} {Eo Ei : CoPset} {P : PROP} : n ≤ m → Ei ⊆ Eo → (|={Eo}[Ei]▷=>^[n] P) ⊢ |={Eo}[Ei]▷=>^[m] P From 4fb2c2ea31319686bb31bc69353d472ca63f4a71 Mon Sep 17 00:00:00 2001 From: ayhon Date: Thu, 21 May 2026 11:08:30 +0200 Subject: [PATCH 03/10] fix: rename rw_iProp to IProp.ext --- Iris/Iris/ProgramLogic/EctxLifting.lean | 2 -- Iris/Iris/ProgramLogic/Lifting.lean | 8 ++++---- 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean index d49d6d97..9b1f5982 100644 --- a/Iris/Iris/ProgramLogic/EctxLifting.lean +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -164,8 +164,6 @@ theorem wp_lift_atomic_base_step_no_fork : simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] iframe -#check wp_lift_pure_det_step_no_fork - theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] : toVal e₁ = none → (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index 13ef425a..d8a07629 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -36,7 +36,7 @@ theorem wp_lift_step_fupdN : [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by intro h - rw [rw_iProp wp_unfold] + rw [IProp.ext wp_unfold] simp only [wp.pre, h] exact .rfl @@ -74,7 +74,7 @@ theorem wp_lift_stuck : stateInterp σ ns obs nt ={E,∅}=∗ ⌜PrimStep.Stuck (e,σ)⌝) ⊢ WP e @ E ? {{ Φ }} := by iintro %h H - simp only [rw_iProp wp_unfold] + simp only [IProp.ext wp_unfold] simp only [wp.pre, h] iintro %σ₁ %ns %obs %obs' %nt Hσ imod H $$ Hσ with %Hirr @@ -221,7 +221,7 @@ theorem wp_pure_step_fupd [Inhabited State] : induction Hexec using Relation.Iterate.head_induction_on with | rfl => simp only [Nat.repeat] - rw (occs := [2]) [rw_iProp fupd_wp_iff] + rw (occs := [2]) [IProp.ext fupd_wp_iff] icases lc_zero with >Hz iapply Hwp $$ Hz | @head n e₁ e₃ inicio fin IH => @@ -257,6 +257,6 @@ theorem wp_pure_step_later [Inhabited State] : | zero => exact .rfl | succ n IH => simp [Nat.repeat] - rw [rw_iProp <| BI.later_laterN n] + rw [IProp.ext <| BI.later_laterN n] refine .trans (BI.later_mono IH) ?_ apply step_fupd_intro (Std.LawfulSet.subset_refl) From f1462292e5301cbe5bbc7f6d0e3ef70d749d0890 Mon Sep 17 00:00:00 2001 From: ayhon Date: Thu, 21 May 2026 11:26:10 +0200 Subject: [PATCH 04/10] refactor: remove `#check` info logs --- Iris/Iris/ProgramLogic/Lifting.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index d8a07629..69d72517 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -210,8 +210,6 @@ theorem wp_lift_pure_det_step_no_fork [Inhabited State] : obtain ⟨rfl, _, rfl, rfl⟩:= Hpuredet _ _ _ _ _ aux iassumption -#check BIUpdate.intro - theorem wp_pure_step_fupd [Inhabited State] : Language.PureExec φ n e₁ e₂ → φ → From fc71720aa10cda531ca60f968100bce314ab85bd Mon Sep 17 00:00:00 2001 From: ayhon Date: Fri, 22 May 2026 14:47:59 +0200 Subject: [PATCH 05/10] fix: address #393 comments in #397 --- Iris/Iris/ProgramLogic/EctxLifting.lean | 82 +++++++++------------ Iris/Iris/ProgramLogic/Lifting.lean | 94 +++++++++++-------------- 2 files changed, 75 insertions(+), 101 deletions(-) diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean index 9b1f5982..74a66c3c 100644 --- a/Iris/Iris/ProgramLogic/EctxLifting.lean +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -17,8 +17,7 @@ variable [ι : IrisGS_gen hlc Expr GF] variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} -theorem wp_lift_base_step_fupd : - toVal e₁ = none → +theorem wp_lift_base_step_fupd (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ ⌜BaseStep.Reducible (e₁,σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁,σ₁) -->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=> @@ -26,20 +25,19 @@ theorem wp_lift_base_step_fupd : WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_step_fupd toVal_e₁ + iintro H + iapply wp_lift_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ imod H $$ Hσ with ⟨%Hred, H⟩ imodintro isplit - · ipure_intro; cases s <;> simp only [Stuckness.MaybeReducible, Hred, EctxLanguage.primStep_reducible_of_baseStep_reducible] + · ipure_intro; grind only [EctxLanguage.primStep_reducible_of_baseStep_reducible] iintro %e₂ %σ₂ %eₜ %Hstep iapply H $$ %_ %_ %_ ipure_intro apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred Hstep -theorem wp_lift_base_step : - toVal e₁ = none → +theorem wp_lift_base_step (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂,σ₂,eₜ)⌝ -∗ £ 1 ={∅,E}=∗ @@ -47,40 +45,37 @@ theorem wp_lift_base_step : WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_base_step_fupd toVal_e₁ + iintro H + iapply wp_lift_base_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ imod H $$ [$] with ⟨$, H⟩ iintro !> %e₂ %σ₂ %eₜ %Hbstep Hcred !> !> iapply H $$ %_ %_ %_ %Hbstep Hcred -theorem wp_lift_base_stuck : - toVal e = none → +theorem wp_lift_base_stuck (h : toVal e = none) : EctxLanguage.SubredexesAreValues e → (∀ σ ns obs' nt, stateInterp σ ns obs' nt ={E,∅}=∗ ⌜BaseStep.Stuck (e,σ)⌝) ⊢ WP e @ E ? {{ Φ }} := by - iintro %toVal_e %sav_e H - iapply wp_lift_stuck toVal_e + iintro %sav_e H + iapply wp_lift_stuck h iintro %σ %ns %obs' %nt Hσ imod H $$ Hσ with %H ipure_intro apply EctxLanguage.primStep_stuck_of_baseStep_stuck H sav_e -theorem wp_lift_pure_base_stuck : - toVal e = none → +theorem wp_lift_pure_base_stuck (h : toVal e = none) : EctxLanguage.SubredexesAreValues e → (∀ σ, BaseStep.Stuck (e,σ)) → ⊢ WP e @ E ?{{ Φ }} := by - iintro %toVal_e %sav_e %Hstuck - iapply wp_lift_base_stuck toVal_e sav_e + iintro %sav_e %Hstuck + iapply wp_lift_base_stuck h sav_e iintro %σ %ns %obs' %nt Hσ iapply fupd_mask_intro Std.LawfulSet.empty_subset - iintro _ + iintro - ipure_intro apply Hstuck -theorem wp_lift_atomic_base_step_fupd : - toVal e₁ = none → +theorem wp_lift_atomic_base_step_fupd (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E1}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ @@ -88,20 +83,19 @@ theorem wp_lift_atomic_base_step_fupd : (toVal e₂).rec iprop(False) Φ ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E1 {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_atomic_step_fupd toVal_e₁ + iintro H + iapply wp_lift_atomic_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ Hσ₁ with ⟨%Hbred, H⟩ imodintro isplit - · ipure_intro; cases s <;> simp [Stuckness.MaybeReducible, EctxLanguage.primStep_reducible_of_baseStep_reducible, *] + · ipure_intro; grind only [EctxLanguage.primStep_reducible_of_baseStep_reducible] iintro %_ %_ %_ %Hstep iapply H ipure_intro apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hbred Hstep -theorem wp_lift_atomic_base_step : - toVal e₁ = none → +theorem wp_lift_atomic_base_step (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ @@ -109,28 +103,27 @@ theorem wp_lift_atomic_base_step : (toVal e₂).rec iprop(False) Φ ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e H - iapply wp_lift_atomic_step toVal_e + iintro H + iapply wp_lift_atomic_step h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ Hσ₁ with ⟨%Hbred, H⟩ imodintro isplit - · ipure_intro; cases s <;> simp [Stuckness.MaybeReducible, EctxLanguage.primStep_reducible_of_baseStep_reducible, *] + · ipure_intro; grind only [EctxLanguage.primStep_reducible_of_baseStep_reducible] inext iintro %e₂ %σ₂ %eₜ %Hstep Hcred iapply H $$ %_ %_ %_ [] Hcred ipure_intro apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hbred Hstep -theorem wp_lift_atomic_base_step_no_fork_fupd : - toVal e₁ = none → +theorem wp_lift_atomic_base_step_no_fork_fupd (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E1}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (toVal e₂).rec iprop(False) Φ) ⊢ WP e₁ @ s; E1 {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_atomic_base_step_fupd toVal_e₁ + iintro H + iapply wp_lift_atomic_base_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ %_ %_ %_ %_ %_ Hσ₁ with ⟨$, H⟩ imodintro @@ -144,15 +137,14 @@ theorem wp_lift_atomic_base_step_no_fork_fupd : iapply fupd_mask_intro_discard Std.LawfulSet.subset_refl exact .rfl -theorem wp_lift_atomic_base_step_no_fork : - toVal e₁ = none → +theorem wp_lift_atomic_base_step_no_fork (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (toVal e₂).rec iprop(False) Φ ) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_atomic_base_step toVal_e₁ + iintro H + iapply wp_lift_atomic_base_step h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ Hσ₁ with ⟨$, H⟩ imodintro @@ -164,25 +156,21 @@ theorem wp_lift_atomic_base_step_no_fork : simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] iframe -theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] : - toVal e₁ = none → +theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (h : toVal e₁ = none) : (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → (∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → (|={E}[E']▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e₁ %Hbred %Hpure _ + iintro %Hbred %Hpure _ apply wp_lift_pure_det_step_no_fork - · cases s <;> simp [EctxLanguage.primStep_reducible_of_baseStep_reducible, *] - · intro _ _ _ _ _ _ - apply Hpure - grind [EctxLanguage.baseStep_of_primStep_of_baseStep_reducible] + · grind [EctxLanguage.primStep_reducible_of_baseStep_reducible] + · grind only [→ EctxLanguage.baseStep_of_primStep_of_baseStep_reducible] -theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] : - toVal e₁ = none → +theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] (h : toVal e₁ = none) : (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → (∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → ▷ (£ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e₁ %Hbred %Hpure _ - refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork (E' := E) toVal_e₁ Hbred Hpure + iintro %Hbred %Hpure _ + refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork (E' := E) h Hbred Hpure exact step_fupd_intro Std.LawfulSet.subset_refl diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index 69d72517..128de2fb 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -7,7 +7,7 @@ public section namespace Iris.ProgramLogic -open Language.Notation +open Language.Notation BI variable {hlc : outParam Bool} variable {Expr State Obs Val} @@ -18,31 +18,23 @@ variable [ι : IrisGS_gen hlc Expr GF] variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} -attribute [local simp] Language.reducible_of_reducibleNoObs - @[rocq_alias wp_lift_step_fupdN] -theorem wp_lift_step_fupdN : - toVal e₁ = none → +theorem wp_lift_step_fupdN (h : toVal e₁ = none) : (∀ σ₁ ns (obs obs' : List Obs) nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ - £ (ι.numLatersPerStep ns + 1) - ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> + £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> -- NOTE: Changed the order of `nt` and `eₜ.length` since in Lean -- we have `n + 0 = n` and not `0 + n = n` stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - intro h - rw [IProp.ext wp_unfold] - simp only [wp.pre, h] - exact .rfl + simp only [IProp.ext (wp_unfold (e := e₁)), wp.pre, h, BIBase.Entails.rfl] @[rocq_alias wp_lift_step_fupd] -theorem wp_lift_step_fupd : - toVal e₁ = none → +theorem wp_lift_step_fupd (h : toVal e₁ = none) : (∀ σ₁ ns (obs obs' : List Obs) nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ @@ -54,26 +46,24 @@ theorem wp_lift_step_fupd : WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - intro h refine .trans ?_ <| wp_lift_step_fupdN h iintro Hwp %σ₁ %ns %obs %obs' %nt Hσ imod Hwp $$ Hσ with ⟨$, Hwp⟩ iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred ihave Hcred := lc_weaken 1 (Nat.le_add_left 1 (ι.numLatersPerStep ns)) $$ Hcred -- simp only [Nat.repeat] - refine .trans ?_ <| BIFUpdate.mono <| BI.later_mono <| BIFUpdate.mono <| - (BI.laterN_intro _ |>.trans <| step_fupdN_intro Std.LawfulSet.empty_subset) + refine .trans ?_ <| BIFUpdate.mono <| later_mono <| BIFUpdate.mono <| + (laterN_intro _ |>.trans <| step_fupdN_intro Std.LawfulSet.empty_subset) iintro ⟨Hwp, Hcred⟩ imod Hwp $$ %_ %_ %_ %Hstep Hcred with Hwp iapply step_fupd_intro Std.LawfulSet.empty_subset iassumption -theorem wp_lift_stuck : - toVal e = none → +theorem wp_lift_stuck (h : toVal e = none) : (∀ σ ns obs nt, stateInterp σ ns obs nt ={E,∅}=∗ ⌜PrimStep.Stuck (e,σ)⌝) ⊢ WP e @ E ? {{ Φ }} := by - iintro %h H + iintro H simp only [IProp.ext wp_unfold] simp only [wp.pre, h] iintro %σ₁ %ns %obs %obs' %nt Hσ @@ -89,8 +79,7 @@ theorem wp_lift_stuck : @[rocq_alias wp_lift_step] -theorem wp_lift_step : - toVal e₁ = none → +theorem wp_lift_step (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={∅,E}=∗ @@ -98,8 +87,8 @@ theorem wp_lift_step : WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_step_fupd toVal_e₁ + iintro H + iapply wp_lift_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ imod H $$ %_ %_ %_ %_ %_ Hσ with ⟨$, H⟩ iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> @@ -109,7 +98,8 @@ theorem wp_lift_step : -- TODO: Why does `E₂` even appear here? -- Probably shouldn't be inferring it... theorem wp_lift_pure_step_no_fork [Inhabited State] : - (∀ σ₁, if s matches .NotStuck then PrimStep.Reducible (e₁,σ₁) else toVal e₁ = none) → + -- (∀ σ₁, if s matches .NotStuck then PrimStep.Reducible (e₁,σ₁) else toVal e₁ = none) → + (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → (∀ obs σ₁ e₂ σ₂ eₜ, (e₁, σ₁) --> (e₂, σ₂, eₜ) → obs = [] ∧ σ₂ = σ₁ ∧ eₜ = []) → (|={E₁}[E₂]▷=> ∀ obs e₂ eₜ σ, ⌜(e₁, σ) --> (e₂, σ, eₜ)⌝ -∗ £ 1 -∗ WP e₂ @ s; E₁ {{ Φ }}) ⊢ WP e₁ @ s; E₁ {{ Φ }} := by @@ -121,7 +111,7 @@ theorem wp_lift_pure_step_no_fork [Inhabited State] : iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro Hclose isplit - { ipure_intro; grind only } + { ipure_intro; cases s <;> grind only} -- TODO: Why is `grind [cases S]` not enough? inext iintro %e₂ %σ₂ %eₜ %Hstep Hcred obtain ⟨rfl, rfl, rfl⟩ := Hpure _ _ _ _ _ Hstep @@ -138,17 +128,16 @@ theorem wp_lift_pure_step_no_fork [Inhabited State] : theorem wp_lift_pure_stuck [Inhabited State] : (∀ σ, PrimStep.Stuck (e,σ)) → True ⊢ WP e @ E ?{{ Φ }} := by - iintro %Hstuck _ + 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 _ + iintro - ipure_intro apply Hstuck -theorem wp_lift_atomic_step_fupd : - toVal e₁ = none → +theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E1}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ @@ -156,12 +145,15 @@ theorem wp_lift_atomic_step_fupd : (toVal e₂).rec iprop(False) Φ ∗ -- NOTE: I tried something like this -- (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ - -- but I can't destruct the exists in the IPM. Why was `.rec` chosen? - -- Is it related to this restriction on destructing `∃`? + -- which seems to work better for the proof. However, I + -- don't fully understand why `Option.rec` was used + -- instead, so I haven't made the change. + -- Why is `Option.rec` (or `from_option` in Iris) used + -- in the first place. [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E1 {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_step_fupd toVal_e₁ + iintro H + iapply wp_lift_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ Hσ₁ with ⟨$, H⟩ iapply fupd_mask_intro Std.LawfulSet.empty_subset @@ -172,7 +164,8 @@ theorem wp_lift_atomic_step_fupd : iintro Hclose !> imod Hclose imod H with ⟨$, HQ, $⟩ - -- imod H with ⟨$, ⟨v, %_, _⟩, $⟩ + -- imod H with ⟨$, ⟨%v, %h, HQ⟩, $⟩ + -- iapply wp_value ⟨ToVal.coe_of_toVal_eq_some h⟩ $$ HQ match h : toVal e₂ with | some v => iintro !> @@ -181,8 +174,7 @@ theorem wp_lift_atomic_step_fupd : iexfalso; iassumption -theorem wp_lift_atomic_step : - toVal e₁ = none → +theorem wp_lift_atomic_step (h : toVal e₁ = none) : (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ @@ -190,15 +182,16 @@ theorem wp_lift_atomic_step : (toVal e₂).rec iprop(False) Φ ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %toVal_e₁ H - iapply wp_lift_atomic_step_fupd toVal_e₁ + iintro H + iapply wp_lift_atomic_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ [$] with ⟨$, H⟩ iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> iapply H $$ %_ %_ %_ %Hstep Hcred theorem wp_lift_pure_det_step_no_fork [Inhabited State] : - (∀ σ₁, if s matches .NotStuck then PrimStep.Reducible (e₁,σ₁) else toVal e₁ = none) → + -- TODO: Why not have this `∀` only in the left match branch? + (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → (∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) --> (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by @@ -211,9 +204,7 @@ theorem wp_lift_pure_det_step_no_fork [Inhabited State] : iassumption theorem wp_pure_step_fupd [Inhabited State] : - Language.PureExec φ n e₁ e₂ → - φ → - (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + Language.PureExec φ n e₁ e₂ → φ → (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro %Hexec %Hφ Hwp replace Hexec := Hexec.pureExec Hφ induction Hexec using Relation.Iterate.head_induction_on with @@ -226,11 +217,8 @@ theorem wp_pure_step_fupd [Inhabited State] : obtain ⟨Hsafe, Hdet⟩ := inicio iapply wp_lift_pure_det_step_no_fork (E₂ := E₂) (e₂ := e₃) (by intro σ - cases s with - | NotStuck => grind - | MaybeStuck => - apply Language.toVal_none_of_reducible (σ := σ) - grind + have : PrimStep.Reducible (e₁, σ) := by grind only [Language.reducible_of_reducibleNoObs] + grind [cases Stuckness] ) (by grind) simp only [Nat.repeat] iapply step_fupd_wand $$ Hwp @@ -243,9 +231,7 @@ theorem wp_pure_step_fupd [Inhabited State] : iframe theorem wp_pure_step_later [Inhabited State] : - Language.PureExec φ n e₁ e₂ → - φ → - ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + Language.PureExec φ n e₁ e₂ → φ → ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by intro Hexec Hφ refine .trans ?_ (@wp_pure_step_fupd hlc Expr State Obs Val Λ GF ι s E E e₁ e₂ Φ φ n _ Hexec Hφ) suffices Hwp : ∀ (P : IProp GF), ▷^[n] P ⊢ |={E}▷=>^[n] P by iapply Hwp @@ -254,7 +240,7 @@ theorem wp_pure_step_later [Inhabited State] : induction n with | zero => exact .rfl | succ n IH => - simp [Nat.repeat] - rw [IProp.ext <| BI.later_laterN n] - refine .trans (BI.later_mono IH) ?_ + simp only [Nat.repeat] + rw [IProp.ext <| later_laterN n] + refine (later_mono IH).trans ?_ apply step_fupd_intro (Std.LawfulSet.subset_refl) From b52e1bf729f1bac34a2ee1a80f2eefa7b401133d Mon Sep 17 00:00:00 2001 From: ayhon Date: Fri, 22 May 2026 15:02:50 +0200 Subject: [PATCH 06/10] fix: clean up proofs --- Iris/Iris/BI/Updates.lean | 6 +++++- Iris/Iris/ProgramLogic/EctxLifting.lean | 6 +++--- Iris/Iris/ProgramLogic/Lifting.lean | 27 +++++++++++-------------- 3 files changed, 20 insertions(+), 19 deletions(-) diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean index 8cc2796b..018e5d9e 100644 --- a/Iris/Iris/BI/Updates.lean +++ b/Iris/Iris/BI/Updates.lean @@ -375,6 +375,10 @@ theorem step_fupd_mask_mono {Eo₁ Eo₂ Ei₁ Ei₂ : CoPset} {P : PROP} refine fupd_frame_r.trans ?_ exact mono emp_sep.1 +theorem step_fupd_mono {Eo Ei : CoPset} {P Q : PROP} : + (Q ⊢ P) → (|={Eo}[Ei]▷=> Q) ⊢ |={Eo}[Ei]▷=> P := + (BIFUpdate.mono <| later_mono <| BIFUpdate.mono ·) + @[rocq_alias step_fupd_intro] theorem step_fupd_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : ▷ P ⊢ |={Eo}[Ei]▷=> P := by @@ -385,7 +389,7 @@ theorem step_fupd_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : @[rocq_alias step_fupdN_intro] theorem step_fupdN_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : - ▷^[n] P ⊢ |={Eo}[Ei]▷=>^[n] P := + ▷^[n] P ⊢ |={Eo}[Ei]▷=>^[n] P := match n with | 0 => .rfl | n+1 => by diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean index 74a66c3c..e4fecc93 100644 --- a/Iris/Iris/ProgramLogic/EctxLifting.lean +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -156,11 +156,11 @@ theorem wp_lift_atomic_base_step_no_fork (h : toVal e₁ = none) : simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] iframe -theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (h : toVal e₁ = none) : +theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (E₂ : CoPset) (h : toVal e₁ = none) : (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → (∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → - (|={E}[E']▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro %Hbred %Hpure _ apply wp_lift_pure_det_step_no_fork · grind [EctxLanguage.primStep_reducible_of_baseStep_reducible] @@ -172,5 +172,5 @@ theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] (h : toVal e₁ = (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → ▷ (£ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro %Hbred %Hpure _ - refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork (E' := E) h Hbred Hpure + refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork E h Hbred Hpure exact step_fupd_intro Std.LawfulSet.subset_refl diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index 128de2fb..d35535d2 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -51,9 +51,8 @@ theorem wp_lift_step_fupd (h : toVal e₁ = none) : imod Hwp $$ Hσ with ⟨$, Hwp⟩ iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred ihave Hcred := lc_weaken 1 (Nat.le_add_left 1 (ι.numLatersPerStep ns)) $$ Hcred - -- simp only [Nat.repeat] - refine .trans ?_ <| BIFUpdate.mono <| later_mono <| BIFUpdate.mono <| - (laterN_intro _ |>.trans <| step_fupdN_intro Std.LawfulSet.empty_subset) + refine .trans ?_ <| step_fupd_mono <| + (laterN_intro _).trans <| step_fupdN_intro Std.LawfulSet.empty_subset iintro ⟨Hwp, Hcred⟩ imod Hwp $$ %_ %_ %_ %Hstep Hcred with Hwp iapply step_fupd_intro Std.LawfulSet.empty_subset @@ -71,7 +70,7 @@ theorem wp_lift_stuck (h : toVal e = none) : replace ⟨_, Hirr⟩ := Hirr imodintro isplit - · ipure_intro; simp only [Stuckness.MaybeReducible] + · ipure_intro; simp [Stuckness.MaybeReducible] iintro %e₂ %σ₂ %eₜ %Hstep nomatch Hirr obs e₂ σ₂ eₜ Hstep @@ -95,9 +94,7 @@ theorem wp_lift_step (h : toVal e₁ = none) : iapply H $$ %_ %_ %_ %Hstep Hcred @[rocq_alias wp_lift_pure_step_no_fork] --- TODO: Why does `E₂` even appear here? --- Probably shouldn't be inferring it... -theorem wp_lift_pure_step_no_fork [Inhabited State] : +theorem wp_lift_pure_step_no_fork [Inhabited State] (E₂ : CoPset) : -- (∀ σ₁, if s matches .NotStuck then PrimStep.Reducible (e₁,σ₁) else toVal e₁ = none) → (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → (∀ obs σ₁ e₂ σ₂ eₜ, (e₁, σ₁) --> (e₂, σ₂, eₜ) → obs = [] ∧ σ₂ = σ₁ ∧ eₜ = []) → @@ -189,21 +186,21 @@ theorem wp_lift_atomic_step (h : toVal e₁ = none) : iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> iapply H $$ %_ %_ %_ %Hstep Hcred -theorem wp_lift_pure_det_step_no_fork [Inhabited State] : +theorem wp_lift_pure_det_step_no_fork [Inhabited State] (E₂ : CoPset) : -- TODO: Why not have this `∀` only in the left match branch? (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → (∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) --> (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro %Hsafe %Hpuredet H - iapply wp_lift_pure_step_no_fork Hsafe (by grind only) (E₂ := E₂) + iapply wp_lift_pure_step_no_fork E₂ Hsafe (by grind only) iapply step_fupd_wand $$ H iintro H iintro %obs %e' %eₜ' %σ %aux obtain ⟨rfl, _, rfl, rfl⟩:= Hpuredet _ _ _ _ _ aux iassumption -theorem wp_pure_step_fupd [Inhabited State] : +theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset): Language.PureExec φ n e₁ e₂ → φ → (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro %Hexec %Hφ Hwp replace Hexec := Hexec.pureExec Hφ @@ -213,9 +210,9 @@ theorem wp_pure_step_fupd [Inhabited State] : rw (occs := [2]) [IProp.ext fupd_wp_iff] icases lc_zero with >Hz iapply Hwp $$ Hz - | @head n e₁ e₃ inicio fin IH => - obtain ⟨Hsafe, Hdet⟩ := inicio - iapply wp_lift_pure_det_step_no_fork (E₂ := E₂) (e₂ := e₃) (by + | @head n e₁ e₃ _ _ IH => + obtain ⟨Hsafe, Hdet⟩ := ‹e₁ -ᵖ-> e₃› + iapply wp_lift_pure_det_step_no_fork E₂ (e₂ := e₃) (by intro σ have : PrimStep.Reducible (e₁, σ) := by grind only [Language.reducible_of_reducibleNoObs] grind [cases Stuckness] @@ -233,10 +230,10 @@ theorem wp_pure_step_fupd [Inhabited State] : theorem wp_pure_step_later [Inhabited State] : Language.PureExec φ n e₁ e₂ → φ → ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by intro Hexec Hφ - refine .trans ?_ (@wp_pure_step_fupd hlc Expr State Obs Val Λ GF ι s E E e₁ e₂ Φ φ n _ Hexec Hφ) + refine .trans ?_ (wp_pure_step_fupd E Hexec Hφ) suffices Hwp : ∀ (P : IProp GF), ▷^[n] P ⊢ |={E}▷=>^[n] P by iapply Hwp intro P - clear Hexec + clear Hexec -- So it is not captured by the `induction` induction n with | zero => exact .rfl | succ n IH => From d3c276e207d97a3276454292ab78a0acf3f81143 Mon Sep 17 00:00:00 2001 From: ayhon Date: Fri, 22 May 2026 15:09:11 +0200 Subject: [PATCH 07/10] feat: add rocq_alias atrtibutes, prefer subscript indices --- Iris/Iris/ProgramLogic/EctxLifting.lean | 22 ++++++++++++++++------ Iris/Iris/ProgramLogic/Lifting.lean | 10 ++++++---- 2 files changed, 22 insertions(+), 10 deletions(-) diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean index e4fecc93..9aa050d3 100644 --- a/Iris/Iris/ProgramLogic/EctxLifting.lean +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -17,6 +17,7 @@ variable [ι : IrisGS_gen hlc Expr GF] variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} 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,∅}=∗ ⌜BaseStep.Reducible (e₁,σ₁)⌝ ∗ @@ -37,6 +38,7 @@ theorem wp_lift_base_step_fupd (h : toVal e₁ = none) : ipure_intro apply EctxLanguage.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,∅}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ @@ -52,6 +54,7 @@ theorem wp_lift_base_step (h : toVal e₁ = none) : iintro !> %e₂ %σ₂ %eₜ %Hbstep Hcred !> !> iapply H $$ %_ %_ %_ %Hbstep Hcred +@[rocq_alias wp_lift_base_stuck] theorem wp_lift_base_stuck (h : toVal e = none) : EctxLanguage.SubredexesAreValues e → (∀ σ ns obs' nt, stateInterp σ ns obs' nt ={E,∅}=∗ ⌜BaseStep.Stuck (e,σ)⌝) @@ -63,6 +66,7 @@ theorem wp_lift_base_stuck (h : toVal e = none) : ipure_intro apply EctxLanguage.primStep_stuck_of_baseStep_stuck H sav_e +@[rocq_alias wp_lift_pure_base_stuck] theorem wp_lift_pure_base_stuck (h : toVal e = none) : EctxLanguage.SubredexesAreValues e → (∀ σ, BaseStep.Stuck (e,σ)) → @@ -75,14 +79,15 @@ theorem wp_lift_pure_base_stuck (h : toVal e = none) : ipure_intro apply Hstuck +@[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 ={E1}=∗ + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ (toVal e₂).rec iprop(False) Φ ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) - ⊢ WP e₁ @ s; E1 {{ Φ }} := by + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro H iapply wp_lift_atomic_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ @@ -95,6 +100,7 @@ theorem wp_lift_atomic_base_step_fupd (h : toVal e₁ = none) : ipure_intro apply EctxLanguage.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}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ @@ -116,12 +122,13 @@ theorem wp_lift_atomic_base_step (h : toVal e₁ = none) : ipure_intro apply EctxLanguage.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 ={E1}=∗ + (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E₁}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (toVal e₂).rec iprop(False) Φ) - ⊢ WP e₁ @ s; E1 {{ Φ }} := by + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro H iapply wp_lift_atomic_base_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ @@ -137,6 +144,7 @@ theorem wp_lift_atomic_base_step_no_fork_fupd (h : toVal e₁ = none) : iapply fupd_mask_intro_discard Std.LawfulSet.subset_refl exact .rfl +@[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}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ @@ -156,6 +164,7 @@ theorem wp_lift_atomic_base_step_no_fork (h : toVal e₁ = none) : simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] iframe +@[rocq_alias wp_lift_pure_det_base_step_no_fork] theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (E₂ : CoPset) (h : toVal e₁ = none) : (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → (∀ σ₁ obs e₂' σ₂ eₜ', @@ -166,6 +175,7 @@ theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (E₂ : CoPset) (h · grind [EctxLanguage.primStep_reducible_of_baseStep_reducible] · grind only [→ EctxLanguage.baseStep_of_primStep_of_baseStep_reducible] +@[rocq_alias wp_lift_pure_det_base_step_no_fork'] theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] (h : toVal e₁ = none) : (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → (∀ σ₁ obs e₂' σ₂ eₜ', diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index d35535d2..2b252ce7 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -58,6 +58,7 @@ theorem wp_lift_step_fupd (h : toVal e₁ = none) : iapply step_fupd_intro Std.LawfulSet.empty_subset iassumption +@[rocq_alias wp_lift_stuck] theorem wp_lift_stuck (h : toVal e = none) : (∀ σ ns obs nt, stateInterp σ ns obs nt ={E,∅}=∗ ⌜PrimStep.Stuck (e,σ)⌝) @@ -134,10 +135,11 @@ theorem wp_lift_pure_stuck [Inhabited State] : ipure_intro apply Hstuck -theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) : - (∀ σ₁ ns obs obs' nt, stateInterp σ₁ ns (obs ++ obs') nt ={E1}=∗ +@[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₁}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E1}[E2]▷=∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ (toVal e₂).rec iprop(False) Φ ∗ -- NOTE: I tried something like this @@ -148,7 +150,7 @@ theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) : -- Why is `Option.rec` (or `from_option` in Iris) used -- in the first place. [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) - ⊢ WP e₁ @ s; E1 {{ Φ }} := by + ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro H iapply wp_lift_step_fupd h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ From a17b1d403c54604a43c79899e98bfcd35830afb9 Mon Sep 17 00:00:00 2001 From: ayhon Date: Fri, 22 May 2026 15:10:03 +0200 Subject: [PATCH 08/10] feat: include copyright headers --- Iris/Iris/ProgramLogic/EctxLifting.lean | 4 ++++ Iris/Iris/ProgramLogic/Lifting.lean | 8 ++++++++ 2 files changed, 12 insertions(+) diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean index 9aa050d3..b5e75a53 100644 --- a/Iris/Iris/ProgramLogic/EctxLifting.lean +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -1,3 +1,7 @@ +/- +Copyright (c) 2026 Fernando Leal. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ module public import Iris.ProgramLogic.Lifting diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index 2b252ce7..5a99a043 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -1,3 +1,7 @@ +/- +Copyright (c) 2026 Fernando Leal. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ module public import Iris.ProofMode @@ -173,6 +177,7 @@ theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) (E₂ : CoPset) : iexfalso; iassumption +@[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}=∗ ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ @@ -188,6 +193,7 @@ theorem wp_lift_atomic_step (h : toVal e₁ = none) : iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> iapply H $$ %_ %_ %_ %Hstep Hcred +@[rocq_alias wp_lift_pure_det_step_no_fork] theorem wp_lift_pure_det_step_no_fork [Inhabited State] (E₂ : CoPset) : -- TODO: Why not have this `∀` only in the left match branch? (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → @@ -202,6 +208,7 @@ theorem wp_lift_pure_det_step_no_fork [Inhabited State] (E₂ : CoPset) : obtain ⟨rfl, _, rfl, rfl⟩:= Hpuredet _ _ _ _ _ aux iassumption +@[rocq_alias wp_pure_step_fupd] theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset): Language.PureExec φ n e₁ e₂ → φ → (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro %Hexec %Hφ Hwp @@ -229,6 +236,7 @@ theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset): iapply lc_split iframe +@[rocq_alias wp_pure_step_later] theorem wp_pure_step_later [Inhabited State] : Language.PureExec φ n e₁ e₂ → φ → ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by intro Hexec Hφ From 1e79407f4ba68d8ce2c00f927e28edb6657e4d97 Mon Sep 17 00:00:00 2001 From: ayhon Date: Fri, 22 May 2026 15:11:55 +0200 Subject: [PATCH 09/10] chore: remove duplicate comment, whitespace --- Iris/Iris/ProgramLogic/Lifting.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index 5a99a043..5d8e1da7 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -44,8 +44,6 @@ theorem wp_lift_step_fupd (h : toVal e₁ = none) : ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=> - -- NOTE: Changed the order of `nt` and `eₜ.length` since in Lean - -- we have `n + 0 = n` and not `0 + n = n` stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ WP e₂ @ s; E {{ Φ }} ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) @@ -81,7 +79,6 @@ theorem wp_lift_stuck (h : toVal e = none) : /-! ## 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,∅}=∗ From aca995b9ca8d73d2c8071f27fd68530a51015aa1 Mon Sep 17 00:00:00 2001 From: Markus de Medeiros Date: Sat, 23 May 2026 10:22:21 -0400 Subject: [PATCH 10/10] chore: cleanup --- Iris/Iris/BI/Updates.lean | 4 +- Iris/Iris/ProgramLogic/EctxLifting.lean | 67 ++++++------- Iris/Iris/ProgramLogic/Lifting.lean | 127 ++++++++++-------------- 3 files changed, 86 insertions(+), 112 deletions(-) diff --git a/Iris/Iris/BI/Updates.lean b/Iris/Iris/BI/Updates.lean index 018e5d9e..59027684 100644 --- a/Iris/Iris/BI/Updates.lean +++ b/Iris/Iris/BI/Updates.lean @@ -396,8 +396,8 @@ theorem step_fupdN_intro {Ei Eo : CoPset} {P : PROP} (Ei_Eo : Ei ⊆ Eo) : simp only [Nat.repeat] refine .trans (later_laterN n).1 ?_ refine .trans (step_fupd_intro Ei_Eo) ?_ - apply BIFUpdate.mono ∘ later_mono ∘ BIFUpdate.mono - exact (step_fupdN_intro (n := n) (P := P) Ei_Eo) + refine mono <| later_mono <| mono ?_ + exact step_fupdN_intro Ei_Eo @[rocq_alias step_fupdN_le] theorem step_fupdN_le {n m : Nat} {Eo Ei : CoPset} {P : PROP} : diff --git a/Iris/Iris/ProgramLogic/EctxLifting.lean b/Iris/Iris/ProgramLogic/EctxLifting.lean index b5e75a53..d1e2f7e3 100644 --- a/Iris/Iris/ProgramLogic/EctxLifting.lean +++ b/Iris/Iris/ProgramLogic/EctxLifting.lean @@ -9,15 +9,12 @@ public import Iris.ProgramLogic.EctxiLanguage namespace Iris.ProgramLogic -open Language.Notation -open EctxLanguage.Notation +open Language.Notation EctxLanguage EctxLanguage.Notation -variable {hlc : outParam Bool} -variable {Expr Ectx State Obs Val} +variable {hlc : outParam Bool} {Expr Ectx State Obs Val} variable [Λ : EctxLanguage Expr Ectx State Obs Val] variable {GF : BundledGFunctors} variable [ι : IrisGS_gen hlc Expr GF] - variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} variable {σ : State} {P Q : IProp GF} {Φ : Val → IProp GF} @@ -36,11 +33,12 @@ theorem wp_lift_base_step_fupd (h : toVal e₁ = none) : imod H $$ Hσ with ⟨%Hred, H⟩ imodintro isplit - · ipure_intro; grind only [EctxLanguage.primStep_reducible_of_baseStep_reducible] + · ipure_intro + grind [primStep_reducible_of_baseStep_reducible] iintro %e₂ %σ₂ %eₜ %Hstep iapply H $$ %_ %_ %_ ipure_intro - apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hred Hstep + exact baseStep_of_primStep_of_baseStep_reducible Hred Hstep @[rocq_alias wp_lift_base_step] theorem wp_lift_base_step (h : toVal e₁ = none) : @@ -60,7 +58,7 @@ theorem wp_lift_base_step (h : toVal e₁ = none) : @[rocq_alias wp_lift_base_stuck] theorem wp_lift_base_stuck (h : toVal e = none) : - EctxLanguage.SubredexesAreValues e → + SubredexesAreValues e → (∀ σ ns obs' nt, stateInterp σ ns obs' nt ={E,∅}=∗ ⌜BaseStep.Stuck (e,σ)⌝) ⊢ WP e @ E ? {{ Φ }} := by iintro %sav_e H @@ -68,11 +66,11 @@ theorem wp_lift_base_stuck (h : toVal e = none) : iintro %σ %ns %obs' %nt Hσ imod H $$ Hσ with %H ipure_intro - apply EctxLanguage.primStep_stuck_of_baseStep_stuck H sav_e + exact primStep_stuck_of_baseStep_stuck H sav_e @[rocq_alias wp_lift_pure_base_stuck] theorem wp_lift_pure_base_stuck (h : toVal e = none) : - EctxLanguage.SubredexesAreValues e → + SubredexesAreValues e → (∀ σ, BaseStep.Stuck (e,σ)) → ⊢ WP e @ E ?{{ Φ }} := by iintro %sav_e %Hstuck @@ -81,7 +79,7 @@ theorem wp_lift_pure_base_stuck (h : toVal e = none) : iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro - ipure_intro - apply Hstuck + exact Hstuck _ @[rocq_alias wp_lift_atomic_base_step_fupd] theorem wp_lift_atomic_base_step_fupd (h : toVal e₁ = none) : @@ -89,20 +87,20 @@ theorem wp_lift_atomic_base_step_fupd (h : toVal e₁ = none) : ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ - (toVal e₂).rec iprop(False) Φ ∗ + (∃ 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 h + iapply wp_lift_atomic_step_fupd (E₂ := E₂) h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ Hσ₁ with ⟨%Hbred, H⟩ imodintro isplit - · ipure_intro; grind only [EctxLanguage.primStep_reducible_of_baseStep_reducible] + · ipure_intro; grind only [primStep_reducible_of_baseStep_reducible] iintro %_ %_ %_ %Hstep iapply H ipure_intro - apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hbred Hstep + 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) : @@ -110,7 +108,7 @@ theorem wp_lift_atomic_base_step (h : toVal e₁ = none) : ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ - (toVal e₂).rec iprop(False) Φ ∗ + (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E {{ Φ }} := by iintro H @@ -119,22 +117,22 @@ theorem wp_lift_atomic_base_step (h : toVal e₁ = none) : imod H $$ Hσ₁ with ⟨%Hbred, H⟩ imodintro isplit - · ipure_intro; grind only [EctxLanguage.primStep_reducible_of_baseStep_reducible] + · ipure_intro; grind only [primStep_reducible_of_baseStep_reducible] inext iintro %e₂ %σ₂ %eₜ %Hstep Hcred iapply H $$ %_ %_ %_ [] Hcred ipure_intro - apply EctxLanguage.baseStep_of_primStep_of_baseStep_reducible Hbred Hstep + 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₁}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ - ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (toVal e₂).rec iprop(False) Φ) + ⌜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 h + iapply wp_lift_atomic_base_step_fupd (E₂ := E₂) h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ %_ %_ %_ %_ %_ Hσ₁ with ⟨$, H⟩ imodintro @@ -145,15 +143,14 @@ theorem wp_lift_atomic_base_step_no_fork_fupd (h : toVal e₁ = none) : subst h simp only [List.length_nil, Nat.add_zero, Algebra.BigOpL.bigOpL_nil] iframe - iapply fupd_mask_intro_discard Std.LawfulSet.subset_refl - exact .rfl + itrivial @[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}=∗ ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -->ᵇ (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ - ⌜eₜ = []⌝ ∗ stateInterp σ₂ (ns + 1) obs' nt ∗ (toVal e₂).rec iprop(False) Φ ) + ⌜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 @@ -169,22 +166,22 @@ theorem wp_lift_atomic_base_step_no_fork (h : toVal e₁ = none) : iframe @[rocq_alias wp_lift_pure_det_base_step_no_fork] -theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (E₂ : CoPset) (h : toVal e₁ = none) : - (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → - (∀ σ₁ obs e₂' σ₂ eₜ', - (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → +theorem wp_lift_pure_det_base_step_no_fork [Inhabited State] (E₂ : CoPset) (h : toVal e₁ = none) + (Hbred : ∀ σ₁, BaseStep.Reducible (e₁, σ₁)) + (Hpure : ∀ σ₁ obs e₂' σ₂ eₜ', + (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) : (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %Hbred %Hpure _ + iintro _ apply wp_lift_pure_det_step_no_fork - · grind [EctxLanguage.primStep_reducible_of_baseStep_reducible] - · grind only [→ EctxLanguage.baseStep_of_primStep_of_baseStep_reducible] + · grind [primStep_reducible_of_baseStep_reducible] + · grind only [→ baseStep_of_primStep_of_baseStep_reducible] @[rocq_alias wp_lift_pure_det_base_step_no_fork'] -theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] (h : toVal e₁ = none) : - (∀ σ₁, BaseStep.Reducible (e₁, σ₁)) → - (∀ σ₁ obs e₂' σ₂ eₜ', - (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → +theorem wp_lift_pure_det_base_step_no_fork' [Inhabited State] (h : toVal e₁ = none) + (Hbred : ∀ σ₁, BaseStep.Reducible (e₁, σ₁)) + (Hpure : ∀ σ₁ obs e₂' σ₂ eₜ', + (e₁, σ₁) -->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) : ▷ (£ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %Hbred %Hpure _ + iintro _ refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork E h Hbred Hpure exact step_fupd_intro Std.LawfulSet.subset_refl diff --git a/Iris/Iris/ProgramLogic/Lifting.lean b/Iris/Iris/ProgramLogic/Lifting.lean index 5d8e1da7..124e1aca 100644 --- a/Iris/Iris/ProgramLogic/Lifting.lean +++ b/Iris/Iris/ProgramLogic/Lifting.lean @@ -11,43 +11,38 @@ public section namespace Iris.ProgramLogic -open Language.Notation BI +open Language Language.Notation BI -variable {hlc : outParam Bool} -variable {Expr State Obs Val} +variable {hlc : outParam Bool} {Expr State Obs Val} variable [Λ : Language Expr State Obs Val] variable {GF : BundledGFunctors} variable [ι : IrisGS_gen hlc Expr GF] - variable {s : Stuckness} {E E₁ E₂ : CoPset} {v : Val} {e e₁ e₂ : Expr} 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,∅}=∗ - ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ - £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=> - -- NOTE: Changed the order of `nt` and `eₜ.length` since in Lean - -- we have `n + 0 = n` and not `0 + n = n` - stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ - WP e₂ @ s; E {{ Φ }} ∗ - [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) - ⊢ WP e₁ @ s; E {{ Φ }} := by - simp only [IProp.ext (wp_unfold (e := e₁)), wp.pre, h, BIBase.Entails.rfl] + (∀ σ₁ ns (obs obs' : List Obs) nt, + stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂,σ₂, eₜ)⌝ -∗ + £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 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 simp [IProp.ext (wp_unfold (e := e₁)), wp.pre, h] @[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,∅}=∗ - ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ - ∀ e₂ σ₂ eₜ, ⌜(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 + (∀ σ₁ ns (obs obs' : List Obs) nt, + stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗ + ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ + ∀ e₂ σ₂ eₜ, ⌜(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σ imod Hwp $$ Hσ with ⟨$, Hwp⟩ @@ -62,11 +57,10 @@ theorem wp_lift_step_fupd (h : toVal e₁ = none) : @[rocq_alias wp_lift_stuck] theorem wp_lift_stuck (h : toVal e = none) : - (∀ σ ns obs nt, - stateInterp σ ns obs nt ={E,∅}=∗ ⌜PrimStep.Stuck (e,σ)⌝) + (∀ σ ns obs nt, stateInterp σ ns obs nt ={E,∅}=∗ ⌜PrimStep.Stuck (e,σ)⌝) ⊢ WP e @ E ? {{ Φ }} := by iintro H - simp only [IProp.ext wp_unfold] + rw [IProp.ext wp_unfold] simp only [wp.pre, h] iintro %σ₁ %ns %obs %obs' %nt Hσ imod H $$ Hσ with %Hirr @@ -97,20 +91,19 @@ theorem wp_lift_step (h : toVal e₁ = none) : @[rocq_alias wp_lift_pure_step_no_fork] theorem wp_lift_pure_step_no_fork [Inhabited State] (E₂ : CoPset) : - -- (∀ σ₁, if s matches .NotStuck then PrimStep.Reducible (e₁,σ₁) else toVal e₁ = none) → (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → (∀ obs σ₁ e₂ σ₂ eₜ, (e₁, σ₁) --> (e₂, σ₂, eₜ) → obs = [] ∧ σ₂ = σ₁ ∧ eₜ = []) → (|={E₁}[E₂]▷=> ∀ obs e₂ eₜ σ, ⌜(e₁, σ) --> (e₂, σ, eₜ)⌝ -∗ £ 1 -∗ WP e₂ @ s; E₁ {{ Φ }}) ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro %Hsafe %Hpure H - iapply wp_lift_step - { grind only [Language.toVal_none_of_reducible, Hsafe default] } + have Hnone : toVal e₁ = none := by grind [Hsafe default] + iapply wp_lift_step Hnone iintro %σ₁ %ns %obs %obs' %nt Hσ imod H iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro Hclose isplit - { ipure_intro; cases s <;> grind only} -- TODO: Why is `grind [cases S]` not enough? + · ipure_intro; cases s <;> grind -- TODO: Why is `grind [cases S]` not enough? inext iintro %e₂ %σ₂ %eₜ %Hstep Hcred obtain ⟨rfl, rfl, rfl⟩ := Hpure _ _ _ _ _ Hstep @@ -142,14 +135,7 @@ theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) (E₂ : CoPset) : ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E₁}[E₂]▷=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗ - (toVal e₂).rec iprop(False) Φ ∗ - -- NOTE: I tried something like this - -- (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ - -- which seems to work better for the proof. However, I - -- don't fully understand why `Option.rec` was used - -- instead, so I haven't made the change. - -- Why is `Option.rec` (or `from_option` in Iris) used - -- in the first place. + (∃ v, ⌜(toVal e₂) = some v⌝ ∧ Φ v) ∗ [∗list] ef ∈ eₜ, WP ef @ s; ⊤ {{ ι.forkPost }}) ⊢ WP e₁ @ s; E₁ {{ Φ }} := by iintro H @@ -158,21 +144,13 @@ theorem wp_lift_atomic_step_fupd (h : toVal e₁ = none) (E₂ : CoPset) : imod H $$ Hσ₁ with ⟨$, H⟩ iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro Hclose %e₂ %σ₂ %eₜ %Hstep Hcred - imod Hclose + imod Hclose with - imod H $$ %_ %_ %_ %Hstep Hcred with H iapply fupd_mask_intro Std.LawfulSet.empty_subset iintro Hclose !> - imod Hclose - imod H with ⟨$, HQ, $⟩ - -- imod H with ⟨$, ⟨%v, %h, HQ⟩, $⟩ - -- iapply wp_value ⟨ToVal.coe_of_toVal_eq_some h⟩ $$ HQ - match h : toVal e₂ with - | some v => - iintro !> - iapply wp_value ⟨ToVal.coe_of_toVal_eq_some h⟩ $$ HQ - | none => - iexfalso; iassumption - + imod Hclose with - + imod H with ⟨$, ⟨%v, %h, HQ⟩, $⟩ + iapply wp_value ⟨ToVal.coe_of_toVal_eq_some h⟩ $$ HQ @[rocq_alias wp_lift_atomic_step] theorem wp_lift_atomic_step (h : toVal e₁ = none) : @@ -180,35 +158,35 @@ theorem wp_lift_atomic_step (h : toVal e₁ = none) : ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗ ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) --> (e₂, σ₂, eₜ)⌝ -∗ £ 1 ={E}=∗ stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length ) ∗ - (toVal e₂).rec iprop(False) Φ ∗ + (∃ 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 h + iapply wp_lift_atomic_step_fupd (E₂ := E) h iintro %σ₁ %ns %obs %obs' %nt Hσ₁ imod H $$ [$] with ⟨$, H⟩ iintro !> %e₂ %σ₂ %eₜ %Hstep Hcred !> !> iapply H $$ %_ %_ %_ %Hstep Hcred @[rocq_alias wp_lift_pure_det_step_no_fork] -theorem wp_lift_pure_det_step_no_fork [Inhabited State] (E₂ : CoPset) : - -- TODO: Why not have this `∀` only in the left match branch? - (∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) → - (∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) --> (e₂', σ₂, eₜ') → - obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) → +theorem wp_lift_pure_det_step_no_fork [Inhabited State] (E₂ : CoPset) + (Hsafe : ∀ σ₁, match s with | .NotStuck => PrimStep.Reducible (e₁,σ₁) | _ => toVal e₁ = none) + (Hpuredet : ∀ σ₁ obs e₂' σ₂ eₜ', (e₁, σ₁) --> (e₂', σ₂, eₜ') → + obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) : (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %Hsafe %Hpuredet H + iintro H iapply wp_lift_pure_step_no_fork E₂ Hsafe (by grind only) iapply step_fupd_wand $$ H iintro H iintro %obs %e' %eₜ' %σ %aux - obtain ⟨rfl, _, rfl, rfl⟩:= Hpuredet _ _ _ _ _ aux + obtain ⟨rfl, _, rfl, rfl⟩ := Hpuredet _ _ _ _ _ aux iassumption @[rocq_alias wp_pure_step_fupd] -theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset): - Language.PureExec φ n e₁ e₂ → φ → (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - iintro %Hexec %Hφ Hwp +theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset) + (Hexec : PureExec φ n e₁ e₂) (Hφ : φ) : + (|={E}[E₂]▷=>^[n] £ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by + iintro Hwp replace Hexec := Hexec.pureExec Hφ induction Hexec using Relation.Iterate.head_induction_on with | rfl => @@ -218,11 +196,11 @@ theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset): iapply Hwp $$ Hz | @head n e₁ e₃ _ _ IH => obtain ⟨Hsafe, Hdet⟩ := ‹e₁ -ᵖ-> e₃› - iapply wp_lift_pure_det_step_no_fork E₂ (e₂ := e₃) (by - intro σ - have : PrimStep.Reducible (e₁, σ) := by grind only [Language.reducible_of_reducibleNoObs] - grind [cases Stuckness] - ) (by grind) + iapply wp_lift_pure_det_step_no_fork E₂ (e₂ := e₃) ?Hred (by grind) + case Hred => + intro σ + have _ : PrimStep.Reducible (e₁, σ) := by grind only [reducible_of_reducibleNoObs] + grind [cases Stuckness] simp only [Nat.repeat] iapply step_fupd_wand $$ Hwp iintro Hwp Hone @@ -234,17 +212,16 @@ theorem wp_pure_step_fupd [Inhabited State] (E₂ : CoPset): iframe @[rocq_alias wp_pure_step_later] -theorem wp_pure_step_later [Inhabited State] : - Language.PureExec φ n e₁ e₂ → φ → ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by - intro Hexec Hφ +theorem wp_pure_step_later [Inhabited State] (Hexec : PureExec φ n e₁ e₂) (Hφ : φ) : + ▷^[n] (£ n -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by refine .trans ?_ (wp_pure_step_fupd E Hexec Hφ) suffices Hwp : ∀ (P : IProp GF), ▷^[n] P ⊢ |={E}▷=>^[n] P by iapply Hwp intro P - clear Hexec -- So it is not captured by the `induction` + clear Hexec induction n with | zero => exact .rfl | succ n IH => simp only [Nat.repeat] rw [IProp.ext <| later_laterN n] - refine (later_mono IH).trans ?_ - apply step_fupd_intro (Std.LawfulSet.subset_refl) + refine (later_mono IH).trans ?_ + exact step_fupd_intro Std.LawfulSet.subset_refl