Add U-modality

_CoqProject

@@ -4,6 +4,7 @@
 theories/lib/mset.v
 theories/lib/flock.v
 theories/lib/locking_heap.v
+theories/lib/U.v
 theories/c_translation/monad.v
 theories/c_translation/lifting.v
 theories/c_translation/proofmode.v

theories/c_translation/lifting.v

@@ -4,18 +4,6 @@ From iris.base_logic.lib Require Import fractional.
 From iris_c.lib Require Export locking_heap mset flock.
 From iris_c.c_translation Require Export monad.
 
-Notation "l ↦[ x ] v" := (mapsto l x v)
-  (at level 20, x at level 50, format "l  ↦[ x ]  v") : uPred_scope.
-Notation "l ↦L v" := (l ↦[LLvl] v)%I
-  (at level 20, format "l  ↦L  v") : uPred_scope.
-Notation "l ↦U v" := (l ↦[ULvl] v)%I
-  (at level 20, format "l  ↦U  v") : uPred_scope.
-
-Notation "l ↦L -" := (∃ v, l ↦L v)%I
-  (at level 20, format "l  ↦L  -") : uPred_scope.
-Notation "l ↦U -" := (∃ v, l ↦U v)%I
-  (at level 20, format "l  ↦U  -") : uPred_scope.
-
 Section lifting.
   Context `{locking_heapG Σ, heapG Σ, flockG Σ}.
 

theories/c_translation/translation.v

@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.heap_lang Require Import spin_lock assert par.
 From iris.algebra Require Import frac auth.
 From iris.base_logic.lib Require Import fractional.
-From iris_c.lib Require Import locking_heap mset flock.
+From iris_c.lib Require Import locking_heap mset flock U.
 From iris_c.c_translation Require Import monad lifting proofmode.
 
 Definition a_alloc : val := λ: "x",
@@ -41,6 +41,40 @@ Definition a_seq : val := λ: "env",
 Section proofs.
   Context `{locking_heapG Σ, heapG Σ, flockG Σ, spawnG Σ}.
 
+  Lemma a_seq_spec R `{Timeless _ R} Φ :
+    U (Φ #()) -∗
+    awp a_seq R Φ.
+  Proof.
+    iIntros "HΦ". rewrite /a_seq.
+    rewrite /awp. iIntros (γ π env lk) "Hflock Hunfl".
+    wp_rec. iRevert "Hflock Hunfl". iRevert (γ π env lk).
+    iApply awp_atomic_env.
+    iIntros (env) "Henv HR".
+    iApply wp_fupd.
+    rewrite {2}/env_inv.
+    iDestruct "Henv" as (X σ) "(HX & Hσ & Hls & Hlocks)".
+    iDestruct "Hlocks" as %Hlocks.
+    wp_let. iApply (mset_clear_spec with "HX").
+    iNext. iIntros "HX".
+    iDestruct "HΦ" as (us) "[Hus HΦ]".
+    clear Hlocks.
+    iInduction us as [|u us] "IH" forall (σ); simpl.
+    - iModIntro. iFrame "HR". iSplitR "HΦ".
+      + iExists ∅, σ. iFrame. iPureIntro.
+        rewrite /correct_locks /set_Forall. set_solver.
+      + by iApply "HΦ".
+    - iDestruct "Hus" as "[Hu Hus]".
+      iAssert (⌜σ !! u.1 = Some LLvl⌝%I) with "[Hσ Hu]" as %?.
+      { rewrite mapsto_eq /mapsto_def.
+        iDestruct "Hu" as "[Hu Hl]".
+          by iDestruct (own_valid_2 with "Hσ Hl")
+            as %[?%heap_singleton_included _]%auth_valid_discrete_2. }
+      iMod (locking_heap_change_lock _ _ _ ULvl with "Hσ Hu") as "[Hσ Hu]".
+      iApply ("IH" with "Hus [HΦ Hu] Hσ [Hls] HR HX").
+      { iIntros "Hus". iApply "HΦ". by iFrame. }
+      { rewrite -big_sepM_insert_override; eauto. }
+  Qed.
+
   Lemma a_load_spec R `{Timeless _ R} (l : loc) (v : val) Φ :
     l ↦U v -∗
     (l ↦U v -∗ Φ v) -∗

theories/lib/U.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.algebra Require Import frac.
+From iris.base_logic.lib Require Import fractional.
+From iris_c.lib Require Import flock locking_heap.
+
+Section contents.
+  Context `{heapG Σ, flockG Σ, locking_heapG Σ}.
+
+  (** * Unlocking modality *)
+  Definition U (P : iProp Σ) : iProp Σ :=
+  (∃ ls : list (loc*val),
+    ([∗ list] x ∈ ls, x.1 ↦L x.2) ∗
+    (([∗ list] x ∈ ls, x.1 ↦U x.2) -∗ P))%I.
+
+  Lemma U_mono P Q : (P ⊢ Q) → (U P) ⊢ (U Q).
+  Proof.
+    intros HPQ.
+    unfold U. iDestruct 1 as (ls) "[Hls HP]".
+    iExists ls. iFrame. iIntros "Hls". iApply HPQ. by iApply "HP".
+  Qed.
+
+  Lemma U_intro P : P ⊢ U P.
+  Proof.
+    iIntros "HP". iExists [].
+    rewrite !big_sepL_nil. eauto.
+  Qed.
+
+  Lemma U_multiplicative P Q : (U P) ∗ (U Q) ⊢ (U (P ∗ Q)).
+  Proof.
+    iIntros "[HP HQ]".
+    iDestruct "HP" as (ls1) "[HP1 HP2]".
+    iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
+    iExists (ls1++ls2). rewrite !big_sepL_app. iFrame.
+    iIntros "[HP1 HQ1]". iSplitL "HP1 HP2".
+    - by iApply "HP2".
+    - by iApply "HQ2".
+  Qed.
+
+  Lemma U_unlock l v : l ↦L v ⊢ U (l ↦U v).
+  Proof.
+    iIntros "Hl". iExists [(l,v)].
+    rewrite !big_sepL_cons !big_sepL_nil !right_id.
+    iFrame. simpl. iIntros "Hl". iFrame.
+  Qed.
+
+End contents.

theories/lib/locking_heap.v

@@ -204,3 +204,14 @@ Section properties.
   Qed.
 End properties.
 
+Notation "l ↦[ x ] v" := (mapsto l x v)
+  (at level 20, x at level 50, format "l  ↦[ x ]  v") : uPred_scope.
+Notation "l ↦L v" := (l ↦[LLvl] v)%I
+  (at level 20, format "l  ↦L  v") : uPred_scope.
+Notation "l ↦U v" := (l ↦[ULvl] v)%I
+  (at level 20, format "l  ↦U  v") : uPred_scope.
+
+Notation "l ↦L -" := (∃ v, l ↦L v)%I
+  (at level 20, format "l  ↦L  -") : uPred_scope.
+Notation "l ↦U -" := (∃ v, l ↦U v)%I
+  (at level 20, format "l  ↦U  -") : uPred_scope.