Whitespace clean-up and abstraction removal.

theories/auth_excl.v

@@ -22,7 +22,6 @@ Proof. solve_inG. Qed.
 Definition to_auth_excl {A : Type} (a : A) : exclUR A :=
   Excl' (a: leibnizC A).
 
-
 Section auth_excl.
   Context `{!auth_exclG A Σ}.
 
@@ -39,7 +38,7 @@ Section auth_excl.
     iFrame.
     eauto.
   Qed.
-  
+
   Lemma excl_update γ x y z :
     own γ (● to_auth_excl y) -∗ own γ (◯  to_auth_excl x) ==∗
     own γ (● to_auth_excl z) ∗ own γ (◯  to_auth_excl z).

theories/channel.v

@@ -4,22 +4,18 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import proofmode notation.
 From iris.algebra Require Import excl auth.
 From iris.base_logic.lib Require Import auth.
-From iris.heap_lang.lib Require Import lock.
 From iris.heap_lang.lib Require Import spin_lock.
 From osiris Require Import list.
 From osiris Require Import auth_excl.
 Set Default Proof Using "Type".
 Import uPred.
 
-Definition new_list : val :=
-  λ: <>, lnil #().
-
-Definition new_chan : val := 
+Definition new_chan : val :=
   λ: <>,
-     let l := ref new_list #() in
-     let r := ref new_list #() in
-     let lk := newlock #() in
-     ((l,r),lk).
+     let: "l" := ref lnil #() in
+     let: "r" := ref lnil #() in
+     let: "lk" := newlock #() in
+     (("l","r"),"lk").
 
 Notation left := (#true) (only parsing).
 Notation right := (#false) (only parsing).
@@ -68,7 +64,7 @@ Section channel.
 
   Definition is_side (s : val) : Prop :=
     s = left ∨ s = right.
-  
+
   Record chan_name := Chan_name {
     chan_lock_name : gname;
     chan_l_name : gname;
@@ -78,7 +74,7 @@ Section channel.
   Definition chan_ctx (γ : chan_name) (c : val) : iProp Σ :=
     (∃ l r lk : val,
       ⌜c = ((l, r), lk)%V⌝ ∧
-      is_lock N (chan_lock_name γ) lk (∃ ls rs, 
+      is_lock N (chan_lock_name γ) lk (∃ ls rs,
         is_list_ref l ls ∗ own (chan_l_name γ) (● to_auth_excl ls) ∗
         is_list_ref r rs ∗ own (chan_r_name γ) (● to_auth_excl rs)))%I.
 
@@ -88,7 +84,8 @@ Section channel.
   Definition chan_frag (γ : chan_name) (c : val) (ls rs : list val) : iProp Σ :=
     (∃ l r lk : val,
       ⌜c = ((l, r), lk)%V⌝ ∧
-      own (chan_l_name γ) (◯ to_auth_excl ls) ∗ own (chan_r_name γ) (◯ to_auth_excl rs))%I.
+      own (chan_l_name γ) (◯ to_auth_excl ls) ∗
+      own (chan_r_name γ) (◯ to_auth_excl rs))%I.
 
   Global Instance chan_frag_timeless : Timeless (chan_frag γ c ls rs).
   Proof. by apply _. Qed.
@@ -100,32 +97,27 @@ Section channel.
     {{{ True }}}
       new_chan #()
     {{{ c γ, RET c; is_chan γ c [] [] }}}.
-  Proof. 
-    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_ctx /chan_frag /is_lock.
-    repeat wp_lam. wp_alloc lk as "Hlk".
-    iMod (own_alloc (Excl ())) as (lkγ) "Hγlk"; first done.
-    repeat wp_lam. wp_alloc r as "Hr".
-    iMod (own_alloc (Auth (Excl' (to_auth_excl [])) (to_auth_excl []))) as (lsγ) "Hls"; first done.
-    repeat wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (Auth (Excl' (to_auth_excl [])) (to_auth_excl []))) as (rsγ) "Hrs"; first done.
-    rewrite auth_both_op own_op own_op.
-    pose (Chan_name lkγ lsγ rsγ). 
-    iDestruct "Hls" as "[Hlsa Hlsf]".
-    iDestruct "Hrs" as "[Hrsa Hrsf]".
-    iMod (inv_alloc N _ (lock_inv lkγ lk (∃ (ls rs : list val), is_list_ref #l ls ∗ own lsγ (● to_auth_excl ls) ∗ is_list_ref #r rs ∗ own rsγ (● to_auth_excl rs)))%I with "[Hlk Hγlk Hr Hl Hlsa Hrsa]") as "Hlk".
-    {
-      rewrite /is_list_ref /is_list /lock_inv.
-      iNext. iExists _.
-      iSplitL "Hlk"=> //=.
-      iSplitL "Hγlk"=> //=.
-      iExists _, _. iFrame.      
-      iSplitL "Hl"=> //; iExists _, _; iSplit=> //; iFrame=> //. 
-    }
-    wp_pures.
-    iSpecialize ("HΦ" $!(#l, #r, #lk)%V c).
-    iApply ("HΦ").
-    iSplitR "Hlsf Hrsf"=> //;
-    eauto 10 with iFrame.
+  Proof.
+    iIntros (Φ) "_ HΦ". rewrite /is_chan /chan_ctx /chan_frag.
+    wp_lam.
+    wp_apply (lnil_spec with "[//]"); iIntros (ls Hls). wp_alloc l as "Hl".
+    wp_apply (lnil_spec with "[//]"); iIntros (rs Hrs). wp_alloc r as "Hr".
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
+      as (lsγ) "[Hls Hls']"; first done.
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
+      as (rsγ) "[Hrs Hrs']"; first done.
+    iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
+    { rewrite /is_list_ref; eauto. }
+    iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
+    { rewrite /is_list_ref; eauto. }
+    wp_apply (newlock_spec N (∃ ls rs,
+      is_list_ref #l ls ∗ own lsγ (● to_auth_excl ls) ∗
+      is_list_ref #r rs ∗ own rsγ (● to_auth_excl rs))%I
+                with "[Hl Hr Hls Hrs]").
+    { eauto 10 with iFrame. }
+    iIntros (lk γlk) "#Hlk". wp_pures.
+    iApply ("HΦ" $! _ (Chan_name γlk lsγ rsγ)).
+    eauto 20 with iFrame.
   Qed.
 
   Definition chan_frag_snoc γ c ls rs s v : iProp Σ :=
@@ -227,7 +219,8 @@ Section channel.
         iDestruct (excl_eq with "Hrsa Hrsf") as %->.
         iSpecialize ("HΦ" $!(InjLV #())).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_fail /chan_frag. eauto 10 with iFrame. } 
+        { rewrite /try_recv_upd /try_recv_upd_fail /chan_frag.
+          eauto 10 with iFrame. }
         iModIntro.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
         { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
@@ -244,7 +237,8 @@ Section channel.
         iDestruct (excl_update _ _ _ (rs) with "Hrsa Hrsf") as ">[Hrsa Hrsf]".
         iSpecialize ("HΦ" $!(InjRV (v))).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_succ /chan_frag. eauto 10 with iFrame. }
+        { rewrite /try_recv_upd /try_recv_upd_succ /chan_frag.
+          eauto 10 with iFrame. }
         iModIntro.
         wp_store.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
@@ -264,7 +258,8 @@ Section channel.
         iDestruct (excl_eq with "Hrsa Hrsf") as %->.
         iSpecialize ("HΦ" $!(InjLV #())).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_fail /chan_frag. eauto 10 with iFrame. } 
+        { rewrite /try_recv_upd /try_recv_upd_fail /chan_frag.
+          eauto 10 with iFrame. }
         iModIntro.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").
         { rewrite /is_list_ref /is_list. eauto 10 with iFrame. }
@@ -281,7 +276,8 @@ Section channel.
         iDestruct (excl_update _ _ _ (ls) with "Hlsa Hlsf") as ">[Hlsa Hlsf]".
         iSpecialize ("HΦ" $!(InjRV (v))).
         iMod ("HΦ" with "[Hlsf Hrsf]") as "HΦ".
-        { rewrite /try_recv_upd /try_recv_upd_succ /chan_frag. eauto 10 with iFrame. }
+        { rewrite /try_recv_upd /try_recv_upd_succ /chan_frag.
+          eauto 10 with iFrame. }
         iModIntro.
         wp_store.
         wp_apply (release_spec with "[-HΦ $Hlocked $Hlock]").

theories/logrel.v

@@ -2,18 +2,16 @@ From iris.proofmode Require Import tactics.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.heap_lang.lib Require Import lock.
 From iris.heap_lang.lib Require Import spin_lock.
 From osiris Require Import typing auth_excl channel.
 From iris.algebra Require Import list auth excl.
-From iris.base_logic Require Import invariants auth saved_prop.
-Require Import FunctionalExtensionality.
+From iris.base_logic Require Import invariants.
 
 Section logrel.
   Context `{!heapG Σ, !lockG Σ} (N : namespace).
   Context `{!auth_exclG (list val) Σ}.
   Context `{!auth_exclG stype Σ}.
-  
+
   Record st_name := SessionType_name {
     st_c_name : chan_name;
     st_l_name : gname;
@@ -43,15 +41,13 @@ Section logrel.
         st_eval (v::vs) st1 (TRecv P st2).
   Hint Constructors st_eval.
 
-  Lemma st_eval_send :
-    ∀ (P : val → Prop) (st : val → stype) (l : list val) (str : stype) (v : val),
+  Lemma st_eval_send (P : val -> Prop) st l str v :
       P v → st_eval l (TSend P st) str → st_eval (l ++ [v]) (st v) str.
   Proof.
-    intros P st l str v HP Heval.
-    generalize dependent str.
-    induction l; intros.
-    - inversion Heval; by constructor.
-    - inversion Heval; subst. simpl.
+    revert str.
+    induction l; intros str.
+    - inversion 2; by constructor.
+    - inversion 2; subst. simpl.
       constructor=> //.
       apply IHl=> //.
   Qed.
@@ -61,7 +57,7 @@ Section logrel.
       chan_frag (st_c_name γ) c l r ∗
       stmapsto_full γ stl Left  ∗
       stmapsto_full γ str Right ∗
-      ((⌜r = []⌝ ∗ ⌜st_eval l stl str⌝) ∨ 
+      ((⌜r = []⌝ ∗ ⌜st_eval l stl str⌝) ∨
        (⌜l = []⌝ ∗ ⌜st_eval r str stl⌝)))%I.
 
   Definition st_ctx (γ : st_name) (st : stype) (c : val) : iProp Σ :=
@@ -70,14 +66,14 @@ Section logrel.
   Definition st_frag  (γ : st_name) (st : stype) (s : side) : iProp Σ :=
     stmapsto_frag γ st s.
 
-  Definition interp_st (γ : st_name) (st : stype) (c : val) (s : side) : iProp Σ :=
+  Definition interp_st (γ : st_name) (st : stype)
+      (c : val) (s : side) : iProp Σ :=
     (st_frag γ st s ∗ st_ctx γ st c)%I.
 
   Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st γ sτ c s)
     (at level 10, s at next level, sτ at next level, γ at next level,
      format "⟦  c  @  s  :  sτ  ⟧{ γ }").
 
-  
   Lemma new_chan_vs st E c cγ :
     is_chan N cγ c [] [] ={E}=∗
       ∃ lγ rγ,
@@ -85,13 +81,12 @@ Section logrel.
         ⟦ c @ Left : st ⟧{γ} ∗ ⟦ c @ Right : dual_stype st ⟧{γ}.
   Proof.
     iIntros "[#Hcctx Hcf]".
-    iMod (own_alloc (Auth (Excl' (to_auth_excl st)) (to_auth_excl st))) as (lγ) "Hlst"; first done.
-    iMod (own_alloc (Auth (Excl' (to_auth_excl (dual_stype st))) (to_auth_excl (dual_stype st)))) as (rγ) "Hrst"; first done.
-    rewrite (auth_both_op (to_auth_excl st)). 
-    rewrite (auth_both_op (to_auth_excl (dual_stype st))). 
-    rewrite own_op own_op.
-    iDestruct "Hlst" as "[Hlsta Hlstf]".
-    iDestruct "Hrst" as "[Hrsta Hrstf]".
+    iMod (own_alloc (● (to_auth_excl st) ⋅
+                     ◯ (to_auth_excl st)))
+      as (lγ) "[Hlsta Hlstf]"; first done.
+    iMod (own_alloc (● (to_auth_excl (dual_stype st)) ⋅
+                     ◯ (to_auth_excl (dual_stype st))))
+      as (rγ) "[Hrsta Hrstf]"; first done.
     pose (SessionType_name cγ lγ rγ) as stγ.
     iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
     { iNext. rewrite /inv_st. eauto 10 with iFrame. }
@@ -100,11 +95,12 @@ Section logrel.
     iFrame. simpl.
     repeat iSplitL=> //.
   Qed.
-  
+
   Lemma new_chan_st_spec st :
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c;  ⟦ c @ Left : st ⟧{γ} ∗ ⟦ c @ Right : dual_stype st ⟧{γ} }}}.
+    {{{ c γ, RET c;  ⟦ c @ Left : st ⟧{γ} ∗
+                     ⟦ c @ Right : dual_stype st ⟧{γ} }}}.
   Proof.
     iIntros (Φ _) "HΦ".
     iApply (wp_fupd).
@@ -119,12 +115,12 @@ Section logrel.
     iFrame.
   Qed.
 
-Lemma send_vs c γ s (P : val → Prop) st E :
+  Lemma send_vs c γ s (P : val → Prop) st E :
     ↑N ⊆ E →
     ⟦ c @ s : TSend P st ⟧{γ} ={E,E∖↑N}=∗
       ∃ l r, chan_frag (st_c_name γ) c l r ∗
-      ▷ (∀ v, ⌜P v⌝ -∗ 
-              match s with 
+      ▷ (∀ v, ⌜P v⌝ -∗
+              match s with
               | Left  => chan_frag (st_c_name γ) c (l ++ [v]) r
               | Right => chan_frag (st_c_name γ) c l (r ++ [v])
               end ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).