Add the locking_heap ghost theory

_CoqProject

@@ -3,5 +3,6 @@
 
 theories/lib/mset.v
 theories/lib/flock.v
+theories/lib/locking_heap.v
 theories/c_translation/monad.v
-theories/c_translation/translation.v
\ No newline at end of file
+theories/c_translation/translation.v

theories/lib/locking_heap.v

+From iris.algebra Require Import cmra auth gmap excl.
+From iris.base_logic.lib Require Export own.
+From iris.heap_lang Require Import lang lifting.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+Import uPred.
+
+Inductive level : Set :=
+| LLvl : level
+| ULvl : level.
+Canonical Structure lvlC := leibnizC level.
+
+Definition locking_heapUR : ucmraT :=
+  gmapUR loc (exclR lvlC).
+
+(** The CMRA we need. *)
+Class locking_heapG (Σ : gFunctors) := LHeapG {
+  lheap_inG :> inG Σ (authR locking_heapUR);
+  lheap_name : gname
+}.
+Class locking_heapPreG (Σ : gFunctors) :=
+  { lheap_preG_inG :> inG Σ (authR locking_heapUR) }.
+
+Definition locking_heapΣ : gFunctors :=
+  #[GFunctor (authR locking_heapUR)].
+
+Instance subG_heapPreG {Σ} :
+  subG locking_heapΣ Σ → locking_heapPreG Σ.
+Proof. solve_inG. Qed.
+
+Section definitions.
+  Context `{hG : locking_heapG Σ, !heapG Σ}.
+
+  Definition to_locking_heap (σ : gmap loc level) : locking_heapUR :=
+    fmap (λ x, Excl x) σ.
+
+  Definition is_lock_lvl (a : loc * level) : bool :=
+    match (snd a) with
+    | LLvl => true
+    | ULvl => false
+    end.
+
+  Definition locked_locs (σ : gmap loc level) : gset loc :=
+    dom (gset loc) (filter is_lock_lvl σ).
+
+  Definition full_locking_heap (σ : gmap loc level) :=
+    own (@lheap_name _ hG) (● (to_locking_heap σ)).
+
+  Definition mapsto_def (l : loc) (b : level) (v: val) : iProp Σ :=
+    (l ↦ v ∗
+     own (@lheap_name _ hG) (◯ {[ l := Excl b ]}))%I.
+
+  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
+  Definition mapsto := unseal mapsto_aux.
+  Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
+End definitions.
+
+Local Notation "l ↦[ x ] v" := (mapsto l x v)
+  (at level 20, x at level 50, format "l  ↦[ x ]  v") : uPred_scope.
+Local Notation "l ↦L v" := (l ↦[LLvl] v)%I
+  (at level 20, format "l  ↦L  v") : uPred_scope.
+Local Notation "l ↦U v" := (l ↦[ULvl] v)%I
+  (at level 20, format "l  ↦U  v") : uPred_scope.
+
+Local Notation "l ↦L -" := (∃ v, l ↦L v)%I
+  (at level 20, format "l  ↦L  -") : uPred_scope.
+Local Notation "l ↦U -" := (∃ v, l ↦U v)%I
+  (at level 20, format "l  ↦U  -") : uPred_scope.
+
+Lemma to_locking_heap_valid (σ : gmap loc level) : ✓ to_locking_heap σ.
+Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
+
+Lemma locking_heap_init `{locking_heapPreG Σ} σ :
+  (|==> ∃ _ : locking_heapG Σ, full_locking_heap σ)%I.
+Proof.
+  iMod (own_alloc (● to_locking_heap σ)) as (γ) "Hh".
+  { apply: auth_auth_valid. exact: to_locking_heap_valid. }
+  iModIntro. by iExists (LHeapG Σ _ γ).
+Qed.
+
+Section properties.
+  Context `{hG : locking_heapG Σ, !heapG Σ}.
+  Implicit Type σ : gmap loc level.
+  Implicit Type x y : level.
+  Implicit Type l : loc.
+
+  Lemma to_locking_heap_insert σ l x :
+    to_locking_heap (<[l := x]> σ) = <[l := Excl x]>(to_locking_heap σ).
+  Proof. by rewrite /to_locking_heap fmap_insert. Qed.
+
+  Lemma to_locking_heap_lookup_Some σ l x :
+    σ !! l = Some x → to_locking_heap σ !! l = Some (Excl x).
+  Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
+  Lemma to_locking_heap_lookup_None σ l :
+    σ !! l = None → to_locking_heap σ !! l = None.
+  Proof. rewrite /to_locking_heap lookup_fmap => -> //. Qed.
+  
+  Lemma locked_locs_lock σ l :
+    locked_locs (<[l := LLvl]>σ) = {[l]} ∪ locked_locs σ.
+  Proof.
+    rewrite /locked_locs -map_filter_lookup_insert; last done.
+    apply dom_insert_L.
+  Qed.
+
+  Lemma locked_locs_unlock σ l :
+    σ !! l = Some LLvl →
+    locked_locs (<[l := ULvl]>σ) = locked_locs σ ∖ {[l]}.
+  Proof.
+    intros Hl. rewrite /locked_locs -dom_delete_L. f_equal.
+    apply map_eq => j.
+    destruct (decide (l = j)) as [->|?].
+    - rewrite lookup_delete. apply map_filter_lookup_None.
+      right. intros ?. rewrite lookup_insert=>?. simplify_eq/=.
+      naive_solver.
+    - rewrite lookup_delete_ne; last done.
+      admit.
+  Admitted.
+
+  Lemma heap_singleton_included (σ : gmap loc level) l x :
+    {[l := Excl x]} ≼ (to_locking_heap σ) → σ !! l = Some x.
+  Proof.
+    rewrite singleton_included => -[y []]. fold_leibniz.
+    move=>Hl /Some_included_exclusive Hx. revert Hl.    
+    rewrite /to_locking_heap lookup_fmap fmap_Some => -[z [-> Hz]].
+    simplify_eq/=. naive_solver.
+  Qed.
+
+  Lemma locked_locs_locked σ l v :
+    l ↦L v -∗ full_locking_heap σ -∗ ⌜l ∈ locked_locs σ⌝.
+  Proof.
+    rewrite mapsto_eq /mapsto_def /full_locking_heap.
+    iIntros "[Hl Hpart] Hfull".
+    iDestruct (own_valid_2 with "Hfull Hpart")
+      as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
+    iPureIntro. rewrite /locked_locs.
+    eapply elem_of_dom_2. apply map_filter_lookup_Some. eauto.
+  Qed.
+
+  Lemma locked_locs_unlocked σ l v :
+    l ↦U v -∗ full_locking_heap σ -∗ ⌜l ∉ locked_locs σ⌝.
+  Proof.
+    rewrite mapsto_eq /mapsto_def /full_locking_heap.
+    iIntros "[Hl Hpart] Hfull".
+    iDestruct (own_valid_2 with "Hfull Hpart")
+      as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
+    iPureIntro. rewrite /locked_locs.
+    eapply not_elem_of_dom. apply map_filter_lookup_None.
+    right. intros. simplify_eq/=. eauto.
+  Qed.
+
+  Lemma locking_heap_change_lock (l : loc) (v : val) (x y : level) σ :
+    full_locking_heap σ -∗ l ↦[ x ] v
+    ==∗ full_locking_heap (<[l:=y]>σ) ∗ l ↦[ y ] v.
+  Proof.
+    rewrite /full_locking_heap mapsto_eq /mapsto_def.
+    iIntros "Hauth ($ & Hl)".
+    iDestruct (own_valid_2 with "Hauth Hl")
+      as %[Hl%heap_singleton_included _]%auth_valid_discrete_2.
+    iMod (own_update_2 with "Hauth Hl") as "Hauth".
+    { apply (auth_update _ _ (to_locking_heap (<[l:=y]>σ)) {[l := Excl y]}).
+      rewrite to_locking_heap_insert.
+      eapply singleton_local_update; first by eapply to_locking_heap_lookup_Some.
+      by apply exclusive_local_update. }
+    by iDestruct "Hauth" as "[$ $]".
+  Qed.
+
+  Lemma locking_heap_alloc σ l x v :
+    σ !! l = None →
+    l ↦ v -∗ full_locking_heap σ ==∗ full_locking_heap (<[l:=x]>σ) ∗ l ↦[ x ] v.
+  Proof.
+    rewrite /full_locking_heap mapsto_eq /mapsto_def. iIntros (?) "$ Hauth".
+    iMod (own_update with "Hauth") as "Hauth".
+    { eapply (auth_update_alloc _ (to_locking_heap (<[l:=x]> σ)) {[l := Excl x]}).
+      rewrite to_locking_heap_insert.
+      apply alloc_singleton_local_update; last done.
+      by apply to_locking_heap_lookup_None. }
+    by iDestruct "Hauth" as "[$ $]".
+  Qed.
+End properties.