refinement.v 17 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.algebra Require Import auth list.
Amin Timany's avatar
Amin Timany committed
2
From iris.program_logic Require Import adequacy ectxi_language.
Amin Timany's avatar
Amin Timany committed
3
4
5
From iris_examples.logrel.F_mu_ref_conc Require Import soundness_binary.
From iris_examples.logrel.F_mu_ref_conc.examples Require Import lock.
From iris_examples.logrel.F_mu_ref_conc.examples.stack Require Import
Amin Timany's avatar
Amin Timany committed
6
7
8
9
10
11
12
  CG_stack FG_stack stack_rules.
From iris.proofmode Require Import tactics.

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

Section Stack_refinement.
  Context `{heapIG Σ, cfgSG Σ, inG Σ (authR stackUR)}.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
  Notation D := (prodO valO valO -n> iPropO Σ).
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  Implicit Types Δ : listO D.
Amin Timany's avatar
Amin Timany committed
15
16
17
18
19
20
21
22

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

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 (Σ := #[invΣ; gen_heapΣ loc val; GFunctor (authR cfgUR); GFunctor (authR stackUR)]).
  set (HG := soundness_unary.HeapPreIG Σ _ _).
Amin Timany's avatar
Amin Timany committed
338
  eapply (binary_soundness Σ); eauto using FG_stack_type, CG_stack_type.
Amin Timany's avatar
Amin Timany committed
339
340
  intros; apply FG_CG_counter_refinement.
Qed.