Seal off mapsto, invariants, and ghost ownership.

Fixes issue #20.

heap_lang/heap.v

@@ -24,8 +24,13 @@ Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd).
 Section definitions.
   Context `{i : heapG Σ}.
 
-  Definition heap_mapsto (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
+  Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ :=
     auth_own heap_name {[ l := (q, DecAgree v) ]}.
+  Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
+  Definition heap_mapsto := proj1_sig heap_mapsto_aux.
+  Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
+    proj2_sig heap_mapsto_aux.
+
   Definition heap_inv (h : heapUR) : iPropG heap_lang Σ :=
     ownP (of_heap h).
   Definition heap_ctx (N : namespace) : iPropG heap_lang Σ :=
@@ -107,7 +112,7 @@ Section heap.
       apply (auth_alloc (ownP ∘ of_heap) N E); auto using to_heap_valid. }
     apply pvs_mono, exist_elim=> γ.
     rewrite -(exist_intro (HeapG _ _ γ)) /heap_ctx; apply and_mono_r.
-    rewrite /heap_mapsto /heap_name.
+    rewrite heap_mapsto_eq /heap_mapsto_def /heap_name.
     induction σ as [|l v σ Hl IH] using map_ind.
     { rewrite big_sepM_empty; apply True_intro. }
     rewrite to_heap_insert big_sepM_insert //.
@@ -120,17 +125,19 @@ Section heap.
 
   (** General properties of mapsto *)
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
-  Proof. rewrite /heap_mapsto. apply _. Qed.
+  Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
   Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ★ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
-  Proof. by rewrite -auth_own_op op_singleton pair_op dec_agree_idemp. Qed.
+  Proof.
+    by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
+  Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
     l ↦{q1} v1 ★ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
   Proof.
     destruct (decide (v1 = v2)) as [->|].
     { by rewrite heap_mapsto_op_eq const_equiv // left_id. }
-    rewrite -auth_own_op op_singleton pair_op dec_agree_ne //.
+    rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
     apply (anti_symm (⊢)); last by apply const_elim_l.
     rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
     rewrite option_validI prod_validI frac_validI discrete_valid.
@@ -155,7 +162,7 @@ Section heap.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
     iFrame "Hheap". iSplit; first iPureIntro.
     { by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
-    iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
+    iIntros "Hheap". iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
   Qed.
 
   Lemma wp_load N E l q v Φ :
@@ -163,7 +170,8 @@ Section heap.
     heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)
     ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
-    iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iIntros {?} "[#Hh [Hl HΦ]]".
+    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
@@ -177,7 +185,8 @@ Section heap.
     heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))
     ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iIntros {??} "[#Hh [Hl HΦ]]".
+    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
@@ -192,7 +201,8 @@ Section heap.
     heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iIntros {????} "[#Hh [Hl HΦ]]".
+    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
@@ -206,7 +216,8 @@ Section heap.
     heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))
     ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iIntros {???} "[#Hh [Hl HΦ]]".
+    rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
     iApply (auth_fsa heap_inv (wp_fsa _)); simpl; eauto 10.
     iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.

program_logic/ghost_ownership.v

@@ -4,8 +4,11 @@ From iris.program_logic Require Export pviewshifts global_functor.
 From iris.program_logic Require Import ownership.
 Import uPred.
 
-Definition own `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
+Definition own_def `{inG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
   ownG (to_globalF γ a).
+Definition own_aux : { x | x = @own_def }. by eexists. Qed.
+Definition own {Λ Σ A i} := proj1_sig own_aux Λ Σ A i.
+Definition own_eq : @own = @own_def := proj2_sig own_aux.
 Instance: Params (@own) 5.
 Typeclasses Opaque own.
 
@@ -16,16 +19,16 @@ Implicit Types a : A.
 
 (** * Properties of own *)
 Global Instance own_ne γ n : Proper (dist n ==> dist n) (own γ).
-Proof. solve_proper. Qed.
+Proof. rewrite !own_eq. solve_proper. Qed.
 Global Instance own_proper γ : Proper ((≡) ==> (⊣⊢)) (own γ) := ne_proper _.
 
 Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
-Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
+Proof. by rewrite !own_eq /own_def -ownG_op to_globalF_op. Qed.
 Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (own γ).
 Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
 Proof.
-  rewrite /own ownG_valid /to_globalF.
+  rewrite !own_eq /own_def ownG_valid /to_globalF.
   rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
   rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
   (* implicit arguments differ a bit *)
@@ -36,9 +39,9 @@ Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ★ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
-Proof. rewrite /own; apply _. Qed.
+Proof. rewrite !own_eq /own_def; apply _. Qed.
 Global Instance own_core_persistent γ a : Persistent a → PersistentP (own γ a).
-Proof. rewrite /own; apply _. Qed.
+Proof. rewrite !own_eq /own_def; apply _. Qed.
 
 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
@@ -52,7 +55,7 @@ Proof.
       first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
       naive_solver.
   - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]].
-    by rewrite -(exist_intro γ) const_equiv // left_id.
+    by rewrite !own_eq /own_def -(exist_intro γ) const_equiv // left_id.
 Qed.
 Lemma own_alloc a E : ✓ a → True ={E}=> ∃ γ, own γ a.
 Proof.
@@ -60,10 +63,9 @@ Proof.
   apply pvs_mono, exist_mono=>?. eauto with I.
 Qed.
 
-Lemma own_updateP P γ a E :
-  a ~~>: P → own γ a ={E}=> ∃ a', ■ P a' ∧ own γ a'.
+Lemma own_updateP P γ a E : a ~~>: P → own γ a ={E}=> ∃ a', ■ P a' ∧ own γ a'.
 Proof.
-  intros Ha.
+  intros Ha. rewrite !own_eq.
   rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I).
   - eapply pvs_ownG_updateP, iprod_singleton_updateP;
       first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
@@ -85,7 +87,8 @@ Implicit Types a : A.
 
 Lemma own_empty γ E : True ={E}=> own γ ∅.
 Proof.
-  rewrite ownG_empty /own. apply pvs_ownG_update, iprod_singleton_update_empty.
+  rewrite ownG_empty !own_eq /own_def.
+  apply pvs_ownG_update, iprod_singleton_update_empty.
   apply (alloc_unit_singleton_update (cmra_transport inG_prf ∅)); last done.
   - apply cmra_transport_valid, ucmra_unit_valid.
   - intros x; destruct inG_prf. by rewrite left_id.

program_logic/invariants.v

@@ -4,8 +4,11 @@ From iris.proofmode Require Import pviewshifts.
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
-Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
+Definition inv_def {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
   (∃ i, ■ (i ∈ nclose N) ∧ ownI i P)%I.
+Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
+Definition inv {Λ Σ} := proj1_sig inv_aux Λ Σ.
+Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
 Instance: Params (@inv) 3.
 Typeclasses Opaque inv.
 
@@ -17,10 +20,12 @@ Implicit Types P Q R : iProp Λ Σ.
 Implicit Types Φ : val Λ → iProp Λ Σ.
 
 Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
-Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed.
+Proof.
+  rewrite inv_eq=> n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive.
+Qed.
 
 Global Instance inv_persistent N P : PersistentP (inv N P).
-Proof. rewrite /inv; apply _. Qed.
+Proof. rewrite inv_eq /inv; apply _. Qed.
 
 Lemma always_inv N P : □ inv N P ⊣⊢ inv N P.
 Proof. by rewrite always_always. Qed.
@@ -28,7 +33,7 @@ Proof. by rewrite always_always. Qed.
 Lemma inv_alloc N E P : nclose N ⊆ E → ▷ P ={E}=> inv N P.
 Proof.
   intros. rewrite -(pvs_mask_weaken N) //.
-  by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
+  by rewrite inv_eq /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
 Qed.
 
 (** Fairly explicit form of opening invariants *)
@@ -37,7 +42,7 @@ Lemma inv_open E N P :
   inv N P ⊢ ∃ E', ■ (E ∖ nclose N ⊆ E' ⊆ E) ★
                     |={E,E'}=> ▷ P ★ (▷ P ={E',E}=★ True).
 Proof.
-  rewrite /inv. iDestruct 1 as {i} "[% #Hi]".
+  rewrite inv_eq /inv. iDestruct 1 as {i} "[% #Hi]".
   iExists (E ∖ {[ i ]}). iSplit. { iPureIntro. set_solver. }
   iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|].
   iPvsIntro. iSplitL "HP"; first done. iIntros "HP".
@@ -57,8 +62,7 @@ Proof.
   iPvs "Hvs" as "[HP Hvs]"; first set_solver.
   (* TODO: How do I do sth. like [iSpecialize "HΨ HP"]? *)
   iPvsIntro. iApply (fsa_mask_weaken _ (E ∖ N)); first set_solver.
-  iApply fsa_wand_r. iSplitR "Hvs"; first by iApply "HΨ".
-  simpl. iIntros {v} "[HP HΨ]". iPvs ("Hvs" with "HP"); first set_solver.
-  done.
+  iApply fsa_wand_r. iSplitR "Hvs"; first by iApply "HΨ"; simpl.
+  iIntros {v} "[HP HΨ]". by iPvs ("Hvs" with "HP"); first set_solver.
 Qed.
 End inv.

tests/heap_lang.v

@@ -30,6 +30,18 @@ Section LiftingTests.
     wp_alloc l. wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
   Qed.
 
+  Definition heap_e2  : expr [] :=
+    let: "x" := ref #1 in
+    let: "y" := ref #1 in
+    '"x" <- !'"x" + #1 ;; !'"x".
+  Lemma heap_e2_spec E N :
+     nclose N ⊆ E → heap_ctx N ⊢ WP heap_e2 @ E {{ v, v = #2 }}.
+  Proof.
+    iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
+    wp_alloc l. wp_let. wp_alloc l'. wp_let.
+    wp_load. wp_op. wp_store. wp_seq. wp_load. done.
+  Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := '"y" + #1 in