Library iris.chan_lang.refine_heap_proofmode
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.algebra Require Export upred_tactics.
From iris.chan_lang Require Export tactics refine_heap.
Import uPred.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{scheapG Λ Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types Δ : envs (iResUR Λ (globalF Σ)).
Context (d: nat).
Context (d': nat).
Context (Hd_le: (d ≤ Kd)%nat).
Context (Hd'_le: (d' ≤ Kd)%nat).
Lemma tac_refine_alloc Δ E i k j t K P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Alloc) K d) →
(envs_delete k false Δ ⊢ ⧆ (envs_delete k false Δ)) →
nclose scheapN ⊆ E →
(∀ l, ∃ Δ',
envs_simple_replace k false (Esnoc (Esnoc Enil j (l ↦c ([], []))) k
(ownT t (Pair (Lit (LitLoc l cleft))
(Lit (LitLoc l cright))) K d')) Δ
= Some Δ' ∧ (Δ' ⊢ P)) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite relevant_elim assoc (refine_alloc _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite sep_exist_r.
apply exist_elim⇒l. edestruct (HΔ l) as (Δ'&Heq&Himpl).
rewrite -Himpl affine_elim (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite (comm _ (ownT t _ _ _)).
by apply wand_elim_r.
Qed.
Lemma tac_refine_recv k t Δ Δ' Δ'' E i j K l side v l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Recv (Lit (LitLoc l side))) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, v :: l2))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c (v :: l1, l2))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c (l1, l2))) k
(ownT t (Pair (Lit (LitLoc l side)) (of_val v)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_recv_miss k t Δ Δ' Δ'' E i j K l side l1 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Recv (Lit (LitLoc l side))) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, []))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c ([], l1))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c
match side with
|cleft ⇒ (l1, [])
|cright ⇒ ([], l1)
end)) k
(ownT t (Recv (Lit (LitLoc l side))) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_miss_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_miss_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_send k t e Δ Δ' Δ'' E i j K l side v' l1 l2 P :
to_val e = Some v' →
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Send (Lit (LitLoc l side)) e) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦c (l1, l2))%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c match side with
| cleft ⇒ (l1 ++ [v'], l2)
| cright ⇒ (l1, l2 ++ [v'])
end)) k
(ownT t (Lit (LitLoc l side)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros ? Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
destruct side.
- rewrite (refine_send_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite (refine_send_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_select k t Δ Δ' Δ'' E i j K l side choice l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Select (Lit (LitLoc l side)) choice) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦c (l1, l2))%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c match side with
| cleft ⇒ (l1 ++ [label_to_sum choice], l2)
| cright ⇒ (l1, l2 ++ [label_to_sum choice])
end)) k
(ownT t (Lit (LitLoc l side)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
destruct side.
- rewrite (refine_select_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite (refine_select_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rcase_left k t Δ Δ' Δ'' E i j K l side e1 e2 l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, InjLV (LitV LitUnit) :: l2))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c (InjLV (LitV LitUnit) :: l1, l2))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c (l1, l2))) k
(ownT t (App e1 (Lit (LitLoc l side))) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_left_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_right_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rcase_right k t Δ Δ' Δ'' E i j K l side e1 e2 l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, InjRV (LitV LitUnit) :: l2))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c (InjRV (LitV LitUnit) :: l1, l2))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c (l1, l2))) k
(ownT t (App e2 (Lit (LitLoc l side))) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_left_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_right_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rcase_miss k t Δ Δ' Δ'' E i j K l side e1 e2 l1 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, []))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c ([], l1))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c
match side with
|cleft ⇒ (l1, [])
|cright ⇒ ([], l1)
end)) k
(ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_miss_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_miss_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_pure Δ Δ' E i k t K e e' P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
((scheap_ctx ★ ownT t e K d) ⊢ |={E}=>> ownT t e' K d') →
envs_simple_replace k false (Esnoc Enil k (ownT t e' K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Haff ? Hstep HΔ1 HΔ2.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc.
rewrite relevant_elim.
rewrite Hstep.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rec Δ Δ' E i k t K f x erec e2 v2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (App (Rec f x erec) e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e2 = Some v2 →
Closed (f :b: x :b: []) erec →
envs_simple_replace k false
(Esnoc Enil k (ownT t (subst' x e2 (subst' f (Rec f x erec) erec)) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_rec; eauto. Qed.
Lemma tac_refine_letp Δ Δ' E i k t K x y e1 e2 eb v1 v2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Letp x y (Pair e1 e2) eb) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e1 = Some v1 →
to_val e2 = Some v2 →
Closed (x :b: y :b: []) eb →
envs_simple_replace k false
(Esnoc Enil k (ownT t (subst' y e2 (subst' x e1 eb)) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_letp; eauto. Qed.
Lemma tac_refine_lam Δ Δ' E i k t K x ef e v P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (App (Lam x ef) e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e = Some v →
Closed (x :b: []) ef →
envs_simple_replace k false (Esnoc Enil k (ownT t (subst' x e ef) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto using refine_lam. Qed.
Lemma tac_refine_bin_op Δ Δ' E i k t K op l1 l2 l' P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (BinOp op (Lit l1) (Lit l2)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
bin_op_eval op l1 l2 = Some l' →
envs_simple_replace k false (Esnoc Enil k (ownT t (Lit l') K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_bin_op; eauto. Qed.
Lemma tac_refine_un_op Δ Δ' E i k t K op l l' P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (UnOp op (Lit l)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
un_op_eval op l = Some l' →
envs_simple_replace k false (Esnoc Enil k (ownT t (Lit l') K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_un_op; eauto. Qed.
Lemma tac_refine_if_true Δ Δ' E i k t K e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (If (Lit (LitBool true)) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
envs_simple_replace k false (Esnoc Enil k (ownT t e1 K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_if_true; eauto. Qed.
Lemma tac_refine_if_false Δ Δ' E i k t K e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (If (Lit (LitBool false)) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
envs_simple_replace k false (Esnoc Enil k (ownT t e2 K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_if_false; eauto. Qed.
Lemma tac_refine_case_inl Δ Δ' E i k t K e0 v0 e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjL e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e0 = Some v0 →
envs_simple_replace k false (Esnoc Enil k (ownT t (App e1 e0) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_case_inl; eauto. Qed.
Lemma tac_refine_case_inr Δ Δ' E i k t K e0 v0 e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjR e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e0 = Some v0 →
envs_simple_replace k false (Esnoc Enil k (ownT t (App e2 e0) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_case_inr; eauto. Qed.
Lemma tac_refine_fork j Δ E i k t K e P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Fork e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
(∀ t', ∃ Δ',
envs_simple_replace k false (Esnoc (Esnoc Enil j (ownT t' e empty_ectx (fresh_delay _ Fd e)))
k (ownT t (Lit LitUnit) K d')) Δ
= Some Δ' ∧
(Δ' ⊢ P)) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite relevant_elim assoc (refine_fork _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite sep_exist_r.
apply exist_elim⇒t'. edestruct (HΔ t') as (Δ'&Heq&Himpl).
rewrite -Himpl affine_elim (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite (comm _ (ownT t _ _ _)).
by apply wand_elim_r.
Qed.
Lemma tac_refine_stopped Δ k t e v :
to_val e = Some v →
envs_lookup k Δ = Some (false, ownT t e empty_ectx 0) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
Δ ⊢ uPred_stopped.
Proof.
intros Hval Hl1 Haff.
rewrite envs_lookup_sound //=; simpl.
rewrite Haff. rewrite -(of_to_val e v); eauto.
rewrite ownT_val_stopped. auto.
Qed.
Lemma tac_refine_delay Δ E Δ' i k t e K P:
(d > d')%nat →
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
envs_simple_replace k false (Esnoc Enil k (ownT t e K d')) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hgt Hl1 Hl2 Haff ? Hrep Hd.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite relevant_elim assoc.
rewrite (refine_delay _ d' _ _ E); eauto.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite affine_elim.
simpl. rewrite right_id.
rewrite -Hd. by apply wand_elim_r.
Qed.
Lemma tac_refine_bind Δ Δ' k t e K K' P :
envs_lookup k Δ = Some (false, ownT t (fill K' e) K d) →
envs_simple_replace k false (Esnoc Enil k (ownT t e (comp_ectx K K') d)) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
by rewrite ownT_focus //= ?right_id 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') d) →
envs_simple_replace k false (Esnoc Enil k (ownT t (fill K' e) K d)) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
by rewrite -ownT_fill //= ?right_id wand_elim_r.
Qed.
End heap.
Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply (tac_refine_bind _ _ _ j _ _ _ K);
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_bind" constr(K) :=
lazymatch eval hnf in K with
| _ ⇒
eapply (tac_refine_bind _ _ _ _ _ _ _ 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 _ _ _ j _ _ _ K);
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) constr(K') "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply (tac_refine_unbind _ _ _ j _ _ K 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 _ _ _ _ _ _ _ K);
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_alloc" constr(dnew) ident(l) "as" constr(H) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?id (ownT ?i ?e ?K ?dold)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Alloc ⇒ refine_bind K' at id;
eapply tac_refine_alloc with dold dnew _ _ H _ _
end)
| fail 1 "refine_alloc: cannot find 'Alloc' in " e];
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_alloc: non-affine ctxt"
| done || eauto with ndisj
| first [ intros l | fail 1 "refine_alloc:" l "not fresh" ];
eexists; split;
[ env_cbv ; reflexivity || fail "refine_allc:" H "not fresh"
| rewrite -ownT_fill; simpl ectx_language.fill ]]
| _ ⇒ fail "refine_alloc: no ownT found"
end.
Tactic Notation "refine_alloc" constr(dnew) ident(l) :=
let H := iFresh in refine_alloc dnew l as H.
Tactic Notation "refine_recv" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Recv ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_recv with d0 dnew j i _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_recv_miss" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Recv ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_recv_miss with d0 dnew j i _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_send" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e0 ?K ?d0)] ⇒
first
[ reshape_expr e0 ltac:(fun K' e' ⇒
match eval hnf in e' with
Send ?el ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_send with d0 dnew j i e'' _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_send: cannot find 'Send' in " e0 ];
[ try omega | try omega | wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_send: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_send: no ownT found"
end.
Tactic Notation "refine_select" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e0 ?K ?d0)] ⇒
first
[ reshape_expr e0 ltac:(fun K' e' ⇒
match eval hnf in e' with
Select ?el ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_select with d0 dnew j i _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_select: cannot find 'Select' in " e0 ];
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_select: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_select: no ownT found"
end.
Tactic Notation "refine_rcase_left" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
RCase _ _ _ ⇒ refine_bind K' at j;
eapply tac_refine_rcase_left with d0 dnew j i
_ _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_rcase_right" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
RCase _ _ _ ⇒ refine_bind K' at j;
eapply tac_refine_rcase_right with d0 dnew j i
_ _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_rcase_miss" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
RCase _ _ _ ⇒ refine_bind K' at j;
eapply tac_refine_rcase_miss with d0 dnew j i
_ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_rec" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e
ltac:(fun K' e' ⇒
match eval hnf in e' with
chan_lang.App ?e1 _ ⇒ refine_bind K' at j;
eapply (tac_refine_rec d0 dnew);
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _
|| fail "refine_lam: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill; simpl_subst ]
end)
| fail 1 "refine_lam: cannot find 'App' in " e ]
| _ ⇒ fail "refine_lam: no ownT found"
end.
Tactic Notation "refine_lam" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e
ltac:(fun K' e' ⇒
match eval hnf in e' with
App ?e1 _ ⇒ refine_bind K' at j;
eapply (tac_refine_lam d0 dnew);
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _
|| fail "refine_lam: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill; simpl_subst ]
end)
| fail 1 "refine_lam: cannot find 'App' in " e ]
| _ ⇒ fail "refine_lam: no ownT found"
end.
Tactic Notation "refine_let" constr(dnew) := refine_lam dnew.
Tactic Notation "refine_seq" constr(dnew) := refine_let dnew.
Tactic Notation "refine_letp" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?id (ownT ?i ?e ?K0 ?dold)] ⇒
first
[ reshape_expr e
ltac:(fun K' e' ⇒
match eval hnf in e' with
Letp ?x0 ?y0 ?e0 ?eb0 ⇒ refine_bind K' at id;
eapply (tac_refine_letp dold dnew);
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _
|| fail "refine_rec: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill; simpl_subst ]
end)
| fail 1 "refine_rec: cannot find 'App' in " e ]
| _ ⇒ fail "refine_rec: no ownT found"
end.
Tactic Notation "refine_delay" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
eapply (tac_refine_delay d0 dnew);
[ try omega | try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; eauto
| ]
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_delay1" :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
refine_delay (d0 - 1)%nat
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_op" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
| BinOp ?op ?l1 ?l2 ⇒
refine_bind K' at j;
eapply (tac_refine_bin_op d0 dnew)
| UnOp ?op ?l1 ⇒
refine_bind K' at j;
eapply (tac_refine_un_op d0 dnew)
end)
| fail 1 "refine_op: cannot find 'BinOp' or 'UnOp' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_cas_suc: non-affine ctxt"
| done || eauto with ndisj
| rewrite /= ?to_of_val; fast_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_op: no ownT found"
end.
Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?id (ownT ?i ?e0 ?K ?d0)] ⇒
first
[reshape_expr e0 ltac:(fun K' e' ⇒
match eval hnf in e' with
chan_lang.Fork ?e'' ⇒ refine_bind K' at id;
eapply tac_refine_fork with d0 dnew H _ _ _ _ _
end)
| fail 1 "refine_fork: cannot find 'Fork' in " e0];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_fork: non-affine ctxt"
| done || eauto with ndisj
| first [ intros t | fail 1 "refine_fork:" t "not fresh" ];
eexists; split;
[ env_cbv ; reflexivity || fail "refine_fork:" H "not fresh"
| rewrite -ownT_fill; simpl ectx_language.fill; rewrite /fresh_delay /= ?to_of_val ]]
| _ ⇒ fail "refine_fork: no ownT found"
end.
Tactic Notation "refine_fork" constr(dnew) ident(t) :=
let H := iFresh in refine_fork dnew t as H.
Ltac refine_stopped :=
lazymatch goal with
| |- context[Esnoc _ _ (ownT ?i ?e0 ?K ?d0)] ⇒
eapply tac_refine_stopped with _ _ e0 _;
[ rewrite /= ?to_of_val; fast_done | iAssumptionCore | apply affine_intro; auto; apply _ ]
end.
Tactic Notation "refine_if_true" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
If _ _ _ ⇒ refine_bind K' at j;
eapply (tac_refine_if_true d0 dnew)
end)
| fail 1 "refine_if_true: cannot find 'If' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_if_true: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_if_true: no ownT found"
end.
Tactic Notation "refine_if_false" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
If _ _ _ ⇒ refine_bind K' at j;
eapply (tac_refine_if_false d0 dnew)
end)
| fail 1 "refine_if_false: cannot find 'If' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_if_true: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_if_false: no ownT found"
end.
Tactic Notation "refine_focus" open_constr(efoc) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
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.
Module Test.
From iris.chan_lang Require Import notation.
From iris.heap_lang Require Import lang notation heap.
Import heap_lang.
Context {Σ : gFunctors}.
Context (Kd: nat).
Context (Fd: nat).
Context `{refineG heap_lang Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{scheapG heap_lang Σ}.
Context `{heap.heapG Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
Local Notation iProp := (iPropG heap_lang Σ).
Definition heap_dummy : heap_lang.expr :=
Skip ;; Skip ;; Skip ;; Skip ;; Skip ;; Skip ;; Skip.
Definition chan_select_case: chan_lang.expr:=
letp: "x" "y" := newch in
let: "x'" := Select "x" lright in
let: "x'" := Select "x'" lleft in
ch_case: "y" with
left ⇒ λ: "_", #true
| right ⇒ λ: "y",
ch_case: "y" with
left ⇒ λ: "y",
ch_case: "y" with
left ⇒ λ: "_", #true
| right ⇒ λ: "_", #true
end
| right ⇒ λ: "_", #true
end
end.
Definition heap_op_test : heap_lang.expr :=
let: "x" := #1 + #1 in
let: "y" := -"x" in
if: "y" < #3 then (if: #3 < "y" then #false else #true) else #false.
Definition chan_op_test : chan_lang.expr :=
let: "x" := #1 + #1 in
let: "y" := -"x" in
if: "y" < #3 then (if: #3 < "y" then #false else #true) else #false.
Definition heap_e2 : heap_lang.expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Definition chan_e2 : chan_lang.expr :=
let: "f" := #1 in
letp: "x" "y" := newch in
letp: "x'" "y'" := newch in
let: "x1" := ("x" <- #2) in
letp: "x" "v" := !"y" in
"v".
Context (HBIG: Kd > 100).
Definition chan_miss : chan_lang.expr :=
letp: "x" "y" := newch in
letp: "y" "v" := !"y" in
"v".
Definition heap_acquire : heap_lang.expr :=
rec: "acquire" "l" :=
if: CAS "l" #false #true then #() else (("acquire": heap_lang.expr) "l")%E.
Definition chan_acquire : chan_lang.expr :=
rec: "acquire" "l" :=
letp: "l'" "v" := !"l" in
if: "v" then "v" else (("acquire": chan_lang.expr) ("l'": chan_lang.expr))%C.
Definition heap_e_rec b: expr :=
let: "x" := ref #true in heap_acquire "x" ;; #b.
Definition chan_e_rec b: chan_lang.expr :=
letp: "x" "y" := newch in chan_acquire "x" ;; #b.
Definition heap_e_fork : heap_lang.expr :=
let: "x" := Fork (#()) in #true.
Definition chan_e_fork : chan_lang.expr :=
(let: "x" := chan_lang.Fork (#true) in #true)%C.
Require Import iris.heap_lang.proofmode.
Lemma chan_case_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i chan_select_case K Kd)
⊢ WP (heap_dummy) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_dummy /chan_select_case.
wp_seq. refine_alloc Kd l'.
wp_value. iPvsIntro. wp_seq.
refine_letp Kd.
wp_seq. refine_select Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd.
wp_seq. refine_select Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd. wp_seq.
refine_rcase_right Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd.
wp_seq. refine_rcase_left Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd. wp_seq.
refine_rcase_miss Kd.
wp_value. iPvsIntro. wp_seq.
refine_rcase_miss Kd.
Abort.
Lemma heap_e2_spec E i K:
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap.heap_ctx ★ scheap_ctx ★ ownT i chan_e2 K Kd)
⊢ WP heap_e2 @ E {{ v, v = #2 ★ ownT i (chan_lang.Lit $ chan_lang.LitInt 2) K 0}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2 /chan_e2.
wp_alloc l.
refine_lam Kd.
wp_let.
refine_alloc Kd cl as "FOO".
wp_alloc l'.
refine_letp Kd.
wp_let.
refine_alloc Kd cl'.
wp_load.
refine_letp Kd.
wp_op.
refine_send Kd.
wp_store.
refine_lam Kd.
wp_seq.
refine_recv Kd.
wp_load.
refine_letp 0%nat.
by iFrame "Hown".
Qed.
Lemma heap_e_rec_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i (chan_e_rec false) K Kd)
⊢ WP (heap_e_rec true) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_rec /chan_e_rec /heap_acquire.
wp_alloc l.
refine_focus (letp: _ _ := _ in _)%C.
refine_focus (newch)%C.
refine_unfocus.
refine_unfocus.
refine_alloc Kd l'.
wp_let. rewrite /chan_acquire. refine_letp Kd.
fold heap_acquire.
wp_focus (heap_acquire _).
wp_rec.
refine_rec Kd.
iLob as "IH".
apply affine_intro; first apply _.
iIntros "! Hpts Hown Hpt".
rewrite affine_later_1.
rewrite /heap_acquire. simpl_subst.
wp_cas_fail.
refine_recv_miss Kd.
wp_if. refine_recv_miss Kd.
wp_rec. refine_recv_miss Kd.
rewrite affine_elim.
iClear "~". iClear "~1".
iSpecialize ("IH" with "Hpts").
iSpecialize ("IH" with "Hown").
iSpecialize ("IH" with "Hpt").
done.
Qed.
Lemma heap_fork_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i chan_e_fork K Kd)
⊢ WP (heap_e_fork) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_fork /chan_e_fork.
wp_apply wp_fork.
refine_fork Kd i' as "HFOO".
iSplitL "Hown".
- wp_let. refine_let 0%nat. wp_value. iFrame "Hown".
iPvsIntro. done.
- wp_value. iPvsIntro. refine_stopped.
Qed.
Lemma heap_op_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i chan_op_test K Kd)
⊢ WP (heap_op_test) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_op_test /chan_op_test.
wp_op. refine_op Kd.
wp_let. refine_let Kd.
wp_op. refine_op Kd.
wp_let. refine_let Kd.
wp_op; intros. refine_op Kd.
wp_if. refine_if_true Kd.
wp_op; intros; first (exfalso; eauto with *; idtac) .
refine_op Kd.
wp_if.
refine_if_false Kd.
Abort.
Lemma heap_e2_spec' E i K:
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap.heap_ctx ★ scheap_ctx ★ ownT i chan_miss K Kd)
⊢ WP heap_e2 @ E {{ v, v = #2 ★ ownT i (chan_lang.Lit $ chan_lang.LitInt 2) K 0}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2 /chan_miss.
wp_alloc l.
refine_alloc Kd cl as "FOO".
wp_let. refine_letp Kd.
wp_alloc l'. refine_recv_miss Kd.
Abort.
End Test.
From iris.proofmode Require Export weakestpre.
From iris.algebra Require Export upred_tactics.
From iris.chan_lang Require Export tactics refine_heap.
Import uPred.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{scheapG Λ Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types Δ : envs (iResUR Λ (globalF Σ)).
Context (d: nat).
Context (d': nat).
Context (Hd_le: (d ≤ Kd)%nat).
Context (Hd'_le: (d' ≤ Kd)%nat).
Lemma tac_refine_alloc Δ E i k j t K P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Alloc) K d) →
(envs_delete k false Δ ⊢ ⧆ (envs_delete k false Δ)) →
nclose scheapN ⊆ E →
(∀ l, ∃ Δ',
envs_simple_replace k false (Esnoc (Esnoc Enil j (l ↦c ([], []))) k
(ownT t (Pair (Lit (LitLoc l cleft))
(Lit (LitLoc l cright))) K d')) Δ
= Some Δ' ∧ (Δ' ⊢ P)) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite relevant_elim assoc (refine_alloc _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite sep_exist_r.
apply exist_elim⇒l. edestruct (HΔ l) as (Δ'&Heq&Himpl).
rewrite -Himpl affine_elim (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite (comm _ (ownT t _ _ _)).
by apply wand_elim_r.
Qed.
Lemma tac_refine_recv k t Δ Δ' Δ'' E i j K l side v l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Recv (Lit (LitLoc l side))) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, v :: l2))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c (v :: l1, l2))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c (l1, l2))) k
(ownT t (Pair (Lit (LitLoc l side)) (of_val v)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_recv_miss k t Δ Δ' Δ'' E i j K l side l1 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Recv (Lit (LitLoc l side))) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, []))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c ([], l1))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c
match side with
|cleft ⇒ (l1, [])
|cright ⇒ ([], l1)
end)) k
(ownT t (Recv (Lit (LitLoc l side))) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_miss_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_recv_miss_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_send k t e Δ Δ' Δ'' E i j K l side v' l1 l2 P :
to_val e = Some v' →
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Send (Lit (LitLoc l side)) e) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦c (l1, l2))%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c match side with
| cleft ⇒ (l1 ++ [v'], l2)
| cright ⇒ (l1, l2 ++ [v'])
end)) k
(ownT t (Lit (LitLoc l side)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros ? Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
destruct side.
- rewrite (refine_send_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite (refine_send_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_select k t Δ Δ' Δ'' E i j K l side choice l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Select (Lit (LitLoc l side)) choice) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦c (l1, l2))%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c match side with
| cleft ⇒ (l1 ++ [label_to_sum choice], l2)
| cright ⇒ (l1, l2 ++ [label_to_sum choice])
end)) k
(ownT t (Lit (LitLoc l side)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
destruct side.
- rewrite (refine_select_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite (refine_select_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rcase_left k t Δ Δ' Δ'' E i j K l side e1 e2 l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, InjLV (LitV LitUnit) :: l2))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c (InjLV (LitV LitUnit) :: l1, l2))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c (l1, l2))) k
(ownT t (App e1 (Lit (LitLoc l side))) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_left_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_right_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rcase_right k t Δ Δ' Δ'' E i j K l side e1 e2 l1 l2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, InjRV (LitV LitUnit) :: l2))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c (InjRV (LitV LitUnit) :: l1, l2))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c (l1, l2))) k
(ownT t (App e2 (Lit (LitLoc l side))) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_left_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_right_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rcase_miss k t Δ Δ' Δ'' E i j K l side e1 e2 l1 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d, Δ' ) →
match side with
| cleft ⇒ envs_lookup j Δ' = Some (false, l ↦c (l1, []))%I
| cright ⇒ envs_lookup j Δ' = Some (false, l ↦c ([], l1))%I
end →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose scheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦c
match side with
|cleft ⇒ (l1, [])
|cright ⇒ ([], l1)
end)) k
(ownT t (RCase (Lit (LitLoc l side)) e1 e2) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Hl3 Haff ? HΔ1 HΔ2.
destruct side.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_miss_left _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
- rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_delete_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc assoc -(assoc _ _ (ownT _ _ _ _)) .
rewrite relevant_elim.
rewrite (refine_rcase_miss_right _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim. rewrite -assoc.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite assoc.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_pure Δ Δ' E i k t K e e' P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
((scheap_ctx ★ ownT t e K d) ⊢ |={E}=>> ownT t e' K d') →
envs_simple_replace k false (Esnoc Enil k (ownT t e' K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Haff ? Hstep HΔ1 HΔ2.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite assoc.
rewrite relevant_elim.
rewrite Hstep.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite affine_elim.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id.
rewrite -HΔ2. by apply wand_elim_r.
Qed.
Lemma tac_refine_rec Δ Δ' E i k t K f x erec e2 v2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (App (Rec f x erec) e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e2 = Some v2 →
Closed (f :b: x :b: []) erec →
envs_simple_replace k false
(Esnoc Enil k (ownT t (subst' x e2 (subst' f (Rec f x erec) erec)) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_rec; eauto. Qed.
Lemma tac_refine_letp Δ Δ' E i k t K x y e1 e2 eb v1 v2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Letp x y (Pair e1 e2) eb) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e1 = Some v1 →
to_val e2 = Some v2 →
Closed (x :b: y :b: []) eb →
envs_simple_replace k false
(Esnoc Enil k (ownT t (subst' y e2 (subst' x e1 eb)) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_letp; eauto. Qed.
Lemma tac_refine_lam Δ Δ' E i k t K x ef e v P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (App (Lam x ef) e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e = Some v →
Closed (x :b: []) ef →
envs_simple_replace k false (Esnoc Enil k (ownT t (subst' x e ef) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto using refine_lam. Qed.
Lemma tac_refine_bin_op Δ Δ' E i k t K op l1 l2 l' P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (BinOp op (Lit l1) (Lit l2)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
bin_op_eval op l1 l2 = Some l' →
envs_simple_replace k false (Esnoc Enil k (ownT t (Lit l') K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_bin_op; eauto. Qed.
Lemma tac_refine_un_op Δ Δ' E i k t K op l l' P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (UnOp op (Lit l)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
un_op_eval op l = Some l' →
envs_simple_replace k false (Esnoc Enil k (ownT t (Lit l') K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_un_op; eauto. Qed.
Lemma tac_refine_if_true Δ Δ' E i k t K e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (If (Lit (LitBool true)) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
envs_simple_replace k false (Esnoc Enil k (ownT t e1 K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_if_true; eauto. Qed.
Lemma tac_refine_if_false Δ Δ' E i k t K e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (If (Lit (LitBool false)) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
envs_simple_replace k false (Esnoc Enil k (ownT t e2 K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_if_false; eauto. Qed.
Lemma tac_refine_case_inl Δ Δ' E i k t K e0 v0 e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjL e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e0 = Some v0 →
envs_simple_replace k false (Esnoc Enil k (ownT t (App e1 e0) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_case_inl; eauto. Qed.
Lemma tac_refine_case_inr Δ Δ' E i k t K e0 v0 e1 e2 P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjR e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
to_val e0 = Some v0 →
envs_simple_replace k false (Esnoc Enil k (ownT t (App e2 e0) K d')) Δ
= Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof. intros; eapply tac_refine_pure; eauto. eapply refine_case_inr; eauto. Qed.
Lemma tac_refine_fork j Δ E i k t K e P :
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Fork e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
(∀ t', ∃ Δ',
envs_simple_replace k false (Esnoc (Esnoc Enil j (ownT t' e empty_ectx (fresh_delay _ Fd e)))
k (ownT t (Lit LitUnit) K d')) Δ
= Some Δ' ∧
(Δ' ⊢ P)) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hl1 Hl2 Haff ? HΔ.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite relevant_elim assoc (refine_fork _ d' _ _ E) //.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite sep_exist_r.
apply exist_elim⇒t'. edestruct (HΔ t') as (Δ'&Heq&Himpl).
rewrite -Himpl affine_elim (envs_simple_replace_sound' _ _ _ false) //; eauto.
simpl. rewrite right_id. rewrite (comm _ (ownT t _ _ _)).
by apply wand_elim_r.
Qed.
Lemma tac_refine_stopped Δ k t e v :
to_val e = Some v →
envs_lookup k Δ = Some (false, ownT t e empty_ectx 0) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
Δ ⊢ uPred_stopped.
Proof.
intros Hval Hl1 Haff.
rewrite envs_lookup_sound //=; simpl.
rewrite Haff. rewrite -(of_to_val e v); eauto.
rewrite ownT_val_stopped. auto.
Qed.
Lemma tac_refine_delay Δ E Δ' i k t e K P:
(d > d')%nat →
envs_lookup i Δ = Some (true, scheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose scheapN ⊆ E →
envs_simple_replace k false (Esnoc Enil k (ownT t e K d')) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros Hgt Hl1 Hl2 Haff ? Hrep Hd.
rewrite envs_lookup_relevant_sound //=; simpl.
rewrite envs_lookup_sound //=; simpl.
rewrite relevant_elim assoc.
rewrite (refine_delay _ d' _ _ E); eauto.
rewrite Haff psvs_frame_r.
apply psvs_mono.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
rewrite affine_elim.
simpl. rewrite right_id.
rewrite -Hd. by apply wand_elim_r.
Qed.
Lemma tac_refine_bind Δ Δ' k t e K K' P :
envs_lookup k Δ = Some (false, ownT t (fill K' e) K d) →
envs_simple_replace k false (Esnoc Enil k (ownT t e (comp_ectx K K') d)) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
by rewrite ownT_focus //= ?right_id 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') d) →
envs_simple_replace k false (Esnoc Enil k (ownT t (fill K' e) K d)) Δ = Some Δ' →
(Δ' ⊢ P) →
Δ ⊢ P.
Proof.
intros Hl1 Hrep Hd.
rewrite envs_lookup_sound //=; simpl.
rewrite (envs_simple_replace_sound' _ _ _ false) //; eauto.
by rewrite -ownT_fill //= ?right_id wand_elim_r.
Qed.
End heap.
Tactic Notation "refine_bind" constr(K) "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply (tac_refine_bind _ _ _ j _ _ _ K);
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_bind" constr(K) :=
lazymatch eval hnf in K with
| _ ⇒
eapply (tac_refine_bind _ _ _ _ _ _ _ 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 _ _ _ j _ _ _ K);
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_unbind" constr(K) constr(K') "at" constr(j) :=
lazymatch eval hnf in K with
| _ ⇒
eapply (tac_refine_unbind _ _ _ j _ _ K 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 _ _ _ _ _ _ _ K);
first (fast_by iAssumptionCore);
[ env_cbv; reflexivity | ]
end.
Tactic Notation "refine_alloc" constr(dnew) ident(l) "as" constr(H) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?id (ownT ?i ?e ?K ?dold)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Alloc ⇒ refine_bind K' at id;
eapply tac_refine_alloc with dold dnew _ _ H _ _
end)
| fail 1 "refine_alloc: cannot find 'Alloc' in " e];
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_alloc: non-affine ctxt"
| done || eauto with ndisj
| first [ intros l | fail 1 "refine_alloc:" l "not fresh" ];
eexists; split;
[ env_cbv ; reflexivity || fail "refine_allc:" H "not fresh"
| rewrite -ownT_fill; simpl ectx_language.fill ]]
| _ ⇒ fail "refine_alloc: no ownT found"
end.
Tactic Notation "refine_alloc" constr(dnew) ident(l) :=
let H := iFresh in refine_alloc dnew l as H.
Tactic Notation "refine_recv" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Recv ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_recv with d0 dnew j i _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_recv_miss" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Recv ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_recv_miss with d0 dnew j i _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_send" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e0 ?K ?d0)] ⇒
first
[ reshape_expr e0 ltac:(fun K' e' ⇒
match eval hnf in e' with
Send ?el ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_send with d0 dnew j i e'' _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_send: cannot find 'Send' in " e0 ];
[ try omega | try omega | wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_send: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_send: no ownT found"
end.
Tactic Notation "refine_select" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e0 ?K ?d0)] ⇒
first
[ reshape_expr e0 ltac:(fun K' e' ⇒
match eval hnf in e' with
Select ?el ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_select with d0 dnew j i _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_select: cannot find 'Select' in " e0 ];
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_select: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_select: no ownT found"
end.
Tactic Notation "refine_rcase_left" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
RCase _ _ _ ⇒ refine_bind K' at j;
eapply tac_refine_rcase_left with d0 dnew j i
_ _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_rcase_right" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
RCase _ _ _ ⇒ refine_bind K' at j;
eapply tac_refine_rcase_right with d0 dnew j i
_ _ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_rcase_miss" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
RCase _ _ _ ⇒ refine_bind K' at j;
eapply tac_refine_rcase_miss with d0 dnew j i
_ _ _ _ _ _ _ _ _ _
end)
| fail 1 "refine_recv: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| env_cbv; eauto
| case cleft; iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_recv: no ownT found"
end.
Tactic Notation "refine_rec" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e
ltac:(fun K' e' ⇒
match eval hnf in e' with
chan_lang.App ?e1 _ ⇒ refine_bind K' at j;
eapply (tac_refine_rec d0 dnew);
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _
|| fail "refine_lam: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill; simpl_subst ]
end)
| fail 1 "refine_lam: cannot find 'App' in " e ]
| _ ⇒ fail "refine_lam: no ownT found"
end.
Tactic Notation "refine_lam" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e
ltac:(fun K' e' ⇒
match eval hnf in e' with
App ?e1 _ ⇒ refine_bind K' at j;
eapply (tac_refine_lam d0 dnew);
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _
|| fail "refine_lam: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill; simpl_subst ]
end)
| fail 1 "refine_lam: cannot find 'App' in " e ]
| _ ⇒ fail "refine_lam: no ownT found"
end.
Tactic Notation "refine_let" constr(dnew) := refine_lam dnew.
Tactic Notation "refine_seq" constr(dnew) := refine_let dnew.
Tactic Notation "refine_letp" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?id (ownT ?i ?e ?K0 ?dold)] ⇒
first
[ reshape_expr e
ltac:(fun K' e' ⇒
match eval hnf in e' with
Letp ?x0 ?y0 ?e0 ?eb0 ⇒ refine_bind K' at id;
eapply (tac_refine_letp dold dnew);
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _
|| fail "refine_rec: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill; simpl_subst ]
end)
| fail 1 "refine_rec: cannot find 'App' in " e ]
| _ ⇒ fail "refine_rec: no ownT found"
end.
Tactic Notation "refine_delay" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
eapply (tac_refine_delay d0 dnew);
[ try omega | try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_load: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; eauto
| ]
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_delay1" :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
refine_delay (d0 - 1)%nat
| _ ⇒ fail "refine_focus: could not find ownT"
end.
Tactic Notation "refine_op" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[ reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
| BinOp ?op ?l1 ?l2 ⇒
refine_bind K' at j;
eapply (tac_refine_bin_op d0 dnew)
| UnOp ?op ?l1 ⇒
refine_bind K' at j;
eapply (tac_refine_un_op d0 dnew)
end)
| fail 1 "refine_op: cannot find 'BinOp' or 'UnOp' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_cas_suc: non-affine ctxt"
| done || eauto with ndisj
| rewrite /= ?to_of_val; fast_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_op: no ownT found"
end.
Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?id (ownT ?i ?e0 ?K ?d0)] ⇒
first
[reshape_expr e0 ltac:(fun K' e' ⇒
match eval hnf in e' with
chan_lang.Fork ?e'' ⇒ refine_bind K' at id;
eapply tac_refine_fork with d0 dnew H _ _ _ _ _
end)
| fail 1 "refine_fork: cannot find 'Fork' in " e0];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_fork: non-affine ctxt"
| done || eauto with ndisj
| first [ intros t | fail 1 "refine_fork:" t "not fresh" ];
eexists; split;
[ env_cbv ; reflexivity || fail "refine_fork:" H "not fresh"
| rewrite -ownT_fill; simpl ectx_language.fill; rewrite /fresh_delay /= ?to_of_val ]]
| _ ⇒ fail "refine_fork: no ownT found"
end.
Tactic Notation "refine_fork" constr(dnew) ident(t) :=
let H := iFresh in refine_fork dnew t as H.
Ltac refine_stopped :=
lazymatch goal with
| |- context[Esnoc _ _ (ownT ?i ?e0 ?K ?d0)] ⇒
eapply tac_refine_stopped with _ _ e0 _;
[ rewrite /= ?to_of_val; fast_done | iAssumptionCore | apply affine_intro; auto; apply _ ]
end.
Tactic Notation "refine_if_true" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
If _ _ _ ⇒ refine_bind K' at j;
eapply (tac_refine_if_true d0 dnew)
end)
| fail 1 "refine_if_true: cannot find 'If' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_if_true: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_if_true: no ownT found"
end.
Tactic Notation "refine_if_false" constr(dnew) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
If _ _ _ ⇒ refine_bind K' at j;
eapply (tac_refine_if_false d0 dnew)
end)
| fail 1 "refine_if_false: cannot find 'If' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_if_true: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_if_false: no ownT found"
end.
Tactic Notation "refine_focus" open_constr(efoc) :=
lazymatch goal with
| |- context[Esnoc ?Δ ?j (ownT ?i ?e ?K ?d0)] ⇒
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.
Module Test.
From iris.chan_lang Require Import notation.
From iris.heap_lang Require Import lang notation heap.
Import heap_lang.
Context {Σ : gFunctors}.
Context (Kd: nat).
Context (Fd: nat).
Context `{refineG heap_lang Σ (delayed_lang (chan_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{scheapG heap_lang Σ}.
Context `{heap.heapG Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val → iPropG heap_lang Σ.
Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
Local Notation iProp := (iPropG heap_lang Σ).
Definition heap_dummy : heap_lang.expr :=
Skip ;; Skip ;; Skip ;; Skip ;; Skip ;; Skip ;; Skip.
Definition chan_select_case: chan_lang.expr:=
letp: "x" "y" := newch in
let: "x'" := Select "x" lright in
let: "x'" := Select "x'" lleft in
ch_case: "y" with
left ⇒ λ: "_", #true
| right ⇒ λ: "y",
ch_case: "y" with
left ⇒ λ: "y",
ch_case: "y" with
left ⇒ λ: "_", #true
| right ⇒ λ: "_", #true
end
| right ⇒ λ: "_", #true
end
end.
Definition heap_op_test : heap_lang.expr :=
let: "x" := #1 + #1 in
let: "y" := -"x" in
if: "y" < #3 then (if: #3 < "y" then #false else #true) else #false.
Definition chan_op_test : chan_lang.expr :=
let: "x" := #1 + #1 in
let: "y" := -"x" in
if: "y" < #3 then (if: #3 < "y" then #false else #true) else #false.
Definition heap_e2 : heap_lang.expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Definition chan_e2 : chan_lang.expr :=
let: "f" := #1 in
letp: "x" "y" := newch in
letp: "x'" "y'" := newch in
let: "x1" := ("x" <- #2) in
letp: "x" "v" := !"y" in
"v".
Context (HBIG: Kd > 100).
Definition chan_miss : chan_lang.expr :=
letp: "x" "y" := newch in
letp: "y" "v" := !"y" in
"v".
Definition heap_acquire : heap_lang.expr :=
rec: "acquire" "l" :=
if: CAS "l" #false #true then #() else (("acquire": heap_lang.expr) "l")%E.
Definition chan_acquire : chan_lang.expr :=
rec: "acquire" "l" :=
letp: "l'" "v" := !"l" in
if: "v" then "v" else (("acquire": chan_lang.expr) ("l'": chan_lang.expr))%C.
Definition heap_e_rec b: expr :=
let: "x" := ref #true in heap_acquire "x" ;; #b.
Definition chan_e_rec b: chan_lang.expr :=
letp: "x" "y" := newch in chan_acquire "x" ;; #b.
Definition heap_e_fork : heap_lang.expr :=
let: "x" := Fork (#()) in #true.
Definition chan_e_fork : chan_lang.expr :=
(let: "x" := chan_lang.Fork (#true) in #true)%C.
Require Import iris.heap_lang.proofmode.
Lemma chan_case_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i chan_select_case K Kd)
⊢ WP (heap_dummy) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_dummy /chan_select_case.
wp_seq. refine_alloc Kd l'.
wp_value. iPvsIntro. wp_seq.
refine_letp Kd.
wp_seq. refine_select Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd.
wp_seq. refine_select Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd. wp_seq.
refine_rcase_right Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd.
wp_seq. refine_rcase_left Kd.
wp_value. iPvsIntro. wp_seq.
refine_let Kd. wp_seq.
refine_rcase_miss Kd.
wp_value. iPvsIntro. wp_seq.
refine_rcase_miss Kd.
Abort.
Lemma heap_e2_spec E i K:
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap.heap_ctx ★ scheap_ctx ★ ownT i chan_e2 K Kd)
⊢ WP heap_e2 @ E {{ v, v = #2 ★ ownT i (chan_lang.Lit $ chan_lang.LitInt 2) K 0}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2 /chan_e2.
wp_alloc l.
refine_lam Kd.
wp_let.
refine_alloc Kd cl as "FOO".
wp_alloc l'.
refine_letp Kd.
wp_let.
refine_alloc Kd cl'.
wp_load.
refine_letp Kd.
wp_op.
refine_send Kd.
wp_store.
refine_lam Kd.
wp_seq.
refine_recv Kd.
wp_load.
refine_letp 0%nat.
by iFrame "Hown".
Qed.
Lemma heap_e_rec_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i (chan_e_rec false) K Kd)
⊢ WP (heap_e_rec true) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_rec /chan_e_rec /heap_acquire.
wp_alloc l.
refine_focus (letp: _ _ := _ in _)%C.
refine_focus (newch)%C.
refine_unfocus.
refine_unfocus.
refine_alloc Kd l'.
wp_let. rewrite /chan_acquire. refine_letp Kd.
fold heap_acquire.
wp_focus (heap_acquire _).
wp_rec.
refine_rec Kd.
iLob as "IH".
apply affine_intro; first apply _.
iIntros "! Hpts Hown Hpt".
rewrite affine_later_1.
rewrite /heap_acquire. simpl_subst.
wp_cas_fail.
refine_recv_miss Kd.
wp_if. refine_recv_miss Kd.
wp_rec. refine_recv_miss Kd.
rewrite affine_elim.
iClear "~". iClear "~1".
iSpecialize ("IH" with "Hpts").
iSpecialize ("IH" with "Hown").
iSpecialize ("IH" with "Hpt").
done.
Qed.
Lemma heap_fork_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i chan_e_fork K Kd)
⊢ WP (heap_e_fork) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_fork /chan_e_fork.
wp_apply wp_fork.
refine_fork Kd i' as "HFOO".
iSplitL "Hown".
- wp_let. refine_let 0%nat. wp_value. iFrame "Hown".
iPvsIntro. done.
- wp_value. iPvsIntro. refine_stopped.
Qed.
Lemma heap_op_spec E K i :
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap_ctx ★ scheap_ctx ★ ownT i chan_op_test K Kd)
⊢ WP (heap_op_test) @ E {{ v, v = #true ★ ownT i (#true)%C K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_op_test /chan_op_test.
wp_op. refine_op Kd.
wp_let. refine_let Kd.
wp_op. refine_op Kd.
wp_let. refine_let Kd.
wp_op; intros. refine_op Kd.
wp_if. refine_if_true Kd.
wp_op; intros; first (exfalso; eauto with *; idtac) .
refine_op Kd.
wp_if.
refine_if_false Kd.
Abort.
Lemma heap_e2_spec' E i K:
nclose heapN ⊆ E →
nclose scheapN ⊆ E →
(heap.heap_ctx ★ scheap_ctx ★ ownT i chan_miss K Kd)
⊢ WP heap_e2 @ E {{ v, v = #2 ★ ownT i (chan_lang.Lit $ chan_lang.LitInt 2) K 0}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2 /chan_miss.
wp_alloc l.
refine_alloc Kd cl as "FOO".
wp_let. refine_letp Kd.
wp_alloc l'. refine_recv_miss Kd.
Abort.
End Test.