Full version of the "callback with lock" example

theories/examples/various.v

@@ -186,10 +186,10 @@ Section refinement.
   Qed.
 
   (* Also known as "callback with lock" *)
-  Definition i3 x x' b b' : iProp Σ :=
-    ((∃ (n : nat), x ↦ᵢ #n ∗ x' ↦ₛ #n ∗
-                 b ↦ᵢ #true ∗ b' ↦ₛ #true)
-               ∨ (b ↦ᵢ #false ∗ b' ↦ₛ #false))%I.
+  Definition i3 (x x' b b' : loc) : iProp Σ :=
+    (∃ (n:nat), x ↦ᵢ{1/2} #n ∗ x' ↦ₛ{1/2} #n ∗
+    ((b ↦ᵢ #true ∗ b' ↦ₛ #true ∗ x ↦ᵢ{1/2} #n ∗ x' ↦ₛ{1/2} #n)
+    ∨ (b ↦ᵢ #false ∗ b' ↦ₛ #false)))%I.
   Definition i3n := nroot .@ "i3".
   Lemma refinement3 Γ :
     Γ ⊨
@@ -197,15 +197,17 @@ Section refinement.
       let: "x" := ref #0 in
       (λ: "f", if: CAS "b" #true #false
                then "f" #();; "x" <- !"x" + #1 ;; "b" <- #true
-               else #())
+               else #(),
+       λ: <>, !"x")
     ≤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.
+               else #(),
+       λ: <>, !"x"))
+    : ((Unit → Unit) → Unit) × (Unit → TNat).
   Proof.
     iIntros (Δ).
     rel_alloc_l as b "Hb".
@@ -217,51 +219,77 @@ Section refinement.
     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 x with "Hx Hx1") as %Hfoo.
-        cbv in Hfoo. by exfalso. }
-      iModIntro; iExists _; iFrame; iNext; iIntros "Hb".
-      rel_store_r.
+    { iNext. unfold i3. iExists 0.
+      iDestruct "Hx" as "[$ Hx]".
+      iDestruct "Hx'" as "[$ Hx']".
+      iLeft. iFrame. }
+    iApply bin_log_related_pair.
+    - iApply bin_log_related_arrow; eauto.
+      iAlways. iIntros (f f') "Hf".
+      rel_let_l.
+      rel_let_r.
+      rel_cas_l_atomic.
+      iInv i3n as (n) "(Hx & Hx' & >Hbb)" "Hcl".
+      iDestruct "Hbb" as "[(Hb & Hb' & Hx1 & Hx'1) | (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. iExists n. iFrame. iRight. iFrame. }
+        rel_vals; eauto.
+      }
+      { 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' Hx Hx']") as "_".
+        { iNext. iExists _; iFrame. 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_atomic.
+        iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
+        iDestruct (mapsto_agree with "Hx Hx1") as %->.
+        iCombine "Hx Hx1" as "Hx".
+        iModIntro. iExists _; iFrame. iNext.
+        iIntros "Hx".
+        iCombine "Hx' Hx'1" as "Hx'".
+        rel_store_r.
+        iDestruct "Hx" as "[Hx Hx1]".
+        iDestruct "Hx'" as "[Hx' Hx'1]".
+        iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | Hbb]".
+        { iCombine "Hx Hx1" as "Hx".
+          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+          compute in Hfoo. eauto. }
+        iMod ("Hcl" with "[Hx Hx' Hbb]") as "_".
+        { iNext. iExists _. iFrame. }
+        rel_seq_l. rel_seq_r.
+        rel_store_l_atomic. clear n'.
+        iInv i3n as (n') "(>Hx & Hx' & >Hbb)" "Hcl".
+        iDestruct (mapsto_agree with "Hx Hx1") as %->.
+        iDestruct "Hbb" as "[(Hb & Hb' & Hx2 & Hx'2) | (Hb & Hb')]".
+        { iCombine "Hx Hx1" as "Hx".
+          iDestruct (mapsto_valid_2 with "Hx Hx2") as %Hfoo. exfalso.
+          compute in Hfoo. eauto. }
+        iModIntro; iExists _; iFrame; iNext. iIntros "Hb".
+        rel_store_r.
+        iMod ("Hcl" with "[-]") as "_".
+        { iNext. iExists _. iFrame. iLeft. iFrame. }
+        rel_vals; eauto. }
+    - iApply bin_log_related_arrow; eauto.
+      iAlways. iIntros (u u') "_".
+      rel_let_l. rel_let_r.
+      rel_load_l_atomic.
+      iInv i3n as (n) "(>Hx & Hx' & >Hbb)" "Hcl".
+      iModIntro. iExists _; iFrame; iNext. iIntros "Hx".
+      rel_load_r.
       iMod ("Hcl" with "[-]") as "_".
-      { iNext. iLeft. iExists _. iFrame. }
-      rel_vals; eauto. }
+      { iNext. iExists _. iFrame. }
+      iApply bin_log_related_nat.
   Qed.
 
   (* /Sort of/ a well-bracketedness example.