refinement.v 14.2 KB
Newer Older
1 2 3
From iris.proofmode Require Import tactics.
From iris_logrel Require Import logrel.
From iris_logrel.examples.stack Require Import
4
  CG_stack FG_stack stack_rules.
5

6 7
Definition stackN : namespace := nroot .@ "stack".

8
Section Stack_refinement.
9
  Context `{logrelG Σ}.
10
  Notation D := (prodC valC valC -n> iProp Σ).
11
  Implicit Types Δ : listC D.
12
  Import lang.
13

14 15 16 17
  Definition sinv' {SPG : authG Σ stackUR} γ τi stk stk' l' : iProp Σ :=
    ( (istk : loc) v h, (prestack_owns γ h)
         stk' ↦ₛ v
         stk ↦ᵢ (FoldV #istk)
18
         preStackLink γ τi (#istk, v)
19 20 21
         l' ↦ₛ #false)%I.

  Context `{stackG Σ}.
22
  Definition sinv τi stk stk' l : iProp Σ :=
23
    ( (istk : loc) v h, (stack_owns h)
24
         stk' ↦ₛ v
25
         stk ↦ᵢ (FoldV #istk)
26
         StackLink τi (#istk, v)
27 28 29 30
         l ↦ₛ #false)%I.
  Lemma sinv_unfold τi stk stk' l :
    sinv τi stk stk' l = sinv' stack_name τi stk stk' l.
  Proof. reflexivity. Qed.
31 32 33 34 35

  Ltac close_sinv Hcl asn :=
    iMod (Hcl with asn) as "_";
    [iNext; rewrite /sinv; iExists _,_,_; by iFrame |]; try iModIntro.

36
  Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l Γ :
Dan Frumin's avatar
Dan Frumin committed
37
    N ## logrelN 
38
    inv N (sinv τi st st' l) -  τi (v,v') -
39
    Γ  (FG_push $/ (LitV (Loc st))) v log (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
40
  Proof.
41
    iIntros (?) "#Hinv #Hvv'". iIntros (Δ).
42 43 44 45
    Transparent FG_push.
    unfold FG_push. unlock. simpl_subst/=.
    iLöb as "IH".
    rel_rec_l.
46
    rel_load_l_atomic.
47
    iInv N as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
48 49
    iExists (FoldV #istk). iFrame.
    iModIntro. iNext. iIntros "Hst".
50 51
    close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
    rel_rec_l.
52 53
    rel_alloc_l as nstk "Hnstk". simpl.
    rel_cas_l_atomic.
54
    iInv N as (istk' w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
55 56
    iExists (FoldV #istk'). iFrame.
    iModIntro.
57
    destruct (decide (istk' = istk)) as [e | nestk]; subst.
58 59 60
    - (* CAS succeeds *)
      iSplitR; first by iIntros ([]).
      iIntros (?). iNext. iIntros "Hst".
61
      rel_apply_r (CG_push_r with "Hst' Hl").
62
      { solve_ndisj. }
63
      iIntros "Hst' Hl".
64 65 66 67
      iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
      iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]").
      { iNext. rewrite {2}/sinv. iExists _,_,_.
        iFrame "Hoe Hst' Hst Hl".
68
        rewrite (StackLink_unfold _ (# nstk, _)).
69
        iExists _, _. iSplitR; auto.
70 71
        iFrame "Hnstk".
        iRight. iExists _, _, _, _. auto. }
72
      rel_if_true_l.
73
      by rel_vals.
74 75 76
    - (* CAS fails *)
      iSplitL; last by (iIntros (?); congruence).
      iIntros (?); iNext; iIntros "Hst".
77 78 79 80
      close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
      rel_if_false_l. simpl.
      rel_rec_l.
      by iApply "IH".
81 82
  Qed.

83
  Lemma FG_CG_pop_refinement' N st st' (τi : D) l Δ Γ :
Dan Frumin's avatar
Dan Frumin committed
84
    N ## logrelN 
85
    inv N (sinv τi st st' l) -
86
    {τi::Δ;Γ}  (FG_pop $/ LitV (Loc st)) #() log (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
87
  Proof.
88
Transparent CG_locked_pop FG_pop CG_pop.
89
    iIntros (?) "#Hinv".
90
    iLöb as "IH".
91
    rewrite {2}/FG_pop. unlock.  simpl_subst/=.
92 93 94 95 96 97 98 99 100 101 102 103

replace ((rec: "pop" "st" <> :=
             let: "stv" := ! "st" in
             let: "x" := ! (Unfold "stv") in
             match: "x" with
               InjL <> => InjL #()
             | InjR "x" =>
               let: "y" := Fst "x" in let: "ys" := Snd "x" in if: CAS "st" "stv" "ys" then InjR "y" else ("pop" "st") #()
             end))%E with
(of_val FG_pop) by (by rewrite /FG_pop; unlock).

    rel_rec_l.
104
    rel_load_l_atomic.
105
    iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
106 107 108 109
    iExists _. iFrame.
    iModIntro. iNext. iIntros "Hst /=".
    rel_rec_l.
    rel_unfold_l.
110 111 112
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
113 114 115
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
116
      rel_apply_r (CG_pop_fail_r with "Hst' Hl").
117
      { solve_ndisj. }
118
      iIntros "Hst' Hl".
119 120
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'".
      rel_load_l_atomic.
121
      iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
122 123 124 125
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame "Histk_i".
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
126
      rel_rec_l.
127
      rel_case_l.
128
      rel_rec_l.
129 130 131 132

      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
      rel_vals.
      { iModIntro. iLeft. iExists (_,_). eauto. }
133 134
    - (* The stack has a value *)
      iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
135 136
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h.
      rel_load_l_atomic.
137
      iInv N as (istk v h) "[Hoe [Hst' [Hst [HLK Hl]]]]" "Hclose".
138 139 140 141
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame.
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
142
      rel_rec_l.
143
      rel_case_l.
144
      rel_rec_l.
145 146 147
      do 2 (rel_proj_l; rel_rec_l).
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h istk v.
      rel_cas_l_atomic.
148
      iInv N as (istk v h) "[Hoe [Hst' [Hst [HLK2 Hl]]]]" "Hclose".
149 150 151 152 153 154 155 156 157 158 159 160 161
      iExists _. iFrame.
      iModIntro.
      destruct (decide (istk = istk2)) as [? |NE]; simplify_eq/=.
      + (* CAS succeeds *)
        iSplitR; first by (iIntros (?); contradiction).
        iIntros "%". iNext. iIntros "Hst".
        rel_if_l.
        rewrite (StackLink_unfold _ (#istk2, v)).
        iDestruct "HLK2" as (istk2' v') "[% [#Histk' HLK2]]"; simplify_eq/=.
        iDestruct (stack_mapstos_agree with "Histk Histk'") as "%"; simplify_eq/=.
        iDestruct "HLK2" as "[[% %]|HLK2]"; simplify_eq/=.
        iDestruct "HLK2" as (ym1 ym2 zm1 zm2)
                              "[% [% [#Hrel #HLK2_tail]]]"; simplify_eq/=.
162
        rel_apply_r (CG_pop_suc_r with "Hst' Hl").
163
        { solve_ndisj. }
164
        iIntros "Hst' Hl".
165 166 167 168
        iMod ("Hclose" with "[-]").
        { iNext. rewrite /sinv.
          rewrite (StackLink_unfold _ (ym2, z2)).
          iDestruct "HLK_tail" as (yn2loc ?) "[% _]"; simplify_eq /=.
169 170 171 172 173 174 175 176
          iExists _,_,_. by iFrame. }
        rel_vals.
        { iModIntro. iRight.
          iExists (_,_). eauto. }
      + (* CAS fails *)
        iSplitL; last by (iIntros (?); congruence).
        iIntros (?). iNext. iIntros "Hst".
        rel_if_l.
177
        close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
178 179
        rel_rec_l.
        iApply "IH".
180
  Qed.
181

182
  Lemma FG_CG_pop_refinement st st' (τi : D) l Δ Γ :
183
    inv stackN (sinv τi st st' l) -
184
    {τi::Δ;Γ}  FG_pop $/ LitV (Loc st) log CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)).
185 186 187 188 189 190 191 192
  Proof.
    iIntros "#Hinv".
    iApply bin_log_related_arrow_val; eauto.
    { unlock FG_pop CG_locked_pop. reflexivity. }
    { unlock FG_pop CG_locked_pop. reflexivity. }
    { unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
    { unlock FG_pop CG_locked_pop. simpl_subst/=. solve_closed. }
    iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
193 194
    iApply (FG_CG_pop_refinement' stackN); eauto.
    { solve_ndisj. }
195 196
  Qed.

197
  Lemma FG_CG_iter_refinement st st' (τi : D) l Δ Γ:
198
    inv stackN (sinv τi st st' l) -
199
    {τi::Δ;Γ}  FG_read_iter $/ LitV (Loc st) log CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit.
200
  Proof.
201 202 203 204
    iIntros "#Hinv".
    Transparent FG_read_iter CG_snap_iter.
    unfold FG_read_iter, CG_snap_iter. unlock.
    simpl_subst/=.
205 206
    iApply bin_log_related_arrow_val; eauto.
    iAlways. iIntros (f1 f2) "#Hff /=".
207 208 209 210 211 212 213 214 215 216 217
    rel_rec_r.
    rel_rec_l.
    Transparent FG_iter CG_iter. unlock FG_iter CG_iter.
    rel_rec_l.
    rel_rec_r.
    Transparent CG_snap. unlock CG_snap.
    rel_rec_r.
    rel_rec_r.
    rel_rec_r.

    rel_load_l_atomic.
218
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
219 220 221 222 223 224 225 226 227 228 229 230 231 232
    iExists _. iFrame.
    iModIntro. iNext. iIntros "Hst /=".

    rel_apply_r (bin_log_related_acquire_r with "Hl").
    { solve_ndisj. }
    iIntros "Hl /=".
    rel_rec_r.
    rel_load_r.
    rel_rec_r.
    rel_apply_r (bin_log_related_release_r with "Hl").
    { solve_ndisj. }
    iIntros "Hl /=".
    rel_rec_r.
    close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h.
233 234

    iLöb as "IH" forall (istk v) "HLK".
235 236 237 238 239 240 241 242 243 244 245 246
    rel_rec_l.
    rel_unfold_l.
    rel_rec_r.
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
      rel_fold_r.
      rel_case_r.
      rel_rec_r.
247

248
      rel_load_l_atomic.
249
      iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
250 251 252 253 254 255
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame "Histk_i".
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
      rel_case_l.
      rel_rec_l.
256

257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". iClear "HLK".
      by rel_vals.
    - (* The stack has a value *)
      iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
      rel_fold_r.
      rel_case_r.
      rel_rec_r.
      rel_fst_r.

      rel_load_l_atomic.
      iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
      iDestruct (stack_owns_later_open_close with "Hoe Histk") as "[Histk_i Hoe]".
      iExists _. iFrame "Histk_i".
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
      rel_case_l.
      rel_rec_l.
      rel_fst_l.
      rel_rec_l.
      rel_snd_l.
      rel_rec_l.
278
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
279
      simpl.
280
      iApply (bin_log_related_app _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
281
      + iApply bin_log_related_arrow; eauto.
282
        iAlways. iIntros (? ?) "?"; simplify_eq/=.
283 284 285 286 287 288 289 290 291 292
        rel_rec_l.
        rel_rec_l.
        rel_rec_r.
        rel_rec_r.
        rel_proj_r.
        iPoseProof "HLK_tail" as "HLK_tail.bak".
        rewrite {1}StackLink_unfold.
        iDestruct "HLK_tail" as (? ?) "[% [? HLK_tail]]"; simplify_eq/=.
        by iApply "IH".
      + clear.
293 294
        iClear "IH Histk HLK_tail HLK HLK'".
        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
295
        iApply (related_ret with "[Hff]").
296
        done.
297
  Qed.
298

299 300 301 302 303
End Stack_refinement.

Section Full_refinement.
  Local Ltac replace_l c :=
    lazymatch goal with
304
    | [|- envs_entails _ (bin_log_related _ _ _ ?e _ _) ] =>
305 306 307 308
      replace e with c; last first
    end.
  Local Ltac replace_r c :=
    lazymatch goal with
309
    | [|- envs_entails _ (bin_log_related _ _ _ _ ?e' _) ] =>
310 311 312
      replace e' with c; last first
    end.

313
  (*  α. (α  Unit) * (Unit  Unit + α) * ((α  Unit)  Unit) *)
314
  Lemma FG_CG_stack_refinement `{SPG: stackPreG Σ, logrelG Σ} Δ Γ :
315
     {Δ;Γ}  FG_stack log CG_stack : TForall (TProd (TProd
316 317 318
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit)).
319
  Proof.
320 321
    unfold FG_stack. unfold CG_stack.
    iApply bin_log_related_tlam; auto.
322
    iIntros (τi) "!#".
323 324 325 326 327
    rel_alloc_r as l "Hl".
    rel_rec_r.
    rel_alloc_r as st' "Hst'".
    unlock CG_stack_body.
    repeat rel_rec_r.
328 329
    (* TODO: i have to do a bind before allocation, otherwise it doesn't pick the correct reduct. *)
    rel_bind_l (ref (InjL #()))%E.
330 331 332 333 334
    rel_alloc_l as istk "Histk".
    simpl.
    rel_alloc_l as st "Hst".
    simpl.
    rel_rec_l.
335
    iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
336 337
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
338 339
    change (@stack_pre_inG _ SPG) with (@stack_inG _ istkG).
    clearbody istkG. clear γ SPG.
340
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
341
    { rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty.
342 343
      iFrame "Hemp". }
    iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
344
    iAssert (StackLink τi (#istk, FoldV (InjLV Unit))) with "[Histk]" as "#HLK".
345 346
    { rewrite StackLink_unfold.
      iExists _, _. iSplitR; simpl; trivial.
347 348 349 350 351 352 353 354 355 356 357 358
      iFrame "Histk". iLeft. iSplit; trivial. }
    iAssert (sinv τi st st' l) with "[Hoe Hst Hst' HLK Hl]" as "Hinv".
    { iExists _, _, _. by iFrame. }
    iMod (inv_alloc stackN with "[Hinv]") as "#Hinv".
    { iNext. iExact "Hinv". }
    unlock FG_stack_body.
    unlock FG_push.
    repeat rel_rec_l.
    unlock FG_pop.
    repeat rel_rec_l. simpl_subst/=.
    unlock FG_read_iter.
    repeat rel_rec_l.
359

360 361 362 363 364 365 366 367
    unlock CG_locked_push. simpl_subst/=.
    repeat rel_rec_r.
    unlock CG_locked_pop. simpl_subst/=.
    repeat rel_rec_r.
    unlock CG_snap_iter. simpl_subst/=.
    repeat rel_rec_r.

    repeat iApply bin_log_related_pair.
368 369
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "#Hτ /=".
370
      replace_l ((FG_push $/ LitV (Loc st)) v1)%E.
371
      { unlock FG_push. simpl_subst/=. reflexivity. }
372
      replace_r ((CG_locked_push $/ LitV (Loc st') $/ LitV (Loc l)) v2)%E.
373 374
      { unlock CG_locked_push. simpl_subst/=. reflexivity. }
      iApply (FG_CG_push_refinement with "Hinv Hτ").
375
      { solve_ndisj. }
376
    - replace_l (FG_pop $/ LitV (Loc st))%E.
377
      { unlock FG_pop. by simpl_subst/=. }
378
      replace_r (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E.
379 380
      { unlock CG_locked_pop. by simpl_subst/=. }
      iApply (FG_CG_pop_refinement with "Hinv").
381
    - replace_l (FG_read_iter $/ LitV (Loc st))%E.
382
      { unlock FG_read_iter. by simpl_subst/=. }
383
      replace_r (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E.
384 385
      { unlock CG_snap_iter. by simpl_subst/=. }
      iApply (FG_CG_iter_refinement with "Hinv").
386
  Qed.
387

388 389 390 391 392 393 394 395 396 397 398
  Theorem stack_ctx_refinement :
      FG_stack ctx CG_stack :
      TForall (TProd (TProd (TArrow (TVar 0) TUnit)
                            (TArrow TUnit (TSum TUnit (TVar 0))))
                            (TArrow (TArrow (TVar 0) TUnit) TUnit)).
  Proof.
    set (Σ := #[logrelΣ; GFunctor (authR stackUR)]).
    eapply (logrel_ctxequiv Σ); [solve_closed.. | intros ].
    apply FG_CG_stack_refinement.
  Qed.
End Full_refinement.