fix compilation *oops*; make inv_alloc more flexible

barrier/client.v

@@ -76,9 +76,7 @@ Section ClosedProofs.
 
   Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc ⊤ (nroot .@ "Barrier")); last first.
-    { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
-      by move=>? _. }
+    apply ht_alt. rewrite (heap_alloc (nroot .@ "Barrier")); last done.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -(client_safe (nroot .@ "Barrier") (nroot .@ "Heap")) //.
     (* This, too, should be automated. *)

barrier/proof.v

@@ -2,8 +2,8 @@ From prelude Require Import functions.
 From algebra Require Import upred_big_op upred_tactics.
 From program_logic Require Import sts saved_prop.
 From heap_lang Require Export heap wp_tactics.
-From barrier Require Import protocol.
 From barrier Require Export barrier.
+From barrier Require Import protocol.
 Import uPred.
 
 (** The monoids we need. *)

heap_lang/heap.v

@@ -90,13 +90,13 @@ Section heap.
   Hint Resolve heap_store_valid.
 
   (** Allocation *)
-  Lemma heap_alloc E N σ :
+  Lemma heap_alloc N E σ :
     authG heap_lang Σ heapR → nclose N ⊆ E →
     ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} (λ l v, l ↦ v)).
   Proof.
     intros. rewrite -{1}(from_to_heap σ). etrans.
     { rewrite [ownP _]later_intro.
-      apply (auth_alloc (ownP ∘ of_heap) E N (to_heap σ)); last done.
+      apply (auth_alloc (ownP ∘ of_heap) N E (to_heap σ)); last done.
       apply to_heap_valid. }
     apply pvs_mono, exist_elim=> γ.
     rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.

heap_lang/tests.v

@@ -24,7 +24,7 @@ Section LiftingTests.
   Definition heap_e  : expr [] :=
     let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
   Lemma heap_e_spec E N :
-     nclose N ⊆ E → heap_ctx N ⊑ || heap_e @ E {{ λ v, v = #2 }}.
+     nclose N ⊆ E → heap_ctx N ⊑ #> heap_e @ E {{ λ v, v = #2 }}.
   Proof.
     rewrite /heap_e=>HN. rewrite -(wp_mask_weaken N E) //.
     wp eapply wp_alloc; eauto. apply forall_intro=>l; apply wand_intro_l.
@@ -44,7 +44,7 @@ Section LiftingTests.
 
   Lemma FindPred_spec n1 n2 E Φ :
     n1 < n2 → 
-    Φ #(n2 - 1) ⊑ || FindPred #n2 #n1 @ E {{ Φ }}.
+    Φ #(n2 - 1) ⊑ #> FindPred #n2 #n1 @ E {{ Φ }}.
   Proof.
     revert n1. wp_rec=>n1 Hn.
     wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
@@ -53,7 +53,7 @@ Section LiftingTests.
     - assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 
-  Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊑ || Pred #n @ E {{ Φ }}.
+  Lemma Pred_spec n E Φ : ▷ Φ #(n - 1) ⊑ #> Pred #n @ E {{ Φ }}.
   Proof.
     wp_lam. wp_op=> ?; wp_if.
     - wp_op. wp_op.
@@ -63,7 +63,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    (True : iProp) ⊑ || let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
+    (True : iProp) ⊑ #> let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
   Proof.
     intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
   Qed.
@@ -75,7 +75,7 @@ Section ClosedProofs.
 
   Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = #2 }}.
   Proof.
-    apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot.
+    apply ht_alt. rewrite (heap_alloc nroot ⊤); last by rewrite nclose_nroot.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
   Qed.

program_logic/auth.v

@@ -49,19 +49,19 @@ Section auth.
   Lemma auth_own_valid γ a : auth_own γ a ⊑ ✓ a.
   Proof. by rewrite /auth_own own_valid auth_validI. Qed.
 
-  Lemma auth_alloc E N a :
+  Lemma auth_alloc N E a :
     ✓ a → nclose N ⊆ E →
     ▷ φ a ⊑ (|={E}=> ∃ γ, auth_ctx γ N φ ∧ auth_own γ a).
   Proof.
     intros Ha HN. eapply sep_elim_True_r.
-    { by eapply (own_alloc (Auth (Excl a) a) N). }
-    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //. apply pvs_strip_pvs.
+    { by eapply (own_alloc (Auth (Excl a) a) E). }
+    rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     trans (▷ auth_inv γ φ ★ auth_own γ a)%I.
     { rewrite /auth_inv -(exist_intro a) later_sep.
       ecancel [▷ φ _]%I.
       by rewrite -later_intro -own_op auth_both_op. }
-    rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
+    rewrite (inv_alloc N E) // /auth_ctx pvs_frame_r. apply pvs_mono.
     by rewrite always_and_sep_l.
   Qed.
 

program_logic/invariants.v

@@ -68,7 +68,10 @@ Lemma wp_open_close E e N P Φ R :
   R ⊑ #> e @ E {{ Φ }}.
 Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
 
-Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P).
-Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
+Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ⊑ pvs E E (inv N P).
+Proof. 
+  intros. rewrite -(pvs_mask_weaken N) //.
+  by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
+Qed.
 
 End inv.

program_logic/sts.v

@@ -81,16 +81,15 @@ Section sts.
     ▷ φ s ⊑ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)).
   Proof.
     intros HN. eapply sep_elim_True_r.
-    { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) N).
+    { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) E).
       apply sts_auth_valid; set_solver. }
-    rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //.
-    apply pvs_strip_pvs.
+    rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     trans (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
     { rewrite /sts_inv -(exist_intro s) later_sep.
       ecancel [▷ φ _]%I.
       by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
-    rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
+    rewrite (inv_alloc N E) // /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
   Qed.