Robbert Krebbers committed Oct 31, 2018 1 2 3 4 5 6 ``````(** This file proves the basic and correct usage of resources adequacy statements for [heap_lang]. It does do so by appealing to the generic results in [iron_logic/adequacy]. Note, we only state adequacy for the lifted logic, because in the Coq formalization we state all specifications in terms of the lifted logic. *) `````` Robbert Krebbers committed Jun 11, 2019 7 ``````From iris.algebra Require Import big_op gmap ufrac excl ufrac_auth. `````` Robbert Krebbers committed Oct 31, 2018 8 9 10 11 12 13 14 ``````From iron.iron_logic Require Export weakestpre adequacy. From iron.heap_lang Require Import heap. From iris.proofmode Require Import tactics. Set Default Proof Using "Type". Class heapPreG Σ := HeapPreG { heap_preG_iris :> ironInvPreG Σ; `````` Robbert Krebbers committed Feb 03, 2019 15 16 `````` heap_preG_inG :> inG Σ (ufrac_authR heapUR); heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionC ufracC)))); `````` Robbert Krebbers committed Oct 31, 2018 17 18 19 20 ``````}. Definition heapΣ : gFunctors := #[ ironInvΣ; `````` Robbert Krebbers committed Feb 03, 2019 21 22 `````` GFunctor (ufrac_authR heapUR); GFunctor (authR (gmapUR positive (exclR (optionC ufracC))))]. `````` Robbert Krebbers committed Oct 31, 2018 23 24 25 26 27 28 29 30 31 32 33 34 35 ``````Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ. Proof. solve_inG. Qed. (** A generic helper *) Theorem heap_adequacy Σ `{heapPreG Σ} s e σ φ : (∀ `{heapG Σ}, ([∗ map] l ↦ v ∈ σ, l ↦ v) ⊢ WP e @ s; ⊤ {{ v, |={⊤,∅}=> ⎡∀ h m, heap_ctx h [] m -∗ ⌜φ v h⌝⎤ }}%I) → adequate s e σ φ. Proof. (* TODO: refactor this proof so we don't have the two cases *) destruct (decide (σ = ∅)) as [->|Heq]. - intros Hwp; eapply (iron_wp_adequacy _ _ _ _ _ _ (1 / 2) ε); iIntros (? κs) "". `````` Robbert Krebbers committed Jun 11, 2019 36 `````` iMod (own_alloc (●U{1} ∅ ⋅ (◯U{1/2} ∅ ⋅ ◯U{1/2} ε))) as (γ) "[Hσ [Hp Hp']]". `````` Robbert Krebbers committed Feb 03, 2019 37 38 `````` { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. by apply ufrac_auth_valid. } `````` Hai Dang committed May 24, 2019 39 `````` iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. `````` Robbert Krebbers committed Oct 31, 2018 40 41 42 43 44 45 46 47 48 49 50 51 52 `````` iModIntro. pose (HeapG _ _ _ γ _ _ γf). iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I. iFrame "Hp". iSplitL "Hσ Hf". { iExists ∅. rewrite /= to_heap_empty fmap_empty big_opM_empty. by iFrame. } iPoseProof (Hwp _) as "Hwp"; clear Hwp. iApply (iron_wp_wand with "[Hwp]"). { iApply "Hwp". by rewrite fracPred_at_emp. } iIntros (v π1) "Hupd". iExists π1, ε; repeat (iSplit || iModIntro)=> //. iIntros (π2 π3 h2 Qs Hπ) "Hctx _ _". iMod ("Hupd" with "Hp'") as (π4 π5 _) "[_ H]". iModIntro. iApply ("H" with "Hctx"). - intros Hwp; eapply (iron_wp_adequacy _ _ _ _ _ _ (1 / 2 / 2) (Some (1 / 2)%Qp)). iIntros (? κs) "". `````` Robbert Krebbers committed Jun 11, 2019 53 54 `````` iMod (own_alloc (●U{1} (to_heap σ) ⋅ (◯U{1/2} (to_heap σ) ⋅ ◯U{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]". `````` Robbert Krebbers committed Feb 03, 2019 55 56 `````` { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. apply ufrac_auth_valid; by apply to_heap_valid. } `````` Hai Dang committed May 24, 2019 57 `````` iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. `````` Robbert Krebbers committed Oct 31, 2018 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 `````` iModIntro. pose (HeapG _ _ _ γ _ _ γf). iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _, True%I. iFrame "Hp". iSplitL "Hσ Hf". { iExists ∅. rewrite /= fmap_empty big_opM_empty. by iFrame. } iPoseProof (Hwp _) as "Hwp"; clear Hwp. iDestruct (big_mapsto_alt_2 with "Hσ'") as "Hσ'"; first done. iDestruct ("Hwp" with "Hσ'") as "Hwp'". iApply (iron_wp_wand with "Hwp'"). iIntros (v π1) "Hupd". iExists π1, ε; repeat (iSplit || iModIntro)=> //. iIntros (π2 π3 h2 Qs Hπ) "Hctx _ _". iMod ("Hupd" with "Hp'") as (π4 π5 _) "[_ H]". iModIntro. iApply ("H" with "Hctx"). Qed. (** The basic adequacy statement: the program is safe & when the main thread terminates, the postcondition hold. *) Theorem heap_basic_adequacy Σ `{heapPreG Σ} s e σ φ : (∀ `{heapG Σ}, {{{ [∗ map] l ↦ v ∈ σ, l ↦ v }}} e @ s; ⊤ {{{ v, RET v; ⌜φ v⌝ }}}%I) → adequate s e σ (λ v _, φ v). Proof. intros Hwp. apply (heap_adequacy Σ). iIntros (?) "Hall". iApply (Hwp with "Hall"). iIntros "!>" (v) "Hφ". iMod (fupd_intro_mask' ⊤ ∅) as "H"; first done. iModIntro. iDestruct "Hφ" as %Hφ. by iIntros "!>" (σ' Qs) "_". Qed. (** Adequacy for correct usage of resources: when all threads terminate, and the post-condition exactly characterizes the heap, we know that the heap is in fact of the given shape. *) Theorem heap_all_adequacy Σ `{heapPreG Σ} s e σ1 σ2 σ2' v vs φ : (∀ `{heapG Σ}, ([∗ map] l ↦ v ∈ σ1, l ↦ v) ⊢ WP e @ s; ⊤ {{ v, ([∗ map] l ↦ v ∈ σ2, l ↦ v) ∧ ⌜φ v⌝ }}%I ) → rtc erased_step ([e], σ1) (of_val <\$> v :: vs, σ2') → σ2' = σ2. Proof. (* TODO: refactor this proof so we don't have the two cases *) destruct (decide (σ1 = ∅)) as [->|Heq]. - intros Hwp Hsteps. eapply (iron_wp_all_adequacy _ heap_lang _ _ ∅ σ2' _ _ (λ _, σ2' = σ2) _ ε); [|done]; iIntros (? κs) "". `````` Hai Dang committed May 24, 2019 100 `````` iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. `````` Robbert Krebbers committed Jun 11, 2019 101 `````` iMod (own_alloc (●U{1} (to_heap ∅) ⋅ (◯U{1/2} (to_heap ∅) ⋅ ◯U{1/2} ε))) `````` Robbert Krebbers committed Oct 31, 2018 102 `````` as (γ) "[Hσ [Hσ' Hp]]". `````` Robbert Krebbers committed Feb 03, 2019 103 104 `````` { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. apply ufrac_auth_valid; by apply to_heap_valid. } `````` Robbert Krebbers committed Oct 31, 2018 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 `````` iModIntro. pose (HeapG _ _ _ γ _ _ γf). iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _. iFrame "Hp"; iExists ([∗ map] l ↦ v ∈ σ2, l ↦ v)%I. iSplitL "Hσ Hf". { iExists ∅. rewrite /= to_heap_empty fmap_empty big_opM_empty. by iFrame. } iPoseProof (Hwp _) as "Hwp"; clear Hwp. iDestruct ("Hwp" with "[]") as "Hwp'". { rewrite big_opM_empty fracPred_at_emp; auto. } iApply (iron_wp_wand with "Hwp'"); iIntros (v' π) "[Hσ2 _] /=". iExists π, ε; iSplit; first (by rewrite left_id_L right_id_L). iFrame "Hσ2". iModIntro; iSplit; first done. iIntros (π1 π2 Hπ) "Hσ2' HQs Hp' Hσ2". rewrite to_heap_empty. iMod (heap_thread_adequacy _ _ _ (1/2 + π1)%Qp with "Hσ2' [HQs] [Hσ' Hp'] Hσ2") as "\$". { by rewrite -frac_op' cmra_op_opM_assoc_L -Hπ frac_op' Qp_div_2. } { by iApply big_sepL_replicate. } { by iSplitL "Hσ'". } iMod (fupd_intro_mask' ⊤ ∅) as "_"; auto. - intros Hwp Hsteps. eapply (iron_wp_all_adequacy _ heap_lang _ _ σ1 σ2' _ _ (λ _, σ2' = σ2) _ (Some (1 / 2)%Qp)); [|done]; iIntros (? κs) "". `````` Hai Dang committed May 24, 2019 125 `````` iMod (own_alloc (● ∅)) as (γf) "Hf"; first by apply auth_auth_valid. `````` Robbert Krebbers committed Jun 11, 2019 126 `````` iMod (own_alloc (●U{1} (to_heap σ1) ⋅ (◯U{1/2} (to_heap σ1) ⋅ ◯U{1/2} ε))) `````` Robbert Krebbers committed Oct 31, 2018 127 `````` as (γ) "[Hσ [Hσ' Hp]]". `````` Robbert Krebbers committed Feb 03, 2019 128 129 `````` { rewrite -ufrac_auth_frag_op Qp_div_2 right_id. apply ufrac_auth_valid; by apply to_heap_valid. } `````` Robbert Krebbers committed Oct 31, 2018 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 `````` iModIntro. pose (HeapG _ _ _ γ _ _ γf). iExists heap_perm, heap_ctx, (λ _, heap_fork_post), _, _. iFrame "Hp"; iExists ([∗ map] l ↦ v ∈ σ2, l ↦ v)%I. iSplitL "Hσ Hf". { iExists ∅. rewrite /= fmap_empty big_opM_empty. by iFrame. } iPoseProof (Hwp _) as "Hwp"; clear Hwp. iDestruct ("Hwp" with "[Hσ']") as "Hwp'"; first by iApply big_mapsto_alt_2. iApply (iron_wp_wand with "Hwp'"). iIntros (v' π) "[Hσ2 _]". iExists π, ε; iSplit; first (erewrite left_id_L, right_id_L; auto; apply _). iFrame "Hσ2". iModIntro; iSplit; first done. iIntros (π1 π2 Hπ) "Hσ2' HQs Hp' Hσ2". iMod (heap_thread_adequacy with "Hσ2' [HQs] Hp' Hσ2") as "\$". { by rewrite -Hπ /= frac_op' Qp_div_2. } { by iApply big_sepL_replicate. } iMod (fupd_intro_mask' ⊤ ∅) as "_"; auto. Qed.``````