From f0c8ef325ba5928e3354d9cbeed63134eb73e7af Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 18 Sep 2017 18:03:03 +0200 Subject: [PATCH] Add another refinement example --- theories/examples/various.v | 78 +++++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) diff --git a/theories/examples/various.v b/theories/examples/various.v index 5565c90..cf24a08 100644 --- a/theories/examples/various.v +++ b/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. -- GitLab