Library iris.heap_lang.refine_proofmode
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap refine_heap proofmode notation.
Import uPred.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{sheapG Λ Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types Δ : envs (iResUR Λ (globalF Σ)).
Global Instance into_sep_smapsto l q v :
IntoSep false (l ↦s{q} v) (l ↦s{q/2} v) (l ↦s{q/2} v).
Proof. by rewrite /IntoSep sheap_mapsto_op_split. Qed.
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 e v P :
to_val e = Some v →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Alloc e) K d) →
(envs_delete k false Δ ⊢ ⧆ (envs_delete k false Δ)) →
nclose sheapN ⊆ E →
(∀ l, ∃ Δ',
envs_simple_replace k false (Esnoc (Esnoc Enil j (l ↦s v)) k (ownT t (Lit (LitLoc l)) 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_load Δ Δ' Δ'' E i k j t K l v q P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Load (Lit (LitLoc l))) K d, Δ' ) →
envs_lookup j Δ' = Some (false, l ↦s{q} v)%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s{q} v)) k (ownT t (of_val v) 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.
rewrite (refine_load _ 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_store Δ Δ' Δ'' E i k j t K l v e v' P :
to_val e = Some v' →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Store (Lit (LitLoc l)) e) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s v)%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s v')) k (ownT t (Lit LitUnit) 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.
rewrite (refine_store _ 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_cas_fail Δ Δ' Δ'' E i k j t K l q v e1 v1 e2 v2 P :
to_val e1 = Some v1 → to_val e2 = Some v2 →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (CAS (Lit (LitLoc l)) e1 e2) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s{q} v)%I →
v ≠ v1 →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s{q} v)) k
(ownT t (Lit (LitBool false)) 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.
rewrite (refine_cas_fail _ 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_cas_suc Δ Δ' Δ'' E i k j t K l v e1 v1 e2 v2 P :
to_val e1 = Some v1 → to_val e2 = Some v2 →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (CAS (Lit (LitLoc l)) e1 e2) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s v)%I →
v = v1 →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s v2)) k
(ownT t (Lit (LitBool true)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros ?? Hl1 Hl2 Hl3 ? Haff ? HΔ1 HΔ2. subst.
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_cas_suc _ 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_swap Δ Δ' Δ'' E i k j t K l v e v' P :
to_val e = Some v' →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Swap (Lit (LitLoc l)) e) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s v)%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s v')) k (ownT t (of_val v) 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.
rewrite (refine_swap _ 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_fai Δ Δ' Δ'' E i k j t K l k' P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (FAI (Lit (LitLoc l))) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s (LitV $ LitInt k'))%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s (LitV $ LitInt (k'+1))))
k (ownT t (Lit $ LitInt k') 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.
rewrite (refine_fai _ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ E →
((sheap_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, sheap_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 sheapN ⊆ 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_lam Δ Δ' E i k t K x ef e v P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (App (Lam x ef) e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_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 sheapN ⊆ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (UnOp op (Lit l)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_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 sheapN ⊆ 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, sheap_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 sheapN ⊆ 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_fst Δ Δ' E i k t K e1 v1 e2 v2 P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Fst (Pair e1 e2)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ E →
to_val e1 = Some v1 → to_val e2 = Some v2 →
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_fst; eauto. Qed.
Lemma tac_refine_snd Δ Δ' E i k t K e1 v1 e2 v2 P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Snd (Pair e1 e2)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ E →
to_val e1 = Some v1 → to_val e2 = Some v2 →
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_snd; eauto. Qed.
Lemma tac_refine_case_inl Δ Δ' E i k t K e0 v0 e1 e2 P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjL e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjR e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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 Δ E i k j t K e P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Fork e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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 ?Δ ?j (ownT ?i ?e ?K ?dold)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Alloc ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_alloc with dold dnew _ _ H i _ e'' _
end)
| fail 1 "refine_alloc: cannot find 'Alloc' in " e];
[ try omega | try omega
| wp_done
| 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_load" 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
Load ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_load with d0 dnew _ _ _ _ _ i _ _ _ _
end)
| fail 1 "refine_load: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| 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_load: no ownT found"
end.
Tactic Notation "refine_store" 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
Store ?e'' ?e''' ⇒ refine_bind K' at j;
eapply tac_refine_store with d0 dnew _ _ _ _ _ i _ _ _ e''' _
end)
| fail 1 "refine_store: cannot find 'Store' in " e ];
[ try omega | try omega | wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_store: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_store: no ownT found"
end.
Tactic Notation "refine_cas_fail" 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
CAS ?e'' ?e''' ?e'''' ⇒
refine_bind K' at j;
eapply tac_refine_cas_fail with
d0 dnew _ _ _ _ _ i _ _ _ _ e''' _ e'''' _
end)
| fail 1 "refine_cas_fail: cannot find 'CAS' in " e ];
[ try omega | try omega
| wp_done
| wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| try congruence
| apply affine_intro; auto; apply _ || fail "refine_cas_fail: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_cas_fail: no ownT found"
end.
Tactic Notation "refine_cas_suc" 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
CAS ?e'' ?e''' ?e'''' ⇒
refine_bind K' at j;
eapply tac_refine_cas_suc with
d0 dnew _ _ _ _ _ i _ _ _ e''' _ e'''' _
end)
| fail 1 "refine_cas_suc: cannot find 'CAS' in " e ];
[ try omega | try omega
| wp_done
| wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| try congruence
| apply affine_intro; auto; apply _ || fail "refine_cas_suc: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_cas_suc: no ownT found"
end.
Tactic Notation "refine_swap" 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
Swap ?e'' ?e''' ⇒ refine_bind K' at j;
eapply tac_refine_swap with d0 dnew _ _ _ _ _ i _ _ _ e''' _
end)
| fail 1 "refine_store: cannot find 'Store' in " e ];
[ try omega | try omega | wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_store: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_store: no ownT found"
end.
Tactic Notation "refine_fai" 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
FAI ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_fai with d0 dnew _ _ _ _ _ i _ _ _
end)
| fail 1 "refine_store: cannot find 'FAI' in " e ];
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_store: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_store: 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
App ?e1 ?e2 ⇒ refine_bind K' at j;
eapply tac_refine_rec with d0 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
| fast_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_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 with d0 dnew _ _ _ _ (comp_ectx K K') _ _ _ _;
[ 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_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
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_op: no ownT found"
end.
Tactic Notation "refine_proj" 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
| Fst _ ⇒
refine_bind K' at j;
eapply (tac_refine_fst d0 dnew)
| Snd _ ⇒
refine_bind K' at j;
eapply (tac_refine_snd d0 dnew)
end)
| fail 1 "refine_proj: cannot find 'Fst' or 'Snd' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_proj: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_proj: no ownT found"
end.
Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
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
Fork ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_fork with d0 dnew _ _ H i _ e''
end)
| fail 1 "refine_fork: cannot find 'Fork' in " e];
[ 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 ]]
| _ ⇒ 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 ?e ?K ?d0)] ⇒
eapply tac_refine_stopped with _ i e _;
[ wp_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 with 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 with 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 ⇒ 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 "wp_focus: not a 'wp'"
end.
Section Test.
Context {Σ : gFunctors}.
Context (Kd: nat).
Context (Fd: nat).
Context `{refineG heap_lang Σ (delayed_lang (heap_lang) Kd Kd) (S Kd × (Kd + 3))}.
Context `{heapG Σ}.
Context `{sheapG heap_lang Σ}.
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 Σ).
Context (HBIG: Kd > 100).
Definition heap_proj : expr :=
let: "x" := Fst (Snd (#1, (#2, #3))) in
"x".
Lemma heap_proj_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_proj K Kd)
⊢ WP heap_proj @ E {{ v, v = #2 ★ ownT i (of_val (#2)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_proj.
wp_proj. refine_focus (Snd _)%E; refine_proj Kd; refine_unfocus.
wp_proj. refine_proj Kd.
wp_let. refine_let O.
wp_value. iPvsIntro.
iFrame; done.
Qed.
Definition heap_swap : expr :=
let: "x" := ref #1 in
let: "z" := Swap "x" #2 in
"z".
Lemma heap_swap_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_swap K Kd)
⊢ WP heap_swap @ E {{ v, v = #1 ★ ownT i (of_val (#1)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_swap.
wp_alloc l1. refine_alloc Kd l1'.
wp_let. refine_let Kd.
wp_swap. refine_swap Kd.
wp_let. refine_let O.
wp_value. iPvsIntro.
iFrame; done.
Qed.
Definition heap_fai : expr :=
let: "x" := ref #1 in
let: "z" := FAI "x" in
"z".
Lemma heap_fai_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_fai K Kd)
⊢ WP heap_fai @ E {{ v, v = #1 ★ ownT i (of_val (#1)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_fai.
wp_alloc l1. refine_alloc Kd l1'.
wp_let. refine_let Kd.
wp_fai. refine_fai Kd.
wp_let. refine_let O.
wp_value. iPvsIntro.
iFrame; done.
Qed.
Definition heap_e2 : expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e2 K Kd)
⊢ WP heap_e2 @ E {{ v, v = #2 ★ ownT i (of_val (#2)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2.
wp_alloc l1. refine_alloc Kd l1'.
wp_let. refine_let Kd.
wp_alloc l2. refine_alloc Kd l2'.
wp_let. refine_let Kd.
wp_load. refine_load Kd.
wp_op. refine_op Kd.
wp_store. refine_store Kd.
wp_seq. refine_seq Kd.
wp_load. refine_load 0%nat.
by iFrame "Hown".
Qed.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;;
"x" <- - !"x" ;;
CAS "x" #2 #4 ;;
CAS "x" #(-2) #3.
Lemma heap_e_spec E P i K :
nclose sheapN ⊆ E →
nclose heapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e K Kd)
⊢ WP heap_e @ E {{ v, v = #true ★ ownT i (of_val (#true)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e.
wp_alloc l.
refine_alloc Kd l'.
wp_let.
refine_let Kd.
wp_load.
refine_focus (! (#_))%E.
refine_load Kd. simpl.
refine_unfocus.
refine_unfocus.
refine_bind K.
wp_op.
refine_op Kd.
wp_store.
refine_store Kd.
wp_let.
refine_let Kd.
wp_load.
refine_load Kd.
wp_op.
refine_op Kd.
wp_store.
refine_store Kd.
wp_seq.
refine_seq Kd.
wp_cas_fail; auto.
refine_cas_fail Kd; auto.
wp_seq.
refine_seq Kd.
wp_cas_suc; auto.
refine_cas_suc 0%nat; auto.
iFrame "Hown". auto.
Qed.
Definition heap_e_fork : expr :=
let: "x" := ref #1 in Fork ("x" <- !"x" + #1) ;; #2.
Lemma heap_e_fork_spec E K N N' i :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e_fork K Kd)
⊢ WP heap_e_fork @ E {{ v, (v = #2 ∨ v = #1) ★ ownT i (of_val (v)) K Kd}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_fork.
wp_alloc l. refine_alloc Kd l'.
wp_let. refine_let (Kd-1)%nat.
wp_apply wp_fork.
refine_fork Kd i' as "Hown'".
iSplitL "Hown".
- wp_seq. refine_seq (Kd)%nat. wp_value. iPvsIntro.
iFrame "Hown". iClear "~". iClear "~1". iLeft. auto.
- wp_load. refine_load (Kd -1)%nat.
rewrite /fresh_delay //=.
wp_op. refine_op Kd.
wp_store. refine_store 0%nat.
refine_stopped.
Qed.
Definition acquire : expr :=
rec: "acquire" "l" :=
if: CAS "l" #false #true then #() else "acquire" "l".
Definition heap_e_rec b: expr :=
let: "x" := ref #true in acquire "x" ;; #b.
Lemma heap_e_rec_spec E K i :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i (heap_e_rec false) K Kd)
⊢ WP (heap_e_rec true) @ E {{ v, v = #true ★ ownT i (of_val (v)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_rec /acquire.
wp_alloc l. refine_alloc Kd l'.
wp_let. refine_let Kd.
wp_focus ((rec: "acquire" "l" := if: CAS "l" #false #true then #() else "acquire" "l") (#l)%E)%E.
iLob as "IH".
apply affine_intro; first apply _.
iIntros "! Hpts Hown Hpt".
rewrite affine_later_1.
wp_rec. refine_rec Kd.
wp_cas_fail. refine_cas_fail Kd.
wp_if. refine_if_false Kd.
rewrite affine_elim.
iClear "~". iClear "~1".
by iApply ("IH" with "Hpts Hown").
Qed.
End Test.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap refine_heap proofmode notation.
Import uPred.
Section heap.
Context {Σ : gFunctors}.
Context `{refineG Λ Σ (delayed_lang (heap_lang) Kd Fd) (S Kd × (Kd + 3))}.
Context `{sheapG Λ Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types Φ : val → iPropG Λ Σ.
Implicit Types Δ : envs (iResUR Λ (globalF Σ)).
Global Instance into_sep_smapsto l q v :
IntoSep false (l ↦s{q} v) (l ↦s{q/2} v) (l ↦s{q/2} v).
Proof. by rewrite /IntoSep sheap_mapsto_op_split. Qed.
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 e v P :
to_val e = Some v →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Alloc e) K d) →
(envs_delete k false Δ ⊢ ⧆ (envs_delete k false Δ)) →
nclose sheapN ⊆ E →
(∀ l, ∃ Δ',
envs_simple_replace k false (Esnoc (Esnoc Enil j (l ↦s v)) k (ownT t (Lit (LitLoc l)) 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_load Δ Δ' Δ'' E i k j t K l v q P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Load (Lit (LitLoc l))) K d, Δ' ) →
envs_lookup j Δ' = Some (false, l ↦s{q} v)%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s{q} v)) k (ownT t (of_val v) 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.
rewrite (refine_load _ 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_store Δ Δ' Δ'' E i k j t K l v e v' P :
to_val e = Some v' →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Store (Lit (LitLoc l)) e) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s v)%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s v')) k (ownT t (Lit LitUnit) 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.
rewrite (refine_store _ 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_cas_fail Δ Δ' Δ'' E i k j t K l q v e1 v1 e2 v2 P :
to_val e1 = Some v1 → to_val e2 = Some v2 →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (CAS (Lit (LitLoc l)) e1 e2) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s{q} v)%I →
v ≠ v1 →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s{q} v)) k
(ownT t (Lit (LitBool false)) 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.
rewrite (refine_cas_fail _ 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_cas_suc Δ Δ' Δ'' E i k j t K l v e1 v1 e2 v2 P :
to_val e1 = Some v1 → to_val e2 = Some v2 →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (CAS (Lit (LitLoc l)) e1 e2) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s v)%I →
v = v1 →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s v2)) k
(ownT t (Lit (LitBool true)) K d')) Δ'
= Some Δ'' →
(Δ'' ⊢ P) →
Δ ⊢ |={E}=>> P.
Proof.
intros ?? Hl1 Hl2 Hl3 ? Haff ? HΔ1 HΔ2. subst.
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_cas_suc _ 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_swap Δ Δ' Δ'' E i k j t K l v e v' P :
to_val e = Some v' →
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (Swap (Lit (LitLoc l)) e) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s v)%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s v')) k (ownT t (of_val v) 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.
rewrite (refine_swap _ 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_fai Δ Δ' Δ'' E i k j t K l k' P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup_delete k Δ = Some (false, ownT t (FAI (Lit (LitLoc l))) K d, Δ') →
envs_lookup j Δ' = Some (false, l ↦s (LitV $ LitInt k'))%I →
(envs_delete j false Δ' ⊢ ⧆ envs_delete j false Δ') →
nclose sheapN ⊆ E →
envs_simple_replace j false (Esnoc (Esnoc Enil j (l ↦s (LitV $ LitInt (k'+1))))
k (ownT t (Lit $ LitInt k') 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.
rewrite (refine_fai _ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ E →
((sheap_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, sheap_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 sheapN ⊆ 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_lam Δ Δ' E i k t K x ef e v P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (App (Lam x ef) e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_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 sheapN ⊆ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (UnOp op (Lit l)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_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 sheapN ⊆ 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, sheap_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 sheapN ⊆ 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_fst Δ Δ' E i k t K e1 v1 e2 v2 P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Fst (Pair e1 e2)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ E →
to_val e1 = Some v1 → to_val e2 = Some v2 →
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_fst; eauto. Qed.
Lemma tac_refine_snd Δ Δ' E i k t K e1 v1 e2 v2 P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Snd (Pair e1 e2)) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ E →
to_val e1 = Some v1 → to_val e2 = Some v2 →
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_snd; eauto. Qed.
Lemma tac_refine_case_inl Δ Δ' E i k t K e0 v0 e1 e2 P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjL e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Case (InjR e0) e1 e2) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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 Δ E i k j t K e P :
envs_lookup i Δ = Some (true, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t (Fork e) K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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, sheap_ctx) →
envs_lookup k Δ = Some (false, ownT t e K d) →
(envs_delete k false Δ ⊢ ⧆ envs_delete k false Δ) →
nclose sheapN ⊆ 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 ?Δ ?j (ownT ?i ?e ?K ?dold)] ⇒
first
[reshape_expr e ltac:(fun K' e' ⇒
match eval hnf in e' with
Alloc ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_alloc with dold dnew _ _ H i _ e'' _
end)
| fail 1 "refine_alloc: cannot find 'Alloc' in " e];
[ try omega | try omega
| wp_done
| 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_load" 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
Load ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_load with d0 dnew _ _ _ _ _ i _ _ _ _
end)
| fail 1 "refine_load: cannot find 'Load' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| 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_load: no ownT found"
end.
Tactic Notation "refine_store" 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
Store ?e'' ?e''' ⇒ refine_bind K' at j;
eapply tac_refine_store with d0 dnew _ _ _ _ _ i _ _ _ e''' _
end)
| fail 1 "refine_store: cannot find 'Store' in " e ];
[ try omega | try omega | wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_store: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_store: no ownT found"
end.
Tactic Notation "refine_cas_fail" 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
CAS ?e'' ?e''' ?e'''' ⇒
refine_bind K' at j;
eapply tac_refine_cas_fail with
d0 dnew _ _ _ _ _ i _ _ _ _ e''' _ e'''' _
end)
| fail 1 "refine_cas_fail: cannot find 'CAS' in " e ];
[ try omega | try omega
| wp_done
| wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| try congruence
| apply affine_intro; auto; apply _ || fail "refine_cas_fail: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_cas_fail: no ownT found"
end.
Tactic Notation "refine_cas_suc" 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
CAS ?e'' ?e''' ?e'''' ⇒
refine_bind K' at j;
eapply tac_refine_cas_suc with
d0 dnew _ _ _ _ _ i _ _ _ e''' _ e'''' _
end)
| fail 1 "refine_cas_suc: cannot find 'CAS' in " e ];
[ try omega | try omega
| wp_done
| wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| try congruence
| apply affine_intro; auto; apply _ || fail "refine_cas_suc: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_cas_suc: no ownT found"
end.
Tactic Notation "refine_swap" 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
Swap ?e'' ?e''' ⇒ refine_bind K' at j;
eapply tac_refine_swap with d0 dnew _ _ _ _ _ i _ _ _ e''' _
end)
| fail 1 "refine_store: cannot find 'Store' in " e ];
[ try omega | try omega | wp_done
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_store: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_store: no ownT found"
end.
Tactic Notation "refine_fai" 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
FAI ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_fai with d0 dnew _ _ _ _ _ i _ _ _
end)
| fail 1 "refine_store: cannot find 'FAI' in " e ];
[ try omega | try omega
| iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_store: non-affine ctxt"
| done || eauto with ndisj
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_store: 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
App ?e1 ?e2 ⇒ refine_bind K' at j;
eapply tac_refine_rec with d0 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
| fast_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_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 with d0 dnew _ _ _ _ (comp_ectx K K') _ _ _ _;
[ 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_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
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_op: no ownT found"
end.
Tactic Notation "refine_proj" 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
| Fst _ ⇒
refine_bind K' at j;
eapply (tac_refine_fst d0 dnew)
| Snd _ ⇒
refine_bind K' at j;
eapply (tac_refine_snd d0 dnew)
end)
| fail 1 "refine_proj: cannot find 'Fst' or 'Snd' in " e ];
[ try omega | try omega | iAssumptionCore || fail "cannot find sheap_ctx"
| iAssumptionCore
| apply affine_intro; auto; apply _ || fail "refine_proj: non-affine ctxt"
| done || eauto with ndisj
| wp_done
| wp_done
| env_cbv; reflexivity
| rewrite -ownT_fill; simpl ectx_language.fill ]
| _ ⇒ fail "refine_proj: no ownT found"
end.
Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
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
Fork ?e'' ⇒ refine_bind K' at j;
eapply tac_refine_fork with d0 dnew _ _ H i _ e''
end)
| fail 1 "refine_fork: cannot find 'Fork' in " e];
[ 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 ]]
| _ ⇒ 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 ?e ?K ?d0)] ⇒
eapply tac_refine_stopped with _ i e _;
[ wp_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 with 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 with 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 ⇒ 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 "wp_focus: not a 'wp'"
end.
Section Test.
Context {Σ : gFunctors}.
Context (Kd: nat).
Context (Fd: nat).
Context `{refineG heap_lang Σ (delayed_lang (heap_lang) Kd Kd) (S Kd × (Kd + 3))}.
Context `{heapG Σ}.
Context `{sheapG heap_lang Σ}.
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 Σ).
Context (HBIG: Kd > 100).
Definition heap_proj : expr :=
let: "x" := Fst (Snd (#1, (#2, #3))) in
"x".
Lemma heap_proj_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_proj K Kd)
⊢ WP heap_proj @ E {{ v, v = #2 ★ ownT i (of_val (#2)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_proj.
wp_proj. refine_focus (Snd _)%E; refine_proj Kd; refine_unfocus.
wp_proj. refine_proj Kd.
wp_let. refine_let O.
wp_value. iPvsIntro.
iFrame; done.
Qed.
Definition heap_swap : expr :=
let: "x" := ref #1 in
let: "z" := Swap "x" #2 in
"z".
Lemma heap_swap_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_swap K Kd)
⊢ WP heap_swap @ E {{ v, v = #1 ★ ownT i (of_val (#1)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_swap.
wp_alloc l1. refine_alloc Kd l1'.
wp_let. refine_let Kd.
wp_swap. refine_swap Kd.
wp_let. refine_let O.
wp_value. iPvsIntro.
iFrame; done.
Qed.
Definition heap_fai : expr :=
let: "x" := ref #1 in
let: "z" := FAI "x" in
"z".
Lemma heap_fai_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_fai K Kd)
⊢ WP heap_fai @ E {{ v, v = #1 ★ ownT i (of_val (#1)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_fai.
wp_alloc l1. refine_alloc Kd l1'.
wp_let. refine_let Kd.
wp_fai. refine_fai Kd.
wp_let. refine_let O.
wp_value. iPvsIntro.
iFrame; done.
Qed.
Definition heap_e2 : expr :=
let: "x" := ref #1 in
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
Lemma heap_e2_spec E i K:
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e2 K Kd)
⊢ WP heap_e2 @ E {{ v, v = #2 ★ ownT i (of_val (#2)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e2.
wp_alloc l1. refine_alloc Kd l1'.
wp_let. refine_let Kd.
wp_alloc l2. refine_alloc Kd l2'.
wp_let. refine_let Kd.
wp_load. refine_load Kd.
wp_op. refine_op Kd.
wp_store. refine_store Kd.
wp_seq. refine_seq Kd.
wp_load. refine_load 0%nat.
by iFrame "Hown".
Qed.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;;
"x" <- - !"x" ;;
CAS "x" #2 #4 ;;
CAS "x" #(-2) #3.
Lemma heap_e_spec E P i K :
nclose sheapN ⊆ E →
nclose heapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e K Kd)
⊢ WP heap_e @ E {{ v, v = #true ★ ownT i (of_val (#true)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e.
wp_alloc l.
refine_alloc Kd l'.
wp_let.
refine_let Kd.
wp_load.
refine_focus (! (#_))%E.
refine_load Kd. simpl.
refine_unfocus.
refine_unfocus.
refine_bind K.
wp_op.
refine_op Kd.
wp_store.
refine_store Kd.
wp_let.
refine_let Kd.
wp_load.
refine_load Kd.
wp_op.
refine_op Kd.
wp_store.
refine_store Kd.
wp_seq.
refine_seq Kd.
wp_cas_fail; auto.
refine_cas_fail Kd; auto.
wp_seq.
refine_seq Kd.
wp_cas_suc; auto.
refine_cas_suc 0%nat; auto.
iFrame "Hown". auto.
Qed.
Definition heap_e_fork : expr :=
let: "x" := ref #1 in Fork ("x" <- !"x" + #1) ;; #2.
Lemma heap_e_fork_spec E K N N' i :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i heap_e_fork K Kd)
⊢ WP heap_e_fork @ E {{ v, (v = #2 ∨ v = #1) ★ ownT i (of_val (v)) K Kd}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_fork.
wp_alloc l. refine_alloc Kd l'.
wp_let. refine_let (Kd-1)%nat.
wp_apply wp_fork.
refine_fork Kd i' as "Hown'".
iSplitL "Hown".
- wp_seq. refine_seq (Kd)%nat. wp_value. iPvsIntro.
iFrame "Hown". iClear "~". iClear "~1". iLeft. auto.
- wp_load. refine_load (Kd -1)%nat.
rewrite /fresh_delay //=.
wp_op. refine_op Kd.
wp_store. refine_store 0%nat.
refine_stopped.
Qed.
Definition acquire : expr :=
rec: "acquire" "l" :=
if: CAS "l" #false #true then #() else "acquire" "l".
Definition heap_e_rec b: expr :=
let: "x" := ref #true in acquire "x" ;; #b.
Lemma heap_e_rec_spec E K i :
nclose heapN ⊆ E →
nclose sheapN ⊆ E →
(heap_ctx ★ sheap_ctx ★ ownT i (heap_e_rec false) K Kd)
⊢ WP (heap_e_rec true) @ E {{ v, v = #true ★ ownT i (of_val (v)) K 0%nat}}.
Proof.
iIntros (HN HN') "(#?&#?&Hown)". rewrite /heap_e_rec /acquire.
wp_alloc l. refine_alloc Kd l'.
wp_let. refine_let Kd.
wp_focus ((rec: "acquire" "l" := if: CAS "l" #false #true then #() else "acquire" "l") (#l)%E)%E.
iLob as "IH".
apply affine_intro; first apply _.
iIntros "! Hpts Hown Hpt".
rewrite affine_later_1.
wp_rec. refine_rec Kd.
wp_cas_fail. refine_cas_fail Kd.
wp_if. refine_if_false Kd.
rewrite affine_elim.
iClear "~". iClear "~1".
by iApply ("IH" with "Hpts Hown").
Qed.
End Test.