Revert "Revert "Merge branch 'swasey/progress' into 'master'""

This reverts commit 913059d2.

CHANGELOG.md

@@ -13,6 +13,13 @@ Changes in and extensions of the theory:
 * Constructions for least and greatest fixed points over monotone predicates
   (defined in the logic of Iris using impredicative quantification).
 * Add a proof of the inverse of `wp_bind`.
+* Support verifying code that might get stuck by distinguishing
+  "progressive" vs. "non-progressive" weakest preconditions. (See
+  [Swasey et al. OOPSLA '17] for examples.) The progressive `WP e @ E
+  {{ Φ }}` ensures that, as `e` runs, it does not get stuck. The
+  non-progressive `WP e @ E ?{{ Φ }}` ensures that, as usual, all
+  invariants are preserved while `e` runs, but it permits execution to
+  get stuck. The former implies the latter.
 
 Changes in Coq:
 
@@ -88,6 +95,13 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Move the `prelude` folder to its own project: std++
 * The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
   stated in the logic, i.e. they are `iApply` friendly.
+* Use *stuckness bits* `s` to define progressive vs. non-progressive
+  WP. The full judgment is `WP e @ s; E {{ Φ }}`; progressive WP uses
+  `s = not_stuck` while non-progressive WP uses `s = maybe_stuck`.
+* Restore the original, stronger notion of atomicity alongside the
+  weaker notion. These are `Atomic s e` where the stuckness bit `s`
+  indicates whether expression `e` is weakly (`s = not_stuck`) or
+  strongly (`s = maybe_stuck`) atomic.
 
 ## Iris 3.0.0 (released 2017-01-11)
 

naming.txt

@@ -17,7 +17,7 @@ o
 p
 q
 r : iRes = resources
-s : state (STSs)
+s : state (STSs), stuckness bits
 t
 u
 v : val = values of language

theories/heap_lang/adequacy.v

@@ -14,9 +14,9 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
-Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
-  (∀ `{heapG Σ}, WP e {{ v, ⌜φ v⌝ }}%I) →
-  adequate e σ φ.
+Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
+  (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}%I) →
+  adequate s e σ φ.
 Proof.
   intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".

theories/heap_lang/lifting.v

@@ -47,7 +47,7 @@ Ltac inv_head_step :=
      inversion H; subst; clear H
   end.
 
-Local Hint Extern 0 (atomic _) => solve_atomic.
+Local Hint Extern 0 (atomic _ _) => solve_atomic.
 Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _; simpl.
 
 Local Hint Constructors head_step.
@@ -62,21 +62,21 @@ Implicit Types efs : list expr.
 Implicit Types σ : state.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {E e} K Φ :
-  WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
+Lemma wp_bind {s E e} K Φ :
+  WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }} ⊢ WP fill K e @ s; E {{ Φ }}.
 Proof. exact: wp_ectx_bind. Qed.
 
-Lemma wp_bindi {E e} Ki Φ :
-  WP e @ E {{ v, WP fill_item Ki (of_val v) @ E {{ Φ }} }} ⊢
-     WP fill_item Ki e @ E {{ Φ }}.
+Lemma wp_bindi {s E e} Ki Φ :
+  WP e @ s; E {{ v, WP fill_item Ki (of_val v) @ s; E {{ Φ }} }} ⊢
+     WP fill_item Ki e @ s; E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
-Lemma wp_fork E e Φ :
-  ▷ Φ (LitV LitUnit) ∗ ▷ WP e {{ _, True }} ⊢ WP Fork e @ E {{ Φ }}.
+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.
+  - by rewrite -step_fupd_intro // later_sep -(wp_value _ _ _ (Lit _)) // right_id.
   - intros; inv_head_step; eauto.
 Qed.
 
@@ -132,9 +132,9 @@ Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
 Proof. solve_pure_exec. Qed.
 
 (** Heap *)
-Lemma wp_alloc E e v :
+Lemma wp_alloc s E e v :
   IntoVal e v →
-  {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
+  {{{ True }}} Alloc e @ s; E {{{ l, RET LitV (LitLoc l); l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
@@ -143,8 +143,8 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_load E l q v :
-  {{{ ▷ l ↦{q} v }}} Load (Lit (LitLoc l)) @ E {{{ RET v; l ↦{q} v }}}.
+Lemma wp_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 wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
@@ -153,9 +153,9 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_store E l v' e v :
+Lemma wp_store s E l v' e v :
   IntoVal e v →
-  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l ↦ v }}}.
+  {{{ ▷ l ↦ v' }}} Store (Lit (LitLoc l)) e @ s; E {{{ RET LitV LitUnit; l ↦ v }}}.
 Proof.
   iIntros (<-%of_to_val Φ) ">Hl HΦ".
   iApply wp_lift_atomic_head_step_no_fork; auto.
@@ -165,9 +165,9 @@ Proof.
   iModIntro. iSplit=>//. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_fail E l q v' e1 v1 e2 :
+Lemma wp_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 @ E
+  {{{ ▷ 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Φ".
@@ -177,9 +177,9 @@ Proof.
   iModIntro; iSplit=> //. iFrame. by iApply "HΦ".
 Qed.
 
-Lemma wp_cas_suc E l e1 v1 e2 v2 :
+Lemma wp_cas_suc s E l e1 v1 e2 v2 :
   IntoVal e1 v1 → IntoVal e2 v2 →
-  {{{ ▷ l ↦ v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
+  {{{ ▷ 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Φ".

theories/heap_lang/proofmode.v

@@ -5,21 +5,21 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
+Lemma tac_wp_pure `{heapG Σ} K Δ Δ' s E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 Δ Δ' →
-  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K e2 @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
-Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
+Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
   IntoVal e v →
-  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
@@ -27,7 +27,7 @@ Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [simpl; apply _                 (* PureExec *)
@@ -52,9 +52,9 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" := wp_case; wp_let.
 
-Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
-  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
-  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e :
+  envs_entails Δ (WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
 Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
 
 Ltac wp_bind_core K :=
@@ -66,7 +66,7 @@ Ltac wp_bind_core K :=
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
     || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
@@ -79,13 +79,13 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types Δ : envs (iResUR Σ).
 
-Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
+Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
   IntoVal e v →
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
-  envs_entails Δ (WP fill K (Alloc e) @ E {{ Φ }}).
+    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc e) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ?? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
@@ -94,11 +94,11 @@ Proof.
   by rewrite right_id HΔ'.
 Qed.
 
-Lemma tac_wp_load Δ Δ' E i K l q v Φ :
+Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ???.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
@@ -106,13 +106,13 @@ Proof.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
+Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
   IntoVal e v' →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit LitUnit) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ?????.
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
@@ -120,12 +120,12 @@ Proof.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 Φ :
+Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ??????.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
@@ -133,13 +133,13 @@ Proof.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
 
-Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
+Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
   IntoVal e1 v1 → IntoVal e2 v2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
-  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
+  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
 Proof.
   rewrite /envs_entails=> ???????; subst.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
@@ -151,7 +151,7 @@ End heap.
 Tactic Notation "wp_apply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
-    | |- envs_entails _ (wp ?E ?e ?Q) =>
+    | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
       lazymatch iTypeOf H with
@@ -163,10 +163,10 @@ Tactic Notation "wp_apply" open_constr(lem) :=
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
+         eapply (tac_wp_alloc _ _ _ _ H K); [apply _|..])
       |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
     [apply _
     |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
@@ -182,9 +182,9 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
-      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
+      [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -196,10 +196,10 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
+         eapply (tac_wp_store _ _ _ _ _ _ K); [apply _|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -212,10 +212,10 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_wp_cas_fail _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
@@ -228,10 +228,10 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) =>
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
-         eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
+         eapply (tac_wp_cas_suc _ _ _ _ _ _ K); [apply _|apply _|..])
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in

theories/heap_lang/tactics.v

@@ -187,11 +187,12 @@ Definition is_atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma is_atomic_correct e : is_atomic e → Atomic (to_expr e).
+Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
 Proof.
+  enough (is_atomic e → Atomic maybe_stuck (to_expr e)).
+  { destruct s; auto using strongly_atomic_atomic. }
   intros He. apply ectx_language_atomic.
-  - intros σ e' σ' ef Hstep; simpl in *.
-    apply language.val_irreducible; revert Hstep.
+  - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
     destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
       inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
     unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
@@ -227,11 +228,11 @@ Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- Atomic ?e =>
-     let e' := W.of_expr e in change (Atomic (W.to_expr e'));
+  | |- Atomic ?s ?e =>
+     let e' := W.of_expr e in change (Atomic s (W.to_expr e'));
      apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (Atomic _ _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=

theories/program_logic/adequacy.v

@@ -34,23 +34,24 @@ Proof.
 Qed.
 
 (* Program logic adequacy *)
-Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
+Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
    rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
   adequate_safe t2 σ2 e2 :
+   s = not_stuck →
    rtc step ([e1], σ1) (t2, σ2) →
-   e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
+   e2 ∈ t2 → progressive e2 σ2
 }.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
-  adequate e1 σ1 φ →
+  adequate not_stuck e1 σ1 φ →
   rtc step ([e1], σ1) (t2, σ2) →
   Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
 Proof.
   intros Had ?.
   destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
   apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (adequate_safe e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
+  destruct (adequate_safe not_stuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
     rewrite ?eq_None_not_Some; auto.
   { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
@@ -64,13 +65,15 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation world σ := (wsat ∗ ownE ⊤ ∗ state_interp σ)%I.
+Notation world' E σ := (wsat ∗ ownE E ∗ state_interp σ)%I (only parsing).
+Notation world σ := (world' ⊤ σ) (only parsing).
 
-Notation wptp t := ([∗ list] ef ∈ t, WP ef {{ _, True }})%I.
+Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 
-Lemma wp_step e1 σ1 e2 σ2 efs Φ :
+Lemma wp_step s E e1 σ1 e2 σ2 efs Φ :
   prim_step e1 σ1 e2 σ2 efs →
-  world σ1 ∗ WP e1 {{ Φ }} ==∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp efs).
+  world' E σ1 ∗ WP e1 @ s; E {{ Φ }}
+  ==∗ ▷ |==> ◇ (world' E σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
 Proof.
   rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
   rewrite (val_stuck e1 σ1 e2 σ2 efs) // fupd_eq /fupd_def.
@@ -79,10 +82,10 @@ Proof.
   iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)"; auto.
 Qed.
 
-Lemma wptp_step e1 t1 t2 σ1 σ2 Φ :
+Lemma wptp_step s e1 t1 t2 σ1 σ2 Φ :
   step (e1 :: t1,σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
-  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2').
+  world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  ==∗ ∃ e2 t2', ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -93,11 +96,11 @@ Proof.
     iApply wp_step; eauto with iFrame.
 Qed.
 
-Lemma wptp_steps n e1 t1 t2 σ1 σ2 Φ :
+Lemma wptp_steps s n e1 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
+  world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
   Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 {{ Φ }} ∗ wptp t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   revert e1 t1 t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 t2 σ1 σ2 /=.
   { inversion_clear 1; iIntros "?"; eauto 10. }
@@ -119,9 +122,9 @@ Proof.
   by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
 Qed.
 
-Lemma wptp_result n e1 t1 v2 t2 σ1 σ2 φ :
+Lemma wptp_result s n e1 t1 v2 t2 σ1 σ2 φ :
   nsteps step n (e1 :: t1, σ1) (of_val v2 :: t2, σ2) →
-  world σ1 ∗ WP e1 {{ v, ⌜φ v⌝ }} ∗ wptp t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝.
+  world σ1 ∗ WP e1 @ s; ⊤ {{ v, ⌜φ v⌝ }} ∗ wptp s t1 ⊢ ▷^(S (S n)) ⌜φ v2⌝.
 Proof.
   intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2 t2' ?) "((Hw & HE & _) & H & _)"; simplify_eq.
@@ -129,18 +132,20 @@ Proof.
   iMod ("H" with "[Hw HE]") as ">(_ & _ & $)"; iFrame; auto.
 Qed.
 
-Lemma wp_safe e σ Φ :
-  world σ -∗ WP e {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+Lemma wp_safe E e σ Φ :
+  world' E σ -∗ WP e @ E {{ Φ }} ==∗ ▷ ⌜progressive e σ⌝.
 Proof.
   rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
-  destruct (to_val e) as [v|] eqn:?; [eauto 10|].
-  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; eauto 10 with iFrame.
+  destruct (to_val e) as [v|] eqn:?.
+  { iIntros "!> !> !%". left. by exists v. }
+  rewrite fupd_eq. iMod ("H" with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
+  iIntros "!> !> !%". by right.
 Qed.
 
 Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1 ⊢
-  ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
+  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp not_stuck t1
+  ⊢ ▷^(S (S n)) ⌜progressive e2 σ2⌝.
 Proof.
   intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
   iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
@@ -149,9 +154,9 @@ Proof.
   - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
-Lemma wptp_invariance n e1 e2 t1 t2 σ1 σ2 φ Φ :
+Lemma wptp_invariance s n e1 e2 t1 t2 σ1 σ2 φ Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) →
-  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 {{ Φ }} ∗ wptp t1
+  (state_interp σ2 ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ⊢ ▷^(S (S n)) ⌜φ⌝.
 Proof.
   intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
@@ -162,12 +167,12 @@ Proof.
 Qed.
 End adequacy.
 
-Theorem wp_adequacy Σ Λ `{invPreG Σ} e σ φ :
+Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ ∗ WP e {{ v, ⌜φ v⌝ }})%I) →
-  adequate e σ φ.
+       stateI σ ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }})%I) →
+  adequate s e σ φ.
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n ?]%rtc_nsteps.
@@ -176,7 +181,7 @@ Proof.
     rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
     iDestruct "Hwp" as (Istate) "[HI Hwp]".
     iApply (@wptp_result _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
-  - intros t2 σ2 e2 [n ?]%rtc_nsteps ?.
+  - destruct s; last done. intros t2 σ2 e2 _ [n ?]%rtc_nsteps ?.
     eapply (soundness (M:=iResUR Σ) _ (S (S n))).
     iMod wsat_alloc as (Hinv) "[Hw HE]".
     rewrite fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
@@ -184,11 +189,11 @@ Proof.
     iApply (@wptp_safe _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.
 
-Theorem wp_invariance Σ Λ `{invPreG Σ} e σ1 t2 σ2 φ :
+Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   (∀ `{Hinv : invG Σ},
      (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
        let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
-       stateI σ1 ∗ WP e {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
+       stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 ={⊤,∅}=∗ ⌜φ⌝))%I) →
   rtc step ([e], σ1) (t2, σ2) →
   φ.
 Proof.

theories/program_logic/ectx_language.v

@@ -4,7 +4,7 @@ From iris.algebra Require Export base.
 From iris.program_logic Require Import language.
 Set Default Proof Using "Type".
 
-(* We need to make thos arguments indices that we want canonical structure
+(* We need to make those arguments indices that we want canonical structure
    inference to use a keys. *)
 Class EctxLanguage (expr val ectx state : Type) := {
   of_val : val → expr;
@@ -61,6 +61,8 @@ Section ectx_language.
     ∃ e' σ' efs, head_step e σ e' σ' efs.
   Definition head_irreducible (e : expr) (σ : state) :=
     ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
+  Definition head_progressive (e : expr) (σ : state) :=
+    is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ.
 
   (* All non-value redexes are at the root.  In other words, all sub-redexes are
      values. *)
@@ -89,6 +91,11 @@ Section ectx_language.
     language.val_stuck := val_prim_stuck;
   |}.
 
+  Class HeadAtomic (s : stuckness) (e : expr) : Prop :=
+    head_atomic σ e' σ' efs :
+      head_step e σ e' σ' efs →
+      if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
+
   (* Some lemmas about this language *)
   Lemma head_prim_step e1 σ1 e2 σ2 efs :
     head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs.
@@ -117,10 +124,16 @@ Section ectx_language.
     rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
   Qed.
 
-  Lemma ectx_language_atomic e :
-    (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
-    sub_redexes_are_values e →
-    Atomic e.
+  Lemma progressive_head_progressive e σ :