refinement.v 15.4 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 34 35
    Transparent FG_push.
    unfold CG_locked_push. unlock. simpl_subst/=.
    rel_rec_r.
    unfold FG_push. unlock. simpl_subst/=.
    iLöb as "IH".
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
36 37 38 39
    rel_load_l_atomic.
    iInv stackN as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
    iExists (FoldV #istk). iFrame.
    iModIntro. iNext. iIntros "Hst".
40 41
    close_sinv "Hclose" "[Hst Hoe Hst' Hl HLK]". clear w h.
    rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
42 43 44 45 46
    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.
47
    destruct (decide (istk' = istk)) as [e | nestk]; subst.
Dan Frumin's avatar
Dan Frumin committed
48 49 50 51
    - (* CAS succeeds *)
      iSplitR; first by iIntros ([]).
      iIntros (?). iNext. iIntros "Hst".
      rel_apply_r (bin_log_related_acquire_r with "Hl").
52 53 54 55 56
      { solve_ndisj. }
      iIntros "Hl /=". 
      rel_rec_r.
      unfold CG_push. unlock. do 2 rel_rec_r.     
      rel_load_r.
Dan Frumin's avatar
Dan Frumin committed
57
      rel_store_r.
58
      rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
59
      rel_apply_r (bin_log_related_release_r with "Hl").
60 61 62 63
      { solve_ndisj. }
      iIntros "Hl /=".
      iApply fupd_logrel'. (* TODO iMod should pick this up on its own *)
      iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
64
      iModIntro.
65 66 67
      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 70 71
        iExists _, _. iSplitR; auto. 
        iFrame "Hnstk".
        iRight. iExists _, _, _, _. auto. }
Dan Frumin's avatar
Dan Frumin committed
72
      rel_if_true_l.
73
      by rel_vals.
Dan Frumin's avatar
Dan Frumin committed
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' st st' (τi : D) l {τP :  ww, PersistentP (τi ww)} Δ Γ :
Dan Frumin's avatar
Dan Frumin committed
84
    inv stackN (sinv τi st st' l) -
85
    {,;τi::Δ;Γ}  (FG_pop $/ LitV (Loc st)) #() log (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l)) #() : TSum TUnit (TVar 0).
86
  Proof.
87
Transparent CG_locked_pop FG_pop CG_pop.
Dan Frumin's avatar
Dan Frumin committed
88
    iIntros "#Hinv".
89
    iLöb as "IH".
90
    rewrite {2}/FG_pop. unlock.  simpl_subst/=.
91 92 93 94 95 96 97 98 99 100 101 102

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
103 104 105 106 107 108
    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.
109 110 111
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
Dan Frumin's avatar
Dan Frumin committed
112 113 114
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
115
      rewrite {2}/CG_locked_pop. unlock. simpl_subst/=.
116
      rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
117
      rel_apply_r (bin_log_related_acquire_r with "Hl").
118 119 120
      { solve_ndisj. }
      iIntros "Hl /=".
      unfold CG_pop. unlock.
Dan Frumin's avatar
Dan Frumin committed
121
      repeat rel_rec_r.
122 123
      rel_load_r.
      rel_fold_r.
Dan Frumin's avatar
Dan Frumin committed
124 125 126
      rel_case_r.
      repeat rel_rec_r.
      rel_apply_r (bin_log_related_release_r with "Hl").
127 128 129
      { solve_ndisj. }
      iIntros "Hl /=".
      rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
130 131 132 133 134 135 136 137

      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").
138
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
139
      rel_case_l.
140
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
141 142 143 144

      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
      rel_vals.
      { iModIntro. iLeft. iExists (_,_). eauto. }
145 146
    - (* The stack has a value *)
      iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
147 148 149 150 151 152 153
      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").
154
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
155
      rel_case_l.
156
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
      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/=.
174
        rewrite {2}/CG_locked_pop. unlock. simpl_subst/=.
175
        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
176
        rel_apply_r (bin_log_related_acquire_r with "Hl").
177 178 179
        { solve_ndisj. }
        iIntros "Hl /=".
        unfold CG_pop. unlock.
Dan Frumin's avatar
Dan Frumin committed
180
        repeat rel_rec_r.
181
        rel_load_r.
Dan Frumin's avatar
Dan Frumin committed
182 183
        rel_fold_r.
        rel_case_r.
184
        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
185 186
        rel_proj_r.
        rel_store_r.
187
        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
188
        rel_proj_r.
189
        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
190
        rel_apply_r (bin_log_related_release_r with "Hl").
191 192 193 194 195 196 197
        { solve_ndisj. }
        iIntros "Hl /=".
        rel_rec_r.
        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
198 199 200 201 202 203 204 205
          iExists _,_,_. by iFrame. }
        rel_vals.
        { iModIntro. iRight.
          iExists (_,_). eauto. }
      + (* CAS fails *)
        iSplitL; last by (iIntros (?); congruence).
        iIntros (?). iNext. iIntros "Hst".
        rel_if_l.
206
        close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
207 208
        rel_rec_l.
        iApply "IH".
209
  Qed.
210

211 212
  Lemma FG_CG_pop_refinement st st' (τi : D) l {τP :  ww, PersistentP (τi ww)} Δ Γ :
    inv stackN (sinv τi st st' l) -
213
    {,;τi::Δ;Γ}  FG_pop $/ LitV (Loc st) log CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (TSum TUnit (TVar 0)).
214 215 216 217 218 219 220 221 222 223 224
  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
225 226
  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
227
    {,;τi::Δ;Γ}  FG_read_iter $/ LitV (Loc st) log CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l) : TArrow (TArrow (TVar 0) TUnit) TUnit.
228
  Proof.
Dan Frumin's avatar
Dan Frumin committed
229 230 231 232
    iIntros "#Hinv".
    Transparent FG_read_iter CG_snap_iter.
    unfold FG_read_iter, CG_snap_iter. unlock.
    simpl_subst/=.
233 234
    iApply bin_log_related_arrow_val; eauto.
    iAlways. iIntros (f1 f2) "#Hff /=".
Dan Frumin's avatar
Dan Frumin committed
235 236 237 238 239 240 241 242 243 244 245
    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.
246
    iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
247 248 249 250 251 252 253 254 255 256 257 258 259 260
    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.
261 262

    iLöb as "IH" forall (istk v) "HLK".
Dan Frumin's avatar
Dan Frumin committed
263 264 265 266 267 268 269 270 271 272 273 274
    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.
275

Dan Frumin's avatar
Dan Frumin committed
276 277 278 279 280 281 282 283
      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.
284

Dan Frumin's avatar
Dan Frumin committed
285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305
      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.
306
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".      
307
      simpl.
308
      iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
Dan Frumin's avatar
Dan Frumin committed
309
      + iApply bin_log_related_arrow; eauto.
310
        iAlways. iIntros (? ?) "?"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
311 312 313 314 315 316 317 318 319 320
        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.
321 322 323 324
        iClear "IH Histk HLK_tail HLK HLK'".
        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
        iApply (related_ret with "[Hff]"). 
        done.
325
  Qed.
326

Dan Frumin's avatar
Dan Frumin committed
327 328 329 330 331 332 333 334 335 336 337 338 339 340
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.

341
  (*  α. (α  Unit) * (Unit  Unit + α) * ((α  Unit)  Unit) *)
342
  Lemma FG_CG_stack_refinement `{stackPreG Σ, logrelG Σ} Δ Γ :
Dan Frumin's avatar
Dan Frumin committed
343
     {,;Δ;Γ}  FG_stack log CG_stack : TForall (TProd (TProd
344 345 346
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit)).
347
  Proof.
Dan Frumin's avatar
Dan Frumin committed
348
    unfold FG_stack. unfold CG_stack.
349
    assert (Closed (dom _ Γ) ((λ: "st", FG_stack_body "st") (ref Fold (ref InjL #())))%E).
Dan Frumin's avatar
Dan Frumin committed
350
    { apply Closed_mono with ; last done. solve_closed. }
351
    assert (Closed (dom _ Γ) ((λ: "l", (λ: "st", (CG_stack_body "st") "l") (ref Fold (InjL #()))) (ref #false))%E).
Dan Frumin's avatar
Dan Frumin committed
352 353 354 355 356 357 358 359 360
    { 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.
361 362
    (* 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
363 364 365 366 367
    rel_alloc_l as istk "Histk".
    simpl.
    rel_alloc_l as st "Hst".
    simpl.
    rel_rec_l.
368

Dan Frumin's avatar
Dan Frumin committed
369
    iApply fupd_logrel.
370
    iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
371 372
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
373
    change (@stack_pre_inG _ H) with (@stack_inG _ istkG).
Robbert Krebbers's avatar
Robbert Krebbers committed
374
    clearbody istkG. clear γ H1.
375
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
Dan Frumin's avatar
Dan Frumin committed
376
    { rewrite /stack_owns big_sepM_empty fmap_empty.
Dan Frumin's avatar
Dan Frumin committed
377 378 379
      iFrame "Hemp". }
    iMod (stack_owns_alloc with "[$Hoe $Histk]") as "[Hoe #Histk]".
    iAssert (StackLink τi (#istk, FoldV (InjLV (LitV Unit)))) with "[Histk]" as "#HLK".
380 381
    { rewrite StackLink_unfold.
      iExists _, _. iSplitR; simpl; trivial.
Dan Frumin's avatar
Dan Frumin committed
382 383 384 385 386 387 388 389 390 391 392 393 394
      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.
395

Dan Frumin's avatar
Dan Frumin committed
396 397 398 399 400 401 402 403
    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.
404 405
    - iApply bin_log_related_arrow_val; eauto.
      iAlways. iIntros (v1 v2) "#Hτ /=".
406
      replace_l ((FG_push $/ LitV (Loc st)) v1)%E.
Dan Frumin's avatar
Dan Frumin committed
407
      { unlock FG_push. simpl_subst/=. reflexivity. }
408
      replace_r ((CG_locked_push $/ LitV (Loc st') $/ LitV (Loc l)) v2)%E.
Dan Frumin's avatar
Dan Frumin committed
409 410
      { unlock CG_locked_push. simpl_subst/=. reflexivity. }
      iApply (FG_CG_push_refinement with "Hinv Hτ").
411
    - replace_l (FG_pop $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
412
      { unlock FG_pop. by simpl_subst/=. }
413
      replace_r (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
414 415
      { unlock CG_locked_pop. by simpl_subst/=. }
      iApply (FG_CG_pop_refinement with "Hinv").
416
    - replace_l (FG_read_iter $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
417
      { unlock FG_read_iter. by simpl_subst/=. }
418
      replace_r (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
419 420
      { unlock CG_snap_iter. by simpl_subst/=. }
      iApply (FG_CG_iter_refinement with "Hinv").
421
  Qed.
422

Dan Frumin's avatar
Dan Frumin committed
423 424 425 426 427 428 429 430 431 432 433
  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.