Merge branch 'total_weakestpre'

_CoqProject

@@ -56,12 +56,16 @@ theories/base_logic/lib/fancy_updates_from_vs.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v
+theories/program_logic/total_weakestpre.v
+theories/program_logic/total_adequacy.v
 theories/program_logic/hoare.v
 theories/program_logic/language.v
 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
@@ -75,6 +79,7 @@ theories/heap_lang/lib/ticket_lock.v
 theories/heap_lang/lib/counter.v
 theories/heap_lang/proofmode.v
 theories/heap_lang/adequacy.v
+theories/heap_lang/total_adequacy.v
 theories/proofmode/base.v
 theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v

theories/heap_lang/lib/assert.v

@@ -9,6 +9,13 @@ Definition assert : val :=
 (* just below ;; *)
 Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
 
+Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
+  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗ WP assert: e @ E [{ Φ }].
+Proof.
+  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
+  wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
+Qed.
+
 Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e `{!Closed [] e} :
   WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗ WP assert: e @ E {{ Φ }}.
 Proof.

theories/heap_lang/lifting.v

 From iris.base_logic Require Export gen_heap.
-From iris.program_logic Require Export weakestpre lifting.
-From iris.program_logic Require Import ectx_lifting.
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
 From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
-Import uPred.
-
-(** Basic rules for language operations. *)
 
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
@@ -39,8 +36,6 @@ Ltac inv_head_step :=
   repeat match goal with
   | _ => progress simplify_map_eq/= (* simplify memory stuff *)
   | H : to_val _ = Some _ |- _ => apply of_to_val in H
-  | H : _ = of_val ?v |- _ =>
-     is_var v; destruct v; first[discriminate H|injection H as H]
   | H : head_step ?e _ _ _ _ |- _ =>
      try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
      and can thus better be avoided. *)
@@ -54,22 +49,6 @@ Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Section lifting.
-Context `{heapG Σ}.
-Implicit Types P Q : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types efs : list expr.
-Implicit Types σ : state.
-
-(** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork s E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
-Proof.
-  rewrite -(wp_lift_pure_det_head_step (Fork e) (Lit LitUnit) [e]) //=; eauto.
-  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id.
-  - intros; inv_head_step; eauto.
-Qed.
-
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
 Local Ltac solve_pure_exec :=
@@ -79,48 +58,69 @@ Local Ltac solve_pure_exec :=
 
 Class AsRec (e : expr) (f x : binder) (erec : expr) :=
   as_rec : e = Rec f x erec.
-Global Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
-Global Instance AsRec_rec_locked_val v f x e :
+Instance AsRec_rec f x e : AsRec (Rec f x e) f x e := eq_refl.
+Instance AsRec_rec_locked_val v f x e :
   AsRec (of_val v) f x e → AsRec (of_val (locked v)) f x e.
 Proof. by unlock. Qed.
 
-Global Instance pure_rec f x (erec e1 e2 : expr)
+Instance pure_rec f x (erec e1 e2 : expr)
     `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
   PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
 Proof. unfold AsRec in *; solve_pure_exec. Qed.
 
-Global Instance pure_unop op e v v' `{!IntoVal e v} :
+Instance pure_unop op e v v' `{!IntoVal e v} :
   PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
+Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
   PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_if_true e1 e2 :
-  PureExec True (If (Lit (LitBool true)) e1 e2) e1.
+Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_if_false e1 e2 :
-  PureExec True (If (Lit (LitBool false)) e1 e2) e2.
+Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
+Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
   PureExec True (Fst (Pair e1 e2)) e1.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
+Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
+Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
 Proof. solve_pure_exec. Qed.
 
-Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
+Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
 Proof. solve_pure_exec. Qed.
 
+Section lifting.
+Context `{heapG Σ}.
+Implicit Types P Q : iProp Σ.
+Implicit Types Φ : val → iProp Σ.
+Implicit Types efs : list expr.
+Implicit Types σ : state.
+
+(** Base axioms for core primitives of the language: Stateless reductions *)
+Lemma wp_fork s E e Φ :
+  ▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
+Proof.
+  iIntros "[HΦ He]".
+  iApply wp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iModIntro; iNext; iIntros "!> /= {$He}". by iApply wp_value.
+Qed.
+Lemma twp_fork s E e Φ :
+  Φ (LitV LitUnit) ∗ WP e @ s; ⊤ [{ _, True }] ⊢ WP Fork e @ s; E [{ Φ }].
+Proof.
+  iIntros "[HΦ He]".
+  iApply twp_lift_pure_det_head_step; [auto|intros; inv_head_step; eauto|].
+  iIntros "!> /= {$He}". by iApply twp_value.
+Qed.
+
 (** Heap *)
 Lemma wp_alloc s E e v :
   IntoVal e v →
@@ -132,6 +132,16 @@ Proof.
   iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_alloc s E e v :
+  IntoVal e v →
+  [[{ True }]] Alloc e @ s; E [[{ l, RET LitV (LitLoc l); l ↦ v }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "_ HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>"; iSplit; first by auto.
+  iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_load s E l q v :
   {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ s; E {{{ RET v; l ↦{q} v }}}.
@@ -142,6 +152,15 @@ Proof.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_load s E l q v :
+  [[{ l ↦{q} v }]] Load (Lit (LitLoc l)) @ s; E [[{ RET v; l ↦{q} v }]].
+Proof.
+  iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto.
+  iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_store s E l v' e v :
   IntoVal e v →
@@ -154,6 +173,17 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_store s E l v' e v :
+  IntoVal e v →
+  [[{ l ↦ v' }]] Store (Lit (LitLoc l)) e @ s; E [[{ RET LitV LitUnit; l ↦ v }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2 σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 
 Lemma wp_cas_fail s E l q v' e1 v1 e2 :
   IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
@@ -166,6 +196,17 @@ Proof.
   iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
+Lemma twp_cas_fail s E l q v' e1 v1 e2 :
+  IntoVal e1 v1 → AsVal e2 → v' ≠ v1 →
+  [[{ l ↦{q} v' }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+  [[{ RET LitV (LitBool false); l ↦{q} v' }]].
+Proof.
+  iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+Qed.
 
 Lemma wp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 → IntoVal e2 v2 →
@@ -179,6 +220,18 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_cas_suc s E l e1 v1 e2 v2 :
+  IntoVal e1 v1 → IntoVal e2 v2 →
+  [[{ l ↦ v1 }]] CAS (Lit (LitLoc l)) e1 e2 @ s; E
+  [[{ RET LitV (LitBool true); l ↦ v2 }]].
+Proof.
+  iIntros (<-%of_to_val <-%of_to_val Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 
 Lemma wp_faa s E l i1 e2 i2 :
   IntoVal e2 (LitV (LitInt i2)) →
@@ -192,4 +245,16 @@ Proof.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
+Lemma twp_faa s E l i1 e2 i2 :
+  IntoVal e2 (LitV (LitInt i2)) →
+  [[{ l ↦ LitV (LitInt i1) }]] FAA (Lit (LitLoc l)) e2 @ s; E
+  [[{ RET LitV (LitInt i1); l ↦ LitV (LitInt (i1 + i2)) }]].
+Proof.
+  iIntros (<-%of_to_val Φ) "Hl HΦ".
+  iApply twp_lift_atomic_head_step_no_fork; auto.
+  iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
+  iSplit; first by eauto. iIntros (v2' σ2 efs Hstep); inv_head_step.
+  iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
+  iModIntro. iSplit=>//. by iApply "HΦ".
+Qed.
 End lifting.

theories/heap_lang/total_adequacy.v

+From iris.program_logic Require Export total_adequacy.
+From iris.heap_lang Require Export adequacy.
+From iris.heap_lang Require Import proofmode notation.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+Definition heap_total Σ `{heapPreG Σ} s e σ φ :
+  (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌝ }]%I) →
+  sn step ([e], σ).
+Proof.
+  intros Hwp; eapply (twp_total _ _); iIntros (?) "".
+  iMod (gen_heap_init σ) as (?) "Hh".
+  iModIntro. iExists gen_heap_ctx; iFrame.
+  iApply (Hwp (HeapG _ _ _)).
+Qed.

theories/program_logic/total_adequacy.v

+From iris.program_logic Require Export total_weakestpre adequacy.
+From iris.algebra Require Import gmap auth agree gset coPset.
+From iris.base_logic Require Import big_op soundness fixpoint.
+From iris.base_logic.lib Require Import wsat.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Section adequacy.
+Context `{irisG Λ Σ}.
+Implicit Types e : expr Λ.
+
+Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
+    (t1 : list (expr Λ)) : iProp Σ :=
+  (∀ t2 σ1 σ2, ⌜step (t1,σ1) (t2,σ2)⌝ -∗
+    state_interp σ1 ={⊤}=∗ state_interp σ2 ∗ twptp t2)%I.
+
+Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
+  ((□ ∀ t, twptp1 t -∗ twptp2 t) →
+  ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.
+Proof.
+  iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
+  iIntros (t2 σ1 σ2) "Hstep Hσ". iMod ("Hwp" with "[$] [$]") as "[$ ?]".
+  by iApply "H".
+Qed.
+
+Local Instance twptp_pre_mono' : BIMonoPred twptp_pre.
+Proof.
+  constructor; first apply twptp_pre_mono.
+  intros wp Hwp n t1 t2 ?%(discrete_iff _ _)%leibniz_equiv; solve_proper.
+Qed.
+
+Definition twptp (t : list (expr Λ)) : iProp Σ :=
+  uPred_least_fixpoint twptp_pre t.
+
+Lemma twptp_unfold t : twptp t ⊣⊢ twptp_pre twptp t.
+Proof. by rewrite /twptp least_fixpoint_unfold. Qed.
+
+Lemma twptp_ind Ψ :
+  ((□ ∀ t, twptp_pre (λ t, Ψ t ∧ twptp t) t -∗ Ψ t) → ∀ t, twptp t -∗ Ψ t)%I.
+Proof.
+  iIntros "#IH" (t) "H".
+  assert (NonExpansive Ψ).
+  { by intros n ?? ->%(discrete_iff _ _)%leibniz_equiv. }
+  iApply (least_fixpoint_strong_ind _ Ψ with "[] H").
+  iIntros "!#" (t') "H". by iApply "IH".
+Qed.
+
+Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
+Proof.
+  iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
+  iApply twptp_ind; iIntros "!#" (t1) "IH"; iIntros (t1' Ht).
+  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 σ2 Hstep) "Hσ".
+  destruct (step_Permutation t1' t1 t2 σ1 σ2) as (t2'&?&?); try done.
+  iMod ("IH" $! t2' with "[% //] Hσ") as "[$ [IH _]]". by iApply "IH".
+Qed.
+
+Lemma twptp_app t1 t2 : twptp t1 -∗ twptp t2 -∗ twptp (t1 ++ t2).
+Proof.
+  iIntros "H1". iRevert (t2). iRevert (t1) "H1".
+  iApply twptp_ind; iIntros "!#" (t1) "IH1". iIntros (t2) "H2".
+  iRevert (t1) "IH1"; iRevert (t2) "H2".
+  iApply twptp_ind; iIntros "!#" (t2) "IH2". iIntros (t1) "IH1".
+  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 σ2 Hstep) "Hσ1".
+  destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' ?? Hstep]; simplify_eq/=.
+  apply app_eq_inv in H as [(t&?&?)|(t&?&?)]; subst.
+  - destruct t as [|e1' ?]; simplify_eq/=.
+    + iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]".
+      { by eapply step_atomic with (t1:=[]). }
+      iModIntro. rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
+      by setoid_rewrite (right_id_L [] (++)).
+    + iMod ("IH1" with "[%] Hσ1") as "[$ [IH1 _]]"; first by econstructor.
+      iAssert (twptp t2) with "[IH2]" as "Ht2".
+      { rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
+        iIntros "!# * [_ ?] //". }
+      iModIntro. rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L.
+      by iApply "IH1".
+  - iMod ("IH2" with "[%] Hσ1") as "[$ [IH2 _]]"; first by econstructor.
+    iModIntro. rewrite -assoc. by iApply "IH2".
+Qed.
+
+Lemma twp_twptp s Φ e : WP e @ s; ⊤ [{ Φ }] -∗ twptp [e].
+Proof.
+  iIntros "He". remember (⊤ : coPset) as E eqn:HE.
+  iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
+  iIntros "!#" (e E Φ); iIntros "IH" (->).
+  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' σ2' Hstep) "Hσ1".
+  destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
+    simplify_eq/=; try discriminate_list.
+  destruct (to_val e1) as [v|] eqn:He1.
+  { apply val_stuck in Hstep; naive_solver. }
+  iMod ("IH" with "Hσ1") as "[_ IH]".
+  iMod ("IH" with "[% //]") as "[$ [[IH _] IHfork]]"; iModIntro.
+  iApply (twptp_app [_] with "[IH]"); first by iApply "IH".
+  clear. iInduction efs as [|e efs] "IH"; simpl.
+  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 σ2 Hstep).
+    destruct Hstep; simplify_eq/=; discriminate_list. }
+  iDestruct "IHfork" as "[[IH' _] IHfork]".
+  iApply (twptp_app [_] with "[IH']"); [by iApply "IH'"|by iApply "IH"].
+Qed.
+
+Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
+
+Lemma twptp_total σ t : world σ -∗ twptp t -∗ ▷ ⌜sn step (t, σ)⌝.
+Proof.
+  iIntros "Hw Ht". iRevert (σ) "Hw". iRevert (t) "Ht".
+  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ) "(Hw&HE&Hσ)".
+  iApply (pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] Hstep).
+  rewrite /twptp_pre fupd_eq /fupd_def.
+  iMod ("IH" with "[% //] Hσ [$Hw $HE]") as ">(Hw & HE & Hσ & [IH _])".
+  iApply "IH". by iFrame.
+Qed.
+End adequacy.
+
+Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
+  (∀ `{Hinv : invG Σ},
+     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ ∗ WP e @ s; ⊤ [{ Φ }])%I) →
+  sn step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
+Proof.
+  intros Hwp.
+  eapply (soundness (M:=iResUR Σ) _ 1); iIntros "/=".
+  iMod wsat_alloc as (Hinv) "[Hw HE]".
+  rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
+  iDestruct "Hwp" as (Istate) "[HI Hwp]".
+  iApply (@twptp_total _ _ (IrisG _ _ Hinv Istate) with "[$Hw $HE $HI]").
+  by iApply (@twp_twptp _ _ (IrisG _ _ Hinv Istate)).
+Qed.

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.

theories/program_logic/weakestpre.v

@@ -13,16 +13,14 @@ Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
 Inductive stuckness := NotStuck | MaybeStuck.
 
-Definition stuckness_le (s1 s2 : stuckness) : bool :=
+Definition stuckness_leb (s1 s2 : stuckness) : bool :=
   match s1, s2 with
   | MaybeStuck, NotStuck => false
   | _, _ => true
   end.
-Instance: PreOrder stuckness_le.
-Proof.
-  split; first by case. move=>s1 s2 s3. by case: s1; case: s2; case: s3.
-Qed.