Library iris.program_logic.refine
From iris.prelude Require Export set irelations.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import
language wsat refine_raw refine_raw_adequacy hoare ownership stepshifts.
From iris.proofmode Require Import pviewshifts pstepshifts invariants.
Section refine.
Context (sΛ: language).
Context `{refineG Λ Σ sΛ Kd}.
Definition ownSP (sσ: state sΛ) :=
(⧆(∃ ts cs ixs, owne (refine sΛ Kd master ∅ (cs ++ [(ts, sσ)]) ixs)))%I.
Instance ownSP_affine sσ: AffineP (ownSP sσ).
Proof. rewrite /ownSP; apply _. Qed.
Instance ownSP_atimeless sσ: ATimelessP (ownSP sσ).
Proof. rewrite /ownSP; apply _. Qed.
Definition ownT (i: nat) (e: expr sΛ) :=
(∃ c cs ixs, ⧆■(nth_error (fst c) i = Some e) ★
ownle (refine sΛ Kd snapshot {[i]} (cs ++ [c]) ixs))%I.
Section refine_lemmas.
Import uPred.
Lemma ownSP_ownSP sσ sσ': (ownSP sσ ★ ownSP sσ') ⊢ False.
Proof.
rewrite /ownSP /master_own_exact.
rewrite ?affine_elim.
rewrite ?sep_exist_r. apply exist_elim⇒ ts.
rewrite ?sep_exist_r. apply exist_elim⇒ cs.
rewrite ?sep_exist_r. apply exist_elim⇒ ixs.
rewrite ?sep_exist_l. apply exist_elim⇒ ts'.
rewrite ?sep_exist_l. apply exist_elim⇒ cs'.
rewrite ?sep_exist_l. apply exist_elim⇒ ixs'.
rewrite -owne_op owne_valid affine_elim. apply valid_elim.
inversion 1 as (_&_&Hdisj).
inversion Hdisj.
Qed.
Lemma ownT_ownT i i' e e':
(ownT i e ★ ownT i' e') ⊣⊢ (⧆■(i ≠ i') ★ ownT i e ★ ownT i' e').
Proof.
apply (anti_symm (⊢)); last (by rewrite sep_elim_r).
case (decide (i = i')).
- intros →.
etransitivity; last apply False_elim.
rewrite /ownT /snapshot_ownl_exact.
rewrite ?sep_exist_r. apply exist_elim⇒ c.
rewrite ?sep_exist_r. apply exist_elim⇒ cs.
rewrite ?sep_exist_r. apply exist_elim⇒ ixs.
rewrite ?sep_exist_l. apply exist_elim⇒ c'.
rewrite ?sep_exist_l. apply exist_elim⇒ cs'.
rewrite ?sep_exist_l. apply exist_elim⇒ ixs'.
rewrite ?sep_elim_r.
rewrite -ownle_op ownle_valid_l.
rewrite valid_elim. rewrite affine_elim. rewrite sep_False; auto.
inversion 1 as (_&_&Hdisj).
inversion Hdisj as [?????? Hdisj' | |]. clear -Hdisj'. set_solver.
- intros Hneq. rewrite pure_equiv //= -emp_True ?left_id //=.
Qed.
Lemma ownT_ownSP_step_nofork N' E i e sσ e' sσ':
nsteps (prim_step_nofork sΛ) N' (e, sσ) (e', sσ') →
(1 ≤ N' ∧ N' ≤ Kd) →
(ownT i e ★ ownSP sσ) ⊢ |={E}=>> ownT i e' ★ ownSP sσ'.
Proof.
iIntros (Hnsteps Hbound).
iIntros "(Hown1&Hown2)".
rewrite /ownT /ownSP.
iDestruct "Hown1" as (c cs ixs) "(%&Hown1)".
rewrite ?affine_exist. iDestruct "Hown2" as (ts') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (cs') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (ixs') "Hown2".
destruct c as (ts&sσ0).
efeed pose proof (owne_stepP refine_alt_triv) as Hshift0.
{ eapply snap_master_stepshift_nofork; eauto. }
iPoseProof Hshift0 as "Hshift".
- rewrite (affine_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
iPsvs ("Hshift" with "Hown").
iDestruct "~" as (r' rl') "(%&Hownr&Hownrl)".
destruct H1 as (cs''&ts''&ixs''&Hnth_error''&Hr'_equiv&Hrl'_equiv).
rewrite Hr'_equiv. rewrite Hrl'_equiv.
iPvsIntro.
iSplitL "Hownrl".
× iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl"; auto.
× iExists ts''. apply affine_intro; first apply _.
iExists cs'', ixs''; auto.
Qed.
Lemma prim_step_nofork_ctx `{LanguageCtx sΛ K} N' e sσ e' sσ':
nsteps (prim_step_nofork sΛ) N' (e, sσ) (e', sσ') →
nsteps (prim_step_nofork sΛ) N' (K e, sσ) (K e', sσ').
Proof.
remember (e, sσ) as c eqn:Heq_c.
remember (e', sσ') as c' eqn:Heq_c'.
intros Hnsteps. revert e sσ e' sσ' Heq_c Heq_c'.
induction Hnsteps; intros.
- subst. inversion Heq_c'. subst. econstructor.
- subst. destruct y as (e''&sσ''). econstructor; eauto.
× rewrite /prim_step_nofork //=. eapply fill_step; eauto.
Qed.
Lemma ownT_ownSP_step_nofork_ctx `{LanguageCtx sΛ K} N' E i e sσ e' sσ':
nsteps (prim_step_nofork sΛ) N' (e, sσ) (e', sσ') →
(1 ≤ N' ∧ N' ≤ Kd) →
(ownT i (K e) ★ ownSP sσ) ⊢ |={E}=>> ownT i (K e') ★ ownSP sσ'.
Proof.
intros. eapply ownT_ownSP_step_nofork; eauto using prim_step_nofork_ctx.
Qed.
Lemma ownT_ownSP_step_nofork_ctx1 `{LanguageCtx sΛ K} E i e sσ e' sσ':
prim_step e sσ e' sσ' None →
(ownT i (K e) ★ ownSP sσ) ⊢ |={E}=>> ownT i (K e') ★ ownSP sσ'.
Proof.
intros; eapply (ownT_ownSP_step_nofork_ctx 1).
rewrite /prim_step_nofork.
eapply nsteps_once; eauto.
split; auto.
destruct Kd; last omega. exfalso. eapply refine_Knz; auto.
Qed.
Lemma ownT_ownSP_step_fork E i e sσ e' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
(ownT i e ★ ownSP sσ) ⊢ |={E}=>> ∃ i', ownT i e' ★ ownT i' ef ★ ownSP sσ'.
Proof.
iIntros (Hstep).
iIntros "(Hown1&Hown2)".
rewrite /ownT /ownSP.
iDestruct "Hown1" as (c cs ixs) "(%&Hown1)".
rewrite ?affine_exist. iDestruct "Hown2" as (ts') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (cs') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (ixs') "Hown2".
destruct c as (ts&sσ0).
efeed pose proof (owne_stepP refine_alt_triv) as Hshift0.
{ eapply snap_master_simple_fork; eauto using refine_Knz. }
iPoseProof Hshift0 as "Hshift"; eauto.
- rewrite (affine_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
iPsvs ("Hshift" with "Hown").
iDestruct "~" as (r' rl') "(%&Hownr&Hownrl)".
destruct H1 as (i'&cs''&ts''&ixs''&Hnth_error''&Hnth_error2''&Hr'_equiv&Hrl'_equiv).
rewrite Hr'_equiv. rewrite Hrl'_equiv.
rewrite ownle_op. iDestruct "Hownrl" as "(Hownrl1&Hownrl2)".
iPvsIntro.
iExists i'.
iSplitL "Hownrl1".
× iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl1"; auto.
× iSplitL "Hownrl2".
** iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl2"; auto.
** apply affine_intro; first apply _. iExists ts'', cs'', ixs''; auto.
Qed.
Lemma ownT_ownSP_step_fork_ctx `{LanguageCtx sΛ K} E i e sσ e' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
(ownT i (K e) ★ ownSP sσ) ⊢ |={E}=>> ∃ i', ownT i (K e') ★ ownT i' ef ★ ownSP sσ'.
Proof.
intros Hprim. eapply ownT_ownSP_step_fork; eauto using fill_step.
Qed.
Lemma ownT_val_stopped i v P:
(ownT i (of_val v) ★ ⧆P) ⊢ uPred_stopped.
Proof.
rewrite /ownT.
rewrite sep_exist_r. apply exist_elim⇒ V.
rewrite sep_exist_r. apply exist_elim⇒ cs.
rewrite sep_exist_r. apply exist_elim⇒ ixs.
rewrite -assoc.
apply pure_elim_sep_l⇒Hnth.
destruct V.
etransitivity; last eapply own_value_stopped; eauto.
- rewrite /snapshot_ownl.
rewrite -(exist_intro cs).
rewrite -(exist_intro ixs).
eauto.
- eapply (refine_Knz).
Qed.
End refine_lemmas.
Section refine_adequacy.
Import uPred.
Context (PrimDet: ∀ (e: expr sΛ) σ e1' σ1' ef1' e2' σ2' ef2',
prim_step e σ e1' σ1' ef1' →
prim_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2').
Context (PrimDec: ∀ (e: expr sΛ) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}).
Lemma init_ownT E σ:
ownGl (to_globalFe (refine sΛ Kd snapshot {[0]} ([([E], σ)]) []))
⊢ ownT 0 E.
Proof.
rewrite /ownT. iIntros "H1". iExists ([E], σ). iExists ([]). iExists [].
rewrite ownle_eq. iFrame "H1".
rewrite pure_equiv //= -emp_True; auto.
Qed.
Lemma init_ownSP E σ:
ownG (to_globalFe (refine sΛ Kd master ∅ ([([E], σ)]) []))
⊢ ownSP σ.
Proof.
rewrite /ownSP. iIntros "H1". apply affine_intro; first apply _.
iExists [E]. iExists ([]). iExists [].
rewrite owne_eq // app_nil_l.
Qed.
Lemma ht_adequacy_refine' (E: expr sΛ) (e: expr Λ) v t2 (sσ: state sΛ) (σ σ2: state Λ) Φ l:
isteps idx_step l ([e], σ) (of_val v :: t2, σ2) →
Forall (λ e, ¬ reducible e σ2) (of_val v :: t2) →
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
∃ l' V T2 sσ2,
isteps idx_step l' ([E], sσ) (of_val V :: T2, sσ2) ∧
(∀ i, ¬ (enabled idx_step (of_val V :: T2, sσ2)) i) ∧
Φ v V.
Proof.
intros Histep Hnr Hht.
eapply ht_adequacy_refine; eauto using refine_Knz.
rewrite Hht; apply ht_mono.
- repeat apply sep_mono; auto.
× rewrite /ownT /snapshot_ownl_exact.
rewrite -(exist_intro ([E], sσ)) -(exist_intro []) -(exist_intro []).
rewrite (pure_equiv) //= -emp_True left_id //=.
× rewrite /ownSP /master_own_exact.
apply affine_intro; first apply _.
rewrite -(exist_intro ([E])) -(exist_intro []) -(exist_intro []) //=.
- intros v'.
rewrite /ownT /snapshot_ownl.
apply exist_elim⇒ V.
rewrite sep_exist_r. apply exist_elim⇒ c.
rewrite sep_exist_r. apply exist_elim⇒ cs.
rewrite sep_exist_r. apply exist_elim⇒ ixs.
rewrite -assoc.
apply pure_elim_sep_l⇒Hnth.
destruct c as (ts&sσ').
destruct ts as [| t ts']; simpl in Hnth; first congruence.
inversion Hnth; subst.
rewrite -(exist_intro V) -(exist_intro ts') -(exist_intro sσ').
rewrite -(exist_intro cs) -(exist_intro ixs) //=.
Qed.
Lemma ht_adequacy_inf_refine' (E: expr sΛ) (e: expr Λ) (sσ: state sΛ) (σ σ2: state Λ) Φ
(tr: trace idx_step ([e], σ)):
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
∃ (tr': trace idx_step ([E], sσ)), fair_pres _ _ tr tr'.
Proof.
intros Hht.
eapply ht_adequacy_inf_refine with _ _ _ (λ v V, ■Φ v V)%I; eauto using refine_Knz.
rewrite Hht; apply ht_mono.
- repeat apply sep_mono; auto.
× rewrite /ownT /snapshot_ownl_exact.
rewrite -(exist_intro ([E], sσ)) -(exist_intro []) -(exist_intro []).
rewrite (pure_equiv) //= -emp_True left_id //=.
× rewrite /ownSP /master_own_exact.
apply affine_intro; first apply _.
rewrite -(exist_intro ([E])) -(exist_intro []) -(exist_intro []) //=.
- intros v'.
rewrite /ownT /snapshot_ownl.
apply exist_elim⇒ V.
rewrite sep_exist_r. apply exist_elim⇒ c.
rewrite sep_exist_r. apply exist_elim⇒ cs.
rewrite sep_exist_r. apply exist_elim⇒ ixs.
rewrite -assoc.
apply pure_elim_sep_l⇒Hnth.
destruct c as (ts&sσ').
destruct ts as [| t ts']; simpl in Hnth; first congruence.
inversion Hnth; subst.
rewrite -(exist_intro V) -(exist_intro ts') -(exist_intro sσ').
rewrite -(exist_intro cs) -(exist_intro ixs) //=.
Qed.
Lemma ht_safe_refine' e σ E sσ Φ:
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }} e {{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
safe_refine' Φ e σ E sσ.
Proof.
intros Ht. split_and!.
- intros; apply Forall_forall⇒e' Hin.
case_eq (to_val e').
× intros; left; eauto.
× intros; right.
eapply (adequacy.ht_adequacy_reducible _
(λ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V)%I)); eauto; last first.
** erewrite Ht. apply ht_mono; last auto.
repeat apply sep_mono; eauto using init_ownT, init_ownSP.
** eapply init_own_snap_master_valid; apply refine_Knz.
- intros ???? Histeps Hforall.
edestruct (ht_adequacy_refine') as (l'&V&T2&sσ2&Hstep&Hnenabled&Hphi);
eauto.
{ econstructor.
- intros Hr%reducible_not_val.
rewrite to_of_val in Hr; congruence.
- apply Forall_forall. rewrite Forall_forall in Hforall ×.
intros Hforall e' Hin Hr%reducible_not_val. edestruct (Hforall); eauto.
congruence.
}
∃ l', V, T2, sσ2.
split_and!; auto.
× apply forall_not_enabled_forall_not_reducible, Forall_cons in Hnenabled.
destruct Hnenabled; auto.
- intros t Hfair.
edestruct (ht_adequacy_inf_refine') as (T&Hfp);
eauto.
Qed.
Lemma ht_safe_refine e σ E sσ Φ:
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }} e {{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
safe_refine Φ e σ E sσ.
Proof.
eauto using ht_safe_refine', safe_refine'_to_safe_refine.
Qed.
End refine_adequacy.
End refine.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import
language wsat refine_raw refine_raw_adequacy hoare ownership stepshifts.
From iris.proofmode Require Import pviewshifts pstepshifts invariants.
Section refine.
Context (sΛ: language).
Context `{refineG Λ Σ sΛ Kd}.
Definition ownSP (sσ: state sΛ) :=
(⧆(∃ ts cs ixs, owne (refine sΛ Kd master ∅ (cs ++ [(ts, sσ)]) ixs)))%I.
Instance ownSP_affine sσ: AffineP (ownSP sσ).
Proof. rewrite /ownSP; apply _. Qed.
Instance ownSP_atimeless sσ: ATimelessP (ownSP sσ).
Proof. rewrite /ownSP; apply _. Qed.
Definition ownT (i: nat) (e: expr sΛ) :=
(∃ c cs ixs, ⧆■(nth_error (fst c) i = Some e) ★
ownle (refine sΛ Kd snapshot {[i]} (cs ++ [c]) ixs))%I.
Section refine_lemmas.
Import uPred.
Lemma ownSP_ownSP sσ sσ': (ownSP sσ ★ ownSP sσ') ⊢ False.
Proof.
rewrite /ownSP /master_own_exact.
rewrite ?affine_elim.
rewrite ?sep_exist_r. apply exist_elim⇒ ts.
rewrite ?sep_exist_r. apply exist_elim⇒ cs.
rewrite ?sep_exist_r. apply exist_elim⇒ ixs.
rewrite ?sep_exist_l. apply exist_elim⇒ ts'.
rewrite ?sep_exist_l. apply exist_elim⇒ cs'.
rewrite ?sep_exist_l. apply exist_elim⇒ ixs'.
rewrite -owne_op owne_valid affine_elim. apply valid_elim.
inversion 1 as (_&_&Hdisj).
inversion Hdisj.
Qed.
Lemma ownT_ownT i i' e e':
(ownT i e ★ ownT i' e') ⊣⊢ (⧆■(i ≠ i') ★ ownT i e ★ ownT i' e').
Proof.
apply (anti_symm (⊢)); last (by rewrite sep_elim_r).
case (decide (i = i')).
- intros →.
etransitivity; last apply False_elim.
rewrite /ownT /snapshot_ownl_exact.
rewrite ?sep_exist_r. apply exist_elim⇒ c.
rewrite ?sep_exist_r. apply exist_elim⇒ cs.
rewrite ?sep_exist_r. apply exist_elim⇒ ixs.
rewrite ?sep_exist_l. apply exist_elim⇒ c'.
rewrite ?sep_exist_l. apply exist_elim⇒ cs'.
rewrite ?sep_exist_l. apply exist_elim⇒ ixs'.
rewrite ?sep_elim_r.
rewrite -ownle_op ownle_valid_l.
rewrite valid_elim. rewrite affine_elim. rewrite sep_False; auto.
inversion 1 as (_&_&Hdisj).
inversion Hdisj as [?????? Hdisj' | |]. clear -Hdisj'. set_solver.
- intros Hneq. rewrite pure_equiv //= -emp_True ?left_id //=.
Qed.
Lemma ownT_ownSP_step_nofork N' E i e sσ e' sσ':
nsteps (prim_step_nofork sΛ) N' (e, sσ) (e', sσ') →
(1 ≤ N' ∧ N' ≤ Kd) →
(ownT i e ★ ownSP sσ) ⊢ |={E}=>> ownT i e' ★ ownSP sσ'.
Proof.
iIntros (Hnsteps Hbound).
iIntros "(Hown1&Hown2)".
rewrite /ownT /ownSP.
iDestruct "Hown1" as (c cs ixs) "(%&Hown1)".
rewrite ?affine_exist. iDestruct "Hown2" as (ts') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (cs') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (ixs') "Hown2".
destruct c as (ts&sσ0).
efeed pose proof (owne_stepP refine_alt_triv) as Hshift0.
{ eapply snap_master_stepshift_nofork; eauto. }
iPoseProof Hshift0 as "Hshift".
- rewrite (affine_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
iPsvs ("Hshift" with "Hown").
iDestruct "~" as (r' rl') "(%&Hownr&Hownrl)".
destruct H1 as (cs''&ts''&ixs''&Hnth_error''&Hr'_equiv&Hrl'_equiv).
rewrite Hr'_equiv. rewrite Hrl'_equiv.
iPvsIntro.
iSplitL "Hownrl".
× iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl"; auto.
× iExists ts''. apply affine_intro; first apply _.
iExists cs'', ixs''; auto.
Qed.
Lemma prim_step_nofork_ctx `{LanguageCtx sΛ K} N' e sσ e' sσ':
nsteps (prim_step_nofork sΛ) N' (e, sσ) (e', sσ') →
nsteps (prim_step_nofork sΛ) N' (K e, sσ) (K e', sσ').
Proof.
remember (e, sσ) as c eqn:Heq_c.
remember (e', sσ') as c' eqn:Heq_c'.
intros Hnsteps. revert e sσ e' sσ' Heq_c Heq_c'.
induction Hnsteps; intros.
- subst. inversion Heq_c'. subst. econstructor.
- subst. destruct y as (e''&sσ''). econstructor; eauto.
× rewrite /prim_step_nofork //=. eapply fill_step; eauto.
Qed.
Lemma ownT_ownSP_step_nofork_ctx `{LanguageCtx sΛ K} N' E i e sσ e' sσ':
nsteps (prim_step_nofork sΛ) N' (e, sσ) (e', sσ') →
(1 ≤ N' ∧ N' ≤ Kd) →
(ownT i (K e) ★ ownSP sσ) ⊢ |={E}=>> ownT i (K e') ★ ownSP sσ'.
Proof.
intros. eapply ownT_ownSP_step_nofork; eauto using prim_step_nofork_ctx.
Qed.
Lemma ownT_ownSP_step_nofork_ctx1 `{LanguageCtx sΛ K} E i e sσ e' sσ':
prim_step e sσ e' sσ' None →
(ownT i (K e) ★ ownSP sσ) ⊢ |={E}=>> ownT i (K e') ★ ownSP sσ'.
Proof.
intros; eapply (ownT_ownSP_step_nofork_ctx 1).
rewrite /prim_step_nofork.
eapply nsteps_once; eauto.
split; auto.
destruct Kd; last omega. exfalso. eapply refine_Knz; auto.
Qed.
Lemma ownT_ownSP_step_fork E i e sσ e' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
(ownT i e ★ ownSP sσ) ⊢ |={E}=>> ∃ i', ownT i e' ★ ownT i' ef ★ ownSP sσ'.
Proof.
iIntros (Hstep).
iIntros "(Hown1&Hown2)".
rewrite /ownT /ownSP.
iDestruct "Hown1" as (c cs ixs) "(%&Hown1)".
rewrite ?affine_exist. iDestruct "Hown2" as (ts') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (cs') "Hown2".
rewrite ?affine_exist. iDestruct "Hown2" as (ixs') "Hown2".
destruct c as (ts&sσ0).
efeed pose proof (owne_stepP refine_alt_triv) as Hshift0.
{ eapply snap_master_simple_fork; eauto using refine_Knz. }
iPoseProof Hshift0 as "Hshift"; eauto.
- rewrite (affine_elim (owne _)). iCombine "Hown2" "Hown1" as "Hown".
iPsvs ("Hshift" with "Hown").
iDestruct "~" as (r' rl') "(%&Hownr&Hownrl)".
destruct H1 as (i'&cs''&ts''&ixs''&Hnth_error''&Hnth_error2''&Hr'_equiv&Hrl'_equiv).
rewrite Hr'_equiv. rewrite Hrl'_equiv.
rewrite ownle_op. iDestruct "Hownrl" as "(Hownrl1&Hownrl2)".
iPvsIntro.
iExists i'.
iSplitL "Hownrl1".
× iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl1"; auto.
× iSplitL "Hownrl2".
** iExists (ts'', sσ'), cs'', ixs''.
iSplitR "" "Hownrl2"; auto.
** apply affine_intro; first apply _. iExists ts'', cs'', ixs''; auto.
Qed.
Lemma ownT_ownSP_step_fork_ctx `{LanguageCtx sΛ K} E i e sσ e' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
(ownT i (K e) ★ ownSP sσ) ⊢ |={E}=>> ∃ i', ownT i (K e') ★ ownT i' ef ★ ownSP sσ'.
Proof.
intros Hprim. eapply ownT_ownSP_step_fork; eauto using fill_step.
Qed.
Lemma ownT_val_stopped i v P:
(ownT i (of_val v) ★ ⧆P) ⊢ uPred_stopped.
Proof.
rewrite /ownT.
rewrite sep_exist_r. apply exist_elim⇒ V.
rewrite sep_exist_r. apply exist_elim⇒ cs.
rewrite sep_exist_r. apply exist_elim⇒ ixs.
rewrite -assoc.
apply pure_elim_sep_l⇒Hnth.
destruct V.
etransitivity; last eapply own_value_stopped; eauto.
- rewrite /snapshot_ownl.
rewrite -(exist_intro cs).
rewrite -(exist_intro ixs).
eauto.
- eapply (refine_Knz).
Qed.
End refine_lemmas.
Section refine_adequacy.
Import uPred.
Context (PrimDet: ∀ (e: expr sΛ) σ e1' σ1' ef1' e2' σ2' ef2',
prim_step e σ e1' σ1' ef1' →
prim_step e σ e2' σ2' ef2' →
e1' = e2' ∧ σ1' = σ2' ∧ ef1' = ef2').
Context (PrimDec: ∀ (e: expr sΛ) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}).
Lemma init_ownT E σ:
ownGl (to_globalFe (refine sΛ Kd snapshot {[0]} ([([E], σ)]) []))
⊢ ownT 0 E.
Proof.
rewrite /ownT. iIntros "H1". iExists ([E], σ). iExists ([]). iExists [].
rewrite ownle_eq. iFrame "H1".
rewrite pure_equiv //= -emp_True; auto.
Qed.
Lemma init_ownSP E σ:
ownG (to_globalFe (refine sΛ Kd master ∅ ([([E], σ)]) []))
⊢ ownSP σ.
Proof.
rewrite /ownSP. iIntros "H1". apply affine_intro; first apply _.
iExists [E]. iExists ([]). iExists [].
rewrite owne_eq // app_nil_l.
Qed.
Lemma ht_adequacy_refine' (E: expr sΛ) (e: expr Λ) v t2 (sσ: state sΛ) (σ σ2: state Λ) Φ l:
isteps idx_step l ([e], σ) (of_val v :: t2, σ2) →
Forall (λ e, ¬ reducible e σ2) (of_val v :: t2) →
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
∃ l' V T2 sσ2,
isteps idx_step l' ([E], sσ) (of_val V :: T2, sσ2) ∧
(∀ i, ¬ (enabled idx_step (of_val V :: T2, sσ2)) i) ∧
Φ v V.
Proof.
intros Histep Hnr Hht.
eapply ht_adequacy_refine; eauto using refine_Knz.
rewrite Hht; apply ht_mono.
- repeat apply sep_mono; auto.
× rewrite /ownT /snapshot_ownl_exact.
rewrite -(exist_intro ([E], sσ)) -(exist_intro []) -(exist_intro []).
rewrite (pure_equiv) //= -emp_True left_id //=.
× rewrite /ownSP /master_own_exact.
apply affine_intro; first apply _.
rewrite -(exist_intro ([E])) -(exist_intro []) -(exist_intro []) //=.
- intros v'.
rewrite /ownT /snapshot_ownl.
apply exist_elim⇒ V.
rewrite sep_exist_r. apply exist_elim⇒ c.
rewrite sep_exist_r. apply exist_elim⇒ cs.
rewrite sep_exist_r. apply exist_elim⇒ ixs.
rewrite -assoc.
apply pure_elim_sep_l⇒Hnth.
destruct c as (ts&sσ').
destruct ts as [| t ts']; simpl in Hnth; first congruence.
inversion Hnth; subst.
rewrite -(exist_intro V) -(exist_intro ts') -(exist_intro sσ').
rewrite -(exist_intro cs) -(exist_intro ixs) //=.
Qed.
Lemma ht_adequacy_inf_refine' (E: expr sΛ) (e: expr Λ) (sσ: state sΛ) (σ σ2: state Λ) Φ
(tr: trace idx_step ([e], σ)):
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
∃ (tr': trace idx_step ([E], sσ)), fair_pres _ _ tr tr'.
Proof.
intros Hht.
eapply ht_adequacy_inf_refine with _ _ _ (λ v V, ■Φ v V)%I; eauto using refine_Knz.
rewrite Hht; apply ht_mono.
- repeat apply sep_mono; auto.
× rewrite /ownT /snapshot_ownl_exact.
rewrite -(exist_intro ([E], sσ)) -(exist_intro []) -(exist_intro []).
rewrite (pure_equiv) //= -emp_True left_id //=.
× rewrite /ownSP /master_own_exact.
apply affine_intro; first apply _.
rewrite -(exist_intro ([E])) -(exist_intro []) -(exist_intro []) //=.
- intros v'.
rewrite /ownT /snapshot_ownl.
apply exist_elim⇒ V.
rewrite sep_exist_r. apply exist_elim⇒ c.
rewrite sep_exist_r. apply exist_elim⇒ cs.
rewrite sep_exist_r. apply exist_elim⇒ ixs.
rewrite -assoc.
apply pure_elim_sep_l⇒Hnth.
destruct c as (ts&sσ').
destruct ts as [| t ts']; simpl in Hnth; first congruence.
inversion Hnth; subst.
rewrite -(exist_intro V) -(exist_intro ts') -(exist_intro sσ').
rewrite -(exist_intro cs) -(exist_intro ixs) //=.
Qed.
Lemma ht_safe_refine' e σ E sσ Φ:
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }} e {{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
safe_refine' Φ e σ E sσ.
Proof.
intros Ht. split_and!.
- intros; apply Forall_forall⇒e' Hin.
case_eq (to_val e').
× intros; left; eauto.
× intros; right.
eapply (adequacy.ht_adequacy_reducible _
(λ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V)%I)); eauto; last first.
** erewrite Ht. apply ht_mono; last auto.
repeat apply sep_mono; eauto using init_ownT, init_ownSP.
** eapply init_own_snap_master_valid; apply refine_Knz.
- intros ???? Histeps Hforall.
edestruct (ht_adequacy_refine') as (l'&V&T2&sσ2&Hstep&Hnenabled&Hphi);
eauto.
{ econstructor.
- intros Hr%reducible_not_val.
rewrite to_of_val in Hr; congruence.
- apply Forall_forall. rewrite Forall_forall in Hforall ×.
intros Hforall e' Hin Hr%reducible_not_val. edestruct (Hforall); eauto.
congruence.
}
∃ l', V, T2, sσ2.
split_and!; auto.
× apply forall_not_enabled_forall_not_reducible, Forall_cons in Hnenabled.
destruct Hnenabled; auto.
- intros t Hfair.
edestruct (ht_adequacy_inf_refine') as (T&Hfp);
eauto.
Qed.
Lemma ht_safe_refine e σ E sσ Φ:
{{ ownT 0 E ★ ownP σ ★ ownSP sσ }} e {{ v, (∃ V, ownT 0 (of_val V) ★ ⧆■ Φ v V) }} →
safe_refine Φ e σ E sσ.
Proof.
eauto using ht_safe_refine', safe_refine'_to_safe_refine.
Qed.
End refine_adequacy.
End refine.