Update to the latest Iris

README.md

@@ -5,8 +5,8 @@ This version is known to compile with:
  - Coq 8.6.1
  - Ssreflect 1.6
  - Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- - std++ version [ca0be4274dd7593c44db46670d078095e9f6c1c7](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/ca0be4274dd7593c44db46670d078095e9f6c1c7)
- - Iris version [bfdd67a736ad91c3838bffde3f57af516dec56d8](https://gitlab.mpi-sws.org/FP/iris-coq/tree/bfdd67a736ad91c3838bffde3f57af516dec56d8)
+ - std++ version [5912d750ffe247b5a41f27cb42b98f23c571897d](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/5912d750ffe247b5a41f27cb42b98f23c571897d)
+ - Iris version [6c7b99c2dd261fb7e67a339da89bdb12a3189678](https://gitlab.mpi-sws.org/FP/iris-coq/tree/6c7b99c2dd261fb7e67a339da89bdb12a3189678)
 
 # Compilation
 

theories/F_mu_ref_conc/lang.v

@@ -120,8 +120,8 @@ Module lang.
 
   Fixpoint of_val (v : val) : expr :=
     match v with
-    | RecV f x e _ => Rec f x e
-    | TLamV e _ => TLam e
+    | RecV f x e => Rec f x e
+    | TLamV e => TLam e
     | LitV l => Lit l
     | PairV v1 v2 => Pair (of_val v1) (of_val v2)
     | InjLV v => InjL (of_val v)
@@ -460,20 +460,19 @@ Module lang.
     let l := fresh (dom (gset loc) σ) in
     to_val e = Some v → head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) [].
   Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
-End lang.
 
-(** Language instance for Iris *)
-Program Instance heap_ectxi_lang :
-  EctxiLanguage
-    (lang.expr) lang.val lang.ectx_item lang.state := {|
-  of_val := lang.of_val; to_val := lang.to_val;
-  fill_item := lang.fill_item; head_step := lang.head_step
-|}.
-Solve Obligations with eauto using lang.to_of_val, lang.of_to_val,
-  lang.val_stuck, lang.fill_item_val, lang.fill_item_no_val_inj,
-  lang.head_ctx_step_val.
+  Lemma F_mu_ref_conc_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+  Proof.
+    split; apply _ || eauto using to_of_val, of_to_val, val_stuck,
+           fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+  Qed.
+
+End lang.
 
-Canonical Structure lang := ectx_lang (lang.expr).
+(** Language *)
+Canonical Structure F_mu_ref_conc_ectxi_lang := EctxiLanguage lang.F_mu_ref_conc_mixin.
+Canonical Structure F_mu_ref_conc_ectx_lang := EctxLanguageOfEctxi F_mu_ref_conc_ectxi_lang.
+Canonical Structure F_mu_ref_conc_lang := LanguageOfEctx F_mu_ref_conc_ectx_lang.
 
 Export lang.
 
@@ -485,11 +484,11 @@ Local Hint Resolve language.val_irreducible.
 Local Hint Resolve to_of_val.
 Local Hint Unfold language.irreducible.
 
-Lemma is_atomic_correct e : is_atomic e → language.atomic e.
+Lemma is_atomic_correct e : is_atomic e → Atomic e.
 Proof.
   intros ?; apply ectx_language_atomic.
   - destruct 1; simpl; eauto.
-  - apply ectxi_language_sub_values=> /= Ki e' Hfill.
+  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
     destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
                    naive_solver eauto using to_val_is_Some.
 Qed.
@@ -498,8 +497,7 @@ Ltac solve_atomic :=
   apply is_atomic_correct; simpl; repeat split;
     rewrite ?to_of_val; eapply mk_is_Some; fast_done.
 
-Hint Extern 0 (language.atomic _) => solve_atomic.
-Hint Extern 0 (language.atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
 
 (* Some other useful tactics *)
 Ltac inv_head_step :=

theories/F_mu_ref_conc/pureexec.v

@@ -3,25 +3,24 @@ From iris_logrel.F_mu_ref_conc Require Export lang subst notation.
 
 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_pureexec :=
+Local Ltac solve_pure_exec :=
   repeat lazymatch goal with
   | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
   end;
-  apply hoist_pred_pureexec; intros; destruct_and?;
-  apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
+  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
 Local Hint Resolve to_of_val.
 
 Instance pure_binop op e1 v1 e2 v2 v `{!IntoVal e1 v1} `{!IntoVal e2 v2} :
   PureExec (binop_eval op v1 v2 = Some v)
            (BinOp op e1 e2)
            (of_val v).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_rec f x e1 e2 v2 `{Closed ∅ (Rec f x e1)} `{!IntoVal e2 v2} :
   PureExec True
            (App (Rec f x e1) e2)
            (subst' f (Rec f x e1) (subst' x e2 e1)).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 (* TODO: give this one a correct priority? *)
 Instance pure_rec_locked e f x e1 e2 v2 `{!IntoVal e2 v2} `(e = Rec f x e1) `{Closed (x :b: f :b: ∅) e1} :
@@ -29,8 +28,7 @@ Instance pure_rec_locked e f x e1 e2 v2 `{!IntoVal e2 v2} `(e = Rec f x e1) `{Cl
            (App e e2)
            (e $/ v2) | 100.
 Proof.
-  apply hoist_pred_pureexec; intros; destruct_and?;
-  apply det_head_step_pureexec.
+  apply det_head_step_pure_exec.
   - solve_exec_safe.
   - rewrite -(of_to_val e2 _ into_val).
     destruct f; solve_exec_puredet.
@@ -38,38 +36,38 @@ Qed.
 
 Instance pure_fst e1 v1 e2 v2 `{!IntoVal e1 v1} `{!IntoVal e2 v2} :
   PureExec True (Fst (Pair e1 e2)) e1.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_snd e1 v1 e2 v2 `{!IntoVal e1 v1} `{!IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_unfold e1 v1 `{!IntoVal e1 v1} :
   PureExec True (Unfold (Fold e1)) e1.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_unpack e1 e2 v1 `{!IntoVal e1 v1} :
   PureExec True (Unpack (Pack e1) e2) (e2 e1).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_if_true e1 e2 :
   PureExec True (If #true e1 e2) e1.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_if_false e1 e2 :
   PureExec True (If #false e1 e2) e2.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_case_inl e0 v `{!IntoVal e0 v} e1 e2  :
   PureExec True (Case (InjL e0) e1 e2) (e1 e0).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_case_inr e0 v `{!IntoVal e0 v} e1 e2  :
   PureExec True (Case (InjR e0) e1 e2) (e2 e0).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Instance pure_tlam e `{Closed ∅ e} :
   PureExec True
            (TApp (TLam e))
            e.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.

theories/F_mu_ref_conc/reflection.v

@@ -43,7 +43,7 @@ Inductive expr :=
 Fixpoint to_expr (e : expr) : lang.expr :=
   match e with
   | Val v e _ => e
-  | ClosedExpr e _ => e
+  | ClosedExpr e => e
   | Var x => lang.Var x
   | Rec f x e => lang.Rec f x (to_expr e)
   | App e1 e2 => lang.App (to_expr e1) (to_expr e2)
@@ -119,7 +119,7 @@ Ltac of_expr e :=
 Fixpoint is_closed (X : stringset) (e : expr) : bool :=
   match e with
   | Val _ _ _ => true
-  | ClosedExpr e _ => true
+  | ClosedExpr e => true
   | Var x => bool_decide (x ∈ X)
   | Lit l => true
   | Rec f x e => is_closed (x :b: f :b: X) e
@@ -135,7 +135,7 @@ Fixpoint is_closed (X : stringset) (e : expr) : bool :=
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
   | Val _ _ _ => e
-  | ClosedExpr _ _ => e
+  | ClosedExpr _ => e
   | Var y => if decide (x = y) then es else Var y
   | Rec f y e =>
     Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e

theories/F_mu_ref_conc/rules.v

@@ -14,7 +14,7 @@ Class heapG Σ := HeapG {
   heapG_gen_heapG :> gen_heapG loc val Σ;
 }.
 
-Instance heapG_irisG `{heapG Σ} : irisG lang Σ := {
+Instance heapG_irisG `{heapG Σ} : irisG F_mu_ref_conc_lang Σ := {
   iris_invG := heapG_invG;
   state_interp := gen_heap_ctx
 }.
@@ -27,7 +27,7 @@ Notation "l ↦ᵢ v" := (mapsto (L:=loc) (V:=val) l 1 v) (at level 20) : uPred_
 Section mapsto.
   Context `{heapG Σ}.
 
-  Global Instance mapsto_timeless l q v : TimelessP (l ↦ᵢ{q} v).
+  Global Instance mapsto_timeless l q v : Timeless (l ↦ᵢ{q} v).
   Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦ᵢ{q} v)%I.
   Proof.
@@ -158,6 +158,6 @@ Section lang_rules.
 
   Lemma wp_bind {E e} K Φ :
     WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}.
-  Proof. exact: wp_ectx_bind. Qed.
+  Proof. exact: wp_bind. Qed.
 
 End lang_rules.

theories/F_mu_ref_conc/subst.v

@@ -537,7 +537,7 @@ Proof.
     edestruct (step_by_val K (subst_ctx es K') e1' (subst_p es e1''))
       as [K1 ?]; eauto using val_stuck.
     edestruct (step_by_val (subst_ctx es K') K (subst_p es e1'') e1')
-      as [[|??] ->]; eauto using val_stuck; discriminate_list. }
+      as [[|??] ->]; eauto using val_stuck; simpl in *; discriminate_list. }
   apply fill_inj in H; subst.
   rewrite fill_subst.
   cut (σ1 = σ2 ∧ subst_p es e2'' = e2' ∧ [] = efs).

theories/F_mu_ref_conc/tactics.v

@@ -72,25 +72,35 @@ Ltac reshape_expr e tac :=
   end in go (@nil ectx_item) e.
 
 (** wp-specific helper tactics *)
+(* TODO: duplication? *)
+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 {{ Φ }}).
+Proof. rewrite /envs_entails => ->. by apply: wp_bind. Qed.
+Lemma tac_wp_bind'' `{heapG Σ} K Δ E E1 E2 Φ e :
+  envs_entails Δ (|={E1,E2}=> WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+  envs_entails Δ (|={E1,E2}=> WP fill K e @ E {{ Φ }}).
+Proof. rewrite /envs_entails => ->. by apply fupd_mono, wp_bind. Qed.
+
 Ltac wp_bind_core K := 
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
+  | _ => apply (tac_wp_bind K); simpl
   end.
 
-Ltac wp_bind_core'' K E1 E2 := 
+Ltac wp_bind_core'' K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etrans; [|fast_by apply (fupd_mono E1 E2 _ _ (wp_bind K _))]; simpl
+  | _ => apply (tac_wp_bind'' K)
   end.
 
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc; wp_bind_core K) 
-  | |- _ ⊢ |={?E1,?E2}=> wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    unify e' efoc; wp_bind_core'' K E1 E2) 
+  | |- envs_entails _ (|={?E1,?E2}=> wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
+    unify e' efoc; wp_bind_core'' K)
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
@@ -100,28 +110,25 @@ Lemma tac_wp_pure `{heapG Σ} K φ e1 e2 ℶ1 ℶ2 E Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 ℶ1 ℶ2 →
-  (ℶ2 ⊢ WP fill K e2 @ E {{ Φ }}) →
-  (ℶ1 ⊢ WP fill K e1 @ E {{ Φ }}).
+  envs_entails ℶ2 (WP fill K e2 @ E {{ Φ }}) →
+  envs_entails ℶ1 (WP fill K e1 @ E {{ Φ }}).
 Proof.
-  intros ?? Hφ Hgoal.
+  rewrite /envs_entails=> ??? Hℶ2.
   rewrite into_laterN_env_sound /=.
-  rewrite Hgoal.
-  iIntros "HWP".
-  wp_bind_core K.
-  iApply wp_pure_step_later; eauto.
-  iApply (wp_bind_inv with "HWP").
-  { (* TODO: how to get rid of this? *)
-    change lang with (ectx_lang expr).
-    change fill with (ectx_language.fill).
-    eapply ectx_lang_ctx. }
+  rewrite Hℶ2 -wp_pure_step_later //.
 Qed.
 
-Ltac wp_value := etrans; [|eapply wp_value; apply _]; simpl.
+Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+
+Ltac wp_value := eapply tac_wp_value; [apply _|lazy beta].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [apply _ (* PureExec *)
@@ -164,8 +171,8 @@ Lemma tac_wp_alloc Δ Δ' E j e v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ᵢ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ Φ (LitV (Loc l)))) →
-  Δ ⊢ WP Alloc e @ E {{ Φ }}.
+    (envs_entails Δ'' (Φ (LitV (Loc l))))) →
+  envs_entails Δ (WP Alloc e @ E {{ Φ }}).
 Proof.
   intros ?? HΔ. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
@@ -176,8 +183,8 @@ Qed.
 Lemma tac_wp_load Δ Δ' E i l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ᵢ{q} v)%I →
-  (Δ' ⊢ Φ v) →
-  Δ ⊢ WP Load (Lit (Loc l)) @ E {{ Φ }}.
+  envs_entails Δ' (Φ v) →
+  envs_entails Δ (WP Load (Lit (Loc l)) @ E {{ Φ }}).
 Proof.
   intros. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
@@ -189,8 +196,8 @@ Lemma tac_wp_store Δ Δ' Δ'' E i l v e v' Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ᵢ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ᵢ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ Φ (LitV Unit)) →
-  Δ ⊢ WP Store (Lit (Loc l)) e @ E {{ Φ }}.
+  envs_entails Δ'' (Φ (LitV Unit)) →
+  envs_entails Δ (WP Store (Lit (Loc l)) e @ E {{ Φ }}).
 Proof.
   intros. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -201,8 +208,8 @@ Lemma tac_wp_cas_fail Δ Δ' E i l q v e1 v1 e2 v2 Φ :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ᵢ{q} v)%I → v ≠ v1 →
-  (Δ' ⊢ Φ (LitV (Bool false))) →
-  Δ ⊢ WP CAS (Lit (Loc l)) e1 e2 @ E {{ Φ }}.
+  envs_entails Δ' (Φ (LitV (Bool false))) →
+  envs_entails Δ (WP CAS (Lit (Loc l)) e1 e2 @ E {{ Φ }}).
 Proof.
   intros. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
@@ -214,8 +221,8 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i l v e1 v1 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 Δ'' →
-  (Δ'' ⊢ Φ (LitV (Bool true))) →
-  Δ ⊢ WP CAS (Lit (Loc l)) e1 e2 @ E {{ Φ }}.
+  envs_entails Δ'' (Φ (LitV (Bool true))) →
+  envs_entails Δ (WP CAS (Lit (Loc l)) e1 e2 @ E {{ Φ }}).
 Proof.
   intros; subst. eapply wand_apply; first exact: wp_cas_suc.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -226,7 +233,7 @@ End heap.
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          match eval hnf in e' with Alloc _ => wp_bind_core K end)
@@ -248,7 +255,7 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          match eval hnf in e' with Load _ => wp_bind_core K end)
@@ -264,7 +271,7 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          match eval hnf in e' with Store _ _ => wp_bind_core K end)
@@ -283,7 +290,7 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)
@@ -304,7 +311,7 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          match eval hnf in e' with CAS _ _ _ => wp_bind_core K end)

theories/examples/bit.v

@@ -57,7 +57,7 @@ Section bit_refinement.
     (∃ b : bool, ⌜vv.1 = #b⌝ ∗ ⌜vv.2 = #(bitf b)⌝)%I.
   Next Obligation. solve_proper. Qed.
 
-  Instance bitτi_persistent ww : PersistentP (bitτi ww).
+  Instance bitτi_persistent ww : Persistent (bitτi ww).
   Proof. apply _. Qed.
 
   Lemma bit_prerefinement Γ E1 :

theories/examples/generative.v

@@ -52,7 +52,7 @@ Section namegen_refinement.
    ∗ inBij γ l n)%I.
   Next Obligation. solve_proper. Qed.
 
-  Instance ngR_persistent γ ww : PersistentP (ngR γ ww).
+  Instance ngR_persistent γ ww : Persistent (ngR γ ww).
   Proof. apply _. Qed.
 
   Definition ng_Inv (γ : gname) (c : loc) : iProp Σ :=
@@ -91,13 +91,13 @@ Section namegen_refinement.
       iIntros "Hc".
       rel_seq_r.
       rel_load_r.
-      iAssert (⌜¬(∃ y, (l', y) ∈ L)⌝)%I with "[HL Hl']" as %Hl'.
+      iAssert (⌜(∃ y, (l', y) ∈ L) → False⌝)%I with "[HL Hl']" as %Hl'.
       { iIntros (Hy). destruct Hy as [y Hy].
         rewrite (big_sepS_elem_of _ L (l',y) Hy).
         iDestruct "HL" as "[Hl _]".
         iDestruct (mapsto_valid_2 with "Hl Hl'") as %Hfoo.
         compute in Hfoo. eauto. }
-      iAssert (⌜¬(∃ x, (x, S n) ∈ L)⌝)%I with "[HL]" as %Hc.
+      iAssert (⌜(∃ x, (x, S n) ∈ L) → False⌝)%I with "[HL]" as %Hc.
       { iIntros (Hx). destruct Hx as [x Hy].
         rewrite (big_sepS_elem_of _ L (x,S n) Hy).
         iDestruct "HL" as "[_ %]". omega. }
@@ -126,7 +126,6 @@ Section namegen_refinement.
       (* we would like to have an atomic version of `rel_op_l`? *)
       rel_bind_l (#l = #l')%E.
       iApply bin_log_related_wp_atomic_l.
-      { solve_atomic. }
       iInv N as (m L) "(>HB & >Hc & HL)" "Hcl".
       iModIntro. wp_op.
       rel_op_r.
@@ -214,7 +213,7 @@ Section cell_refinement.
      ∗ cellInt R r1 r2 r3 l r)%I.
   Next Obligation. solve_proper. Qed.
 
-  Instance cellR_persistent R ww : PersistentP (cellR R ww).
+  Instance cellR_persistent R ww : Persistent (cellR R ww).
   Proof. apply _. Qed.
 
   Lemma cell2_cell1_refinement Γ :

theories/examples/lock.v

@@ -64,9 +64,9 @@ Section lockG_rules.
   Global Instance is_lock_ne l : NonExpansive (is_lock γ l).
   Proof. solve_proper. Qed.
 
-  Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
+  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
   Proof. apply _. Qed.
-  Global Instance locked_timeless γ : TimelessP (locked γ).
+  Global Instance locked_timeless γ : Timeless (locked γ).
   Proof. apply _. Qed.
 
   Lemma bin_log_related_newlock_l (R : iProp Σ) Δ Γ E K t τ :

theories/examples/stack/helping.v

@@ -192,7 +192,7 @@ Section refinement.
 
   Definition stackRel (v1 v2 : val) : iProp Σ :=
     ⟦ LIST TNat ⟧ [] (v1, v2).
-  Instance stackRel_persistent v1 v2 : PersistentP (stackRel v1 v2).
+  Instance stackRel_persistent v1 v2 : Persistent (stackRel v1 v2).
   Proof. apply _. Qed.
   Lemma stackRel_empty : stackRel (FoldV (InjLV #())) (FoldV (InjLV #())).
   Proof.

theories/examples/stack/module_refinement.v

@@ -14,7 +14,7 @@ Section Mod_refinement.
       ∗ inv (stackN .@ (stk,stk')) (sinv' γ τi stk stk' l))%I.
   Solve Obligations with solve_proper.
 
-  Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : PersistentP (sint τi vv).
+  Instance sint_persistent `{logrelG Σ, stackPreG Σ} τi vv : Persistent (sint τi vv).
   Proof. apply _. Qed.
   
   Lemma module_refinement `{SPG : stackPreG Σ} Δ Γ :
@@ -39,7 +39,7 @@ Section Mod_refinement.
       rel_alloc_r as stk' "Hstk'".
       rel_alloc_r as l "Hl".
       rel_vals.
-      rewrite -persistentP.
+      rewrite -persistent.
       iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done.
       pose (SG := StackG Σ _ γ).
       iAssert (prestack_owns γ ∅) with "[Hemp]" as "Hoe".

theories/examples/stack/refinement.v

@@ -33,8 +33,8 @@ Section Stack_refinement.
     iMod (Hcl with asn) as "_";
     [iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.
 
-  Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l {τP : ∀ ww, PersistentP (τi ww)} Γ :
-    N ⊥ logrelN →
+  Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l {τP : ∀ ww, Persistent (τi ww)} Γ :
+    N ## logrelN →
     inv N (sinv τi st st' l) -∗ τi (v,v') -∗
     Γ ⊨ (FG_push $/ (LitV (Loc st))) v ≤log≤ (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
   Proof.
@@ -82,8 +82,8 @@ Section Stack_refinement.
       by iApply "IH".
   Qed.
 
-  Lemma FG_CG_pop_refinement' N st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ :
-    N ⊥ logrelN →
+  Lemma FG_CG_pop_refinement' N st st' (τi : D) l {τP : ∀ ww, Persistent (τi ww)} Δ Γ :
+    N ## logrelN →
     inv N (sinv τi st st' l) -∗
     {⊤,⊤;τi::Δ;Γ} ⊨ (FG_pop $/ LitV (Loc st)) #() ≤log≤ (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
   Proof.
@@ -181,7 +181,7 @@ replace ((rec: "pop" "st" <> :=
         iApply "IH".
   Qed.
 
-  Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, PersistentP (τi ww)} Δ Γ :
+  Lemma FG_CG_pop_refinement st st' (τi : D) l {τP : ∀ ww, Persistent (τi ww)} Δ Γ :
     inv stackN (sinv τi st st' l) -∗
     {⊤,⊤;τi::Δ;Γ} ⊨ FG_pop $/ LitV (Loc st) ≤log≤ CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)).
   Proof.
@@ -196,7 +196,7 @@ replace ((rec: "pop" "st" <> :=
     { solve_ndisj. }
   Qed.
 
-  Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, PersistentP (τi ww)} Γ:
+  Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP : ∀ ww, Persistent (τi ww)} Γ:
     inv stackN (sinv τi st st' l) -∗
     {⊤,⊤;τi::Δ;Γ} ⊨ FG_read_iter $/ LitV (Loc st) ≤log≤ CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit.
   Proof.
@@ -303,12 +303,12 @@ End Stack_refinement.
 Section Full_refinement.
   Local Ltac replace_l c :=
     lazymatch goal with
-    | [|- _ ⊢ bin_log_related _ _ _ _ ?e _ _ ] =>
+    | [|- envs_entails _ (bin_log_related _ _ _ _ ?e _ _) ] =>
       replace e with c; last first
     end.
   Local Ltac replace_r c :=
     lazymatch goal with
-    | [|- _ ⊢ bin_log_related _ _ _ _ _ ?e' _ ] =>
+    | [|- envs_entails _ (bin_log_related _ _ _ _ _ ?e' _) ] =>
       replace e' with c; last first
     end.
 

theories/examples/stack/stack_rules.v

@@ -28,7 +28,7 @@ Section Rules_pre.
   Notation D := (prodC valC valC -n> iProp Σ).
   Notation "l ↦ˢᵗᵏ v" := (prestack_mapsto γ l v) (at level 20) : uPred_scope.
 
-  Global Instance stack_mapsto_persistent l v : PersistentP (l ↦ˢᵗᵏ v).
+  Global Instance stack_mapsto_persistent l v : Persistent (l ↦ˢᵗᵏ v).
   Proof. apply _. Qed.
   
   Lemma prestack_mapstos_agree_uncurried l v w : l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ⊢ ⌜v = w⌝.
@@ -74,17 +74,17 @@ Section Rules_pre.
 
   Global Opaque preStackLink. (* So that we can only use the unfold above. *)
 
-  Global Instance preStackLink_persistent (Q : D) v `{∀ vw, PersistentP (Q vw)} :
-    PersistentP (preStackLink Q v).
+  Global Instance preStackLink_persistent (Q : D) v `{∀ vw, Persistent (Q vw)} :
+    Persistent (preStackLink Q v).
   Proof.
-    rewrite /PersistentP.
+    rewrite /Persistent.
     iIntros "H". iLöb as "IH" forall (v). rewrite preStackLink_unfold.
     iDestruct "H" as (l w) "[% [#Hl [[% %]|Hr]]]"; subst.
     { iExists l, _; iAlways; eauto. }
     iDestruct "Hr" as (y1 z1 y2 z2) "[% [% [#HQ Hrec]]]"; subst.    
     rewrite later_forall. 
     iSpecialize ("IH" $! (z1, z2)). rewrite later_wand. 
-    iSpecialize ("IH" with "Hrec"). rewrite -always_later.
+    iSpecialize ("IH" with "Hrec"). rewrite -persistently_later.
     iDestruct "IH" as "#IH".
     iAlways. iExists _,_; eauto 20.
   Qed.
@@ -169,8 +169,8 @@ Section Rules.
                       ∗ Q (y1, y2) ∗ ▷ StackLink Q (z1, z2))))%I.
   Proof. by rewrite /StackLink preStackLink_unfold. Qed.