Library iris.program_logic.refine_ectx
From iris.prelude Require Export set irelations.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import
language ectx_language wsat refine_raw refine_raw_adequacy hoare ownership stepshifts.
From iris.proofmode Require Import pviewshifts pstepshifts invariants.
Section refine_ectx.
Context {expr val ectx state: Type}.
Context {sΛ : EctxLanguage expr val ectx state}.
Context `{refineG Λ Σ (@ectx_lang expr val ectx state sΛ) Kd}.
Require iris.program_logic.refine.
Definition ownSP (sσ: state) := refine.ownSP _ sσ.
Instance ownSP_affine sσ: AffineP (ownSP sσ). apply _. Qed.
Instance ownSP_atimeless sσ: ATimelessP (ownSP sσ). apply _. Qed.
Definition ownT (i: nat) (e: expr) (K: ectx):=
(∃ c cs ixs, ⧆■(nth_error (fst c) i = Some (fill K e)) ★
ownle (refine (@ectx_lang expr val ectx state sΛ)
Kd snapshot {[i]} (cs ++ [c]) ixs))%I.
Lemma ownT_equiv i e e' K K':
fill K e = fill K' e' →
ownT i e K ⊣⊢ ownT i e' K'.
Proof.
rewrite /ownT. intros →. auto.
Qed.
Lemma ownT_ownT_ectx i K e:
refine.ownT _ i (fill K e) ⊣⊢ ownT i e K.
Proof. rewrite /refine.ownT /ownT; auto. Qed.
Lemma ownSP_ownSP_ectx σ:
refine.ownSP _ σ ⊣⊢ ownSP σ.
Proof. rewrite /refine.ownSP /ownSP; auto. Qed.
Section refine_lemmas.
Import uPred.
Lemma ownSP_ownSP sσ sσ': (ownSP sσ ★ ownSP sσ') ⊢ False.
Proof. apply refine.ownSP_ownSP. Qed.
Lemma ownT_ownT i i' e K e' K':
(ownT i e K ★ ownT i' e' K') ⊣⊢ (⧆■(i ≠ i') ★ ownT i e K ★ ownT i' e' K').
Proof. rewrite -?ownT_ownT_ectx. apply refine.ownT_ownT. Qed.
Lemma ownT_fill i e K K': ownT i (fill K e) K' ⊣⊢ ownT i e (comp_ectx K' K).
Proof. apply ownT_equiv; auto using fill_comp. Qed.
Lemma ownT_focus i e K K': ownT i (fill K e) K' ⊢ ownT i e (comp_ectx K' K).
Proof. rewrite ownT_fill; auto. Qed.
Lemma ownT_unfocus i e K: ownT i e K ⊢ ownT i (fill K e) empty_ectx.
Proof. rewrite ownT_equiv; eauto using fill_empty. Qed.
Lemma prim_step_nofork_ectx K N' e sσ e' sσ':
nsteps (prim_step_nofork _) N' (e, sσ) (e', sσ') →
nsteps (prim_step_nofork _) N' (fill K e, sσ) (fill 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 N' E i e K sσ e' sσ':
nsteps (prim_step_nofork _) N' (e, sσ) (e', sσ') →
(1 ≤ N' ∧ N' ≤ Kd) →
(ownT i e K ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K ★ ownSP sσ'.
Proof.
rewrite -?ownT_ownT_ectx. intros; rewrite refine.ownT_ownSP_step_nofork; eauto.
by apply prim_step_nofork_ectx.
Qed.
Lemma ownT_ownSP_step_nofork_ctx1 K E i e sσ e' sσ':
prim_step e sσ e' sσ' None →
(ownT i e K ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K ★ ownSP sσ'.
Proof.
rewrite -?ownT_ownT_ectx. intros; rewrite refine.ownT_ownSP_step_nofork_ctx1; eauto.
Qed.
Lemma ownT_ownSP_step_fork K E i e sσ e' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
(ownT i e K ★ ownSP sσ) ⊢ |={E}=>> ∃ i', ownT i e' K ★ ownT i' ef empty_ectx ★ ownSP sσ'.
Proof.
setoid_rewrite <-ownT_ownT_ectx. intros; rewrite refine.ownT_ownSP_step_fork; eauto.
rewrite fill_empty; by apply fill_step.
Qed.
Lemma ownT_val_stopped i v P:
(ownT i (of_val v) empty_ectx ★ ⧆P) ⊢ uPred_stopped.
Proof.
rewrite -ownT_ownT_ectx fill_empty. by rewrite refine.ownT_val_stopped.
Qed.
End refine_lemmas.
Section refine_adequacy.
Import uPred.
Context (PrimDet: ∀ (e: expr) σ 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) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}).
From iris.program_logic Require refine.
Lemma ht_equiv_ectx (E: expr) e (sσ: state) σ Φ:
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} ⊢
{{ refine.ownT (ectx_lang expr) 0 E ★ ownP σ ★ refine.ownSP (ectx_lang expr) sσ }}
e
{{ v, (∃ V, refine.ownT (ectx_lang expr) 0 (of_val V) ★ ⧆■ Φ v V) }}.
Proof.
apply ht_mono; intros.
- by rewrite -?ownT_ownT_ectx -?ownSP_ownSP_ectx ?fill_empty.
- apply exist_mono; intros;
by rewrite -?ownT_ownT_ectx -?ownSP_ownSP_ectx ?fill_empty.
Qed.
Lemma ht_adequacy_refine' (E: expr) e v t2 (sσ: state) σ σ2 Φ l:
isteps idx_step l ([e], σ) (of_val v :: t2, σ2) →
Forall (λ e, ¬ reducible e σ2) (of_val v :: t2) →
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ 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.
rewrite ht_equiv_ectx. eapply @refine.ht_adequacy_refine'; eauto.
Qed.
Lemma ht_adequacy_inf_refine' (E: expr) e (sσ: state) σ Φ
(tr: trace idx_step ([e], σ)):
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} →
∃ (tr': trace idx_step ([E], sσ)), fair_pres _ _ tr tr'.
Proof.
rewrite ht_equiv_ectx. eapply @refine.ht_adequacy_inf_refine'; eauto.
Qed.
Lemma ht_safe_refine' e σ E sσ Φ:
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} →
safe_refine' Φ e σ E sσ.
Proof.
rewrite ht_equiv_ectx. eapply @refine.ht_safe_refine'; eauto.
Qed.
Lemma ht_safe_refine e σ E sσ Φ:
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} →
safe_refine Φ e σ E sσ.
Proof.
rewrite ht_equiv_ectx. eapply @refine.ht_safe_refine; eauto.
Qed.
End refine_adequacy.
End refine_ectx.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import
language ectx_language wsat refine_raw refine_raw_adequacy hoare ownership stepshifts.
From iris.proofmode Require Import pviewshifts pstepshifts invariants.
Section refine_ectx.
Context {expr val ectx state: Type}.
Context {sΛ : EctxLanguage expr val ectx state}.
Context `{refineG Λ Σ (@ectx_lang expr val ectx state sΛ) Kd}.
Require iris.program_logic.refine.
Definition ownSP (sσ: state) := refine.ownSP _ sσ.
Instance ownSP_affine sσ: AffineP (ownSP sσ). apply _. Qed.
Instance ownSP_atimeless sσ: ATimelessP (ownSP sσ). apply _. Qed.
Definition ownT (i: nat) (e: expr) (K: ectx):=
(∃ c cs ixs, ⧆■(nth_error (fst c) i = Some (fill K e)) ★
ownle (refine (@ectx_lang expr val ectx state sΛ)
Kd snapshot {[i]} (cs ++ [c]) ixs))%I.
Lemma ownT_equiv i e e' K K':
fill K e = fill K' e' →
ownT i e K ⊣⊢ ownT i e' K'.
Proof.
rewrite /ownT. intros →. auto.
Qed.
Lemma ownT_ownT_ectx i K e:
refine.ownT _ i (fill K e) ⊣⊢ ownT i e K.
Proof. rewrite /refine.ownT /ownT; auto. Qed.
Lemma ownSP_ownSP_ectx σ:
refine.ownSP _ σ ⊣⊢ ownSP σ.
Proof. rewrite /refine.ownSP /ownSP; auto. Qed.
Section refine_lemmas.
Import uPred.
Lemma ownSP_ownSP sσ sσ': (ownSP sσ ★ ownSP sσ') ⊢ False.
Proof. apply refine.ownSP_ownSP. Qed.
Lemma ownT_ownT i i' e K e' K':
(ownT i e K ★ ownT i' e' K') ⊣⊢ (⧆■(i ≠ i') ★ ownT i e K ★ ownT i' e' K').
Proof. rewrite -?ownT_ownT_ectx. apply refine.ownT_ownT. Qed.
Lemma ownT_fill i e K K': ownT i (fill K e) K' ⊣⊢ ownT i e (comp_ectx K' K).
Proof. apply ownT_equiv; auto using fill_comp. Qed.
Lemma ownT_focus i e K K': ownT i (fill K e) K' ⊢ ownT i e (comp_ectx K' K).
Proof. rewrite ownT_fill; auto. Qed.
Lemma ownT_unfocus i e K: ownT i e K ⊢ ownT i (fill K e) empty_ectx.
Proof. rewrite ownT_equiv; eauto using fill_empty. Qed.
Lemma prim_step_nofork_ectx K N' e sσ e' sσ':
nsteps (prim_step_nofork _) N' (e, sσ) (e', sσ') →
nsteps (prim_step_nofork _) N' (fill K e, sσ) (fill 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 N' E i e K sσ e' sσ':
nsteps (prim_step_nofork _) N' (e, sσ) (e', sσ') →
(1 ≤ N' ∧ N' ≤ Kd) →
(ownT i e K ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K ★ ownSP sσ'.
Proof.
rewrite -?ownT_ownT_ectx. intros; rewrite refine.ownT_ownSP_step_nofork; eauto.
by apply prim_step_nofork_ectx.
Qed.
Lemma ownT_ownSP_step_nofork_ctx1 K E i e sσ e' sσ':
prim_step e sσ e' sσ' None →
(ownT i e K ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K ★ ownSP sσ'.
Proof.
rewrite -?ownT_ownT_ectx. intros; rewrite refine.ownT_ownSP_step_nofork_ctx1; eauto.
Qed.
Lemma ownT_ownSP_step_fork K E i e sσ e' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
(ownT i e K ★ ownSP sσ) ⊢ |={E}=>> ∃ i', ownT i e' K ★ ownT i' ef empty_ectx ★ ownSP sσ'.
Proof.
setoid_rewrite <-ownT_ownT_ectx. intros; rewrite refine.ownT_ownSP_step_fork; eauto.
rewrite fill_empty; by apply fill_step.
Qed.
Lemma ownT_val_stopped i v P:
(ownT i (of_val v) empty_ectx ★ ⧆P) ⊢ uPred_stopped.
Proof.
rewrite -ownT_ownT_ectx fill_empty. by rewrite refine.ownT_val_stopped.
Qed.
End refine_lemmas.
Section refine_adequacy.
Import uPred.
Context (PrimDet: ∀ (e: expr) σ 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) σ, { t | prim_step e σ (fst (fst t)) (snd (fst t)) (snd t)} +
{¬ ∃ e' σ' ef', prim_step e σ e' σ' ef'}).
From iris.program_logic Require refine.
Lemma ht_equiv_ectx (E: expr) e (sσ: state) σ Φ:
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} ⊢
{{ refine.ownT (ectx_lang expr) 0 E ★ ownP σ ★ refine.ownSP (ectx_lang expr) sσ }}
e
{{ v, (∃ V, refine.ownT (ectx_lang expr) 0 (of_val V) ★ ⧆■ Φ v V) }}.
Proof.
apply ht_mono; intros.
- by rewrite -?ownT_ownT_ectx -?ownSP_ownSP_ectx ?fill_empty.
- apply exist_mono; intros;
by rewrite -?ownT_ownT_ectx -?ownSP_ownSP_ectx ?fill_empty.
Qed.
Lemma ht_adequacy_refine' (E: expr) e v t2 (sσ: state) σ σ2 Φ l:
isteps idx_step l ([e], σ) (of_val v :: t2, σ2) →
Forall (λ e, ¬ reducible e σ2) (of_val v :: t2) →
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ 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.
rewrite ht_equiv_ectx. eapply @refine.ht_adequacy_refine'; eauto.
Qed.
Lemma ht_adequacy_inf_refine' (E: expr) e (sσ: state) σ Φ
(tr: trace idx_step ([e], σ)):
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} →
∃ (tr': trace idx_step ([E], sσ)), fair_pres _ _ tr tr'.
Proof.
rewrite ht_equiv_ectx. eapply @refine.ht_adequacy_inf_refine'; eauto.
Qed.
Lemma ht_safe_refine' e σ E sσ Φ:
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} →
safe_refine' Φ e σ E sσ.
Proof.
rewrite ht_equiv_ectx. eapply @refine.ht_safe_refine'; eauto.
Qed.
Lemma ht_safe_refine e σ E sσ Φ:
{{ ownT 0 E empty_ectx ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx ★ ⧆■ Φ v V) }} →
safe_refine Φ e σ E sσ.
Proof.
rewrite ht_equiv_ectx. eapply @refine.ht_safe_refine; eauto.
Qed.
End refine_adequacy.
End refine_ectx.