feat: add lifting and ectx lifting

Iris/Iris/BI/Updates.lean

@@ -401,6 +401,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
@@ -409,6 +413,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) ?_
+    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} :
     n ≤ m → Ei ⊆ Eo → (|={Eo}[Ei]▷=>^[n] P) ⊢ |={Eo}[Ei]▷=>^[m] P

Iris/Iris/ProgramLogic/EctxLifting.lean

@@ -0,0 +1,187 @@
+/-
+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
+public import Iris.ProgramLogic.EctxiLanguage
+
+namespace Iris.ProgramLogic
+
+open Language.Notation EctxLanguage EctxLanguage.Notation
+
+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}
+
+@[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₁,σ₁)⌝ ∗
+      ∀ e₂ σ₂ eₜ, ⌜(e₁,σ₁) -<obs>->ᵇ (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 ⟨%Hred, H⟩
+  imodintro
+  isplit
+  · ipure_intro
+    grind [primStep_reducible_of_baseStep_reducible]
+  iintro %e₂ %σ₂ %eₜ %Hstep
+  iapply H $$ %_ %_ %_
+  ipure_intro
+  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,∅}=∗
+      ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗
+      ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<obs>->ᵇ (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σ
+  imod H $$ [$] with ⟨$, H⟩
+  iintro !> %e₂ %σ₂ %eₜ %Hbstep Hcred !> !>
+  iapply H $$ %_ %_ %_ %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,σ)⌝)
+    ⊢ WP e @ E ? {{ Φ }} := by
+  iintro %sav_e H
+  iapply wp_lift_stuck h
+  iintro %σ %ns %obs' %nt Hσ
+  imod H $$ Hσ with %H
+  ipure_intro
+  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) :
+    SubredexesAreValues e →
+    (∀ σ, BaseStep.Stuck (e,σ)) →
+    ⊢ WP e @ E ?{{ Φ }} := by
+  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 -
+  ipure_intro
+  exact 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 ={E₁}=∗
+      ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗
+      ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<obs>->ᵇ (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σ₁
+  imod H $$ Hσ₁ with ⟨%Hbred, H⟩
+  imodintro
+  isplit
+  · ipure_intro; grind only [primStep_reducible_of_baseStep_reducible]
+  iintro %_ %_ %_ %Hstep
+  iapply H
+  ipure_intro
+  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}=∗
+      ⌜BaseStep.Reducible (e₁, σ₁)⌝ ∗
+      ▷ ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<obs>->ᵇ (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σ₁
+  imod H $$ Hσ₁ with ⟨%Hbred, H⟩
+  imodintro
+  isplit
+  · ipure_intro; grind only [primStep_reducible_of_baseStep_reducible]
+  inext
+  iintro %e₂ %σ₂ %eₜ %Hstep Hcred
+  iapply H $$ %_ %_ %_ [] Hcred
+  ipure_intro
+  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₁, σ₁) -<obs>->ᵇ (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⟩
+  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
+  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₁, σ₁) -<obs>->ᵇ (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σ₁
+  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
+
+@[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)
+    (Hbred : ∀ σ₁, BaseStep.Reducible (e₁, σ₁))
+    (Hpure : ∀ σ₁ obs e₂' σ₂ eₜ',
+      (e₁, σ₁) -<obs>->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) :
+    (|={E}[E₂]▷=> £ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by
+  iintro _
+  apply wp_lift_pure_det_step_no_fork
+  · 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)
+    (Hbred : ∀ σ₁, BaseStep.Reducible (e₁, σ₁))
+    (Hpure : ∀ σ₁ obs e₂' σ₂ eₜ',
+      (e₁, σ₁) -<obs>->ᵇ (e₂', σ₂, eₜ') → obs = [] ∧ σ₂ = σ₁ ∧ e₂' = e₂ ∧ eₜ' = []) :
+    ▷ (£ 1 -∗ WP e₂ @ s; E {{ Φ }}) ⊢ WP e₁ @ s; E {{ Φ }} := by
+  iintro _
+  refine .trans ?_ <| wp_lift_pure_det_base_step_no_fork E h Hbred Hpure
+  exact step_fupd_intro Std.LawfulSet.subset_refl