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 13 14 15 16 17 18 19 20 21 22
  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)}.
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types Δ : listC D.

  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.