diff --git a/theories/examples/coinflip.v b/theories/examples/coinflip.v
index c9745b63dabc6d0082e02e5a093188ab88df859f..331417968cd8855c44d73a93d3f3b758515755e2 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), lk ↦ₛ #false
+           (∃ (b : bool), is_lock_r lk Unlocked_r
                         ∗ 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 _
-           (lk ↦ₛ #false
+           (is_lock_r lk Unlocked_r
           ∗ (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 5cbd28a7a1b6e219b083f28e26a9ec465376163f..db2ec400552b707d50eb798cf1a009a2b25e911d 100644
--- a/theories/examples/stack/CG_stack.v
+++ b/theories/examples/stack/CG_stack.v
@@ -39,10 +39,10 @@ Section rules.
 
   Lemma refines_CG_push_r st l (v w : val) E t K A :
     nclose relocN ⊆ E →
-    st ↦ₛ v -∗ l ↦ₛ #false -∗
-    (st ↦ₛ SOMEV (w, v) -∗ l ↦ₛ #false
+    st ↦ₛ v -∗ is_lock_r l Unlocked_r -∗
+    (st ↦ₛ SOMEV (w, v) -∗ is_lock_r l Unlocked_r
       -∗ REL t << fill K (of_val #()) @ E : A) -∗
-    REL t << fill K (CG_locked_push (#st, #l)%V w) @ E : A.
+    REL t << fill K (CG_locked_push (#st, l)%V w) @ E : A.
   Proof.
     iIntros (?) "Hst Hl Hlog".
     rel_rec_r. repeat rel_pure_r.
@@ -59,10 +59,10 @@ Section rules.
   Lemma refines_CG_pop_suc_r st l (w v : val) E t K A :
     nclose relocN ⊆ E →
     st ↦ₛ SOMEV (w, v) -∗
-    l ↦ₛ #false -∗
-    (st ↦ₛ v -∗ l ↦ₛ #false
+    is_lock_r l Unlocked_r -∗
+    (st ↦ₛ v -∗ is_lock_r l Unlocked_r
       -∗ REL t << fill K (of_val (SOMEV w)) @ E : A) -∗
-    REL t << fill K (CG_locked_pop (#st, #l)%V) @ E : A.
+    REL t << fill K (CG_locked_pop (#st, l)%V) @ E : A.
   Proof.
     iIntros (?) "Hst Hl Hlog".
     rel_rec_r. repeat rel_pure_r.
@@ -78,10 +78,10 @@ Section rules.
   Lemma refines_CG_pop_fail_r st l E t K A :
     nclose relocN ⊆ E →
     st ↦ₛ NONEV -∗
-    l ↦ₛ #false -∗
-    (st ↦ₛ NONEV -∗ l ↦ₛ #false
+    is_lock_r l Unlocked_r -∗
+    (st ↦ₛ NONEV -∗ is_lock_r l Unlocked_r
       -∗ REL t << fill K (of_val NONEV) @ E : A) -∗
-    REL t << fill K (CG_locked_pop (#st, #l)%V) @ E : A.
+    REL t << fill K (CG_locked_pop (#st, l)%V) @ E : A.
   Proof.
     iIntros (?) "Hst Hl Hlog".
     rel_rec_r. repeat rel_pure_r.
diff --git a/theories/examples/stack/refinement.v b/theories/examples/stack/refinement.v
index 69bf97345f890d61cc0ccc32c18c48c334a9dc6d..98a59f0e4b66e4a66155e60761937160dd3ddb4f 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
-     ∗ l'   ↦ₛ #false
+     ∗ is_lock_r l' Unlocked_r
      ∗ stk  ↦ #istk
      ∗ stack_link A istk v)%I.
 
@@ -86,7 +86,7 @@ Section proof.
     A v v' -∗
     REL (FG_push #st v)
        <<
-        (CG_locked_push (#st', #l)%V v') : ().
+        (CG_locked_push (#st', l)%V v') : ().
   Proof.
     iIntros (?) "#Hinv #Hvv".
     rel_rec_l. iLöb as "IH".
@@ -128,7 +128,7 @@ Section proof.
     inv N (sinv A st st' l) -∗
     REL FG_pop #st
       <<
-        CG_locked_pop (#st', #l)%V : () + A.
+        CG_locked_pop (#st', l)%V : () + A.
   Proof.
     iIntros (?) "#Hinv".
     iLöb as "IH". rel_rec_l.
@@ -184,7 +184,7 @@ Section proof.
   Qed.
 
   Definition stackInt A : lrel Σ := LRel (λ v1 v2,
-    ∃ (l stk stk' : loc), ⌜(v2) = (#stk', #l)%V⌝ ∗ ⌜v1 = #stk⌝
+    ∃ (l : val) (stk stk' : loc), ⌜v2 = (#stk', l)%V⌝ ∗ ⌜v1 = #stk⌝
       ∗ inv (stackN .@ (stk,stk')) (sinv A stk stk' l))%I.
 
   Lemma stack_refinement :
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 5fc5e9bebcbb2f62ed70d7e4897113e636428d95..a0ca780e0915cfc54a8257eb588e76815ae8a751 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -107,10 +107,10 @@ Section rules.
                            ∗ tbl1 ↦{1/2} ls ∗ tbl2 ↦ₛ{1/2} ls
                            ∗ lrel_list lrel_int ls ls)%I.
 
-  Definition lok_inv (size1 size2 tbl1 tbl2 l : loc) : iProp Σ :=
+  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
-                           ∗ l ↦ₛ #false)%I.
+                           ∗ is_lock_r l Unlocked_r)%I.
 End rules.
 
 Section proof.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 672e5b71f390030856245390e1f9e641a28f07b1..ce9a44965fa9e58b23c443cf0b8605b5012fdbba 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -73,27 +73,27 @@ Section refinement.
   Opaque ticket issuedTickets.
 
   (** * Invariants and abstracts for them *)
-  Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ :=
-    (∃ (o n : nat) (b : bool), lo ↦ #o ∗ ln ↦ #n
-   ∗ issuedTickets γ n ∗ l' ↦ₛ #b
-   ∗ if b then ticket γ o else True)%I.
+  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.
 
-  Instance ifticket_timeless (b : bool) γ o : Timeless (if b then ticket γ o else True%I).
-  Proof. destruct b; apply _. Qed.
+  Instance ifticket_timeless st γ o :
+    Timeless (match st with Unlocked_r => True | Locked_r => ticket γ o end)%I.
+  Proof. destruct st; apply _. Qed.
   Instance lockInv_timeless lo ln γ l' : Timeless (lockInv lo ln γ l').
   Proof. apply _. Qed.
 
   Definition N := relocN.@"locked".
 
   Definition lockInt : lrel Σ := LRel (λ v1 v2,
-    ∃ (lo ln : loc) (γ : gname) (l' : loc),
-        ⌜v1 = (#lo, #ln)%V⌝ ∗ ⌜v2 = #l'⌝
-      ∗ inv N (lockInv lo ln γ l'))%I.
+    ∃ (lo ln : loc) (γ : gname),
+     ⌜v1 = (#lo, #ln)%V⌝ ∗ inv N (lockInv lo ln γ v2))%I.
 
   (** * Refinement proofs *)
 
   Local Ltac openI :=
-    iInv N as (o n b) ">(Hlo & Hln & Hissued & Hl' & Hbticket)" "Hcl".
+    iInv N as (o n st) ">(Hlo & Hln & Hissued & Hl' & Hbticket)" "Hcl".
   Local Ltac closeI := iMod ("Hcl" with "[-]") as "_";
     first by (iNext; iExists _,_,_; iFrame).
 
@@ -116,15 +116,15 @@ Section refinement.
     { iNext. iExists 0%nat,0%nat,_. by iFrame. }
     rel_pure_l.
     rel_values.
-    iExists _,_,_,_. iFrame "Hinv". eauto.
+    iExists _,_,_. iFrame "Hinv". eauto.
   Qed.
 
   (* Acquiring a lock *)
   (* helper lemma *)
-  Lemma wait_loop_refinement (lo ln : loc) γ (l' : loc) (m : nat) :
-    inv N (lockInv lo ln γ l') -∗
+  Lemma wait_loop_refinement (lo ln : loc) γ lk (m : nat) :
+    inv N (lockInv lo ln γ lk) -∗
     ticket γ m -∗
-    REL wait_loop #m (#lo, #ln)%V << reloc.lib.lock.acquire #l' : ().
+    REL wait_loop #m (#lo, #ln)%V << reloc.lib.lock.acquire lk : ().
   Proof.
     iIntros "#Hinv Hticket".
     rel_rec_l.
@@ -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 b.
+    - destruct st; last first.
       { iDestruct (ticket_nondup with "Hticket Hbticket") as %[]. }
       rel_apply_r (refines_acquire_r with "Hl'").
       iIntros "Hl'".
@@ -207,27 +207,26 @@ Section refinement.
     REL acquire << reloc.lib.lock.acquire : lockInt → ().
   Proof.
     iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? ?) "/= #Hl".
-    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq/=.
+    iAlways. iIntros (? lk) "/= #Hl".
+    iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq/=.
     rel_apply_l (acquire_l_logatomic
-                   (fun o => ∃ (b : bool),
-                             l' ↦ₛ #b ∗
-                             if b then ticket γ o else True)%I
+                   (fun o => ∃ st, is_lock_r lk st ∗
+                             if st then True else ticket γ o)%I
                    True%I γ); first done.
     iAlways.
     openI.
     iModIntro. iExists _,_; iFrame.
     iSplitL "Hbticket Hl'".
     { iExists _. iFrame. }
-    clear b o n.
+    clear st o n.
     iSplit.
     - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Hrest)".
       iDestruct "Hrest" as (b) "[Hl' Ht]".
       iApply ("Hcl" with "[-]").
       iNext. iExists _,_,_. by iFrame.
     - iIntros (o). iDestruct 1 as (n) "(Hlo & Hln & Hissued & Ht & Hrest)".
-      iIntros "_". iDestruct "Hrest" as (b) "[Hl' Ht']".
-      destruct b.
+      iIntros "_". iDestruct "Hrest" as (st) "[Hl' Ht']".
+      destruct st; last first.
       { iDestruct (ticket_nondup with "Ht Ht'") as %[]. }
       rel_apply_r (refines_acquire_r with "Hl'").
       iIntros "Hl'".
@@ -241,7 +240,7 @@ Section refinement.
   Proof.
     iApply refines_arrow_val; [done|done|].
     iAlways. iIntros (? ?) "/= #Hl".
-    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
+    iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq.
     rel_rec_l. repeat rel_proj_l.
     rel_apply_l (FG_increment_atomic_l (issuedTickets γ)%I True%I); first done.
     iAlways.
@@ -306,13 +305,13 @@ Section refinement.
     REL release << reloc.lib.lock.release : lockInt → ().
   Proof.
     iApply refines_arrow_val; [done|done|].
-    iAlways. iIntros (? ?) "/= #Hl".
-    iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
+    iAlways. iIntros (? lk) "/= #Hl".
+    iDestruct "Hl" as (lo ln γ) "(% & Hin)". simplify_eq.
     rel_rec_l. rel_proj_l.
     pose (R := fun (o : nat) =>
-                 (∃ (n : nat) (b : bool), ln ↦ #n
-                 ∗ issuedTickets γ n ∗ l' ↦ₛ #b
-                 ∗ if b then ticket γ o else True)%I).
+                 (∃ (n : nat) st, ln ↦ #n
+                 ∗ issuedTickets γ n ∗ is_lock_r lk st ∗
+                 if st then True else ticket γ o)%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 0e85fbb4951d618d1b63496d5813024986d6a7fd..bc5d4ef7f614f8bac93faeddc1001892d8c920d8 100644
--- a/theories/lib/counter.v
+++ b/theories/lib/counter.v
@@ -32,12 +32,12 @@ Definition FG_counter : val := λ: <>,
 Section CG_Counter.
   Context `{relocG Σ}.
 
-  Lemma CG_increment_r K E t A (x l : loc) (n : nat) :
+  Lemma CG_increment_r K E t A (x : loc) (lk : val) (n : nat) :
     nclose specN ⊆ E →
-    (x ↦ₛ # n -∗ l ↦ₛ #false -∗
-    (x ↦ₛ # (n + 1) -∗ l ↦ₛ #false -∗
+    (x ↦ₛ # n -∗ is_lock_r lk Unlocked_r -∗
+    (x ↦ₛ # (n + 1) -∗ is_lock_r lk Unlocked_r -∗
       (REL t << fill K (of_val #n) @ E : A)) -∗
-    REL t << fill K (CG_increment #x #l) @ E : A)%I.
+    REL t << fill K (CG_increment #x lk) @ E : A)%I.
   Proof.
     iIntros (?) "Hx Hl Hlog".
     rel_rec_r.
@@ -140,17 +140,17 @@ Section CG_Counter.
 
   Definition counterN : namespace := nroot .@ "counter".
 
-  Definition counter_inv l cnt cnt' : iProp Σ :=
-    (∃ n : nat, l ↦ₛ #false ∗ cnt ↦ #n ∗ cnt' ↦ₛ #n)%I.
+  Definition counter_inv lk cnt cnt' : iProp Σ :=
+    (∃ n : nat, is_lock_r lk Unlocked_r ∗ cnt ↦ #n ∗ cnt' ↦ₛ #n)%I.
 
-  Lemma FG_CG_increment_refinement l cnt cnt' :
-    inv counterN (counter_inv l cnt cnt') -∗
-    REL FG_increment #cnt << CG_increment #cnt' #l : lrel_int.
+  Lemma FG_CG_increment_refinement lk cnt cnt' :
+    inv counterN (counter_inv lk cnt cnt') -∗
+    REL FG_increment #cnt << CG_increment #cnt' lk : lrel_int.
   Proof.
     iIntros "#Hinv".
     rel_apply_l
       (FG_increment_atomic_l
-              (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I
+              (fun n => is_lock_r lk Unlocked_r ∗ cnt' ↦ₛ #n)%I
               True%I); first done.
     iAlways. iInv counterN as ">Hcnt" "Hcl". iModIntro.
     iDestruct "Hcnt" as (n) "(Hl & Hcnt & Hcnt')".
@@ -168,14 +168,14 @@ Section CG_Counter.
       rel_values.
   Qed.
 
-  Lemma counter_read_refinement l cnt cnt' :
-    inv counterN (counter_inv l cnt cnt') -∗
+  Lemma counter_read_refinement lk cnt cnt' :
+    inv counterN (counter_inv lk cnt cnt') -∗
     REL counter_read #cnt << counter_read #cnt' : lrel_int.
   Proof.
     iIntros "#Hinv".
     rel_apply_l
       (counter_read_atomic_l
-         (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I
+         (fun n => is_lock_r lk Unlocked_r ∗ 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 26ba9dfe5c3db72b640141f23fd7e7209d3597dd..d0e60e843f9e22c3042356ddfd64ff4733859094 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -2,6 +2,7 @@ From reloc Require Export reloc.
 From iris.algebra Require Import excl.
 Set Default Proof Using "Type".
 
+
 Definition newlock : val := λ: <>, ref #false.
 Definition acquire : val := rec: "acquire" "x" :=
   if: CAS "x" #false #true
@@ -109,40 +110,50 @@ 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.
+
   Lemma refines_newlock_r K t A
     (Hcl : nclose specN ⊆ E) :
-    (∀ l : loc, l ↦ₛ #false -∗ REL t << fill K (of_val #l) @ E : A) -∗
+    (∀ v, is_lock_r v Unlocked_r -∗ REL t << fill K (of_val v) @ E : A) -∗
     REL t << fill K (newlock #()) @ E : A.
   Proof.
     iIntros "Hlog".
     rel_rec_r.
     rel_alloc_r l as "Hl".
-    iApply ("Hlog" with "Hl").
+    iApply ("Hlog" with "[Hl]").
+    iExists _. by iFrame.
   Qed.
 
-  Lemma refines_acquire_r K l t A
+  Lemma refines_acquire_r K v t A
     (Hcl : nclose specN ⊆ E) :
-    l ↦ₛ #false -∗
-    (l ↦ₛ #true -∗ REL t << fill K (of_val #()) @ E : A) -∗
-    REL t << fill K (acquire #l) @ E : A.
+    is_lock_r v Unlocked_r -∗
+    (is_lock_r v Locked_r -∗ REL t << fill K (of_val #()) @ E : A) -∗
+    REL t << fill K (acquire v) @ E : A.
   Proof.
     iIntros "Hl Hlog".
+    iDestruct "Hl" as (lk ->) "Hl".
     rel_rec_r.
-    rel_cas_suc_r. simpl.
+    rel_cas_suc_r.
     rel_if_r.
-    by iApply "Hlog".
+    iApply "Hlog". iExists _. by iFrame.
   Qed.
 
-  Lemma refines_release_r K l t A (b : bool)
+  Lemma refines_release_r K v t A st
     (Hcl : nclose specN ⊆ E) :
-    l ↦ₛ #b -∗
-    (l ↦ₛ #false -∗ REL t << fill K (of_val #()) @ E : A) -∗
-    REL t << fill K (release #l) @ E : A.
+    is_lock_r v st -∗
+    (is_lock_r v Unlocked_r -∗ REL t << fill K (of_val #()) @ E : A) -∗
+    REL t << fill K (release v) @ E : A.
   Proof.
     iIntros "Hl Hlog".
+    iDestruct "Hl" as (lk ->) "Hl".
     rel_rec_r.
     rel_store_r.
-    by iApply "Hlog".
+    iApply "Hlog". iExists _. by iFrame.
   Qed.
 
 End lock_rules_r.