CG_stack.v 18.6 KB
Newer Older
1 2
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import namespaces.
3
From iris_logrel.F_mu_ref_conc Require Import examples.lock.
4 5
Import uPred.

6 7 8 9 10
Definition CG_StackType τ :=
  TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).

(* Coarse-grained push *)
Definition CG_push (st : expr) : expr :=
11
  Rec (Store
12 13 14 15 16 17
         (st.[ren (+2)]) (Fold (InjR (Pair (Var 1) (Load st.[ren (+ 2)]))))).

Definition CG_locked_push (st l : expr) := with_lock (CG_push st) l.
Definition CG_locked_pushV (st l : expr) : val := with_lockV (CG_push st) l.

Definition CG_pop (st : expr) : expr :=
18
  Rec (Case (Unfold (Load st.[ren (+ 2)]))
19 20
            (InjL Unit)
            (
21
              App (Rec (InjR (Fst (Var 2))))
22 23 24 25 26 27 28
                  (Store st.[ren (+ 3)] (Snd (Var 0)))
            )
      ).

Definition CG_locked_pop (st l : expr) := with_lock (CG_pop st) l.
Definition CG_locked_popV (st l : expr) : val := with_lockV (CG_pop st) l.

29 30
Definition CG_snap (st l : expr) :=  with_lock (Rec (Load st.[ren (+2)])) l.
Definition CG_snapV (st l : expr) : val := with_lockV (Rec (Load st.[ren (+2)])) l.
31 32

Definition CG_iter (f : expr) : expr :=
33
  Rec (Case (Unfold (Var 1))
34 35
            Unit
            (
36
              App (Rec (App (Var 3) (Snd (Var 2))))
37 38 39 40 41
                  (App f.[ren (+3)] (Fst (Var 0)))
            )
      ).

Definition CG_iterV (f : expr) : val :=
42
  RecV (Case (Unfold (Var 1))
43 44
            Unit
            (
45
              App (Rec (App (Var 3) (Snd (Var 2))))
46 47 48 49 50
                  (App f.[ren (+3)] (Fst (Var 0)))
            )
      ).

Definition CG_snap_iter (st l : expr) : expr :=
51
  Rec (App (CG_iter (Var 1)) (App (CG_snap st.[ren (+2)] l.[ren (+2)]) Unit)).
52 53 54 55 56
Definition CG_stack_body (st l : expr) : expr :=
  Pair (Pair (CG_locked_push st l) (CG_locked_pop st l))
       (CG_snap_iter st l).

Definition CG_stack : expr :=
57
  TLam (App (Rec (App (Rec (CG_stack_body (Var 1) (Var 3)))
58 59
                (Alloc (Fold (InjL Unit))))) newlock).

60
Section CG_Stack.
61
  Context `{cfgSG Σ}.
62 63 64 65 66 67

  Lemma CG_push_type st Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ (CG_push st) (TArrow τ TUnit).
  Proof.
    intros H1. repeat econstructor.
68 69
    eapply (context_weakening [_; _]); eauto.
    repeat constructor; asimpl; trivial.
70 71 72 73 74
    eapply (context_weakening [_; _]); eauto.
  Qed.

  Lemma CG_push_closed (st : expr) :
    ( f, st.[f] = st)   f, (CG_push st).[f] = CG_push st.
75
  Proof. intros Hst f. unfold CG_push. asimpl. rewrite ?Hst; trivial. Qed.
76

Robbert Krebbers's avatar
Robbert Krebbers committed
77
  Lemma CG_push_subst (st : expr) f : (CG_push st).[f] = CG_push st.[f].
78 79
  Proof. unfold CG_push; asimpl; trivial. Qed.

80 81
  Lemma steps_CG_push E ρ j K st v w :
    nclose specN  E 
82 83
    spec_ctx ρ  st ↦ₛ v  j  fill K (App (CG_push (Loc st)) (of_val w))
     |={E}=> j  fill K Unit  st ↦ₛ FoldV (InjRV (PairV w v)).
84 85
  Proof.
    intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
86
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
87
    asimpl.
88
    iMod (step_load _ _ j (K ++ [StoreRCtx (LocV _); FoldCtx;
89
                                   InjRCtx; PairRCtx _])
90 91 92 93
                    _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. simpl.
94
    iMod (step_store _ _ j K _ _ _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
    { by iFrame. }
96
    iModIntro. by iFrame.
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
    Unshelve.
    all: try match goal with |- to_val _ = _ => auto using to_of_val end.
    simpl; by rewrite ?to_of_val.
  Qed.

  Global Opaque CG_push.

  Lemma CG_locked_push_to_val st l :
    to_val (CG_locked_push st l) = Some (CG_locked_pushV st l).
  Proof. trivial. Qed.

  Lemma CG_locked_push_of_val st l :
    of_val (CG_locked_pushV st l) = CG_locked_push st l.
  Proof. trivial. Qed.

  Global Opaque CG_locked_pushV.

  Lemma CG_locked_push_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ l LockType 
    typed Γ (CG_locked_push st l) (TArrow τ TUnit).
  Proof.
    intros H1 H2. repeat econstructor.
    eapply with_lock_type; auto using CG_push_type.
  Qed.

  Lemma CG_locked_push_closed (st l : expr) :
    ( f, st.[f] = st)  ( f, l.[f] = l) 
     f, (CG_locked_push st l).[f] = CG_locked_push st l.
  Proof.
    intros H1 H2 f. asimpl. unfold CG_locked_push.
    rewrite with_lock_closed; trivial. apply CG_push_closed; trivial.
  Qed.

  Lemma CG_locked_push_subst (st l : expr) f :
Robbert Krebbers's avatar
Robbert Krebbers committed
132
    (CG_locked_push st l).[f] = CG_locked_push st.[f] l.[f].
133 134
  Proof. by rewrite with_lock_subst CG_push_subst. Qed.

135 136
  Lemma steps_CG_locked_push E ρ j K st w v l :
    nclose specN  E 
137 138 139
    spec_ctx ρ  st ↦ₛ v  l ↦ₛ (#v false)
       j  fill K (App (CG_locked_push (Loc st) (Loc l)) (of_val w))
     |={E}=> j  fill K Unit  st ↦ₛ FoldV (InjRV (PairV w v))  l ↦ₛ (#v false).
140 141
  Proof.
    intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
142
    iMod (steps_with_lock
143
            _ _ j K _ _ _ _ UnitV _ _ _ with "[Hj Hx Hl]") as "Hj"; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
    - iIntros (K') "[#Hspec [Hx Hj]]".
145
      iApply steps_CG_push; first done. iFrame "Hspec Hj Hx"; trivial.
146 147 148 149 150 151
    - iFrame "Hspec Hj Hx"; trivial.
      Unshelve. all: trivial.
  Qed.

  Global Opaque CG_locked_push.

152
  (* Coarse-grained pop *)
153 154 155 156 157
  Lemma CG_pop_type st Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ (CG_pop st) (TArrow TUnit (TSum TUnit τ)).
  Proof.
    intros H1.
158 159 160 161 162 163 164 165 166
    econstructor.
    eapply (Case_typed _ _ _ _ TUnit);
      [| repeat constructor
       | repeat econstructor; eapply (context_weakening [_; _; _]); eauto].
    replace (TSum TUnit (TProd τ (CG_StackType τ))) with
    ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/])
      by (by asimpl).
    repeat econstructor.
    eapply (context_weakening [_; _]); eauto.
167 168 169 170
  Qed.

  Lemma CG_pop_closed (st : expr) :
    ( f, st.[f] = st)   f, (CG_pop st).[f] = CG_pop st.
171
  Proof. intros Hst f. unfold CG_pop. asimpl. rewrite ?Hst; trivial. Qed.
172

173
  Lemma CG_pop_subst (st : expr) f : (CG_pop st).[f] = CG_pop st.[f].
174 175
  Proof. unfold CG_pop; asimpl; trivial. Qed.

176 177
  Lemma steps_CG_pop_suc E ρ j K st v w :
    nclose specN  E 
178
    spec_ctx ρ  st ↦ₛ FoldV (InjRV (PairV w v)) 
179
               j  fill K (App (CG_pop (Loc st)) Unit)
180
       |={E}=> j  fill K (InjR (of_val w))  st ↦ₛ v.
181 182
  Proof.
    intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
183
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
184
    asimpl.
185
    iMod (step_load _ _ j (K ++ [CaseCtx _ _; UnfoldCtx])
186 187 188 189
                    _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. simpl.
190
    iMod (step_Fold  _ _ j (K ++ [CaseCtx _ _])
191 192 193 194
                    _ _ _ _ with "[Hj]") as "Hj"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. simpl.
195
    iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
196
    asimpl.
197
    iMod (step_snd _ _ j (K ++ [AppRCtx (RecV _); StoreRCtx (LocV _)]) _ _ _ _
198 199 200
                   _ _ with "[Hj]") as "Hj"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial.
201
    iMod (step_store _ _ j (K ++ [AppRCtx (RecV _)]) _ _ _ _ _ _
202 203 204 205
          with "[Hj Hx]") as "[Hj Hx]"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. simpl.
206
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
207
    asimpl.
208
    iMod (step_fst _ _ j (K ++ [InjRCtx]) _ _ _ _ _ _
209 210 211 212
          with "[Hj]") as "Hj"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial. asimpl.
    rewrite ?fill_app. simpl.
213
    iModIntro. iFrame "Hj Hx"; trivial.
214 215 216 217 218
    Unshelve.
    all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
    all: trivial.
  Qed.

219 220
  Lemma steps_CG_pop_fail E ρ j K st :
    nclose specN  E 
221
    spec_ctx ρ  st ↦ₛ FoldV (InjLV UnitV) 
222
               j  fill K (App (CG_pop (Loc st)) Unit)
223
       |={E}=> j  fill K (InjL Unit)  st ↦ₛ FoldV (InjLV UnitV).
224
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
    iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop.
226
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
227
    asimpl.
228
    iMod (step_load _ _ j (K ++ [CaseCtx _ _; UnfoldCtx])
229 230 231 232
                    _ _ _ with "[Hj Hx]") as "[Hj Hx]"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. simpl.
233
    iMod (step_Fold _ _ j (K ++ [CaseCtx _ _])
234 235 236 237
                    _ _ _ _ with "[Hj]") as "Hj"; eauto.
    rewrite ?fill_app. simpl.
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. simpl.
238
    iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
239
    asimpl.
240
    iModIntro. iFrame "Hj Hx"; trivial.
241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278
    Unshelve.
    all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
    all: trivial.
  Qed.

  Global Opaque CG_pop.

  Lemma CG_locked_pop_to_val st l :
    to_val (CG_locked_pop st l) = Some (CG_locked_popV st l).
  Proof. trivial. Qed.

  Lemma CG_locked_pop_of_val st l :
    of_val (CG_locked_popV st l) = CG_locked_pop st l.
  Proof. trivial. Qed.

  Global Opaque CG_locked_popV.

  Lemma CG_locked_pop_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ l LockType 
    typed Γ (CG_locked_pop st l) (TArrow TUnit (TSum TUnit τ)).
  Proof.
    intros H1 H2. repeat econstructor.
    eapply with_lock_type; auto using CG_pop_type.
  Qed.

  Lemma CG_locked_pop_closed (st l : expr) :
    ( f, st.[f] = st)  ( f, l.[f] = l) 
     f, (CG_locked_pop st l).[f] = CG_locked_pop st l.
  Proof.
    intros H1 H2 f. asimpl. unfold CG_locked_pop.
    rewrite with_lock_closed; trivial. apply CG_pop_closed; trivial.
  Qed.

  Lemma CG_locked_pop_subst (st l : expr) f :
  (CG_locked_pop st l).[f] = CG_locked_pop st.[f] l.[f].
  Proof. by rewrite with_lock_subst CG_pop_subst. Qed.

279 280
  Lemma steps_CG_locked_pop_suc E ρ j K st v w l :
    nclose specN  E 
281 282 283
    spec_ctx ρ  st ↦ₛ FoldV (InjRV (PairV w v))  l ↦ₛ (#v false)
                j  fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
       |={E}=> j  fill K (InjR (of_val w))  st ↦ₛ v  l ↦ₛ (#v false).
284
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
286
    iMod (steps_with_lock _ _ j K _ _ _ _ (InjRV w) UnitV _ _
287
          with "[Hj Hx Hl]") as "Hj"; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
288
    - iIntros (K') "[#Hspec [Hx Hj]]".
289
      iApply steps_CG_pop_suc; first done. iFrame "Hspec Hj Hx"; trivial.
290 291 292 293
    - iFrame "Hspec Hj Hx"; trivial.
      Unshelve. all: trivial.
  Qed.

294 295
  Lemma steps_CG_locked_pop_fail E ρ j K st l :
    nclose specN  E 
296 297 298
    spec_ctx ρ  st ↦ₛ FoldV (InjLV UnitV)  l ↦ₛ (#v false)
                j  fill K (App (CG_locked_pop (Loc st) (Loc l)) Unit)
       |={E}=> j  fill K (InjL Unit)  st ↦ₛ FoldV (InjLV UnitV)  l ↦ₛ (#v false).
299
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
301
    iMod (steps_with_lock _ _ j K _ _ _ _ (InjLV UnitV) UnitV _ _
302
          with "[Hj Hx Hl]") as "Hj"; last done.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
    - iIntros (K') "[#Hspec [Hx Hj]] /=".
304
      iApply steps_CG_pop_fail; first done. iFrame "Hspec Hj Hx"; trivial.
305 306 307 308 309 310
    - iFrame "Hspec Hj Hx"; trivial.
      Unshelve. all: trivial.
  Qed.

  Global Opaque CG_locked_pop.

Robbert Krebbers's avatar
Robbert Krebbers committed
311
  Lemma CG_snap_to_val st l : to_val (CG_snap st l) = Some (CG_snapV st l).
312 313
  Proof. trivial. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
314
  Lemma CG_snap_of_val st l : of_val (CG_snapV st l) = CG_snap st l.
315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
  Proof. trivial. Qed.

  Global Opaque CG_snapV.

  Lemma CG_snap_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ l LockType 
    typed Γ (CG_snap st l) (TArrow TUnit (CG_StackType τ)).
  Proof.
    intros H1 H2. repeat econstructor.
    eapply with_lock_type; trivial. do 2 constructor.
    eapply (context_weakening [_; _]); eauto.
  Qed.

  Lemma CG_snap_closed (st l : expr) :
    ( f, st.[f] = st)  ( f, l.[f] = l) 
     f, (CG_snap st l).[f] = CG_snap st l.
  Proof.
    intros H1 H2 f. asimpl. unfold CG_snap.
    rewrite with_lock_closed; trivial.
    intros f'. by asimpl; rewrite ?H1.
  Qed.

  Lemma CG_snap_subst (st l : expr) f :
339
    (CG_snap st l).[f] = CG_snap st.[f] l.[f].
340 341
  Proof. unfold CG_snap; rewrite ?with_lock_subst. by asimpl. Qed.

342 343
  Lemma steps_CG_snap E ρ j K st v l :
    nclose specN  E 
344 345 346
    spec_ctx ρ  st ↦ₛ v  l ↦ₛ (#v false)
                j  fill K (App (CG_snap (Loc st) (Loc l)) Unit)
       |={E}=> j  (fill K (of_val v))  st ↦ₛ v  l ↦ₛ (#v false).
347
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
348
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
349
    iMod (steps_with_lock _ _ j K _ _ _ _ v UnitV _ _
350
          with "[Hj Hx Hl]") as "Hj"; last done; [|by iFrame "Hspec Hx Hl Hj"].
Robbert Krebbers's avatar
Robbert Krebbers committed
351
    iIntros (K') "[#Hspec [Hx Hj]]".
352
    iMod (step_rec _ _ j K' _ _ _ _ with "[Hj]") as "Hj"; eauto.
353
    asimpl.
354
    iMod (step_load _ _ j K' _ _ _ _
355 356
          with "[Hj Hx]") as "[Hj Hx]"; eauto.
    - by iFrame "Hspec Hj Hx".
357
    - iModIntro. by iFrame "Hj Hx".
358 359 360 361 362 363 364 365 366 367
      Unshelve.
      all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
      all: trivial.
  Qed.

  Global Opaque CG_snap.

  (* Coarse-grained iter *)
  Lemma CG_iter_folding (f : expr) :
    CG_iter f =
368
    Rec (Case (Unfold (Var 1))
369 370
              Unit
              (
371
                App (Rec (App (Var 3) (Snd (Var 2))))
372
                    (App f.[ren (+3)] (Fst (Var 0)))
373
              )
374
        ).
375 376 377 378 379 380 381
  Proof. trivial. Qed.

  Lemma CG_iter_type f Γ τ :
    typed Γ f (TArrow τ TUnit) 
    typed Γ (CG_iter f) (TArrow (CG_StackType τ) TUnit).
  Proof.
    intros H1.
382 383 384 385 386 387 388
    econstructor.
    eapply (Case_typed _ _ _ _ TUnit);
      [| repeat constructor
       | repeat econstructor; eapply (context_weakening [_; _; _]); eauto].
    replace (TSum TUnit (TProd τ (CG_StackType τ))) with
    ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/])
      by (by asimpl).
389 390 391
    repeat econstructor.
  Qed.

392 393 394 395 396 397 398 399
  Lemma CG_iter_to_val f : to_val (CG_iter f) = Some (CG_iterV f).
  Proof. trivial. Qed.

  Lemma CG_iter_of_val f : of_val (CG_iterV f) = CG_iter f.
  Proof. trivial. Qed.

  Global Opaque CG_iterV.

400 401
  Lemma CG_iter_closed (f : expr) :
    ( g, f.[g] = f)   g, (CG_iter f).[g] = CG_iter f.
402
  Proof. intros Hf g. unfold CG_iter. asimpl. rewrite ?Hf; trivial. Qed.
403

Robbert Krebbers's avatar
Robbert Krebbers committed
404
  Lemma CG_iter_subst (f : expr) g : (CG_iter f).[g] = CG_iter f.[g].
405 406
  Proof. unfold CG_iter; asimpl; trivial. Qed.

407 408 409
  Lemma steps_CG_iter E ρ j K f v w :
    nclose specN  E 
    spec_ctx ρ
410
              j  fill K (App (CG_iter (of_val f))
Amin Timany's avatar
Amin Timany committed
411
                               (Fold (InjR (Pair (of_val w) (of_val v)))))
412
       |={E}=>
413
    j  fill K
414
          (App
415
             (Rec
Amin Timany's avatar
Amin Timany committed
416 417 418
                (App ((CG_iter (of_val f)).[ren (+2)])
                     (Snd (Pair ((of_val w).[ren (+2)]) (of_val v).[ren (+2)]))))
             (App (of_val f) (of_val w))).
419
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
    iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
421
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
422
    rewrite -CG_iter_folding. Opaque CG_iter. asimpl.
423
    iMod (step_Fold _ _ j (K ++ [CaseCtx _ _])
424
                    _ _ _ with "[Hj]") as "Hj"; eauto.
425
    rewrite ?fill_app /=.
426 427
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. asimpl.
428
    iMod (step_case_inr _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
429
    asimpl.
430
    iMod (step_fst _ _ j (K ++ [AppRCtx (RecV _); AppRCtx f]) _ _ _ _
431
                   _ _ with "[Hj]") as "Hj"; eauto.
432
    rewrite ?fill_app /=.
433 434
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. simpl.
435
    by iModIntro.
436 437 438 439 440 441
    Unshelve.
    all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
  Qed.

  Transparent CG_iter.

442 443
  Lemma steps_CG_iter_end E ρ j K f :
    nclose specN  E 
444
    spec_ctx ρ  j  fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
445
       |={E}=> j  fill K Unit.
446
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
447
    iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
448
    iMod (step_rec _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
449
    rewrite -CG_iter_folding. Opaque CG_iter. asimpl.
450
    iMod (step_Fold _ _ j (K ++ [CaseCtx _ _])
451
                    _ _ _ with "[Hj]") as "Hj"; eauto.
452
    rewrite ?fill_app /=.
453 454
    iFrame "Hspec Hj"; trivial.
    rewrite ?fill_app. asimpl.
455
    iMod (step_case_inl _ _ j K _ _ _ _ _ with "[Hj]") as "Hj"; eauto.
456 457 458 459 460 461 462 463 464
    Unshelve.
    all: try match goal with |- to_val _ = _ => simpl; by rewrite ?to_of_val end.
  Qed.

  Global Opaque CG_iter.

  Lemma CG_snap_iter_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ l LockType 
Robbert Krebbers's avatar
Robbert Krebbers committed
465
    typed Γ (CG_snap_iter st l) (TArrow (TArrow τ TUnit) TUnit).
466 467 468 469 470 471 472
  Proof.
    intros H1 H2; repeat econstructor.
    - eapply CG_iter_type; by constructor.
    - eapply CG_snap_type; by eapply (context_weakening [_;_]).
  Qed.

  Lemma CG_snap_iter_closed (st l : expr) :
Robbert Krebbers's avatar
Robbert Krebbers committed
473
    ( f, st.[f] = st)  ( f, l.[f] = l) 
474 475 476 477 478 479 480
     f, (CG_snap_iter st l).[f] = CG_snap_iter st l.
  Proof.
    intros H1 H2 f. unfold CG_snap_iter. asimpl. rewrite H1 H2.
    rewrite CG_snap_closed; auto.
  Qed.

  Lemma CG_snap_iter_subst (st l : expr) g :
Robbert Krebbers's avatar
Robbert Krebbers committed
481
    (CG_snap_iter st l).[g] = CG_snap_iter st.[g] l.[g].
482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503
  Proof.
    unfold CG_snap_iter; asimpl.
    rewrite CG_snap_subst CG_iter_subst. by asimpl.
  Qed.

  Lemma CG_stack_body_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ l LockType 
    typed Γ (CG_stack_body st l)
          (TProd
             (TProd (TArrow τ TUnit) (TArrow TUnit (TSum TUnit τ)))
             (TArrow (TArrow τ TUnit) TUnit)
          ).
  Proof.
    intros H1 H2.
    repeat (econstructor; eauto using CG_locked_push_type,
                          CG_locked_pop_type, CG_snap_iter_type).
  Qed.

  Opaque CG_snap_iter.

  Lemma CG_stack_body_closed (st l : expr) :
Robbert Krebbers's avatar
Robbert Krebbers committed
504
    ( f, st.[f] = st)  ( f, l.[f] = l) 
505 506 507 508 509 510 511 512 513
     f, (CG_stack_body st l).[f] = CG_stack_body st l.
  Proof.
    intros H1 H2 f. unfold CG_stack_body. asimpl.
    rewrite CG_locked_push_closed; trivial.
    rewrite CG_locked_pop_closed; trivial.
    by rewrite CG_snap_iter_closed.
  Qed.

  Lemma CG_stack_type Γ :
514
    typed Γ CG_stack
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531
          (TForall
             (TProd
                (TProd
                   (TArrow (TVar 0) TUnit)
                   (TArrow TUnit (TSum TUnit (TVar 0)))
                )
                (TArrow (TArrow (TVar 0) TUnit) TUnit)
          )).
  Proof.
    repeat econstructor.
    - eapply CG_locked_push_type; constructor; simpl; eauto.
    - eapply CG_locked_pop_type; constructor; simpl; eauto.
    - eapply CG_snap_iter_type; constructor; by simpl.
    - asimpl. repeat constructor.
    - eapply newlock_type.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
532
  Lemma CG_stack_closed f : CG_stack.[f] = CG_stack.
533 534 535 536 537
  Proof.
    unfold CG_stack.
    asimpl; rewrite ?CG_locked_push_subst ?CG_locked_pop_subst.
    asimpl. rewrite ?CG_snap_iter_subst. by asimpl.
  Qed.
538
End CG_Stack.