Clean up some proofs

- rename `bin_log_related_bind_l` to `bin_log_related_wp_l` - use `bin_log_related_wp_l` to simplify derived rules

Clean up some proofs
- rename `bin_log_related_bind_l` to `bin_log_related_wp_l` - use `bin_log_related_wp_l` to simplify derived rules
9b373cca · Dan Frumin · 2084cf74 · 9b373cca · 9b373cca
Commit 9b373cca authored Jul 19, 2017 by Dan Frumin
Hide whitespace changes
Inline Side-by-side

Showing with 42 additions and 117 deletions

F_mu_ref_conc/examples/counter.v F_mu_ref_conc/examples/counter.v +1 -5

F_mu_ref_conc/relational_properties.v F_mu_ref_conc/relational_properties.v +41 -112

No files found.
--- a/F_mu_ref_conc/examples/counter.v
+++ b/F_mu_ref_conc/examples/counter.v
@@ -14,7 +14,6 @@ Definition CG_locked_increment : val := λ: "x" "l" <>,
  acquire "l";;
  CG_increment "x" #();;
  release "l".
-  (* with_lock (λ: "l", CG_increment "x" "l") "l". *)

 Definition counter_read : val := λ: "x" <>, !"x".

@@ -35,9 +34,6 @@ Definition FG_counter : expr :=

 Section CG_Counter.
  Context `{heapIG Σ, cfgSG Σ}.
-
-  Notation D := (prodC valC valC -n> iProp Σ).
-  Implicit Types Δ : listC D.
  
  (* Coarse-grained increment *)
  Lemma CG_increment_type Γ :
@@ -217,7 +213,7 @@ Section CG_Counter.
    {E,E;Γ} ⊨ fill K (FG_increment (Loc x) Unit) ≤log≤ t : τ.
  Proof.
    iIntros "Hx Hlog".
-    iApply bin_log_related_bind_l.
+    iApply bin_log_related_wp_l.
    wp_bind (FG_increment #x).
    unfold FG_increment. unlock.
    iApply wp_rec; eauto. 

--- a/F_mu_ref_conc/relational_properties.v
+++ b/F_mu_ref_conc/relational_properties.v
@@ -289,25 +289,35 @@ Section properties.
  Qed.

  (** *** Stateful reductions *)
-  Lemma bin_log_related_step_l Φ Γ E K e1 e2 τ
-    (Hclosed1 : Closed ∅ e1) :
-    (|={E}=> WP e1 @ E {{ Φ }}) -∗
-    (∀ v, Φ v -∗ {E,E;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ) -∗
-    {E,E;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
+  Lemma bin_log_related_wp_l Γ E K e1 e2 τ
+   (Hclosed1 : Closed ∅ e1) :
+   (WP e1 @ E {{ v,
+     {E,E;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ }})%I -∗
+   {E,E;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
  Proof.
-    iIntros "He Hlog".
+    iIntros "He".
    iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
    rewrite /env_subst fill_subst /=.
-    iApply (wp_bind (subst_ctx _ K)).    
-    iMod "He". iModIntro.
+    rewrite Closed_subst_p_id. iModIntro.
+    iApply (wp_bind (subst_ctx _ K)).
    iApply (wp_mask_mono E); auto.
-    rewrite Closed_subst_p_id.
    iApply (wp_wand with "He").
    iIntros (v) "Hv".
-    iSpecialize ("Hlog" $! v with "Hv Hs [HΓ]"); first by iFrame.
-    iSpecialize ("Hlog" with "Hj"). simpl.
-    rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
    iApply fupd_wp. iApply (fupd_mask_mono E); auto.
+    iMod ("Hv" with "Hs [HΓ] Hj"); auto.
+    rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
+    done.
+  Qed.
+
+  Lemma bin_log_related_step_l Φ Γ E K e1 e2 τ
+    (Hclosed1 : Closed ∅ e1) :
+    (|={E}=> WP e1 @ E {{ Φ }}) -∗
+    (∀ v, Φ v -∗ {E,E;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ) -∗
+    {E,E;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
+  Proof.
+    iIntros "He Hlog".
+    iApply bin_log_related_wp_l.
+    iMod "He". by iApply (wp_wand with "He").
  Qed.
    
  Lemma bin_log_related_wp_atomic_l Γ (E1 E2 : coPset) K e1 e2 τ
@@ -333,26 +343,6 @@ Section properties.
    by iMod "Hlog".
  Qed.
  
-  Lemma bin_log_related_bind_l Γ E K e1 e2 τ
-   (Hclosed1 : Closed ∅ e1) :
-   (WP e1 @ E {{ v,
-     {E,E;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ }})%I -∗
-   {E,E;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
-  Proof.
-    iIntros "He".
-    iIntros (Δ vvs ρ) "#Hs #HΓ". iIntros (j K') "Hj /=".
-    rewrite /env_subst fill_subst /=.
-    rewrite Closed_subst_p_id. iModIntro.
-    iApply (wp_bind (subst_ctx _ K)).
-    iApply (wp_mask_mono E); auto.
-    iApply (wp_wand with "He").
-    iIntros (v) "Hv".
-    iApply fupd_wp. iApply (fupd_mask_mono E); auto.
-    iMod ("Hv" with "Hs [HΓ] Hj"); auto.
-    rewrite /env_subst fill_subst /=. rewrite of_val_subst_p.
-    done.
-  Qed.
-
  Lemma bin_log_related_step_atomic_l {A} (Φ : A → val → iProp Σ) Γ E1 E2 K e1 e2 τ
    (Hatomic : atomic e1)
    (Hclosed1 : Closed ∅ e1) :
@@ -395,13 +385,8 @@ Section properties.
   {E,E;Γ} ⊨ fill K (Fork e) ≤log≤ t : τ.
  Proof.
    iIntros "Hsafe Hlog".
-    pose (Φ:=(fun w => ⌜w = UnitV⌝)%I : val -> iProp Σ).
-    iApply (bin_log_related_step_l Φ with "[Hsafe]"); auto.
-    { cbv[Φ]. iModIntro.
-      iApply wp_fork. iNext. by iFrame "Hsafe".
-    }
-    iIntros (v) "%"; subst. simpl.
-    done.
+    iApply bin_log_related_wp_l.
+    iApply wp_fork. iNext. by iFrame "Hsafe".
  Qed.

  Lemma bin_log_related_alloc_l Γ E1 E2 K e v t τ
@@ -411,16 +396,9 @@ Section properties.
    -∗ {E1,E1;Γ} ⊨ fill K (Alloc e) ≤log≤ t : τ.
  Proof.
    iIntros "Hlog".
-    pose (Φ:=(fun (_ : unit) w => ∃ l, ⌜w = LocV l⌝ ∗ l ↦ᵢ v)%I).
-    iApply (bin_log_related_step_atomic_l Φ); auto.
+    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog". iModIntro. 
-    iExists ().
-    iSplitR "Hlog".
-    - iApply (wp_alloc _ _ v); auto. iNext. iIntros (l) "Hl".            
-      unfold Φ. eauto.
-    - iIntros (w).
-      iDestruct 1 as (l) "[% Hl]"; subst. simpl.
-      iApply ("Hlog" $! l with "Hl").
+    iApply (wp_alloc _ _ v); auto.
  Qed.

  Lemma bin_log_related_alloc_l' Γ E K e v t τ
@@ -439,16 +417,9 @@ Section properties.
    -∗ {E1,E1;Γ} ⊨ fill K (Load (Loc l)) ≤log≤ t : τ.
  Proof.
    iIntros "Hlog".
-    pose (Φ:=(fun v' w => ⌜w = v'⌝ ∗ l ↦ᵢ v')%I).
-    iApply (bin_log_related_step_atomic_l Φ); auto.
+    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
-    iExists v'.
-    iSplitL "Hl".
-    - iApply (wp_load with "Hl"). iNext. iIntros "Hl".
-      iSplit; eauto.
-    - iIntros (v).
-      iDestruct 1 as "[% Hl]"; subst.
-      iApply "Hlog". done.
+    iApply (wp_load with "Hl"); auto.
  Qed.

  Lemma bin_log_related_load_l' Γ E1 K l v' t τ :
@@ -470,18 +441,10 @@ Section properties.
    -∗ {E1,E1;Γ} ⊨ fill K (Store (Loc l) e) ≤log≤ t : τ.
  Proof.
    iIntros (?) "Hlog".
-    pose (Φ:=(fun (_ : unit) w => ⌜w = UnitV⌝ ∗ l ↦ᵢ v')%I).
-    iApply (bin_log_related_step_atomic_l Φ); auto.
-    iMod "Hlog" as (v) "[Hl Hlog]". iModIntro. 
-    iExists ().
-    iSplitR "Hlog".
-    - iApply (wp_store _ _ _ _ v' with "Hl"); auto. 
-      iNext. iIntros "Hl".      
-      iSplit; eauto.      
-    - iIntros (w).
-      iDestruct 1 as "[% Hl]"; subst. simpl.
-      iApply ("Hlog" with "Hl").
-  Qed.
+    iApply bin_log_related_wp_atomic_l; auto.
+    iMod "Hlog" as (v) "[Hl Hlog]". iModIntro.
+    iApply (wp_store _ _ _ _ v' with "Hl"); auto.
+  Qed.    

  Lemma bin_log_related_store_l' Γ E K l e v v' t τ :
    (to_val e = Some v') →
@@ -503,33 +466,15 @@ Section properties.
    -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
  Proof.
    iIntros (??) "Hlog".
-    pose (Φ:=(fun v' w => (⌜v' ≠ v1⌝ -∗ ⌜w = BoolV false⌝ ∗ l ↦ᵢ v') ∗
-                        (⌜v' = v1⌝ -∗ ⌜w = BoolV true⌝ ∗ l ↦ᵢ v2))%I).
-    iApply (bin_log_related_step_atomic_l Φ); auto.
+    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog" as (v') "[Hl [Hlog_fail Hlog_suc]]". iModIntro. 
    destruct (decide (v' = v1)).
    - (* CAS successful *) subst.      
-      iExists v1.
-      iSplitR "Hlog_suc".
-      + iApply (wp_cas_suc with "Hl"); eauto. 
-        iNext. iIntros "Hl".      
-        unfold Φ. iSplitR; eauto.        
-        iDestruct 1 as %Hfoo. by exfalso. 
-      + iIntros (w).
-        iDestruct 1 as "[_ HΦ]"; subst. simpl.
-        iDestruct ("HΦ" with "[]") as "[% Hl]"; auto; subst.
-        iSpecialize ("Hlog_suc" with "[] Hl"); auto.
+      iApply (wp_cas_suc with "Hl"); eauto. 
+      iNext. by iApply "Hlog_suc".
    - (* CAS failed *)
-      iExists v'.
-      iSplitR "Hlog_fail".
-      + iApply (wp_cas_fail with "Hl"); eauto. 
-        iNext. iIntros "Hl".      
-        unfold Φ. iSplitL; eauto.
-        iDestruct 1 as %Hfoo. by exfalso.
-      + iIntros (w).
-        iDestruct 1 as "[HΦ _]"; subst. simpl.
-        iDestruct ("HΦ" with "[]") as "[% Hl]"; auto; subst.
-        iApply ("Hlog_fail" with "[] Hl"); auto.
+      iApply (wp_cas_fail with "Hl"); eauto. 
+      iNext. by iApply "Hlog_fail".
  Qed.

  Lemma bin_log_related_cas_fail_l Γ E1 E2 K l e1 e2 v1 v2 t τ :
@@ -540,17 +485,9 @@ Section properties.
    -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
  Proof.
    iIntros (??) "Hlog".
-    pose (Φ:=(fun v' w => ⌜w = BoolV false⌝ ∗ l ↦ᵢ v')%I).
-    iApply (bin_log_related_step_atomic_l Φ); auto.
+    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog" as (v') "[Hl [% Hlog]]". iModIntro. 
-    iExists v'.
-    iSplitR "Hlog".
-    - iApply (wp_cas_fail with "Hl"); eauto. 
-      iNext. iIntros "Hl".      
-      iSplit; eauto.
-    - iIntros (w).
-      iDestruct 1 as "[% Hl]"; subst. simpl.
-      iApply ("Hlog" with "Hl").
+    iApply (wp_cas_fail with "Hl"); eauto.
  Qed.
  
  Lemma bin_log_related_cas_fail_l' Γ E K l e1 e2 v1 v2 v' t τ :
@@ -574,17 +511,9 @@ Section properties.
    -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
  Proof.  
    iIntros (??) "Hlog".
-    pose (Φ:=(fun (_ : unit) w => ⌜w = BoolV true⌝ ∗ l ↦ᵢ v2)%I).
-    iApply (bin_log_related_step_atomic_l Φ); auto.
+    iApply bin_log_related_wp_atomic_l; auto.
    iMod "Hlog" as "[Hl Hlog]". iModIntro. 
-    iExists ().
-    iSplitR "Hlog".
-    - iApply (wp_cas_suc with "Hl"); eauto. 
-      iNext. iIntros "Hl".      
-      unfold Φ. eauto.
-    - iIntros (w).
-      iDestruct 1 as "[% Hl]"; subst. simpl.
-      iApply ("Hlog" with "Hl").
+    iApply (wp_cas_suc with "Hl"); eauto.
  Qed.

  Lemma bin_log_related_cas_suc_l' Γ E K l e1 e2 v1 v2 v' t τ :