Merge branch 'robbert/heaplang_pointsto_seal' into 'master'

Seal heap_lang `pointsto`.

Closes #549

See merge request iris/iris!1067

CHANGELOG.md

@@ -31,6 +31,7 @@ lemma.
 **Changes in `heap_lang`:**
 
 * Make `wp_cmpxchg_fail` work when the points-to is in the persistent context.
+* Seal definition of `pointsto`, add copies of all relevant lemmas.
 
 **Infrastructure:**
 

iris_heap_lang/primitive_laws.v

@@ -77,9 +77,20 @@ Next Obligation.
   by iMod (steps_auth_update_S with "H") as "$".
 Qed.
 
-(** Since we use an [option val] instance of [gen_heap], we need to overwrite
-the notations.  That also helps for scopes and coercions. *)
-Notation "l ↦ dq v" := (pointsto (L:=loc) (V:=option val) l dq (Some v%V))
+(** Since we use an [option val] instance of [gen_heap], we need to add a
+[Some]. We also seal the definition to avoid confusion between the version from
+[gen_heap], and our version with [Some]. That also helps for scopes and
+coercions. *)
+Local Definition pointsto_def `{heapGS_gen hlc Σ}
+    (l : loc) (dq : dfrac) (v : val) : iProp Σ :=
+  pointsto l dq (Some v).
+Local Definition pointsto_aux : seal (@pointsto_def). Proof. by eexists. Qed.
+Definition pointsto := pointsto_aux.(unseal).
+Local Definition pointsto_unseal :
+  @pointsto = @pointsto_def := pointsto_aux.(seal_eq).
+Global Arguments pointsto {hlc Σ _}.
+
+Notation "l ↦ dq v" := (pointsto l dq v)
   (at level 20, dq custom dfrac at level 1, format "l  ↦ dq  v") : bi_scope.
 
 (** Same for [gen_inv_heap], except that these are higher-order notations so to
@@ -228,41 +239,63 @@ Qed.
 (** Heap *)
 
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
-value type being [option val]. *)
-
-Lemma pointsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
-Proof. apply pointsto_valid. Qed.
-Lemma pointsto_valid_2 l dq1 dq2 v1 v2 :
-  l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
-Proof. iIntros "H1 H2". iCombine "H1 H2" gives %[? [= ?]]. done. Qed.
-Lemma pointsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
-Proof. iIntros "H1 H2". iCombine "H1 H2" gives %[_ [= ?]]. done. Qed.
+value type being [option val] (and sealing). *)
+
+Global Instance pointsto_timeless l dq v : Timeless (l ↦{dq} v).
+Proof. rewrite pointsto_unseal. apply _. Qed.
+Global Instance pointsto_fractional l v : Fractional (λ q, l ↦{#q} v)%I.
+Proof. rewrite pointsto_unseal. apply _. Qed.
+Global Instance pointsto_as_fractional l q v :
+  AsFractional (l ↦{#q} v) (λ q, l ↦{#q} v)%I q.
+Proof. rewrite pointsto_unseal. apply _. Qed.
+Global Instance pointsto_persistent l v : Persistent (l ↦□ v).
+Proof. rewrite pointsto_unseal. apply _. Qed.
 
 Global Instance pointsto_combine_sep_gives l dq1 dq2 v1 v2 : 
-  CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝ | 20. 
-  (* We provide an instance with lower cost than the gen_heap instance
-     to avoid having to deal with Some v1 = Some v2 *)
+  CombineSepGives (l ↦{dq1} v1) (l ↦{dq2} v2) ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
 Proof.
-  rewrite /CombineSepGives. iIntros "[H1 H2]".
+  rewrite pointsto_unseal /CombineSepGives. iIntros "[H1 H2]".
   iCombine "H1 H2" gives %[? [=->]]. eauto.
 Qed.
 
 Lemma pointsto_combine l dq1 dq2 v1 v2 :
   l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
 Proof.
-  iIntros "Hl1 Hl2". by iCombine "Hl1 Hl2" as "$" gives %[_ ->].
+  rewrite pointsto_unseal.
+  iIntros "Hl1 Hl2". by iCombine "Hl1 Hl2" as "$" gives %[_ [= ->]].
 Qed.
 
+Global Instance pointsto_combine_as l dq1 dq2 v1 v2 :
+  CombineSepAs (l ↦{dq1} v1) (l ↦{dq2} v2) (l ↦{dq1 ⋅ dq2} v1) | 60.
+  (* higher cost than the Fractional instance, which kicks in for #qs *)
+Proof.
+  rewrite /CombineSepAs. iIntros "[H1 H2]".
+  iDestruct (pointsto_combine with "H1 H2") as "[$ _]".
+Qed.
+
+Lemma pointsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝.
+Proof. rewrite pointsto_unseal. apply pointsto_valid. Qed.
+Lemma pointsto_valid_2 l dq1 dq2 v1 v2 :
+  l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
+Proof. iIntros "H1 H2". iCombine "H1 H2" gives %[? [= ?]]. done. Qed.
+Lemma pointsto_agree l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜v1 = v2⌝.
+Proof. iIntros "H1 H2". iCombine "H1 H2" gives %[_ [= ?]]. done. Qed.
+
 Lemma pointsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
   ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
-Proof. apply pointsto_frac_ne. Qed.
+Proof. rewrite pointsto_unseal. apply pointsto_frac_ne. Qed.
 Lemma pointsto_ne l1 l2 dq2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
-Proof. apply pointsto_ne. Qed.
+Proof. rewrite pointsto_unseal. apply pointsto_ne. Qed.
 
 Lemma pointsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
-Proof. apply pointsto_persist. Qed.
+Proof. rewrite pointsto_unseal. apply pointsto_persist. Qed.
 Lemma pointsto_unpersist l v : l ↦□ v ==∗ ∃ q, l ↦{#q} v.
-Proof. apply pointsto_unpersist. Qed.
+Proof. rewrite pointsto_unseal. apply pointsto_unpersist. Qed.
+
+Global Instance frame_pointsto p l v q1 q2 q :
+  FrameFractionalQp q1 q2 q →
+  Frame p (l ↦{#q1} v) (l ↦{#q2} v) (l ↦{#q} v) | 5.
+Proof. apply: frame_fractional. Qed.
 
 Global Instance inv_pointsto_own_proper l v :
   Proper (pointwise_relation _ iff ==> (≡)) (inv_pointsto_own l v).
@@ -281,7 +314,10 @@ Lemma make_inv_pointsto l v (I : val → Prop) E :
   ↑inv_heapN ⊆ E →
   I v →
   inv_heap_inv -∗ l ↦ v ={E}=∗ l ↦_I v.
-Proof. iIntros (??) "#HI Hl". iApply make_inv_pointsto; done. Qed.
+Proof.
+  iIntros (??) "#HI Hl". rewrite pointsto_unseal.
+  iApply make_inv_pointsto; done.
+Qed.
 Lemma inv_pointsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
 Proof. apply inv_pointsto_own_inv. Qed.
 
@@ -291,7 +327,7 @@ Lemma inv_pointsto_own_acc_strong E :
     (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗
       inv_pointsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
 Proof.
-  iIntros (?) "#Hinv".
+  iIntros (?) "#Hinv". rewrite pointsto_unseal.
   iMod (inv_pointsto_own_acc_strong with "Hinv") as "Hacc"; first done.
   iIntros "!>" (l v I) "Hl". iDestruct ("Hacc" with "Hl") as "(% & Hl & Hclose)".
   iFrame "%∗". iIntros (w) "% Hl". iApply "Hclose"; done.
@@ -302,7 +338,7 @@ Lemma inv_pointsto_own_acc E l v I:
   inv_heap_inv -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
     (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
 Proof.
-  iIntros (?) "#Hinv Hl".
+  iIntros (?) "#Hinv Hl". rewrite pointsto_unseal.
   iMod (inv_pointsto_own_acc with "Hinv Hl") as "(% & Hl & Hclose)"; first done.
   iFrame "%∗". iIntros "!>" (w) "% Hl". iApply "Hclose"; done.
 Qed.
@@ -312,7 +348,7 @@ Lemma inv_pointsto_acc l I E :
   inv_heap_inv -∗ l ↦_I □ ={E, E ∖ ↑inv_heapN}=∗
     ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ True).
 Proof.
-  iIntros (?) "#Hinv Hl".
+  iIntros (?) "#Hinv Hl". rewrite pointsto_unseal.
   iMod (inv_pointsto_acc with "Hinv Hl") as ([v|]) "(% & Hl & Hclose)"; [done| |done].
   iIntros "!>". iExists (v). iFrame "%∗".
 Qed.
@@ -348,7 +384,8 @@ Proof.
   rewrite Loc.add_0 -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
   setoid_rewrite <-Loc.add_assoc.
-  rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
+  rewrite big_opM_singleton pointsto_unseal.
+  iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
 Qed.
 
 Lemma twp_allocN_seq s E v n :
@@ -423,7 +460,7 @@ Lemma twp_free s E l v :
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
-  iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with base_step.
   iIntros (κ v2 σ2 efs Hstep); inv_base_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".
@@ -450,7 +487,7 @@ Lemma twp_load s E l dq v :
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
-  iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with base_step.
   iIntros (κ v2 σ2 efs Hstep); inv_base_step.
   iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
@@ -478,7 +515,7 @@ Lemma twp_store s E l v' v :
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
-  iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with base_step.
   iIntros (κ v2 σ2 efs Hstep); inv_base_step.
   iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
@@ -507,7 +544,7 @@ Lemma twp_xchg s E l v' v :
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
-  iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with base_step.
   iIntros (κ v2 σ2 efs Hstep); inv_base_step.
   iMod (steps_auth_update_S with "Hsteps") as "Hsteps".
@@ -537,7 +574,7 @@ Lemma twp_cmpxchg_fail s E l dq v' v1 v2 :
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
-  iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with base_step.
   iIntros (κ v2' σ2 efs Hstep); inv_base_step.
   rewrite bool_decide_false //.
@@ -570,7 +607,7 @@ Lemma twp_cmpxchg_suc s E l v1 v2 v' :
 Proof.
   iIntros (?? Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
-  iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with base_step.
   iIntros (κ v2' σ2 efs Hstep); inv_base_step.
   rewrite bool_decide_true //.
@@ -604,7 +641,7 @@ Lemma twp_faa s E l i1 i2 :
 Proof.
   iIntros (Φ) "Hl HΦ". iApply twp_lift_atomic_base_step_no_fork; first done.
   iIntros (σ1 ns κs nt) "(Hσ & Hκs & Hsteps) !>".
-  iDestruct (gen_heap_valid with "Hσ Hl") as %?.
+  rewrite pointsto_unseal. iDestruct (gen_heap_valid with "Hσ Hl") as %?.
   iSplit; first by eauto with base_step.
   iIntros (κ e2 σ2 efs Hstep); inv_base_step.
   iMod (gen_heap_update with "Hσ Hl") as "[$ Hl]".