Library iris.program_logic.refine_ectx_delay
From iris.prelude Require Export set irelations.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import
language nat_delayed_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} {sΛ : EctxLanguage expr val ectx state}.
Context `{refineG Λ Σ (delayed_lang (ectx_lang expr) Kd Fd) (S Kd × (Kd + 3))}.
Require iris.program_logic.refine.
Definition ownSP (sσ: delayed_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) (d: nat):=
(∃ (c: cfg (delayed_lang _ Kd Fd)) cs ixs, ⧆■(nth_error (fst c) i = Some (fill K e, d)) ★
ownle (refine _ (S Kd × (Kd + 3)) snapshot {[i]} (cs ++ [c]) ixs))%I.
Lemma ownT_equiv i e e' K K' d:
fill K e = fill K' e' →
ownT i e K d ⊣⊢ ownT i e' K' d.
Proof.
rewrite /ownT. intros →. auto.
Qed.
Lemma ownT_ownT_ectx i K e d:
refine.ownT _ i ((fill K e, d) : delayed_expr _) ⊣⊢ ownT i e K d.
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 d e' K' d':
(ownT i e K d ★ ownT i' e' K' d') ⊣⊢ (⧆■(i ≠ i') ★ ownT i e K d ★ ownT i' e' K' d').
Proof. rewrite -?ownT_ownT_ectx. apply refine.ownT_ownT. Qed.
Lemma ownT_fill i e K K' d: ownT i (fill K e) K' d ⊣⊢ ownT i e (comp_ectx K' K) d.
Proof. apply ownT_equiv; auto using fill_comp. Qed.
Lemma ownT_focus i e K K' d: ownT i (fill K e) K' d ⊢ ownT i e (comp_ectx K' K) d.
Proof. rewrite ownT_fill; auto. Qed.
Lemma ownT_unfocus i e K d: ownT i e K d ⊢ ownT i (fill K e) empty_ectx d.
Proof. rewrite ownT_equiv; eauto using fill_empty. Qed.
Lemma prim_step_nofork_ectx_aux K d d' N e sσ e' sσ':
nsteps (prim_step_nofork _) N (e, sσ) (e', sσ') →
match N with
| 0 ⇒ d' ≤ d
| S _ ⇒ d' ≤ Kd
end →
∃ N', N' = match N with
| 0 ⇒ d - d'
| S N ⇒ S d + (N × (S Kd)) + (Kd - d')
end
∧ nsteps (prim_step_nofork (delayed_lang _ Kd Fd)) N'
((fill K e, d), sσ)
((fill K e', d'), 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' d d'.
induction Hnsteps; intros; subst.
- simpl. ∃ (d - d').
split; trivial.
inversion Heq_c'; subst.
assert (∃ k, d = d' + k) as (k&->).
{ ∃ (d - d'). omega. }
replace (d' + k - d') with k by omega.
clear; induction k.
× replace (d' + 0) with d' by omega.
econstructor; eauto.
× econstructor; eauto.
replace (d' + S k) with (S (d' + k)) by omega.
econstructor.
- eexists; split; eauto.
induction d.
× simpl. rewrite /prim_step_nofork in H0.
eapply (nsteps_l _ _ _ ((fill K (fst y), Kd), snd y)); eauto.
** rewrite /prim_step_nofork. simpl.
replace (None: option (delayed_expr _)) with
(default None None (λ e, Some (e, @fresh_delay (ectx_lang expr) Fd e))) by auto.
econstructor; eauto using fill_step.
** destruct n as [| n].
*** simpl. simpl.
destruct y as (e1, sσ1).
specialize (IHHnsteps e1 sσ1 e' sσ' Coq.Init.Logic.eq_refl Coq.Init.Logic.eq_refl).
edestruct (IHHnsteps Kd d') as (?&?&?); eauto.
subst. eauto.
*** replace (S n × S Kd + (Kd - d')) with
(S Kd + n × S Kd + (Kd - d')) by lia.
destruct y as (e1, sσ1).
specialize (IHHnsteps e1 sσ1 e' sσ' Coq.Init.Logic.eq_refl Coq.Init.Logic.eq_refl).
edestruct (IHHnsteps Kd d') as (?&?&?); eauto.
subst. eauto.
× replace (S (S d) + n × S Kd + (Kd - d')) with
(S (S d + n × S Kd + (Kd - d'))) by omega.
econstructor; eauto.
rewrite /prim_step_nofork. simpl.
replace (None: option (delayed_expr _)) with
(default None None (λ e, Some (e, @fresh_delay (ectx_lang expr) Kd e))) by auto.
econstructor.
Qed.
Lemma prim_step_nofork_ectx K d d' N e sσ e' sσ':
nsteps (prim_step_nofork _) (S N) (e, sσ) (e', sσ') →
d ≤ Kd →
d' ≤ Kd →
∃ N', 1 ≤ N' ∧ N' ≤ (S Kd) × (S (S N)) ∧ nsteps (prim_step_nofork (delayed_lang _ Kd Fd)) N'
((fill K e, d), sσ)
((fill K e', d'), sσ').
Proof.
intros. edestruct prim_step_nofork_ectx_aux as (N'&?&?); eauto.
{ simpl; eauto. }
∃ N'. subst. split_and!; eauto; lia.
Qed.
Lemma ownT_ownSP_step_nofork N' E i e K d sσ e' sσ' d':
nsteps (prim_step_nofork _) N' (e, sσ) (e', sσ') →
d ≤ Kd →
d' ≤ Kd →
(1 ≤ N' ∧ N' ≤ S Kd) →
(ownT i e K d ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K d' ★ ownSP sσ'.
Proof.
rewrite -?ownT_ownT_ectx.
intros ? ? ? (?&?).
destruct N' as [|N']; first omega.
edestruct (prim_step_nofork_ectx K d d') as (?&?&?&?); eauto.
rewrite refine.ownT_ownSP_step_nofork; eauto.
split; first omega.
etransitivity; eauto.
apply mult_le_compat_l; omega.
Qed.
Lemma ownT_ownSP_step_nofork_ctx1 K E i e d sσ e' d' sσ':
prim_step e sσ e' sσ' None →
d ≤ Kd →
d' ≤ Kd →
(ownT i e K d ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K d' ★ ownSP sσ'.
Proof.
intros; eapply ownT_ownSP_step_nofork; eauto.
- econstructor; last apply nsteps_O; eauto.
- split; auto. destruct Kd; omega.
Qed.
Lemma ownT_ownSP_step_fork K E i e d sσ e' d' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
d ≤ Kd →
d' ≤ Kd →
(ownT i e K d ★ ownSP sσ)
⊢ |={E}=>> ∃ i', ownT i e' K d' ★ ownT i' ef empty_ectx (fresh_delay _ Fd ef)★ ownSP sσ'.
Proof.
iIntros (Hstep Hd Hd').
iIntros "(Hown1&Hown2)".
rewrite /ownT /ownSP /refine.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).
iPoseProof (owne_stepP refine_alt_triv _ ((refine (delayed_lang (ectx_lang expr) Kd Fd)
(Kd + 3 + Kd × (Kd + 3)) master
∅ (cs' ++ [(ts', sσ)]) ixs'))
((refine (delayed_lang (ectx_lang expr) Kd Fd)
(Kd + 3 + Kd × (Kd + 3)) snapshot
{[i]} (cs ++ [(ts, sσ0)]) ixs))) as "Hshift"; eauto.
** eapply (snap_master_fork (delayed_lang (ectx_lang expr) Kd Fd) (S Kd × (Kd + 3)) i
d (Kd - d') (fill K e, d) (fill K e, 0)
(ef, fresh_delay _ Fd ef) (fill K e', Kd)
(fill K e', d') ts ts' sσ0 sσ sσ sσ' sσ'); eauto.
*** cut ( S (d + (Kd - d')) ≤ S Kd × (Kd + 3)); first omega.
transitivity (S (Kd + Kd)); first by omega.
clear. induction Kd; lia.
*** clear. induction d; first econstructor.
econstructor; last eapply IHd; eauto; econstructor.
*** eapply (base_step _ Kd Fd _ _ _ _ (Some ef)); eauto.
apply fill_step. eauto.
***
assert (∃ k, k + d' = Kd) as (k&Heqk); first (∃ (Kd - d'); omega).
replace (Kd - d') with k; last omega.
replace (fill K e', Kd, sσ') with (fill K e', k + d', sσ'); last f_equal; auto.
clear Heqk.
induction k.
**** simpl. econstructor.
**** replace (S k + d') with (S (k + d')); last omega.
eapply nsteps_l; last eapply IHk.
econstructor; auto.
** 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.
rewrite fill_empty pure_equiv //= -emp_True; auto.
**** apply affine_intro; first apply _. iExists ts'', cs'', ixs''; auto.
Qed.
Lemma ownT_ownSP_delay E i e K d d' sσ:
1 ≤ d - d' ∧ d - d' ≤ S Kd →
(ownT i e K d ★ ownSP sσ) ⊢ |={E}=>> ownT i e K d' ★ ownSP sσ.
Proof.
rewrite -?ownT_ownT_ectx; intros (?&Hle).
rewrite (refine.ownT_ownSP_step_nofork _ (d - d')); eauto.
- assert (∃ k, k + d' = d) as (k&Heq).
{ ∃ (d - d'). omega. }
replace (d - d') with k by omega.
replace (d - d') with k by omega.
rewrite -Heq. clear Heq.
induction k.
× econstructor.
× replace (S k + d') with (S (k + d')) by omega. econstructor; eauto.
econstructor.
- split; auto. clear -Hle. induction Kd; first lia; lia.
Qed.
Lemma ownT_ownSP_delay1 E i e K d sσ:
(ownT i e K (S d) ★ ownSP sσ) ⊢ |={E}=>> ownT i e K d ★ ownSP sσ.
Proof.
eapply ownT_ownSP_delay.
split; omega.
Qed.
Lemma ownT_val_stopped i v P:
(ownT i (of_val v) empty_ectx 0 ★ ⧆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) d e (sσ: state) σ Φ:
{{ ownT 0 E empty_ectx d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} ⊢
{{ refine.ownT (delayed_lang (ectx_lang expr) Kd Fd) 0 (E, d) ★ ownP σ
★ refine.ownSP (delayed_lang (ectx_lang expr) Kd Fd) sσ }}
e
{{ v, (∃ V, refine.ownT (delayed_lang (ectx_lang expr) Kd Fd) 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) d 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 d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} →
∃ l' V T2 sσ2,
isteps (@idx_step (delayed_lang (ectx_lang expr) Kd Fd)) l'
([(E, d)], sσ) (of_val V :: T2, sσ2) ∧
(∀ i, ¬ (enabled (@idx_step (delayed_lang (ectx_lang expr) Kd Fd)) (of_val V :: T2, sσ2)) i) ∧
Φ v V.
Proof.
rewrite ht_equiv_ectx. intros.
edestruct (@refine.ht_adequacy_refine' (delayed_lang (ectx_lang expr) Kd Fd)); eauto.
× eapply delayed_lang_det; eauto.
× eapply delayed_lang_dec; eauto.
Qed.
Lemma ht_adequacy_inf_refine' (E: expr) d e (sσ: state) σ Φ
(tr: trace idx_step ([e], σ)):
{{ ownT 0 E empty_ectx d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} →
∃ (tr': trace (@idx_step (delayed_lang (ectx_lang expr) Kd Fd))
([(E, d)], sσ)), fair_pres _ _ tr tr'.
Proof.
rewrite ht_equiv_ectx. intros.
eapply (@refine.ht_adequacy_inf_refine' (delayed_lang (ectx_lang expr) Kd Fd)); eauto.
× eapply delayed_lang_det; eauto.
× eapply delayed_lang_dec; eauto.
Qed.
Lemma ht_safe_refine e σ E d sσ Φ:
{{ ownT 0 E empty_ectx d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} →
safe_refine Φ e σ E sσ.
Proof.
rewrite ht_equiv_ectx.
intros. eapply delayed_lang_safe_refine.
eapply (@refine.ht_safe_refine (delayed_lang (ectx_lang expr) Kd Fd)); eauto.
× eapply delayed_lang_det; eauto.
× eapply delayed_lang_dec; eauto.
Qed.
End refine_adequacy.
End refine_ectx.
From iris.algebra Require Import dra cmra_tactics.
From iris.program_logic Require Import
language nat_delayed_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} {sΛ : EctxLanguage expr val ectx state}.
Context `{refineG Λ Σ (delayed_lang (ectx_lang expr) Kd Fd) (S Kd × (Kd + 3))}.
Require iris.program_logic.refine.
Definition ownSP (sσ: delayed_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) (d: nat):=
(∃ (c: cfg (delayed_lang _ Kd Fd)) cs ixs, ⧆■(nth_error (fst c) i = Some (fill K e, d)) ★
ownle (refine _ (S Kd × (Kd + 3)) snapshot {[i]} (cs ++ [c]) ixs))%I.
Lemma ownT_equiv i e e' K K' d:
fill K e = fill K' e' →
ownT i e K d ⊣⊢ ownT i e' K' d.
Proof.
rewrite /ownT. intros →. auto.
Qed.
Lemma ownT_ownT_ectx i K e d:
refine.ownT _ i ((fill K e, d) : delayed_expr _) ⊣⊢ ownT i e K d.
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 d e' K' d':
(ownT i e K d ★ ownT i' e' K' d') ⊣⊢ (⧆■(i ≠ i') ★ ownT i e K d ★ ownT i' e' K' d').
Proof. rewrite -?ownT_ownT_ectx. apply refine.ownT_ownT. Qed.
Lemma ownT_fill i e K K' d: ownT i (fill K e) K' d ⊣⊢ ownT i e (comp_ectx K' K) d.
Proof. apply ownT_equiv; auto using fill_comp. Qed.
Lemma ownT_focus i e K K' d: ownT i (fill K e) K' d ⊢ ownT i e (comp_ectx K' K) d.
Proof. rewrite ownT_fill; auto. Qed.
Lemma ownT_unfocus i e K d: ownT i e K d ⊢ ownT i (fill K e) empty_ectx d.
Proof. rewrite ownT_equiv; eauto using fill_empty. Qed.
Lemma prim_step_nofork_ectx_aux K d d' N e sσ e' sσ':
nsteps (prim_step_nofork _) N (e, sσ) (e', sσ') →
match N with
| 0 ⇒ d' ≤ d
| S _ ⇒ d' ≤ Kd
end →
∃ N', N' = match N with
| 0 ⇒ d - d'
| S N ⇒ S d + (N × (S Kd)) + (Kd - d')
end
∧ nsteps (prim_step_nofork (delayed_lang _ Kd Fd)) N'
((fill K e, d), sσ)
((fill K e', d'), 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' d d'.
induction Hnsteps; intros; subst.
- simpl. ∃ (d - d').
split; trivial.
inversion Heq_c'; subst.
assert (∃ k, d = d' + k) as (k&->).
{ ∃ (d - d'). omega. }
replace (d' + k - d') with k by omega.
clear; induction k.
× replace (d' + 0) with d' by omega.
econstructor; eauto.
× econstructor; eauto.
replace (d' + S k) with (S (d' + k)) by omega.
econstructor.
- eexists; split; eauto.
induction d.
× simpl. rewrite /prim_step_nofork in H0.
eapply (nsteps_l _ _ _ ((fill K (fst y), Kd), snd y)); eauto.
** rewrite /prim_step_nofork. simpl.
replace (None: option (delayed_expr _)) with
(default None None (λ e, Some (e, @fresh_delay (ectx_lang expr) Fd e))) by auto.
econstructor; eauto using fill_step.
** destruct n as [| n].
*** simpl. simpl.
destruct y as (e1, sσ1).
specialize (IHHnsteps e1 sσ1 e' sσ' Coq.Init.Logic.eq_refl Coq.Init.Logic.eq_refl).
edestruct (IHHnsteps Kd d') as (?&?&?); eauto.
subst. eauto.
*** replace (S n × S Kd + (Kd - d')) with
(S Kd + n × S Kd + (Kd - d')) by lia.
destruct y as (e1, sσ1).
specialize (IHHnsteps e1 sσ1 e' sσ' Coq.Init.Logic.eq_refl Coq.Init.Logic.eq_refl).
edestruct (IHHnsteps Kd d') as (?&?&?); eauto.
subst. eauto.
× replace (S (S d) + n × S Kd + (Kd - d')) with
(S (S d + n × S Kd + (Kd - d'))) by omega.
econstructor; eauto.
rewrite /prim_step_nofork. simpl.
replace (None: option (delayed_expr _)) with
(default None None (λ e, Some (e, @fresh_delay (ectx_lang expr) Kd e))) by auto.
econstructor.
Qed.
Lemma prim_step_nofork_ectx K d d' N e sσ e' sσ':
nsteps (prim_step_nofork _) (S N) (e, sσ) (e', sσ') →
d ≤ Kd →
d' ≤ Kd →
∃ N', 1 ≤ N' ∧ N' ≤ (S Kd) × (S (S N)) ∧ nsteps (prim_step_nofork (delayed_lang _ Kd Fd)) N'
((fill K e, d), sσ)
((fill K e', d'), sσ').
Proof.
intros. edestruct prim_step_nofork_ectx_aux as (N'&?&?); eauto.
{ simpl; eauto. }
∃ N'. subst. split_and!; eauto; lia.
Qed.
Lemma ownT_ownSP_step_nofork N' E i e K d sσ e' sσ' d':
nsteps (prim_step_nofork _) N' (e, sσ) (e', sσ') →
d ≤ Kd →
d' ≤ Kd →
(1 ≤ N' ∧ N' ≤ S Kd) →
(ownT i e K d ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K d' ★ ownSP sσ'.
Proof.
rewrite -?ownT_ownT_ectx.
intros ? ? ? (?&?).
destruct N' as [|N']; first omega.
edestruct (prim_step_nofork_ectx K d d') as (?&?&?&?); eauto.
rewrite refine.ownT_ownSP_step_nofork; eauto.
split; first omega.
etransitivity; eauto.
apply mult_le_compat_l; omega.
Qed.
Lemma ownT_ownSP_step_nofork_ctx1 K E i e d sσ e' d' sσ':
prim_step e sσ e' sσ' None →
d ≤ Kd →
d' ≤ Kd →
(ownT i e K d ★ ownSP sσ) ⊢ |={E}=>> ownT i e' K d' ★ ownSP sσ'.
Proof.
intros; eapply ownT_ownSP_step_nofork; eauto.
- econstructor; last apply nsteps_O; eauto.
- split; auto. destruct Kd; omega.
Qed.
Lemma ownT_ownSP_step_fork K E i e d sσ e' d' sσ' ef:
prim_step e sσ e' sσ' (Some ef) →
d ≤ Kd →
d' ≤ Kd →
(ownT i e K d ★ ownSP sσ)
⊢ |={E}=>> ∃ i', ownT i e' K d' ★ ownT i' ef empty_ectx (fresh_delay _ Fd ef)★ ownSP sσ'.
Proof.
iIntros (Hstep Hd Hd').
iIntros "(Hown1&Hown2)".
rewrite /ownT /ownSP /refine.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).
iPoseProof (owne_stepP refine_alt_triv _ ((refine (delayed_lang (ectx_lang expr) Kd Fd)
(Kd + 3 + Kd × (Kd + 3)) master
∅ (cs' ++ [(ts', sσ)]) ixs'))
((refine (delayed_lang (ectx_lang expr) Kd Fd)
(Kd + 3 + Kd × (Kd + 3)) snapshot
{[i]} (cs ++ [(ts, sσ0)]) ixs))) as "Hshift"; eauto.
** eapply (snap_master_fork (delayed_lang (ectx_lang expr) Kd Fd) (S Kd × (Kd + 3)) i
d (Kd - d') (fill K e, d) (fill K e, 0)
(ef, fresh_delay _ Fd ef) (fill K e', Kd)
(fill K e', d') ts ts' sσ0 sσ sσ sσ' sσ'); eauto.
*** cut ( S (d + (Kd - d')) ≤ S Kd × (Kd + 3)); first omega.
transitivity (S (Kd + Kd)); first by omega.
clear. induction Kd; lia.
*** clear. induction d; first econstructor.
econstructor; last eapply IHd; eauto; econstructor.
*** eapply (base_step _ Kd Fd _ _ _ _ (Some ef)); eauto.
apply fill_step. eauto.
***
assert (∃ k, k + d' = Kd) as (k&Heqk); first (∃ (Kd - d'); omega).
replace (Kd - d') with k; last omega.
replace (fill K e', Kd, sσ') with (fill K e', k + d', sσ'); last f_equal; auto.
clear Heqk.
induction k.
**** simpl. econstructor.
**** replace (S k + d') with (S (k + d')); last omega.
eapply nsteps_l; last eapply IHk.
econstructor; auto.
** 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.
rewrite fill_empty pure_equiv //= -emp_True; auto.
**** apply affine_intro; first apply _. iExists ts'', cs'', ixs''; auto.
Qed.
Lemma ownT_ownSP_delay E i e K d d' sσ:
1 ≤ d - d' ∧ d - d' ≤ S Kd →
(ownT i e K d ★ ownSP sσ) ⊢ |={E}=>> ownT i e K d' ★ ownSP sσ.
Proof.
rewrite -?ownT_ownT_ectx; intros (?&Hle).
rewrite (refine.ownT_ownSP_step_nofork _ (d - d')); eauto.
- assert (∃ k, k + d' = d) as (k&Heq).
{ ∃ (d - d'). omega. }
replace (d - d') with k by omega.
replace (d - d') with k by omega.
rewrite -Heq. clear Heq.
induction k.
× econstructor.
× replace (S k + d') with (S (k + d')) by omega. econstructor; eauto.
econstructor.
- split; auto. clear -Hle. induction Kd; first lia; lia.
Qed.
Lemma ownT_ownSP_delay1 E i e K d sσ:
(ownT i e K (S d) ★ ownSP sσ) ⊢ |={E}=>> ownT i e K d ★ ownSP sσ.
Proof.
eapply ownT_ownSP_delay.
split; omega.
Qed.
Lemma ownT_val_stopped i v P:
(ownT i (of_val v) empty_ectx 0 ★ ⧆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) d e (sσ: state) σ Φ:
{{ ownT 0 E empty_ectx d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} ⊢
{{ refine.ownT (delayed_lang (ectx_lang expr) Kd Fd) 0 (E, d) ★ ownP σ
★ refine.ownSP (delayed_lang (ectx_lang expr) Kd Fd) sσ }}
e
{{ v, (∃ V, refine.ownT (delayed_lang (ectx_lang expr) Kd Fd) 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) d 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 d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} →
∃ l' V T2 sσ2,
isteps (@idx_step (delayed_lang (ectx_lang expr) Kd Fd)) l'
([(E, d)], sσ) (of_val V :: T2, sσ2) ∧
(∀ i, ¬ (enabled (@idx_step (delayed_lang (ectx_lang expr) Kd Fd)) (of_val V :: T2, sσ2)) i) ∧
Φ v V.
Proof.
rewrite ht_equiv_ectx. intros.
edestruct (@refine.ht_adequacy_refine' (delayed_lang (ectx_lang expr) Kd Fd)); eauto.
× eapply delayed_lang_det; eauto.
× eapply delayed_lang_dec; eauto.
Qed.
Lemma ht_adequacy_inf_refine' (E: expr) d e (sσ: state) σ Φ
(tr: trace idx_step ([e], σ)):
{{ ownT 0 E empty_ectx d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} →
∃ (tr': trace (@idx_step (delayed_lang (ectx_lang expr) Kd Fd))
([(E, d)], sσ)), fair_pres _ _ tr tr'.
Proof.
rewrite ht_equiv_ectx. intros.
eapply (@refine.ht_adequacy_inf_refine' (delayed_lang (ectx_lang expr) Kd Fd)); eauto.
× eapply delayed_lang_det; eauto.
× eapply delayed_lang_dec; eauto.
Qed.
Lemma ht_safe_refine e σ E d sσ Φ:
{{ ownT 0 E empty_ectx d ★ ownP σ ★ ownSP sσ }}
e
{{ v, (∃ V, ownT 0 (of_val V) empty_ectx 0 ★ ⧆■ Φ v V) }} →
safe_refine Φ e σ E sσ.
Proof.
rewrite ht_equiv_ectx.
intros. eapply delayed_lang_safe_refine.
eapply (@refine.ht_safe_refine (delayed_lang (ectx_lang expr) Kd Fd)); eauto.
× eapply delayed_lang_det; eauto.
× eapply delayed_lang_dec; eauto.
Qed.
End refine_adequacy.
End refine_ectx.