Add another refinement example

theories/examples/various.v

@@ -135,4 +135,82 @@ Section refinement.
         rel_vals; eauto.
   Qed.
 
+  Definition i3 x x' b b' : iProp Σ :=
+    ((∃ (n : nat), x ↦ᵢ #n ∗ x' ↦ₛ #n ∗
+                 b ↦ᵢ #true ∗ b' ↦ₛ #true)
+               ∨ (b ↦ᵢ #false ∗ b' ↦ₛ #false))%I.
+  Definition i3n := nroot .@ "i3".
+  Lemma refinement3  Γ :
+    Γ ⊨
+      let: "b" := ref #true in
+      let: "x" := ref #0 in
+      (λ: "f", if: CAS "b" #true #false
+               then "f" #();; "x" <- !"x" + #1 ;; "b" <- #true
+               else #())
+    ≤log≤
+      (let: "b" := ref #true in
+      let: "x" := ref #0 in
+      (λ: "f", if: CAS "b" #true #false
+               then let: "n" := !"x" in
+                    "f" #();; "x" <- "n" + #1 ;; "b" <- #true
+               else #()))
+    : TArrow (TArrow TUnit TUnit) TUnit.
+  Proof.
+    iIntros (Δ).
+    rel_alloc_l as b "Hb".
+    rel_let_l.
+    rel_alloc_l as x "Hx".
+    rel_let_l.
+    rel_alloc_r as b' "Hb'".
+    rel_let_r.
+    rel_alloc_r as x' "Hx'".
+    rel_let_r.
+    iMod (inv_alloc i3n _ (i3 x x' b b') with "[-]") as "#Hinv".
+    { iNext. unfold i3.
+      iLeft. iExists 0. iFrame. }
+    iApply bin_log_related_arrow; eauto.
+    iAlways. iIntros (f f') "Hf".
+    rel_let_l.
+    rel_let_r.
+    rel_cas_l_atomic.
+    iInv i3n as ">Hbb" "Hcl".
+    rewrite {2}/i3.
+    iDestruct "Hbb" as "[Hbb | (Hb & Hb')]"; last first.
+    { iModIntro; iExists _; iFrame.
+      iSplitL; last by iIntros (?); congruence.
+      iIntros (?); iNext; iIntros "Hb".
+      rel_cas_fail_r; rel_if_r; rel_if_l.
+      iMod ("Hcl" with "[-]").
+      { iNext. iRight. iFrame. }
+      rel_vals; eauto.
+    }
+    { iDestruct "Hbb" as (n) "(Hx & Hx' & Hb & Hb')".
+      iModIntro. iExists _; iFrame.
+      iSplitR; first by iIntros (?); congruence.
+      iIntros (?); iNext; iIntros "Hb".
+      rel_cas_suc_r; rel_if_r; rel_if_l.
+      rel_load_r. rel_let_r.
+      iMod ("Hcl" with "[Hb Hb']") as "_".
+      { iNext. iRight. iFrame. }
+      iApply (bin_log_related_seq with "[Hf]"); auto.
+      { iApply (bin_log_related_app with "Hf").
+        iApply bin_log_related_unit. }
+      rel_load_l.
+      rel_op_l. rel_op_r.
+      rel_store_l. rel_store_r.
+      rel_seq_l. rel_seq_r.
+      rel_store_l_atomic.
+      iInv i3n as ">Hi3" "Hcl".
+      iDestruct "Hi3" as "[Hi3 | [Hb Hb']]".
+      { iDestruct "Hi3" as (m) "(Hx1 & Hx1' & Hb & Hb')".
+        iModIntro. iExists _; iFrame; iNext. iIntros "Hb".
+        iDestruct (mapsto_valid_2 with "Hx Hx1") as %Hfoo.
+        cbv in Hfoo. by exfalso. }
+      iModIntro; iExists _; iFrame; iNext; iIntros "Hb".
+      rel_store_r.
+      iMod ("Hcl" with "[-]") as "_".
+      { iNext. iLeft. iExists _. iFrame. }
+      rel_vals; eauto. }
+  Qed.
+
 End refinement.