A logically atomic specification for FG_increment

F_mu_ref_conc/examples/counter.v

@@ -164,7 +164,7 @@ Section CG_Counter.
     Unshelve. all: trivial.
   Qed.
   
-  Lemma bin_log_related_CG_locked_increment Γ K E1 E2 t τ x n l :
+  Lemma bin_log_related_CG_locked_increment_r Γ K E1 E2 t τ x n l :
     nclose specN ⊆ E1 →
     (x ↦ₛ (#nv n) -∗ l ↦ₛ (#♭v false) -∗
     (x ↦ₛ (#nv S n) -∗ l ↦ₛ (#♭v false) -∗
@@ -275,6 +275,7 @@ Section CG_Counter.
     iIntros "Hx Hlog".
     iApply bin_log_related_bind_l.
     { autosubst. }
+    Transparent FG_increment.
     iApply wp_rec; auto. iNext.
     change (Rec
           (App
@@ -394,13 +395,68 @@ Section CG_Counter.
   Definition counter_inv l cnt cnt' : iProp Σ :=
     (∃ n, l ↦ₛ (#♭v false) ∗ cnt ↦ᵢ (#nv n) ∗ cnt' ↦ₛ (#nv n))%I.
 
+  (* A logically atomic specification for
+     a fine-grained increment with a baked in frame. *)
+  (* Unfortunately, the precondition is not baked in the rule so you can only use it when your spatial context is empty *)
+  Lemma bin_log_FG_increment_logatomic R Γ E1 E2 K x t τ  :
+    □ (|={E1,E2}=> ∃ n, x ↦ᵢ (#nv n) ∗ R(n) ∗
+       ((∃ n, x ↦ᵢ (#nv n) ∗ R(n)) ={E2,E1}=∗ True) ∧
+        (∀ m, x ↦ᵢ (#nv (S m)) ∗ R(m) -∗ 
+            {E2,E1;Γ} ⊨ fill K Unit ≤log≤ t : τ))
+    -∗ ({E1,E1;Γ} ⊨ fill K (App (FG_increment (Loc x)) Unit) ≤log≤ t : τ).
+  Proof.
+    iIntros "#H".
+    iLöb as "IH".   
+    iApply (bin_log_related_rec_l _ _ K); auto. iNext.
+    fold (FG_increment (Loc x)).
+    Opaque FG_increment. simpl. asimpl.
+    rewrite FG_increment_closed; auto.
+    rel_bind_l (Load (Loc x)). rewrite -fill_app.
+    iPoseProof "H" as "H2". (* lolwhat *)    
+    Opaque bin_log_related.
+    iApply (bin_log_related_load_l).
+    iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
+    iExists (#nv n). iFrame. iSplit; eauto.
+    iIntros "Hx".
+    rewrite ->uPred.and_elim_l.
+    iApply fupd_logrel.
+    iMod ("Hrev" with "[HR Hx]").
+    { iExists _. iFrame. } iModIntro.
+    rewrite fill_app /=. iApply (bin_log_related_rec_l); auto. asimpl.
+    rewrite FG_increment_closed; auto.
+    iNext.
+    rel_bind_l (BinOp _ _ _). rewrite -fill_app.
+    iApply (bin_log_related_binop_l). iNext. rewrite fill_app /=.
+    rel_bind_l (CAS _ _ _). rewrite -fill_app.
+    iApply (bin_log_related_cas_l); auto.
+    iMod "H2" as (n') "[Hx [HR HQ]]". iModIntro.
+    rewrite ?fill_app /=.
+    destruct (decide (n = n')); subst.
+    - iExists (#nv n'). iFrame. 
+      iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
+      iIntros "_ Hx". simpl.
+      rewrite ->uPred.and_elim_r.
+      iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
+      iApply (bin_log_related_if_true_masked_l _ _ _ K); auto.   
+    - iExists (#nv n'). iFrame. 
+      iSplitL; eauto; last first.
+      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
+      iIntros "_ Hx". simpl.
+      iApply (bin_log_related_if_false_masked_l _ _ _ K); auto.   
+      rewrite ->uPred.and_elim_l.
+      iMod ("HQ" with "[Hx HR]").
+      { iExists _; iFrame. }      
+      iApply "IH".
+  Qed.    
+
   Lemma FG_CG_increment_refinement l cnt cnt' Γ :
     inv counterN (counter_inv l cnt cnt') -∗
     Γ ⊨ FG_increment (Loc cnt) ≤log≤ CG_locked_increment (Loc cnt') (Loc l) : (TArrow TUnit TUnit).
   Proof.
     iIntros "#Hinv".
     Transparent CG_locked_increment with_lock.
-    unfold FG_increment, CG_locked_increment, with_lock.
+    Transparent FG_increment.
+    unfold CG_locked_increment, with_lock.
     iApply (bin_log_related_arrow); auto.
     iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ. simpl.
      (* fold this stuff back *)
@@ -419,72 +475,26 @@ Section CG_Counter.
                      (BinOp Add (#n 1) (Var 1))) Unit
                   (App (Var 2) (Var 3)))) (Load (Loc cnt))))
     with (FG_increment (Loc cnt)).
-    iLöb as "Hlat".
-    iApply (bin_log_related_rec_l _ _ []); auto. iNext. asimpl.
-    rel_bind_l (Load (Loc cnt)).
-    iApply (bin_log_related_load_l).
-    iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". iModIntro.
-    iExists (#nv n). iSplit; eauto. iFrame "Hcnt".
-    iIntros "Hcnt". simpl.
-    iMod ("Hclose" with "[Hl Hcnt Hcnt']").
-    { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
-    iApply (bin_log_related_rec_l _ _ []); auto. iNext. asimpl.
-    rel_bind_l (BinOp Add (#n 1) (#n n)).
-    iApply (bin_log_related_binop_l). iNext. simpl.
-    rel_bind_l (CAS (Loc cnt) (#n n) (#n (S n))).
-    iApply (bin_log_related_cas_l); auto. 
-    iInv counterN as (m) "[>Hl [Hcnt >Hcnt']]" "Hclose". 
-    iModIntro. 
-    iExists (#nv m). iFrame "Hcnt".
-    destruct (decide (n = m)).
-    + (* CAS succeeds *) subst. iSplitR; eauto.
-      { iDestruct 1 as %Hfoo. by exfalso. }
-      iIntros "_ Hcnt". simpl.
-      iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl");
-        auto. solve_ndisj.
-      iIntros "Hcnt' Hl". 
-      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
-      { iNext. iExists (S m). iFrame. }
-      iApply (bin_log_related_if_true_l _ _ []); auto.
-      iNext. simpl.
-      iPoseProof (bin_log_related_unit [] ⊤) as "H".
-      iExact "H". (* TODO iApply does not work *)
-    + (* CAS fails *)
-      iSplitL; eauto; last first.
-      { iDestruct 1 as %Hfoo. injection Hfoo. intro. by exfalso. }
-      iIntros "_ Hcnt". simpl.
-      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
-      { iNext. iExists m. iFrame. }
-      iApply (bin_log_related_if_false_l [] []); auto.      
-    (* iApply (bin_log_related_bind_l []); auto. *)
-    (* iApply wp_rec; auto. iNext. simpl. *)
-    (* wp_bind (Load _). *)
-    (* iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose".  *)
-    (* iApply (wp_load with "Hcnt"). *)
-    (* iNext. iIntros "Hcnt". simpl. *)
-    (* iMod ("Hclose" with "[Hl Hcnt Hcnt']"). *)
-    (* { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". } *)
-    (* iApply wp_rec; auto. iNext. simpl. *)
-    (* wp_bind (BinOp _ _ _). *)
-    (* iApply (wp_nat_binop). iNext. iModIntro. *)
-    (* wp_bind (CAS _ _ _). *)
-    (* iInv counterN as (m) "[>Hl [Hcnt >Hcnt']]" "Hclose".  *)
-    (* destruct (decide (n = m)). *)
-    (* + (* CAS succeeds *) subst. *)
-    (*   iApply (wp_cas_suc with "Hcnt"); auto. *)
-    (*   iNext. iIntros "Hcnt".  *)
-    (*   iApply wp_if_true. iApply wp_value; auto. *)
-    (*   iApply fupd_mono. *)
-    (*   { iApply uPred.later_intro. } *)
-    (*   iApply fupd_frame_r. *)
-    (*   iApply (uPred.sep_mono_r _ (cnt' ↦ₛ (#nv m) *)
-    (*          ∗ l ↦ₛ (#♭v false)                           *)
-    (*          ∗ []  ⊨ Unit ≤log≤ Unit : TUnit)%I). *)
-    (*   { simpl. iIntros "[Hcnt' [Hl Hlog]]". *)
-    (*     iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl"); auto. } *)
-    (*   i. *)
+    Opaque FG_increment.
+    iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]").
+    iAlways.
+    iInv counterN as ">Hcnt" "Hcl". iModIntro.
+    iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
+    iExists n. iFrame. clear n.
+    iSplit. 
+    - iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]".
+      iMod ("Hcl" with "[-]").
+      { iNext. iExists _. iFrame. }
+      done.
+    - iIntros (m) "[Hcnt [Hl Hcnt']]".
+      iApply (bin_log_related_CG_locked_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj.  }
+      iIntros "Hcnt' Hl".
+      iMod ("Hcl" with "[-]").
+      { iNext. iExists _. iFrame. }
+      simpl.
+      iApply bin_log_related_unit.
       Opaque CG_locked_increment with_lock.
-  Qed.    
+  Qed.
 
   Lemma FG_CG_counter_refinement :
     [] ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat).

F_mu_ref_conc/relational_properties.v

@@ -34,19 +34,19 @@ Section properties.
     iMod "HP". iApply ("HI" with "HP").
   Qed.
   
-  Lemma bin_log_related_val Γ τ e e' v v'
+  Lemma bin_log_related_val Γ E τ e e' v v'
     (Hclosed : ∀ f, e.[f] = e)
     (Hclosed' : ∀ f, e'.[f] = e') :
     to_val e = Some v →
     to_val e' = Some v' →
-    (∀ Δ, ⟦ τ ⟧ Δ (v, v')) ⊢ Γ ⊨ e ≤log≤ e' : τ.
+    (∀ Δ, |={E}=> ⟦ τ ⟧ Δ (v, v')) ⊢ {E,E;Γ} ⊨ e ≤log≤ e' : τ.
   Proof.
     iIntros (Hv Hv') "IH".
     iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     rewrite Hclosed Hclosed'.
+    iMod ("IH" $! Δ) as "IH".
     iModIntro. iApply wp_value; eauto.
     iExists v'. rewrite (of_to_val e' v' _); auto.
-    iFrame. iApply ("IH" $! Δ).
   Qed.
 
   (** ** Reductions on the left *)
@@ -72,7 +72,29 @@ Section properties.
     iApply wp_bind_inv. iApply fupd_wp. 
     iApply (fupd_mask_mono E); auto. 
   Qed.
-  
+
+  Lemma bin_log_pure_masked_l Γ E1 E2 K' τ (e e' : expr) t
+    (Hclosed : ∀ f, e.[f] = e)
+    (Hclosed' : ∀ f, e'.[f] = e')
+    (Hsafe : ∀ σ, head_reducible e σ) :
+    to_val e = None ->
+    (∀ σ1 e2 σ2 efs, head_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ [] = efs) →
+    {E1,E2;Γ} ⊨ fill K' e' ≤log≤ t : τ
+    ⊢ {E1,E2;Γ} ⊨ fill K' e ≤log≤ t : τ.
+  Proof.
+    iIntros (Hval Hstep) "IH".
+    iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
+    rewrite fill_subst Hclosed.
+    iApply (wp_bind (subst_ctx (env_subst (vvs.*1)) K')). 
+    iMod ("IH" with "* Hs [HΓ] * Hj") as "IH"; auto. 
+    iModIntro.    
+    iApply wp_lift_pure_det_head_step_no_fork; eauto.
+    iNext. 
+    rewrite fill_subst.
+    rewrite -{2}(Hclosed' (env_subst (vvs.*1))).
+    iApply wp_bind_inv. done.
+  Qed.
+ 
   Lemma bin_log_related_fst_l Γ K e v1 v2 τ
    (Hclosed1 : ∀ f, (of_val v1).[f] = (of_val v1))
    (Hclosed2 : ∀ f, (of_val v2).[f] = (of_val v2)) :
@@ -240,6 +262,32 @@ Section properties.
       end. done.
   Qed.
 
+  Lemma bin_log_related_if_true_masked_l Γ E1 E2 (K : list ectx_item) (e1 e2 : expr) t τ
+   (Hclosed1 : ∀ f, e1.[f] = e1) 
+   (Hclosed2 : ∀ f, e2.[f] = e2) :
+   ({E1,E2;Γ} ⊨ fill K e1 ≤log≤ t : τ)
+   ⊢ {E1,E2;Γ} ⊨ (fill K (If (#♭ true) e1 e2)) ≤log≤ t : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_masked_l with "Hlog"); auto.
+    - intros; simpl; by rewrite Hclosed1 Hclosed2.
+    - do 3 eexists. econstructor; eauto. 
+    - by inversion 1.
+  Qed.
+
+  Lemma bin_log_related_if_false_masked_l Γ E1 E2 (K : list ectx_item) (e1 e2 : expr) t τ
+   (Hclosed1 : ∀ f, e1.[f] = e1) 
+   (Hclosed2 : ∀ f, e2.[f] = e2) :
+   ({E1,E2;Γ} ⊨ fill K e2 ≤log≤ t : τ)
+   ⊢ {E1,E2;Γ} ⊨ (fill K (If (#♭ false) e1 e2)) ≤log≤ t : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_masked_l with "Hlog"); auto.
+    - intros; simpl; by rewrite Hclosed1 Hclosed2.
+    - do 3 eexists. econstructor; eauto. 
+    - by inversion 1.
+  Qed.
+  
   Lemma bin_log_related_binop_l Γ E K op a b t τ :
    ▷ ({E,E;Γ} ⊨ fill K (of_val (binop_eval op a b)) ≤log≤ t : τ)
    ⊢ {E,E;Γ} ⊨ (fill K (BinOp op (#n a) (#n b))) ≤log≤ t : τ.