Commit 2191406a authored by Amin Timany's avatar Amin Timany

Add context weakening and prove typing for locks

parent dd0e26e8
From iris.proofmode Require Import invariants ghost_ownership tactics.
From F_mu_ref_par Require Import lang rules rules_binary.
From F_mu_ref_par Require Import lang rules rules_binary typing.
Import uPred.
Definition newlock : expr := Alloc ( false).
......@@ -17,9 +17,99 @@ Definition with_lock (e : expr) (l : expr) : expr :=
l
.
Lemma newlock_closed f : newlock.[f] = newlock.
Proof. by asimpl. Qed.
Lemma acquire_closed f : acquire.[f] = acquire.
Proof. by asimpl. Qed.
Lemma release_closed f : release.[f] = release.
Proof. by asimpl. Qed.
Lemma with_lock_closed e l:
( f : var expr, e.[f] = e)
( f : var expr, l.[f] = l)
f, (with_lock e l).[f] = with_lock e l.
Proof. asimpl => H1 H2 f. by rewrite H1 H2. Qed.
Definition LockType := Tref TBool.
Lemma newlock_type Γ : typed Γ newlock LockType.
Proof. repeat constructor. Qed.
Lemma acquire_type Γ : typed Γ acquire (TArrow LockType TUnit).
Proof. do 3 econstructor; eauto using EqTBool; repeat constructor. Qed.
Lemma release_type Γ : typed Γ release (TArrow LockType TUnit).
Proof. repeat econstructor. Qed.
Lemma with_lock_type e l Γ τ :
( f : var expr, e.[f] = e)
typed Γ e (TArrow TUnit τ)
typed Γ l LockType
typed Γ (with_lock e l) TUnit.
Proof.
intros H1 H2 H3. econstructor; eauto.
repeat (econstructor; eauto using release_type, acquire_type).
eapply (closed_context_weakening [_; _; _; _]); eauto.
Qed.
Section proof.
Context {Σ : gFunctors} {iS : cfgSG Σ}.
Context (S : namespace).
Lemma steps_newlock N E ρ j K :
nclose N E
(((Spec_ctx N ρ j (fill K (newlock)))%I)
|={E}=>( l, j (fill K (Loc l)) l ↦ₛ (v false))%I).
Proof.
intros HNE.
iIntros "[#Hspec Hj]".
iPvs (step_alloc _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iFrame "Hspec Hj"; trivial.
Unshelve. all: trivial.
Qed.
Global Opaque newlock.
Lemma steps_acquire N E ρ j K l :
nclose N E
(((Spec_ctx N ρ l ↦ₛ (v false) j (fill K (App acquire (Loc l))))%I)
|={E}=>(j (fill K Unit) l ↦ₛ (v true))%I).
Proof.
intros HNE.
iIntros "[#Hspec [Hl Hj]]". unfold acquire.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iFrame "Hspec Hj"; trivial. simpl.
iPvs (step_cas_suc _ _ _ j (K ++ [IfCtx _ _])
_ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj Hl"; trivial.
iNext; trivial.
rewrite ?fill_app. simpl.
iPvs (step_if_true _ _ _ j K _ _ _ with "[Hj]") as "Hj"; trivial.
iFrame "Hspec Hj"; trivial.
iPvsIntro. iFrame "Hj Hl"; trivial.
Unshelve. all:trivial.
Qed.
Global Opaque acquire.
Lemma steps_release N E ρ j K l b:
nclose N E
(((Spec_ctx N ρ l ↦ₛ (v b) j (fill K (App release (Loc l))))%I)
|={E}=>(j (fill K Unit) l ↦ₛ (v false))%I).
Proof.
intros HNE.
iIntros "[#Hspec [Hl Hj]]". unfold release.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iFrame "Hspec Hj"; trivial. simpl.
iPvs (step_store _ _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
iFrame "Hspec Hj"; trivial.
iPvsIntro. iFrame "Hj Hl"; trivial.
Unshelve. all: trivial.
Qed.
Global Opaque release.
Lemma steps_with_lock N E ρ j K e l P Q :
nclose N E
......@@ -28,55 +118,37 @@ Section proof.
( v, K', ((Spec_ctx N ρ P j (fill K' (App e Unit)))%I)
|={E}=>(j (fill K' (of_val v)) Q)%I)
(((Spec_ctx N ρ P l ↦ₛ (v false) j (fill K (with_lock e (Loc l))))%I)
(((Spec_ctx N ρ P l ↦ₛ (v false)
j (fill K (with_lock e (Loc l))))%I)
|={E}=>(j (fill K (Unit)) Q l ↦ₛ (v false))%I).
Proof.
intros HNE H1 [v H2].
iIntros "[#Hspec [HP [Hl Hj]]]".
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iFrame "Hspec Hj"; trivial. simpl.
rewrite acquire_closed release_closed H1. asimpl.
iPvs (steps_acquire _ _ _ j (K ++ [AppRCtx (LamV _)])
_ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
rewrite fill_app; simpl.
iFrame "Hspec Hj"; trivial.
asimpl.
Unshelve. 3: simpl; auto.
iPvs (step_lam _ _ _ j (K ++ [AppRCtx (LamV _)])
_ _ _ _ with "[Hj]") as "Hj"; eauto.
rewrite fill_app. simpl.
iFrame "Hspec Hj"; trivial.
Unshelve. 3: simpl; trivial.
asimpl.
iPvs (step_cas_suc _ _ _ j (K ++ [AppRCtx (LamV _); IfCtx _ _])
_ _ _ _ _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; trivial.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj Hl"; trivial.
Unshelve. 7: simpl; trivial. 5: simpl; trivial. 4: trivial.
iNext; trivial.
rewrite fill_app. simpl.
iPvs (step_if_true _ _ _ j (K ++ [AppRCtx (LamV _)])
_ _ _ with "[Hj]") as "Hj"; trivial.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial.
rewrite fill_app. simpl.
Unshelve. all: trivial.
rewrite fill_app; simpl.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iFrame "Hspec Hj"; trivial.
asimpl.
Unshelve. 3: simpl; auto.
rewrite H1.
iFrame "Hspec Hj"; trivial. asimpl.
rewrite release_closed H1.
iPvs (H2 (K ++ [AppRCtx (LamV _)]) with "[Hj HP]") as "[Hj HQ]"; eauto.
rewrite ?fill_app. simpl.
iFrame "Hspec Hj"; trivial.
rewrite ?fill_app. simpl.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iFrame "Hspec Hj"; trivial.
asimpl.
Unshelve. 3: auto using to_of_val.
iPvs (step_lam _ _ _ j K _ _ _ _ with "[Hj]") as "Hj"; eauto.
iFrame "Hspec Hj"; trivial.
asimpl.
Unshelve. 3: simpl; auto.
iPvs (step_store _ _ _ j K _ _ _ _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
iFrame "Hspec Hj"; trivial.
Unshelve. 3: auto.
iPvsIntro. iFrame "HQ Hj Hl"; trivial.
iFrame "Hspec Hj"; trivial. simpl.
rewrite release_closed.
iPvs (steps_release _ _ _ j K _ _ with "[Hj Hl]") as "[Hj Hl]"; eauto.
iFrame "Hspec Hl Hj"; trivial.
iPvsIntro. iFrame "Hj HQ Hl"; trivial.
Unshelve.
all: try match goal with |- to_val _ = _ => auto using to_of_val end.
trivial.
Qed.
Global Opaque with_lock.
End proof.
\ No newline at end of file
......@@ -79,15 +79,16 @@ Inductive typed (Γ : list type) : expr → type → Prop :=
.
Local Hint Extern 1 =>
match goal with [H : context [length (map _ _)] |- _] => rewrite map_length in H end
: typed_subst_invariant.
match goal with [H : context [length (map _ _)] |- _] =>
rewrite map_length in H end : typed_subst_invariant.
Lemma typed_subst_invariant Γ e τ s1 s2 :
typed Γ e τ ( x, x < length Γ s1 x = s2 x) e.[s1] = e.[s2].
Proof.
intros Htyped; revert s1 s2.
assert ( {A} `{Ids A} `{Rename A}
(s1 s2 : nat A) x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
(s1 s2 : nat A) x, (x 0 s1 (pred x) = s2 (pred x))
up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
(induction Htyped => s1 s2 Hs; f_equal/=);
eauto using lookup_lt_Some with omega typed_subst_invariant.
......@@ -96,6 +97,44 @@ Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option (Var x) (of_val <$> vs !! x).
Lemma context_gen_weakening ξ Γ' Γ e τ :
typed (Γ' ++ Γ) e τ
typed (Γ' ++ ξ ++ Γ) e.[iter (List.length Γ') up (ren (+ (List.length ξ)))] τ.
Proof.
intros H1.
remember (Γ' ++ Γ) as Ξ. revert Γ' Γ ξ HeqΞ.
induction H1 => Γ1 Γ2 ξ HeqΞ; subst; asimpl in *; eauto using typed.
- rewrite iter_up; destruct lt_dec as [Hl | Hl].
+ constructor. rewrite lookup_app_l; trivial. by rewrite lookup_app_l in H.
+ asimpl. constructor. rewrite lookup_app_r; auto with omega.
rewrite lookup_app_r; auto with omega.
rewrite lookup_app_r in H; auto with omega.
match goal with
|- _ !! ?A = _ => by replace A with (x - List.length Γ1) by omega
end.
- econstructor; eauto.
+ eapply (IHtyped2 (_ :: Γ1) Γ2 ξ Logic.eq_refl).
+ eapply (IHtyped3 (_ :: Γ1) Γ2 ξ Logic.eq_refl).
- constructor.
eapply (IHtyped (_ :: _ :: Γ1) Γ2 ξ Logic.eq_refl).
- constructor.
specialize (IHtyped
(map (λ t : type, t.[ren (+1)]) Γ1)
(map (λ t : type, t.[ren (+1)]) Γ2)
(map (λ t : type, t.[ren (+1)]) ξ)).
asimpl in *. rewrite ?map_length in IHtyped.
repeat rewrite map_app. apply IHtyped.
by repeat rewrite map_app.
Qed.
Lemma context_weakening ξ Γ e τ :
typed Γ e τ typed (ξ ++ Γ) e.[(ren (+ (List.length ξ)))] τ.
Proof. eapply (context_gen_weakening _ []). Qed.
Lemma closed_context_weakening ξ Γ e τ :
( f, e.[f] = e) typed Γ e τ typed (ξ ++ Γ) e τ.
Proof. intros H1 H2. erewrite <- H1. by eapply context_weakening. Qed.
Notation "# v" := (of_val v) (at level 20).
Lemma typed_subst_head_simpl Δ τ e w ws :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment