Generalize the logatomic rule for the counter increment

theories/examples/counter.v

@@ -123,14 +123,15 @@ Section CG_Counter.
   (* 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 τ  :
+  Lemma bin_log_FG_increment_logatomic R P Γ E1 E2 K x t τ  :
+    P -∗
     □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R n ∗
        ((∃ n : nat, x ↦ᵢ #n ∗ R n) ={E2,E1}=∗ True) ∧
-        (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ 
+        (∀ m, x ↦ᵢ # (S m) ∗ R m -∗ P -∗
             {E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ))
     -∗ ({E1,E1;Δ;Γ} ⊨ fill K ((FG_increment $/ LitV (Loc x)) #()) ≤log≤ t : τ).
   Proof.
-    iIntros "#H".
+    iIntros "HP #H".
     iLöb as "IH".
     rewrite {2}/FG_increment. unlock. simpl.
     rel_rec_l.
@@ -152,7 +153,7 @@ Section CG_Counter.
       iIntros "_ !> Hx". simpl.
       iDestruct "HQ" as "[_ HQ]".
       iSpecialize ("HQ" $! n' with "[Hx HR]"). { iFrame. }
-      rel_if_true_l. done.
+      rel_if_true_l. by iApply "HQ".
     - iExists #n'. iFrame. 
       iSplitL; eauto; last first.
       { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
@@ -162,7 +163,7 @@ Section CG_Counter.
       iMod ("HQ" with "[Hx HR]").
       { iExists _; iFrame. }
       rewrite /FG_increment. unlock. simpl.
-      iApply "IH".
+      by iApply "IH".
   Qed.
 
   (* A similar atomic specification for the counter_read fn *)
@@ -197,7 +198,7 @@ Section CG_Counter.
     { unfold CG_increment. unlock; simpl_subst/=. solve_closed. }
 
     iAlways. iIntros (v v') "[% %]"; simpl in *; subst.
-    iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I _ _ _ [] cnt with "[Hinv]").
+    iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ #false) ∗ cnt' ↦ₛ #n)%I True%I _ _ _ [] cnt with "[Hinv]"); auto.
     iAlways.
     iInv counterN as ">Hcnt" "Hcl". iModIntro.
     iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]".
@@ -207,7 +208,7 @@ Section CG_Counter.
       iMod ("Hcl" with "[-]").
       { iNext. iExists _. iFrame. }
       done.
-    - iIntros (m) "[Hcnt [Hl Hcnt']]".
+    - iIntros (m) "[Hcnt [Hl Hcnt']] _".
       iApply (bin_log_related_CG_increment_r _ [] with "[Hcnt'] [Hl]"); auto. { solve_ndisj.  }
       iIntros "Hcnt' Hl".
       iMod ("Hcl" with "[-]").

theories/examples/various.v

@@ -331,7 +331,7 @@ Section refinement.
       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).
+      (fun (n : nat) => (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))%I True%I); first done.
     iAlways.
     iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht)]" "Hcl";
       iModIntro; iExists _; iFrame.
@@ -344,7 +344,7 @@ Section refinement.
         + iExists (m-1). iRight.
           rewrite minus_Sn_m // /= -minus_n_O.
           iFrame. }
-      { iIntros (m) "[Hc1 Hc]".
+      { iIntros (m) "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
         - unlock FG_increment. simpl.
           rel_rec_r. rel_rec_r.
@@ -377,7 +377,7 @@ Section refinement.
         + iExists (m-1). iRight.
           rewrite minus_Sn_m // /= -minus_n_O.
           iFrame. }
-      { iIntros (m) "[Hc1 Hc]".
+      { iIntros (m) "[Hc1 Hc] _".
         iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
         - unlock FG_increment. simpl.
           rel_rec_r. rel_rec_r.
@@ -416,6 +416,63 @@ Section refinement.
     iApply profiled_g; eauto.
   Qed.
 
+  Lemma close_i6 c1 c2 γ γ' `{oneshotG Σ} `{inG Σ (exclR unitR)} :
+    ((∃ n : nat, c1 ↦ᵢ #n
+     ∗ (c2 ↦ₛ #n ∗ pending γ
+       ∨ c2 ↦ₛ #(n - 1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ n⌝))
+     -∗ i6 c1 c2 γ γ')%I.
+  Proof.
+    iDestruct 1 as (m) "[Hc1 Hc2]".
+    iDestruct "Hc2" as "[[Hc2 Hp] | (Hc2 & Hs & Ht & %)]";
+      [iExists m; iLeft | iExists (m - 1); iRight]; iFrame.
+    rewrite minus_Sn_m // /= -minus_n_O; done.
+  Qed.
+
+  Lemma refinement6_helper Δ Γ f'1 f'2 g1 g2 c1 c2 γ γ' m `{oneshotG Σ} `{inG Σ (exclR unitR)} :
+    inv shootN (i6 c1 c2 γ γ') -∗
+    ⟦ τg ⟧ Δ (g1, g2) -∗
+    ⟦ τf ⟧ Δ (f'1, f'2) -∗
+    (▷ i6 c1 c2 γ γ' ={⊤ ∖ ↑shootN,⊤}=∗ True) -∗
+    c1 ↦ᵢ #(S m) -∗
+    (c2 ↦ₛ #m ∗ pending γ
+      ∨ c2 ↦ₛ #(m - 1) ∗ shot γ ∗ own γ' (Excl ()) ∗ ⌜1 ≤ m⌝) -∗
+    own γ' (Excl ()) -∗
+    {⊤ ∖ ↑shootN,⊤;Δ;Γ} ⊨
+      (g1 #() ;; f'1 (λ: <>, (FG_increment #c1) #() ;; g1 #()) ;; #() ;; ! #c1)
+    ≤log≤
+      (g2 #() ;;
+       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.
+    { iDestruct (own_valid_2 with "Ht Ht'2") as %Hfoo.
+      inversion Hfoo. }
+    iApply fupd_logrel.
+    iMod (shoot γ with "Hp") as "#Hs".
+    iMod ("Hcl" with "[-]") as "_".
+    { iNext. iExists m. iRight. iFrame. done. }
+    iModIntro.
+    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
+    { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]").
+      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+      iApply bin_log_related_unit. }
+    iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
+    { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
+      iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
+        by iApply profiled_g'. }
+    rel_seq_l. rel_seq_r.
+    rel_load_l_atomic. clear m.
+    iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl";
+      iModIntro; iExists _; iFrame.
+    { iExFalso. by iApply shot_not_pending. }
+    iNext. iIntros "Hc1".
+    rel_load_r. rel_op_r.
+    iMod ("Hcl" with "[-]") as "_".
+    { iNext. iExists m. iRight. iFrame. }
+    rewrite Nat.add_1_r.
+    iApply bin_log_related_nat.
+  Qed.
+
   Lemma refinement6 `{oneshotG Σ} `{inG Σ (exclR unitR)} Γ :
     Γ ⊨
       (λ: "f" "g" "f'",
@@ -463,63 +520,27 @@ Section refinement.
       iApply profiled_g'; eauto. }
     rel_seq_l.
     rel_bind_l (FG_increment _). rel_rec_l.
-    (* rel_apply_l (bin_log_FG_increment_logatomic _ *)
-    (*   (fun (n : nat) => own γ' (Excl ()) ∗ (c2 ↦ₛ #n ∗ pending γ) ∨ (c2 ↦ₛ #(n-1) ∗ shot γ ∗ ⌜1 ≤ n⌝))%I). *)
-    unlock {2}FG_increment. simpl.
-    (* rel_rec_l. TODO: doesn't work :( *)
-    iLöb as "IH".
-    rel_pure_l (App (Rec "inc" _ _) _).
-    rel_load_l_atomic.
+    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.
     iInv shootN as (n) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
       iModIntro; iExists _; iFrame; last first.
-    { iDestruct (own_valid_2 with "Ht' Ht'2") as %Hfoo.
-      inversion Hfoo. }
-    iNext. iIntros "Hc1".
-    iMod ("Hcl" with "[Hc1 Hc2 Ht]") as "_".
-    { iNext. iExists n. iLeft. iFrame. }
-    (* rel_let_l. TODO: doesn't work :( *)
-    rel_pure_l (App (Lam "c" _) _).
-    rel_op_l.
-    rel_cas_l_atomic.
-    iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht'2)]" "Hcl";
-      iModIntro; iExists _; iFrame; last first.
-    { iDestruct (own_valid_2 with "Ht' Ht'2") as %Hfoo.
-      inversion Hfoo. }
-    iSplit.
-    - iIntros (?).
-      iNext. iIntros "Hc1".
-      iMod ("Hcl" with "[Hc1 Hc2 Ht]") as "_".
-      { iNext. iExists m. iLeft. iFrame. }
-      rel_if_l.
-      by iApply "IH".
-    - iIntros (?); simplify_eq/=.
-      iNext. iIntros "Hc1".
-      iApply fupd_logrel.
-      iMod (shoot γ with "Ht") as "#Hs".
-      iMod ("Hcl" with "[Hc1 Hc2 Hs Ht']") as "_".
-      { iNext. iExists n. iRight. iFrame. done. }
-      iModIntro.
-      rel_if_l.
-      rel_seq_l.
-      iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
-      { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]").
-        iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
-        iApply bin_log_related_unit. }
-      iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
-      { iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
-        iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
-        by iApply profiled_g'. }
-      rel_seq_l. rel_seq_r.
-      rel_load_l_atomic.
-      iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl";
-        iModIntro; iExists _; iFrame.
-      { iExFalso. by iApply shot_not_pending. }
-      iNext. iIntros "Hc1".
-      rel_load_r. rel_op_r.
-      iMod ("Hcl" with "[-]") as "_".
-      { iNext. iExists m. iRight. iFrame. }
-      rewrite Nat.add_1_r.
-      iApply bin_log_related_nat.
+    { iSplitL "Hc2 Ht Ht'2".
+      { iRight. simpl. rewrite -minus_n_O. iFrame. iPureIntro. omega. }
+      iSplit.
+      - iIntros. iApply "Hcl". by iApply close_i6.
+      - iIntros (m) "[Hc1 Hc2] Ht".
+        rel_seq_l.
+        iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
+    }
+    { iSplitL "Hc2 Ht".
+      { iLeft. by iFrame. }
+      iSplit.
+      - iIntros. iApply "Hcl". by iApply close_i6.
+      - iIntros (m) "[Hc1 Hc2] Ht".
+        rel_seq_l.
+        iApply (refinement6_helper with "Hinv Hg Hf' Hcl Hc1 Hc2 Ht").
+    }
   Qed.
 
 End refinement.