From cgraphs.locks.lambdalock Require Export langdef definitions.
Notation vertex := nat.
Inductive label : Type :=
| BarrierLabel (b : bool) (t1 t2 : type)
| LockLabel (c : lockcap) (t : type).
Canonical Structure typeO := leibnizO type.
Canonical Structure labelO := leibnizO label.
Notation rProp := (hProp vertex labelO).
Definition linbox l (P : rProp) : rProp :=
match l with
| Lin => P
| Unr => □ P
end.
Fixpoint rtyped (Γ : env) e t : rProp :=
match e with
| Val v => ⌜⌜ env_unr Γ ⌝⌝ ∗ vtyped v t
| Var x => ⌜⌜ env_var Γ x t ⌝⌝
| Fun x e =>
∃ l t1 t2, ⌜⌜ t = FunT l t1 t2 ⌝⌝ ∗
∃ Γ', ⌜⌜ env_bind Γ' x t1 Γ ∧ (l = Unr -> env_unr Γ) ⌝⌝ ∗
linbox l (rtyped Γ' e t2)
| App e1 e2 =>
∃ Γ1 Γ2, ⌜⌜ env_split Γ Γ1 Γ2 ⌝⌝ ∗
∃ t1 l,
rtyped Γ1 e1 (FunT l t1 t) ∗
rtyped Γ2 e2 t1
| Unit => ⌜⌜ t = UnitT ∧ env_unr Γ ⌝⌝
| Pair e1 e2 =>
∃ Γ1 Γ2, ⌜⌜ env_split Γ Γ1 Γ2 ⌝⌝ ∗
∃ t1 t2, ⌜⌜ t = PairT t1 t2 ⌝⌝ ∗
rtyped Γ1 e1 t1 ∗ rtyped Γ2 e2 t2
| LetPair e1 e2 =>
∃ Γ1 Γ2, ⌜⌜ env_split Γ Γ1 Γ2 ⌝⌝ ∗
∃ t1 t2,
rtyped Γ1 e1 (PairT t1 t2) ∗
rtyped Γ2 e2 (FunT Lin t1 (FunT Lin t2 t))
| Sum i e =>
∃ n (ts : fin n -> type) (i' : fin n), ⌜⌜ t = SumT n ts ⌝⌝ ∗ ⌜⌜ i = i' ⌝⌝ ∗
rtyped Γ e (ts i')
| MatchSum n e es =>
∃ Γ1 Γ2, ⌜⌜ env_split Γ Γ1 Γ2 ∧ (n = 0 -> env_unr Γ2)⌝⌝ ∗
∃ ts,
rtyped Γ1 e (SumT n ts) ∗
if decide (n=0) then ⌜⌜ env_unr Γ2 ⌝⌝ else (∀ i, rtyped Γ2 (es i) (FunT Lin (ts i) t))
| ForkBarrier e =>
∃ t1 t2, ⌜⌜ t = FunT Lin t1 t2 ⌝⌝ ∗
rtyped Γ e (FunT Lin (FunT Lin t2 t1) UnitT)
| NewLock e =>
∃ t', ⌜⌜ t = LockT (Owner,Closed) t' ⌝⌝ ∗
rtyped Γ e t'
| ForkLock e1 e2 =>
∃ Γ1 Γ2, ⌜⌜ env_split Γ Γ1 Γ2 ⌝⌝ ∗
∃ t' l1 l2 l3, ⌜⌜ t = LockT l3 t' ∧ lockcap_split l1 l2 l3 ⌝⌝ ∗
rtyped Γ1 e1 (LockT l1 t') ∗
rtyped Γ2 e2 (FunT Lin (LockT l2 t') UnitT)
| Acquire e =>
∃ lo t', ⌜⌜ t = PairT (LockT (lo,Opened) t') t' ⌝⌝ ∗
rtyped Γ e (LockT (lo,Closed) t')
| Release e1 e2 =>
∃ Γ1 Γ2, ⌜⌜ env_split Γ Γ1 Γ2 ⌝⌝ ∗
∃ lo t', ⌜⌜ t = LockT (lo,Closed) t' ⌝⌝ ∗
rtyped Γ1 e1 (LockT (lo,Opened) t') ∗
rtyped Γ2 e2 t'
| Wait e =>
rtyped Γ e (LockT (Owner,Closed) t)
| Drop e =>
∃ t', ⌜⌜ t = UnitT ⌝⌝ ∗
rtyped Γ e (LockT (Client,Closed) t')
end
with vtyped v t :=
match v with
| FunV x e =>
∃ l t1 t2, ⌜⌜ t = FunT l t1 t2 ⌝⌝ ∗ linbox l (rtyped {[ x := t1 ]} e t2)
| UnitV => ⌜⌜ t = UnitT ⌝⌝
| PairV v1 v2 =>
∃ t1 t2, ⌜⌜ t = PairT t1 t2 ⌝⌝ ∗
vtyped v1 t1 ∗ vtyped v2 t2
| SumV i v =>
∃ n ts (i' : fin n), ⌜⌜ t = SumT n ts ∧ i = i' ⌝⌝ ∗
vtyped v (ts i')
| BarrierV k =>
∃ t1 t2, ⌜⌜ t = FunT Lin t1 t2 ⌝⌝ ∗
own_out k ((BarrierLabel false t1 t2) : labelO)
| LockV k =>
∃ l t', ⌜⌜ t = LockT l t' ⌝⌝ ∗
own_out k ((LockLabel l t') : labelO)
end.
Lemma typed_rtyped Γ e t :
⌜⌜ typed Γ e t ⌝⌝ -∗ rtyped Γ e t.
Proof.
iIntros (H).
iInduction e as [] "IH" forall (t Γ H);
inv H; simpl; eauto; repeat iExists _; try iSplitL; eauto;
repeat iExists _; try iSplitL; eauto; try iSplitL;
try destruct l; try case_decide; repeat iIntros (?); subst; eauto;
try solve [ iApply ("IH" with "[%]") || iApply ("IH1" with "[%]"); eauto].
Qed.
(* From stdpp's naive_solver *)
Ltac simp :=
repeat match goal with
(**i solve the goal *)
| |- _ => fast_done
(**i intros *)
| |- ∀ _, _ => intro
(**i simplification of assumptions *)
| H : False |- _ => destruct H
| H : _ ∧ _ |- _ =>
(* Work around bug https://coq.inria.fr/bugs/show_bug.cgi?id=2901 *)
let H1 := fresh in let H2 := fresh in
destruct H as [H1 H2]; try clear H
| H : ∃ _, _ |- _ =>
let x := fresh in let Hx := fresh in
destruct H as [x Hx]; try clear H
| H : ?P → ?Q, H2 : ?P |- _ => specialize (H H2)
| H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
| H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
(**i simplify and solve equalities *)
| |- _ => progress simplify_eq/=
(**i operations that generate more subgoals *)
(* | |- _ ∧ _ => split *)
(* | |- Is_true (bool_decide _) => apply (bool_decide_pack _) *)
(* | |- Is_true (_ && _) => apply andb_True; split *)
(* | H : _ ∨ _ |- _ => *)
(* let H1 := fresh in destruct H as [H1|H1]; try clear H *)
(* | H : Is_true (_ || _) |- _ => *)
(* apply orb_True in H; let H1 := fresh in destruct H as [H1|H1]; try clear H *)
(**i solve the goal using the user supplied tactic *)
end.
Ltac iDestr H := repeat (iDestruct "H" as %? || iDestruct H as (?) H).
Ltac iSpl := repeat (iExists _ || iSplit || iIntros (?)).
Lemma unrestricted_box v t :
unr t -> vtyped v t -∗ □ vtyped v t.
Proof.
iIntros (H) "H".
iInduction v as [] "IH" forall (t H); simpl;
iDestr "H"; simp; inv H; simp; eauto.
- iDestruct "H" as "#H". iModIntro. eauto.
- iDestruct "H" as "[H1 H2]".
iDestruct ("IH" with "[%] H1") as "H1"; first done.
iDestruct ("IH1" with "[%] H2") as "H2"; first done.
iDestruct "H1" as "#H1".
iDestruct "H2" as "#H2".
iModIntro. repeat (iExists _ || iSplitL); eauto.
- iDestruct ("IH" with "[%] H") as "H"; first done.
iDestruct "H" as "#H". iModIntro. eauto.
Qed.
Definition substR (Γ : env) x v := from_option (vtyped v) emp%I (Γ !! x).
Ltac sdec := repeat case_decide; simplify_eq; simpl in *; eauto; try done.
Ltac smap := repeat (rewrite lookup_alter_spec || rewrite lookup_union || rewrite lookup_insert_spec || rewrite lookup_delete_spec || sdec).
Lemma env_unr_substR Γ x v :
env_unr Γ -> substR Γ x v ⊢ emp.
Proof.
rewrite /env_unr /substR.
destruct (Γ !! x) eqn:E; simp.
rewrite unrestricted_box; eauto.
Qed.
Lemma env_split_substR Γ Γ1 Γ2 x v :
env_split Γ Γ1 Γ2 -> substR Γ x v ⊢ substR Γ1 x v ∗ substR Γ2 x v.
Proof.
rewrite /env_split /substR. simp.
rewrite lookup_union.
destruct (Γ1 !! x) eqn:E;
destruct (Γ2 !! x) eqn:F; rewrite ?E ?F; simpl; eauto.
edestruct (H1 x); eauto. simp.
iIntros "H".
iDestruct (unrestricted_box with "H") as "H"; eauto.
iDestruct "H" as "#H". iSplitL; eauto.
Qed.
Lemma env_var_substR Γ x y v t :
env_var Γ y t ->
substR Γ x v ⊢ if decide (x = y) then vtyped v t else emp.
Proof.
rewrite /env_var /substR. simp. smap.
destruct (_!!_) eqn:E; simp.
rewrite unrestricted_box; eauto.
Qed.
Lemma env_bind_substR Γ Γ' x y v t :
env_bind Γ' y t Γ ->
substR Γ x v ⊢ if decide (x = y) then emp else substR Γ' x v.
Proof.
rewrite /env_bind /substR. simp. smap.
- destruct (Γ !! y) eqn:E; simpl; eauto.
rewrite unrestricted_box; eauto.
- destruct (Γ !! x) eqn:E; rewrite ?E; destruct l; eauto; simpl.
rewrite {1}unrestricted_box; eauto.
eapply H; eauto.
Qed.
Lemma env_unr_delete Γ x :
env_unr Γ -> env_unr (delete x Γ).
Proof.
rewrite /env_unr. intros ???. smap.
Qed.
Lemma env_split_delete Γ Γ1 Γ2 x :
env_split Γ Γ1 Γ2 -> env_split (delete x Γ) (delete x Γ1) (delete x Γ2).
Proof.
rewrite /env_split /disj. simp.
split; [apply delete_union|].
intros ???. smap.
Qed.
Lemma env_var_delete y x Γ t :
env_var Γ x t -> if decide (y = x) then env_unr (delete y Γ) else env_var (delete y Γ) x t.
Proof.
rewrite /env_var /env_unr. simp. smap.
- simp. revert H. smap.
- exists (delete y H0). split.
+ apply map_eq. intro. smap.
+ intros ??. smap.
Qed.
Lemma env_bind_delete x y t Γ Γ' :
env_bind Γ' x t Γ ->
env_bind (if decide (y = x) then Γ' else delete y Γ') x t (delete y Γ).
Proof.
rewrite /env_bind. simp.
split.
- apply map_eq. intro. smap.
- intro. smap.
Qed.
Lemma env_unr_empty :
env_unr ∅.
Proof.
rewrite /env_unr. intros ??. smap.
Qed.
Lemma env_split_empty Γ1 Γ2 :
env_split ∅ Γ1 Γ2 <-> Γ1 = ∅ ∧ Γ2 = ∅.
Proof.
rewrite /env_split.
split. simp.
- symmetry in H0.
pose proof (map_positive_l _ _ H0). subst.
rewrite left_id in H0. subst. eauto.
- simp. rewrite left_id. split; eauto.
rewrite /disj. intros ??. smap.
Qed.
Lemma env_var_empty x t :
env_var ∅ x t <-> False.
Proof.
rewrite /env_var. split; simp.
rewrite map_eq_iff in H. specialize (H x). revert H. smap.
Qed.
Lemma env_bind_empty Γ x t1 :
env_bind Γ x t1 ∅ <-> Γ = {[ x := t1 ]}.
Proof.
rewrite /env_bind. repeat split; simp.
Qed.
Lemma linbox_mono P Q l :
□ (P -∗ Q) -∗ linbox l P -∗ linbox l Q.
Proof.
iIntros "#H P".
destruct l; simpl; [|iDestruct "P" as "#P"; iModIntro];
iApply "H"; done.
Qed.
Lemma linbox_sep P Q l :
linbox l P ∗ linbox l Q ⊢ linbox l (P ∗ Q).
Proof.
destruct l; simpl; eauto.
iIntros "[#H #R]". iModIntro.
iSplitL; eauto.
Qed.
Lemma substitution Γ x v e t :
substR Γ x v ∗
rtyped Γ e t -∗
rtyped (delete x Γ) (subst x v e) t.
Proof.
iIntros "RH".
iInduction e as [] "IH" forall (Γ t); simpl;
iDestruct "RH" as "[R H]"; iDestr "H"; try iDestruct "H" as "[H Q]"; simp.
- rewrite env_unr_substR //. iSpl; eauto using env_unr_delete.
- rewrite env_var_substR //.
eapply (env_var_delete x) in H.
case_decide; subst; simpl; iFrame; iPureIntro; eauto.
- iExists _,_,_. iSplit; first done.
iExists _. iSplit; eauto 6 using env_bind_delete, env_unr_delete.
rewrite env_bind_substR; eauto.
case_decide; subst; iFrame.
iApply linbox_mono; eauto.
iApply linbox_sep. iFrame.
- iDestruct (env_split_substR with "R") as "[R1 R2]"; eauto.
iSpl; eauto using env_split_delete.
iSplitL "H R1"; (iApply "IH" || iApply "IH1"); eauto with iFrame.
- rewrite env_unr_substR //.
eauto using env_unr_delete.
- iDestruct (env_split_substR with "R") as "[R1 R2]"; eauto.
iSpl; eauto using env_split_delete.
iSplitL "H R1"; (iApply "IH" || iApply "IH1"); eauto with iFrame.
- iDestruct (env_split_substR with "R") as "[R1 R2]"; eauto.
iSpl; eauto using env_split_delete.
iSplitL "H R1"; (iApply "IH" || iApply "IH1"); eauto with iFrame.
- iSpl; eauto. iApply "IH". iFrame.
- iDestruct (env_split_substR with "R") as "[R1 R2]"; eauto.
iSpl; first iPureIntro; eauto using env_split_delete, env_unr_delete.
case_decide; subst.
{ iDestruct "Q" as "%". iSplit; eauto using env_unr_delete.
eapply env_unr_substR in H. rewrite H.
iApply "IH1". iFrame. }
iSplitL "H R1"; iSpl; (iApply "IH" || iApply "IH1"); eauto with iFrame.
- iSpl; eauto. (iApply "IH" || iApply "IH1"); eauto with iFrame.
- iSpl; eauto. iApply "IH". iFrame.
- iSpl; eauto using env_split_delete.
iDestruct (env_split_substR with "R") as "[R1 R2]"; eauto.
iSplitL "H R1"; (iApply "IH" || iApply "IH1"); iFrame.
- iSpl; eauto. iApply "IH". iFrame.
- iSpl; eauto using env_split_delete.
iDestruct (env_split_substR with "R") as "[R1 R2]"; eauto.
iSplitL "H R1"; (iApply "IH" || iApply "IH1"); iFrame.
- iSpl; eauto. iApply "IH". iFrame.
- iSpl; eauto. iApply "IH". iFrame.
Qed.
Fixpoint rtyped0 e t : rProp :=
match e with
| Val v => vtyped v t
| Var x => False
| Fun x e =>
∃ l t1 t2, ⌜⌜ t = FunT l t1 t2 ⌝⌝ ∗
∃ Γ, ⌜⌜ env_bind Γ x t1 ∅ ⌝⌝ ∗
linbox l (rtyped Γ e t2)
| App e1 e2 =>
∃ t1 l,
rtyped0 e1 (FunT l t1 t) ∗
rtyped0 e2 t1
| Unit => ⌜⌜ t = UnitT ⌝⌝
| Pair e1 e2 =>
∃ t1 t2, ⌜⌜ t = PairT t1 t2 ⌝⌝ ∗
rtyped0 e1 t1 ∗ rtyped0 e2 t2
| LetPair e1 e2 =>
∃ t1 t2,
rtyped0 e1 (PairT t1 t2) ∗
rtyped0 e2 (FunT Lin t1 (FunT Lin t2 t))
| Sum i e =>
∃ n (ts : fin n -> type) (i' : fin n), ⌜⌜ t = SumT n ts ⌝⌝ ∗ ⌜⌜ i = i' ⌝⌝ ∗
rtyped0 e (ts i')
| MatchSum n e es =>
∃ ts,
rtyped0 e (SumT n ts) ∗
if decide (n=0) then emp else (∀ i, rtyped0 (es i) (FunT Lin (ts i) t))
(* Barriers *)
| ForkBarrier e =>
∃ t1 t2, ⌜⌜ t = FunT Lin t1 t2 ⌝⌝ ∗
rtyped0 e (FunT Lin (FunT Lin t2 t1) UnitT)
(* Locks *)
| NewLock e =>
∃ t', ⌜⌜ t = LockT (Owner,Closed) t' ⌝⌝ ∗
rtyped0 e t'
| ForkLock e1 e2 =>
∃ t' l1 l2 l3, ⌜⌜ t = LockT l3 t' ∧ lockcap_split l1 l2 l3 ⌝⌝ ∗
rtyped0 e1 (LockT l1 t') ∗
rtyped0 e2 (FunT Lin (LockT l2 t') UnitT)
| Acquire e =>
∃ lo t', ⌜⌜ t = PairT (LockT (lo,Opened) t') t' ⌝⌝ ∗
rtyped0 e (LockT (lo,Closed) t')
| Release e1 e2 =>
∃ lo t', ⌜⌜ t = LockT (lo,Closed) t' ⌝⌝ ∗
rtyped0 e1 (LockT (lo,Opened) t') ∗
rtyped0 e2 t'
| Wait e =>
rtyped0 e (LockT (Owner,Closed) t)
| Drop e =>
∃ t', ⌜⌜ t = UnitT ⌝⌝ ∗
rtyped0 e (LockT (Client,Closed) t')
end.
Lemma rtyped_rtyped0 e t :
rtyped ∅ e t ⊣⊢ rtyped0 e t.
Proof.
revert t. induction e; intros; simpl;
iSplit; iIntros "H";
try setoid_rewrite env_split_empty;
try setoid_rewrite env_var_empty;
try setoid_rewrite env_bind_empty;
iDestr "H"; simp; eauto using env_unr_empty;
try iDestruct "H" as "[H Q]";
repeat (iExists _ || iSplit); eauto using env_unr_empty;
rewrite ?H ?IHe ?IHe1 ?IHe2; try case_decide; iFrame; eauto using env_unr_empty;
iIntros (?); setoid_rewrite H; eauto.
Qed.
Lemma substitution0 v t1 t2 x e :
vtyped v t1 ∗
rtyped {[ x := t1 ]} e t2 -∗
rtyped0 (subst x v e) t2.
Proof.
rewrite -rtyped_rtyped0.
iIntros "[H Q]".
iDestruct (substitution _ x v e t2 with "[H Q]") as "H"; iFrame.
- rewrite /substR lookup_singleton //.
- rewrite delete_singleton //.
Qed.
Lemma pure_preservation e e' t :
pure_step e e' ->
rtyped0 e t -∗ rtyped0 e' t.
Proof.
intros []; simpl;
iIntros "H";
try setoid_rewrite env_bind_empty;
repeat (iDestr "H" || iDestruct "H" as "[H ?]"); simp;
repeat (iExists _ || iSplit || case_decide); eauto with iFrame.
- iApply substitution0. iFrame. by destruct l0.
- subst. inv_fin i'.
Qed.
Lemma replacement1 k e B :
ctx1 k ->
rtyped0 (k e) B -∗ ∃ t, rtyped0 e t ∗ ∀ e', rtyped0 e' t -∗ rtyped0 (k e') B.
Proof.
destruct 1; simpl; iIntros "H";
iDestr "H"; try iDestruct "H" as "[H Q]";
eauto 9 with iFrame.
Qed.
Lemma replacement k e B :
ctx k ->
rtyped0 (k e) B ⊣⊢ ∃ t, rtyped0 e t ∗ ∀ e', rtyped0 e' t -∗ rtyped0 (k e') B.
Proof.
intros Hk.
iSplit; iIntros "H"; last first.
{ iDestruct "H" as (t) "[H Q]". by iApply "Q". }
iInduction Hk as [] "IH" forall (B e); simpl.
{ iExists _. iFrame. eauto. } subst.
iDestruct (replacement1 with "H") as (?) "[H R]"; eauto.
iDestruct ("IH" with "H") as (?) "[Q H]".
iExists _. iFrame. iIntros (?) "?".
iApply "R". iApply "H". done.
Qed.
Ltac solve_ctx := solve [iPureIntro; do 2 eexists; split; last done; eauto using ctx, ctx1].
Ltac solve_step := solve [iPureIntro; do 2 eexists; split; eauto using Ctx_id; simp; eauto using pure_step].
Ltac solve_pr := simp; solve [solve_ctx || solve_step].
Inductive impure : expr -> Prop :=
| imp_ForkBarrier v : impure (ForkBarrier (Val v))
| imp_NewLock v : impure (NewLock (Val v))
| imp_Waiting e i : expr_head_waiting e i -> impure e.
Definition step_or_impure e := ∃ k e0,
ctx k ∧ e = k e0 ∧ ((∃ e', pure_step e0 e') ∨ impure e0).
Lemma step_or_impure_ctx1 e e0 k :
ctx1 k -> e0 = k e -> step_or_impure e -> step_or_impure e0.
Proof.
intros Hctx -> (k' & e' & Hctx' & -> & D).
unfold step_or_impure. eexists (k ∘ k'),_.
eauto using Ctx_comp.
Qed.
Lemma pure_step_or_impure e e' :
pure_step e e' -> step_or_impure e.
Proof.
intros Hs. eexists id,_;
eauto using Ctx_id.
Qed.
Lemma impure_or_impure e :
impure e -> step_or_impure e.
Proof.
intros Hi. eexists id,_;
eauto using Ctx_id.
Qed.
Definition is_Val e := ∃ v, e = Val v.
Ltac into_val H1 H2 :=
iDestruct (H1 with H2) as %[[? ->]|?];
last by eauto using step_or_impure_ctx1, ctx1.
Ltac ppdone := simp; eauto using pure_step_or_impure, pure_step, impure_or_impure, impure, expr_head_waiting.
Lemma pure_progress e t :
rtyped0 e t -∗ ⌜ is_Val e ∨ step_or_impure e ⌝.
Proof.
iIntros "H".
iInduction e as [] "IH" forall (t); simpl; eauto;
first (iLeft; unfold is_Val; by eauto); iRight.
(* Base language *)
- ppdone.
- iDestr "H". iDestruct "H" as "[H H1]".
into_val "IH" "H".
into_val "IH1" "H1".
destruct x; simpl; iDestr "H"; ppdone.
- ppdone.
- iDestr "H". iDestruct "H" as "[H H1]".
into_val "IH" "H".
into_val "IH1" "H1".
ppdone.
- iDestr "H". iDestruct "H" as "[H H1]".
into_val "IH" "H". simpl.
destruct x; simpl; iDestr "H"; ppdone.
- iDestr "H"; simp.
into_val "IH" "H". simpl.
ppdone.
- iDestr "H". iDestruct "H" as "[H H1]".
into_val "IH1" "H". simpl.
destruct x; simpl; iDestr "H";
ppdone.
(* Barriers *)
- iDestr "H".
into_val "IH" "H". ppdone.
(* Locks *)
- iDestr "H". into_val "IH" "H". ppdone.
- iDestr "H". iDestruct "H" as "[H H1]".
into_val "IH" "H".
into_val "IH1" "H1".
destruct x; simpl; iDestr "H"; simp.
ppdone.
- iDestr "H".
into_val "IH" "H".
destruct x; simpl; iDestr "H"; simp.
ppdone.
- iDestr "H". iDestruct "H" as "[H H1]".
into_val "IH" "H".
into_val "IH1" "H1".
destruct x; simpl; iDestr "H"; simp.
ppdone.
- iDestr "H".
into_val "IH" "H".
destruct x; simpl; iDestr "H"; simp.
ppdone.
- iDestr "H".
into_val "IH" "H".
destruct x; simpl; iDestr "H"; simp.
ppdone.
Qed.