Fractional heap.

heap_lang/heap.v

 From heap_lang Require Export lifting.
-From algebra Require Import upred_big_op frac.
+From algebra Require Import upred_big_op frac dec_agree.
 From program_logic Require Export invariants ghost_ownership.
 From program_logic Require Import ownership auth.
 Import uPred.
@@ -7,7 +7,7 @@ Import uPred.
    a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
    predicates over finmaps instead of just ownP. *)
 
-Definition heapRA : cmraT := mapRA loc (exclRA (leibnizC val)).
+Definition heapRA : cmraT := mapRA loc (fracRA (dec_agreeRA val)).
 Definition heapGF : iFunctor := authGF heapRA.
 
 Class heapG Σ := HeapG {
@@ -17,13 +17,15 @@ Class heapG Σ := HeapG {
 Instance heap_authG `{i : heapG Σ} : authG heap_lang Σ heapRA :=
   {| auth_inG := heap_inG |}.
 
-Definition to_heap : state → heapRA := fmap Excl.
-Definition of_heap : heapRA → state := omap (maybe Excl).
+Definition to_heap : state → heapRA := fmap (λ v, Frac 1 (DecAgree v)).
+Definition of_heap : heapRA → state :=
+  omap (mbind (maybe DecAgree ∘ snd) ∘ maybe2 Frac).
 
 (* heap_mapsto is defined strongly opaquely, to prevent unification from
 matching it against other forms of ownership. *)
-Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
-  auth_own heap_name {[ l := Excl v ]}.
+Definition heap_mapsto `{heapG Σ}
+    (l : loc)(q : Qp) (v: val) : iPropG heap_lang Σ :=
+  auth_own heap_name {[ l := Frac q (DecAgree v) ]}.
 Typeclasses Opaque heap_mapsto.
 
 Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
@@ -31,7 +33,9 @@ Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
 Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
   auth_ctx heap_name N heap_inv.
 
-Notation "l ↦ v" := (heap_mapsto l v) (at level 20) : uPred_scope.
+Notation "l ↦{ q } v" := (heap_mapsto l q v)
+  (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
+Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
 
 Section heap.
   Context {Σ : iFunctorG}.
@@ -50,27 +54,45 @@ Section heap.
   Qed.
   Lemma to_heap_valid σ : ✓ to_heap σ.
   Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
-  Lemma of_heap_insert l v h : of_heap (<[l:=Excl v]> h) = <[l:=v]> (of_heap h).
-  Proof. by rewrite /of_heap -(omap_insert _ _ _ (Excl v)). Qed.
-  Lemma to_heap_insert l v σ : to_heap (<[l:=v]> σ) = <[l:=Excl v]> (to_heap σ).
+  Lemma of_heap_insert l v h :
+    of_heap (<[l:=Frac 1 (DecAgree v)]> h) = <[l:=v]> (of_heap h).
+  Proof. by rewrite /of_heap -(omap_insert _ _ _ (Frac 1 (DecAgree v))). Qed.
+  Lemma of_heap_singleton_op l q v h :
+    ✓ ({[l := Frac q (DecAgree v)]} ⋅ h) →
+    of_heap ({[l := Frac q (DecAgree v)]} ⋅ h) = <[l:=v]> (of_heap h).
+  Proof.
+    intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|].
+    - move: (Hv l). rewrite /of_heap lookup_insert
+        lookup_omap (lookup_op _ h) lookup_singleton.
+      case _:(h !! l)=>[[q' [v'|]|]|] //=; last by move=> [??].
+      move=> [? /dec_agree_op_inv [->]]. by rewrite dec_agree_idemp.
+    - rewrite /of_heap lookup_insert_ne // !lookup_omap.
+      by rewrite (lookup_op _ h) lookup_singleton_ne // left_id.
+  Qed.
+  Lemma to_heap_insert l v σ :
+    to_heap (<[l:=v]> σ) = <[l:=Frac 1 (DecAgree v)]> (to_heap σ).
   Proof. by rewrite /to_heap -fmap_insert. Qed.
   Lemma of_heap_None h l :
-    ✓ h → of_heap h !! l = None → h !! l = None ∨ h !! l ≡ Some ExclUnit.
+    ✓ h → of_heap h !! l = None → h !! l = None ∨ h !! l ≡ Some FracUnit.
   Proof.
     move=> /(_ l). rewrite /of_heap lookup_omap.
-    by case: (h !! l)=> [[]|]; auto.
+    by case: (h !! l)=> [[q [v|]|]|] //=; destruct 1; auto.
   Qed.
-  Lemma heap_singleton_inv_l h l v :
-    ✓ ({[l := Excl v]} ⋅ h) → h !! l = None ∨ h !! l ≡ Some ExclUnit.
+  Lemma heap_store_valid l h v1 v2 :
+    ✓ ({[l := Frac 1 (DecAgree v1)]} ⋅ h) →
+    ✓ ({[l := Frac 1 (DecAgree v2)]} ⋅ h).
   Proof.
-    move=> /(_ l). rewrite lookup_op lookup_singleton.
-    by case: (h !! l)=> [[]|]; auto.
+    intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|].
+    - rewrite !lookup_op !lookup_singleton.
+      case: (h !! l)=>[x|]; [|done]=> /frac_valid_inv_l=>-> //.
+    - by rewrite !lookup_op !lookup_singleton_ne.
   Qed.
+  Hint Resolve heap_store_valid.
 
   (** Allocation *)
   Lemma heap_alloc E N σ :
     authG heap_lang Σ heapRA → nclose N ⊆ E →
-    ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} heap_mapsto).
+    ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} (λ l v, l ↦ v)).
   Proof.
     intros. rewrite -{1}(from_to_heap σ). etrans.
     { rewrite [ownP _]later_intro.
@@ -95,11 +117,19 @@ Section heap.
   Proof. solve_proper. Qed.
 
   (** General properties of mapsto *)
-  Lemma heap_mapsto_disjoint l v1 v2 : (l ↦ v1 ★ l ↦ v2)%I ⊑ False.
+  Lemma heap_mapsto_op_eq l q1 q2 v :
+    (l ↦{q1} v ★ l ↦{q2} v)%I ≡ (l ↦{q1+q2} v)%I.
+  Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.
+
+  Lemma heap_mapsto_op l q1 q2 v1 v2 :
+    (l ↦{q1} v1 ★ l ↦{q2} v2)%I ≡ (v1 = v2 ∧ l ↦{q1+q2} v1)%I.
   Proof.
-    rewrite -auth_own_op auth_own_valid map_op_singleton.
-    rewrite map_validI (forall_elim l) lookup_singleton.
-    by rewrite option_validI excl_validI.
+    destruct (decide (v1 = v2)) as [->|].
+    { by rewrite heap_mapsto_op_eq const_equiv // left_id. }
+    rewrite -auth_own_op map_op_singleton Frac_op dec_agree_ne //.
+    apply (anti_symm (⊑)); last by apply const_elim_l.
+    rewrite auth_own_valid map_validI (forall_elim l) lookup_singleton.
+    rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
   (** Weakest precondition *)
@@ -120,29 +150,28 @@ Section heap.
     apply sep_mono_r; rewrite HP; apply later_mono.
     apply forall_mono=> l; apply wand_intro_l.
     rewrite always_and_sep_l -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(exist_intro (op {[ l := Excl v ]})).
+    rewrite -(exist_intro (op {[ l := Frac 1 (DecAgree v) ]})).
     repeat erewrite <-exist_intro by apply _; simpl.
     rewrite -of_heap_insert left_id right_id.
     rewrite /heap_mapsto. ecancel [_ -★ Φ _]%I.
     rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
-    rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
-    apply later_intro.
+    rewrite const_equiv; last by apply (map_insert_valid h).
+    by rewrite left_id -later_intro.
   Qed.
 
-  Lemma wp_load N E l v P Φ :
+  Lemma wp_load N E l q v P Φ :
     P ⊑ heap_ctx N → nclose N ⊆ E →
-    P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Φ v)) →
+    P ⊑ (▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) →
     P ⊑ || Load (Loc l) @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=> ?? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
+      with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_load_pst _ (<[l:=v]>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
-    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
-    rewrite -of_heap_insert.
+    rewrite /heap_inv of_heap_singleton_op //.
     apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
   Qed.
 
@@ -153,33 +182,30 @@ Section heap.
     P ⊑ || Store (Loc l) e @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=> ??? HPΦ.
-    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
-      with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
+    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
+      with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
-    rewrite /heap_inv alter_singleton insert_insert.
-    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
-    rewrite -!of_heap_insert const_equiv;
-      last (split; [naive_solver|by eapply map_insert_valid, cmra_valid_op_r]).
+    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
+    rewrite const_equiv; last naive_solver.
     apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
   Qed.
 
-  Lemma wp_cas_fail N E l v' e1 v1 e2 v2 P Φ :
+  Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 P Φ :
     to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
     P ⊑ heap_ctx N → nclose N ⊆ E →
-    P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Φ (LitV (LitBool false)))) →
+    P ⊑ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) →
     P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=>????? HPΦ.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
+      with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
     rewrite const_equiv // left_id.
-    rewrite -(map_insert_singleton_op h); last by eapply heap_singleton_inv_l.
-    rewrite -of_heap_insert.
+    rewrite /heap_inv !of_heap_singleton_op //.
     apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
   Qed.
 
@@ -190,17 +216,14 @@ Section heap.
     P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
   Proof.
     rewrite /heap_ctx /heap_inv=> ???? HPΦ.
-    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
-      with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
+    apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
+      with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
     rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
     rewrite -assoc discrete_valid; apply const_elim_sep_l=> ?.
     rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
       last by rewrite lookup_insert.
-    rewrite /heap_inv alter_singleton insert_insert.
-    rewrite -!(map_insert_singleton_op h); try by eapply heap_singleton_inv_l.
-    rewrite -!of_heap_insert const_equiv; last first.
-    { split; last by eapply map_insert_valid, cmra_valid_op_r.
-      eexists; rewrite lookup_insert; naive_solver. }
+    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
+    rewrite lookup_insert const_equiv; last naive_solver.
     apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
   Qed.
 End heap.