refinement.v 18.6 KB
Newer Older
1 2
From iris.base_logic Require Import auth.
From iris.program_logic Require Import adequacy ectxi_language.
3 4 5
From iris_logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_logrel.F_mu_ref_conc.examples Require Import lock.
From iris_logrel.F_mu_ref_conc.examples.stack Require Import
Robbert Krebbers's avatar
Robbert Krebbers committed
6
  CG_stack FG_stack stack_rules.
7
From iris.proofmode Require Import tactics.
8

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

11
Section Stack_refinement.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
  Context `{cfgSG Σ, authG Σ stackUR}.
  Notation D := (prodC valC valC -n> iProp Σ).
14
  Implicit Types Δ : listC D.
Robbert Krebbers's avatar
Robbert Krebbers committed
15

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

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