From 6edb53e772f71859f4c4f0a57b12c04e7f45ca14 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Aug 2016 13:22:11 +0200
Subject: [PATCH] Some clean up/tweaks of locks.

---
 heap_lang/lib/lock.v        |  51 +++++-----
 heap_lang/lib/spin_lock.v   | 126 ++++++++++++-------------
 heap_lang/lib/ticket_lock.v | 183 ++++++++++++++++++------------------
 3 files changed, 176 insertions(+), 184 deletions(-)

diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 7b1bda1a0..0b764bb1a 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -1,32 +1,29 @@
-(** Abstract Lock Interface **)
-
 From iris.heap_lang Require Import heap notation.
 
-Structure lock Σ `{!heapG Σ} :=
-  Lock {
-      (* -- operations -- *)
-      newlock : val;
-      acquire : val;
-      release : val;
-      (* -- predicates -- *)
-      (* name is used to associate locked with is_lock *)
-      name: Type;
-      is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
-      locked (γ: name) : iProp Σ;
-      (* -- general properties -- *)
-      is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
-      is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
-      locked_timeless γ : TimelessP (locked γ);
-      locked_exclusive γ : locked γ ★ locked γ ⊢ False;
-      (* -- operation specs -- *)
-      newlock_spec N (R : iProp Σ) Φ :
-        heapN ⊥ N →
-        heap_ctx ★ R ★ (∀ l γ, is_lock N γ l R -★ Φ l) ⊢ WP newlock #() {{ Φ }};
-      acquire_spec N γ lk R (Φ : val → iProp Σ) :
-        is_lock N γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
-      release_spec N γ lk R (Φ : val → iProp Σ) :
-        is_lock N γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
-    }.
+Structure lock Σ `{!heapG Σ} := Lock {
+  (* -- operations -- *)
+  newlock : val;
+  acquire : val;
+  release : val;
+  (* -- predicates -- *)
+  (* name is used to associate locked with is_lock *)
+  name : Type;
+  is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
+  locked (γ: name) : iProp Σ;
+  (* -- general properties -- *)
+  is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
+  is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
+  locked_timeless γ : TimelessP (locked γ);
+  locked_exclusive γ : locked γ ★ locked γ ⊢ False;
+  (* -- operation specs -- *)
+  newlock_spec N (R : iProp Σ) Φ :
+    heapN ⊥ N →
+    heap_ctx ★ R ★ (∀ l γ, is_lock N γ l R -★ Φ l) ⊢ WP newlock #() {{ Φ }};
+  acquire_spec N γ lk R (Φ : val → iProp Σ) :
+    is_lock N γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }};
+  release_spec N γ lk R (Φ : val → iProp Σ) :
+    is_lock N γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}
+}.
 
 Arguments newlock {_ _} _.
 Arguments acquire {_ _} _.
diff --git a/heap_lang/lib/spin_lock.v b/heap_lang/lib/spin_lock.v
index 86547734e..870b48e8d 100644
--- a/heap_lang/lib/spin_lock.v
+++ b/heap_lang/lib/spin_lock.v
@@ -21,71 +21,65 @@ Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
 Section proof.
-Context `{!heapG Σ, !lockG Σ} (N : namespace).
-
-Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
-  (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
-
-Definition is_lock (γ: gname) (lk : val) (R : iProp Σ) : iProp Σ :=
-  (∃ (l: loc), heapN ⊥ N ∧ heap_ctx ∧ lk = #l ∧ inv N (lock_inv γ l R))%I.
-
-Definition locked (γ: gname): iProp Σ := own γ (Excl ())%I.
-
-Lemma locked_exclusive (γ: gname): (locked γ ★ locked γ ⊢ False)%I.
-Proof.
-  iIntros "[Hl Hl']". iCombine "Hl" "Hl'" as "Hl". by iDestruct (own_valid with "Hl") as %[].
-Qed.
-
-Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
-Proof. solve_proper. Qed.
-Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock γ l).
-Proof. solve_proper. Qed.
-(* Global Instance locked_ne n γ : Proper (dist n ==> dist n) (locked γ). *)
-(* Proof. solve_proper. Qed. *)
-
-(** The main proofs. *)
-Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
-Proof. apply _. Qed.
-
-(* Lemma locked_is_lock lk R : locked lk R ⊢ is_lock lk R. *)
-(* Proof. rewrite /is_lock. iDestruct 1 as (γ l) "(?&?&?&?&_)". iExists γ, l. auto. Qed. *)
-
-Global Instance locked_timeless γ : TimelessP (locked γ).
-Proof. apply _. Qed.
-
-Lemma newlock_spec (R : iProp Σ) Φ :
-  heapN ⊥ N →
-  heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
-Proof.
-  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
-  wp_seq. wp_alloc l as "Hl".
-  iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-  iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
-  { iIntros "!>". iExists false. by iFrame. }
-  iVsIntro. iApply "HΦ". iExists l. eauto.
-Qed.
-
-Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
-  is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
-Proof.
-  iIntros "[Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
-  iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
-  iInv N as ([]) "[Hl HR]" "Hclose".
-  - wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-    iVsIntro. wp_if. by iApply "IH".
-  - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
-    iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
-    iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). by iFrame.
-Qed.
-
-Lemma release_spec γ lk R (Φ : val → iProp Σ) :
-  is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
-Proof.
-  iIntros "(Hlock & Hlocked & HR & HΦ)". iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
-  rewrite /release. wp_let. iInv N as (b) "[Hl _]" "Hclose".
-  wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
-Qed.
+  Context `{!heapG Σ, !lockG Σ} (N : namespace).
+
+  Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
+    (∃ b : bool, l ↦ #b ★ if b then True else own γ (Excl ()) ★ R)%I.
+
+  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
+    (∃ l: loc, heapN ⊥ N ∧ heap_ctx ∧ lk = #l ∧ inv N (lock_inv γ l R))%I.
+
+  Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
+
+  Lemma locked_exclusive (γ : gname) : locked γ ★ locked γ ⊢ False.
+  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
+
+  Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
+  Proof. solve_proper. Qed.
+  Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock γ l).
+  Proof. solve_proper. Qed.
+
+  (** The main proofs. *)
+  Global Instance is_lock_persistent γ l R : PersistentP (is_lock γ l R).
+  Proof. apply _. Qed.
+  Global Instance locked_timeless γ : TimelessP (locked γ).
+  Proof. apply _. Qed.
+
+  Lemma newlock_spec (R : iProp Σ) Φ :
+    heapN ⊥ N →
+    heap_ctx ★ R ★ (∀ lk γ, is_lock γ lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+  Proof.
+    iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
+    wp_seq. wp_alloc l as "Hl".
+    iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
+    iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
+    { iIntros "!>". iExists false. by iFrame. }
+    iVsIntro. iApply "HΦ". iExists l. eauto.
+  Qed.
+
+  Lemma acquire_spec γ lk R (Φ : val → iProp Σ) :
+    is_lock γ lk R ★ (locked γ -★ R -★ Φ #()) ⊢ WP acquire lk {{ Φ }}.
+  Proof.
+    iIntros "[Hl HΦ]". iDestruct "Hl" as (l) "(% & #? & % & #?)". subst.
+    iLöb as "IH". wp_rec. wp_bind (CAS _ _ _)%E.
+    iInv N as ([]) "[Hl HR]" "Hclose".
+    - wp_cas_fail. iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+      iVsIntro. wp_if. by iApply "IH".
+    - wp_cas_suc. iDestruct "HR" as "[Hγ HR]".
+      iVs ("Hclose" with "[Hl]"); first (iNext; iExists true; eauto).
+      iVsIntro. wp_if. iApply ("HΦ" with "[-HR] HR"). by iFrame.
+  Qed.
+
+  Lemma release_spec γ lk R (Φ : val → iProp Σ) :
+    is_lock γ lk R ★ locked γ ★ R ★ Φ #() ⊢ WP release lk {{ Φ }}.
+  Proof.
+    iIntros "(Hlock & Hlocked & HR & HΦ)".
+    iDestruct "Hlock" as (l) "(% & #? & % & #?)". subst.
+    rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
+    wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
+  Qed.
 End proof.
 
-Definition spin_lock `{!heapG Σ, !lockG Σ} :=
-  Lock _ _ newlock acquire release gname is_lock locked _ _ _ locked_exclusive newlock_spec acquire_spec release_spec.
+Definition spin_lock `{!heapG Σ, !lockG Σ} : lock Σ :=
+  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
+     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 322c00cd9..9611cd2bb 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -4,7 +4,7 @@ From iris.program_logic Require Import auth.
 From iris.proofmode Require Import invariants.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import gset.
-From iris.heap_lang.lib Require Import lock.
+From iris.heap_lang.lib Require Export lock.
 Import uPred.
 
 Definition wait_loop: val :=
@@ -53,7 +53,7 @@ Section proof.
     (∃ (o n: nat),
        lo ↦ #o ★ ln ↦ #n ★
        auth_inv γ1 (tickets_inv n) ★
-       ((own γ2 (Excl ()) ★  R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
+       ((own γ2 (Excl ()) ★ R) ∨ auth_own γ1 (GSet {[ o ]})))%I.
 
   Definition is_lock (γs: gname * gname) (l: val) (R: iProp Σ) : iProp Σ :=
     (∃ (lo ln: loc),
@@ -68,7 +68,8 @@ Section proof.
 
   Definition locked (γs: gname * gname) : iProp Σ := own (snd γs) (Excl ())%I.
 
-  Global Instance lock_inv_ne n γ1 γ2 lo ln : Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
+  Global Instance lock_inv_ne n γ1 γ2 lo ln :
+    Proper (dist n ==> dist n) (lock_inv γ1 γ2 lo ln).
   Proof. solve_proper. Qed.
   Global Instance is_lock_ne γs n l : Proper (dist n ==> dist n) (is_lock γs l).
   Proof. solve_proper. Qed.
@@ -78,14 +79,13 @@ Section proof.
   Proof. apply _. Qed.
 
   Lemma locked_exclusive (γs: gname * gname) : (locked γs ★ locked γs ⊢ False)%I.
-  Proof.
-    iIntros "[Hl Hl']". iCombine "Hl" "Hl'" as "Hl". by iDestruct (own_valid with "Hl") as %[].
-  Qed.
+  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
 
   Lemma newlock_spec (R : iProp Σ) Φ :
-    heapN ⊥ N → heap_ctx ★ R ★ (∀ lk γs, is_lock γs lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
+    heapN ⊥ N →
+    heap_ctx ★ R ★ (∀ lk γs, is_lock γs lk R -★ Φ lk) ⊢ WP newlock #() {{ Φ }}.
   Proof.
-    iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock.
+    iIntros (HN) "(#Hh & HR & HΦ)". rewrite /newlock /=.
     wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
     iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
     iVs (own_alloc_strong (Auth (Excl' ∅) ∅) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
@@ -99,95 +99,96 @@ Section proof.
         by iFrame.
       + iLeft. by iFrame.
     - iVsIntro.
-      iSpecialize ("HΦ" $! (#lo, #ln)%V (γ1, γ2)). iApply "HΦ".
+      iApply ("HΦ" $! (#lo, #ln)%V (γ1, γ2)).
       iExists lo, ln.
       iSplit; by eauto.
   Qed.
 
-Lemma wait_loop_spec γs l x R (Φ : val → iProp Σ) :
-  issued γs l x R ★ (locked γs -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
-Proof.
-  iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
-  iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
-  iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
-  wp_load. destruct (decide (x = o)) as [->|Hneq].
-  - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
-    + iVs ("Hclose" with "[Hlo Hln Hainv Ht]").
-      { iNext. iExists o, n. iFrame. eauto. }
-      iVsIntro. wp_let. wp_op=>[_|[]] //.
-      wp_if. iVsIntro.
-      iApply ("HΦ" with "[-HR] HR"). eauto.
-    + iExFalso. iCombine "Ht" "Haown" as "Haown".
-      iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
-      set_solver.
-  - iVs ("Hclose" with "[Hlo Hln Ha]").
+  Lemma wait_loop_spec γs l x R (Φ : val → iProp Σ) :
+    issued γs l x R ★ (locked γs -★ R -★ Φ #()) ⊢ WP wait_loop #x l {{ Φ }}.
+  Proof.
+    iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #? & Ht)".
+    iLöb as "IH". wp_rec. subst. wp_let. wp_proj. wp_bind (! _)%E.
+    iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
+    wp_load. destruct (decide (x = o)) as [->|Hneq].
+    - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+      + iVs ("Hclose" with "[Hlo Hln Hainv Ht]").
+        { iNext. iExists o, n. iFrame. eauto. }
+        iVsIntro. wp_let. wp_op=>[_|[]] //.
+        wp_if. iVsIntro.
+        iApply ("HΦ" with "[-HR] HR"). eauto.
+      + iExFalso. iCombine "Ht" "Haown" as "Haown".
+        iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
+        set_solver.
+    - iVs ("Hclose" with "[Hlo Hln Ha]").
+      { iNext. iExists o, n. by iFrame. }
+      iVsIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
+      wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
+  Qed.
+
+  Lemma acquire_spec γs l R (Φ : val → iProp Σ) :
+    is_lock γs l R ★ (locked γs -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
+  Proof.
+    iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
+    iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
+    iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
+    wp_load. iVs ("Hclose" with "[Hlo Hln Ha]").
     { iNext. iExists o, n. by iFrame. }
-    iVsIntro. wp_let. wp_op=>[[/Nat2Z.inj //]|?].
-    wp_if. iApply ("IH" with "Ht"). by iExact "HΦ".
-Qed.
-
-Lemma acquire_spec γs l R (Φ : val → iProp Σ) :
-  is_lock γs l R ★ (locked γs -★ R -★ Φ #()) ⊢ WP acquire l {{ Φ }}.
-Proof.
-  iIntros "[Hl HΦ]". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
-  iLöb as "IH". wp_rec. wp_bind (! _)%E. subst. wp_proj.
-  iInv N as (o n) "[Hlo [Hln Ha]]" "Hclose".
-  wp_load. iVs ("Hclose" with "[Hlo Hln Ha]").
-  { iNext. iExists o, n. by iFrame. }
-  iVsIntro. wp_let. wp_proj. wp_op.
-  wp_bind (CAS _ _ _).
-  iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
-  destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
-  - wp_cas_suc.
-    iDestruct "Hainv" as (s) "[Ho %]"; subst.
-    iVs (own_update with "Ho") as "Ho".
-    { eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
-      rewrite elem_of_seq_set; omega. }
-    iDestruct "Ho" as "[Hofull Hofrag]".
-    iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
-    { rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
-      rewrite -(seq_set_S_union_L 0).
-      iNext. iExists o', (S n)%nat.
-      rewrite Nat2Z.inj_succ -Z.add_1_r.
-      iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
-    iVsIntro. wp_if.
-    iApply (wait_loop_spec γs (#lo, #ln)).
-    iSplitR "HΦ"; last by auto.
-    rewrite /issued /auth_own; eauto 10.
-  - wp_cas_fail.
-    iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
-    { iNext. iExists o', n'. by iFrame. }
-    iVsIntro. wp_if. by iApply "IH".
-Qed.
-
-Lemma release_spec γs l R (Φ : val → iProp Σ):
-  is_lock γs l R ★ locked γs ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
-Proof.
-  iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
-  iLöb as "IH". wp_rec. subst. wp_proj. wp_bind (! _)%E.
-  iInv N as (o n) "[Hlo [Hln Hr]]" "Hclose".
-  wp_load. iVs ("Hclose" with "[Hlo Hln Hr]").
-  { iNext. iExists o, n. by iFrame. }
-  iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
-  wp_proj. wp_op.
-  iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
-  destruct (decide (#o' = #o))%V as [[= ->%Nat2Z.inj ] | Hneq].
-  - wp_cas_suc.
-    iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
-    + iExFalso. iCombine "Hγ" "Ho" as "Ho".
-      iDestruct (own_valid with "#Ho") as %[].
-    + iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
-      { iNext. iExists (o + 1)%nat, n'%nat.
-        iFrame. rewrite Nat2Z.inj_add.
-        iFrame. iLeft; by iFrame. }
-      iVsIntro. by wp_if.
-  - wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
-    { iNext. iExists o', n'. by iFrame. }
-    iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
-Qed.
+    iVsIntro. wp_let. wp_proj. wp_op.
+    wp_bind (CAS _ _ _).
+    iInv N as (o' n') "[Hlo' [Hln' [Hainv Haown]]]" "Hclose".
+    destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
+    - wp_cas_suc.
+      iDestruct "Hainv" as (s) "[Ho %]"; subst.
+      iVs (own_update with "Ho") as "Ho".
+      { eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
+        rewrite elem_of_seq_set; omega. }
+      iDestruct "Ho" as "[Hofull Hofrag]".
+      iVs ("Hclose" with "[Hlo' Hln' Haown Hofull]").
+      { rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
+        rewrite -(seq_set_S_union_L 0).
+        iNext. iExists o', (S n)%nat.
+        rewrite Nat2Z.inj_succ -Z.add_1_r.
+        iFrame. iExists (GSet (seq_set 0 (S n))). by iFrame. }
+      iVsIntro. wp_if.
+      iApply (wait_loop_spec γs (#lo, #ln)).
+      iSplitR "HΦ"; last by auto.
+      rewrite /issued /auth_own; eauto 10.
+    - wp_cas_fail.
+      iVs ("Hclose" with "[Hlo' Hln' Hainv Haown]").
+      { iNext. iExists o', n'. by iFrame. }
+      iVsIntro. wp_if. by iApply "IH".
+  Qed.
+
+  Lemma release_spec γs l R (Φ : val → iProp Σ):
+    is_lock γs l R ★ locked γs ★ R ★ Φ #() ⊢ WP release l {{ Φ }}.
+  Proof.
+    iIntros "(Hl & Hγ & HR & HΦ)". iDestruct "Hl" as (lo ln) "(% & #? & % & #?)".
+    iLöb as "IH". wp_rec. subst. wp_proj. wp_bind (! _)%E.
+    iInv N as (o n) "[Hlo [Hln Hr]]" "Hclose".
+    wp_load. iVs ("Hclose" with "[Hlo Hln Hr]").
+    { iNext. iExists o, n. by iFrame. }
+    iVsIntro. wp_let. wp_bind (CAS _ _ _ ).
+    wp_proj. wp_op.
+    iInv N as (o' n') "[Hlo' [Hln' Hr]]" "Hclose".
+    destruct (decide (#o' = #o))%V as [[= ->%Nat2Z.inj ] | Hneq].
+    - wp_cas_suc.
+      iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
+      + iExFalso. iCombine "Hγ" "Ho" as "Ho".
+        iDestruct (own_valid with "#Ho") as %[].
+      + iVs ("Hclose" with "[Hlo' Hln' HR Hγ Hainv]").
+        { iNext. iExists (o + 1)%nat, n'%nat.
+          iFrame. rewrite Nat2Z.inj_add.
+          iFrame. iLeft; by iFrame. }
+        iVsIntro. by wp_if.
+    - wp_cas_fail. iVs ("Hclose" with "[Hlo' Hln' Hr]").
+      { iNext. iExists o', n'. by iFrame. }
+      iVsIntro. wp_if. by iApply ("IH" with "Hγ HR").
+  Qed.
 End proof.
 
 Typeclasses Opaque is_lock issued locked.
 
-Definition ticket_lock `{!heapG Σ, !tlockG Σ} :=
-  Lock _ _ newlock acquire release (gname * gname) is_lock locked _ _ _ locked_exclusive newlock_spec acquire_spec release_spec.
+Definition ticket_lock `{!heapG Σ, !tlockG Σ} : lock Σ :=
+  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
+     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.
-- 
GitLab