Merge branch 'master' into onemask

theories/examples/counter.v

@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
 From iris_logrel Require Export logrel.
 From iris_logrel.examples Require Import lock.
 
-Definition CG_increment : val := λ: "x" "l" <>,
+Definition CG_increment : val := λ: "x" "l",
   acquire "l";;
   let: "n" := !"x" in
   "x" <- #1 + "n";;
@@ -14,17 +14,17 @@ Definition counter_read : val := λ: "x" <>, !"x".
 Definition CG_counter : val := λ: <>,
   let: "l" := newlock #() in
   let: "x" := ref #0 in
-  (CG_increment "x" "l", counter_read "x").
+  ((λ: <>, CG_increment "x" "l"), counter_read "x").
 
-Definition FG_increment : val := λ: "v", rec: "inc" <> :=
+Definition FG_increment : val := rec: "inc" "v" :=
   let: "c" := !"v" in
   if: CAS "v" "c" (#1 + "c")
   then "c"
-  else "inc" #().
+  else "inc" "v".
 
 Definition FG_counter : val := λ: <>,
   let: "x" := ref #0 in
-  (FG_increment "x", counter_read "x").
+  ((λ: <>, FG_increment "x"), counter_read "x").
 
 Section CG_Counter.
   Context `{logrelG Σ}.
@@ -32,7 +32,7 @@ Section CG_Counter.
 
   (* Coarse-grained increment *)  
   Lemma CG_increment_type Γ :
-    typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType (TArrow TUnit TNat))).
+    typed Γ CG_increment (TArrow (Tref TNat) (TArrow LockType TNat)).
   Proof. solve_typed. Qed.
 
   Hint Resolve CG_increment_type : typeable.
@@ -42,11 +42,11 @@ Section CG_Counter.
     (x ↦ₛ # n -∗ l ↦ₛ #false -∗
     (x ↦ₛ # (S n) -∗ l ↦ₛ #false -∗
       ({E;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ)) -∗
-    {E;Δ;Γ} ⊨ t ≤log≤ fill K ((CG_increment $/ (LitV (Loc x)) $/ LitV (Loc l)) #()) : τ)%I.
+    {E;Δ;Γ} ⊨ t ≤log≤ fill K (CG_increment #x #l) : τ)%I.
   Proof.
     iIntros (?) "Hx Hl Hlog".
     unfold CG_increment. unlock. simpl_subst/=.
-    rel_seq_r.
+    repeat rel_rec_r.
     rel_apply_r (bin_log_related_acquire_r with "Hl"); eauto.
     iIntros "Hl".
     rel_rec_r.
@@ -87,7 +87,7 @@ Section CG_Counter.
 
   (* Fine-grained increment *)
   Lemma FG_increment_type Γ :
-    typed Γ FG_increment (TArrow (Tref TNat) (TArrow TUnit TNat)).
+    typed Γ FG_increment (TArrow (Tref TNat) TNat).
   Proof. solve_typed. Qed.
 
   Hint Resolve FG_increment_type : typeable.
@@ -97,7 +97,7 @@ Section CG_Counter.
     (x ↦ₛ # n -∗
     (x ↦ₛ #(S n) -∗
       {E;Δ;Γ} ⊨ t ≤log≤ fill K #n : τ) -∗
-    {E;Δ;Γ} ⊨ t ≤log≤ fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
+    {E;Δ;Γ} ⊨ t ≤log≤ fill K (FG_increment #x) : τ)%I.
   Proof.
     iIntros (?) "Hx Hlog".
     unlock FG_increment. simpl_subst/=.
@@ -129,7 +129,7 @@ Section CG_Counter.
        ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E,⊤}=∗ True) ∧
         (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ P -∗
             {E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ))
-    -∗ ({Δ;Γ} ⊨ fill K ((FG_increment $/ LitV (Loc x)) #()) ≤log≤ t : τ).
+    -∗ ({Δ;Γ} ⊨ fill K (FG_increment #x) ≤log≤ t : τ).
   Proof.
     iIntros "HP #H".
     iLöb as "IH".
@@ -187,22 +187,9 @@ Section CG_Counter.
 
   Lemma FG_CG_increment_refinement l cnt cnt' Γ :
     inv counterN (counter_inv l cnt cnt') -∗
-    {Δ;Γ} ⊨ FG_increment #cnt ≤log≤ CG_increment #cnt' #l : TArrow TUnit TNat.
+    {Δ;Γ} ⊨ FG_increment #cnt ≤log≤ CG_increment #cnt' #l : TNat.
   Proof.
     iIntros "#Hinv".
-    rel_rec_l.
-    unlock CG_increment.
-    do 2 rel_rec_r.
-    replace (λ: <>, acquire #l;; let: "n" := ! #cnt' in #cnt' <- #1 + "n";; release #l;; "n")%E
-        with (CG_increment $/ LitV (Loc cnt') $/ LitV (Loc l))%E; last first.
-    { unlock CG_increment. by simpl_subst/=. }
-    iApply bin_log_related_arrow_val.
-    { unfold FG_increment. unlock; simpl_subst. reflexivity. }
-    { unfold CG_increment. unlock; simpl_subst. reflexivity. }
-    { unfold FG_increment. unlock; simpl_subst/=. solve_closed. (* TODO: add a clause to the reflection mechanism that reifies a [lambdasubst] expression as a closed one *) }
-    { unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
-
-    iAlways. iIntros (v v') "[% %]"; simplify_eq/=.
     rel_apply_l
       (bin_log_FG_increment_logatomic
               (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I
@@ -279,7 +266,9 @@ Section CG_Counter.
     iMod (inv_alloc counterN with "[Hinv]") as "#Hinv"; trivial.
 
     iApply bin_log_related_pair.
-    - iApply (FG_CG_increment_refinement with "Hinv").
+    - iApply bin_log_related_arrow; eauto.
+      iAlways. iIntros (??) "_". rel_seq_l; rel_seq_r.
+      iApply (FG_CG_increment_refinement with "Hinv").
     - iApply (counter_read_refinement with "Hinv").
   Qed.
 End CG_Counter.

theories/examples/generative.v

@@ -16,7 +16,7 @@ Definition nameGen1 : val :=
 
 Definition nameGen2 : expr :=
   let: "x" := ref #0 in
-  Pack (λ: <>, FG_increment "x" #();; !"x"
+  Pack (λ: <>, FG_increment "x";; !"x"
        ,λ: "y" "z", "y" = "z").
 
 Lemma nameGen1_typed Γ :
@@ -39,7 +39,6 @@ Proof.
   econstructor. cbn.
   econstructor. cbn. solve_typed.
   econstructor; eauto; solve_typed.
-  econstructor; eauto; solve_typed.
 Qed.
 Hint Resolve nameGen2_typed : typeable.
 
@@ -83,7 +82,6 @@ Section namegen_refinement.
       rel_alloc_l_atomic.
       iInv N as (n L) "(HB & Hc & HL)" "Hcl".
       iModIntro. iNext. iIntros (l') "Hl'".
-      rel_rec_r.
       rel_apply_r (bin_log_related_FG_increment_r with "Hc").
       { solve_ndisj. }
       iIntros "Hc".

theories/examples/ticket_lock.v

@@ -13,7 +13,7 @@ Definition newlock : val :=
   λ: <>, ((* owner *) ref #0, (* next *) ref #0).
 
 Definition acquire : val := λ: "lk",
-  let: "n" := FG_increment (Snd "lk") #() in
+  let: "n" := FG_increment (Snd "lk") in
   wait_loop "n" "lk".
 
 Definition wkincr : val := λ: "l",
@@ -35,7 +35,6 @@ Proof.
   econstructor; cbn; solve_typed.
   econstructor; cbn; solve_typed.
   econstructor; cbn; solve_typed.
-  econstructor; cbn; solve_typed.
 Qed.
 
 Hint Resolve acquire_type : typeable.
@@ -71,10 +70,6 @@ Section refinement.
   Definition ticket (γ : gname) (n : nat) := own γ (◯ GSet {[ n ]}).
   (** total number of issued tickets is `n` *)
   Definition issuedTickets (γ : gname) (n : nat) := own γ (● GSet (seq_set 0 n)).
-  (** the locks `(ln, lo)` and `l'` are linked together in the pool `γP` *)
-  Definition inPool (γP : gname) (lo ln : loc) (γ : gname) (l' : loc) := own γP (◯ {[(lo, ln, γ), l']}).
-  (** the set `P` is in fact the lock pool associated with `γP` *)
-  Definition isPool (γP : gname) (P : lockPool) := own γP (● P).
 
   Lemma ticket_nondup γ n : ticket γ n -∗ ticket γ n -∗ False.
   Proof.
@@ -99,52 +94,12 @@ Section refinement.
     by iFrame.
   Qed.
 
-  Instance inPool_persistent γP lo ln γ l' : Persistent (inPool γP lo ln γ l').
-  Proof. apply _. Qed.
-
-  Lemma inPool_lookup γP lo ln γ l' P :
-    inPool γP lo ln γ l' -∗ isPool γP P -∗
-    ⌜(lo, ln, γ, l') ∈ P⌝.
-  Proof.
-    iIntros "Hrs Ho".
-    iDestruct (own_valid_2 with "Ho Hrs") as %Hfoo.
-    iPureIntro.
-    apply auth_valid_discrete in Hfoo.
-    simpl in Hfoo. destruct Hfoo as [Hfoo _].
-    revert Hfoo. rewrite left_id.
-    by rewrite gset_included elem_of_subseteq_singleton.
-  Qed.
-
-  Lemma isPool_insert γP lo ln γ l' P :
-    isPool γP P ==∗
-    inPool γP lo ln γ l' ∗ isPool γP ({[(lo, ln, γ, l')]} ∪ P).
-  Proof.
-    iIntros "HP".
-    iMod (own_update with "HP") as "[HP Hls]".
-    { eapply auth_update_alloc.
-      eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} ∪ P)).
-      apply union_subseteq_r. }
-    iFrame "HP".
-    rewrite -gset_op_union.
-    by iDestruct "Hls" as "[#Hls _]".
-  Qed.
-
-  Lemma newIsPool (P : lockPool) : (|==> ∃ γP, isPool γP P)%I.
-  Proof.
-    apply (own_alloc (● (P : lockPoolR))).
-    by apply auth_auth_valid.
-  Qed.
-
-  Instance isPool_timeless γP P : Timeless (isPool γP P).
-  Proof. apply _. Qed.
-  Instance inPool_timeless γP lo ln γ l' : Timeless (inPool γP lo ln γ l').
-  Proof. apply _. Qed.
   Instance ticket_timeless γ n : Timeless (ticket γ n).
   Proof. apply _. Qed.
   Instance issuedTickets_timeless γ n : Timeless (issuedTickets γ n).
   Proof. apply _. Qed.
 
-  Opaque ticket issuedTickets inPool isPool.
+  Opaque ticket issuedTickets.
 
   (** * Invariants and abstracts for them *)
   Definition lockInv (lo ln : loc) (γ : gname) (l' : loc) : iProp Σ :=
@@ -157,84 +112,28 @@ Section refinement.
   Instance lockInv_timeless lo ln γ l' : Timeless (lockInv lo ln γ l').
   Proof. apply _. Qed.
 
-  Definition lockPoolInv (P : lockPool) : iProp Σ :=
-    ([∗ set] rs ∈ P, match rs with
-                     | ((lo, ln, γ), l') => lockInv lo ln γ l'
-                     end)%I.
-
-  Instance lockPoolInv_timeless P : Timeless (lockPoolInv P).
-  Proof.
-    apply big_sepS_timeless.
-    intros [[[? ?] ?] ?]. apply _.
-  Qed.
-
-  Lemma lockPoolInv_empty : lockPoolInv ∅.
-  Proof. by rewrite /lockPoolInv big_sepS_empty. Qed.
-
-  Lemma lockPool_open γP (P : lockPool) (lo ln : loc) (γ : gname) (l' : loc) :
-    isPool γP P -∗
-    inPool γP lo ln γ l' -∗
-    lockPoolInv P -∗
-    isPool γP P ∗ (lockInv lo ln γ l') ∗ (lockInv lo ln γ l' -∗ lockPoolInv P).
-  Proof.
-    iIntros "HP #Hin HPinv".
-    iDestruct (inPool_lookup with "Hin HP") as %Hin.
-    rewrite /lockPoolInv.
-    iDestruct (big_sepS_elem_of_acc _ P _ with "HPinv") as "[Hrs Hreg]"; first apply Hin.
-    by iFrame.
-  Qed.
-
-  Lemma lockPool_insert γP (P : lockPool) (lo ln : loc) γ l' :
-    isPool γP P -∗
-    lockPoolInv P -∗
-    lockInv lo ln γ l' ==∗
-    isPool γP ({[(lo, ln, γ, l')]} ∪ P)
-    ∗ lockPoolInv ({[(lo, ln, γ, l')]} ∪ P)
-    ∗ inPool γP lo ln γ l'.
-  Proof.
-    iIntros "HP HPinv".
-    iDestruct 1 as (n o b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
-    iMod (isPool_insert γP lo ln γ l' P with "HP") as "[$ $]".
-    rewrite /lockInv.
-    iAssert (⌜(lo, ln, γ, l') ∈ P⌝ → False)%I as %Hbaz.
-    { iIntros (HP).
-      rewrite /lockPoolInv.
-      rewrite (big_sepS_elem_of _ P _ HP).
-      iDestruct "HPinv" as (? ? ?) "(Hlo' & Hln' & ?)".
-      iDestruct (mapsto_valid_2 with "Hlo' Hlo") as %Hfoo.
-      compute in Hfoo; contradiction. }
-    rewrite /lockPoolInv.
-    rewrite big_sepS_insert; last assumption.
-    iFrame. iExists _,_,_. by iFrame.
-  Qed.
-
-  Opaque lockPoolInv.
-
-  Definition moduleInv γp : iProp Σ :=
-    (∃ (P : lockPool), isPool γp P ∗ lockPoolInv P)%I.
+  Definition N := logrelN.@"locked".
 
-  Program Definition lockInt (γp : gname) := λne vv,
+  Program Definition lockInt := λne vv,
     (∃ (lo ln : loc) (γ : gname) (l' : loc),
         ⌜vv.1 = (#lo, #ln)%V⌝ ∗ ⌜vv.2 = #l'⌝
-      ∗ inPool γp lo ln γ l')%I.
+      ∗ inv N (lockInv lo ln γ l'))%I.
   Next Obligation. solve_proper. Qed.
   
-  Instance lockInt_persistent γp ww : Persistent (lockInt γp ww).
+  Instance lockInt_persistent ww : Persistent (lockInt ww).
   Proof. apply _. Qed.
 
   (** * Refinement proofs *)
-  Definition N := logrelN.@"locked".
 
-  Local Ltac openI N := iInv N as (P) ">[HP HPinv]" "Hcl".
+  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).
+    first by (iNext; iExists _,_,_; iFrame).
 
   (* Allocating a new lock *)
-  Lemma newlock_refinement Δ Γ γp:
-    inv N (moduleInv γp) -∗
-    {(lockInt γp :: Δ); ⤉Γ} ⊨ newlock ≤log≤ lock.newlock : (Unit → TVar 0).
+  Lemma newlock_refinement Δ Γ:
+    {(lockInt:: Δ); ⤉Γ} ⊨ newlock ≤log≤ lock.newlock : (Unit → TVar 0).
   Proof.
-    iIntros "#Hinv".
     unlock newlock.
     iApply bin_log_related_arrow_val; eauto.
     { by unlock lock.newlock. }
@@ -248,51 +147,42 @@ Section refinement.
     { solve_ndisj. }
     iIntros (l') "Hl'".
     (* Establishing the invariant *)
-    openI N.
     iMod newIssuedTickets as (γ) "Hγ".
-    iMod (lockPool_insert _ _ lo ln with "HP HPinv [Hlo Hln Hl' Hγ]") as "(HP & HPinv & #Hin)".
-    { iExists _,_,_; by iFrame. }
-    closeI.
-    rel_vals; iModIntro; iAlways.
-    iExists _,_,_,_. by iFrame "Hin".
+    iMod (inv_alloc N _ (lockInv lo ln γ l') with "[-]") as "#Hinv".
+    { iNext. iExists _,_,_. iFrame. }
+    rel_vals. iModIntro. iAlways.
+    iExists _,_,_,_. iFrame "Hinv". eauto.
   Qed.
 
   (* Acquiring a lock *)
   (* helper lemma *)
-  Lemma wait_loop_refinement Δ Γ γp (lo ln : loc) γ (l' : loc) (m : nat) :
-    inv N (moduleInv γp) -∗
-    inPool γp lo ln γ l' -∗ (* two locks are linked *)
+  Lemma wait_loop_refinement Δ Γ (lo ln : loc) γ (l' : loc) (m : nat) :
+    inv N (lockInv lo ln γ l') -∗
     ticket γ m -∗
-    {(lockInt γp :: Δ); ⤉Γ} ⊨
+    {(lockInt :: Δ); ⤉Γ} ⊨
       wait_loop #m (#lo, #ln) ≤log≤ lock.acquire #l' : TUnit.
   Proof.
-    iIntros "#Hinv #Hin Hticket".
+    iIntros "#Hinv Hticket".
     rel_rec_l.
     iLöb as "IH".
     unlock {2}wait_loop. simpl.
     rel_let_l. rel_proj_l.
     rel_load_l_atomic.
-    openI N.
-    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
-    rewrite {1}/lockInv.
-    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hrest)".
+    openI.
     iModIntro. iExists _; iFrame; iNext.
     iIntros "Hlo".
     rel_op_l.
     case_decide; subst; rel_if_l.
     (* Whether the ticket is called out *)
     - destruct b.
-      { iDestruct (ticket_nondup with "Hticket Hrest") as %[]. }
+      { iDestruct (ticket_nondup with "Hticket Hbticket") as %[]. }
       rel_apply_r (bin_log_related_acquire_r with "Hl'").
       { solve_ndisj. }
       iIntros "Hl'".
-      iSpecialize ("HPinv" with "[Hlo Hln Hl' Hissued Hticket]").
-      { iExists _,_,_. by iFrame. }
       closeI.
       iApply bin_log_related_unit.
     - iMod ("Hcl" with "[-Hticket]") as "_".
-      { iNext. iExists P; iFrame.
-        iApply "HPinv". iExists _,_,_; by iFrame. }
+      { iNext. iExists _,_,_; by iFrame. }
       rel_rec_l.
       unlock wait_loop. simpl_subst/=. by iApply "IH".
   Qed.
@@ -314,8 +204,6 @@ Section refinement.
     iIntros "HP #H".
     rewrite /acquire. unlock. simpl.
     rel_rec_l. rel_proj_l.
-    rel_bind_l ((FG_increment #ln) #())%E.
-    rel_rec_l.
     rel_apply_l (bin_log_FG_increment_logatomic _ (fun n : nat => ∃ o : nat, lo ↦ᵢ #o ∗ issuedTickets γ n ∗ R o)%I P%I with "HP").
     iAlways.
     iPoseProof "H" as "H2".
@@ -355,11 +243,9 @@ Section refinement.
         rel_rec_l. iApply ("IH" with "HP Hm").
   Qed.
 
-  Lemma acquire_refinement Δ Γ γp :
-    inv N (moduleInv γp) -∗
-    {(lockInt γp :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
+  Lemma acquire_refinement Δ Γ :
+    {lockInt :: Δ; ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
   Proof.
-    iIntros "#Hinv".
     iApply bin_log_related_arrow_val; eauto.
     { by unlock acquire. }
     { by unlock lock.acquire. }
@@ -371,20 +257,16 @@ Section refinement.
                              if b then ticket γ o else True)%I
                    True%I γ); first done.
     iAlways.
-    openI N.
-    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
-    rewrite {1}/lockInv.
-    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
+    openI.
     iModIntro. iExists _,_; iFrame.
-    iSplitL "Hticket Hl'".
+    iSplitL "Hbticket Hl'".
     { iExists _. iFrame. }
     clear b o n.
     iSplit.
     - iDestruct 1 as (o' n') "(Hlo & Hln & Hissued & Hrest)".
       iDestruct "Hrest" as (b) "[Hl' Ht]".
       iApply ("Hcl" with "[-]").
-      iNext. iExists P; iFrame.
-      iApply "HPinv". iExists _,_,_. by iFrame.
+      iNext. iExists _,_,_. by iFrame.
     - iIntros (o n) "(Hlo & Hln & Hissued & Ht & Hrest) _".
       iDestruct "Hrest" as (b) "[Hl' Ht']".
       destruct b.
@@ -393,42 +275,31 @@ Section refinement.
       { solve_ndisj. }
       iIntros "Hl'".
       iMod ("Hcl" with "[-]") as "_".
-      { iNext. iExists P; iFrame.
-        iApply "HPinv". iExists _,_,_; by iFrame. }
+      { iNext. iExists _,_,_; by iFrame. }
       iApply bin_log_related_unit.
   Qed.
 
-  Lemma acquire_refinement_direct Δ Γ γp :
-    inv N (moduleInv γp) -∗
-    {(lockInt γp :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
+  Lemma acquire_refinement_direct Δ Γ :
+    {(lockInt :: Δ); ⤉Γ} ⊨ acquire ≤log≤ lock.acquire : (TVar 0 → Unit).
   Proof.
-    iIntros "#Hinv".
     unlock acquire; simpl.
     iApply bin_log_related_arrow_val; eauto.
     { by unlock lock.acquire. }
     iAlways. iIntros (? ?) "/= #Hl".
     iDestruct "Hl" as (lo ln γ l') "(% & % & Hin)". simplify_eq.
     rel_let_l. repeat rel_proj_l.
-    (* rel_rec_l. (* TODO: cannot find the reduct *) *)
-    rel_bind_l (FG_increment _ #()).
-    rel_rec_l.
     rel_apply_l (bin_log_FG_increment_logatomic _ (issuedTickets γ)%I True%I); first done.
     iAlways.
-    openI N.
-    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
-    rewrite {1}/lockInv.
-    iDestruct "Hls" as (o n b) "(Hlo & Hln & Hissued & Hl' & Hticket)".
+    openI.
     iModIntro. iExists _; iFrame.
     iSplit.
     - iDestruct 1 as (m) "[Hln ?]".
       iApply ("Hcl" with "[-]").
-      iNext. iExists P; iFrame.
-      iApply "HPinv". iExists _,_,_; by iFrame.
+      iNext. iExists _,_,_; by iFrame.
     - iIntros (m) "[Hln Hissued] _".
       iMod (issueNewTicket with "Hissued") as "[Hissued Hm]".
       iMod ("Hcl" with "[-Hm]") as "_".
-      { iNext. iExists P; iFrame.
-        iApply "HPinv". iExists _,_,_; by iFrame. }
+      { iNext. iExists _,_,_; by iFrame. }
       rel_let_l.
       by iApply wait_loop_refinement.
   Qed.
@@ -476,11 +347,9 @@ Section refinement.
     iExists _; iFrame.
   Qed.
 
-  Lemma release_refinement Δ Γ γp :
-    inv N (moduleInv γp) -∗
-    {(lockInt γp :: Δ); ⤉Γ} ⊨ release ≤log≤ lock.release : (TVar 0 → Unit).
+  Lemma release_refinement Δ Γ :
+    {(lockInt :: Δ); ⤉Γ} ⊨ release ≤log≤ lock.release : (TVar 0 → Unit).
   Proof.
-    iIntros "#Hinv".
     unlock release.
     iApply bin_log_related_arrow_val; eauto.
     { by unlock lock.release. }
@@ -493,19 +362,15 @@ Section refinement.
                  ∗ if b then ticket γ o else True)%I).
     rel_apply_l (wkincr_atomic_l R True%I); first done.
     iAlways.
-    openI N.
-    iDestruct (lockPool_open with "HP Hin HPinv") as "(HP & Hls & HPinv)".
-    rewrite {1}/lockInv.
-    iDestruct "Hls" as (o n b) "(Hlo & Hrest)".
+    openI.
     iModIntro. iExists _; iFrame.
-    rewrite {1}/R. iSplitL "Hrest".
-    { iExists _,_; iFrame. } clear o n b.
+    rewrite {1}/R. iSplitR "Hcl".
+    { iExists _,_; by iFrame. } clear o n b.
     iSplit.
     - iDestruct 1 as (o) "[Hlo HR]".
       unfold R. iDestruct "HR" as (n b) "HR".
       iApply "Hcl".
-      iNext. iExists P; iFrame.
-      iApply "HPinv". iExists _,_,_; by iFrame.
+      iNext. iExists _,_,_; by iFrame.
     - iIntros (?) "[Hlo HR] _".
       iDestruct "Hlo" as (o) "Hlo".
       unfold R. iDestruct "HR" as (n b) "(Hln & Hissued & Hl' & Hticket)".
@@ -513,8 +378,7 @@ Section refinement.
       { solve_ndisj. }
       iIntros "Hl'".
       iMod ("Hcl" with "[-]") as "_".
-      { iNext. iExists P; iFrame.
-        iApply "HPinv". iExists _,_,_. by iFrame. }
+      { iNext. iExists _,_,_. by iFrame. }
       iApply bin_log_related_unit.
   Qed.
 
@@ -524,13 +388,10 @@ Section refinement.
         Pack (lock.newlock, lock.acquire, lock.release) : lockT.
   Proof.
     iIntros (Δ).
-    iMod (newIsPool ∅) as (γp) "HP".
-    iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv".
-    { iNext. iExists _; iFrame. iApply lockPoolInv_empty. }
-    iApply (bin_log_related_pack (lockInt γp)).
+    iApply (bin_log_related_pack lockInt).
     repeat iApply bin_log_related_pair.
     - by iApply newlock_refinement.
-    - by iApply acquire_refinement.
+    - by iApply acquire_refinement_direct.
     - by iApply release_refinement.
   Qed.
 

theories/examples/various.v

@@ -360,7 +360,7 @@ Section refinement.
   Definition τg := TArrow TUnit TUnit.
   Definition τf := TArrow τg TUnit.
   Definition p : val := λ: "g", let: "c" := ref #0 in
-                                (λ: <>, FG_increment "c" #();; "g" #(), λ: <>, !"c").
+                                (λ: <>, FG_increment "c";; "g" #(), λ: <>, !"c").
   (** The idea for the invariant is that we have to states:
        a) c1 = n, c2 = n
        b) c1 = n+1, c2 = n
@@ -378,16 +378,15 @@ Section refinement.
     inv shootN (i6 c1 c2 γ γ') -∗
     ⟦ τg ⟧ Δ (g1, g2) -∗
     {Δ;Γ} ⊨
-      (FG_increment #c1 #() ;; g1 #())
+      (FG_increment #c1;; g1 #())
     ≤log≤
-      (FG_increment #c2 #() ;; g2 #()) : TUnit.
+      (FG_increment #c2;; g2 #()) : TUnit.
   Proof.
     iIntros "#Hinv #Hg".
     iApply (bin_log_related_seq TRV _ _ _ _ _ _ (TVar 0)); auto; last first.
     { iApply (bin_log_related_app _ _ _ _ _ _ TUnit).
       iApply bin_log_related_val; eauto using to_of_val.
       iApply bin_log_related_unit. }
-    rel_rec_l.
     rel_apply_l (bin_log_FG_increment_logatomic _
       (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I True%I); first done.
     iAlways.
@@ -404,7 +403,6 @@ Section refinement.
           iFrame. }
       { iIntros (m) "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
-          rel_rec_r;
           (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
           iIntros "Hc2".
         - iMod ("Hcl" with "[-]") as "_".
@@ -428,7 +426,6 @@ Section refinement.
           iFrame. }
       { iIntros (m) "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
-          rel_rec_r;
           (rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
           iIntros "Hc2".
         - iMod ("Hcl" with "[-]") as "_".
@@ -445,9 +442,9 @@ Section refinement.
     inv shootN (i6 c1 c2 γ γ') -∗
     ⟦ τg ⟧ Δ (g1, g2) -∗
     {Δ;Γ} ⊨
-      (λ: <>, FG_increment #c1 #() ;; g1 #())
+      (λ: <>, FG_increment #c1;; g1 #())
     ≤log≤
-      (λ: <>, FG_increment #c2 #() ;; g2 #()) : τg.
+      (λ: <>, FG_increment #c2;; g2 #()) : τg.
   Proof.
     iIntros "#Hinv #Hg".
     iApply bin_log_related_arrow_val; auto.
@@ -478,10 +475,10 @@ Section refinement.
       ∨ c2 ↦ₛ #(m - 1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ m⌝) -∗
     own γ' (Excl ()) -∗
     {⊤ ∖ ↑shootN;Δ;Γ} ⊨
-      (g1 #() ;; f'1 (λ: <>, (FG_increment #c1) #() ;; g1 #()) ;; #() ;; ! #c1)
+      (g1 #() ;; f'1 (λ: <>, (FG_increment #c1);; g1 #()) ;; #() ;; ! #c1)
     ≤log≤
       (g2 #() ;;
-       f'2 (λ: <>, (FG_increment #c2) #() ;; g2 #()) ;; (#() ;; ! #c2) + #1) : TNat.
+       f'2 (λ: <>, (FG_increment #c2);; g2 #()) ;; (#() ;; ! #c2) + #1) : TNat.
   Proof.
     iIntros "#Hinv #Hg #Hf Hcl Hc1 Hc2 Ht".
     iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first.
@@ -555,7 +552,6 @@ Section refinement.
       iApply bin_log_related_val; eauto using to_of_val.
       by iApply profiled_g'. }
     rel_seq_l.
-    rel_bind_l (FG_increment _). rel_rec_l.
     rel_apply_l (bin_log_FG_increment_logatomic _
       (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I with "Ht'").
     iAlways.

theories/tests/liftings.v

@@ -56,7 +56,7 @@ Section liftings.
       (fun (n : nat) => x ↦ᵢ #n)%I
       (fun (n : nat) (v : val) => ⌜v = #n⌝ ∗ x ↦ᵢ #(S n))%I
       E
-      ((FG_increment $/ LitV (Loc x)) #())
+      (FG_increment #x)
       Δ Γ.
   Proof.
     iIntros (K t τ R2 R1) "[HR2 #Hlog]".