peritem.v 9.12 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
3
4
5
6
7
8
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import frac auth upred gmap dec_agree upred_big_op csum.
From iris_atomic Require Export treiber misc evmap.

Section defs.
  Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
Zhen Zhang's avatar
Zhen Zhang committed
9
  Context (R: val  iProp Σ) `{ x, TimelessP (R x)}.
Zhen Zhang's avatar
Zhen Zhang committed
10
11
12

  Definition allocated hd := ( q v, hd {q} v)%I.

Zhen Zhang's avatar
Zhen Zhang committed
13
  Definition evs (γ: gname) := ev loc val γ.
Zhen Zhang's avatar
Zhen Zhang committed
14

Zhen Zhang's avatar
Zhen Zhang committed
15
  Fixpoint is_list' (γ: gname) (hd: loc) (xs: list val) : iProp Σ :=
Zhen Zhang's avatar
Zhen Zhang committed
16
17
    match xs with
    | [] => ( q, hd { q } NONEV)%I
Zhen Zhang's avatar
Zhen Zhang committed
18
    | x :: xs => ( (hd': loc) q, hd {q} SOMEV (x, #hd')  evs γ hd x  is_list' γ hd' xs)%I
Zhen Zhang's avatar
Zhen Zhang committed
19
20
    end.

Zhen Zhang's avatar
Zhen Zhang committed
21
  Lemma in_list' γ x xs:
Zhen Zhang's avatar
Zhen Zhang committed
22
     hd, x  xs 
Zhen Zhang's avatar
Zhen Zhang committed
23
24
          is_list' γ hd xs
            (hd' hd'': loc) q, hd' {q} SOMEV (x, #hd'')  evs γ hd' x.
Zhen Zhang's avatar
Zhen Zhang committed
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
  Proof.
    induction xs as [|x' xs' IHxs'].
    - intros ? Hin. inversion Hin.
    - intros hd Hin. destruct (decide (x = x')) as [->|Hneq].
      + iIntros "Hls". simpl.
        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
        iExists hd, hd', q. iFrame.
      + assert (x  xs') as Hin'; first set_solver.
        iIntros "Hls". simpl.
        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
        iApply IHxs'=>//.
  Qed.

  Definition perR' hd v v' := (v = ((: unitR), DecAgree v')  R v'  allocated hd)%I.
  Definition perR  hd v := ( v', perR' hd v v')%I.
  
Zhen Zhang's avatar
Zhen Zhang committed
41
  Definition allR γ := ( m : evmapR loc val unitR, own γ ( m)  [ map] hd  v  m, perR hd v)%I.
Zhen Zhang's avatar
Zhen Zhang committed
42

Zhen Zhang's avatar
Zhen Zhang committed
43
44
  Definition is_stack' γ xs s :=
    ( hd: loc, s  #hd  is_list' γ hd xs  allR γ)%I.
Zhen Zhang's avatar
Zhen Zhang committed
45

Zhen Zhang's avatar
Zhen Zhang committed
46
  Global Instance is_list'_timeless γ hd xs: TimelessP (is_list' γ hd xs).
Zhen Zhang's avatar
Zhen Zhang committed
47
48
  Proof. generalize hd. induction xs; apply _. Qed.

Zhen Zhang's avatar
Zhen Zhang committed
49
  Global Instance is_stack'_timeless γ xs s: TimelessP (is_stack' γ xs s).
Zhen Zhang's avatar
Zhen Zhang committed
50
51
  Proof. apply _. Qed.

Zhen Zhang's avatar
Zhen Zhang committed
52
53
  Lemma dup_is_list' γ :  xs hd,
    heap_ctx  is_list' γ hd xs  |=r=> is_list' γ hd xs  is_list' γ hd xs.
Zhen Zhang's avatar
Zhen Zhang committed
54
55
56
57
58
59
60
61
62
63
  Proof.
    induction xs as [|y xs' IHxs'].
    - iIntros (hd) "(#? & Hs)".
      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
    - iIntros (hd) "(#? & Hs)". simpl.
      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hev & Hs')".
      iDestruct (IHxs' with "[Hs']") as "==>[Hs1 Hs2]"; first by iFrame.
      iVsIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
64
65
  Lemma extract_is_list γ :  xs hd,
    heap_ctx  is_list' γ hd xs  |=r=> is_list' γ hd xs  is_list hd xs.
Zhen Zhang's avatar
Zhen Zhang committed
66
67
68
69
70
71
72
73
74
75
  Proof.
    induction xs as [|y xs' IHxs'].
    - iIntros (hd) "(#? & Hs)".
      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
    - iIntros (hd) "(#? & Hs)". simpl.
      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hev & Hs')".
      iDestruct (IHxs' with "[Hs']") as "==>[Hs1 Hs2]"; first by iFrame.
      iVsIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
76
77
  Definition f_spec γ (xs: list val) (s hd: loc) (f: val) (Rf RI: iProp Σ) :=
    (* Rf, RI are some frames *)
Zhen Zhang's avatar
Zhen Zhang committed
78
79
     Φ (x: val),
      heapN  N  x  xs 
Zhen Zhang's avatar
Zhen Zhang committed
80
81
      heap_ctx  inv N (( xs, is_stack' γ xs s)  RI) 
      (is_list' γ hd xs  Rf)  (is_list' γ hd xs - Rf - Φ #())
Zhen Zhang's avatar
Zhen Zhang committed
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
       WP f x {{ Φ }}.
End defs.

Section proofs.
  Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
  Context (R: val  iProp Σ).

Lemma new_stack_spec' Φ RI:
    heapN  N 
    heap_ctx  RI  ( γ s : loc, inv N (( xs, is_stack' R γ xs s)  RI) - Φ #s)
     WP new_stack #() {{ Φ }}.
  Proof.
    iIntros (HN) "(#Hh & HR & HΦ)".
    iVs (own_alloc ( (: evmapR loc val unitR)   )) as (γ) "[Hm Hm']".
    { apply auth_valid_discrete_2. done. }
    wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
    wp_alloc s as "Hs".
    iAssert (( xs : list val, is_stack' R γ xs s)  RI)%I with "[-HΦ Hm']" as "Hinv".
    { iFrame. iExists [], l. iFrame. simpl. iSplitL "Hl".
      - eauto.
      - iExists . iSplitL. iFrame. by iApply (big_sepM_empty (fun hd v => perR R hd v)). }
    iVs (inv_alloc N _ (( xs : list val, is_stack' R γ xs s)  RI)%I with "[-HΦ Hm']") as "#?"; first eauto.
    by iApply "HΦ".
  Qed.
    
  Lemma iter_spec Φ γ s (Rf RI: iProp Σ):
     xs hd (f: expr) (f': val),
Zhen Zhang's avatar
Zhen Zhang committed
109
      heapN  N  f_spec N R γ xs s hd f' Rf RI  to_val f = Some f' 
Zhen Zhang's avatar
Zhen Zhang committed
110
111
112
113
114
115
116
117
118
      heap_ctx  inv N (( xs, is_stack' R γ xs s)  RI) 
      is_list' γ hd xs  Rf  (Rf - Φ #())
       WP (iter #hd) f {{ v, Φ v }}.
  Proof.
    induction xs as [|x xs' IHxs'].
    - simpl. iIntros (hd f f' HN ? ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
      iDestruct "Hxs1" as (q) "Hhd".
      wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. by iApply "HΦ".
    - simpl. iIntros (hd f f' HN Hf ?) "(#Hh & #? & Hxs1 & HRf & HΦ)".
Zhen Zhang's avatar
Zhen Zhang committed
119
      iDestruct "Hxs1" as (hd2 q) "(Hhd & #Hev & Hhd2)".
Zhen Zhang's avatar
Zhen Zhang committed
120
      wp_rec. wp_value. iVsIntro. wp_let. wp_load. wp_match. wp_proj.
Zhen Zhang's avatar
Zhen Zhang committed
121
122
123
124
125
      wp_bind (f' _). iApply Hf=>//; first set_solver.
      iFrame "#". simpl.
      iSplitL "Hev Hhd Hhd2 HRf".
      { iFrame. iExists hd2, q. iFrame. }
      iIntros "Hls HRf".
Zhen Zhang's avatar
Zhen Zhang committed
126
127
128
129
      wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
      + rewrite /f_spec. iIntros (? ? ? ?) "(#? & #? & ? & ?)".
        iApply Hf=>//.
        * set_solver.
Zhen Zhang's avatar
Zhen Zhang committed
130
131
        * iFrame "#".
            by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
      + apply to_of_val.
      + iFrame "#". by iFrame.
  Qed.
  
  Lemma push_spec Φ γ (s: loc) (x: val) RI:
    heapN  N 
    heap_ctx  R x  inv N (( xs, is_stack' R γ xs s)  RI)  (( hd, evs γ hd x) - Φ #())
     WP push #s x {{ Φ }}.
  Proof.
    iIntros (HN) "(#Hh & HRx & #? & HΦ)".
    iDestruct (push_atomic_spec N s x with "Hh") as "Hpush"=>//.
    iSpecialize ("Hpush" $! (R x) (fun _ ret => ( hd, evs γ hd x)  ret = #())%I with "[]").
    - iIntros "!# Rx".
      (* open the invariant *)
      iInv N as "[IH1 ?]" "Hclose".
      iDestruct "IH1" as (xs hd) "[>Hs [>Hxs HR]]".
      iDestruct (extract_is_list with "[Hxs]") as "==>[Hxs Hxs']"; first by iFrame.
      iDestruct (dup_is_list with "[Hxs']") as "[Hxs'1 Hxs'2]"; first by iFrame.
      (* mask magic *)
151
152
153
      iVs (pvs_intro_mask' (  nclose N) heapN) as "Hvs"; first set_solver.
      iVsIntro. iExists (xs, hd).
      iFrame "Hs Hxs'1". iSplit.
Zhen Zhang's avatar
Zhen Zhang committed
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
      + (* provide a way to rollback *)
        iIntros "[Hs Hl']".
        iVs "Hvs". iVs ("Hclose" with "[-Rx]"); last done.
        { iNext. iFrame. iExists xs. iExists hd. by iFrame. }
      + (* provide a way to commit *)
        iIntros (v) "Hs".
        iDestruct "Hs" as (hd') "[% [Hs [[Hhd'1 Hhd'2] Hxs']]]". subst.
        iVs "Hvs".
        iDestruct "HR" as (m) "[>Hom HRm]".
        destruct (m !! hd') eqn:Heqn.
        * iDestruct (big_sepM_delete_later (perR R) m with "HRm") as "[Hx ?]"=>//.
          iDestruct "Hx" as (?) "(_ & _ & >Hhd'')".
          iDestruct (heap_mapsto_op_1 with "[Hhd'1 Hhd'2]") as "[_ Hhd]"; first iFrame.
          rewrite Qp_div_2.
          iDestruct "Hhd''" as (q v) "Hhd''". iExFalso.
          iApply (bogus_heap hd' 1%Qp q); first apply Qp_not_plus_q_ge_1.
          iFrame "#". iFrame.
        * iAssert (evs γ hd' x   (allR R γ))%I
                  with "==>[Rx Hom HRm Hhd'1]" as "[#Hox ?]".
          {
            iDestruct (evmap_alloc _ _ _ m with "[Hom]") as "==>[Hom Hox]"=>//.
            iDestruct (big_sepM_insert_later (perR R) m) as "H"=>//.
            iSplitL "Hox".
            { rewrite /evs /ev. eauto. }
            iExists (<[hd' := ((), DecAgree x)]> m).
            iFrame. iApply "H". iFrame. iExists x.
            iFrame. rewrite /allocated. iSplitR "Hhd'1"; auto.
          }
          iVs ("Hclose" with "[-]").
          { iNext. iFrame. iExists (x::xs).
            iExists hd'. iFrame.
            iExists hd, (1/2)%Qp. by iFrame.
          }
        iVsIntro. iSplitL; last auto. by iExists hd'.
    - iApply wp_wand_r. iSplitL "HRx Hpush".
      + by iApply "Hpush".
      + iIntros (?) "H". iDestruct "H" as (_) "[? %]". subst.
        by iApply "HΦ".
  Qed.

  (* some helpers *)
  Lemma access (γ: gname) (x: val) (xs: list val) (m: evmapR loc val unitR) :
     hd: loc,
    x  xs  
     ([ map] hdv  m, perR R hd v)  own γ ( m) 
    is_list' γ hd xs
      hd',  ([ map] hdv  delete hd' m, perR R hd v) 
              perR R hd' ((: unitR), DecAgree x)  m !! hd' = Some ((: unitR), DecAgree x)  own γ ( m).
  Proof.
    induction xs as [|x' xs' IHxs'].
    - iIntros (? Habsurd). inversion Habsurd.
    - destruct (decide (x = x')) as [->|Hneq].
      + iIntros (hd _) "(HR & Hom & Hxs)".
        simpl. iDestruct "Hxs" as (hd' q) "[Hhd [#Hev Hxs']]".
Zhen Zhang's avatar
Zhen Zhang committed
208
209
210
211
        rewrite /evs.
        iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame.
        iDestruct (big_sepM_delete_later (perR R) m with "HR") as "[Hp HRm]"=>//.
        iExists hd. by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
212
213
214
215
216
217
218
219
220
      + iIntros (hd ?).
        assert (x  xs'); first set_solver.
        iIntros "(HRs & Hom & Hxs')".
        simpl. iDestruct "Hxs'" as (hd' q) "[Hhd [Hev Hxs']]".
        iDestruct (IHxs' hd' with "[HRs Hxs' Hom]") as "?"=>//.
        iFrame.
  Qed.

End proofs.