refinement.v 14.3 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
Robbert Krebbers's avatar
Robbert Krebbers committed
4
  CG_stack FG_stack stack_rules.
5

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

8
Section Stack_refinement.
Dan Frumin's avatar
Dan Frumin committed
9
  Context `{logrelG Σ, stackG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  Notation D := (prodC valC valC -n> iProp Σ).
11
  Implicit Types Δ : listC D.
12
  Import lang.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

Robbert Krebbers's avatar
Robbert Krebbers committed
14 15
  Definition sinv τi stk stk' l' {SH: stackG Σ} : iProp Σ :=
    ( (istk : loc) v h, (stack_owns h)
16
         stk' ↦ₛ v
Robbert Krebbers's avatar
Robbert Krebbers committed
17
         stk ↦ᵢ (FoldV #istk)
18
         StackLink τi (#istk, v)
Robbert Krebbers's avatar
Robbert Krebbers committed
19
         l' ↦ₛ #false)%I.
20 21 22 23 24

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

Dan Frumin's avatar
Dan Frumin committed
25 26
  Lemma FG_CG_push_refinement st st' (τi : D) (v v' : val) l {τP :  ww, PersistentP (τi ww)} Γ :
    inv stackN (sinv τi st st' l) - τi (v,v') -
Robbert Krebbers's avatar
Robbert Krebbers committed
27
    Γ  (FG_push $/ (LitV (Loc st))) v log (CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v' : TUnit.
28
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
    iIntros "#Hinv #Hvv'" (Δ).
30 31 32 33
    Transparent FG_push.
    unfold FG_push. unlock. simpl_subst/=.
    iLöb as "IH".
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
34 35 36 37
    rel_load_l_atomic.
    iInv stackN as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
    iExists (FoldV #istk). iFrame.
    iModIntro. iNext. iIntros "Hst".
38 39
    close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
40 41 42 43 44
    rel_alloc_l as nstk "Hnstk". simpl.
    rel_cas_l_atomic.
    iInv stackN as (istk' w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
    iExists (FoldV #istk'). iFrame.
    iModIntro.
45
    destruct (decide (istk' = istk)) as [e | nestk]; subst.
Dan Frumin's avatar
Dan Frumin committed
46 47 48
    - (* CAS succeeds *)
      iSplitR; first by iIntros ([]).
      iIntros (?). iNext. iIntros "Hst".
49
      rel_apply_r (CG_push_r with "Hst' Hl").
50
      { solve_ndisj. }
51
      iIntros "Hst' Hl".
52 53
      iApply fupd_logrel'. (* TODO iMod should pick this up on its own *)
      iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
54
      iModIntro.
55 56 57
      iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]").
      { iNext. rewrite {2}/sinv. iExists _,_,_.
        iFrame "Hoe Hst' Hst Hl".
58
        rewrite (StackLink_unfold _ (# nstk, _)).
59 60 61
        iExists _, _. iSplitR; auto. 
        iFrame "Hnstk".
        iRight. iExists _, _, _, _. auto. }
Dan Frumin's avatar
Dan Frumin committed
62
      rel_if_true_l.
63
      by rel_vals.
Dan Frumin's avatar
Dan Frumin committed
64 65 66
    - (* CAS fails *)
      iSplitL; last by (iIntros (?); congruence).
      iIntros (?); iNext; iIntros "Hst".
67 68 69 70
      close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
      rel_if_false_l. simpl.
      rel_rec_l.
      by iApply "IH".
71 72
  Qed.

73
  Lemma FG_CG_pop_refinement' st st' (τi : D) l {τP :  ww, PersistentP (τi ww)} Δ Γ :
Dan Frumin's avatar
Dan Frumin committed
74
    inv stackN (sinv τi st st' l) -
75
    {,;τi::Δ;Γ}  (FG_pop $/ LitV (Loc st)) #() log (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
76
  Proof.
77
Transparent CG_locked_pop FG_pop CG_pop.
Dan Frumin's avatar
Dan Frumin committed
78
    iIntros "#Hinv".
79
    iLöb as "IH".
80
    rewrite {2}/FG_pop. unlock.  simpl_subst/=.
81 82 83 84 85 86 87 88 89 90 91 92

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.
Dan Frumin's avatar
Dan Frumin committed
93 94 95 96 97 98
    rel_load_l_atomic.
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
    iExists _. iFrame.
    iModIntro. iNext. iIntros "Hst /=".
    rel_rec_l.
    rel_unfold_l.
99 100 101
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
Dan Frumin's avatar
Dan Frumin committed
102 103 104
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
105
      rel_apply_r (CG_pop_fail_r with "Hst' Hl").
106
      { solve_ndisj. }
107
      iIntros "Hst' Hl".
Dan Frumin's avatar
Dan Frumin committed
108 109 110 111 112 113 114
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'".
      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").
115
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
116
      rel_case_l.
117
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
118 119 120 121

      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
      rel_vals.
      { iModIntro. iLeft. iExists (_,_). eauto. }
122 123
    - (* The stack has a value *)
      iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
124 125 126 127 128 129 130
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h.
      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.
      iModIntro. iNext. iIntros "Histk_i /=".
      iSpecialize ("Hoe" with "Histk_i").
131
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
132
      rel_case_l.
133
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150
      do 2 (rel_proj_l; rel_rec_l).
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]". clear h istk v.
      rel_cas_l_atomic.
      iInv stackN as (istk v h) "[Hoe [Hst' [Hst [HLK2 Hl]]]]" "Hclose".
      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/=.
151
        rel_apply_r (CG_pop_suc_r with "Hst' Hl").
152
        { solve_ndisj. }
153
        iIntros "Hst' Hl".
154 155 156 157
        iMod ("Hclose" with "[-]").
        { iNext. rewrite /sinv.
          rewrite (StackLink_unfold _ (ym2, z2)).
          iDestruct "HLK_tail" as (yn2loc ?) "[% _]"; simplify_eq /=.
Dan Frumin's avatar
Dan Frumin committed
158 159 160 161 162 163 164 165
          iExists _,_,_. by iFrame. }
        rel_vals.
        { iModIntro. iRight.
          iExists (_,_). eauto. }
      + (* CAS fails *)
        iSplitL; last by (iIntros (?); congruence).
        iIntros (?). iNext. iIntros "Hst".
        rel_if_l.
166
        close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
167 168
        rel_rec_l.
        iApply "IH".
169
  Qed.
170

171 172
  Lemma FG_CG_pop_refinement st st' (τi : D) l {τP :  ww, PersistentP (τi ww)} Δ Γ :
    inv stackN (sinv τi st st' l) -
173
    {,;τi::Δ;Γ}  FG_pop $/ LitV (Loc st) log CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)).
174 175 176 177 178 179 180 181 182 183 184
  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/=.
    by iApply FG_CG_pop_refinement'.
  Qed.

Dan Frumin's avatar
Dan Frumin committed
185 186
  Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP :  ww, PersistentP (τi ww)} {SH : stackG Σ} Γ:
    inv stackN (sinv τi st st' l) -
Robbert Krebbers's avatar
Robbert Krebbers committed
187
    {,;τi::Δ;Γ}  FG_read_iter $/ LitV (Loc st) log CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit.
188
  Proof.
Dan Frumin's avatar
Dan Frumin committed
189 190 191 192
    iIntros "#Hinv".
    Transparent FG_read_iter CG_snap_iter.
    unfold FG_read_iter, CG_snap_iter. unlock.
    simpl_subst/=.
193 194
    iApply bin_log_related_arrow_val; eauto.
    iAlways. iIntros (f1 f2) "#Hff /=".
Dan Frumin's avatar
Dan Frumin committed
195 196 197 198 199 200 201 202 203 204 205
    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.
206
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
207 208 209 210 211 212 213 214 215 216 217 218 219 220
    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.
221 222

    iLöb as "IH" forall (istk v) "HLK".
Dan Frumin's avatar
Dan Frumin committed
223 224 225 226 227 228 229 230 231 232 233 234
    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.
235

Dan Frumin's avatar
Dan Frumin committed
236 237 238 239 240 241 242 243
      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.
244

Dan Frumin's avatar
Dan Frumin committed
245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
      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.
266
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".      
267
      simpl.
268
      iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
Dan Frumin's avatar
Dan Frumin committed
269
      + iApply bin_log_related_arrow; eauto.
270
        iAlways. iIntros (? ?) "?"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
271 272 273 274 275 276 277 278 279 280
        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.
281 282 283 284
        iClear "IH Histk HLK_tail HLK HLK'".
        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
        iApply (related_ret with "[Hff]"). 
        done.
285
  Qed.
286

Dan Frumin's avatar
Dan Frumin committed
287 288 289 290 291 292 293 294 295 296 297 298 299 300
End Stack_refinement.

Section Full_refinement.
  Local Ltac replace_l c :=
    lazymatch goal with
    | [|- _  bin_log_related _ _ _ _ ?e _ _ ] =>
      replace e with c; last first
    end.
  Local Ltac replace_r c :=
    lazymatch goal with
    | [|- _  bin_log_related _ _ _ _ _ ?e' _ ] =>
      replace e' with c; last first
    end.

301
  (*  α. (α  Unit) * (Unit  Unit + α) * ((α  Unit)  Unit) *)
302
  Lemma FG_CG_stack_refinement `{stackPreG Σ, logrelG Σ} Δ Γ :
Dan Frumin's avatar
Dan Frumin committed
303
     {,;Δ;Γ}  FG_stack log CG_stack : TForall (TProd (TProd
304 305 306
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit)).
307
  Proof.
Dan Frumin's avatar
Dan Frumin committed
308
    unfold FG_stack. unfold CG_stack.
309
    assert (Closed (dom _ Γ) ((λ: "st", FG_stack_body "st") (ref Fold (ref InjL #())))%E).
Dan Frumin's avatar
Dan Frumin committed
310
    { apply Closed_mono with ; last done. solve_closed. }
311
    assert (Closed (dom _ Γ) ((λ: "l", (λ: "st", (CG_stack_body "st") "l") (ref Fold (InjL #()))) (ref #false))%E).
Dan Frumin's avatar
Dan Frumin committed
312 313 314 315 316 317 318 319 320
    { apply Closed_mono with ; last done. solve_closed. }

    iApply bin_log_related_tlam; auto.
    iIntros (τi) "% !#".
    rel_alloc_r as l "Hl".
    rel_rec_r.
    rel_alloc_r as st' "Hst'".
    unlock CG_stack_body.
    repeat rel_rec_r.
321 322
    (* TODO: i have to do a bind before allocation, otherwise it doesn't pick the correct reduct. *)
    rel_bind_l (ref (InjL #()))%E.
Dan Frumin's avatar
Dan Frumin committed
323 324 325 326 327
    rel_alloc_l as istk "Histk".
    simpl.
    rel_alloc_l as st "Hst".
    simpl.
    rel_rec_l.
328

Dan Frumin's avatar
Dan Frumin committed
329
    iApply fupd_logrel.
330
    iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
331 332
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
333
    change (@stack_pre_inG _ H) with (@stack_inG _ istkG).
Robbert Krebbers's avatar
Robbert Krebbers committed
334
    clearbody istkG. clear γ H1.
335
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
Dan Frumin's avatar
Dan Frumin committed
336
    { rewrite /stack_owns big_sepM_empty fmap_empty.
Dan Frumin's avatar
Dan Frumin committed
337 338 339
      iFrame "Hemp". }
    iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
    iAssert (StackLink τi (#istk, FoldV (InjLV (LitV Unit)))) with "[Histk]" as "#HLK".
340 341
    { rewrite StackLink_unfold.
      iExists _, _. iSplitR; simpl; trivial.
Dan Frumin's avatar
Dan Frumin committed
342 343 344 345 346 347 348 349 350 351 352 353 354
      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". }
    iModIntro.
    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.
355

Dan Frumin's avatar
Dan Frumin committed
356 357 358 359 360 361 362 363
    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.
364 365
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "#Hτ /=".
366
      replace_l ((FG_push $/ LitV (Loc st)) v1)%E.
Dan Frumin's avatar
Dan Frumin committed
367
      { unlock FG_push. simpl_subst/=. reflexivity. }
368
      replace_r ((CG_locked_push $/ LitV (Loc st') $/ LitV (Loc l)) v2)%E.
Dan Frumin's avatar
Dan Frumin committed
369 370
      { unlock CG_locked_push. simpl_subst/=. reflexivity. }
      iApply (FG_CG_push_refinement with "Hinv Hτ").
371
    - replace_l (FG_pop $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
372
      { unlock FG_pop. by simpl_subst/=. }
373
      replace_r (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
374 375
      { unlock CG_locked_pop. by simpl_subst/=. }
      iApply (FG_CG_pop_refinement with "Hinv").
376
    - replace_l (FG_read_iter $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
377
      { unlock FG_read_iter. by simpl_subst/=. }
378
      replace_r (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
379 380
      { unlock CG_snap_iter. by simpl_subst/=. }
      iApply (FG_CG_iter_refinement with "Hinv").
381
  Qed.
382

Dan Frumin's avatar
Dan Frumin committed
383 384 385 386 387 388 389 390 391 392 393
  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.