stack_rules.v 5.51 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
15 16

Definition stack_mapsto `{stackG Σ} (l : loc) (v : val) : iProp Σ :=
17
  own stack_name ( {[ l := to_agree v ]}).
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
25 26
  Global Instance stack_mapsto_persistent l v : PersistentP (l ↦ˢᵗᵏ v).
  Proof. apply _. Qed.
27 28 29
  
  (* TODO:this is bad*)
  Lemma stack_mapstos_agree_uncurried l v w : l ↦ˢᵗᵏ v  l ↦ˢᵗᵏ w  v = w.
30
  Proof.
31 32 33 34 35 36
    rewrite -own_op -auth_frag_op op_singleton.
    change (own stack_name ( {[l := to_agree v  to_agree w]}))
      with (auth_own stack_name {[l := to_agree v  to_agree w]}).
    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).
37 38
  Qed.

39 40 41 42 43 44
  Lemma stack_mapstos_agree l v w : l ↦ˢᵗᵏ v - l ↦ˢᵗᵏ w - v = w.
  Proof.
    iIntros "??".
    iApply stack_mapstos_agree_uncurried. by iFrame.
  Qed.
  
45 46 47 48
  (* stacklink Q := {((Loc l), nil)  l ↦ˢᵗᵏ (InjL #()) }
            {((Loc l), cons y2 z2)   y1 z1, l ↦ˢᵗᵏ (y1, z1) 
                                     (y1, y2)  Q
                                      stacklink Q (z1, z2) }*)
49
  Program Definition StackLink_pre (Q : D) : D -n> D := λne P v,
Robbert Krebbers's avatar
Robbert Krebbers committed
50
    ( l w, v.1 = LocV l  l ↦ˢᵗᵏ w 
Dan Frumin's avatar
Dan Frumin committed
51
            ((w = InjLV (LitV tt)  v.2 = FoldV (InjLV (LitV tt))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
52 53
            ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1)) 
              v.2 = FoldV (InjRV (PairV y2 z2))  Q (y1, y2)   P(z1, z2))))%I.
54
  Solve Obligations with solve_proper.
55

56
  Global Instance StackLink_pre_contractive Q : Contractive (StackLink_pre Q).
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  Proof. solve_contractive. Qed.
58

Robbert Krebbers's avatar
Robbert Krebbers committed
59
  Definition StackLink (Q : D) : D := fixpoint (StackLink_pre Q).
60 61 62

  Lemma StackLink_unfold Q v :
    StackLink Q v  ( l w,
Robbert Krebbers's avatar
Robbert Krebbers committed
63
      v.1 = LocV l  l ↦ˢᵗᵏ w 
Dan Frumin's avatar
Dan Frumin committed
64
      ((w = InjLV (LitV tt)  v.2 = FoldV (InjLV (LitV tt))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
65 66
      ( y1 z1 y2 z2, w = InjRV (PairV y1 (FoldV z1))
                       v.2 = FoldV (InjRV (PairV y2 z2))
67
                       Q (y1, y2)   StackLink Q (z1, z2))))%I.
68
  Proof. by rewrite {1}/StackLink fixpoint_unfold. Qed.
69 70 71

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

Robbert Krebbers's avatar
Robbert Krebbers committed
72 73
  Global Instance StackLink_persistent (Q : D) v `{ vw, PersistentP (Q vw)} :
    PersistentP (StackLink Q v).
74
  Proof. 
Robbert Krebbers's avatar
Robbert Krebbers committed
75
    iIntros "H". iLöb as "IH" forall (v). rewrite StackLink_unfold.
76 77 78 79 80 81 82 83
    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.
84 85
  Qed.

86
  Lemma stackR_alloc (h : stackUR) (i : loc) (v : val) :
87
    h !! i = None   h ~~>  (<[i := to_agree v]> h)   {[i := to_agree v]}.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
  Proof. intros. by apply auth_update_alloc, alloc_singleton_local_update. Qed.
89

Dan Frumin's avatar
Dan Frumin committed
90
  Context `{logrelG Σ}.
91

Dan Frumin's avatar
Dan Frumin committed
92 93 94
  Definition stack_owns (h : gmap loc val) : iProp Σ :=
    (own stack_name ( (to_agree <$> h : stackUR))
         [ map] l  v  h, l ↦ᵢ v)%I.
95

Robbert Krebbers's avatar
Robbert Krebbers committed
96
  Lemma stack_owns_alloc h l v :
Dan Frumin's avatar
Dan Frumin committed
97
    stack_owns h  l ↦ᵢ v == stack_owns (<[l := v]> h)  l ↦ˢᵗᵏ v.
98
  Proof.
99
    iIntros "[[Hown Hall] Hl]".
Dan Frumin's avatar
Dan Frumin committed
100 101
    iDestruct (own_valid with "Hown") as %Hvalid.
    destruct (h !! l) as [av|] eqn:Hhl.
Robbert Krebbers's avatar
Robbert Krebbers committed
102
    { iDestruct (big_sepM_lookup with "Hall") as "Hl'"; first done.
Dan Frumin's avatar
Dan Frumin committed
103 104 105 106 107 108 109 110 111 112 113
      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.
      - iModIntro. rewrite /stack_owns. rewrite fmap_insert.
        iFrame "Hown Hl'".
        iApply big_sepM_insert; eauto.
        by iFrame. }
114 115
  Qed.

116
  Lemma stack_owns_open_close h l v :
Robbert Krebbers's avatar
Robbert Krebbers committed
117
    stack_owns h - l ↦ˢᵗᵏ v - l ↦ᵢ v  (l ↦ᵢ v - stack_owns h).
118
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
    iIntros "[Howns Hls] Hl".
120
    iDestruct (own_valid_2 with "Howns Hl") 
Dan Frumin's avatar
Dan Frumin committed
121 122 123 124 125 126 127 128 129
      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.
    iIntros "Hl'". rewrite /stack_owns. iFrame "Howns". by iApply "Hclose".
  Qed.
130 131

  Lemma stack_owns_later_open_close h l v :
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
     stack_owns h - l ↦ˢᵗᵏ v -  (l ↦ᵢ v  (l ↦ᵢ v - stack_owns h)).
  Proof. iIntros "H1 H2". iNext; by iApply (stack_owns_open_close with "H1"). Qed.
134
End Rules.