diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v index 465157c08718b966193cee75c58d1336071e2b5e..1ac17b28c439462d06f0b604a0f436047b4db653 100644 --- a/theories/examples/ticket_lock.v +++ b/theories/examples/ticket_lock.v @@ -117,21 +117,15 @@ Section refinement. Program Definition lockInt := λne vv, (∃ (lo ln : loc) (γ : gname) (l' : loc), ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝ - ∗ inv (N.@(lo,ln,l')) (lockInv lo ln γ l'))%I. + ∗ inv N (lockInv lo ln γ l'))%I. Next Obligation. solve_proper. Qed. - (* Program Definition lockInt (γp : gname) := λne vv, *) - (* (∃ (lo ln : loc) (γ : gname) (l' : loc), *) - (* ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝ *) - (* ∗ inPool γp lo ln γ l')%I. *) - (* Next Obligation. solve_proper. Qed. *) - Instance lockInt_persistent ww : Persistent (lockInt ww). Proof. apply _. Qed. (** * Refinement proofs *) - Local Ltac openI N := + Local Ltac openI := iInv N as (o n b) ">(Hlo & Hln & Hissued & Hl' & Hbticket)" "Hcl". Local Ltac closeI := iMod ("Hcl" with "[-]") as "_"; first by (iNext; iExists _,_,_; iFrame). @@ -154,7 +148,7 @@ Section refinement. iIntros (l') "Hl'". (* Establishing the invariant *) iMod newIssuedTickets as (γ) "Hγ". - iMod (inv_alloc (N.@(lo,ln,l')) _ (lockInv lo ln γ l') with "[-]") as "#Hinv". + iMod (inv_alloc N _ (lockInv lo ln γ l') with "[-]") as "#Hinv". { iNext. iExists _,_,_. iFrame. } rel_vals. iModIntro. iAlways. iExists _,_,_,_. iFrame "Hinv". eauto. @@ -163,7 +157,7 @@ Section refinement. (* Acquiring a lock *) (* helper lemma *) Lemma wait_loop_refinement Δ Γ (lo ln : loc) γ (l' : loc) (m : nat) : - inv (N.@(lo,ln,l')) (lockInv lo ln γ l') -∗ + inv N (lockInv lo ln γ l') -∗ ticket γ m -∗ {(lockInt :: Δ); ⤉Γ} ⊨ wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit. @@ -174,7 +168,7 @@ Section refinement. unlock {2}wait_loop. simpl. rel_let_l. rel_proj_l. rel_load_l_atomic. - openI (N.@(lo, ln, l')). + openI. iModIntro. iExists _; iFrame; iNext. iIntros "Hlo". rel_op_l. @@ -263,7 +257,7 @@ Section refinement. if b then ticket γ o else True)%I True%I γ); first done. iAlways. - openI (N.@(lo, ln, l')). + openI. iModIntro. iExists _,_; iFrame. iSplitL "Hbticket Hl'". { iExists _. iFrame. } @@ -296,7 +290,7 @@ Section refinement. rel_let_l. repeat rel_proj_l. rel_apply_l (bin_log_FG_increment_logatomic _ (issuedTickets γ)%I True%I); first done. iAlways. - openI (N.@(lo, ln, l')). + openI. iModIntro. iExists _; iFrame. iSplit. - iDestruct 1 as (m) "[Hln ?]". @@ -368,7 +362,7 @@ Section refinement. ∗ if b then ticket γ o else True)%I). rel_apply_l (wkincr_atomic_l R True%I); first done. iAlways. - openI (N.@(lo, ln, l')). + openI. iModIntro. iExists _; iFrame. rewrite {1}/R. iSplitR "Hcl". { iExists _,_; by iFrame. } clear o n b.