Logically atomic specifications for FAI and FAD

_CoqProject

@@ -44,6 +44,7 @@ theories/examples/or.v
 theories/examples/symbol.v
 theories/examples/generative.v
 theories/examples/Y.v
+theories/examples/FAI.v
 theories/tests/typetest.v
 theories/tests/ghosttp.v
 theories/tests/tactics.v

theories/examples/FAI.v

+From iris.proofmode Require Import tactics.
+From iris_logrel Require Import logrel.
+
+Definition FAI : val := rec: "inc" "x" :=
+  let: "c" := !"x" in
+  if: CAS "x" "c" (#1 + "c")
+  then "c"
+  else "inc" "x".
+
+Definition FAD : val := rec: "dec" "x" :=
+  let: "c" := !"x" in
+  if: CAS "x" "c" ("c"-#1)
+  then "c"
+  else "dec" "x".
+
+Section contents.
+  Context `{logrelG Σ}.
+
+  Lemma FAI_atomic R1 R2 Γ E K x t τ Δ :
+    R2 -∗
+    □ (|={⊤,E}=> ∃ m : nat, x ↦ᵢ #m ∗ R1 m ∗
+       ((x ↦ᵢ #m ∗ R1 m ={E,⊤}=∗ True) ∧
+        (x ↦ᵢ #(S m) ∗ R1 m -∗ R2 -∗
+            {E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)))
+    -∗ ({Δ;Γ} ⊨ fill K (FAI #x) ≤log≤ t : τ).
+  Proof.
+    iIntros "HR2 #H".
+    iLöb as "IH".
+    rewrite {2}/FAI. unlock; simpl.
+    rel_rec_l.
+    iPoseProof "H" as "H2". (* iMod later on destroys H *)
+    rel_load_l_atomic.
+    iMod "H" as (n) "[Hx [HR Hrev]]".
+    iModIntro. iRename "H2" into "H".
+    iExists #n. iFrame. iNext. iIntros "Hx".
+    iDestruct "Hrev" as "[Hrev _]".
+    iMod ("Hrev" with "[HR Hx]") as "_"; first by iFrame.
+    rel_rec_l. rel_op_l.
+    rel_cas_l_atomic.
+    iMod "H" as (n') "[Hx [HR HQ]]". iModIntro.
+    iExists #n'. iFrame.
+    destruct (decide (n = n')); subst.
+    - iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
+      iIntros "_ !> Hx". simpl.
+      iDestruct "HQ" as "[_ HQ]".
+      iSpecialize ("HQ" with "[Hx HR]"). { iFrame. }
+      rel_if_l. by iApply "HQ".
+    - iSplitL; eauto; last first.
+      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
+      iIntros "_ !> Hx". simpl.
+      rel_if_l.
+      iDestruct "HQ" as "[HQ _]".
+      iMod ("HQ" with "[Hx HR]") as "_"; first by iFrame.
+      unlock FAI.
+      by iApply "IH".
+  Qed.
+
+  Lemma FAD_atomic R1 R2 Γ E K x t τ Δ :
+    R2 -∗
+    □ (|={⊤,E}=> ∃ m : nat, x ↦ᵢ #m ∗ R1 m ∗
+       ((x ↦ᵢ #m ∗ R1 m ={E,⊤}=∗ True) ∧
+        (x ↦ᵢ #(m-1) ∗ R1 m -∗ R2 -∗
+            {E;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)))
+    -∗ ({Δ;Γ} ⊨ fill K (FAD #x) ≤log≤ t : τ).
+  Proof.
+    iIntros "HR2 #H".
+    iLöb as "IH".
+    rewrite {2}/FAD. unlock; simpl.
+    rel_rec_l.
+    iPoseProof "H" as "H2". (* iMod later on destroys H *)
+    rel_load_l_atomic.
+    iMod "H" as (n) "[Hx [HR Hrev]]".
+    iModIntro. iRename "H2" into "H".
+    iExists #n. iFrame. iNext. iIntros "Hx".
+    iDestruct "Hrev" as "[Hrev _]".
+    iMod ("Hrev" with "[HR Hx]") as "_"; first by iFrame.
+    rel_rec_l. rel_op_l.
+    rel_cas_l_atomic.
+    iMod "H" as (n') "[Hx [HR HQ]]". iModIntro.
+    iExists #n'. iFrame.
+    destruct (decide (n = n')); subst.
+    - iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. }
+      iIntros "_ !> Hx". simpl.
+      iDestruct "HQ" as "[_ HQ]".
+      iSpecialize ("HQ" with "[Hx HR]"). { iFrame. }
+      rel_if_l. by iApply "HQ".
+    - iSplitL; eauto; last first.
+      { iDestruct 1 as %Hfoo. exfalso. simplify_eq. }
+      iIntros "_ !> Hx". simpl.
+      rel_if_l.
+      iDestruct "HQ" as "[HQ _]".
+      iMod ("HQ" with "[Hx HR]") as "_"; first by iFrame.
+      unlock FAD.
+      by iApply "IH".
+  Qed.
+
+End contents.