Library iris.locks.lock_reln
From iris.heap_lang Require Export lang notation.
From iris.prelude Require Import gmap stringmap mapset list.
Global Set Bullet Behavior "Strict Subproofs".
Section lock_reln.
Inductive typ :=
| Product: typ → typ → typ
| Arrow: typ → typ → typ
| Unit: typ
| Int: typ
| Bool: typ
| Sum: typ → typ → typ
| Ref: typ → typ
| Lock: typ.
Definition typ_ctx := gmap string typ.
Definition sync (acq rel: expr) : expr :=
λ: "lk" "f", acq "lk" ;; let: "z" := "f" #() in rel "lk" ;; "z".
Reserved Notation "Γ ⊩ e1 ↝ e2 : ty"
(no associativity, at level 90, e1 at next level, e2 at next level).
Context (acq1 acq2: val).
Context (rel1 rel2: val).
Context (newlock1 newlock2: val).
Definition sync1 := sync acq1 rel1.
Definition sync2 := sync acq2 rel2.
Inductive type_trans : typ_ctx → expr → expr → typ → Prop :=
| var_typ Γ x ty:
Γ !! x = Some ty →
Γ ⊩ (Var x) ↝ (Var x) : ty
| bool_typ Γ b:
Γ ⊩ (Lit (LitBool b)) ↝ (Lit (LitBool b)) : Bool
| int_typ Γ n:
Γ ⊩ (Lit (LitInt n)) ↝ (Lit (LitInt n)) : Int
| unit_typ Γ:
Γ ⊩ (Lit (LitUnit)) ↝ (Lit (LitUnit)) : Unit
| pair_intro_typ Γ e1 e1' ty1 e2 e2' ty2:
Γ ⊩ e1 ↝ e1' : ty1 →
Γ ⊩ e2 ↝ e2' : ty2 →
Γ ⊩ (Pair e1 e2) ↝ (Pair e1' e2') : (Product ty1 ty2)
| pair_elim_fst_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : (Product ty1 ty2) →
Γ ⊩ (Fst e) ↝ (Fst e') : ty1
| pair_elim_snd_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : (Product ty1 ty2) →
Γ ⊩ (Snd e) ↝ (Snd e') : ty2
| sum_intro_left_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : ty1 →
Γ ⊩ (InjL e) ↝ (InjL e') : (Sum ty1 ty2)
| sum_intro_right_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : ty2 →
Γ ⊩ (InjR e) ↝ (InjR e') : (Sum ty1 ty2)
| sum_elim_typ Γ e e' el el' er er' ty1 ty2 ty:
Γ ⊩ e ↝ e' : Sum ty1 ty2 →
Γ ⊩ el ↝ el' : Arrow ty1 ty →
Γ ⊩ er ↝ er' : Arrow ty2 ty →
Γ ⊩ (Case e el er) ↝ (Case e' el' er') : ty
| seq_typ Γ e1 e1' ty1 e2 e2' ty2:
Γ ⊩ e1 ↝ e1' : ty1 →
Γ ⊩ e2 ↝ e2' : ty2 →
Γ ⊩ (App (Lam BAnon e1) e2) ↝ (App (Lam BAnon e1') e2') : ty1
| fork_typ Γ e e' ty:
Γ ⊩ e ↝ e' : ty →
Γ ⊩ (Fork e) ↝ (Fork e') : Unit
| arrow_intro_typ Γ y x ty1 e e' ty2 :
x ≠ y →
(<[y := Arrow ty1 ty2]>(<[x := ty1]>Γ)) ⊩ e ↝ e' : ty2 →
Γ ⊩ (Rec (BNamed y) (BNamed x) e) ↝ (Rec (BNamed y) (BNamed x) e') : (Arrow ty1 ty2)
| arrow_elim_typ Γ e1 e1' ty1 ty2 e2 e2':
Γ ⊩ e1 ↝ e1' : (Arrow ty1 ty2) →
Γ ⊩ e2 ↝ e2' : ty1 →
Γ ⊩ (App e1 e2) ↝ (App e1' e2') : ty2
| ref_intro_typ Γ e e' ty:
Γ ⊩ e ↝ e' : ty →
Γ ⊩ Alloc e ↝ Alloc e' : Ref ty
| ref_store_typ Γ el el' e e' ty:
Γ ⊩ el ↝ el' : Ref ty →
Γ ⊩ e ↝ e' : ty →
Γ ⊩ Store el e ↝ Store el' e' : Unit
| ref_load_typ Γ el el' ty:
Γ ⊩ el ↝ el' : Ref ty →
Γ ⊩ Load el ↝ Load el' : ty
| lock_intro_typ Γ:
Γ ⊩ newlock1 ↝ newlock2 : Arrow Unit Lock
| lock_elim_typ Γ el el' e e' ty:
Γ ⊩ el ↝ el' : Lock →
Γ ⊩ e ↝ e' : (Arrow Unit ty) →
Γ ⊩ sync1 el e ↝ sync2 el' e' : ty
where "Γ ⊩ e1 ↝ e2 : ty" := (type_trans Γ e1 e2 ty).
Lemma typ_context_closed_1 Γ l e e' ty:
Γ ⊩ e ↝ e' : ty → (∀ x, x ∈ dom (gset string) Γ → x ∈ l) → Closed l e ∧ Closed l e'.
Proof.
intros Htyp; revert l; induction Htyp⇒l; try done;
rewrite /Closed⇒Hin; split; simplify_eq/=;
repeat (match goal with
| [ |- context [is_closed ?l1 ?e1 && is_closed ?l2 ?e2] ] ⇒
apply andb_prop_intro; split
| [ H: ∀ l : list string, ?P → Closed l ?e ∧ Closed _ _ |- context [is_closed ?l' ?e]] ⇒
eapply H; intros x'; rewrite ?dom_insert; set_unfold; naive_solver
| [ H: ∀ l : list string, ?P → Closed _ _ ∧ Closed l ?e |- context [is_closed ?l' ?e]] ⇒
eapply H; intros x'; rewrite ?dom_insert; set_unfold; naive_solver
end).
- rewrite bool_decide_spec. apply Hin, elem_of_dom; eauto.
- rewrite bool_decide_spec. apply Hin, elem_of_dom; eauto.
- apply is_closed_of_val.
- apply is_closed_of_val.
- rewrite ?andb_true_r. repeat (apply andb_prop_intro || split).
× apply is_closed_of_val.
× eapply is_closed_weaken_nil; eauto using is_closed_of_val.
× eapply IHHtyp1; eauto.
× eapply IHHtyp2; eauto.
- rewrite ?andb_true_r. repeat (apply andb_prop_intro || split).
× apply is_closed_of_val.
× eapply is_closed_weaken_nil; eauto using is_closed_of_val.
× eapply IHHtyp1; eauto.
× eapply IHHtyp2; eauto.
Qed.
Lemma typ_context_closed_2 Γ e e' ty:
Γ ⊩ e ↝ e' : ty → Closed (map_to_list Γ.*1) e ∧ Closed (map_to_list Γ.*1) e'.
Proof.
intros ?%typ_context_closed_1; eauto.
intros x. rewrite elem_of_dom. intros [ty' Heq].
rewrite elem_of_list_fmap. ∃ (x, ty'); split; auto.
by apply elem_of_map_to_list.
Qed.
Arguments type_trans _ _%E _%E _.
Hint Constructors type_trans.
Section lr.
From iris.heap_lang Require Import heap proofmode notation refine_proofmode.
From iris.proofmode Require Import invariants.
Context (dinit : nat) (Σ: gFunctors) (N: namespace).
Context (Hdisj1: N ⊥ heapN).
Context (Hdisj2: N ⊥ sheapN).
Context (Kd: nat).
Context `{!heapG Σ, !sheapG heap_lang Σ}.
Context `{!refineG heap_lang Σ (delayed_lang (heap_lang) Kd dinit) (S Kd × (Kd + 3))}.
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Local Notation exprC := (leibnizC (expr)).
Local Notation valC := (leibnizC (val)).
Context (Hle_init: dinit ≤ Kd).
Context (is_lock : gname → val → val → iProp → iProp).
Context (locked: gname → val → val → iProp).
Context (is_lock_relevant: ∀ γ lks lk R, RelevantP (is_lock γ lks lk R)).
Context (is_lock_affine: ∀ γ lks lk R, AffineP (is_lock γ lks lk R)).
Context (locked_affine: ∀ γ lks lk, AffineP (locked γ lks lk)).
Global Set Bullet Behavior "Strict Subproofs".
Definition dK K e :=
match to_val (ectx_language.fill K e) with
| None ⇒ dinit
| Some _ ⇒ O
end.
Context (newlock_spec:
∀ i K R, (heap_ctx ★ sheap_ctx
★ ownT i (newlock1 #()) K (dK K (newlock1 #())) ★ ⧆R
⊢ WP (newlock2 #()) {{ lk, ∃ lks γ, is_lock γ lks lk R ★
ownT i (of_val lks) K (dK K (of_val lks))}})%I).
Context (acquire_spec:
∀ i K R lks lk γ,
(is_lock γ lks lk R ★ ownT i (acq1 lks) K (dK K (acq1 lks))
⊢ WP (acq2 lk) {{ v, ⧆■(v = #()) ★ locked γ lks lk ★
ownT i (#())%E K (dK K #()) ★ ⧆R}})%I).
Context (release_spec:
∀ i K R lks lk γ,
(is_lock γ lks lk R ★ locked γ lks lk
★ ownT i (rel1 lks) K (dK K (rel1 lks)) ★ ⧆R
⊢ WP (rel2 lk) {{ v, ⧆■(v = #()) ★ ownT i (#())%E K (dK K #())}})%I).
Definition refN : namespace := N .@ "ref".
Definition expr_rel_lift (vrel: valC -n> valC -n> iProp) e e' : iProp :=
(∀ i K, ⧆□ (ownT i e K (dK K e)
-★ WP e' {{ v', ∃ v, ⧆ vrel v v'
★ ownT i (of_val v) K (dK K v)}}))%I.
Import uPred.
Lemma expr_rel_lift_ne n : Proper (dist n ==> (=) ==> (=) ==> dist n) expr_rel_lift.
Proof. intros ?? Hr ?? → ?? ->; rewrite /expr_rel_lift; by setoid_rewrite Hr. Qed.
Lemma expr_rel_aff_pres (vrel: valC -n> valC -n> iProp): (∀ v v', AffineP (vrel v v')) →
∀ e e', AffineP (expr_rel_lift vrel e e').
Proof. rewrite /AffineP /expr_rel_lift; intros; apply affine_intro; [apply _ | auto]. Qed.
Lemma expr_rel_rel_pres (vrel: valC -n> valC -n> iProp): (∀ v v', RelevantP (vrel v v')) →
∀ e e', RelevantP (expr_rel_lift vrel e e').
Proof. rewrite /RelevantP /expr_rel_lift; intros; apply relevant_intro; [ apply _ | auto ]. Qed.
Definition lift2 (f: valC → valC → iProp) : valC -n> valC -n> iProp :=
CofeMor(λ x, CofeMor (λ y, f x y)).
Definition lift3 (f: typC → valC → valC → iProp) : typC -n> valC -n> valC -n> iProp :=
CofeMor(λ x, CofeMor(λ y, CofeMor (λ z, f x y z))).
Fixpoint val_equiv_pre (ve: typC -n> valC -n> valC -n> iProp) (ty: typ) (v v': val)
: iProp :=
(match ty with
| Int ⇒ ∃ (n: Z), ⧆(v = #n) ★ ⧆(v' = #n)
| Bool ⇒ ∃ (b: bool), ⧆(v = #b) ★ ⧆(v' = #b)
| Unit ⇒ ⧆(v = #()) ★ ⧆(v' = #())
| Product ty1 ty2 ⇒
∃ (v1 v2 v1' v2': heap_lang.val),
⧆(v = (v1, v2)%V) ★
⧆(v' = (v1', v2')%V) ★
(val_equiv_pre ve ty1 v1 v1') ★
(val_equiv_pre ve ty2 v2 v2')
| Sum ty1 ty2 ⇒
(∃ v1 v1', ⧆(v = InjLV v1) ★ ⧆(v' = InjLV v1') ★ val_equiv_pre ve ty1 v1 v1')
∨ (∃ v2 v2', ⧆(v = InjRV v2) ★ ⧆(v' = InjRV v2') ★ val_equiv_pre ve ty2 v2 v2')
| Arrow ty1 ty2 ⇒
∀ va va', ⧆□(val_equiv_pre ve ty1 va va'
-★ expr_rel_lift (lift2 (val_equiv_pre ve ty2))
(v va) (v' va'))
| Ref ty ⇒ ∃ (l l': loc),
⧆(v = (#l)%V) ★
⧆(v' = (#l')%V) ★
inv refN (∃ v v', l ↦s v ★ l' ↦ v' ★ val_equiv_pre ve ty v v')
| Lock ⇒ ∃ γ, is_lock γ v v' Emp
end)%I.
Definition val_equiv_preC (ve: typC -n> valC -n> valC -n> iProp):
typC -n> valC -n> valC -n> iProp := lift3 (val_equiv_pre ve).
Instance val_equiv_pre_contractive : Contractive (val_equiv_preC).
Proof.
intros n ve1 ve2 Hvd ty vh vc. simpl.
revert n ve1 ve2 Hvd vh vc.
induction ty; intros; rewrite /val_equiv_pre; fold val_equiv_pre.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto;
eapply later_contractive; intros; eapply Hvd; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
repeat apply forall_ne=>?.
apply affine_ne, relevant_ne, wand_ne; first eauto.
eapply expr_rel_lift_ne; eauto.
intros ??. rewrite //=.
eapply IHty2; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
- eauto.
- apply exist_ne=>?; apply sep_ne; eauto.
- apply or_ne; repeat apply exist_ne=>?; repeat apply sep_ne; eauto.
- repeat apply exist_ne=>?.
apply sep_ne; eauto.
apply sep_ne; eauto.
apply inv_contractive; intros.
repeat apply exist_ne=>?.
repeat apply sep_ne; eauto.
eapply IHty=>??. eapply Hvd. omega.
- apply exist_ne=>?; done.
Qed.
Definition val_equiv: typC -n> valC -n> valC -n> iProp := fixpoint val_equiv_preC.
Lemma val_equiv_fix_unfold ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_preC val_equiv ty vh vc.
Proof. by rewrite /val_equiv -fixpoint_unfold. Qed.
Lemma val_equiv_fix_unfold' ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_pre val_equiv ty vh vc.
Proof. rewrite val_equiv_fix_unfold. auto. Qed.
Instance val_equiv_affine ty e e': AffineP (val_equiv ty e e').
Proof.
rewrite /AffineP val_equiv_fix_unfold'; revert e e'; induction ty⇒e e'; simpl.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply sep_affine; rewrite /AffineP; eauto.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply affine_intro; first apply _.
repeat (rewrite ?affine_forall; apply forall_mono=>?).
apply affine_mono; eauto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply or_affine; apply affine_intro;
repeat apply exist_affine=>?; repeat apply sep_affine; try apply _;
rewrite /AffineP; eauto.
- repeat apply exist_affine=>?. repeat apply sep_affine; try apply _.
- apply exist_affine=>?. apply is_lock_affine.
Qed.
Instance val_equiv_pre_affine ty eh ec: AffineP (val_equiv_pre val_equiv ty eh ec).
Proof. rewrite /AffineP. rewrite -val_equiv_fix_unfold'. apply val_equiv_affine. Qed.
Instance val_equiv_relevant ty e e': RelevantP (val_equiv ty e e').
Proof.
rewrite /RelevantP val_equiv_fix_unfold'; revert e e'; induction ty⇒e e'; simpl.
- repeat (rewrite ?relevant_exist; apply exist_mono=>?).
repeat (apply sep_relevant; first apply _).
apply sep_relevant; rewrite /RelevantP; eauto.
- repeat (rewrite ?relevant_exist; apply exist_mono=>?).
repeat (apply sep_relevant; first apply _).
apply relevant_intro; first apply _.
repeat (rewrite ?relevant_forall; apply forall_mono=>?).
apply unlimited_mono; eauto.
- apply relevant_intro; first apply _; auto.
- apply relevant_intro; first apply _; auto.
- apply relevant_intro; first apply _; auto.
- apply or_relevant; apply relevant_intro;
repeat apply exist_relevant=>?; repeat apply sep_relevant; try apply _;
rewrite /RelevantP; eauto.
- repeat apply exist_relevant=>?. repeat apply sep_relevant; try apply _.
- apply exist_relevant=>?. apply is_lock_relevant.
Qed.
Instance val_equiv_pre_relevant ty eh ec: RelevantP (val_equiv_pre val_equiv ty eh ec).
Proof. rewrite /RelevantP. rewrite -val_equiv_fix_unfold'. apply val_equiv_relevant. Qed.
Definition bool_refine (v v': val) :=
match v, v' with
| LitV (LitBool b), LitV (LitBool b') ⇒
b = b'
| _, _ ⇒ False
end.
Definition expr_equiv ty := expr_rel_lift (val_equiv ty).
Instance expr_equiv_affine ty eh ec: AffineP (expr_equiv ty eh ec).
Proof. eapply expr_rel_aff_pres=>??; apply _. Qed.
Instance expr_equiv_relevant ty eh ec: RelevantP (expr_equiv ty eh ec).
Proof. eapply expr_rel_rel_pres=>??; apply _. Qed.
Record subst_tuple :=
stuple { styp : typ ; sval : expr; tval : expr }.
Definition subst_ctx := gmap string subst_tuple.
From iris.heap_lang Require Import substitution.
Definition subst2typ (S: subst_ctx) : typ_ctx := styp <$> S.
Definition subst2s (S: subst_ctx) : subst_map := sval <$> S.
Definition subst2t (S: subst_ctx) : subst_map := tval <$> S.
Definition ctx_expr_equiv (Γ: typ_ctx) (ty: typ) (e e': expr) : Prop :=
∀ (S: subst_ctx) (Herase: subst2typ S = Γ),
ClosedSubst [] (subst2s S) →
ClosedSubst [] (subst2t S) →
heap_ctx ★ sheap_ctx ★ ([★ map] x ↦ P ∈ S, (expr_equiv (styp P) (sval P) (tval P)))
⊢ expr_equiv ty (msubst (sval <$> S) e)
(msubst (tval <$> S) e').
Instance ctx_prop_affine S:
AffineP ([★ map] x↦P ∈S, (expr_equiv (styp P) (sval P) (tval P)))%I.
Proof.
intros; apply big_sep_affine.
rewrite /AffineL. induction map_to_list as [| a ?]; simpl; eauto using nil_affine.
destruct a; simpl; apply cons_affine; eauto using expr_equiv_affine.
Qed.
Instance ctx_prop_relevant S:
RelevantP ([★ map] x↦P ∈S, (expr_equiv (styp P) (sval P) (tval P)))%I.
Proof.
intros; apply big_sep_relevant.
rewrite /RelevantL. induction map_to_list as [| a ?]; simpl; eauto using nil_relevant.
destruct a; simpl; apply cons_relevant; eauto using expr_equiv_relevant.
Qed.
Lemma val_equiv_expr ty v v':
(val_equiv_pre val_equiv ty v v' ⊢ expr_equiv ty v v')%I.
Proof.
rewrite /expr_equiv /expr_rel_lift.
iIntros "#Hve". iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists v. iFrame "Hown".
iIntros "@". by rewrite val_equiv_fix_unfold'.
Qed.
Lemma expr_equiv_empty ty e e' (pf: ctx_expr_equiv ∅ ty e e'):
heap_ctx ★ sheap_ctx ⊢ (expr_rel_lift (val_equiv ty) e e').
Proof.
rewrite /expr_equiv in pf.
specialize (pf ∅). rewrite /subst2typ fmap_empty in pf.
efeed pose proof pf as pf'; eauto; try done.
rewrite big_sepM_empty right_id in pf' ×.
intros ->; auto.
Qed.
Lemma subst2typ_inv Γ S x ty:
Γ !! x = Some ty →
subst2typ S = Γ →
∃ eh ec, S !! x = Some {| styp := ty; sval := eh; tval := ec |}.
Proof.
rewrite /subst2typ. intros Hlook <-.
move:Hlook. rewrite lookup_fmap. case_eq (S !! x).
- intros st Heq. rewrite ?Heq.
inversion 1. destruct st; eauto.
- intros Hnone. rewrite ?Hnone.
inversion 1.
Qed.
From iris.proofmode Require Import coq_tactics environments.
Lemma tac_refine_bind Δ Δ' k t e K K' P:
envs_lookup k Δ = Some (false, ownT t (fill K' e) K (dK K (fill K' e))) →
envs_simple_replace k false (Esnoc Enil k (ownT t e (comp_ectx K K') (dK (comp_ectx K K') e))) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
rewrite ownT_focus //= ?right_id. by rewrite wand_elim_r.
Qed.
Lemma tac_refine_unbind Δ Δ' k t e K K' P :
envs_lookup k Δ = Some (false, ownT t e (comp_ectx K K') (dK (comp_ectx K K') e)) →
envs_simple_replace k false (Esnoc Enil k (ownT t (fill K' e) K (dK K (fill K' e)))) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
by rewrite -ownT_fill //= ?right_id wand_elim_r.
Qed.
Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_bind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ _ _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_focus" open_constr(efoc) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
heap_lang.tactics.reshape_expr e ltac:(fun K' e' ⇒
match e' with
| efoc ⇒ idtac K';
unify e' efoc;
refine_bind K' at j
end) || fail "refine_focus: cannot find" efoc "in" e
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_unfocus" :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (comp_ectx ?K0 ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (?K0 ++ ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
refine_unbind empty_ectx K at j; simpl_subst
| _ ⇒ fail "refine_unocus: could not find ownT"
end.
Lemma newlock_sound Γ:
ctx_expr_equiv Γ (Arrow Unit Lock) (newlock1) (newlock2).
Proof.
rewrite /ctx_expr_equiv.
intros IS ???.
iIntros "(#?&#?&#?)".
rewrite ?msubst_closed.
iIntros (i' K') "@ ! Hown".
wp_value. iPvsIntro. iExists (newlock1). iFrame.
iIntros "@".
rewrite val_equiv_fix_unfold'.
iIntros (??) "@ ! (%&%)"; subst.
iIntros (i K) "@ ! Hown".
iPoseProof (newlock_spec i K Emp with "[Hown]") as "Hwp".
{ iFrame. rewrite affine_affine right_id.
iSplitL ""; auto. }
iApply wp_wand_l; iFrame "Hwp".
iIntros "@". iIntros (lk) "HRes".
iDestruct "HRes" as (lks γ) "(Hlock&Hown)".
iExists lks. iFrame.
iIntros "@". iExists γ. done.
Qed.
Lemma sync_sound Γ el el' e e' ty:
ctx_expr_equiv Γ Lock el el' →
ctx_expr_equiv Γ (Arrow Unit ty) e e' →
ctx_expr_equiv Γ ty (sync1 el e) (sync2 el' e').
Proof.
rewrite /ctx_expr_equiv.
intros IHhas_typ1 IHhas_typ2 S ???.
iIntros "(#?&#?&#?)".
iIntros (i K) "@ ! Hown".
rewrite /sync1 /sync2 /sync.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
rewrite ?msubst_closed.
wp_focus (msubst (tval <$> S) el').
refine_focus (msubst (sval <$> S) el).
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (lk) "HRes".
iDestruct "HRes" as (lks) "(Hlock&Hown)".
refine_unfocus.
refine_focus (let: "lk" := lks in _)%E.
wp_let. refine_let (dK (K ++ reverse [AppLCtx (msubst (sval <$> S) e)])
((λ: "f", acq1 lks;; let: "z" := "f" #() in rel1 lks ;; "z"))).
{ rewrite /dK. case_match; omega. }
{ rewrite /dK. case_match; omega. }
eapply tac_refine_unbind with _ "Hown" _ _ K _.
{ env_cbv. simpl comp_ectx. reflexivity. }
{ env_cbv. reflexivity. }
idtac.
wp_value. iPvsIntro.
wp_focus (msubst (tval <$> S) e').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(AppRCtx ((λ: "f", acq1 lks;;
let: "z" := "f" #() in rel1 lks ;; "z")) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (f') "HRes".
iDestruct "HRes" as (f) "(Hf&Hown)".
refine_unfocus.
wp_let. refine_let (dK K (acq1 lks ;; let: "z" := f #() in rel1 lks ;; "z")).
{ rewrite /dK. case_match; omega. }
{ rewrite /dK. case_match; omega. }
rewrite val_equiv_fix_unfold'. rewrite /val_equiv_pre.
iDestruct "Hlock" as (γ) "#Hlock".
rewrite affine_elim.
wp_focus (acq2 lk). refine_focus (acq1 lks).
iPoseProof (acquire_spec i with "[Hown]") as "Hwp".
{ iFrame. done. }
iApply wp_wand_l; iFrame "Hwp".
iIntros "@". iIntros (?) "(%&Hlocked&Hown&_)".
subst.
refine_unfocus.
wp_let. refine_let (dK K (let: "z" := f #() in rel1 lks ;; "z")).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
idtac.
wp_focus (f' #())%E.
refine_focus (f #())%E.
rewrite affine_elim.
rewrite val_equiv_fix_unfold'. rewrite /val_equiv_pre -/val_equiv_pre.
iSpecialize ("Hf" $! #()%V).
iSpecialize ("Hf" $! #()%V).
iSpecialize ("Hf" with "[]").
{ iSplitL; auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hf" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hf".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
wp_let. refine_let (dK K (rel1 lks ;; v)).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
wp_focus (rel2 lk)%E.
refine_focus (rel1 lks)%E.
iPoseProof (release_spec i with "[Hown Hlocked]") as "Hwp".
{ iFrame. iSplitL; first done. rewrite affine_affine. done. }
iApply wp_wand_l; iFrame "Hwp".
iIntros "@". iIntros (?) "(%&Hown)".
subst. refine_unfocus.
wp_seq. refine_let (dK K v).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
wp_value. iPvsIntro. iExists v. iFrame.
rewrite val_equiv_fix_unfold'. done.
Qed.
Lemma case_sound Γ ty1 ty2 e e' ty el el' er er':
ctx_expr_equiv Γ (Sum ty1 ty2) e e' →
ctx_expr_equiv Γ (Arrow ty1 ty) el el' →
ctx_expr_equiv Γ (Arrow ty2 ty) er er' →
ctx_expr_equiv Γ ty (Case e el er) (Case e' el' er').
Proof.
rewrite /ctx_expr_equiv.
intros IHhas_typ1 IHhas_typ2 IHhas_typ3 S ???.
iIntros "(#?&#?&#?)".
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(CaseCtx _ _ :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite affine_or.
iDestruct "Hv" as "[?|?]".
× iDestruct "Hv" as (v1 v1') "(%&%&Hv1)".
subst.
iApply wp_case_inl.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
iNext.
iPoseProof (refine_case_inl (dK K _) (dK K (((msubst (sval <$> S) el) v1))) with "[Hown]")
as "Hown";
[ | | | eauto | iFrame; done | ].
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
{ rewrite to_of_val; auto with fsaV. }
iPsvs "Hown".
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
iPvsIntro.
rewrite /expr_equiv /expr_rel_lift.
rewrite -/of_val.
wp_focus (msubst (tval <$> S) el')%E.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) el) _
(AppLCtx _ :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_equiv /expr_rel_lift.
rewrite (affine_elim).
iSpecialize ("Hv" $! v1 v1' with "Hv1").
iSpecialize ("Hv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hv".
iIntros "@". iIntros (vnew') "HRes".
iDestruct "HRes" as (vnew) "(Hvnew&Hown)".
iExists vnew. iFrame. rewrite /lift2 //=.
rewrite ?val_equiv_fix_unfold' //=.
× iDestruct "Hv" as (v1 v1') "(%&%&Hv1)".
subst.
iApply wp_case_inr.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
iNext.
iPoseProof (refine_case_inr (dK K _) (dK K (((msubst (sval <$> S) er) v1))) with "[Hown]")
as "Hown";
[ | | | eauto | iFrame; done | ].
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
{ rewrite to_of_val; auto with fsaV. }
iPsvs "Hown".
iPoseProof (IHhas_typ3 S with "[]") as "Hequiv"; auto.
iPvsIntro.
rewrite /expr_equiv /expr_rel_lift.
rewrite -/of_val.
wp_focus (msubst (tval <$> S) er')%E.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) er) _
(AppLCtx _ :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_equiv /expr_rel_lift.
rewrite (affine_elim).
iSpecialize ("Hv" $! v1 v1' with "Hv1").
iSpecialize ("Hv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hv".
iIntros "@". iIntros (vnew') "HRes".
iDestruct "HRes" as (vnew) "(Hvnew&Hown)".
iExists vnew. iFrame. rewrite /lift2 //=.
rewrite ?val_equiv_fix_unfold' //=.
Qed.
Lemma delete_delete_lookup x y (S: subst_ctx):
delete y (delete x S) !! x = None.
Proof.
case (decide (y = x)).
- intros →. apply lookup_delete.
- intros ?. rewrite lookup_delete_ne //; apply lookup_delete.
Qed.
Lemma closing_helper {A: Type} x y x' ty1 ty2 (f: subst_tuple → A) Γ (S: subst_ctx):
subst2typ S = Γ →
x' ∈ (map_to_list (<[y:=ty1]> (<[x:=ty2]> Γ))).*1 →
x' ∈ [y; x] ∨ x' ∈ dom stringset (delete y (delete x (f <$> S))).
Proof.
intros Hsubst2typ.
intros ((s&e'')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
{ intros. subst. left. set_solver+. }
case (decide (s = y)).
{ intros. subst. left. set_solver+. }
intros Hneqy Hneqx.
right.
apply elem_of_dom.
move: Helem.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
Qed.
Lemma lookup_delete_subst_ctx_1 (S: subst_ctx) (x: string):
delete x S !! x = None.
Proof. apply lookup_delete. Qed.
Lemma rec_sound Γ ty1 ty2 e e' (x y: string):
x ≠ y →
(<[y:=Arrow ty1 ty2]> (<[x:=ty1]> Γ) ⊩ e ↝ e' : ty2) →
ctx_expr_equiv (<[y := Arrow ty1 ty2]>(<[x := ty1]> Γ)) ty2 e e' →
ctx_expr_equiv Γ (Arrow ty1 ty2) (rec: y x := e)%E (rec: y x := e')%E.
Proof.
rewrite /ctx_expr_equiv.
intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iLob as "IH".
iIntros "@ !". iIntros (i K) "@ ! Hown".
rewrite //=.
assert (Hclod1: Closed ([y; x]) (msubst (delete y (delete x (tval <$> S))) e')).
{ rewrite //=.
eapply msubst_closing_1. eapply typ_context_closed_2; eauto.
{ do 2 apply heap_lang.substitution.ClosedSubst_delete. eauto. }
intros x'. eapply closing_helper; assumption.
}
assert (Hclod2: Closed ([y; x]) (msubst (delete y (delete x (sval <$> S))) e)).
{ rewrite //=.
eapply msubst_closing_1. eapply (typ_context_closed_2 _ e e'); eauto.
{ do 2 apply heap_lang.substitution.ClosedSubst_delete. eauto. }
intros x'. eapply closing_helper; assumption.
}
assert (Hclo1: Closed [] (rec: y x := (msubst (delete y (delete x (tval <$> S))) e'))).
{ rewrite /Closed //=. }
assert (Hclo2: Closed [] (rec: y x := (msubst (delete y (delete x (sval <$> S))) e))).
{ rewrite /Closed //=. }
iApply wp_value; eauto.
{ rewrite //=. case_decide; eauto.
- repeat f_equal. apply proof_irrel.
- exfalso; eauto.
}
iExists (rec: y x := (msubst (delete y (delete x (sval <$> S))) e))%V.
iFrame.
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iIntros (vh vc). iIntros "@ ! #Hpre".
rewrite {2}/expr_equiv {2}/expr_rel_lift.
iIntros (i' K') "@ ! Hown".
wp_rec.
pose (S' :=
(<[y := {| styp := Arrow ty1 ty2;
sval := (rec: y x := msubst (delete y (delete x (sval <$> S))) e);
tval := (rec: y x := msubst (delete y (delete x (tval <$> S))) e')|}]>
(<[x := {| styp := ty1;
sval := of_val vh;
tval := of_val vc |}]>(delete y (delete x S))))).
iDestruct "HS" as "(#?&#?&#HS')".
refine_rec (dK K' (msubst (sval <$> S') e)).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
specialize (H1 S').
iPoseProof (H1 with "[]") as "Hequiv".
{ rewrite /S'. rewrite /subst2typ. rewrite ?fmap_insert //=.
rewrite ?fmap_delete ?insert_delete.
rewrite -delete_insert_ne; last congruence.
rewrite ?insert_delete.
rewrite /subst2typ in Herase. subst. auto.
}
{ rewrite /S' /subst2s ?fmap_insert //=.
apply ClosedSubst_insert; auto.
apply ClosedSubst_insert; auto.
rewrite ?fmap_delete.
apply ClosedSubst_delete; auto.
apply ClosedSubst_delete; auto.
solve_closed.
}
{ rewrite /S' /subst2t ?fmap_insert //=.
apply ClosedSubst_insert; auto.
apply ClosedSubst_insert; auto.
rewrite ?fmap_delete.
apply ClosedSubst_delete; auto.
apply ClosedSubst_delete; auto.
solve_closed.
}
iSplitL ""; first done.
iSplitL ""; first done.
idtac.
rewrite /S'. rewrite big_sepM_insert //=.
iSplitL.
{ rewrite affine_elim. rewrite /expr_equiv. done. }
rewrite /S'. rewrite big_sepM_insert //=.
iSplitL.
- by iApply val_equiv_expr.
- case (decide (is_Some (S !! x))).
× intros (P&Heq). rewrite big_sepM_delete; last eapply Heq.
case (decide (is_Some ((delete x S) !! y))).
idtac.
** intros (P'&Heq'). rewrite big_sepM_delete; last eapply Heq'.
iDestruct "HS'" as "(?&?&?)".
iFrame; eauto.
** intros Hnone. assert (delete x S = delete y (delete x S)) as Heq'.
{ rewrite {1}(delete_notin (delete x S) y); eauto. apply eq_None_not_Some; eauto. }
rewrite -Heq'.
iDestruct "HS'" as "(?&?)".
iFrame; eauto.
× intros Hnone. assert (S = delete x S) as Heq.
{ rewrite {1}(delete_notin S x); eauto. apply eq_None_not_Some; eauto. }
rewrite -?Heq.
case (decide (is_Some (S !! y))).
** intros (P'&Heq'). rewrite big_sepM_delete; last eapply Heq'.
iDestruct "HS'" as "(?&?)".
iFrame; eauto.
** intros Hnone'. assert (S = delete y S) as Heq'.
{ rewrite {1}(delete_notin S y); eauto. apply eq_None_not_Some; eauto. }
rewrite -?Heq'.
done.
- apply delete_delete_lookup.
- rewrite -delete_insert_ne //. apply lookup_delete_subst_ctx_1.
- assert (sval <$> S' = <[x := of_val vh]>
(<[y := (rec: y x := (msubst (delete y (delete x (sval <$>S))) e))%E]>
(delete y (delete x (sval <$> S))))) as HsS'.
{ rewrite /S'. rewrite ?fmap_insert ?fmap_delete //=. rewrite insert_commute //. }
assert (tval <$> S' = <[x := of_val vc]>
(<[y := (rec: y x := (msubst (delete y (delete x (tval <$>S))) e'))%E]>
(delete y (delete x (tval <$> S))))) as HtS'.
{ rewrite /S'. rewrite ?fmap_insert ?fmap_delete //=. rewrite insert_commute //. }
rewrite HsS' HtS'.
rewrite msubst_insert_1; last 2 first.
{ apply ClosedSubst_insert; auto. do 2 apply ClosedSubst_delete; auto. }
{ rewrite lookup_insert_ne // lookup_delete_ne //. apply lookup_delete. }
rewrite msubst_insert_1; last 2 first.
{ do 2 apply ClosedSubst_delete; auto. }
{ apply lookup_delete. }
rewrite msubst_insert_1; last 2 first.
{ apply ClosedSubst_insert; auto. do 2 apply ClosedSubst_delete; auto. }
{ rewrite lookup_insert_ne // lookup_delete_ne //. apply lookup_delete. }
rewrite msubst_insert_1; last 2 first.
{ do 2 apply ClosedSubst_delete; auto. }
{ apply lookup_delete. }
iSpecialize ("Hequiv" $! i' K' with "Hown").
iApply wp_wand_l. iFrame "Hequiv".
iIntros "@". iIntros (v) "Hpre'".
iDestruct "Hpre'" as (v') "Hpre'".
iExists v'. rewrite val_equiv_fix_unfold'.
done.
Qed.
Lemma fill_item_val_2 Ki e1 e2 :
is_Some (to_val e1) → is_Some (to_val e2) →
is_Some (to_val (fill_item Ki e1)) →
is_Some (to_val (fill_item Ki e2)).
Proof.
revert e1 e2. induction Ki; simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
Qed.
Lemma fill_val_dK K e1 e2:
is_Some (to_val e1) →
is_Some (to_val e2) →
dK K e1 = dK K e2.
Proof.
intros. rewrite /dK.
rewrite /ectx_language.fill //=.
do 2 case_match; auto.
- exfalso.
specialize (@ectxi_language.fill_val_2 heap_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (fill_item_val_2) K e1 e2);
eauto.
congruence.
- exfalso.
specialize (@ectxi_language.fill_val_2 heap_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (fill_item_val_2) K e2 e1);
eauto.
congruence.
Qed.
Lemma fundamental Γ ty e e':
Γ ⊩ e ↝ e' : ty →
ctx_expr_equiv Γ ty e e'.
Proof.
rewrite /ctx_expr_equiv.
intros has_typ.
induction has_typ .
- intros S Herase HcloSh HcloSc.
rewrite ?msubst_unfold //.
eapply subst2typ_inv in Herase as (e&e'&Hlook); eauto.
rewrite big_sepM_delete; eauto.
rewrite ?lookup_fmap ?Hlook //=.
iIntros "(?&?&?&_)". done.
- intros; iIntros "_". simpl.
rewrite ?msubst_msubst' // /expr_equiv /expr_rel_lift.
iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists #b.
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists b. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite ?msubst_msubst' // /expr_equiv /expr_rel_lift.
iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists #n.
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists n. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite ?msubst_msubst' // /expr_equiv /expr_rel_lift.
iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists #().
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e1) _
(PairLCtx (msubst (sval <$> S) e2) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e1')%E.
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv1"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv1" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv1".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e2) _
(PairRCtx v1 :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e2')%E.
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv2"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv2" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv2".
iIntros "@". iIntros (v2') "HRes".
iDestruct "HRes" as (v2) "(Hv2&Hown)".
refine_unfocus.
wp_value. iPvsIntro. iExists (v1, v2)%V.
iFrame "Hown". iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
iIntros "@". iExists v1, v2, v1', v2'.
do 2 (iSplitL ""; auto).
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(FstCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
iDestruct "Hv" as (v1 v2 v1' v2') "(%&%&Hv1&Hv2)".
subst.
wp_value; iPvsIntro.
iApply wp_fst.
rewrite to_of_val; auto with fsaV.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
iNext. refine_proj (dK K v1).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iExists v1. iFrame. iIntros "@".
rewrite ?val_equiv_fix_unfold' //=.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(SndCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
iDestruct "Hv" as (v1 v2 v1' v2') "(%&%&Hv1&Hv2)".
subst.
wp_value; iPvsIntro.
iApply wp_snd.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
rewrite to_of_val; auto with fsaV.
iNext. refine_proj (dK K v2).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iExists v2. iFrame. iIntros "@".
rewrite ?val_equiv_fix_unfold' //=.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(InjLCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
wp_value; iPvsIntro.
iExists (InjLV v).
rewrite ?val_equiv_fix_unfold' //=.
iFrame. iIntros "@". iLeft.
iExists v, v'.
iSplitL ""; auto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(InjRCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
wp_value; iPvsIntro.
iExists (InjRV v).
rewrite ?val_equiv_fix_unfold' //=.
iFrame. iIntros "@". iRight.
iExists v, v'.
iSplitL ""; auto.
- intros. eapply case_sound; rewrite /ctx_expr_equiv.
× eapply IHhas_typ1.
× eapply IHhas_typ2.
× eapply IHhas_typ3.
× eauto.
× eauto.
× eauto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
rewrite //=.
assert (Closed (≠ :b: ≠ :b: []) (msubst (tval <$> S) e1')).
{ rewrite //=.
eapply msubst_closing_1. eapply typ_context_closed_2; eauto.
assumption.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (Closed (≠ :b: ≠ :b: []) (msubst (sval <$> S) e1)).
{ rewrite //=.
eapply msubst_closing_1. eapply (typ_context_closed_2 _ e1 e1'); eauto.
assumption.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e2) _
(AppRCtx (λ:≠, (msubst (sval <$> S) e1)%V) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e2').
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&#HS')".
wp_seq. refine_seq (dK K (msubst (sval <$> S) e1)).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (vres') "HRes".
iDestruct "HRes" as (vres) "(Hvres&Hown)".
iExists vres. iFrame. done.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_apply wp_fork.
iDestruct "HS" as "(#?&#?&#?)".
refine_fork (dK K #()%E) i' as "Hown'".
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iSplitL "Hown".
{ iExists #(). iFrame. rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
}
idtac.
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i' [] with "[Hown']").
{ rewrite /fresh_delay /dK //=. }
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc) "(?&?)".
rewrite /dK //= to_of_val.
refine_stopped.
- intros. eapply rec_sound; rewrite /ctx_expr_equiv.
× eauto.
× eauto.
× eapply IHhas_typ.
× eauto.
× eauto.
× eauto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) e1').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e1) _
(AppLCtx (msubst (sval <$> S) e2) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
wp_focus (msubst (tval <$> S) e2').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e2) _
(AppRCtx v1 :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v2') "HRes".
iDestruct "HRes" as (v2) "(Hv2&Hown)".
refine_unfocus.
rewrite val_equiv_fix_unfold' //.
rewrite val_equiv_fix_unfold' //.
rewrite (affine_elim).
rewrite (affine_elim).
iSpecialize ("Hv1" $! v2 v2' with "Hv2").
iSpecialize ("Hv1" $! i _ with "Hown").
idtac.
iApply wp_wand_l. iFrame "Hv1".
iIntros "@". iIntros (vres') "HRes".
iDestruct "HRes" as (vres) "(HRes&Hown)".
iExists vres. iFrame.
idtac. rewrite val_equiv_fix_unfold'.
rewrite //=.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) e').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(AllocCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&HS')".
wp_alloc l' as "Hl'".
rewrite -psvs_pvs'.
refine_alloc (dK K (#l')%V) l as "Hl".
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
assert (dK K (#l)%V = dK K (#l')) as HdK.
{ rewrite /dK. rewrite /to_of_val.
eapply fill_val_dK; eauto. }
iExists (#l)%V.
iSplitL "Hl' Hv1 Hl".
iPvs (inv_alloc refN _ (∃ v v', l ↦s v ★ l' ↦ v' ★ val_equiv_pre val_equiv ty v v')%I
with "[Hl' Hv1 Hl]") as "Hinv".
{ rewrite /refN. eauto with ndisj. }
{ iIntros "@ >". iExists v1, v1'. iFrame. rewrite val_equiv_fix_unfold'.
rewrite affine_elim. done. }
iPvsIntro. iIntros "@". rewrite val_equiv_fix_unfold'. iExists l, l'.
iSplitL ""; first auto.
iSplitL ""; first auto.
done.
iPvsIntro. rewrite HdK. done.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) el').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) el) _
(StoreLCtx (msubst (sval <$> S) e) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
wp_focus (msubst (tval <$> S) e')%E.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(StoreRCtx v1 :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v2') "HRes".
iDestruct "HRes" as (v2) "(Hv2&Hown)".
refine_unfocus.
rewrite val_equiv_fix_unfold'.
iDestruct "Hv1" as (l1 l1') "(%&%&Hv1)".
rewrite -/val_equiv_pre.
iInv "Hv1" as "Hinv"; auto with fsaV.
iDestruct "Hinv" as (v v') "(Hl1&Hl2&Hvequiv)".
iTimeless "Hl1". iTimeless "Hl2".
rewrite (affine_elim).
rewrite (affine_elim).
rewrite (affine_elim).
subst.
iDestruct "HS" as "(#?&#?&#?)".
assert (refN ⊥ heapN) as Hdisj1' by (rewrite /refN; eauto with ndisj).
assert (refN ⊥ sheapN) as Hdisj2' by (rewrite /refN; eauto with ndisj).
wp_store. refine_store (dK K #()).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iSplitL "Hl1 Hl2 Hv2".
{ iIntros "@ >". iExists v2, v2'. iFrame.
rewrite val_equiv_fix_unfold'. done. }
iExists #(). iFrame.
rewrite val_equiv_fix_unfold'. rewrite //=.
iIntros "@". iSplitL ""; auto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) el').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) el) _
(LoadCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
rewrite val_equiv_fix_unfold'.
iDestruct "Hv1" as (l1 l1') "(%&%&Hv1)".
rewrite -/val_equiv_pre.
iInv "Hv1" as "Hinv"; auto with fsaV.
iDestruct "Hinv" as (v v') "(Hl1&Hl2&Hvequiv)".
iTimeless "Hl1". iTimeless "Hl2".
rewrite (affine_elim).
rewrite (affine_elim).
rewrite (affine_elim).
subst.
iDestruct "HS" as "(#?&#?&#?)".
assert (refN ⊥ heapN) as Hdisj1' by (rewrite /refN; eauto with ndisj).
assert (refN ⊥ sheapN) as Hdisj2' by (rewrite /refN; eauto with ndisj).
wp_load. refine_load (dK K #()).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
assert (dK K (#())%V = dK K v) as HdK.
{ rewrite /dK. rewrite /to_of_val. eapply fill_val_dK; eauto.
rewrite to_of_val. eauto. }
rewrite HdK.
iDestruct "Hvequiv" as "#Hvequiv".
iSplitL "Hl1 Hl2".
{ iIntros "@ >". iExists v, v'. iFrame. done. }
iExists v. rewrite val_equiv_fix_unfold'. iFrame.
iIntros "@". done.
- intros. eapply newlock_sound; eauto.
- intros. eapply sync_sound; eauto.
Qed.
Lemma heap_prim_dec: ∀ (e: expr) σ,
{ t | prim_step (e: expr) σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}.
Proof.
intros. edestruct (ClassicalEpsilon.excluded_middle_informative
((∃ (e' : language.expr (ectx_lang (heap_lang.expr)))
(σ' : language.state (ectx_lang (heap_lang.expr)))
(ef' : option (language.expr (ectx_lang (heap_lang.expr)))),
language.prim_step e σ e' σ' ef'))).
× apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (e'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (σ'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (ef'&e0).
left. ∃ (e', σ', ef'). eauto.
× right. auto.
Qed.
End lr.
End lock_reln.
From iris.prelude Require Import gmap stringmap mapset list.
Global Set Bullet Behavior "Strict Subproofs".
Section lock_reln.
Inductive typ :=
| Product: typ → typ → typ
| Arrow: typ → typ → typ
| Unit: typ
| Int: typ
| Bool: typ
| Sum: typ → typ → typ
| Ref: typ → typ
| Lock: typ.
Definition typ_ctx := gmap string typ.
Definition sync (acq rel: expr) : expr :=
λ: "lk" "f", acq "lk" ;; let: "z" := "f" #() in rel "lk" ;; "z".
Reserved Notation "Γ ⊩ e1 ↝ e2 : ty"
(no associativity, at level 90, e1 at next level, e2 at next level).
Context (acq1 acq2: val).
Context (rel1 rel2: val).
Context (newlock1 newlock2: val).
Definition sync1 := sync acq1 rel1.
Definition sync2 := sync acq2 rel2.
Inductive type_trans : typ_ctx → expr → expr → typ → Prop :=
| var_typ Γ x ty:
Γ !! x = Some ty →
Γ ⊩ (Var x) ↝ (Var x) : ty
| bool_typ Γ b:
Γ ⊩ (Lit (LitBool b)) ↝ (Lit (LitBool b)) : Bool
| int_typ Γ n:
Γ ⊩ (Lit (LitInt n)) ↝ (Lit (LitInt n)) : Int
| unit_typ Γ:
Γ ⊩ (Lit (LitUnit)) ↝ (Lit (LitUnit)) : Unit
| pair_intro_typ Γ e1 e1' ty1 e2 e2' ty2:
Γ ⊩ e1 ↝ e1' : ty1 →
Γ ⊩ e2 ↝ e2' : ty2 →
Γ ⊩ (Pair e1 e2) ↝ (Pair e1' e2') : (Product ty1 ty2)
| pair_elim_fst_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : (Product ty1 ty2) →
Γ ⊩ (Fst e) ↝ (Fst e') : ty1
| pair_elim_snd_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : (Product ty1 ty2) →
Γ ⊩ (Snd e) ↝ (Snd e') : ty2
| sum_intro_left_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : ty1 →
Γ ⊩ (InjL e) ↝ (InjL e') : (Sum ty1 ty2)
| sum_intro_right_typ Γ e e' ty1 ty2:
Γ ⊩ e ↝ e' : ty2 →
Γ ⊩ (InjR e) ↝ (InjR e') : (Sum ty1 ty2)
| sum_elim_typ Γ e e' el el' er er' ty1 ty2 ty:
Γ ⊩ e ↝ e' : Sum ty1 ty2 →
Γ ⊩ el ↝ el' : Arrow ty1 ty →
Γ ⊩ er ↝ er' : Arrow ty2 ty →
Γ ⊩ (Case e el er) ↝ (Case e' el' er') : ty
| seq_typ Γ e1 e1' ty1 e2 e2' ty2:
Γ ⊩ e1 ↝ e1' : ty1 →
Γ ⊩ e2 ↝ e2' : ty2 →
Γ ⊩ (App (Lam BAnon e1) e2) ↝ (App (Lam BAnon e1') e2') : ty1
| fork_typ Γ e e' ty:
Γ ⊩ e ↝ e' : ty →
Γ ⊩ (Fork e) ↝ (Fork e') : Unit
| arrow_intro_typ Γ y x ty1 e e' ty2 :
x ≠ y →
(<[y := Arrow ty1 ty2]>(<[x := ty1]>Γ)) ⊩ e ↝ e' : ty2 →
Γ ⊩ (Rec (BNamed y) (BNamed x) e) ↝ (Rec (BNamed y) (BNamed x) e') : (Arrow ty1 ty2)
| arrow_elim_typ Γ e1 e1' ty1 ty2 e2 e2':
Γ ⊩ e1 ↝ e1' : (Arrow ty1 ty2) →
Γ ⊩ e2 ↝ e2' : ty1 →
Γ ⊩ (App e1 e2) ↝ (App e1' e2') : ty2
| ref_intro_typ Γ e e' ty:
Γ ⊩ e ↝ e' : ty →
Γ ⊩ Alloc e ↝ Alloc e' : Ref ty
| ref_store_typ Γ el el' e e' ty:
Γ ⊩ el ↝ el' : Ref ty →
Γ ⊩ e ↝ e' : ty →
Γ ⊩ Store el e ↝ Store el' e' : Unit
| ref_load_typ Γ el el' ty:
Γ ⊩ el ↝ el' : Ref ty →
Γ ⊩ Load el ↝ Load el' : ty
| lock_intro_typ Γ:
Γ ⊩ newlock1 ↝ newlock2 : Arrow Unit Lock
| lock_elim_typ Γ el el' e e' ty:
Γ ⊩ el ↝ el' : Lock →
Γ ⊩ e ↝ e' : (Arrow Unit ty) →
Γ ⊩ sync1 el e ↝ sync2 el' e' : ty
where "Γ ⊩ e1 ↝ e2 : ty" := (type_trans Γ e1 e2 ty).
Lemma typ_context_closed_1 Γ l e e' ty:
Γ ⊩ e ↝ e' : ty → (∀ x, x ∈ dom (gset string) Γ → x ∈ l) → Closed l e ∧ Closed l e'.
Proof.
intros Htyp; revert l; induction Htyp⇒l; try done;
rewrite /Closed⇒Hin; split; simplify_eq/=;
repeat (match goal with
| [ |- context [is_closed ?l1 ?e1 && is_closed ?l2 ?e2] ] ⇒
apply andb_prop_intro; split
| [ H: ∀ l : list string, ?P → Closed l ?e ∧ Closed _ _ |- context [is_closed ?l' ?e]] ⇒
eapply H; intros x'; rewrite ?dom_insert; set_unfold; naive_solver
| [ H: ∀ l : list string, ?P → Closed _ _ ∧ Closed l ?e |- context [is_closed ?l' ?e]] ⇒
eapply H; intros x'; rewrite ?dom_insert; set_unfold; naive_solver
end).
- rewrite bool_decide_spec. apply Hin, elem_of_dom; eauto.
- rewrite bool_decide_spec. apply Hin, elem_of_dom; eauto.
- apply is_closed_of_val.
- apply is_closed_of_val.
- rewrite ?andb_true_r. repeat (apply andb_prop_intro || split).
× apply is_closed_of_val.
× eapply is_closed_weaken_nil; eauto using is_closed_of_val.
× eapply IHHtyp1; eauto.
× eapply IHHtyp2; eauto.
- rewrite ?andb_true_r. repeat (apply andb_prop_intro || split).
× apply is_closed_of_val.
× eapply is_closed_weaken_nil; eauto using is_closed_of_val.
× eapply IHHtyp1; eauto.
× eapply IHHtyp2; eauto.
Qed.
Lemma typ_context_closed_2 Γ e e' ty:
Γ ⊩ e ↝ e' : ty → Closed (map_to_list Γ.*1) e ∧ Closed (map_to_list Γ.*1) e'.
Proof.
intros ?%typ_context_closed_1; eauto.
intros x. rewrite elem_of_dom. intros [ty' Heq].
rewrite elem_of_list_fmap. ∃ (x, ty'); split; auto.
by apply elem_of_map_to_list.
Qed.
Arguments type_trans _ _%E _%E _.
Hint Constructors type_trans.
Section lr.
From iris.heap_lang Require Import heap proofmode notation refine_proofmode.
From iris.proofmode Require Import invariants.
Context (dinit : nat) (Σ: gFunctors) (N: namespace).
Context (Hdisj1: N ⊥ heapN).
Context (Hdisj2: N ⊥ sheapN).
Context (Kd: nat).
Context `{!heapG Σ, !sheapG heap_lang Σ}.
Context `{!refineG heap_lang Σ (delayed_lang (heap_lang) Kd dinit) (S Kd × (Kd + 3))}.
Local Notation iProp := (iPropG heap_lang Σ).
Local Notation typC := (leibnizC (typ)).
Local Notation exprC := (leibnizC (expr)).
Local Notation valC := (leibnizC (val)).
Context (Hle_init: dinit ≤ Kd).
Context (is_lock : gname → val → val → iProp → iProp).
Context (locked: gname → val → val → iProp).
Context (is_lock_relevant: ∀ γ lks lk R, RelevantP (is_lock γ lks lk R)).
Context (is_lock_affine: ∀ γ lks lk R, AffineP (is_lock γ lks lk R)).
Context (locked_affine: ∀ γ lks lk, AffineP (locked γ lks lk)).
Global Set Bullet Behavior "Strict Subproofs".
Definition dK K e :=
match to_val (ectx_language.fill K e) with
| None ⇒ dinit
| Some _ ⇒ O
end.
Context (newlock_spec:
∀ i K R, (heap_ctx ★ sheap_ctx
★ ownT i (newlock1 #()) K (dK K (newlock1 #())) ★ ⧆R
⊢ WP (newlock2 #()) {{ lk, ∃ lks γ, is_lock γ lks lk R ★
ownT i (of_val lks) K (dK K (of_val lks))}})%I).
Context (acquire_spec:
∀ i K R lks lk γ,
(is_lock γ lks lk R ★ ownT i (acq1 lks) K (dK K (acq1 lks))
⊢ WP (acq2 lk) {{ v, ⧆■(v = #()) ★ locked γ lks lk ★
ownT i (#())%E K (dK K #()) ★ ⧆R}})%I).
Context (release_spec:
∀ i K R lks lk γ,
(is_lock γ lks lk R ★ locked γ lks lk
★ ownT i (rel1 lks) K (dK K (rel1 lks)) ★ ⧆R
⊢ WP (rel2 lk) {{ v, ⧆■(v = #()) ★ ownT i (#())%E K (dK K #())}})%I).
Definition refN : namespace := N .@ "ref".
Definition expr_rel_lift (vrel: valC -n> valC -n> iProp) e e' : iProp :=
(∀ i K, ⧆□ (ownT i e K (dK K e)
-★ WP e' {{ v', ∃ v, ⧆ vrel v v'
★ ownT i (of_val v) K (dK K v)}}))%I.
Import uPred.
Lemma expr_rel_lift_ne n : Proper (dist n ==> (=) ==> (=) ==> dist n) expr_rel_lift.
Proof. intros ?? Hr ?? → ?? ->; rewrite /expr_rel_lift; by setoid_rewrite Hr. Qed.
Lemma expr_rel_aff_pres (vrel: valC -n> valC -n> iProp): (∀ v v', AffineP (vrel v v')) →
∀ e e', AffineP (expr_rel_lift vrel e e').
Proof. rewrite /AffineP /expr_rel_lift; intros; apply affine_intro; [apply _ | auto]. Qed.
Lemma expr_rel_rel_pres (vrel: valC -n> valC -n> iProp): (∀ v v', RelevantP (vrel v v')) →
∀ e e', RelevantP (expr_rel_lift vrel e e').
Proof. rewrite /RelevantP /expr_rel_lift; intros; apply relevant_intro; [ apply _ | auto ]. Qed.
Definition lift2 (f: valC → valC → iProp) : valC -n> valC -n> iProp :=
CofeMor(λ x, CofeMor (λ y, f x y)).
Definition lift3 (f: typC → valC → valC → iProp) : typC -n> valC -n> valC -n> iProp :=
CofeMor(λ x, CofeMor(λ y, CofeMor (λ z, f x y z))).
Fixpoint val_equiv_pre (ve: typC -n> valC -n> valC -n> iProp) (ty: typ) (v v': val)
: iProp :=
(match ty with
| Int ⇒ ∃ (n: Z), ⧆(v = #n) ★ ⧆(v' = #n)
| Bool ⇒ ∃ (b: bool), ⧆(v = #b) ★ ⧆(v' = #b)
| Unit ⇒ ⧆(v = #()) ★ ⧆(v' = #())
| Product ty1 ty2 ⇒
∃ (v1 v2 v1' v2': heap_lang.val),
⧆(v = (v1, v2)%V) ★
⧆(v' = (v1', v2')%V) ★
(val_equiv_pre ve ty1 v1 v1') ★
(val_equiv_pre ve ty2 v2 v2')
| Sum ty1 ty2 ⇒
(∃ v1 v1', ⧆(v = InjLV v1) ★ ⧆(v' = InjLV v1') ★ val_equiv_pre ve ty1 v1 v1')
∨ (∃ v2 v2', ⧆(v = InjRV v2) ★ ⧆(v' = InjRV v2') ★ val_equiv_pre ve ty2 v2 v2')
| Arrow ty1 ty2 ⇒
∀ va va', ⧆□(val_equiv_pre ve ty1 va va'
-★ expr_rel_lift (lift2 (val_equiv_pre ve ty2))
(v va) (v' va'))
| Ref ty ⇒ ∃ (l l': loc),
⧆(v = (#l)%V) ★
⧆(v' = (#l')%V) ★
inv refN (∃ v v', l ↦s v ★ l' ↦ v' ★ val_equiv_pre ve ty v v')
| Lock ⇒ ∃ γ, is_lock γ v v' Emp
end)%I.
Definition val_equiv_preC (ve: typC -n> valC -n> valC -n> iProp):
typC -n> valC -n> valC -n> iProp := lift3 (val_equiv_pre ve).
Instance val_equiv_pre_contractive : Contractive (val_equiv_preC).
Proof.
intros n ve1 ve2 Hvd ty vh vc. simpl.
revert n ve1 ve2 Hvd vh vc.
induction ty; intros; rewrite /val_equiv_pre; fold val_equiv_pre.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto;
eapply later_contractive; intros; eapply Hvd; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
repeat apply forall_ne=>?.
apply affine_ne, relevant_ne, wand_ne; first eauto.
eapply expr_rel_lift_ne; eauto.
intros ??. rewrite //=.
eapply IHty2; eauto.
- repeat apply exist_ne=>?.
repeat apply sep_ne; auto.
- eauto.
- apply exist_ne=>?; apply sep_ne; eauto.
- apply or_ne; repeat apply exist_ne=>?; repeat apply sep_ne; eauto.
- repeat apply exist_ne=>?.
apply sep_ne; eauto.
apply sep_ne; eauto.
apply inv_contractive; intros.
repeat apply exist_ne=>?.
repeat apply sep_ne; eauto.
eapply IHty=>??. eapply Hvd. omega.
- apply exist_ne=>?; done.
Qed.
Definition val_equiv: typC -n> valC -n> valC -n> iProp := fixpoint val_equiv_preC.
Lemma val_equiv_fix_unfold ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_preC val_equiv ty vh vc.
Proof. by rewrite /val_equiv -fixpoint_unfold. Qed.
Lemma val_equiv_fix_unfold' ty vh vc : val_equiv ty vh vc ⊣⊢ val_equiv_pre val_equiv ty vh vc.
Proof. rewrite val_equiv_fix_unfold. auto. Qed.
Instance val_equiv_affine ty e e': AffineP (val_equiv ty e e').
Proof.
rewrite /AffineP val_equiv_fix_unfold'; revert e e'; induction ty⇒e e'; simpl.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply sep_affine; rewrite /AffineP; eauto.
- repeat (rewrite ?affine_exist; apply exist_mono=>?).
repeat (apply sep_affine; first apply _).
apply affine_intro; first apply _.
repeat (rewrite ?affine_forall; apply forall_mono=>?).
apply affine_mono; eauto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply affine_intro; first apply _; auto.
- apply or_affine; apply affine_intro;
repeat apply exist_affine=>?; repeat apply sep_affine; try apply _;
rewrite /AffineP; eauto.
- repeat apply exist_affine=>?. repeat apply sep_affine; try apply _.
- apply exist_affine=>?. apply is_lock_affine.
Qed.
Instance val_equiv_pre_affine ty eh ec: AffineP (val_equiv_pre val_equiv ty eh ec).
Proof. rewrite /AffineP. rewrite -val_equiv_fix_unfold'. apply val_equiv_affine. Qed.
Instance val_equiv_relevant ty e e': RelevantP (val_equiv ty e e').
Proof.
rewrite /RelevantP val_equiv_fix_unfold'; revert e e'; induction ty⇒e e'; simpl.
- repeat (rewrite ?relevant_exist; apply exist_mono=>?).
repeat (apply sep_relevant; first apply _).
apply sep_relevant; rewrite /RelevantP; eauto.
- repeat (rewrite ?relevant_exist; apply exist_mono=>?).
repeat (apply sep_relevant; first apply _).
apply relevant_intro; first apply _.
repeat (rewrite ?relevant_forall; apply forall_mono=>?).
apply unlimited_mono; eauto.
- apply relevant_intro; first apply _; auto.
- apply relevant_intro; first apply _; auto.
- apply relevant_intro; first apply _; auto.
- apply or_relevant; apply relevant_intro;
repeat apply exist_relevant=>?; repeat apply sep_relevant; try apply _;
rewrite /RelevantP; eauto.
- repeat apply exist_relevant=>?. repeat apply sep_relevant; try apply _.
- apply exist_relevant=>?. apply is_lock_relevant.
Qed.
Instance val_equiv_pre_relevant ty eh ec: RelevantP (val_equiv_pre val_equiv ty eh ec).
Proof. rewrite /RelevantP. rewrite -val_equiv_fix_unfold'. apply val_equiv_relevant. Qed.
Definition bool_refine (v v': val) :=
match v, v' with
| LitV (LitBool b), LitV (LitBool b') ⇒
b = b'
| _, _ ⇒ False
end.
Definition expr_equiv ty := expr_rel_lift (val_equiv ty).
Instance expr_equiv_affine ty eh ec: AffineP (expr_equiv ty eh ec).
Proof. eapply expr_rel_aff_pres=>??; apply _. Qed.
Instance expr_equiv_relevant ty eh ec: RelevantP (expr_equiv ty eh ec).
Proof. eapply expr_rel_rel_pres=>??; apply _. Qed.
Record subst_tuple :=
stuple { styp : typ ; sval : expr; tval : expr }.
Definition subst_ctx := gmap string subst_tuple.
From iris.heap_lang Require Import substitution.
Definition subst2typ (S: subst_ctx) : typ_ctx := styp <$> S.
Definition subst2s (S: subst_ctx) : subst_map := sval <$> S.
Definition subst2t (S: subst_ctx) : subst_map := tval <$> S.
Definition ctx_expr_equiv (Γ: typ_ctx) (ty: typ) (e e': expr) : Prop :=
∀ (S: subst_ctx) (Herase: subst2typ S = Γ),
ClosedSubst [] (subst2s S) →
ClosedSubst [] (subst2t S) →
heap_ctx ★ sheap_ctx ★ ([★ map] x ↦ P ∈ S, (expr_equiv (styp P) (sval P) (tval P)))
⊢ expr_equiv ty (msubst (sval <$> S) e)
(msubst (tval <$> S) e').
Instance ctx_prop_affine S:
AffineP ([★ map] x↦P ∈S, (expr_equiv (styp P) (sval P) (tval P)))%I.
Proof.
intros; apply big_sep_affine.
rewrite /AffineL. induction map_to_list as [| a ?]; simpl; eauto using nil_affine.
destruct a; simpl; apply cons_affine; eauto using expr_equiv_affine.
Qed.
Instance ctx_prop_relevant S:
RelevantP ([★ map] x↦P ∈S, (expr_equiv (styp P) (sval P) (tval P)))%I.
Proof.
intros; apply big_sep_relevant.
rewrite /RelevantL. induction map_to_list as [| a ?]; simpl; eauto using nil_relevant.
destruct a; simpl; apply cons_relevant; eauto using expr_equiv_relevant.
Qed.
Lemma val_equiv_expr ty v v':
(val_equiv_pre val_equiv ty v v' ⊢ expr_equiv ty v v')%I.
Proof.
rewrite /expr_equiv /expr_rel_lift.
iIntros "#Hve". iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists v. iFrame "Hown".
iIntros "@". by rewrite val_equiv_fix_unfold'.
Qed.
Lemma expr_equiv_empty ty e e' (pf: ctx_expr_equiv ∅ ty e e'):
heap_ctx ★ sheap_ctx ⊢ (expr_rel_lift (val_equiv ty) e e').
Proof.
rewrite /expr_equiv in pf.
specialize (pf ∅). rewrite /subst2typ fmap_empty in pf.
efeed pose proof pf as pf'; eauto; try done.
rewrite big_sepM_empty right_id in pf' ×.
intros ->; auto.
Qed.
Lemma subst2typ_inv Γ S x ty:
Γ !! x = Some ty →
subst2typ S = Γ →
∃ eh ec, S !! x = Some {| styp := ty; sval := eh; tval := ec |}.
Proof.
rewrite /subst2typ. intros Hlook <-.
move:Hlook. rewrite lookup_fmap. case_eq (S !! x).
- intros st Heq. rewrite ?Heq.
inversion 1. destruct st; eauto.
- intros Hnone. rewrite ?Hnone.
inversion 1.
Qed.
From iris.proofmode Require Import coq_tactics environments.
Lemma tac_refine_bind Δ Δ' k t e K K' P:
envs_lookup k Δ = Some (false, ownT t (fill K' e) K (dK K (fill K' e))) →
envs_simple_replace k false (Esnoc Enil k (ownT t e (comp_ectx K K') (dK (comp_ectx K K') e))) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
rewrite ownT_focus //= ?right_id. by rewrite wand_elim_r.
Qed.
Lemma tac_refine_unbind Δ Δ' k t e K K' P :
envs_lookup k Δ = Some (false, ownT t e (comp_ectx K K') (dK (comp_ectx K K') e)) →
envs_simple_replace k false (Esnoc Enil k (ownT t (fill K' e) K (dK K (fill K' e)))) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite /dK fill_comp.
by rewrite -ownT_fill //= ?right_id wand_elim_r.
Qed.
Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_bind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ j _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) :=
lazymatch eval hnf in K with
| _ ⇒
eapply tac_refine_unbind with _ _ _ _ _ K;
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_focus" open_constr(efoc) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
heap_lang.tactics.reshape_expr e ltac:(fun K' e' ⇒
match e' with
| efoc ⇒ idtac K';
unify e' efoc;
refine_bind K' at j
end) || fail "refine_focus: cannot find" efoc "in" e
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_unfocus" :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (comp_ectx ?K0 ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e (?K0 ++ ?K) ?d0)] ⇒
refine_unbind K at j; simpl_subst
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
refine_unbind empty_ectx K at j; simpl_subst
| _ ⇒ fail "refine_unocus: could not find ownT"
end.
Lemma newlock_sound Γ:
ctx_expr_equiv Γ (Arrow Unit Lock) (newlock1) (newlock2).
Proof.
rewrite /ctx_expr_equiv.
intros IS ???.
iIntros "(#?&#?&#?)".
rewrite ?msubst_closed.
iIntros (i' K') "@ ! Hown".
wp_value. iPvsIntro. iExists (newlock1). iFrame.
iIntros "@".
rewrite val_equiv_fix_unfold'.
iIntros (??) "@ ! (%&%)"; subst.
iIntros (i K) "@ ! Hown".
iPoseProof (newlock_spec i K Emp with "[Hown]") as "Hwp".
{ iFrame. rewrite affine_affine right_id.
iSplitL ""; auto. }
iApply wp_wand_l; iFrame "Hwp".
iIntros "@". iIntros (lk) "HRes".
iDestruct "HRes" as (lks γ) "(Hlock&Hown)".
iExists lks. iFrame.
iIntros "@". iExists γ. done.
Qed.
Lemma sync_sound Γ el el' e e' ty:
ctx_expr_equiv Γ Lock el el' →
ctx_expr_equiv Γ (Arrow Unit ty) e e' →
ctx_expr_equiv Γ ty (sync1 el e) (sync2 el' e').
Proof.
rewrite /ctx_expr_equiv.
intros IHhas_typ1 IHhas_typ2 S ???.
iIntros "(#?&#?&#?)".
iIntros (i K) "@ ! Hown".
rewrite /sync1 /sync2 /sync.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
rewrite ?msubst_closed.
wp_focus (msubst (tval <$> S) el').
refine_focus (msubst (sval <$> S) el).
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (lk) "HRes".
iDestruct "HRes" as (lks) "(Hlock&Hown)".
refine_unfocus.
refine_focus (let: "lk" := lks in _)%E.
wp_let. refine_let (dK (K ++ reverse [AppLCtx (msubst (sval <$> S) e)])
((λ: "f", acq1 lks;; let: "z" := "f" #() in rel1 lks ;; "z"))).
{ rewrite /dK. case_match; omega. }
{ rewrite /dK. case_match; omega. }
eapply tac_refine_unbind with _ "Hown" _ _ K _.
{ env_cbv. simpl comp_ectx. reflexivity. }
{ env_cbv. reflexivity. }
idtac.
wp_value. iPvsIntro.
wp_focus (msubst (tval <$> S) e').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(AppRCtx ((λ: "f", acq1 lks;;
let: "z" := "f" #() in rel1 lks ;; "z")) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (f') "HRes".
iDestruct "HRes" as (f) "(Hf&Hown)".
refine_unfocus.
wp_let. refine_let (dK K (acq1 lks ;; let: "z" := f #() in rel1 lks ;; "z")).
{ rewrite /dK. case_match; omega. }
{ rewrite /dK. case_match; omega. }
rewrite val_equiv_fix_unfold'. rewrite /val_equiv_pre.
iDestruct "Hlock" as (γ) "#Hlock".
rewrite affine_elim.
wp_focus (acq2 lk). refine_focus (acq1 lks).
iPoseProof (acquire_spec i with "[Hown]") as "Hwp".
{ iFrame. done. }
iApply wp_wand_l; iFrame "Hwp".
iIntros "@". iIntros (?) "(%&Hlocked&Hown&_)".
subst.
refine_unfocus.
wp_let. refine_let (dK K (let: "z" := f #() in rel1 lks ;; "z")).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
idtac.
wp_focus (f' #())%E.
refine_focus (f #())%E.
rewrite affine_elim.
rewrite val_equiv_fix_unfold'. rewrite /val_equiv_pre -/val_equiv_pre.
iSpecialize ("Hf" $! #()%V).
iSpecialize ("Hf" $! #()%V).
iSpecialize ("Hf" with "[]").
{ iSplitL; auto. }
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hf" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hf".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
wp_let. refine_let (dK K (rel1 lks ;; v)).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
wp_focus (rel2 lk)%E.
refine_focus (rel1 lks)%E.
iPoseProof (release_spec i with "[Hown Hlocked]") as "Hwp".
{ iFrame. iSplitL; first done. rewrite affine_affine. done. }
iApply wp_wand_l; iFrame "Hwp".
iIntros "@". iIntros (?) "(%&Hown)".
subst. refine_unfocus.
wp_seq. refine_let (dK K v).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
wp_value. iPvsIntro. iExists v. iFrame.
rewrite val_equiv_fix_unfold'. done.
Qed.
Lemma case_sound Γ ty1 ty2 e e' ty el el' er er':
ctx_expr_equiv Γ (Sum ty1 ty2) e e' →
ctx_expr_equiv Γ (Arrow ty1 ty) el el' →
ctx_expr_equiv Γ (Arrow ty2 ty) er er' →
ctx_expr_equiv Γ ty (Case e el er) (Case e' el' er').
Proof.
rewrite /ctx_expr_equiv.
intros IHhas_typ1 IHhas_typ2 IHhas_typ3 S ???.
iIntros "(#?&#?&#?)".
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(CaseCtx _ _ :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite affine_or.
iDestruct "Hv" as "[?|?]".
× iDestruct "Hv" as (v1 v1') "(%&%&Hv1)".
subst.
iApply wp_case_inl.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
iNext.
iPoseProof (refine_case_inl (dK K _) (dK K (((msubst (sval <$> S) el) v1))) with "[Hown]")
as "Hown";
[ | | | eauto | iFrame; done | ].
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
{ rewrite to_of_val; auto with fsaV. }
iPsvs "Hown".
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
iPvsIntro.
rewrite /expr_equiv /expr_rel_lift.
rewrite -/of_val.
wp_focus (msubst (tval <$> S) el')%E.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) el) _
(AppLCtx _ :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_equiv /expr_rel_lift.
rewrite (affine_elim).
iSpecialize ("Hv" $! v1 v1' with "Hv1").
iSpecialize ("Hv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hv".
iIntros "@". iIntros (vnew') "HRes".
iDestruct "HRes" as (vnew) "(Hvnew&Hown)".
iExists vnew. iFrame. rewrite /lift2 //=.
rewrite ?val_equiv_fix_unfold' //=.
× iDestruct "Hv" as (v1 v1') "(%&%&Hv1)".
subst.
iApply wp_case_inr.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
iNext.
iPoseProof (refine_case_inr (dK K _) (dK K (((msubst (sval <$> S) er) v1))) with "[Hown]")
as "Hown";
[ | | | eauto | iFrame; done | ].
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
{ rewrite to_of_val; auto with fsaV. }
iPsvs "Hown".
iPoseProof (IHhas_typ3 S with "[]") as "Hequiv"; auto.
iPvsIntro.
rewrite /expr_equiv /expr_rel_lift.
rewrite -/of_val.
wp_focus (msubst (tval <$> S) er')%E.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) er) _
(AppLCtx _ :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
rewrite ?val_equiv_fix_unfold' //=.
rewrite /expr_equiv /expr_rel_lift.
rewrite (affine_elim).
iSpecialize ("Hv" $! v1 v1' with "Hv1").
iSpecialize ("Hv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hv".
iIntros "@". iIntros (vnew') "HRes".
iDestruct "HRes" as (vnew) "(Hvnew&Hown)".
iExists vnew. iFrame. rewrite /lift2 //=.
rewrite ?val_equiv_fix_unfold' //=.
Qed.
Lemma delete_delete_lookup x y (S: subst_ctx):
delete y (delete x S) !! x = None.
Proof.
case (decide (y = x)).
- intros →. apply lookup_delete.
- intros ?. rewrite lookup_delete_ne //; apply lookup_delete.
Qed.
Lemma closing_helper {A: Type} x y x' ty1 ty2 (f: subst_tuple → A) Γ (S: subst_ctx):
subst2typ S = Γ →
x' ∈ (map_to_list (<[y:=ty1]> (<[x:=ty2]> Γ))).*1 →
x' ∈ [y; x] ∨ x' ∈ dom stringset (delete y (delete x (f <$> S))).
Proof.
intros Hsubst2typ.
intros ((s&e'')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
case (decide (s = x)).
{ intros. subst. left. set_solver+. }
case (decide (s = y)).
{ intros. subst. left. set_solver+. }
intros Hneqy Hneqx.
right.
apply elem_of_dom.
move: Helem.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite lookup_insert_ne // lookup_delete_ne //.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
Qed.
Lemma lookup_delete_subst_ctx_1 (S: subst_ctx) (x: string):
delete x S !! x = None.
Proof. apply lookup_delete. Qed.
Lemma rec_sound Γ ty1 ty2 e e' (x y: string):
x ≠ y →
(<[y:=Arrow ty1 ty2]> (<[x:=ty1]> Γ) ⊩ e ↝ e' : ty2) →
ctx_expr_equiv (<[y := Arrow ty1 ty2]>(<[x := ty1]> Γ)) ty2 e e' →
ctx_expr_equiv Γ (Arrow ty1 ty2) (rec: y x := e)%E (rec: y x := e')%E.
Proof.
rewrite /ctx_expr_equiv.
intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iLob as "IH".
iIntros "@ !". iIntros (i K) "@ ! Hown".
rewrite //=.
assert (Hclod1: Closed ([y; x]) (msubst (delete y (delete x (tval <$> S))) e')).
{ rewrite //=.
eapply msubst_closing_1. eapply typ_context_closed_2; eauto.
{ do 2 apply heap_lang.substitution.ClosedSubst_delete. eauto. }
intros x'. eapply closing_helper; assumption.
}
assert (Hclod2: Closed ([y; x]) (msubst (delete y (delete x (sval <$> S))) e)).
{ rewrite //=.
eapply msubst_closing_1. eapply (typ_context_closed_2 _ e e'); eauto.
{ do 2 apply heap_lang.substitution.ClosedSubst_delete. eauto. }
intros x'. eapply closing_helper; assumption.
}
assert (Hclo1: Closed [] (rec: y x := (msubst (delete y (delete x (tval <$> S))) e'))).
{ rewrite /Closed //=. }
assert (Hclo2: Closed [] (rec: y x := (msubst (delete y (delete x (sval <$> S))) e))).
{ rewrite /Closed //=. }
iApply wp_value; eauto.
{ rewrite //=. case_decide; eauto.
- repeat f_equal. apply proof_irrel.
- exfalso; eauto.
}
iExists (rec: y x := (msubst (delete y (delete x (sval <$> S))) e))%V.
iFrame.
rewrite val_equiv_fix_unfold' //=.
iIntros "@".
iIntros (vh vc). iIntros "@ ! #Hpre".
rewrite {2}/expr_equiv {2}/expr_rel_lift.
iIntros (i' K') "@ ! Hown".
wp_rec.
pose (S' :=
(<[y := {| styp := Arrow ty1 ty2;
sval := (rec: y x := msubst (delete y (delete x (sval <$> S))) e);
tval := (rec: y x := msubst (delete y (delete x (tval <$> S))) e')|}]>
(<[x := {| styp := ty1;
sval := of_val vh;
tval := of_val vc |}]>(delete y (delete x S))))).
iDestruct "HS" as "(#?&#?&#HS')".
refine_rec (dK K' (msubst (sval <$> S') e)).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
specialize (H1 S').
iPoseProof (H1 with "[]") as "Hequiv".
{ rewrite /S'. rewrite /subst2typ. rewrite ?fmap_insert //=.
rewrite ?fmap_delete ?insert_delete.
rewrite -delete_insert_ne; last congruence.
rewrite ?insert_delete.
rewrite /subst2typ in Herase. subst. auto.
}
{ rewrite /S' /subst2s ?fmap_insert //=.
apply ClosedSubst_insert; auto.
apply ClosedSubst_insert; auto.
rewrite ?fmap_delete.
apply ClosedSubst_delete; auto.
apply ClosedSubst_delete; auto.
solve_closed.
}
{ rewrite /S' /subst2t ?fmap_insert //=.
apply ClosedSubst_insert; auto.
apply ClosedSubst_insert; auto.
rewrite ?fmap_delete.
apply ClosedSubst_delete; auto.
apply ClosedSubst_delete; auto.
solve_closed.
}
iSplitL ""; first done.
iSplitL ""; first done.
idtac.
rewrite /S'. rewrite big_sepM_insert //=.
iSplitL.
{ rewrite affine_elim. rewrite /expr_equiv. done. }
rewrite /S'. rewrite big_sepM_insert //=.
iSplitL.
- by iApply val_equiv_expr.
- case (decide (is_Some (S !! x))).
× intros (P&Heq). rewrite big_sepM_delete; last eapply Heq.
case (decide (is_Some ((delete x S) !! y))).
idtac.
** intros (P'&Heq'). rewrite big_sepM_delete; last eapply Heq'.
iDestruct "HS'" as "(?&?&?)".
iFrame; eauto.
** intros Hnone. assert (delete x S = delete y (delete x S)) as Heq'.
{ rewrite {1}(delete_notin (delete x S) y); eauto. apply eq_None_not_Some; eauto. }
rewrite -Heq'.
iDestruct "HS'" as "(?&?)".
iFrame; eauto.
× intros Hnone. assert (S = delete x S) as Heq.
{ rewrite {1}(delete_notin S x); eauto. apply eq_None_not_Some; eauto. }
rewrite -?Heq.
case (decide (is_Some (S !! y))).
** intros (P'&Heq'). rewrite big_sepM_delete; last eapply Heq'.
iDestruct "HS'" as "(?&?)".
iFrame; eauto.
** intros Hnone'. assert (S = delete y S) as Heq'.
{ rewrite {1}(delete_notin S y); eauto. apply eq_None_not_Some; eauto. }
rewrite -?Heq'.
done.
- apply delete_delete_lookup.
- rewrite -delete_insert_ne //. apply lookup_delete_subst_ctx_1.
- assert (sval <$> S' = <[x := of_val vh]>
(<[y := (rec: y x := (msubst (delete y (delete x (sval <$>S))) e))%E]>
(delete y (delete x (sval <$> S))))) as HsS'.
{ rewrite /S'. rewrite ?fmap_insert ?fmap_delete //=. rewrite insert_commute //. }
assert (tval <$> S' = <[x := of_val vc]>
(<[y := (rec: y x := (msubst (delete y (delete x (tval <$>S))) e'))%E]>
(delete y (delete x (tval <$> S))))) as HtS'.
{ rewrite /S'. rewrite ?fmap_insert ?fmap_delete //=. rewrite insert_commute //. }
rewrite HsS' HtS'.
rewrite msubst_insert_1; last 2 first.
{ apply ClosedSubst_insert; auto. do 2 apply ClosedSubst_delete; auto. }
{ rewrite lookup_insert_ne // lookup_delete_ne //. apply lookup_delete. }
rewrite msubst_insert_1; last 2 first.
{ do 2 apply ClosedSubst_delete; auto. }
{ apply lookup_delete. }
rewrite msubst_insert_1; last 2 first.
{ apply ClosedSubst_insert; auto. do 2 apply ClosedSubst_delete; auto. }
{ rewrite lookup_insert_ne // lookup_delete_ne //. apply lookup_delete. }
rewrite msubst_insert_1; last 2 first.
{ do 2 apply ClosedSubst_delete; auto. }
{ apply lookup_delete. }
iSpecialize ("Hequiv" $! i' K' with "Hown").
iApply wp_wand_l. iFrame "Hequiv".
iIntros "@". iIntros (v) "Hpre'".
iDestruct "Hpre'" as (v') "Hpre'".
iExists v'. rewrite val_equiv_fix_unfold'.
done.
Qed.
Lemma fill_item_val_2 Ki e1 e2 :
is_Some (to_val e1) → is_Some (to_val e2) →
is_Some (to_val (fill_item Ki e1)) →
is_Some (to_val (fill_item Ki e2)).
Proof.
revert e1 e2. induction Ki; simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq.
match goal with
[ |- context[(to_val ?e)]] ⇒ destruct (to_val e)
end; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
- intros e0 e1. inversion 1 as [? ->]. inversion 1 as [? ->].
simplify_option_eq; eauto.
Qed.
Lemma fill_val_dK K e1 e2:
is_Some (to_val e1) →
is_Some (to_val e2) →
dK K e1 = dK K e2.
Proof.
intros. rewrite /dK.
rewrite /ectx_language.fill //=.
do 2 case_match; auto.
- exfalso.
specialize (@ectxi_language.fill_val_2 heap_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (fill_item_val_2) K e1 e2);
eauto.
congruence.
- exfalso.
specialize (@ectxi_language.fill_val_2 heap_lang.expr _ _ _ _).
rewrite /ectxi_language.to_val //=.
rewrite /ectxi_language.fill_item //=.
intros Hfill.
destruct (Hfill (fill_item_val_2) K e2 e1);
eauto.
congruence.
Qed.
Lemma fundamental Γ ty e e':
Γ ⊩ e ↝ e' : ty →
ctx_expr_equiv Γ ty e e'.
Proof.
rewrite /ctx_expr_equiv.
intros has_typ.
induction has_typ .
- intros S Herase HcloSh HcloSc.
rewrite ?msubst_unfold //.
eapply subst2typ_inv in Herase as (e&e'&Hlook); eauto.
rewrite big_sepM_delete; eauto.
rewrite ?lookup_fmap ?Hlook //=.
iIntros "(?&?&?&_)". done.
- intros; iIntros "_". simpl.
rewrite ?msubst_msubst' // /expr_equiv /expr_rel_lift.
iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists #b.
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists b. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite ?msubst_msubst' // /expr_equiv /expr_rel_lift.
iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists #n.
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iExists n. iSplit; auto.
- intros; iIntros "_". simpl.
rewrite ?msubst_msubst' // /expr_equiv /expr_rel_lift.
iIntros (i K) "@ ! Hown".
wp_value. iPvsIntro. iExists #().
iFrame "Hown". rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e1) _
(PairLCtx (msubst (sval <$> S) e2) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e1')%E.
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv1"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv1" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv1".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e2) _
(PairRCtx v1 :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e2')%E.
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv2"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv2" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv2".
iIntros "@". iIntros (v2') "HRes".
iDestruct "HRes" as (v2) "(Hv2&Hown)".
refine_unfocus.
wp_value. iPvsIntro. iExists (v1, v2)%V.
iFrame "Hown". iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
iIntros "@". iExists v1, v2, v1', v2'.
do 2 (iSplitL ""; auto).
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(FstCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
iDestruct "Hv" as (v1 v2 v1' v2') "(%&%&Hv1&Hv2)".
subst.
wp_value; iPvsIntro.
iApply wp_fst.
rewrite to_of_val; auto with fsaV.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
iNext. refine_proj (dK K v1).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iExists v1. iFrame. iIntros "@".
rewrite ?val_equiv_fix_unfold' //=.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(SndCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
iDestruct "Hv" as (v1 v2 v1' v2') "(%&%&Hv1&Hv2)".
subst.
wp_value; iPvsIntro.
iApply wp_snd.
rewrite to_of_val; auto with fsaV.
econstructor; eauto.
rewrite to_of_val; auto with fsaV.
iNext. refine_proj (dK K v2).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iExists v2. iFrame. iIntros "@".
rewrite ?val_equiv_fix_unfold' //=.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(InjLCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
wp_value; iPvsIntro.
iExists (InjLV v).
rewrite ?val_equiv_fix_unfold' //=.
iFrame. iIntros "@". iLeft.
iExists v, v'.
iSplitL ""; auto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(InjRCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e').
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&_)".
iClear "HS". rewrite ?val_equiv_fix_unfold' //=.
wp_value; iPvsIntro.
iExists (InjRV v).
rewrite ?val_equiv_fix_unfold' //=.
iFrame. iIntros "@". iRight.
iExists v, v'.
iSplitL ""; auto.
- intros. eapply case_sound; rewrite /ctx_expr_equiv.
× eapply IHhas_typ1.
× eapply IHhas_typ2.
× eapply IHhas_typ3.
× eauto.
× eauto.
× eauto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
rewrite //=.
assert (Closed (≠ :b: ≠ :b: []) (msubst (tval <$> S) e1')).
{ rewrite //=.
eapply msubst_closing_1. eapply typ_context_closed_2; eauto.
assumption.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
assert (Closed (≠ :b: ≠ :b: []) (msubst (sval <$> S) e1)).
{ rewrite //=.
eapply msubst_closing_1. eapply (typ_context_closed_2 _ e1 e1'); eauto.
assumption.
intros x ((s&e')&Heq&Helem)%elem_of_list_fmap_2.
subst. apply elem_of_map_to_list in Helem.
intros; right. apply elem_of_dom.
move: Helem.
rewrite /subst2typ ?lookup_fmap /is_Some //=.
case_eq (S !! s).
× intros ? Heq. rewrite Heq. eauto.
× intros Hnone. rewrite Hnone. inversion 1.
}
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e2) _
(AppRCtx (λ:≠, (msubst (sval <$> S) e1)%V) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
wp_focus (msubst (tval <$> S) e2').
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v') "HRes".
iDestruct "HRes" as (v) "(Hv&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&#HS')".
wp_seq. refine_seq (dK K (msubst (sval <$> S) e1)).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (vres') "HRes".
iDestruct "HRes" as (vres) "(Hvres&Hown)".
iExists vres. iFrame. done.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_apply wp_fork.
iDestruct "HS" as "(#?&#?&#?)".
refine_fork (dK K #()%E) i' as "Hown'".
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iSplitL "Hown".
{ iExists #(). iFrame. rewrite val_equiv_fix_unfold' /val_equiv_pre.
iIntros "@". iSplit; auto.
}
idtac.
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i' [] with "[Hown']").
{ rewrite /fresh_delay /dK //=. }
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v) "Hpre".
iDestruct "Hpre" as (vc) "(?&?)".
rewrite /dK //= to_of_val.
refine_stopped.
- intros. eapply rec_sound; rewrite /ctx_expr_equiv.
× eauto.
× eauto.
× eapply IHhas_typ.
× eauto.
× eauto.
× eauto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) e1').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e1) _
(AppLCtx (msubst (sval <$> S) e2) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
wp_focus (msubst (tval <$> S) e2').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e2) _
(AppRCtx v1 :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v2') "HRes".
iDestruct "HRes" as (v2) "(Hv2&Hown)".
refine_unfocus.
rewrite val_equiv_fix_unfold' //.
rewrite val_equiv_fix_unfold' //.
rewrite (affine_elim).
rewrite (affine_elim).
iSpecialize ("Hv1" $! v2 v2' with "Hv2").
iSpecialize ("Hv1" $! i _ with "Hown").
idtac.
iApply wp_wand_l. iFrame "Hv1".
iIntros "@". iIntros (vres') "HRes".
iDestruct "HRes" as (vres) "(HRes&Hown)".
iExists vres. iFrame.
idtac. rewrite val_equiv_fix_unfold'.
rewrite //=.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) e').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(AllocCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
iDestruct "HS" as "(#?&#?&HS')".
wp_alloc l' as "Hl'".
rewrite -psvs_pvs'.
refine_alloc (dK K (#l')%V) l as "Hl".
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
assert (dK K (#l)%V = dK K (#l')) as HdK.
{ rewrite /dK. rewrite /to_of_val.
eapply fill_val_dK; eauto. }
iExists (#l)%V.
iSplitL "Hl' Hv1 Hl".
iPvs (inv_alloc refN _ (∃ v v', l ↦s v ★ l' ↦ v' ★ val_equiv_pre val_equiv ty v v')%I
with "[Hl' Hv1 Hl]") as "Hinv".
{ rewrite /refN. eauto with ndisj. }
{ iIntros "@ >". iExists v1, v1'. iFrame. rewrite val_equiv_fix_unfold'.
rewrite affine_elim. done. }
iPvsIntro. iIntros "@". rewrite val_equiv_fix_unfold'. iExists l, l'.
iSplitL ""; first auto.
iSplitL ""; first auto.
done.
iPvsIntro. rewrite HdK. done.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) el').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) el) _
(StoreLCtx (msubst (sval <$> S) e) :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ1 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
wp_focus (msubst (tval <$> S) e')%E.
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) e) _
(StoreRCtx v1 :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ2 S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v2') "HRes".
iDestruct "HRes" as (v2) "(Hv2&Hown)".
refine_unfocus.
rewrite val_equiv_fix_unfold'.
iDestruct "Hv1" as (l1 l1') "(%&%&Hv1)".
rewrite -/val_equiv_pre.
iInv "Hv1" as "Hinv"; auto with fsaV.
iDestruct "Hinv" as (v v') "(Hl1&Hl2&Hvequiv)".
iTimeless "Hl1". iTimeless "Hl2".
rewrite (affine_elim).
rewrite (affine_elim).
rewrite (affine_elim).
subst.
iDestruct "HS" as "(#?&#?&#?)".
assert (refN ⊥ heapN) as Hdisj1' by (rewrite /refN; eauto with ndisj).
assert (refN ⊥ sheapN) as Hdisj2' by (rewrite /refN; eauto with ndisj).
wp_store. refine_store (dK K #()).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
iSplitL "Hl1 Hl2 Hv2".
{ iIntros "@ >". iExists v2, v2'. iFrame.
rewrite val_equiv_fix_unfold'. done. }
iExists #(). iFrame.
rewrite val_equiv_fix_unfold'. rewrite //=.
iIntros "@". iSplitL ""; auto.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "@ ! Hown".
wp_focus (msubst (tval <$> S) el').
eapply tac_refine_bind with _ "Hown" _ (msubst (sval <$> S) el) _
(LoadCtx :: []).
{ env_cbv. simpl fill. reflexivity. }
{ env_cbv. reflexivity. }
iPoseProof (IHhas_typ S with "[]") as "Hequiv"; auto.
rewrite /expr_equiv /expr_rel_lift.
iSpecialize ("Hequiv" $! i _ with "Hown").
iApply wp_wand_l; iFrame "Hequiv".
iIntros "@". iIntros (v1') "HRes".
iDestruct "HRes" as (v1) "(Hv1&Hown)".
refine_unfocus.
rewrite val_equiv_fix_unfold'.
iDestruct "Hv1" as (l1 l1') "(%&%&Hv1)".
rewrite -/val_equiv_pre.
iInv "Hv1" as "Hinv"; auto with fsaV.
iDestruct "Hinv" as (v v') "(Hl1&Hl2&Hvequiv)".
iTimeless "Hl1". iTimeless "Hl2".
rewrite (affine_elim).
rewrite (affine_elim).
rewrite (affine_elim).
subst.
iDestruct "HS" as "(#?&#?&#?)".
assert (refN ⊥ heapN) as Hdisj1' by (rewrite /refN; eauto with ndisj).
assert (refN ⊥ sheapN) as Hdisj2' by (rewrite /refN; eauto with ndisj).
wp_load. refine_load (dK K #()).
{ rewrite /dK; case_match; omega. }
{ rewrite /dK; case_match; omega. }
assert (dK K (#())%V = dK K v) as HdK.
{ rewrite /dK. rewrite /to_of_val. eapply fill_val_dK; eauto.
rewrite to_of_val. eauto. }
rewrite HdK.
iDestruct "Hvequiv" as "#Hvequiv".
iSplitL "Hl1 Hl2".
{ iIntros "@ >". iExists v, v'. iFrame. done. }
iExists v. rewrite val_equiv_fix_unfold'. iFrame.
iIntros "@". done.
- intros. eapply newlock_sound; eauto.
- intros. eapply sync_sound; eauto.
Qed.
Lemma heap_prim_dec: ∀ (e: expr) σ,
{ t | prim_step (e: expr) σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}.
Proof.
intros. edestruct (ClassicalEpsilon.excluded_middle_informative
((∃ (e' : language.expr (ectx_lang (heap_lang.expr)))
(σ' : language.state (ectx_lang (heap_lang.expr)))
(ef' : option (language.expr (ectx_lang (heap_lang.expr)))),
language.prim_step e σ e' σ' ef'))).
× apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (e'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (σ'&e0).
apply ClassicalEpsilon.constructive_indefinite_description in e0.
destruct e0 as (ef'&e0).
left. ∃ (e', σ', ef'). eauto.
× right. auto.
Qed.
End lr.
End lock_reln.