From a3f775877c35f4f9d9d30d14d7fa4ac1ff5095ca Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 9 May 2019 14:58:19 +0200
Subject: [PATCH] better abstract predicate for the lock on the RHS

---
 theories/examples/coinflip.v         |  4 ++--
 theories/examples/stack/CG_stack.v   | 12 ++++++------
 theories/examples/stack/refinement.v |  2 +-
 theories/examples/symbol.v           |  2 +-
 theories/examples/ticket_lock.v      | 24 ++++++++++++------------
 theories/lib/counter.v               | 10 +++++-----
 theories/lib/lock.v                  | 18 +++++++-----------
 theories/logic/proofmode/tactics.v   | 14 +++++++++++++-
 8 files changed, 47 insertions(+), 39 deletions(-)

diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index 3314179..2e9c2fd 100644
--- a/theories/examples/coinflip.v
+++ b/theories/examples/coinflip.v
@@ -131,7 +131,7 @@ Section proofs.
     rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
     do 2 rel_pure_r.
     iMod (inv_alloc coinN _
-           (∃ (b : bool), is_lock_r lk Unlocked_r
+           (∃ (b : bool), is_locked_r lk false
                         ∗ ce ↦ #b
                         ∗ (cl ↦ₛ NONEV ∨ cl ↦ₛ SOMEV #b))%I
             with "[-]") as "#Hinv".
@@ -252,7 +252,7 @@ Section proofs.
     rel_apply_r refines_newlock_r. iIntros (lk) "Hlk".
 
     iMod (inv_alloc coinN _
-           (is_lock_r lk Unlocked_r
+           (is_locked_r lk false
           ∗ (c' ↦ₛ NONEV ∗ c ↦ NONEV
             ∨ ∃ (b : bool), c' ↦ₛ SOMEV #b ∗ c ↦ SOMEV #b))%I
             with "[-]") as "#Hinv".
diff --git a/theories/examples/stack/CG_stack.v b/theories/examples/stack/CG_stack.v
index db2ec40..3cb0452 100644
--- a/theories/examples/stack/CG_stack.v
+++ b/theories/examples/stack/CG_stack.v
@@ -39,8 +39,8 @@ Section rules.
 
   Lemma refines_CG_push_r st l (v w : val) E t K A :
     nclose relocN ⊆ E →
-    st ↦ₛ v -∗ is_lock_r l Unlocked_r -∗
-    (st ↦ₛ SOMEV (w, v) -∗ is_lock_r l Unlocked_r
+    st ↦ₛ v -∗ is_locked_r l false -∗
+    (st ↦ₛ SOMEV (w, v) -∗ is_locked_r l false
       -∗ REL t << fill K (of_val #()) @ E : A) -∗
     REL t << fill K (CG_locked_push (#st, l)%V w) @ E : A.
   Proof.
@@ -59,8 +59,8 @@ Section rules.
   Lemma refines_CG_pop_suc_r st l (w v : val) E t K A :
     nclose relocN ⊆ E →
     st ↦ₛ SOMEV (w, v) -∗
-    is_lock_r l Unlocked_r -∗
-    (st ↦ₛ v -∗ is_lock_r l Unlocked_r
+    is_locked_r l false -∗
+    (st ↦ₛ v -∗ is_locked_r l false
       -∗ REL t << fill K (of_val (SOMEV w)) @ E : A) -∗
     REL t << fill K (CG_locked_pop (#st, l)%V) @ E : A.
   Proof.
@@ -78,8 +78,8 @@ Section rules.
   Lemma refines_CG_pop_fail_r st l E t K A :
     nclose relocN ⊆ E →
     st ↦ₛ NONEV -∗
-    is_lock_r l Unlocked_r -∗
-    (st ↦ₛ NONEV -∗ is_lock_r l Unlocked_r
+    is_locked_r l false -∗
+    (st ↦ₛ NONEV -∗ is_locked_r l false
       -∗ REL t << fill K (of_val NONEV) @ E : A) -∗
     REL t << fill K (CG_locked_pop (#st, l)%V) @ E : A.
   Proof.
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index 98a59f0..0049631 100644
--- a/theories/examples/stack/refinement.v
+++ b/theories/examples/stack/refinement.v
@@ -72,7 +72,7 @@ Section proof.
   Definition sinv (A : lrel Σ) stk stk' l' : iProp Σ :=
     (∃ (istk : loc) v,
        stk' ↦ₛ v
-     ∗ is_lock_r l' Unlocked_r
+     ∗ is_locked_r l' false
      ∗ stk  ↦ #istk
      ∗ stack_link A istk v)%I.
 
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index a0ca780..10d97f3 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -110,7 +110,7 @@ Section rules.
   Definition lok_inv (size1 size2 tbl1 tbl2 : loc) (l : val) : iProp Σ :=
     (∃ (n : nat) (ls : val), size1 ↦{1/2} #n ∗ size2 ↦ₛ{1/2} #n
                            ∗ tbl1 ↦{1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
-                           ∗ is_lock_r l Unlocked_r)%I.
+                           ∗ is_locked_r l false)%I.
 End rules.
 
 Section proof.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index ce9a449..24db89b 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -74,13 +74,13 @@ Section refinement.
 
   (** * Invariants and abstracts for them *)
   Definition lockInv (lo ln : loc) (γ : gname) (l' : val) : iProp Σ :=
-    (∃ (o n : nat) (st : lock_status_r), lo ↦ #o ∗ ln ↦ #n
-   ∗ issuedTickets γ n ∗ is_lock_r l' st
-   ∗ match st with Unlocked_r => True | Locked_r => ticket γ o end)%I.
+    (∃ (o n : nat) (b : bool), lo ↦ #o ∗ ln ↦ #n
+   ∗ issuedTickets γ n ∗ is_locked_r l' b
+   ∗ if b then ticket γ o else True)%I.
 
-  Instance ifticket_timeless st γ o :
-    Timeless (match st with Unlocked_r => True | Locked_r => ticket γ o end)%I.
-  Proof. destruct st; apply _. Qed.
+  Instance ifticket_timeless (b : bool) γ o :
+    Timeless (if b then ticket γ o else True)%I.
+  Proof. destruct b; apply _. Qed.
   Instance lockInv_timeless lo ln γ l' : Timeless (lockInv lo ln γ l').
   Proof. apply _. Qed.
 
@@ -136,7 +136,7 @@ Section refinement.
     iIntros "Hlo". repeat rel_pure_l.
     case_decide; simplify_eq/=; rel_if_l.
     (* Whether the ticket is called out *)
-    - destruct st; last first.
+    - destruct st.
       { iDestruct (ticket_nondup with "Hticket Hbticket") as %[]. }
       rel_apply_r (refines_acquire_r with "Hl'").
       iIntros "Hl'".
@@ -210,8 +210,8 @@ Section refinement.
     iAlways. iIntros (? lk) "/= #Hl".
     iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq/=.
     rel_apply_l (acquire_l_logatomic
-                   (fun o => ∃ st, is_lock_r lk st ∗
-                             if st then True else ticket γ o)%I
+                   (fun o => ∃ st, is_locked_r lk st ∗
+                             if st then ticket γ o else True)%I
                    True%I γ); first done.
     iAlways.
     openI.
@@ -226,7 +226,7 @@ Section refinement.
       iNext. iExists _,_,_. by iFrame.
     - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Ht & Hrest)".
       iIntros "_". iDestruct "Hrest" as (st) "[Hl' Ht']".
-      destruct st; last first.
+      destruct st.
       { iDestruct (ticket_nondup with "Ht Ht'") as %[]. }
       rel_apply_r (refines_acquire_r with "Hl'").
       iIntros "Hl'".
@@ -310,8 +310,8 @@ Section refinement.
     rel_rec_l. rel_proj_l.
     pose (R := fun (o : nat) =>
                  (∃ (n : nat) st, ln ↦ #n
-                 ∗ issuedTickets γ n ∗ is_lock_r lk st ∗
-                 if st then True else ticket γ o)%I).
+                 ∗ issuedTickets γ n ∗ is_locked_r lk st ∗
+                 if st then ticket γ o else True)%I).
     rel_apply_l (wkincr_atomic_l R True%I); first done.
     iAlways.
     openI.
diff --git a/theories/lib/counter.v b/theories/lib/counter.v
index bc5d4ef..fba4c9f 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -34,8 +34,8 @@ Section CG_Counter.
 
   Lemma CG_increment_r K E t A (x : loc) (lk : val) (n : nat) :
     nclose specN ⊆ E →
-    (x ↦ₛ # n -∗ is_lock_r lk Unlocked_r -∗
-    (x ↦ₛ # (n + 1) -∗ is_lock_r lk Unlocked_r -∗
+    (x ↦ₛ # n -∗ is_locked_r lk false -∗
+    (x ↦ₛ # (n + 1) -∗ is_locked_r lk false -∗
       (REL t << fill K (of_val #n) @ E : A)) -∗
     REL t << fill K (CG_increment #x lk) @ E : A)%I.
   Proof.
@@ -141,7 +141,7 @@ Section CG_Counter.
   Definition counterN : namespace := nroot .@ "counter".
 
   Definition counter_inv lk cnt cnt' : iProp Σ :=
-    (∃ n : nat, is_lock_r lk Unlocked_r ∗ cnt ↦ #n ∗ cnt' ↦ₛ #n)%I.
+    (∃ n : nat, is_locked_r lk false ∗ cnt ↦ #n ∗ cnt' ↦ₛ #n)%I.
 
   Lemma FG_CG_increment_refinement lk cnt cnt' :
     inv counterN (counter_inv lk cnt cnt') -∗
@@ -150,7 +150,7 @@ Section CG_Counter.
     iIntros "#Hinv".
     rel_apply_l
       (FG_increment_atomic_l
-              (fun n => is_lock_r lk Unlocked_r ∗ cnt' ↦ₛ #n)%I
+              (fun n => is_locked_r lk false ∗ cnt' ↦ₛ #n)%I
               True%I); first done.
     iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro.
     iDestruct "Hcnt" as (n) "(Hl & Hcnt & Hcnt')".
@@ -175,7 +175,7 @@ Section CG_Counter.
     iIntros "#Hinv".
     rel_apply_l
       (counter_read_atomic_l
-         (fun n => is_lock_r lk Unlocked_r ∗ cnt' ↦ₛ #n)%I
+         (fun n => is_locked_r lk false ∗ cnt' ↦ₛ #n)%I
          True%I); first done.
     iAlways. iInv counterN as (n) "[>Hl [>Hcnt >Hcnt']]" "Hclose".
     iModIntro.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index d0e60e8..d6a3dfc 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -110,16 +110,12 @@ Section lock_rules_r.
   Context `{relocG Σ}.
   Variable (E : coPset).
 
-  Inductive lock_status_r := Unlocked_r | Locked_r.
-  Global Instance lock_status_r_inhab : Inhabited lock_status_r :=
-    populate Unlocked_r.
-
-  Definition is_lock_r v (st : lock_status_r) :=
-    (∃ lk : loc, ⌜v = #lk⌝ ∗ lk ↦ₛ #(if st then false else true))%I.
+  Definition is_locked_r v (b : bool) :=
+    (∃ lk : loc, ⌜v = #lk⌝ ∗ lk ↦ₛ #b)%I.
 
   Lemma refines_newlock_r K t A
     (Hcl : nclose specN ⊆ E) :
-    (∀ v, is_lock_r v Unlocked_r -∗ REL t << fill K (of_val v) @ E : A) -∗
+    (∀ v, is_locked_r v false -∗ REL t << fill K (of_val v) @ E : A) -∗
     REL t << fill K (newlock #()) @ E : A.
   Proof.
     iIntros "Hlog".
@@ -131,8 +127,8 @@ Section lock_rules_r.
 
   Lemma refines_acquire_r K v t A
     (Hcl : nclose specN ⊆ E) :
-    is_lock_r v Unlocked_r -∗
-    (is_lock_r v Locked_r -∗ REL t << fill K (of_val #()) @ E : A) -∗
+    is_locked_r v false -∗
+    (is_locked_r v true -∗ REL t << fill K (of_val #()) @ E : A) -∗
     REL t << fill K (acquire v) @ E : A.
   Proof.
     iIntros "Hl Hlog".
@@ -145,8 +141,8 @@ Section lock_rules_r.
 
   Lemma refines_release_r K v t A st
     (Hcl : nclose specN ⊆ E) :
-    is_lock_r v st -∗
-    (is_lock_r v Unlocked_r -∗ REL t << fill K (of_val #()) @ E : A) -∗
+    is_locked_r v st -∗
+    (is_locked_r v false -∗ REL t << fill K (of_val #()) @ E : A) -∗
     REL t << fill K (release v) @ E : A.
   Proof.
     iIntros "Hl Hlog".
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 4f97eb8..1986990 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import
      sel_patterns environments
      reduction.
 From reloc.logic Require Import proofmode.spec_tactics.
-From reloc.logic Require Export model rules.
+From reloc.logic Require Export model rules derived.
 From iris.proofmode Require Export tactics.
 (* Set Default Proof Using "Type". *)
 
@@ -690,3 +690,15 @@ Tactic Notation "rel_op_r" := rel_binop_r.
 Tactic Notation "rel_if_true_r" := rel_pure_r (If #true _ _).
 Tactic Notation "rel_if_false_r" := rel_pure_r (If #false _ _).
 Tactic Notation "rel_if_r" := rel_pure_r (If _ _ _).
+
+Ltac rel_arrow_val :=
+  rel_pures_l; rel_pures_r;
+  (iApply refines_arrow_val
+  || fail "rel_arrow_val: cannot apply the closure rule");
+  iAlways.
+
+Ltac rel_arrow :=
+  rel_pures_l; rel_pures_r;
+  (iApply refines_arrow
+  || fail "rel_arrow: cannot apply the closure rule");
+  iAlways.
-- 
GitLab