adequacy.v 7.07 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 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 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
(** 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. *)
From iris.algebra Require Import big_op gmap.
From iron.iron_logic Require Export weakestpre adequacy.
From iron.algebra Require Import vfrac_auth vfrac.
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 Σ;
  heap_preG_inG :> inG Σ (vfrac_authR heapUR);
  heap_preG_fork_post_inG :> inG Σ (authR (gmapUR positive (exclR (optionC vfracC))));
}.

Definition heapΣ : gFunctors := #[
  ironInvΣ;
  GFunctor (vfrac_authR heapUR);
  GFunctor (authR (gmapUR positive (exclR (optionC vfracC))))].
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']]".
    { rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
      by apply vfrac_auth_valid. }
    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']]]".
    { rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
      apply vfrac_auth_valid; by apply to_heap_valid. }
    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]]".
    { rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
      apply vfrac_auth_valid; by apply to_heap_valid. }
    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]]".
    { rewrite -vfrac_auth_frag_op Qp_div_2 right_id.
      apply vfrac_auth_valid; by apply to_heap_valid. }
    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.