adequacy.v 7.07 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
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. *)
7
From iris.algebra Require Import big_op gmap ufrac.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
From iron.iron_logic Require Export weakestpre adequacy.
9
From iron.algebra Require Import ufrac_auth.
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12 13 14 15
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 Σ;
16 17
  heap_preG_inG :> inG Σ (ufrac_authR heapUR);
  heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionC ufracC))));
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20 21
}.

Definition heapΣ : gFunctors := #[
  ironInvΣ;
22 23
  GFunctor (ufrac_authR heapUR);
  GFunctor (authR (gmapUR positive (exclR (optionC ufracC))))].
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37
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) "".
    iMod (own_alloc (?{1}   (?{1/2}   ?{1/2} ε))) as (γ) "[Hσ [Hp Hp']]".
38 39
    { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
      by apply ufrac_auth_valid. }
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
    iMod (own_alloc ( )) as (γf) "Hf"; first done.
    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) "".
    iMod (own_alloc (?{1} (to_heap σ) 
      (?{1/2} (to_heap σ)  ?{1/2} ε))) as (γ) "[Hσ [Hσ' [Hp Hp']]]".
56 57
    { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
      apply ufrac_auth_valid; by apply to_heap_valid. }
Robbert Krebbers's avatar
Robbert Krebbers committed
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 100 101 102 103
    iMod (own_alloc ( )) as (γf) "Hf"; first done.
    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) "".
    iMod (own_alloc ( )) as (γf) "Hf"; first done.
    iMod (own_alloc (?{1} (to_heap )  (?{1/2} (to_heap )  ?{1/2} ε)))
      as (γ) "[Hσ [Hσ' Hp]]".
104 105
    { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
      apply ufrac_auth_valid; by apply to_heap_valid. }
Robbert Krebbers's avatar
Robbert Krebbers committed
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
    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) "".
    iMod (own_alloc ( )) as (γf) "Hf"; first done.
    iMod (own_alloc (?{1} (to_heap σ1)  (?{1/2} (to_heap σ1)  ?{1/2} ε)))
      as (γ) "[Hσ [Hσ' Hp]]".
129 130
    { rewrite -ufrac_auth_frag_op Qp_div_2 right_id.
      apply ufrac_auth_valid; by apply to_heap_valid. }
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
    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.