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') -
27
    Γ  ((FG_push $/ (LitV (Loc st))) v)%E log ((CG_locked_push $/ (LitV (Loc st')) $/ (LitV (Loc l))) v')%E : TUnit.
28
  Proof.
Dan Frumin's avatar
Dan Frumin committed
29
    iIntros "#Hinv #Hvv'". iIntros (Δ).
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.
Dan Frumin's avatar
Dan Frumin committed
87 88 89
    iIntros "#Hinv".
    Transparent CG_locked_pop FG_pop CG_pop.
    unfold FG_pop, CG_locked_pop. unlock.
90
    simpl_subst/=.
Dan Frumin's avatar
Dan Frumin committed
91
    iApply bin_log_related_arrow; eauto.
92
    iAlways. iIntros (? ?) "ZZ". simplify_eq/=. iClear "ZZ".
93 94
    rel_rec_r.
    rel_rec_l.
95
    iLöb as "IH".
Dan Frumin's avatar
Dan Frumin committed
96 97 98 99 100 101
    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.
102 103 104
    iPoseProof "HLK" as "HLK'".

    rewrite {1}StackLink_unfold.
Dan Frumin's avatar
Dan Frumin committed
105 106 107 108
    iDestruct "HLK" as (istk2 w) "(% & Histk & HLK)". simplify_eq/=.
    iDestruct "HLK" as "[[% %] | HLK]"; simplify_eq/=.
    - (* The stack is empty *)
      rel_apply_r (bin_log_related_acquire_r with "Hl").
109 110 111
      { solve_ndisj. }
      iIntros "Hl /=".
      unfold CG_pop. unlock.
Dan Frumin's avatar
Dan Frumin committed
112
      repeat rel_rec_r.
113 114
      rel_load_r.
      rel_fold_r.
Dan Frumin's avatar
Dan Frumin committed
115 116 117
      rel_case_r.
      repeat rel_rec_r.
      rel_apply_r (bin_log_related_release_r with "Hl").
118 119 120
      { solve_ndisj. }
      iIntros "Hl /=".
      rel_rec_r.
Dan Frumin's avatar
Dan Frumin committed
121 122 123 124 125 126 127 128

      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").
129
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
130
      rel_case_l.
131
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
132 133 134 135

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

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

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

Dan Frumin's avatar
Dan Frumin committed
251 252 253 254 255 256 257 258
      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.
259

Dan Frumin's avatar
Dan Frumin committed
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
      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.
281
      close_sinv "Hclose" "[Hoe Hst' Hst Hl HLK]".      
282
      simpl.
283
      iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit with "[] [Hτ]"). (* TODO: abbreivate this as related_let *)
Dan Frumin's avatar
Dan Frumin committed
284
      + iApply bin_log_related_arrow; eauto.
285
        iAlways. iIntros (? ?) "?"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
286 287 288 289 290 291 292 293 294 295
        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.
296 297 298 299
        iClear "IH Histk HLK_tail HLK HLK'".
        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
        iApply (related_ret with "[Hff]"). 
        done.
300
  Qed.
Dan Frumin's avatar
Dan Frumin committed
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 `{stackPreG Σ, logrelG Σ} Δ Γ :
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
322
    unfold FG_stack. unfold CG_stack.
323
    assert (Closed (dom _ Γ) ((λ: "st", FG_stack_body "st") (ref Fold (ref InjL #())))%E).
Dan Frumin's avatar
Dan Frumin committed
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).
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
337 338 339 340 341
    rel_alloc_l as istk "Histk".
    simpl.
    rel_alloc_l as st "Hst".
    simpl.
    rel_rec_l.
342

Dan Frumin's avatar
Dan Frumin committed
343
    iApply fupd_logrel.
344
    iMod (own_alloc ( ( : stackUR))) as (γ) "Hemp"; first done.
345 346
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
347
    change (@stack_pre_inG _ H) with (@stack_inG _ istkG).
Robbert Krebbers's avatar
Robbert Krebbers committed
348
    clearbody istkG. clear γ H1.
349
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
Dan Frumin's avatar
Dan Frumin committed
350
    { rewrite /stack_owns big_sepM_empty fmap_empty.
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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

Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
381
      { unlock FG_push. simpl_subst/=. reflexivity. }
382
      replace_r ((CG_locked_push $/ LitV (Loc st') $/ LitV (Loc l)) v2)%E.
Dan Frumin's avatar
Dan Frumin committed
383 384
      { unlock CG_locked_push. simpl_subst/=. reflexivity. }
      iApply (FG_CG_push_refinement with "Hinv Hτ").
385
    - replace_l (FG_pop $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
386
      { unlock FG_pop. by simpl_subst/=. }
387
      replace_r (CG_locked_pop $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
388 389
      { unlock CG_locked_pop. by simpl_subst/=. }
      iApply (FG_CG_pop_refinement with "Hinv").
390
    - replace_l (FG_read_iter $/ LitV (Loc st))%E.
Dan Frumin's avatar
Dan Frumin committed
391
      { unlock FG_read_iter. by simpl_subst/=. }
392
      replace_r (CG_snap_iter $/ LitV (Loc st') $/ LitV (Loc l))%E.
Dan Frumin's avatar
Dan Frumin committed
393 394
      { unlock CG_snap_iter. by simpl_subst/=. }
      iApply (FG_CG_iter_refinement with "Hinv").
395
  Qed.
396

Dan Frumin's avatar
Dan Frumin committed
397 398 399 400 401 402 403 404 405 406 407
  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.