refinement.v 15 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.

Dan Frumin's avatar
Dan Frumin committed
83
84
  Lemma FG_CG_pop_refinement st st' (τi : D) l {τP :  ww, PersistentP (τi ww)} Δ Γ :
    inv stackN (sinv τi st st' l) -
Robbert Krebbers's avatar
Robbert Krebbers committed
85
    {,;τi::Δ;Γ}  FG_pop $/ LitV (Loc st) log CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l) : TArrow TUnit (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
90
91
92
93
94
95
    iApply bin_log_related_arrow_val; eauto.
    { rewrite /FG_pop. unlock. eauto. }
    { rewrite /CG_locked_pop. unlock. eauto. }
    { rewrite /FG_pop. unlock. simpl_subst/=. eauto. }
    { rewrite /CG_locked_pop. unlock. simpl_subst/=. eauto. }

    iAlways. iIntros (? ?) "[% %]". simplify_eq/=.
96
    iLöb as "IH".
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112


    rewrite {2}/FG_pop {2}/CG_locked_pop. unlock.  simpl_subst/=.


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
113
114
115
116
117
118
    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.
119
120
121
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
Dan Frumin's avatar
Dan Frumin committed
122
123
124
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
125
      rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
126
      rel_apply_r (bin_log_related_acquire_r with "Hl").
127
128
129
      { solve_ndisj. }
      iIntros "Hl /=".
      unfold CG_pop. unlock.
Dan Frumin's avatar
Dan Frumin committed
130
      repeat rel_rec_r.
131
132
      rel_load_r.
      rel_fold_r.
Dan Frumin's avatar
Dan Frumin committed
133
134
135
      rel_case_r.
      repeat rel_rec_r.
      rel_apply_r (bin_log_related_release_r with "Hl").
136
137
138
      { solve_ndisj. }
      iIntros "Hl /=".
      rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
139
140
141
142
143
144
145
146

      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").
147
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
148
      rel_case_l.
149
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
150
151
152
153

      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".
      rel_vals.
      { iModIntro. iLeft. iExists (_,_). eauto. }
154
155
    - (* The stack has a value *)
      iDestruct "HLK" as (y1 z1 y2 z2) "(% & % & Hτ & HLK_tail)"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
156
157
158
159
160
161
162
      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").
163
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
164
      rel_case_l.
165
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
      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/=.
183
184

        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
185
        rel_apply_r (bin_log_related_acquire_r with "Hl").
186
187
188
        { solve_ndisj. }
        iIntros "Hl /=".
        unfold CG_pop. unlock.
Dan Frumin's avatar
Dan Frumin committed
189
        repeat rel_rec_r.
190
        rel_load_r.
Dan Frumin's avatar
Dan Frumin committed
191
192
        rel_fold_r.
        rel_case_r.
193
        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
194
195
        rel_proj_r.
        rel_store_r.
196
        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
197
        rel_proj_r.
198
        rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
199
        rel_apply_r (bin_log_related_release_r with "Hl").
200
201
202
203
204
205
206
        { 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
207
208
209
210
211
212
213
214
          iExists _,_,_. by iFrame. }
        rel_vals.
        { iModIntro. iRight.
          iExists (_,_). eauto. }
      + (* CAS fails *)
        iSplitL; last by (iIntros (?); congruence).
        iIntros (?). iNext. iIntros "Hst".
        rel_if_l.
215
        close_sinv "Hclose" "[Hoe Hst Hst' Hl HLK2]".
216
217
218
        rewrite /FG_pop /CG_locked_pop. unlock. simpl_subst/=.
        rel_rec_l.
        iApply "IH".
219
  Qed.
220

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

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

Dan Frumin's avatar
Dan Frumin committed
272
273
274
275
276
277
278
279
      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.
280

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

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

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

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

Dan Frumin's avatar
Dan Frumin committed
418
419
420
421
422
423
424
425
426
427
428
  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.