refinement.v 14.8 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.
9
  Context `{logrelG Σ}.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  Notation D := (prodC valC valC -n> iProp Σ).
11
  Implicit Types Δ : listC D.
12
  Import lang.
13

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

  Context `{stackG Σ}.
  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 37 38
  Lemma FG_CG_push_refinement N st st' (τi : D) (v v' : val) l {τP :  ww, PersistentP (τi ww)} Γ :
    N  logrelN 
    inv N (sinv τi st st' l) - τi (v,v') -
Robbert Krebbers's avatar
Robbert Krebbers committed
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
      iApply fupd_logrel'. (* TODO iMod should pick this up on its own *)
      iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
66
      iModIntro.
67 68 69
      iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]").
      { iNext. rewrite {2}/sinv. iExists _,_,_.
        iFrame "Hoe Hst' Hst Hl".
70
        rewrite (StackLink_unfold _ (# nstk, _)).
71 72 73
        iExists _, _. iSplitR; auto. 
        iFrame "Hnstk".
        iRight. iExists _, _, _, _. auto. }
74
      rel_if_true_l.
75
      by rel_vals.
76 77 78
    - (* CAS fails *)
      iSplitL; last by (iIntros (?); congruence).
      iIntros (?); iNext; iIntros "Hst".
79 80 81 82
      close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
      rel_if_false_l. simpl.
      rel_rec_l.
      by iApply "IH".
83 84
  Qed.

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

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.
106
    rel_load_l_atomic.
107
    iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
108 109 110 111
    iExists _. iFrame.
    iModIntro. iNext. iIntros "Hst /=".
    rel_rec_l.
    rel_unfold_l.
112 113 114
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
115 116 117
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
118
      rel_apply_r (CG_pop_fail_r with "Hst' Hl").
119
      { solve_ndisj. }
120
      iIntros "Hst' Hl".
121 122
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK']". clear h. iClear "HLK'".
      rel_load_l_atomic.
123
      iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
124 125 126 127
      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").
128
      rel_rec_l.
129
      rel_case_l.
130
      rel_rec_l.
131 132 133 134

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

184 185
  Lemma FG_CG_pop_refinement st st' (τi : D) l {τP :  ww, PersistentP (τi ww)} Δ Γ :
    inv stackN (sinv τi st st' l) -
186
    {,;τi::Δ;Γ}  FG_pop $/ LitV (Loc st) log CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)).
187 188 189 190 191 192 193 194
  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/=.
195 196
    iApply (FG_CG_pop_refinement' stackN); eauto.
    { solve_ndisj. }
197 198
  Qed.

199
  Lemma FG_CG_iter_refinement st st' (τi : D) l Δ {τP :  ww, PersistentP (τi ww)} Γ:
200
    inv stackN (sinv τi st st' l) -
201
    {,;τi::Δ;Γ}  FG_read_iter $/ LitV (Loc st) log CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit.
202
  Proof.
203 204 205 206
    iIntros "#Hinv".
    Transparent FG_read_iter CG_snap_iter.
    unfold FG_read_iter, CG_snap_iter. unlock.
    simpl_subst/=.
207 208
    iApply bin_log_related_arrow_val; eauto.
    iAlways. iIntros (f1 f2) "#Hff /=".
209 210 211 212 213 214 215 216 217 218 219
    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.
220
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
221 222 223 224 225 226 227 228 229 230 231 232 233 234
    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.
235 236

    iLöb as "IH" forall (istk v) "HLK".
237 238 239 240 241 242 243 244 245 246 247 248
    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.
249

250
      rel_load_l_atomic.
251
      iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".      
252 253 254 255 256 257
      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.
258

259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279
      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.
280
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".      
281
      simpl.
282
      iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
283
      + iApply bin_log_related_arrow; eauto.
284
        iAlways. iIntros (? ?) "?"; simplify_eq/=.
285 286 287 288 289 290 291 292 293 294
        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.
295 296 297 298
        iClear "IH Histk HLK_tail HLK HLK'".
        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
        iApply (related_ret with "[Hff]"). 
        done.
299
  Qed.
300

301 302 303 304 305 306 307 308 309 310 311 312 313 314
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.

315
  (*  α. (α  Unit) * (Unit  Unit + α) * ((α  Unit)  Unit) *)
316
  Lemma FG_CG_stack_refinement `{SPG: stackPreG Σ, logrelG Σ} Δ Γ :
317
     {,;Δ;Γ}  FG_stack log CG_stack : TForall (TProd (TProd
318 319 320
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit)).
321
  Proof.
322
    unfold FG_stack. unfold CG_stack.
323
    assert (Closed (dom _ Γ) ((λ: "st", FG_stack_body "st") (ref Fold (ref InjL #())))%E).
324
    { apply Closed_mono with ; last done. solve_closed. }
325
    assert (Closed (dom _ Γ) ((λ: "l", (λ: "st", (CG_stack_body "st") "l") (ref Fold (InjL #()))) (ref #false))%E).
326 327 328 329 330 331 332 333 334
    { 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.
335 336
    (* TODO: i have to do a bind before allocation, otherwise it doesn't pick the correct reduct. *)
    rel_bind_l (ref (InjL #()))%E.
337 338 339 340 341
    rel_alloc_l as istk "Histk".
    simpl.
    rel_alloc_l as st "Hst".
    simpl.
    rel_rec_l.
342

343
    iApply fupd_logrel.
344
    iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
345 346
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
347 348
    change (@stack_pre_inG _ SPG) with (@stack_inG _ istkG).
    clearbody istkG. clear γ SPG.
349
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
350
    { rewrite /stack_owns /prestack_owns big_sepM_empty fmap_empty.
351 352 353
      iFrame "Hemp". }
    iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
    iAssert (StackLink τi (#istk, FoldV (InjLV (LitV Unit)))) with "[Histk]" as "#HLK".
354 355
    { rewrite StackLink_unfold.
      iExists _, _. iSplitR; simpl; trivial.
356 357 358 359 360 361 362 363 364 365 366 367 368
      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.
369

370 371 372 373 374 375 376 377
    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.
378 379
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "#Hτ /=".
380
      replace_l ((FG_push $/ LitV (Loc st)) v1)%E.
381
      { unlock FG_push. simpl_subst/=. reflexivity. }
382
      replace_r ((CG_locked_push $/ LitV (Loc st') $/ LitV (Loc l)) v2)%E.
383 384
      { unlock CG_locked_push. simpl_subst/=. reflexivity. }
      iApply (FG_CG_push_refinement with "Hinv Hτ").
385
      { solve_ndisj. }
386
    - replace_l (FG_pop $/ LitV (Loc st))%E.
387
      { unlock FG_pop. by simpl_subst/=. }
388
      replace_r (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E.
389 390
      { unlock CG_locked_pop. by simpl_subst/=. }
      iApply (FG_CG_pop_refinement with "Hinv").
391
    - replace_l (FG_read_iter $/ LitV (Loc st))%E.
392
      { unlock FG_read_iter. by simpl_subst/=. }
393
      replace_r (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E.
394 395
      { unlock CG_snap_iter. by simpl_subst/=. }
      iApply (FG_CG_iter_refinement with "Hinv").
396
  Qed.
397

398 399 400 401 402 403 404 405 406 407 408
  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.