refinement.v 14.5 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14 15 16 17 18 19 20 21
  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 Σ}.
Dan Frumin's avatar
Dan Frumin committed
22
  Definition sinv τi stk stk' l : iProp Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
23
    ( (istk : loc) v h, (stack_owns h)
24
         stk' ↦ₛ v
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Dan Frumin's avatar
Dan Frumin committed
46
    rel_load_l_atomic.
47
    iInv N as (istk w h) "[Hoe [>Hst' [Hst [HLK >Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
55 56
    iExists (FoldV #istk'). iFrame.
    iModIntro.
57
    destruct (decide (istk' = istk)) as [e | nestk]; subst.
Dan Frumin's avatar
Dan Frumin committed
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, _)).
Dan Frumin's avatar
Dan Frumin committed
71
        iExists _, _. iSplitR; auto.
72 73
        iFrame "Hnstk".
        iRight. iExists _, _, _, _. auto. }
Dan Frumin's avatar
Dan Frumin committed
74
      rel_if_true_l.
75
      by rel_vals.
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
106
    rel_load_l_atomic.
107
    iInv N as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
129
      rel_case_l.
130
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
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/=.
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
145
      rel_case_l.
146
      rel_rec_l.
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
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 /=.
Dan Frumin's avatar
Dan Frumin committed
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)} Γ:
Dan Frumin's avatar
Dan Frumin committed
200
    inv stackN (sinv τi st st' l) -
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
Dan Frumin's avatar
Dan Frumin committed
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 /=".
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
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".
Dan Frumin's avatar
Dan Frumin committed
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

Dan Frumin's avatar
Dan Frumin committed
250
      rel_load_l_atomic.
Dan Frumin's avatar
Dan Frumin committed
251
      iInv stackN as (istk v h) "[Hoe [Hst' [Hst [#HLK Hl]]]]" "Hclose".
Dan Frumin's avatar
Dan Frumin committed
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

Dan Frumin's avatar
Dan Frumin committed
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.
Dan Frumin's avatar
Dan Frumin committed
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 *)
Dan Frumin's avatar
Dan Frumin committed
283
      + iApply bin_log_related_arrow; eauto.
284
        iAlways. iIntros (? ?) "?"; simplify_eq/=.
Dan Frumin's avatar
Dan Frumin committed
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
        iClear "IH Histk HLK_tail HLK HLK'".
        iSpecialize ("Hff" $! (y1,y2) with "Hτ").
Dan Frumin's avatar
Dan Frumin committed
297
        iApply (related_ret with "[Hff]").
298
        done.
299
  Qed.
300

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 `{SPG: 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 323 324 325 326 327 328 329
    unfold FG_stack. unfold CG_stack.
    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.
330 331
    (* 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
332 333 334 335 336
    rel_alloc_l as istk "Histk".
    simpl.
    rel_alloc_l as st "Hst".
    simpl.
    rel_rec_l.
337

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

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

Dan Frumin's avatar
Dan Frumin committed
393 394 395 396 397 398 399 400 401 402 403
  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.