refinement.v 18.5 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5
From iris.program_logic Require Import auth.
From iris_logrel.F_mu_ref_par Require Import soundness_binary.
From iris_logrel.F_mu_ref_par.examples Require Import lock.
From iris_logrel.F_mu_ref_par.examples.stack Require Import
  CG_stack FG_stack stack_rules.
6 7
From iris.proofmode Require Import invariants ghost_ownership tactics.

8 9
Definition stackN : namespace := nroot .@ "stack".

10
Section Stack_refinement.
11 12 13
  Context `{cfgSG Σ, heapIG Σ, authG lang Σ stackUR}.
  Notation D := (prodC valC valC -n> iPropG lang Σ).
  Implicit Types Δ : listC D.
14

15 16 17 18 19
  Lemma FG_CG_counter_refinement :
    []  FG_stack log CG_stack : TForall (TProd (TProd
           (TArrow (TVar 0) TUnit)
           (TArrow TUnit (TSum TUnit (TVar 0))))
           (TArrow (TArrow (TVar 0) TUnit) TUnit)).
20 21
  Proof.
    (* executing the preambles *)
22
    iIntros { Δ [|??] ρ ? } "#(Hheap & Hspec & HΓ)"; iIntros {j K} "Hj"; last first.
23 24
    { iDestruct (interp_env_length with "HΓ") as %[=]. } 
    iClear "HΓ". cbn -[FG_stack CG_stack].
Robbert Krebbers's avatar
Robbert Krebbers committed
25
    rewrite ?empty_env_subst /CG_stack /FG_stack.
26 27
    iApply wp_value; eauto.
    iExists (TLamV _); iFrame "Hj".
28
    clear j K. iAlways. iIntros {τi} "%". iIntros {j K} "Hj /=".
29 30 31
    iPvs (step_tlam _ _ j K with "[Hj]") as "Hj"; eauto.
    iApply wp_tlam; iNext.
    iPvs (steps_newlock _ _ j (K ++ [AppRCtx (RecV _)]) _ with "[Hj]")
32
      as {l} "[Hj Hl]"; eauto.
33
    { rewrite fill_app; simpl. iFrame "Hspec Hj"; trivial. }
34
    rewrite fill_app; simpl.
35
    iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
36
    simpl.
37 38
    rewrite CG_locked_push_subst CG_locked_pop_subst
            CG_iter_subst CG_snap_subst. simpl. asimpl.
39
    iPvs (step_alloc  _ _ j (K ++ [AppRCtx (RecV _)]) _ _ _ _ with "[Hj]")
40 41 42 43
      as {stk'} "[Hj Hstk']"; eauto.
    rewrite fill_app; simpl.
    iFrame "Hspec Hj"; trivial.
    rewrite fill_app; simpl.
44
    iPvs (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
45
    simpl.
46 47 48 49 50
    rewrite CG_locked_push_subst CG_locked_pop_subst
            CG_iter_subst CG_snap_subst. simpl. asimpl.
    Unshelve.
    all: try match goal with |- to_val _ = _ => auto using to_of_val end.
    all: trivial.
51
    iApply (@wp_bind _ _ _ [AppRCtx (RecV _); AllocCtx; FoldCtx]);
52 53
      iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
    iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {istk} "Histk".
54
    iPvsIntro. iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
55 56
      iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
    iApply wp_alloc; trivial; iFrame "Hheap"; iNext; iIntros {stk} "Hstk".
57
    simpl. iApply wp_rec; trivial. iPvsIntro. iNext. simpl.
58 59
    rewrite FG_push_subst FG_pop_subst FG_iter_subst. simpl. asimpl.
    (* establishing the invariant *)
Robbert Krebbers's avatar
Robbert Krebbers committed
60
    iPvs (own_alloc ( ( : stackUR))) as {γ} "Hemp".
61
    { constructor; eauto. eapply ucmra_unit_valid. }
62 63
    set (istkG := StackG _ _ γ).
    change γ with (@stack_name _ istkG).
64
    change H1 with (@stack_inG _ istkG).
65
    clearbody istkG. clear γ.
66
    iAssert (@stack_owns _ istkG _ ) with "[Hemp]" as "Hoe".
67 68 69
    { unfold stack_owns; rewrite big_sepM_empty; iFrame "Hemp"; trivial. }
    iPvs (stack_owns_alloc  _ _ _ with "[Hoe Histk]") as "[Hoe Hls]".
    { by iFrame "Hoe Histk". }
Robbert Krebbers's avatar
Robbert Krebbers committed
70
    iAssert (StackLink τi (LocV istk, FoldV (InjLV UnitV))) with "[Hls]" as "HLK".
71 72 73 74 75 76 77 78 79
    { rewrite StackLink_unfold.
      iExists _, _. iSplitR; simpl; trivial.
      iFrame "Hls". iLeft. iSplit; trivial.
    }
    iAssert (( istk v h, (stack_owns h)
                          stk' ↦ₛ v
                          stk ↦ᵢ (FoldV (LocV istk))
                          StackLink τi (LocV istk, v)
                          l ↦ₛ (v false)
80
             )%I) with "[Hoe Hstk Hstk' HLK Hl]" as "Hinv".
81
    { iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl HLK". }
82
    iPvs (inv_alloc stackN with "[Hinv]") as "#Hinv"; trivial.
83 84 85 86 87
    { iNext; iExact "Hinv". }
    clear istk.
    Opaque stack_owns.
    (* splitting *)
    iApply wp_value; simpl; trivial.
88
    iExists (PairV (PairV (CG_locked_pushV _ _) (CG_locked_popV _ _)) (RecV _)).
89 90 91 92 93 94
    simpl. rewrite CG_locked_push_of_val CG_locked_pop_of_val. iFrame "Hj".
    iExists (_, _), (_, _); iSplit; eauto.
    iSplit.
    (* refinement of push and pop *)
    - iExists (_, _), (_, _); iSplit; eauto. iSplit.
      + (* refinement of push *)
95
        iAlways. clear j K. iIntros { [v1 v2] } "#Hrel". iIntros {j K} "Hj /=".
96 97
        rewrite -(FG_push_folding (Loc stk)).
        iLöb as "Hlat".
Robbert Krebbers's avatar
Robbert Krebbers committed
98
        rewrite {2}(FG_push_folding (Loc stk)).
99
        iApply wp_rec; auto using to_of_val.
100 101 102
        iNext.
        rewrite -(FG_push_folding (Loc stk)).
        asimpl.
103
        iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
104
          iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
105 106
        iInv stackN as {istk v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
        iApply (wp_load _ _ _ _ _ _).
Robbert Krebbers's avatar
Robbert Krebbers committed
107
        iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro.
108 109 110
        iSplitL "Hoe Hstk' HLK Hl Hstk".
        iNext. iExists _, _, _; by iFrame "Hoe Hstk' HLK Hl Hstk".
        clear v h.
111
        iApply wp_rec; auto using to_of_val.
112 113 114 115 116
        iNext. asimpl.
        iApply (@wp_bind _ _ _ [IfCtx _ _; CasRCtx (LocV _) (FoldV (LocV _));
                                FoldCtx]);
          iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
        iApply wp_alloc; simpl; trivial; [by rewrite to_of_val|].
117
        iFrame "Hheap". iNext. iIntros {ltmp} "Hltmp". iPvsIntro.
118
        iApply (@wp_bind _ _ _ [IfCtx _ _]);
Robbert Krebbers's avatar
Robbert Krebbers committed
119
          iApply wp_wand_l; iSplitR; [by iIntros {w} "$"|].
120
        iInv stackN as {istk2 v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
121 122 123 124 125
        (* deciding whether CAS will succeed or fail *)
        destruct (decide (istk = istk2)) as [|Hneq]; subst.
        * (* CAS succeeds *)
          (* In this case, the specification pushes *)
          iTimeless "Hstk'". iTimeless "Hl".
126
          iPvs (steps_CG_locked_push _ _ j K _ _ _ _ _ with "[Hj Hl Hstk']")
127 128
            as "[Hj [Hstk' Hl]]".
          { rewrite CG_locked_push_of_val. by iFrame "Hspec Hstk' Hj". }
129 130
          iApply (wp_cas_suc _ _ _ _ _ _ _ _ _ _); simpl; trivial.
          iIntros "{$Hheap $Hstk} > Hstk". iSplitR "Hj".
131 132 133 134 135 136 137
          { iPvs (stack_owns_alloc with "[Hoe Hltmp]") as "[Hoe Hpt]".
            { by iFrame "Hoe". }
            iPvsIntro. iNext. iExists ltmp, _, _.
            iFrame "Hoe Hstk' Hstk Hl".
            do 2 rewrite StackLink_unfold.
            rewrite -StackLink_unfold.
            iExists _, _. iSplit; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
            iFrame "Hpt". eauto 10. }
139 140
          iPvsIntro.
          iApply wp_if_true. iNext; iApply wp_value; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
          iExists UnitV; eauto.
142
        * iApply (wp_cas_fail _ _ _ _ _ _ _ _ _ _ _ _ _); simpl; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
          iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro.
144 145
          iSplitR "Hj".
          { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
146
          iApply wp_if_false. iNext. by iApply "Hlat".
147
      + (* refinement of pop *)
148 149
        iAlways. clear j K. iIntros { [v1 v2] } "[% %]".
        iIntros {j K} "Hj /="; simplify_eq/=.
150 151
        rewrite -(FG_pop_folding (Loc stk)).
        iLöb as "Hlat".
Robbert Krebbers's avatar
Robbert Krebbers committed
152
        rewrite {2}(FG_pop_folding (Loc stk)).
153
        iApply wp_rec; auto using to_of_val.
154 155 156
        iNext.
        rewrite -(FG_pop_folding (Loc stk)).
        asimpl.
157
        iApply (@wp_bind _ _ _ [AppRCtx (RecV _); UnfoldCtx]);
158
          iApply wp_wand_l; iSplitR; [iIntros {v} "Hv"; iExact "Hv"|].
159 160
        iInv stackN as {istk v h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
        iApply (wp_load _ _ _ _ _ _). iIntros "{$Hheap $Hstk} > Hstk".
161 162
        (* Checking whether the stack is empty *)
        iDestruct (StackLink_dup with "[HLK]") as "[HLK HLK']"; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164
        rewrite {2}StackLink_unfold.
        iDestruct "HLK'" as {istk2 w} "[% [Hmpt [[% %]|HLK']]]"; simplify_eq/=.
165
        * (* The stack is empty *)
166
          iPvs (steps_CG_locked_pop_fail _ _ _ _ _ _ _ with "[Hj Hstk' Hl]")
167 168 169 170 171
            as "[Hj [Hstk' Hl]]".
          { by iFrame "Hspec Hstk' Hl Hj". }
          iPvsIntro.
          iSplitR "Hj Hmpt".
          { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk Hl". }
172
          iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
173
          iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
174 175
          iApply wp_fold; simpl; auto using to_of_val.
          iNext. iPvsIntro. iApply wp_rec; auto using to_of_val. iNext. asimpl.
176
          clear h.
177
          iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
178
          iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
179
          iInv stackN as {istk3 w h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
180 181 182
          iDestruct (stack_owns_later_open_close with "[Hmpt Hoe]")
            as "[Histk HLoe]".
          { by iFrame "Hmpt". }
183
          iApply (wp_load _ _ _ _ _ _). iFrame "Hheap Histk".
184
          iIntros "> Histk". iPvsIntro. iSplitR "Hj".
185 186 187
          { iNext. iExists _, _, _. iFrame "Hstk' Hstk HLK Hl".
            iDestruct ("HLoe" with "[Histk]") as "[Hh _]"; trivial.
          }
188
          iApply wp_rec; simpl; trivial.
189 190 191 192 193 194 195
          iNext. asimpl.
          iApply wp_case_inl; trivial.
          iNext. iApply wp_value; simpl; trivial. iExists (InjLV UnitV).
          iSplit; trivial. iLeft. iExists (_, _); repeat iSplit; simpl; trivial.
        * (* The stack is not empty *)
          iPvsIntro. iSplitR "Hj Hmpt HLK'".
          { iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
196
          iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
197
          iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
198 199
          iApply wp_fold; simpl; auto using to_of_val.
          iNext. iApply wp_rec; auto using to_of_val. iPvsIntro. iNext. asimpl.
200
          clear h.
201
          iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
202
          iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
203
          iInv stackN as {istk3 w' h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
204 205 206
          iDestruct (stack_owns_later_open_close with "[Hmpt Hoe]")
            as "[Histk HLoe]".
          { by iFrame "Hmpt". }
207
          iApply (wp_load _ _ _ _ _ _). iFrame "Hheap Histk".
208
          iIntros "> Histk". iPvsIntro.
209 210 211
          iDestruct ("HLoe" with "[Histk]") as "[Hh Hmpt]"; trivial.
          iSplitR "Hj Hmpt HLK'".
          { iNext. iExists _, _, _. by iFrame "Hstk' Hstk HLK Hl". }
212
          iApply wp_rec; auto using to_of_val.
213 214 215 216 217 218 219 220
          iNext. asimpl.
          iDestruct "HLK'" as {y1 z1 y2 z2} "[% HLK']". subst. simpl.
          iApply wp_case_inr; [simpl; by rewrite ?to_of_val |].
          iNext.
          iApply (@wp_bind _ _ _ [IfCtx _ _; CasRCtx (LocV _) (FoldV (LocV _))]);
            iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
          asimpl. iApply wp_snd; [simpl; by rewrite ?to_of_val |
                                  simpl; by rewrite ?to_of_val |].
221
          simpl. iNext. iPvsIntro.
222 223 224
          iApply (@wp_bind _ _ _ [IfCtx _ _]);
            iApply wp_wand_l; iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
          clear istk3 h. asimpl.
225
          iInv stackN as {istk3 w h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
226 227 228 229 230
          { by simpl; rewrite ?to_of_val; simpl. }
          (* deciding whether CAS will succeed or fail *)
          destruct (decide (istk2 = istk3)) as [|Hneq]; subst.
          -- (* CAS succeeds *)
            (* In this case, the specification pushes *)
231
            iApply (wp_cas_suc _ _ _ _ _ _ _ _ _ _).
232
            iIntros "{$Hheap $Hstk} > Hstk {HLK'}".
233
            iDestruct (StackLink_dup with "[HLK]") as "[HLK HLK']"; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
234 235
            rewrite {2}StackLink_unfold.
            iDestruct "HLK'" as {istk4 w2} "[% [Hmpt' HLK']]"; simplify_eq/=.
236 237 238
            iDestruct (stack_mapstos_agree with "[Hmpt Hmpt']")
              as "[Hmpt [Hmpt' %]]".
            { by iFrame "Hmpt Hmpt'". }
Robbert Krebbers's avatar
Robbert Krebbers committed
239 240 241 242 243
            iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
            iDestruct "HLK'" as {yn1 yn2 zn1 zn2}
                                   "[% [% [#Hrel HLK'']]]"; simplify_eq/=.
             (* Now we have proven that specification can also pop. *)
             rewrite CG_locked_pop_of_val.
244
             iPvs (steps_CG_locked_pop_suc _ _ _ _ _ _ _ _ _
Robbert Krebbers's avatar
Robbert Krebbers committed
245 246 247
                   with "[Hj Hstk' Hl]") as "[Hj [Hstk' Hl]]".
             { by iFrame "Hspec Hstk' Hl Hj". }
             iPvsIntro. iSplitR "Hj".
248
             { iIntros "{Hmpt Hmpt' HLK} >". rewrite StackLink_unfold.
Robbert Krebbers's avatar
Robbert Krebbers committed
249 250 251 252 253 254 255 256 257 258 259
               iDestruct "HLK''" as {istk5 w2} "[% [Hmpt HLK]]"; simplify_eq/=.
               iExists istk5, _, _. iFrame "Hoe Hstk' Hstk Hl".
               rewrite StackLink_unfold.
               iExists _, _; iSplitR; trivial.
               by iFrame "HLK".
             }
             iApply wp_if_true. iNext.
             iApply (@wp_bind _ _ _ [InjRCtx]); iApply wp_wand_l;
               iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
             iApply wp_fst; [simpl; by rewrite ?to_of_val |
                             simpl; by rewrite ?to_of_val |].
260
             iNext. iPvsIntro. iApply wp_value; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
261 262 263
             { by rewrite to_of_val. }
             iExists (InjRV _); iFrame "Hj".
             iRight. iExists (_, _). iSplit; trivial.
264
          -- (* CAS will fail *)
265
            iApply (wp_cas_fail  _ _ _ _ _ _ _ _ _ _ _ _ _).
266
            iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro. iSplitR "Hj".
267
            { iNext. iExists _, _, _. by iFrame "Hoe Hstk' Hstk HLK Hl". }
268
            iApply wp_if_false. iNext. by iApply "Hlat".
269
    - (* refinement of iter *)
270
      iAlways. clear j K. iIntros { [f1 f2] } "/= #Hfs". iIntros {j K} "Hj".
271 272
      iApply wp_rec; auto using to_of_val. iNext.
      iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
273 274 275 276 277 278 279 280
      { by iFrame "Hspec Hj". }
      asimpl. rewrite FG_iter_subst CG_snap_subst CG_iter_subst. asimpl.
      replace (FG_iter (# f1)) with (# (FG_iterV (# f1)))
        by (by rewrite FG_iter_of_val).
      replace (CG_iter (# f2)) with (# (CG_iterV (# f2)))
        by (by rewrite CG_iter_of_val).
      iApply (@wp_bind _ _ _ [AppRCtx _]); iApply wp_wand_l;
        iSplitR; [iIntros {w} "Hw"; iExact "Hw"|].
281
      iInv stackN as {istk3 w h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
282 283
      (* coarse-grained stack takes a snapshot *)
      iTimeless "Hstk'"; iTimeless "Hl".
284
      iPvs (steps_CG_snap _ _ _ (K ++ [AppRCtx _]) _ _ _ _
285 286
            with "[Hstk' Hj Hl]") as "[Hj [Hstk' Hl]]".
      { rewrite ?fill_app. simpl. by iFrame "Hspec Hstk' Hl Hj". }
287
      iApply (wp_load _ _ _ _ _ _).
288
      iIntros "{$Hheap $Hstk} > Hstk". iPvsIntro.
289 290 291 292
      iDestruct (StackLink_dup with "HLK") as "[HLK HLK']".
      iSplitR "Hj HLK'".
      { iNext. iExists _, _, _; by iFrame "Hoe Hstk' Hstk HLK Hl". }
      clear h.
Robbert Krebbers's avatar
Robbert Krebbers committed
293 294 295
      rewrite ?fill_app /= -FG_iter_folding.
      iLöb {istk3 w} as "Hlat".
      rewrite {2}FG_iter_folding.
296
      iApply wp_rec; simpl; trivial.
297 298 299 300
      rewrite -FG_iter_folding. asimpl. rewrite FG_iter_subst.
      iNext.
      iApply (@wp_bind _ _ _ [CaseCtx _ _; LoadCtx]); iApply wp_wand_l;
        iSplitR; [iIntros {v} "Hw"; iExact "Hw"|].
301
      iApply wp_fold; simpl; trivial.
302
      iNext. iPvsIntro. simpl.
303 304
      iApply (@wp_bind _ _ _ [CaseCtx _ _]); iApply wp_wand_l;
        iSplitR; [iIntros {v} "Hw"; iExact "Hw"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
305 306
      rewrite StackLink_unfold.
      iDestruct "HLK'" as {istk4 v} "[% [Hmpt HLK']]"; simplify_eq/=.
307
      iInv stackN as {istk5 v' h} "[Hoe [Hstk' [Hstk [HLK Hl]]]]".
308 309 310
      iDestruct (stack_owns_later_open_close with "[Hmpt Hoe]")
            as "[Histk HLoe]".
      { by iFrame "Hmpt". }
311
      iApply (wp_load _ _ _ _ _ _). iIntros "{$Hheap $Histk} > Histk".
312
      iDestruct ("HLoe" with "[Histk]") as "[Hh Hmpt]"; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
313 314
      iDestruct "HLK'" as "[[% %]|HLK']"; simplify_eq/=.
      * rewrite CG_iter_of_val.
315
        iPvs (steps_CG_iter_end _ _ _ _ _ _ with "[Hj]") as "Hj".
316 317 318 319
        { by iFrame "Hspec Hj". }
        iPvsIntro. iSplitR "Hj".
        { iNext. iExists _, _, _. by iFrame "Hh Hstk' Hstk HLK". }
        iApply wp_case_inl; trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
320
        iNext. iApply wp_value; trivial. iExists UnitV; eauto.
321
      * iDestruct "HLK'" as {yn1 yn2 zn1 zn2}
Robbert Krebbers's avatar
Robbert Krebbers committed
322
                              "[% [% [#Hrel HLK'']]]"; simplify_eq/=.
323
        rewrite CG_iter_of_val.
324
        iPvs (steps_CG_iter _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
325 326 327 328 329 330 331
        { by iFrame "Hspec Hj". }
        iPvsIntro. iSplitR "Hj HLK''".
        { iNext. iExists _, _, _. by iFrame "Hh Hstk' Hstk HLK". }
        simpl.
        iApply wp_case_inr; simpl; rewrite ?to_of_val; trivial.
        rewrite FG_iter_subst CG_iter_subst. asimpl.
        iNext.
332
        iApply (@wp_bind _ _ _ [AppRCtx (RecV _); AppRCtx _]);
333
          iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
334
        iApply wp_fst; simpl; rewrite ?to_of_val; trivial. iNext. iPvsIntro.
335
        iApply (@wp_bind _ _ _ [AppRCtx (RecV _)]);
336
          iApply wp_wand_l; iSplitR; [iIntros {w'} "Hw"; iExact "Hw"|].
Robbert Krebbers's avatar
Robbert Krebbers committed
337 338
        rewrite StackLink_unfold.
        iDestruct "HLK''" as {istk6 w'} "[% HLK]"; simplify_eq/=.
339 340
        iSpecialize ("Hfs" $! (yn1, zn1) with "Hrel").
        iSpecialize ("Hfs" $! _ (K ++ [AppRCtx (RecV _)])).
341
        rewrite fill_app; simpl.
342
        iApply wp_wand_l; iSplitR "Hj"; [|iApply "Hfs"; by iFrame "Hj"].
Robbert Krebbers's avatar
Robbert Krebbers committed
343
        iIntros {u} "/="; iDestruct 1 as {z} "[Hj [% %]]".
344
        rewrite fill_app; simpl. subst. asimpl.
345
        iPvs (step_rec _ _ _ _ _ _ _ _ _ with "[Hj]") as "Hj".
346 347 348
        { by iFrame "Hspec Hj". } asimpl. rewrite CG_iter_subst. asimpl.
        replace (CG_iter (# f2)) with (# (CG_iterV (# f2)))
          by (by rewrite CG_iter_of_val).
349
        iPvs (step_snd _ _ _ (K ++ [AppRCtx _]) _ _ _ _ _ _ _ with "[Hj]")
350 351 352
          as "Hj".
        { rewrite fill_app; simpl. by iFrame "Hspec Hj". }
        rewrite fill_app; simpl.
353
        iApply wp_rec; simpl; trivial.
354 355 356 357 358
        iNext. rewrite FG_iter_subst. asimpl.
        replace (FG_iter (# f1)) with (# (FG_iterV (# f1)))
          by (by rewrite FG_iter_of_val).
        iApply (@wp_bind _ _ _ [AppRCtx _]);
          iApply wp_wand_l; iSplitR; [iIntros {w''} "Hw"; iExact "Hw"|].
359
        iApply (wp_snd _ _ _ _ _); auto using to_of_val.
360
        simpl. iNext. rewrite -FG_iter_folding.
Robbert Krebbers's avatar
Robbert Krebbers committed
361 362
        iApply ("Hlat" $! istk6 zn2 with "[Hj] [HLK]"); trivial.
        rewrite StackLink_unfold; eauto.
363 364 365 366 367
        Unshelve.
        all: try match goal with
                   |- to_val _ = _ => simpl; by rewrite ?to_of_val
                 end.
        all: trivial.
Robbert Krebbers's avatar
Robbert Krebbers committed
368
        all: try match goal with |- _  _ => congruence end.
369
        all: unfold heapN, specN, stackN, specN; solve_ndisj.
370
  Qed.
371 372
End Stack_refinement.

373
Theorem stack_ctx_refinement :
Robbert Krebbers's avatar
Robbert Krebbers committed
374
  []  FG_stack ctx CG_stack : TForall (TProd (TProd
375 376
        (TArrow (TVar 0) TUnit)
        (TArrow TUnit (TSum TUnit (TVar 0))))
Robbert Krebbers's avatar
Robbert Krebbers committed
377
        (TArrow (TArrow (TVar 0) TUnit) TUnit)).
378
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
379
  set (Σ := #[authGF heapUR; authGF cfgUR; authGF stackUR]).
380
  eapply (@binary_soundness Σ);
381 382
    eauto using FG_stack_closed, CG_stack_closed.
  all: try typeclasses eauto.
383
  intros. apply FG_CG_counter_refinement.
384
Qed.