hocap_spec.v 9.65 KB
Newer Older
1 2 3 4 5 6
From stdpp Require Import namespaces.
From iris.algebra Require Import excl auth list.
From iris.heap_lang Require Export lifting notation.
From iris.base_logic.lib Require Import invariants.
From iris.program_logic Require Import atomic.
From iris.heap_lang Require Import proofmode atomic_heap.
7
From iris_examples.logatom.elimination_stack Require spec.
8 9
Set Default Proof Using "Type".

10
Module logatom := elimination_stack.spec.
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29

(** A general HoCAP-style interface for a stack, modeled after the spec in
[hocap/abstract_bag.v].  There are two differences:
- We split [bag_contents] into an authoritative part and a fragment as this
  slightly strnegthens the spec: The logically atomic spec only requires
  [stack_content ∗ stack_content] to derive a contradiction, the abstract bag
  spec requires to get *three* pieces which is only possible when actually
  calling a bag operation.
- We also slightly weaken the spec by adding [make_laterable], which is needed
  because logical atomicity can only capture laterable resources, which is
  needed when implementing e.g. the elimination stack on top of an abstract
  logically atomic heap. *)
Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
  (* -- operations -- *)
  new_stack : val;
  push : val;
  pop : val;
  (* -- other data -- *)
  name : Type;
30 31
  name_eqdec : EqDecision name;
  name_countable : Countable name;
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
  (* -- predicates -- *)
  is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
  stack_content_frag (γs : name) (l : list val) : iProp Σ;
  stack_content_auth (γs : name) (l : list val) : iProp Σ;
  (* -- predicate properties -- *)
  is_stack_persistent N γs v : Persistent (is_stack N γs v);
  stack_content_frag_timeless γs l : Timeless (stack_content_frag γs l);
  stack_content_auth_timeless γs l : Timeless (stack_content_auth γs l);
  stack_content_frag_exclusive γs l1 l2 :
    stack_content_frag γs l1 - stack_content_frag γs l2 - False;
  stack_content_auth_exclusive γs l1 l2 :
    stack_content_auth γs l1 - stack_content_auth γs l2 - False;
  stack_content_agree γs l1 l2 :
    stack_content_frag γs l1 - stack_content_auth γs l2 - l1 = l2;
  stack_content_update γs l l' :
    stack_content_frag γs l -
    stack_content_auth γs l -
    |==> stack_content_frag γs l'  stack_content_auth γs l';
  (* -- operation specs -- *)
  new_stack_spec N :
    {{{ True }}} new_stack #() {{{ γs s, RET s; is_stack N γs s  stack_content_frag γs [] }}};
53
  push_spec N γs s (v : val) (Φ : val  iProp Σ) :
54 55
    is_stack N γs s -
    make_laterable ( l, stack_content_auth γs l ={∖↑N}= stack_content_auth γs (v::l)  Φ #()) -
56
    WP push s v {{ Φ }};
57 58 59 60 61 62 63 64 65
  pop_spec N γs s (Φ : val  iProp Σ) :
    is_stack N γs s -
    make_laterable ( l, stack_content_auth γs l ={∖↑N}=
          match l with [] => stack_content_auth γs []  Φ NONEV
                | v :: l' => stack_content_auth γs l'  Φ (SOMEV v) end) -
    WP pop s {{ Φ }};
}.
Arguments hocap_stack _ {_}.

66 67 68
Existing Instances
  is_stack_persistent stack_content_frag_timeless stack_content_auth_timeless
  name_eqdec name_countable.
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

(** Show that our way of writing the [pop_spec] is equivalent to what is done in
[concurrent_stack.spec].  IOW, the conjunction-vs-match doesn't matter.  Fixing
the postcondition (the [Q] in [concurrent_stack.spec]) still matters. *)
Section pop_equiv.
  Context `{invG Σ} (T : Type).

  Lemma pop_equiv E (I : list T  iProp Σ) (Φemp : iProp Σ) (Φret : T  iProp Σ) :
    ( l, I l ={E}=
       match l with [] => I []  Φemp | v :: l' => I l'  Φret v end)
    
    ( v vs, I (v :: vs) ={E}= Φret v  I vs)
     (I [] ={E}= Φemp  I []).
  Proof.
    iSplit.
    - iIntros "HΦ". iSplit.
      + iIntros (??) "HI". iMod ("HΦ" with "HI") as "[$ $]". done.
      + iIntros "HI". iMod ("HΦ" with "HI") as "[$ $]". done.
    - iIntros "HΦ" (l) "HI". destruct l; rewrite [(I _  _)%I]bi.sep_comm; by iApply "HΦ".
  Qed.
End pop_equiv.

(** From a HoCAP stack we can directly implement the logically atomic
interface. *)
Section hocap_logatom.
  Context `{!heapG Σ} (stack: hocap_stack Σ).

96
  Lemma logatom_push N γs s (v : val) :
97 98
    stack.(is_stack) N γs s -
    <<<  l : list val, stack.(stack_content_frag) γs l >>>
99
      stack.(push) s v @ ∖↑N
100 101
    <<< stack.(stack_content_frag) γs (v::l), RET #() >>>.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
102
    iIntros "Hstack". iIntros (Φ) "HΦ".
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117
    iApply (push_spec with "Hstack").
    iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
    iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
    iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
    iMod (stack_content_update with "Hfrag Hauth") as "[Hfrag $]".
    iMod ("Hclose" with "Hfrag") as "HΦ". done.
  Qed.

  Lemma logatom_pop N γs (s : val) :
    stack.(is_stack) N γs s -
    <<<  l : list val, stack.(stack_content_frag) γs l >>>
      stack.(pop) s @ ∖↑N
    <<< stack.(stack_content_frag) γs (tail l),
        RET match l with [] => NONEV | v :: _ => SOMEV v end >>>.
  Proof.
Ralf Jung's avatar
Ralf Jung committed
118
    iIntros "Hstack". iIntros (Φ) "HΦ".
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140
    iApply (pop_spec with "Hstack").
    iApply (make_laterable_intro with "[%] [] HΦ"). iIntros "!# >HΦ" (l) "Hauth".
    iMod "HΦ" as (l') "[Hfrag [_ Hclose]]".
    iDestruct (stack_content_agree with "Hfrag Hauth") as %->.
    destruct l;
    iMod (stack_content_update with "Hfrag Hauth") as "[Hfrag $]";
    iMod ("Hclose" with "Hfrag") as "HΦ"; done.
  Qed.

  Definition hocap_logatom : logatom.atomic_stack Σ :=
    {| logatom.new_stack_spec := stack.(new_stack_spec);
       logatom.push_spec := logatom_push;
       logatom.pop_spec := logatom_pop;
       logatom.stack_content_exclusive := stack.(stack_content_frag_exclusive) |}.

End hocap_logatom.

(** From a logically atomic stack, we can implement a HoCAP stack by adding an
auth invariant. *)

(** The CMRA & functor we need. *)
Class hocapG Σ := HocapG {
Robbert Krebbers's avatar
Robbert Krebbers committed
141
  hocap_stateG :> inG Σ (authR (optionUR $ exclR (listO valO)));
142 143
}.
Definition hocapΣ : gFunctors :=
Robbert Krebbers's avatar
Robbert Krebbers committed
144
  #[GFunctor (exclR unitO); GFunctor (authR (optionUR $ exclR (listO valO)))].
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169

Instance subG_hocapΣ {Σ} : subG hocapΣ Σ  hocapG Σ.
Proof. solve_inG. Qed.

Section logatom_hocap.
  Context `{!heapG Σ} `{!hocapG Σ} (stack: logatom.atomic_stack Σ).

  Definition hocap_name : Type := stack.(logatom.name) * gname.
  Implicit Types γs : hocap_name.

  Definition hocap_stack_content_auth γs l : iProp Σ := own γs.2 ( Excl' l).
  Definition hocap_stack_content_frag γs l : iProp Σ := own γs.2 ( Excl' l).

  Definition hocap_is_stack N γs v : iProp Σ :=
    (stack.(logatom.is_stack) (N .@ "stack") γs.1 v 
     inv (N .@ "wrapper") ( l, stack.(logatom.stack_content) γs.1 l  hocap_stack_content_auth γs l))%I.

  Lemma hocap_new_stack N :
    {{{ True }}}
      stack.(logatom.new_stack) #()
    {{{ γs s, RET s; hocap_is_stack N γs s  hocap_stack_content_frag γs [] }}}.
  Proof.
    iIntros (Φ) "_ HΦ". iApply wp_fupd. iApply logatom.new_stack_spec; first done.
    iIntros "!>" (γs s) "[Hstack Hcont]".
    iMod (own_alloc ( Excl' []   Excl' [])) as (γw) "[Hs● Hs◯]".
Hai Dang's avatar
Hai Dang committed
170
    { apply auth_both_valid. split; done. }
171 172 173 174
    iApply ("HΦ" $! (γs, γw)). rewrite /hocap_is_stack. iFrame.
    iApply inv_alloc. eauto with iFrame.
  Qed.

175
  Lemma hocap_push N γs s (v : val) (Φ : val  iProp Σ) :
176 177
    hocap_is_stack N γs s -
    make_laterable ( l, hocap_stack_content_auth γs l ={∖↑N}= hocap_stack_content_auth γs (v::l)  Φ #()) -
178
    WP stack.(logatom.push) s v {{ Φ }}.
179
  Proof using Type*.
Ralf Jung's avatar
Ralf Jung committed
180 181
    iIntros "#[Hstack Hwrap] Hupd". awp_apply (logatom.push_spec with "Hstack").
    iInv "Hwrap" as (l) "[>Hcont >H●]".
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
    iAaccIntro with "Hcont"; first by eauto 10 with iFrame.
    iIntros "Hcont".
    iMod fupd_intro_mask' as "Hclose";
      last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
    iMod "Hclose" as "_". iIntros "!>".
    eauto with iFrame.
  Qed.

  Lemma hocap_pop N γs s (Φ : val  iProp Σ) :
    hocap_is_stack N γs s -
    make_laterable ( l, hocap_stack_content_auth γs l ={∖↑N}=
          match l with [] => hocap_stack_content_auth γs []  Φ NONEV
                | v :: l' => hocap_stack_content_auth γs l'  Φ (SOMEV v) end) -
    WP stack.(logatom.pop) s {{ Φ }}.
  Proof using Type*.
Ralf Jung's avatar
Ralf Jung committed
197 198
    iIntros "#[Hstack Hwrap] Hupd". awp_apply (logatom.pop_spec with "Hstack").
    iInv "Hwrap" as (l) "[>Hcont >H●]".
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
    iAaccIntro with "Hcont"; first by eauto 10 with iFrame.
    iIntros "Hcont". destruct l.
    - iMod fupd_intro_mask' as "Hclose";
        last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
       iMod "Hclose" as "_". iIntros "!>"; eauto with iFrame.
    - iMod fupd_intro_mask' as "Hclose";
        last iMod (make_laterable_elim with "Hupd H●") as "[H● HΦ]"; first solve_ndisj.
       iMod "Hclose" as "_". iIntros "!>"; eauto with iFrame.
  Qed.

  Program Definition logatom_hocap : hocap_stack Σ :=
    {| new_stack_spec := hocap_new_stack;
       push_spec := hocap_push;
       pop_spec := hocap_pop |}.
  Next Obligation.
    iIntros (???) "Hf1 Hf2". iDestruct (own_valid_2 with "Hf1 Hf2") as %[].
  Qed.
  Next Obligation.
Hai Dang's avatar
Hai Dang committed
217
    iIntros (???) "Ha1 Ha2". by iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
218 219 220
  Qed.
  Next Obligation.
    iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
Hai Dang's avatar
Hai Dang committed
221
      %[->%Excl_included%leibniz_equiv _]%auth_both_valid. done.
222 223 224 225 226 227 228 229
  Qed.
  Next Obligation.
    iIntros (???) "Hf Ha". iMod (own_update_2 with "Ha Hf") as "[? ?]".
    { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
    by iFrame.
  Qed.

End logatom_hocap.