CG_stack.v 15.1 KB
Newer Older
Amin Timany's avatar
Amin Timany committed
1
From iris.proofmode Require Import tactics.
Amin Timany's avatar
Amin Timany committed
2
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
Amin Timany's avatar
Amin Timany committed
3 4 5 6 7 8 9
Import uPred.

Definition CG_StackType τ :=
  TRec (TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).

(* Coarse-grained push *)
Definition CG_push (st : expr) : expr :=
Amin Timany's avatar
Amin Timany committed
10
  Lam (Store (st.[ren (+1)]) (Fold (InjR (Pair (Var 0) (Load st.[ren (+ 1)]))))).
Amin Timany's avatar
Amin Timany committed
11 12 13 14 15

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 :=
Amin Timany's avatar
Amin Timany committed
16
  Lam (Case (Unfold (Load st.[ren (+ 1)]))
Amin Timany's avatar
Amin Timany committed
17 18
            (InjL Unit)
            (
Amin Timany's avatar
Amin Timany committed
19 20 21
              Seq
                (Store st.[ren (+ 2)] (Snd (Var 0)))
                (InjR (Fst (Var 0)))
Amin Timany's avatar
Amin Timany committed
22 23 24 25 26 27
            )
      ).

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.

Amin Timany's avatar
Amin Timany committed
28 29
Definition CG_snap (st l : expr) :=  with_lock (Lam (Load st.[ren (+1)])) l.
Definition CG_snapV (st l : expr) : val := with_lockV (Lam (Load st.[ren (+1)])) l.
Amin Timany's avatar
Amin Timany committed
30 31 32 33 34

Definition CG_iter (f : expr) : expr :=
  Rec (Case (Unfold (Var 1))
            Unit
            (
Amin Timany's avatar
Amin Timany committed
35 36 37
              Seq
                (App f.[ren (+3)] (Fst (Var 0)))
                (App (Var 1) (Snd (Var 0)))
Amin Timany's avatar
Amin Timany committed
38 39 40 41 42 43 44
            )
      ).

Definition CG_iterV (f : expr) : val :=
  RecV (Case (Unfold (Var 1))
            Unit
            (
Amin Timany's avatar
Amin Timany committed
45 46 47
              Seq
                (App f.[ren (+3)] (Fst (Var 0)))
                (App (Var 1) (Snd (Var 0)))
Amin Timany's avatar
Amin Timany committed
48 49 50 51
            )
      ).

Definition CG_snap_iter (st l : expr) : expr :=
Amin Timany's avatar
Amin Timany committed
52 53
  Lam (App (CG_iter (Var 0)) (App (CG_snap st.[ren (+1)] l.[ren (+1)]) Unit)).

Amin Timany's avatar
Amin Timany committed
54 55 56 57 58
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 :=
Amin Timany's avatar
Amin Timany committed
59 60 61 62 63 64
  TLam (
      LetIn
        newlock
        (LetIn
           (Alloc (Fold (InjL Unit)))
           (CG_stack_body (Var 0) (Var 1)))).
Amin Timany's avatar
Amin Timany committed
65 66 67 68 69 70 71 72 73

Section CG_Stack.
  Context `{heapIG Σ, cfgSG Σ}.

  Lemma CG_push_type st Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ (CG_push st) (TArrow τ TUnit).
  Proof.
    intros H1. repeat econstructor.
Amin Timany's avatar
Amin Timany committed
74
    eapply (context_weakening [_]); eauto.
Amin Timany's avatar
Amin Timany committed
75
    repeat constructor; asimpl; trivial.
Amin Timany's avatar
Amin Timany committed
76
    eapply (context_weakening [_]); eauto.
Amin Timany's avatar
Amin Timany committed
77 78 79 80 81
  Qed.

  Lemma CG_push_subst (st : expr) f : (CG_push st).[f] = CG_push st.[f].
  Proof. unfold CG_push; asimpl; trivial. Qed.

Ralf Jung's avatar
Ralf Jung committed
82
  Hint Rewrite CG_push_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
83

84
  Lemma steps_CG_push E j K st v w :
Amin Timany's avatar
Amin Timany committed
85
    nclose specN  E 
86
    spec_ctx  st ↦ₛ v  j  fill K (App (CG_push (Loc st)) (of_val w))
Amin Timany's avatar
Amin Timany committed
87 88 89
     |={E}=> j  fill K Unit  st ↦ₛ FoldV (InjRV (PairV w v)).
  Proof.
    intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_push.
Amin Timany's avatar
Amin Timany committed
90
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
    iAsimpl.
92
    iMod (step_load _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K)
Amin Timany's avatar
Amin Timany committed
93 94
            with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    simpl.
95
    iMod (step_store _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
Amin Timany's avatar
Amin Timany committed
96
    { rewrite /= !to_of_val //. }
Amin Timany's avatar
Amin Timany committed
97 98 99
    iModIntro. by iFrame.
  Qed.

100
  Typeclasses Opaque CG_push.
Amin Timany's avatar
Amin Timany committed
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
  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_subst (st l : expr) f :
    (CG_locked_push st l).[f] = CG_locked_push st.[f] l.[f].
Amin Timany's avatar
Amin Timany committed
123 124 125
  Proof. by rewrite /CG_locked_push; asimpl. Qed.

  Hint Rewrite CG_locked_push_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
126

127
  Lemma steps_CG_locked_push E j K st w v l :
Amin Timany's avatar
Amin Timany committed
128
    nclose specN  E 
129
    spec_ctx  st ↦ₛ v  l ↦ₛ (#v false)
Amin Timany's avatar
Amin Timany committed
130 131 132 133
       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).
  Proof.
    intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
134
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ v)%I _ UnitV with "[$Hj $Hx $Hl]")
Amin Timany's avatar
Amin Timany committed
135 136 137
      as "Hj"; auto.
    iIntros (K') "[#Hspec Hxj]".
    iApply steps_CG_push; first done. by iFrame.
Amin Timany's avatar
Amin Timany committed
138 139
  Qed.

140
  Typeclasses Opaque CG_locked_push.
Amin Timany's avatar
Amin Timany committed
141 142 143 144 145 146 147 148 149
  Global Opaque CG_locked_push.

  (* Coarse-grained pop *)
  Lemma CG_pop_type st Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ (CG_pop st) (TArrow TUnit (TSum TUnit τ)).
  Proof.
    intros H1.
    econstructor.
Amin Timany's avatar
Amin Timany committed
150 151 152 153 154 155 156 157 158
    eapply (Case_typed _ _ _ _ TUnit); eauto using typed.
    - 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.
    - econstructor; eauto using typed.
      econstructor; eauto using typed.
      eapply (context_weakening [_; _]); eauto.
Amin Timany's avatar
Amin Timany committed
159 160
  Qed.

Amin Timany's avatar
Amin Timany committed
161 162 163
  Lemma CG_pop_subst (st : expr) f :
    (CG_pop st).[f] = CG_pop st.[f].
  Proof. by rewrite /CG_pop; asimpl. Qed.
Amin Timany's avatar
Amin Timany committed
164

Amin Timany's avatar
Amin Timany committed
165
  Hint Rewrite CG_pop_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
166

167
  Lemma steps_CG_pop_suc E j K st v w :
Amin Timany's avatar
Amin Timany committed
168
    nclose specN  E 
169
    spec_ctx  st ↦ₛ FoldV (InjRV (PairV w v)) 
Amin Timany's avatar
Amin Timany committed
170 171 172 173
               j  fill K (App (CG_pop (Loc st)) Unit)
       |={E}=> j  fill K (InjR (of_val w))  st ↦ₛ v.
  Proof.
    intros HNE. iIntros "[#Hspec [Hx Hj]]". unfold CG_pop.
Amin Timany's avatar
Amin Timany committed
174
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
    iAsimpl.
176
    iMod (step_load _ _ (UnfoldCtx :: CaseCtx _ _ :: K)  with "[$Hj $Hx]")
Amin Timany's avatar
Amin Timany committed
177
      as "[Hj Hx]"; eauto.
Amin Timany's avatar
Amin Timany committed
178
    simpl.
179
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
180
    simpl.
Amin Timany's avatar
Amin Timany committed
181
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
    iAsimpl.
183
    iMod (do_step_pure _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K)
Amin Timany's avatar
Amin Timany committed
184
            with "[$Hj]") as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
185
    simpl.
186
    iMod (step_store _ j (SeqCtx _ :: K) with "[$Hj $Hx]") as "[Hj Hx]";
Amin Timany's avatar
Amin Timany committed
187 188 189
      eauto using to_of_val.
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
190
    iMod (do_step_pure _ _ (InjRCtx :: K) with "[$Hj]") as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
191 192
    simpl.
    by iFrame "Hj Hx".
Amin Timany's avatar
Amin Timany committed
193 194
  Qed.

195
  Lemma steps_CG_pop_fail E j K st :
Amin Timany's avatar
Amin Timany committed
196
    nclose specN  E 
197
    spec_ctx  st ↦ₛ FoldV (InjLV UnitV) 
Amin Timany's avatar
Amin Timany committed
198 199 200 201
               j  fill K (App (CG_pop (Loc st)) Unit)
       |={E}=> j  fill K (InjL Unit)  st ↦ₛ FoldV (InjLV UnitV).
  Proof.
    iIntros (HNE) "[#Hspec [Hx Hj]]". unfold CG_pop.
Amin Timany's avatar
Amin Timany committed
202
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
203
    iAsimpl.
204
    iMod (step_load _ j (UnfoldCtx :: CaseCtx _ _ :: K)
Amin Timany's avatar
Amin Timany committed
205
                    _ _ _ with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
206
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
207 208 209
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    by iFrame "Hj Hx"; trivial.
Amin Timany's avatar
Amin Timany committed
210 211
  Qed.

212
  Typeclasses Opaque CG_pop.
Amin Timany's avatar
Amin Timany committed
213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234
  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_subst (st l : expr) f :
Amin Timany's avatar
Amin Timany committed
235 236 237 238
    (CG_locked_pop st l).[f] = CG_locked_pop st.[f] l.[f].
  Proof. by rewrite /CG_locked_pop; asimpl. Qed.

  Hint Rewrite CG_locked_pop_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
239

240
  Lemma steps_CG_locked_pop_suc E j K st v w l :
Amin Timany's avatar
Amin Timany committed
241
    nclose specN  E 
242
    spec_ctx  st ↦ₛ FoldV (InjRV (PairV w v))  l ↦ₛ (#v false)
Amin Timany's avatar
Amin Timany committed
243 244 245 246
                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).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
247
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ FoldV (InjRV (PairV w v)))%I
Amin Timany's avatar
Amin Timany committed
248 249 250 251
                          _ (InjRV w) UnitV
            with "[$Hj $Hx $Hl]") as "Hj"; eauto.
    iIntros (K') "[#Hspec Hxj]".
    iApply steps_CG_pop_suc; eauto.
Amin Timany's avatar
Amin Timany committed
252 253
  Qed.

254
  Lemma steps_CG_locked_pop_fail E j K st l :
Amin Timany's avatar
Amin Timany committed
255
    nclose specN  E 
256
    spec_ctx  st ↦ₛ FoldV (InjLV UnitV)  l ↦ₛ (#v false)
Amin Timany's avatar
Amin Timany committed
257 258 259 260
                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).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
261
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ FoldV (InjLV UnitV))%I _
Amin Timany's avatar
Amin Timany committed
262 263 264 265
                          (InjLV UnitV) UnitV
          with "[$Hj $Hx $Hl]") as "Hj"; eauto.
    iIntros (K') "[#Hspec Hxj] /=".
      iApply steps_CG_pop_fail; eauto.
Amin Timany's avatar
Amin Timany committed
266 267
  Qed.

268
  Typeclasses Opaque CG_locked_pop.
Amin Timany's avatar
Amin Timany committed
269 270 271 272 273 274 275 276
  Global Opaque CG_locked_pop.

  Lemma CG_snap_to_val st l : to_val (CG_snap st l) = Some (CG_snapV st l).
  Proof. trivial. Qed.

  Lemma CG_snap_of_val st l : of_val (CG_snapV st l) = CG_snap st l.
  Proof. trivial. Qed.

277
  Typeclasses Opaque CG_snapV.
Amin Timany's avatar
Amin Timany committed
278 279 280 281 282 283 284 285 286
  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.
Amin Timany's avatar
Amin Timany committed
287
    eapply (context_weakening [_]); eauto.
Amin Timany's avatar
Amin Timany committed
288 289 290 291
  Qed.

  Lemma CG_snap_subst (st l : expr) f :
    (CG_snap st l).[f] = CG_snap st.[f] l.[f].
Amin Timany's avatar
Amin Timany committed
292 293 294
  Proof. by unfold CG_snap; asimpl. Qed.

  Hint Rewrite CG_snap_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
295

296
  Lemma steps_CG_snap E j K st v l :
Amin Timany's avatar
Amin Timany committed
297
    nclose specN  E 
298
    spec_ctx  st ↦ₛ v  l ↦ₛ (#v false)
Amin Timany's avatar
Amin Timany committed
299 300 301 302
                j  fill K (App (CG_snap (Loc st) (Loc l)) Unit)
       |={E}=> j  (fill K (of_val v))  st ↦ₛ v  l ↦ₛ (#v false).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
303
    iMod (steps_with_lock _ _ _ _ _ (st ↦ₛ v)%I _ v UnitV
Amin Timany's avatar
Amin Timany committed
304
          with "[$Hj $Hx $Hl]") as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
305
    iIntros (K') "[#Hspec [Hx Hj]]".
Amin Timany's avatar
Amin Timany committed
306
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
308 309
    iMod (step_load with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    by iFrame.
Amin Timany's avatar
Amin Timany committed
310 311
  Qed.

312
  Typeclasses Opaque CG_snap.
Amin Timany's avatar
Amin Timany committed
313 314 315 316 317 318 319 320
  Global Opaque CG_snap.

  (* Coarse-grained iter *)
  Lemma CG_iter_folding (f : expr) :
    CG_iter f =
    Rec (Case (Unfold (Var 1))
              Unit
              (
Amin Timany's avatar
Amin Timany committed
321 322 323
                Seq
                  (App f.[ren (+3)] (Fst (Var 0)))
                  (App (Var 1) (Snd (Var 0)))
Amin Timany's avatar
Amin Timany committed
324 325 326 327 328 329 330 331
              )
        ).
  Proof. trivial. Qed.

  Lemma CG_iter_type f Γ τ :
    typed Γ f (TArrow τ TUnit) 
    typed Γ (CG_iter f) (TArrow (CG_StackType τ) TUnit).
  Proof.
Amin Timany's avatar
Amin Timany committed
332 333
    intros ?. econstructor.
    eapply (Case_typed _ _ _ _ TUnit); eauto using typed.
Amin Timany's avatar
Amin Timany committed
334 335 336 337
    replace (TSum TUnit (TProd τ (CG_StackType τ))) with
    ((TSum TUnit (TProd τ.[ren (+1)] (TVar 0))).[(CG_StackType τ)/])
      by (by asimpl).
    repeat econstructor.
Amin Timany's avatar
Amin Timany committed
338 339
    repeat econstructor; simpl; eauto using typed.
    eapply (context_weakening [_; _; _]); eauto.
Amin Timany's avatar
Amin Timany committed
340 341 342 343 344 345 346 347
  Qed.

  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.

348
  Typeclasses Opaque CG_iterV.
Amin Timany's avatar
Amin Timany committed
349 350 351
  Global Opaque CG_iterV.

  Lemma CG_iter_subst (f : expr) g : (CG_iter f).[g] = CG_iter f.[g].
Amin Timany's avatar
Amin Timany committed
352 353 354
  Proof. by unfold CG_iter; asimpl. Qed.

  Hint Rewrite CG_iter_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
355

356
  Lemma steps_CG_iter E j K f v w :
Amin Timany's avatar
Amin Timany committed
357
    nclose specN  E 
358
    spec_ctx
Amin Timany's avatar
Amin Timany committed
359 360 361 362
              j  fill K (App (CG_iter (of_val f))
                               (Fold (InjR (Pair (of_val w) (of_val v)))))
       |={E}=>
    j  fill K
Amin Timany's avatar
Amin Timany committed
363 364
          (Seq (App (of_val f) (of_val w))
               (App (CG_iter (of_val f)) (Snd (Pair (of_val w) (of_val v))))).
Amin Timany's avatar
Amin Timany committed
365 366
  Proof.
    iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
Amin Timany's avatar
Amin Timany committed
367 368
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
369
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
370
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
371
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
372
    iAsimpl.
373
    iMod (do_step_pure _ _ (AppRCtx f :: SeqCtx _ :: K) with "[$Hj]")
Amin Timany's avatar
Amin Timany committed
374
      as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
375 376
  Qed.

377
  Lemma steps_CG_iter_end E j K f :
Amin Timany's avatar
Amin Timany committed
378
    nclose specN  E 
379
    spec_ctx  j  fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
Amin Timany's avatar
Amin Timany committed
380 381 382
       |={E}=> j  fill K Unit.
  Proof.
    iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
Amin Timany's avatar
Amin Timany committed
383
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
384
    iMod (do_step_pure _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
385
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
386
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
387 388
  Qed.

389
  Typeclasses Opaque CG_iter.
Amin Timany's avatar
Amin Timany committed
390 391 392 393 394 395 396 397 398
  Global Opaque CG_iter.

  Lemma CG_snap_iter_type st l Γ τ :
    typed Γ st (Tref (CG_StackType τ)) 
    typed Γ l LockType 
    typed Γ (CG_snap_iter st l) (TArrow (TArrow τ TUnit) TUnit).
  Proof.
    intros H1 H2; repeat econstructor.
    - eapply CG_iter_type; by constructor.
Amin Timany's avatar
Amin Timany committed
399
    - eapply CG_snap_type; by eapply (context_weakening [_]).
Amin Timany's avatar
Amin Timany committed
400 401 402 403
  Qed.

  Lemma CG_snap_iter_subst (st l : expr) g :
    (CG_snap_iter st l).[g] = CG_snap_iter st.[g] l.[g].
Amin Timany's avatar
Amin Timany committed
404 405 406
  Proof. by unfold CG_snap_iter; asimpl. Qed.

  Hint Rewrite CG_snap_iter_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422

  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.


423
  Typeclasses Opaque CG_snap_iter.
Amin Timany's avatar
Amin Timany committed
424 425 426 427 428 429 430
  Global Opaque CG_snap_iter.

  Lemma CG_stack_body_subst (st l : expr) f :
    (CG_stack_body st l).[f] = CG_stack_body st.[f] l.[f].
  Proof. by unfold CG_stack_body; asimpl. Qed.

  Hint Rewrite CG_stack_body_subst : autosubst.
Amin Timany's avatar
Amin Timany committed
431 432 433 434 435 436 437 438 439 440 441 442

  Lemma CG_stack_type Γ :
    typed Γ CG_stack
          (TForall
             (TProd
                (TProd
                   (TArrow (TVar 0) TUnit)
                   (TArrow TUnit (TSum TUnit (TVar 0)))
                )
                (TArrow (TArrow (TVar 0) TUnit) TUnit)
          )).
  Proof.
Amin Timany's avatar
Amin Timany committed
443 444 445 446
    repeat econstructor;
      eauto 10 using newlock_type, CG_locked_push_type, CG_locked_pop_type,
      CG_snap_iter_type, typed.
    asimpl; repeat constructor.
Amin Timany's avatar
Amin Timany committed
447 448 449
  Qed.

  Lemma CG_stack_closed f : CG_stack.[f] = CG_stack.
Amin Timany's avatar
Amin Timany committed
450 451
  Proof. by unfold CG_stack; asimpl. Qed.

Amin Timany's avatar
Amin Timany committed
452
End CG_Stack.
Amin Timany's avatar
Amin Timany committed
453

Ralf Jung's avatar
Ralf Jung committed
454 455 456 457 458 459 460 461 462 463
Hint Rewrite CG_push_subst : autosubst.
Hint Rewrite CG_locked_push_subst : autosubst.
Hint Rewrite CG_locked_pop_subst : autosubst.
Hint Rewrite CG_pop_subst : autosubst.
Hint Rewrite CG_locked_pop_subst : autosubst.
Hint Rewrite CG_snap_subst : autosubst.
Hint Rewrite CG_iter_subst : autosubst.
Hint Rewrite CG_snap_iter_subst : autosubst.
Hint Rewrite CG_stack_body_subst : autosubst.
Hint Rewrite CG_stack_closed : autosubst.