From 9efd0e45ff4bedc8114119af8e67ec1252997656 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Wed, 28 Mar 2018 13:04:01 +0200 Subject: [PATCH] Further work on liftings --- theories/tests/liftings.v | 76 ++++++++++++++++++++++++++++++++------ theories/tests/relatomic.v | 55 --------------------------- 2 files changed, 64 insertions(+), 67 deletions(-) delete mode 100644 theories/tests/relatomic.v diff --git a/theories/tests/liftings.v b/theories/tests/liftings.v index 448a656..f917d1b 100644 --- a/theories/tests/liftings.v +++ b/theories/tests/liftings.v @@ -46,10 +46,11 @@ Section liftings. Δ Γ : iProp Σ := (∀ K t τ R2 R1, (R2 ∗ □ (|={⊤,Ei}=> ∃ (x : A), α x ∗ R1 x ∗ - (((∃ x, α x ∗ R1 x) ={Ei, ⊤}=∗ True) ∧ - (∀ y v, β y v ∗ R1 y ∗ R2 -∗ {Ei;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ))) - ) -∗ {Δ;Γ} ⊨ fill K e ≤log≤ t : τ)%I. + ((α x ∗ R1 x ={Ei, ⊤}=∗ True) ∧ + (∀ v, β x v ∗ R1 x ∗ R2 -∗ {Ei;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ)))) + -∗ {Δ;Γ} ⊨ fill K e ≤log≤ t : τ)%I. + (* Example: *) (* We can prove the atomic specification for the counter *) Lemma counter_atomic x E Δ Γ : atomic_logrel @@ -59,18 +60,69 @@ Section liftings. (FG_increment #x) Δ Γ. Proof. - iIntros (K t τ R2 R1) "[HR2 #Hlog]". - iApply (bin_log_FG_increment_logatomic _ R1 with "HR2"). - iAlways. iMod "Hlog" as (n) "(Hx & HR & Hlog)". - iModIntro. iExists _. iFrame. + iIntros (K t τ R2 R1) "[HR2 #H]". + iLöb as "IH". + rewrite {2}/FG_increment. unlock. simpl. + rel_rec_l. + iPoseProof "H" as "H2". (* lolwhat *) + rel_load_l_atomic. + iMod "H" as (n) "[Hx [HR Hrev]]". iModIntro. + 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 "H2" as (n') "[Hx [HR HQ]]". iModIntro. simpl. + destruct (decide (n = n')); subst. + - iExists #n'. iFrame. + iSplitR; eauto. { iDestruct 1 as %Hfoo. exfalso. done. } + iIntros "_ !> Hx". simpl. + iDestruct "HQ" as "[_ HQ]". + iSpecialize ("HQ" \$! (#n') with "[Hx HR HR2]"); first by iFrame. + rel_if_true_l. by iApply "HQ". + - iExists #n'. iFrame. + iSplitL; eauto; last first. + { iDestruct 1 as %Hfoo. exfalso. simplify_eq. } + iIntros "_ !> Hx". simpl. + rel_if_false_l. + iDestruct "HQ" as "[HQ _]". + iMod ("HQ" with "[Hx HR]") as "_"; first iFrame. + rewrite /FG_increment. unlock. simpl. + by iApply "IH". + Qed. + + Lemma lift_atomic_tpl {A : Type} + (α: A → iProp Σ) (* atomic pre-condition *) + (β: A → val → iProp Σ) (* atomic post-condition *) + (e : expr) (E : coPset) `{Closed ∅ e} Δ Γ : + atomic_triple α β E ⊤ e -∗ + atomic_logrel α β E e Δ Γ. + Proof. + iIntros "Ht". rewrite /atomic_triple. + iIntros (K t τ R2 R1) "[Hframe #H]". + rewrite bin_log_related_eq /bin_log_related_def. + iIntros (vvs ρ) "#Hspec #HΓ". + iIntros (j K') "Hj /=". + rewrite /env_subst !fill_subst. + rewrite !Closed_subst_p_id. + iModIntro. + wp_bind_core (subst_ctx (fst <\$> vvs) K). + iApply ("Ht" \$! (R2 ∗ j ⤇ fill K' (subst_p (snd <\$> vvs) t))%I with "[] [Hframe Hj]"); last iFrame. + iAlways. iIntros "[Hframe Hj]". + iMod "H" as (a) "(Hα & HR & H)". + iModIntro. iExists _. iFrame "Hα". iSplit. - - iDestruct "Hlog" as "[Hlog _]". done. - - iDestruct "Hlog" as "[_ Hlog]". - iIntros (m) "[Hx HR1] HR2". - iApply ("Hlog" \$! m #m). by iFrame. + - iDestruct "H" as "[H _]". + iIntros "Hα". iFrame. iApply "H". iFrame. + - iDestruct "H" as "[_ H]". + iIntros (v) "Hβ". + iSpecialize ("H" \$! v with "[Hβ HR Hframe]"); first iFrame. + iSpecialize ("H" with "Hspec [HΓ] Hj"); first eauto. + rewrite /interp_expr /= fill_subst Closed_subst_p_id. + done. Qed. - Lemma LA_lift_wtf {A : Type} α (e : expr) β Δ Γ : + (* We can lift a Hoare triple to an atomic triple in which the inner mask is ⊤ *) + Lemma LA_lift {A : Type} α (e : expr) β Δ Γ : (∀ (x : A), lhs_ht (α x) e (β x) Δ Γ) -∗ atomic_logrel α β ⊤ e Δ Γ. Proof. diff --git a/theories/tests/relatomic.v b/theories/tests/relatomic.v deleted file mode 100644 index 89e5d2a..0000000 --- a/theories/tests/relatomic.v +++ /dev/null @@ -1,55 +0,0 @@ -From iris.proofmode Require Import tactics. -From iris_logrel Require Import logrel. -From iris.program_logic Require Import hoare. - -Definition FAI : val := rec: "inc" "x" := - let: "c" := !"x" in - if: CAS "x" "c" (#1 + "c") - then "c" - else "inc" "x". - -Section contents. - Context `{logrelG Σ}. - - Lemma FAI_atomic R1 R2 Γ E1 E2 K x t τ Δ : - R2 -∗ - □ (|={E1,E2}=> ∃ n : nat, x ↦ᵢ #n ∗ R1 n ∗ - ((∃ (m: nat), x ↦ᵢ #m ∗ R1 m) ={E2,E1}=∗ True) ∧ - (∀ m, x ↦ᵢ #(S m) ∗ R1 m -∗ R2 -∗ - {E2,E1;Δ;Γ} ⊨ fill K #m ≤log≤ t : τ)) - -∗ ({E1;Δ;Γ} ⊨ 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 "_". - { iExists _. 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 "_". - { iExists _. by iFrame. } - unlock FAI. - by iApply "IH". - Qed. - -End contents. -- 2.26.2