CG_stack.v 15.2 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.

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

Amin Timany's avatar
Amin Timany committed
84 85 86 87 88 89
  Lemma steps_CG_push E ρ j K st v w :
    nclose specN  E 
    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)).
  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.
91
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
92
    iMod (step_load _ _ j (PairRCtx _ :: InjRCtx :: FoldCtx :: StoreRCtx (LocV _) :: K)
Amin Timany's avatar
Amin Timany committed
93 94 95 96
            with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    simpl.
    iMod (step_store _ _ j K with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    { 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 128 129 130 131 132 133

  Lemma steps_CG_locked_push E ρ j K st w v l :
    nclose specN  E 
    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).
  Proof.
    intros HNE. iIntros "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_push.
Amin Timany's avatar
Amin Timany committed
134 135 136 137
    iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ v)%I _ UnitV with "[$Hj $Hx $Hl]")
      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 168 169 170 171 172 173

  Lemma steps_CG_pop_suc E ρ j K st v w :
    nclose specN  E 
    spec_ctx ρ  st ↦ₛ FoldV (InjRV (PairV w v)) 
               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.
175
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
176 177
    iMod (step_load _ _ _ (UnfoldCtx :: CaseCtx _ _ :: K)  with "[$Hj $Hx]")
      as "[Hj Hx]"; eauto.
Amin Timany's avatar
Amin Timany committed
178
    simpl.
Amin Timany's avatar
Amin Timany committed
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.
182
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
183 184
    iMod (do_step_pure _ _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K)
            with "[$Hj]") as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
185
    simpl.
Amin Timany's avatar
Amin Timany committed
186 187 188 189 190 191 192
    iMod (step_store _ _ j (SeqCtx _ :: K) with "[$Hj $Hx]") as "[Hj Hx]";
      eauto using to_of_val.
    simpl.
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iMod (do_step_pure _ _ _ (InjRCtx :: K) with "[$Hj]") as "Hj"; eauto.
    simpl.
    by iFrame "Hj Hx".
Amin Timany's avatar
Amin Timany committed
193 194 195 196 197 198 199 200 201
  Qed.

  Lemma steps_CG_pop_fail E ρ j K st :
    nclose specN  E 
    spec_ctx ρ  st ↦ₛ FoldV (InjLV UnitV) 
               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.
203
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
204
    iMod (step_load _ _ j (UnfoldCtx :: CaseCtx _ _ :: K)
Amin Timany's avatar
Amin Timany committed
205 206 207 208 209
                    _ _ _ with "[$Hj $Hx]") as "[Hj Hx]"; eauto.
    iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
    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 241 242 243 244 245 246

  Lemma steps_CG_locked_pop_suc E ρ j K st v w l :
    nclose specN  E 
    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).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
Amin Timany's avatar
Amin Timany committed
247 248 249 250 251
    iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ FoldV (InjRV (PairV w v)))%I
                          _ (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 254 255 256 257 258 259 260
  Qed.

  Lemma steps_CG_locked_pop_fail E ρ j K st l :
    nclose specN  E 
    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).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_locked_pop.
Amin Timany's avatar
Amin Timany committed
261 262 263 264 265
    iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ FoldV (InjLV UnitV))%I _
                          (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 297 298 299 300 301 302

  Lemma steps_CG_snap E ρ j K st v l :
    nclose specN  E 
    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).
  Proof.
    iIntros (HNE) "[#Hspec [Hx [Hl Hj]]]". unfold CG_snap.
Amin Timany's avatar
Amin Timany committed
303 304
    iMod (steps_with_lock _ _ _ _ _ _ (st ↦ₛ v)%I _ v UnitV
          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.
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 357 358 359 360 361 362

  Lemma steps_CG_iter E ρ j K f v w :
    nclose specN  E 
    spec_ctx ρ
              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 369
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iAsimpl.
    iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
370
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
371
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
372
    iAsimpl.
Amin Timany's avatar
Amin Timany committed
373 374
    iMod (do_step_pure _ _ _ (AppRCtx f :: SeqCtx _ :: K) with "[$Hj]")
      as "Hj"; eauto.
Amin Timany's avatar
Amin Timany committed
375 376 377 378 379 380 381 382
  Qed.

  Lemma steps_CG_iter_end E ρ j K f :
    nclose specN  E 
    spec_ctx ρ  j  fill K (App (CG_iter (of_val f)) (Fold (InjL Unit)))
       |={E}=> j  fill K Unit.
  Proof.
    iIntros (HNE) "[#Hspec Hj]". unfold CG_iter.
Amin Timany's avatar
Amin Timany committed
383 384
    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
    iMod (do_step_pure _ _ _ (CaseCtx _ _ :: K) with "[$Hj]") as "Hj"; eauto.
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 454 455 456 457 458 459 460 461 462 463

Global Hint Rewrite CG_push_subst : autosubst.
Global Hint Rewrite CG_locked_push_subst : autosubst.
Global Hint Rewrite CG_locked_pop_subst : autosubst.
Global Hint Rewrite CG_pop_subst : autosubst.
Global Hint Rewrite CG_locked_pop_subst : autosubst.
Global Hint Rewrite CG_snap_subst : autosubst.
Global Hint Rewrite CG_iter_subst : autosubst.
Global Hint Rewrite CG_snap_iter_subst : autosubst.
Global Hint Rewrite CG_stack_body_subst : autosubst.
Global Hint Rewrite CG_stack_closed : autosubst.