Commit 9efd0e45 by Dan Frumin

### Further work on liftings

parent c139a492
 ... @@ -46,10 +46,11 @@ Section liftings. ... @@ -46,10 +46,11 @@ Section liftings. Δ Γ : iProp Σ := Δ Γ : iProp Σ := (∀ K t τ R2 R1, (R2 ∗ □ (|={⊤,Ei}=> ∃ (x : A), (∀ K t τ R2 R1, (R2 ∗ □ (|={⊤,Ei}=> ∃ (x : A), α x ∗ R1 x ∗ α x ∗ R1 x ∗ (((∃ x, α x ∗ R1 x) ={Ei, ⊤}=∗ True) ∧ ((α x ∗ R1 x ={Ei, ⊤}=∗ True) ∧ (∀ y v, β y v ∗ R1 y ∗ R2 -∗ {Ei;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ))) (∀ v, β x v ∗ R1 x ∗ R2 -∗ {Ei;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ)))) ) -∗ {Δ;Γ} ⊨ fill K e ≤log≤ t : τ)%I. -∗ {Δ;Γ} ⊨ fill K e ≤log≤ t : τ)%I. (* Example: *) (* We can prove the atomic specification for the counter *) (* We can prove the atomic specification for the counter *) Lemma counter_atomic x E Δ Γ : Lemma counter_atomic x E Δ Γ : atomic_logrel atomic_logrel ... @@ -59,18 +60,69 @@ Section liftings. ... @@ -59,18 +60,69 @@ Section liftings. (FG_increment #x) (FG_increment #x) Δ Γ. Δ Γ. Proof. Proof. iIntros (K t τ R2 R1) "[HR2 #Hlog]". iIntros (K t τ R2 R1) "[HR2 #H]". iApply (bin_log_FG_increment_logatomic _ R1 with "HR2"). iLöb as "IH". iAlways. iMod "Hlog" as (n) "(Hx & HR & Hlog)". rewrite {2}/FG_increment. unlock. simpl. iModIntro. iExists _. iFrame. 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. iSplit. - iDestruct "Hlog" as "[Hlog _]". done. - iDestruct "H" as "[H _]". - iDestruct "Hlog" as "[_ Hlog]". iIntros "Hα". iFrame. iApply "H". iFrame. iIntros (m) "[Hx HR1] HR2". - iDestruct "H" as "[_ H]". iApply ("Hlog" \$! m #m). by iFrame. 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. 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) Δ Γ) -∗ (∀ (x : A), lhs_ht (α x) e (β x) Δ Γ) -∗ atomic_logrel α β ⊤ e Δ Γ. atomic_logrel α β ⊤ e Δ Γ. Proof. Proof. ... ...
 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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!