diff --git a/theories/examples/various.v b/theories/examples/various.v index 90c4c6265946d2bdb157e82f782a412fb255dcca..d9cad561ddf8436ef57ef54aadcddced76a6fde7 100644 --- a/theories/examples/various.v +++ b/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.