fix TWP

theories/heap_lang/lifting.v

@@ -49,12 +49,13 @@ Ltac inv_head_step :=
 
 Local Hint Extern 0 (atomic _ _) => solve_atomic.
 Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
+Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _; simpl.
 
 Local Hint Constructors head_step.
 Local Hint Resolve alloc_fresh.
 Local Hint Resolve to_of_val.
 
-Local Ltac solve_exec_safe := intros; subst; do 4 eexists; econstructor; eauto.
+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 :=
   unfold IntoVal in *;
@@ -148,9 +149,9 @@ Proof.
   iIntros (σ1 κs) "[Hσ Hκs] !>"; iSplit.
   (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
   { iPureIntro. repeat eexists. by apply alloc_fresh. }
-  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
+  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Φ".
+  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_load s E l q v :
@@ -168,8 +169,8 @@ Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto.
-  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
-  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_store s E l v' e v :
@@ -196,9 +197,9 @@ Proof.
   iSplit.
   (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
   { iPureIntro. repeat eexists. constructor; eauto. }
-  iIntros (κ κs' v2 σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (κ v2 σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
+  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_cas_fail s E l q v' e1 v1 e2 :
@@ -220,8 +221,8 @@ Proof.
   iIntros (<- [v2 <-] ?? Φ) "Hl HΦ".
   iApply twp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1 κs) "[Hσ Hκs] !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
-  iSplit; first by eauto. iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
-  iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
+  iSplit; first by eauto. iIntros (κ v2' σ2 efs Hstep); inv_head_step.
+  iModIntro; iSplit=> //. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_cas_suc s E l e1 v1 e2 v2 :
@@ -250,9 +251,9 @@ Proof.
   iSplit.
   (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
   { iPureIntro. repeat eexists. by econstructor. }
-  iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
+  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 Lemma wp_faa s E l i1 e2 i2 :
@@ -281,9 +282,9 @@ Proof.
   iSplit.
   (* TODO (MR) this used to be done by eauto. Why does it not work any more? *)
   { iPureIntro. repeat eexists. by constructor. }
-  iIntros (κ κs' v2' σ2 efs [Hstep ->]); inv_head_step.
+  iIntros (κ v2' σ2 efs Hstep); inv_head_step.
   iMod (@gen_heap_update with "Hσ Hl") as "[$ Hl]".
-  iModIntro. iSplit=>//. iFrame. by iApply "HΦ".
+  iModIntro. iSplit=>//. iSplit; first done. iFrame. by iApply "HΦ".
 Qed.
 
 (** Lifting lemmas for creating and resolving prophecy variables *)

theories/program_logic/ectx_language.v

@@ -99,6 +99,8 @@ Section ectx_language.
 
   Definition head_reducible (e : expr Λ) (σ : state Λ) :=
     ∃ κ e' σ' efs, head_step e σ κ e' σ' efs.
+  Definition head_reducible_no_obs (e : expr Λ) (σ : state Λ) :=
+    ∃ e' σ' efs, head_step e σ None e' σ' efs.
   Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ κ e' σ' efs, ¬head_step e σ κ e' σ' efs.
   Definition head_stuck (e : expr Λ) (σ : state Λ) :=
@@ -143,11 +145,16 @@ Section ectx_language.
     head_step e1 σ1 κ e2 σ2 efs → prim_step e1 σ1 κ e2 σ2 efs.
   Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
 
+  Lemma head_reducible_no_obs_reducible e σ :
+    head_reducible_no_obs e σ → head_reducible e σ.
+  Proof. intros (?&?&?&?). eexists. eauto. Qed.
   Lemma not_head_reducible e σ : ¬head_reducible e σ ↔ head_irreducible e σ.
   Proof. unfold head_reducible, head_irreducible. naive_solver. Qed.
 
   Lemma head_prim_reducible e σ : head_reducible e σ → reducible e σ.
   Proof. intros (κ&e'&σ'&efs&?). eexists κ, e', σ', efs. by apply head_prim_step. Qed.
+  Lemma head_prim_reducible_no_obs e σ : head_reducible_no_obs e σ → reducible_no_obs e σ.
+  Proof. intros (e'&σ'&efs&?). eexists e', σ', efs. by apply head_prim_step. Qed.
   Lemma head_prim_irreducible e σ : irreducible e σ → head_irreducible e σ.
   Proof.
     rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
@@ -208,15 +215,15 @@ Section ectx_language.
   Qed.
 
   Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
-    (∀ σ, P → head_reducible e1 σ) →
+    (∀ σ, P → head_reducible_no_obs e1 σ) →
     (∀ σ1 κ e2' σ2 efs,
       P → head_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
     PureExec P e1 e2.
   Proof.
     intros Hp1 Hp2. split.
-    - intros σ ?. destruct (Hp1 σ) as (κ & e2' & σ2 & efs & ?); first done.
-      eexists κ, e2', σ2, efs. by apply head_prim_step.
-    - intros σ1 κ e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
+    - intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done.
+      eexists e2', σ2, efs. by apply head_prim_step.
+    - intros σ1 κ e2' σ2 efs ? ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
   Qed.
 
   Global Instance pure_exec_fill K e1 e2 φ :

theories/program_logic/language.v

@@ -72,6 +72,9 @@ Section language.
 
   Definition reducible (e : expr Λ) (σ : state Λ) :=
     ∃ κ e' σ' efs, prim_step e σ κ e' σ' efs.
+  (* Total WP only permits reductions without observations *)
+  Definition reducible_no_obs (e : expr Λ) (σ : state Λ) :=
+    ∃ e' σ' efs, prim_step e σ None e' σ' efs.
   Definition irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ κ e' σ' efs, ¬prim_step e σ κ e' σ' efs.
   Definition stuck (e : expr Λ) (σ : state Λ) :=
@@ -130,6 +133,8 @@ Section language.
   Proof. unfold reducible, irreducible. naive_solver. Qed.
   Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
   Proof. intros (?&?&?&?&?); eauto using val_stuck. Qed.
+  Lemma reducible_no_obs_reducible e σ : reducible_no_obs e σ → reducible e σ.
+  Proof. intros (?&?&?&?); eexists; eauto. Qed.
   Lemma val_irreducible e σ : is_Some (to_val e) → irreducible e σ.
   Proof. intros [??] ???? ?%val_stuck. by destruct (to_val e). Qed.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
@@ -145,6 +150,12 @@ Section language.
     intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
     apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
   Qed.
+  Lemma reducible_no_obs_fill `{LanguageCtx Λ K} e σ :
+    to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ.
+  Proof.
+    intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
+    apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
+  Qed.
   Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → irreducible e σ → irreducible (K e) σ.
   Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
@@ -167,7 +178,7 @@ Section language.
 
   Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
     pure_exec_safe σ :
-      P → reducible e1 σ;
+      P → reducible_no_obs e1 σ;
     pure_exec_puredet σ1 κ e2' σ2 efs :
       P → prim_step e1 σ1 κ e2' σ2 efs → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
   }.
@@ -183,10 +194,10 @@ Section language.
     PureExec φ (K e1) (K e2).
   Proof.
     intros [Hred Hstep]. split.
-    - unfold reducible in *. naive_solver eauto using fill_step.
+    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
     - intros σ1 κ e2' σ2 efs ? Hpstep.
       destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
-      + destruct (Hred σ1) as (? & ? & ? & ? & ?); eauto using val_stuck.
+      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
       + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
   Qed.
 

theories/program_logic/lifting.v

@@ -11,6 +11,8 @@ Implicit Types σ : state Λ.
 Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
+Hint Resolve reducible_no_obs_reducible.
+
 Lemma wp_lift_step_fupd s E Φ e1 :
   to_val e1 = None →
   (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗

theories/program_logic/total_adequacy.v

@@ -12,15 +12,15 @@ Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     (t1 : list (expr Λ)) : iProp Σ :=
-  (∀ t2 σ1 κ κs κs' σ2, ⌜step (t1,σ1) κ (t2,σ2) ∧ κs = cons_obs κ κs'⌝ -∗
-    state_interp σ1 κs ={⊤}=∗ state_interp σ2 κs' ∗ twptp t2)%I.
+  (∀ t2 σ1 κ κs σ2, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
+    state_interp σ1 κs ={⊤}=∗ ⌜κ = None⌝ ∗ state_interp σ2 κs ∗ twptp t2)%I.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
   (<pers> (∀ 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 κ κs κs' σ2) "Hstep Hσ". iMod ("Hwp" with "[$] [$]") as "[$ ?]".
+  iIntros (t2 σ1 κ κs σ2) "Hstep Hσ". iMod ("Hwp" with "[$] [$]") as "[$ [$ ?]]".
   by iApply "H".
 Qed.
 
@@ -50,9 +50,9 @@ 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 κ κs κs' σ2 [Hstep ->]) "Hσ".
+  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ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".
+  iMod ("IH" $! t2' with "[% //] Hσ") as "($ & $ & IH & _)". by iApply "IH".
 Qed.
 
 Lemma twptp_app t1 t2 : twptp t1 -∗ twptp t2 -∗ twptp (t1 ++ t2).
@@ -61,21 +61,21 @@ Proof.
   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 κ κs κs' σ2 [Hstep ->]) "Hσ1".
+  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 κ κs σ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 _]]".
-      { split. by eapply step_atomic with (t1:=[]). reflexivity. }
+    + 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 split; econstructor.
+    + 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 split; econstructor.
+  - iMod ("IH2" with "[%] Hσ1") as "($ & $ & IH2 & _)"; first by econstructor.
     iModIntro. rewrite -assoc. by iApply "IH2".
 Qed.
 
@@ -84,44 +84,40 @@ 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' κ κs κs' σ2' [Hstep ->]) "Hσ1".
+  rewrite twptp_unfold /twptp_pre /twp_pre. iIntros (t1' σ1' κ κs σ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.
+  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 κ κs κs' σ2 [Hstep ->]).
+  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 κ κs σ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 σ κs := (wsat ∗ ownE ⊤ ∗ state_interp σ κs)%I.
+Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ [])%I.
 
-(* TODO (MR) prove twtp_total *)
-(*
-Lemma twptp_total σ κs t : world σ κs -∗ twptp t -∗ ▷ ⌜sn erased_step (t, σ)⌝.
+Lemma twptp_total σ t : world σ -∗ twptp t -∗ ▷ ⌜sn erased_step (t, σ)⌝.
 Proof.
-  iIntros "Hw Ht". iRevert (σ κs) "Hw". iRevert (t) "Ht".
-  iApply twptp_ind; iIntros "!#" (t) "IH"; iIntros (σ κs) "(Hw&HE&Hσ)".
-  iApply (pure_mono _ _ (Acc_intro _)).
+  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 uPred_fupd_eq /uPred_fupd_def.
-  iMod ("IH" with "[% //] Hσ [$Hw $HE]") as ">(Hw & HE & Hσ & [IH _])".
+  iMod ("IH" with "[% //] Hσ [$Hw $HE]") as ">(Hw & HE & % & Hσ & [IH _])".
   iApply "IH". by iFrame.
 Qed.
-*)
+
 End adequacy.
 
-(* TODO (MR) prove twp_total *)
-(*
-Theorem twp_total Σ Λ `{invPreG Σ} s e σ κs Φ :
+Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → list (observation Λ) -> iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ _ Hinv stateI in
-       stateI σ κs ∗ WP e @ s; ⊤ [{ Φ }])%I) →
+       stateI σ [] ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
   intros Hwp.
@@ -132,4 +128,3 @@ Proof.
   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

@@ -10,24 +10,25 @@ 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.
+Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step head_reducible_no_obs_reducible.
 
 Lemma twp_lift_head_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
-    ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
-      state_interp σ2 κs' ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+    ⌜head_reducible_no_obs e1 σ1⌝ ∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
+      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
+      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 κs) "Hσ".
   iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
-  iSplit; [destruct s; auto|]. iIntros (κ κs' e2 σ2 efs [Hstep ->]).
+  iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs Hstep).
   iApply "H". by eauto.
 Qed.
 
 Lemma twp_lift_pure_head_step {s E Φ} e1 :
-  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs → κ = None ∧ σ1 = σ2) →
   (|={E}=> ∀ κ e2 efs σ, ⌜head_step e1 σ κ e2 σ efs⌝ →
     WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
@@ -40,42 +41,42 @@ Qed.
 Lemma twp_lift_atomic_head_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κs, state_interp σ1 κs ={E}=∗
-    ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
-      state_interp σ2 κs'∗
+    ⌜head_reducible_no_obs e1 σ1⌝ ∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
+      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
       from_option Φ 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 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
-  iSplit; first by destruct s; auto. iIntros (κ κs' e2 σ2 efs [Hstep ->]). iApply "H"; eauto.
+  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs Hstep). iApply "H"; eauto.
 Qed.
 
 Lemma twp_lift_atomic_head_step_no_fork {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κs, state_interp σ1 κs ={E}=∗
-    ⌜head_reducible e1 σ1⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
-      ⌜efs = []⌝ ∗ state_interp σ2 κs' ∗ from_option Φ False (to_val e2))
+    ⌜head_reducible_no_obs e1 σ1⌝ ∗
+    ∀ κ e2 σ2 efs, ⌜head_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
+      ⌜κ = None⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 κs ∗ from_option Φ False (to_val e2))
   ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (?) "H". iApply twp_lift_atomic_head_step; eauto.
   iIntros (σ1 κs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
-  iIntros (κ κs' v2 σ2 efs [Hstep ->]).
-  iMod ("H" $! κ κs' v2 σ2 efs with "[# //]") as "(% & $ & $)"; subst; auto.
+  iIntros (κ v2 σ2 efs Hstep).
+  iMod ("H" with "[# //]") as "($ & % & $ & $)"; subst; auto.
 Qed.
 
 Lemma twp_lift_pure_det_head_step {s E Φ} e1 e2 efs :
-  (∀ σ1, head_reducible e1 σ1) →
+  (∀ σ1, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ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.
+Proof using Hinh. eauto 10 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, head_reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs',
     head_step e1 σ1 κ e2' σ2 efs' → κ = None ∧ σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].

theories/program_logic/total_lifting.v

@@ -14,28 +14,29 @@ Implicit Types Φ : val Λ → iProp Σ.
 Lemma twp_lift_step s E Φ e1 :
   to_val e1 = None →
   (∀ σ1 κs, state_interp σ1 κs ={E,∅}=∗
-    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
-      state_interp σ2 κs' ∗ WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
+    ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
+    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
+      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗ 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, reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = None /\ σ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). }
+  { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
   iIntros (σ1 κs) "Hσ". iMod "H".
   iMod fupd_intro_mask' as "Hclose"; last iModIntro; first set_solver.
-  iSplit; [by destruct s|]; iIntros (κ κs' e2 σ2 efs [Hstep' ->]).
+  iSplit; [by destruct s|]. iIntros (κ e2 σ2 efs Hstep').
   destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
-  iMod "Hclose" as "_". iFrame "Hσ". iApply "H"; auto.
+  iMod "Hclose" as "_". iModIntro. iSplit; first done.
+  iFrame "Hσ". iApply "H"; auto.
 Qed.
 
 (* Atomic steps don't need any mask-changing business here, one can
@@ -43,23 +44,23 @@ Qed.
 Lemma twp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1 κs, state_interp σ1 κs ={E}=∗
-    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-    ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={E}=∗
-      state_interp σ2 κs' ∗
+    ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
+    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
+      ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
       from_option Φ 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 κs) "Hσ1".
   iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
   iMod (fupd_intro_mask' E ∅) as "Hclose"; first set_solver.
-  iIntros "!>" (κ κs' e2 σ2 efs) "%". iMod "Hclose" as "_".
-  iMod ("H" $! κ κs' e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
+  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.
   iApply twp_value; last done. by apply of_to_val.
 Qed.
 
 Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
-  (∀ σ1, reducible e1 σ1) →
+  (∀ σ1, reducible_no_obs e1 σ1) →
   (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = None /\ σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={E}=> WP e2 @ s; E [{ Φ }] ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ [{ _, True }])
   ⊢ WP e1 @ s; E [{ Φ }].

theories/program_logic/total_weakestpre.v

@@ -10,10 +10,10 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
   match to_val e1 with
   | Some v => |={E}=> Φ v
   | None => ∀ σ1 κs,
-     state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
-     ∀ κ κs' e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs ∧ κs = cons_obs κ κs'⌝ ={∅,E}=∗
-       state_interp σ2 κs' ∗ wp E e2 Φ ∗
-       [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
+     state_interp σ1 κs ={E,∅}=∗ ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
+     ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
+       ⌜κ = None⌝ ∗ state_interp σ2 κs ∗
+       wp E e2 Φ ∗ [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
   end%I.
 
 Lemma twp_pre_mono `{irisG Λ Σ} s
@@ -24,8 +24,9 @@ Proof.
   iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
   destruct (to_val e1) as [v|]; first done.
   iIntros (σ1 κs) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
-  iIntros (κ κs' e2 σ2 efs) "Hstep".
-  iMod ("Hwp" with "Hstep") as "($ & Hwp & Hfork)"; iModIntro; iSplitL "Hwp".
+  iIntros (κ e2 σ2 efs) "Hstep".
+  iMod ("Hwp" with "Hstep") as "($ & $ & Hwp & Hfork)"; iModIntro.
+  iSplitL "Hwp".
   - by iApply "H".
   - iApply (@big_sepL_impl with "[$Hfork]"); iIntros "!#" (k e _) "Hwp".
     by iApply "H".
@@ -44,7 +45,7 @@ Proof.
     iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
   - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
       [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
-    rewrite /uncurry3 /twp_pre. do 22 (f_equiv || done). by apply Hwp, pair_ne.
+    rewrite /uncurry3 /twp_pre. do 22 (f_equiv || done). by apply pair_ne.
 Qed.
 
 Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
@@ -107,8 +108,8 @@ Proof.