stack_rules.v 7.5 KB
Newer Older
1
From iris.algebra Require Import gmap agree.
2 3
From iris.base_logic.lib Require Export auth.
From iris_logrel Require Export logrel.
4

5 6
Import uPred.

7
Definition stackUR : ucmraT := gmapUR loc (agreeR valC).
8 9

Class stackG Σ :=
10
  StackG { stack_inG :> authG Σ stackUR; stack_name : gname }.
11 12 13 14
Class stackPreG Σ := StackPreG { stack_pre_inG :> authG Σ stackUR }.
Definition stackΣ : gFunctors := #[authΣ stackUR].
Instance subG_stackPreG {Σ} : subG stackΣ Σ  stackPreG Σ.
Proof. solve_inG. Qed.
15 16
(* Instance stackG_stackPreG {Σ} : stackG Σ  stackPreG Σ. *)
(* Proof. intros [S ?]. by constructor. Qed. *)
17

18 19 20 21
Definition prestack_mapsto `{authG Σ stackUR} (γ : gname) (l : loc) (v : val) : iProp Σ :=
  own γ ( {[ l := to_agree v ]}).

Definition stack_mapsto `{stackG Σ} l v : iProp Σ := prestack_mapsto stack_name l v.
22 23

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

25 26 27
Section Rules_pre.
  Context `{authG Σ stackUR}.
  Variable (γ : gname).
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  Notation D := (prodC valC valC -n> iProp Σ).
29
  Notation "l ↦ˢᵗᵏ v" := (prestack_mapsto γ l v) (at level 20) : uPred_scope.
30

31 32
  Global Instance stack_mapsto_persistent l v : PersistentP (l ↦ˢᵗᵏ v).
  Proof. apply _. Qed.
33
  
34
  Lemma prestack_mapstos_agree_uncurried l v w : l ↦ˢᵗᵏ v  l ↦ˢᵗᵏ w  v = w.
35
  Proof.
36
    rewrite -own_op -auth_frag_op op_singleton.
37 38
    change (own γ ( {[l := to_agree v  to_agree w]}))
      with (auth_own γ {[l := to_agree v  to_agree w]}).
39 40 41
    rewrite auth_own_valid. iIntros "Hvalid". iDestruct "Hvalid" as %Hvalid.
    rewrite singleton_valid in Hvalid *.
    intros Hagree. by rewrite (agree_op_inv' v w Hagree).
42 43
  Qed.

44
  Lemma prestack_mapstos_agree l v w : l ↦ˢᵗᵏ v - l ↦ˢᵗᵏ w - v = w.
45 46
  Proof.
    iIntros "??".
47
    iApply prestack_mapstos_agree_uncurried. by iFrame.
48 49
  Qed.
  
50 51 52 53
  (* stacklink Q := {((Loc l), nil)  l ↦ˢᵗᵏ (InjL #()) }
            {((Loc l), cons y2 z2)   y1 z1, l ↦ˢᵗᵏ (y1, z1) 
                                     (y1, y2)  Q
                                      stacklink Q (z1, z2) }*)
54
  Program Definition preStackLink_pre (Q : D) : D -n> D := λne P v,
55
    ( (l : loc) w, v.1 = # l  l ↦ˢᵗᵏ w 
56
            ((w = InjLV #()  v.2 = FoldV (InjLV #())) 
57 58
            ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) 
              v.2 = FoldV (InjRV (PairV y2 z2))  Q (y1, y2)   P(z1, z2))))%I.
59
  Solve Obligations with solve_proper.
60

61
  Global Instance StackLink_pre_contractive Q : Contractive (preStackLink_pre Q).
62
  Proof. solve_contractive. Qed.
63

64
  Definition preStackLink (Q : D) : D := fixpoint (preStackLink_pre Q).
65

66 67
  Lemma preStackLink_unfold Q v :
    preStackLink Q v  ( (l : loc) w,
68
      v.1 = # l  l ↦ˢᵗᵏ w 
69
      ((w = InjLV #()  v.2 = FoldV (InjLV #())) 
70 71
      ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
                       v.2 = FoldV (InjRV (PairV y2 z2))
72 73
                       Q (y1, y2)   preStackLink Q (z1, z2))))%I.
  Proof. by rewrite {1}/preStackLink fixpoint_unfold. Qed.
74

75
  Global Opaque preStackLink. (* So that we can only use the unfold above. *)
76

77 78
  Global Instance preStackLink_persistent (Q : D) v `{ vw, PersistentP (Q vw)} :
    PersistentP (preStackLink Q v).
79
  Proof. 
80
    iIntros "H". iLöb as "IH" forall (v). rewrite preStackLink_unfold.
81 82 83 84 85 86 87 88
    iDestruct "H" as (l w) "[% [#Hl [[% %]|Hr]]]"; subst.
    { iExists l, _; iAlways; eauto. }
    iDestruct "Hr" as (y1 z1 y2 z2) "[% [% [#HQ Hrec]]]"; subst.    
    rewrite later_forall. 
    iSpecialize ("IH" $! (z1, z2)). rewrite later_wand. 
    iSpecialize ("IH" with "Hrec"). rewrite -always_later.
    iDestruct "IH" as "#IH".
    iAlways. iExists _,_; eauto 20.
89 90
  Qed.

91
  Lemma stackR_alloc (h : stackUR) (i : loc) (v : val) :
92
    h !! i = None   h ~~>  (<[i := to_agree v]> h)   {[i := to_agree v]}.
93
  Proof. intros. by apply auth_update_alloc, alloc_singleton_local_update. Qed.
94

95 96
  Definition prestack_owns `{logrelG Σ} (h : gmap loc val) : iProp Σ :=
    (own γ ( (to_agree <$> h : stackUR))
Dan Frumin's avatar
Dan Frumin committed
97
         [ map] l  v  h, l ↦ᵢ v)%I.
98

99 100
  Lemma prestack_owns_alloc `{logrelG Σ} h l v :
    prestack_owns h  l ↦ᵢ v == prestack_owns (<[l := v]> h)  l ↦ˢᵗᵏ v.
101
  Proof.
102
    iIntros "[[Hown Hall] Hl]".
Dan Frumin's avatar
Dan Frumin committed
103 104
    iDestruct (own_valid with "Hown") as %Hvalid.
    destruct (h !! l) as [av|] eqn:Hhl.
Dan Frumin's avatar
Dan Frumin committed
105
    { iDestruct (big_sepM_lookup _ h l with "Hall") as "Hl'"; first done.
Dan Frumin's avatar
Dan Frumin committed
106 107 108 109 110 111 112
      iDestruct (@mapsto_valid_2 loc val with "Hl Hl'") as %Hval.
      cbv in Hval. exfalso; by apply Hval. }
    { iMod (own_update with "Hown") as "[Hown Hl']".
      eapply auth_update_alloc.
      eapply (alloc_singleton_local_update _ l (to_agree v)).
      - rewrite lookup_fmap Hhl. by compute.
      - by compute.
113
      - iModIntro. rewrite /prestack_owns. rewrite fmap_insert.
Dan Frumin's avatar
Dan Frumin committed
114
        iFrame "Hown Hl'".
Dan Frumin's avatar
Dan Frumin committed
115
        iApply (big_sepM_insert _ h l); eauto.
Dan Frumin's avatar
Dan Frumin committed
116
        by iFrame. }
117 118
  Qed.

119 120
  Lemma prestack_owns_open_close `{logrelG Σ} h l v :
    prestack_owns h - l ↦ˢᵗᵏ v - l ↦ᵢ v  (l ↦ᵢ v - prestack_owns h).
121
  Proof.
122
    iIntros "[Howns Hls] Hl".
123
    iDestruct (own_valid_2 with "Howns Hl") 
Dan Frumin's avatar
Dan Frumin committed
124 125
      as %[[? [[av [Hav ?]]%equiv_Some_inv_r' Hav']]%singleton_included ?]%auth_valid_discrete_2.
    setoid_subst.
Dan Frumin's avatar
Dan Frumin committed
126 127
    (* TODO: ask Robbert why did I have to change this *)
    apply -> @Some_included_total in Hav'; [| apply _].
Dan Frumin's avatar
Dan Frumin committed
128 129 130
    move: Hav. rewrite lookup_fmap fmap_Some.
    move=> [v' [Hl Hav]]; subst.
    apply to_agree_included in Hav'; setoid_subst.
Dan Frumin's avatar
Dan Frumin committed
131
    iDestruct (big_sepM_lookup_acc _ h l with "Hls") as "[$ Hclose]"; first done.
132
    iIntros "Hl'". rewrite /prestack_owns. iFrame "Howns". by iApply "Hclose".
Dan Frumin's avatar
Dan Frumin committed
133
  Qed.
134

135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
  Lemma prestack_owns_later_open_close `{logrelG Σ} h l v :
     prestack_owns h - l ↦ˢᵗᵏ v -  (l ↦ᵢ v  (l ↦ᵢ v - prestack_owns h)).
  Proof. iIntros "H1 H2". iNext; by iApply (prestack_owns_open_close with "H1"). Qed.
End Rules_pre.

Section Rules.
  Context `{stackG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).

  Definition stack_owns `{logrelG Σ} := prestack_owns stack_name.

  Lemma stack_mapstos_agree l v w : l ↦ˢᵗᵏ v - l ↦ˢᵗᵏ w - v = w.
  Proof. apply prestack_mapstos_agree. Qed.

  Lemma stack_owns_alloc `{logrelG Σ} h l v :
    stack_owns h  l ↦ᵢ v == stack_owns (<[l := v]> h)  l ↦ˢᵗᵏ v.
  Proof. apply prestack_owns_alloc. Qed.

  Lemma stack_owns_open_close `{logrelG Σ} h l v :
    stack_owns h - l ↦ˢᵗᵏ v - l ↦ᵢ v  (l ↦ᵢ v - stack_owns h).
  Proof. apply prestack_owns_open_close. Qed.

  Lemma stack_owns_later_open_close `{logrelG Σ} h l v :
158
     stack_owns h - l ↦ˢᵗᵏ v -  (l ↦ᵢ v  (l ↦ᵢ v - stack_owns h)).
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175
  Proof. apply prestack_owns_later_open_close. Qed.

  Definition StackLink Q v := preStackLink stack_name Q v.
  Lemma StackLink_unfold Q v :
    StackLink Q v  ( (l : loc) w,
      v.1 = # l  l ↦ˢᵗᵏ w 
      ((w = InjLV #()  v.2 = FoldV (InjLV #())) 
      ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
                       v.2 = FoldV (InjRV (PairV y2 z2))
                       Q (y1, y2)   StackLink Q (z1, z2))))%I.
  Proof. by rewrite /StackLink preStackLink_unfold. Qed.

  Global Instance StackLink_persistent (Q : D) v `{ vw, PersistentP (Q vw)} :
    PersistentP (StackLink Q v).
  Proof. apply _. Qed.
  Global Opaque StackLink.

176
End Rules.