stack_rules.v 7.41 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. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
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

Robbert Krebbers's avatar
Robbert Krebbers committed
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 
Robbert Krebbers's avatar
Robbert Krebbers committed
56
            ((w = InjLV #()  v.2 = FoldV (InjLV #())) 
Robbert Krebbers's avatar
Robbert Krebbers committed
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
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 
Robbert Krebbers's avatar
Robbert Krebbers committed
69
      ((w = InjLV #()  v.2 = FoldV (InjLV #())) 
Robbert Krebbers's avatar
Robbert Krebbers committed
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]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
    { iDestruct (big_sepM_lookup 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 115 116
        iFrame "Hown Hl'".
        iApply big_sepM_insert; eauto.
        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.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
    iIntros "[Howns Hls] Hl".
123
    iDestruct (own_valid_2 with "Howns Hl") 
Dan Frumin's avatar
Dan Frumin committed
124 125 126 127 128 129 130
      as %[[? [[av [Hav ?]]%equiv_Some_inv_r' Hav']]%singleton_included ?]%auth_valid_discrete_2.
    setoid_subst.
    apply -> Some_included_total in Hav'.
    move: Hav. rewrite lookup_fmap fmap_Some.
    move=> [v' [Hl Hav]]; subst.
    apply to_agree_included in Hav'; setoid_subst.
    iDestruct (big_sepM_lookup_acc with "Hls") as "[$ Hclose]"; first done.
131
    iIntros "Hl'". rewrite /prestack_owns. iFrame "Howns". by iApply "Hclose".
Dan Frumin's avatar
Dan Frumin committed
132
  Qed.
133

134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
  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 :
Robbert Krebbers's avatar
Robbert Krebbers committed
157
     stack_owns h - l ↦ˢᵗᵏ v -  (l ↦ᵢ v  (l ↦ᵢ v - stack_owns h)).
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
  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.

175
End Rules.