stack_rules.v 9.84 KB
Newer Older
1
From iris.proofmode Require Import tactics.
2
From iris_logrel.F_mu_ref_conc Require Import logrel_binary.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.algebra Require Import gmap dec_agree.
4
From iris.base_logic Require Import auth.
5 6
Import uPred.

7
Definition stackUR : ucmraT := gmapUR loc (dec_agreeR val).
8

9
Lemma stackR_self_op (h : stackUR) : h  h  h.
10 11 12 13 14 15 16 17 18
Proof.
  intros i. rewrite lookup_op.
  match goal with
    |- ?A  ?B  ?B => change B with A; destruct A as [c|]
  end; trivial.
  destruct c as [c|]; cbv -[equiv decide];
    try destruct decide; trivial; tauto.
Qed.

19
Class stackG Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
20
  StackG { stack_inG :> authG Σ stackUR; stack_name : gname }.
21 22

Section Rules.
23
  Context `{stackG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  Notation D := (prodC valC valC -n> iProp Σ).
25

Robbert Krebbers's avatar
Robbert Krebbers committed
26
  Definition stack_mapsto (l : loc) (v: val) : iProp Σ :=
27
    auth_own stack_name {[ l := DecAgree v ]}.
28 29 30

  Notation "l ↦ˢᵗᵏ v" := (stack_mapsto l v) (at level 20) : uPred_scope.

31
  Lemma stack_mapsto_dup l v : l ↦ˢᵗᵏ v  l ↦ˢᵗᵏ v  l ↦ˢᵗᵏ v.
32
  Proof.
33
    by rewrite /stack_mapsto /auth_own -own_op -auth_frag_op -stackR_self_op.
34 35
  Qed.

36
  Lemma stack_mapstos_agree l v w:
37
    l ↦ˢᵗᵏ v  l ↦ˢᵗᵏ w  l ↦ˢᵗᵏ v  l ↦ˢᵗᵏ w  v = w.
38 39 40
  Proof.
    iIntros "H".
    rewrite -own_op.
41
    iDestruct (own_valid _ with "H") as %Hvalid.
42
    rewrite own_op. unfold stack_mapsto, auth_own.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
    iDestruct "H" as "[$ $]".
44 45 46 47
    specialize (Hvalid l). rewrite lookup_op ?lookup_singleton in Hvalid.
    cbv -[decide] in Hvalid; destruct decide; trivial.
  Qed.

48
  Program Definition StackLink_pre (Q : D) : D -n> D := λne P v,
49
    ( l w, v.1 = LocV l  l ↦ˢᵗᵏ w 
50
            ((w = InjLV UnitV  v.2 = FoldV (InjLV UnitV)) 
51 52
            ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) 
              v.2 = FoldV (InjRV (PairV y2 z2))  Q (y1, y2)   P(z1, z2))))%I.
53
  Solve Obligations with solve_proper.
54

55
  Global Instance StackLink_pre_contractive Q : Contractive (StackLink_pre Q).
56 57 58 59 60
  Proof.
    intros n P1 P2 HP v; simpl. repeat (apply exist_ne => ?).
    repeat apply sep_ne; trivial. rewrite or_ne; trivial.
    repeat (apply exist_ne => ?).
    repeat apply sep_ne; trivial.
61
    apply later_contractive => i ?. by apply HP.
62 63
  Qed.

64 65 66 67
  Definition StackLink Q := fixpoint (StackLink_pre Q).

  Lemma StackLink_unfold Q v :
    StackLink Q v  ( l w,
68
      v.1 = LocV l  l ↦ˢᵗᵏ w 
69 70
      ((w = InjLV UnitV  v.2 = FoldV (InjLV UnitV)) 
      ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
71 72
                       v.2 = FoldV (InjRV (PairV y2 z2))
                       Q (y1, y2)   @StackLink Q (z1, z2))))%I.
73
  Proof. by rewrite {1}/StackLink fixpoint_unfold. Qed.
74 75 76

  Global Opaque StackLink. (* So that we can only use the unfold above. *)

77
  Lemma StackLink_dup (Q : D) v `{ vw, PersistentP (Q vw)} :
78
    StackLink Q v  StackLink Q v  StackLink Q v.
79
  Proof.
80
    iIntros "H". iLöb as "Hlat" forall (v). rewrite StackLink_unfold.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
    iDestruct "H" as (l w) "[% [Hl Hr]]"; subst.
82
    iDestruct (stack_mapsto_dup with "[Hl]") as "[Hl1 Hl2]"; first eauto.
83
    iDestruct "Hr" as "[#Hr|Hr]".
Robbert Krebbers's avatar
Robbert Krebbers committed
84 85 86
    { iSplitL "Hl1".
      - iExists _, _; iFrame "Hl1"; eauto.
      - iExists _, _; iFrame "Hl2"; eauto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
87
    iDestruct "Hr" as (y1 z1 y2 z2) "[#H1 [#H2 [#HQ H']]]".
Robbert Krebbers's avatar
Robbert Krebbers committed
88 89 90 91 92
    rewrite later_forall; setoid_rewrite later_wand.
    iDestruct ("Hlat" $! (z1, z2) with "H'") as "[HS1 HS2]".
    iSplitL "Hl1 HS1".
    - iExists _, _; iFrame "Hl1"; eauto 10.
    - iExists _, _; iFrame "Hl2"; eauto 10.
93 94
  Qed.

95
  Lemma stackR_valid (h : stackUR) (i : loc) :
96
     h  h !! i = None   v, h !! i = Some (DecAgree v).
97
  Proof.
98 99
    intros Hh; specialize (Hh i).
    by match type of Hh with
100 101 102 103 104 105 106 107
       ?A => match goal with
             | |- ?B = _  ( _, ?C = _) =>
               change B with A; change C with A;
                 destruct A as [[c|]|]; inversion H; eauto
             end
    end.
  Qed.

108
  Lemma stackR_alloc (h : stackUR) (i : loc) (v : val) :
Robbert Krebbers's avatar
Robbert Krebbers committed
109
    h !! i = None   h ~~>  (<[i := DecAgree v]> h)   {[i := DecAgree v]}.
110
  Proof.
111 112 113
    intros H1; apply cmra_total_update.
    intros n z H2. rewrite (insert_singleton_op h); auto.
    destruct z as [[ze |] zo];
114 115
      unfold validN, cmra_validN in *; simpl in *; trivial.
    destruct H2 as [H21 H22]; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
    - revert H21; rewrite !left_id. apply cmra_monoN_l.
117 118 119 120 121 122 123 124 125 126 127 128
    - intros j. rewrite lookup_op.
      destruct (decide (i = j)) as [|Hneq]; subst.
      + rewrite H1. rewrite lookup_singleton. constructor.
      + rewrite lookup_singleton_ne; trivial.
        specialize (H22 j).
        revert H22.
        match goal with
          |- {_} ?B  {_} (_  ?A) =>
          change B with A; destruct A; by try constructor
        end.
  Qed.

129 130 131 132 133 134 135 136
  Lemma dec_agree_valid_op_eq (x y : dec_agreeR val) :
     (Some x  Some y)  x = y.
  Proof.
    intros H1.
    destruct x as [x|]; destruct y as [y|]; trivial;
      cbv -[decide] in H1; try destruct decide; subst; simpl; intuition trivial.
  Qed.

137
  Lemma stackR_auth_is_subheap (h h' : stackUR) :
138
     ( h   h')   i x, h' !! i = Some x  h !! i = Some x.
139 140 141 142 143
  Proof.
    intros H1 i x H2.
    destruct H1 as [H11 H12]; simpl in H11.
    specialize (H11 1).
    destruct H11 as [z H11].
144
    revert H11; rewrite ucmra_unit_left_id => H11.
145
    eapply cmra_extend in H11; [| by apply cmra_valid_validN].
Robbert Krebbers's avatar
Robbert Krebbers committed
146
    destruct H11 as (z1 & z2 & H31 & H32 & H33); simpl in *.
147 148
    specialize (H32 i).
    assert (H4 :  (z1  z2))by (by rewrite -H31).
Robbert Krebbers's avatar
Robbert Krebbers committed
149
    apply leibniz_equiv.
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
    rewrite H31. rewrite lookup_op.
    specialize (H4 i). rewrite ?lookup_op in H4.
    revert H32; rewrite H2 => H32.
    match type of H32 with
      ?C {_} _ =>
      match goal with
        |- ?A  ?B  _ =>
        change C with A in *; destruct A as [a|]; inversion H32; subst
      end
    end.
    match type of H32 with
      ?C {_} _ =>
      match goal with
        |- ?A  ?B  _ => destruct B
      end
    end.
    - set (H5 := dec_agree_valid_op_eq _ _ H4); clearbody H5. subst.
167
      inversion H3; subst.
168 169
      destruct x as [x|]; cbv -[decide]; try destruct decide;
        constructor; intuition trivial.
170
    - inversion H3; subst. constructor; trivial.
171 172
  Qed.

173 174
  Context {iI : heapIG Σ}.

175
  Definition stack_owns (h : stackUR) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
176
    (own stack_name ( h)
177
         [ map] l  v  h, match v with
178 179 180
                             | DecAgree v' => l ↦ᵢ v'
                             | _ => True
                             end)%I.
181 182

  Lemma stack_owns_alloc E h l v :
183 184
    stack_owns h  l ↦ᵢ v
       |={E}=> stack_owns (<[l := DecAgree v]> h)  l ↦ˢᵗᵏ v.
185
  Proof.
186
    iIntros "[[Hown Hall] Hl]".
187
    iDestruct (own_valid _ with "Hown") as "#Hvalid".
188 189 190
    iDestruct (auth_validI _ with "Hvalid") as "[Ha' Hb]";
      simpl; iClear "Hvalid".
    iDestruct "Hb" as %H1.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
    iDestruct "Ha'" as (h') "Ha'"; iDestruct "Ha'" as %Ha'.
192 193 194 195 196 197
    rewrite ->(left_id _ _) in Ha'; setoid_subst.
    specialize (H1 l).
    match type of H1 with
       ?A => change A with (h' !! l) in H1
    end.
    destruct (h' !! l) as [[w|]|] eqn:Heq; inversion H1.
198
    - rewrite -{2}(insert_id _ _ _ Heq) -insert_delete.
199 200 201
      rewrite big_sepM_insert; [|apply lookup_delete_None; auto].
      iDestruct "Hall" as "[Hl' Hall]".
      iExFalso. iApply heap_mapsto_dup_invalid; by iFrame "Hl Hl'".
202
    - iMod (own_update with "Hown") as "Hown".
203
      by apply stackR_alloc.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
      iDestruct "Hown" as "[Hown Hl']".
205
      iModIntro. iSplitR "Hl'"; [|unfold stack_mapsto, auth_own; trivial].
206 207 208 209 210 211
      iCombine "Hl" "Hall" as "Hall".
      unfold stack_owns. iFrame "Hown".
      rewrite big_sepM_insert; trivial.
  Qed.

  Lemma stack_owns_open h l v :
212
    stack_owns h  l ↦ˢᵗᵏ v
Robbert Krebbers's avatar
Robbert Krebbers committed
213
       own stack_name ( h)
214
            ([ map] l  v  delete l h,
215 216 217
            match v with
            | DecAgree v' => l ↦ᵢ v'
            | DecAgreeBot => True
218
            end)  l ↦ᵢ v  l ↦ˢᵗᵏ v.
219 220 221 222
  Proof.
    iIntros "[[Hown Hall] Hl]".
    unfold stack_mapsto, auth_own.
    iCombine "Hown" "Hl" as "Hown".
223
    iDestruct (own_valid _ with "Hown") as %Hvalid.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
    iDestruct "Hown" as "[Hown Hl]".
225 226
    assert (Heq : h !! l = Some (DecAgree v)).
    eapply stackR_auth_is_subheap; eauto using lookup_singleton.
227
    rewrite -{1}(insert_id _ _ _ Heq) -insert_delete.
228
    rewrite big_sepM_insert; [|apply lookup_delete_None; auto].
229
    iDestruct "Hall" as "[$ $]"; by iFrame.
230 231 232
  Qed.

  Lemma stack_owns_close h l v :
Robbert Krebbers's avatar
Robbert Krebbers committed
233
    own stack_name ( h)
234
        ([ map] l  v  delete l h,
235 236 237 238
        match v with
        | DecAgree v' => l ↦ᵢ v'
        | DecAgreeBot => True
        end)
239
        l ↦ᵢ v  l ↦ˢᵗᵏ v  stack_owns h  l ↦ˢᵗᵏ v.
240 241 242 243
  Proof.
    iIntros "[Hown [Hall [Hl Hl']]]".
    unfold stack_mapsto, auth_own.
    iCombine "Hown" "Hl'" as "Hown".
244
    iDestruct (own_valid _ with "Hown") as %Hvalid.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
    iDestruct "Hown" as "[Hown Hl']".
246 247 248 249 250 251 252 253
    assert (Heq : h !! l = Some (DecAgree v)).
    eapply stackR_auth_is_subheap; eauto using lookup_singleton.
    iCombine "Hl" "Hall" as "Hall".
    rewrite -(big_sepM_insert (λ l v,
        match v with
        | DecAgree v' => (l ↦ᵢ v')%I
        | DecAgreeBot => True%I
        end) _ _ (DecAgree v)); eauto using lookup_delete.
254 255
    rewrite insert_delete insert_id; auto using lookup_delete.
    unfold stack_owns. by iFrame.
256 257
  Qed.

258
  Lemma stack_owns_open_close h l v :
259 260
    stack_owns h  l ↦ˢᵗᵏ v
       l ↦ᵢ v  (l ↦ᵢ v - (stack_owns h  l ↦ˢᵗᵏ v)).
261 262 263 264 265
  Proof.
    iIntros "[Howns Hls]".
    iDestruct (stack_owns_open with "[Howns Hls]") as "[Hh [Hm [Hl Hls]]]".
    { by iFrame "Howns Hls". }
    iFrame "Hl". iIntros "Hl".
266
    iApply stack_owns_close. by iFrame.
267
  Qed.
268 269

  Lemma stack_owns_later_open_close h l v :
270 271
     stack_owns h  l ↦ˢᵗᵏ v
        (l ↦ᵢ v  (l ↦ᵢ v - (stack_owns h  l ↦ˢᵗᵏ v))).
272
  Proof. iIntros "H". by iNext; iApply stack_owns_open_close. Qed.
273
End Rules.