Lifting lemmas for total weakest preconditions.

_CoqProject

@@ -64,6 +64,8 @@ theories/program_logic/ectx_language.v
 theories/program_logic/ectxi_language.v
 theories/program_logic/ectx_lifting.v
 theories/program_logic/ownp.v
+theories/program_logic/total_lifting.v
+theories/program_logic/total_ectx_lifting.v
 theories/heap_lang/lang.v
 theories/heap_lang/tactics.v
 theories/heap_lang/lifting.v

theories/program_logic/total_ectx_lifting.v

+(** Some derived lemmas for ectx-based languages *)
+From iris.program_logic Require Export ectx_language.
+From iris.program_logic Require Export total_weakestpre total_lifting.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Section wp.
+Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Hint Resolve head_prim_reducible head_reducible_prim_step.
+
+Lemma twp_lift_head_step {s E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (?) "H". iApply (twp_lift_step _ E)=>//. iIntros (σ1) "Hσ".
+  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
+  iSplit; [destruct s; auto|]. iIntros (e2 σ2 efs) "%".
+  iApply "H". by eauto.
+Qed.
+
+Lemma twp_lift_pure_head_step {s E Φ} e1 :
+  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
+  (|={E}=> ∀ e2 efs σ, ⌜head_step e1 σ e2 σ efs⌝ →
+    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof using Hinh.
+  iIntros (??) ">H". iApply twp_lift_pure_step; eauto.
+  iIntros "!>" (????). iApply "H"; eauto.
+Qed.
+
+Lemma twp_lift_atomic_head_step {s E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      state_interp σ2 ∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (?) "H". iApply twp_lift_atomic_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
+  iSplit; first by destruct s; auto. iIntros (e2 σ2 efs) "%". iApply "H"; auto.
+Qed.
+
+Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜head_reducible e1 σ1⌝ ∗
+    ∀ e2 σ2 efs, ⌜head_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      ⌜efs = []⌝ ∗ state_interp σ2 ∗ default False (to_val e2) Φ)
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
+  iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
+  iIntros (v2 σ2 efs) "%".
+  iMod ("H" $! v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
+Qed.
+
+Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
+  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1 e2' σ2 efs',
+    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
+  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof using Hinh. eauto using twp_lift_pure_det_step. Qed.
+
+Lemma twp_lift_pure_det_head_step_no_fork {s E Φ} e1 e2 :
+  to_val e1 = None →
+  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1 e2' σ2 efs',
+    head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
+  WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
+Proof using Hinh.
+  intros. rewrite -(twp_lift_pure_det_step e1 e2 []) /= ?right_id; eauto.
+Qed.
+End wp.

theories/program_logic/total_lifting.v

+From iris.program_logic Require Export total_weakestpre.
+From iris.base_logic Require Export big_op.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Section lifting.
+Context `{irisG Λ Σ}.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+Implicit Types σ : state Λ.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+
+Lemma twp_lift_step s E Φ e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E,∅}=∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+      state_interp σ2 ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
+
+(** Derived lifting lemmas. *)
+Lemma twp_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
+  (∀ σ1, reducible e1 σ1) →
+  (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
+  (|={E}=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
+    WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (Hsafe Hstep) "H". iApply twp_lift_step.
+  { eapply reducible_not_val, (Hsafe inhabitant). }
+  iIntros (σ1) "Hσ". iMod "H".
+  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
+  iSplit; [by destruct s|]; iIntros (e2 σ2 efs ?).
+  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
+  iMod "Hclose" as "_". iFrame "Hσ". iApply "H"; auto.
+Qed.
+
+(* Atomic steps don't need any mask-changing business here, one can
+   use the generic lemmas here. *)
+Lemma twp_lift_atomic_step {s E Φ} e1 :
+  to_val e1 = None →
+  (∀ σ1, state_interp σ1 ={E}=∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
+      state_interp σ2 ∗
+      default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (?) "H". iApply (twp_lift_step _ E _ e1)=>//; iIntros (σ1) "Hσ1".
+  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
+  iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
+  iIntros "!>" (e2 σ2 efs) "%". iMod "Hclose" as "_".
+  iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
+  destruct (to_val e2) eqn:?; last by iExFalso.
+  by iApply twp_value.
+Qed.
+
+Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
+  (∀ σ1, reducible e1 σ1) →
+  (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
+  (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+  ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step _ E); try done.
+  { by intros; eapply Hpuredet. }
+  by iIntros "!>" (e' efs' σ (_&->&->)%Hpuredet).
+Qed.
+
+Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ :
+  PureExec φ e1 e2 →
+  φ →
+  WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
+Proof.
+  iIntros ([??] Hφ) "HWP".
+  iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto].
+Qed.
+End lifting.