Library iris.program_logic.adequacy
From iris.prelude Require Export irelations.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import wsat ownership.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Section adequacy.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
Implicit Types Φs : list (val Λ → iProp Λ Σ).
Implicit Types m : iGst Λ Σ.
Inductive idx_stepN {M: cmraT} (n: nat) (i: nat) (ρ1 ρ2 : list M) : Prop :=
| idx_stepN_atomic r1 r2 t1 t2 t1' t2' :
ρ1 = (t1 ++ r1 :: t2) →
ρ2 = (t1' ++ r2 :: t2') →
stepN n r1 r2 →
length t1 = i →
t1 ≡ t1' →
t2 ≡ t2' →
idx_stepN n i ρ1 ρ2
| idx_stepN_fork r1 r2 rf t1 t2 t1' t2':
ρ1 = (t1 ++ r1 :: t2) →
ρ2 = (t1' ++ r2 :: t2' ++ [rf]) →
stepN n r1 (r2 ⋅ rf) →
length t1 = i →
t1 ≡ t1' →
t2 ≡ t2' →
idx_stepN n i ρ1 ρ2.
Lemma idx_stepN_le {M: cmraT}:
∀ n n' i (rs1 rs2: list M),
n' ≤ n →
idx_stepN n i rs1 rs2 →
idx_stepN n' i rs1 rs2.
Proof.
intros n n' i rs1 rs2 Hlt.
induction 1; econstructor; eauto; eapply cmra_stepN_le; eauto.
Qed.
Lemma isteps_idx_stepN_le {M: cmraT}:
∀ n n' l (rs1 rs2: list M),
n' ≤ n →
isteps (idx_stepN n) l rs1 rs2 →
isteps (idx_stepN n') l rs1 rs2.
Proof.
intros ? ? ? ? ? Hlt. induction 1; econstructor; eauto.
eapply idx_stepN_le; eauto.
Qed.
Lemma isteps_aux'_idx_stepN_le {M: cmraT}:
∀ n n' l (rs1 rs2: list M),
n' ≤ n →
isteps_aux' (idx_stepN n) l rs1 rs2 →
isteps_aux' (idx_stepN n') l rs1 rs2.
Proof.
intros ? ? ? ? ? Hlt. induction 1; econstructor; eauto.
eapply idx_stepN_le; eauto.
Qed.
Notation wptp n := (Forall4 (λ e Φ r rl, uPred_holds (wp ⊤ e Φ) n r rl)).
Notation estop Φs :=
(Forall (λ Φ, (∀ v, upred.uPred_entails (Φ v) upred.uPred_stopped)) Φs).
Lemma wptp_le Φs es rs robs n n' :
✓{n'} (big_op rs) → ✓{n'} (big_op robs) →
wptp n es Φs rs robs → n' ≤ n → wptp n' es Φs rs robs.
Proof. induction 3; constructor; eauto 10 using uPred_closed. Qed.
Lemma isteps_wptp Φs l n tσ1 tσ2 robs1 rs1 rf0:
isteps idx_step l tσ1 tσ2 →
1 < n → wptp (length l + n) (tσ1.1) Φs rs1 robs1 →
wsat (length l + n) ⊤ (tσ1.2) (big_op rs1 ⋅ rf0) (big_op robs1) →
∃ l' robs2 rs2 Φs', wptp n (tσ2.1) (Φs ++ Φs') rs2 robs2
∧ wsat n ⊤ (tσ2.2) (big_op rs2 ⋅ rf0) (big_op robs2)
∧ isteps_aux' (idx_stepN n) l' robs1 robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{n} (big_op rs)) (map fst l')
∧ estop Φs'.
Proof.
intros Hsteps Hn; revert Φs robs1 rs1 rf0.
induction Hsteps as [|i l ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH];
simplify_eq/=; intros Φs robs rs rf0.
{ intros. ∃ [], robs, rs, []. rewrite ?right_id_L.
split_and!; eauto;
try econstructor.
}
intros (Φs1&?&rs1&?&robs1&?&->&->&->&?&
(Φ&Φs2&r&rs2&rob&robs2&->&->&->&Hwp&?
)%Forall4_cons_inv_l)%Forall4_app_inv_l
Hwe.
rewrite wp_eq in Hwp.
destruct (wp_step_inv ⊤ ∅ Φ e1 (length l + n) (S (length l + n)) σ1 r rob
(big_op (rs1 ++ rs2) ⋅ rf0) (big_op (robs1 ++ robs2))) as [_ Hwpstep]; eauto using val_stuck.
{ rewrite right_id_L.
rewrite -?Permutation_middle in Hwe ×.
by rewrite -(assoc _ _ (big_op (rs1 ++ rs2))).
}
destruct (Hwpstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&Hwsat&?&?&?&Hrs); auto; clear Hwpstep.
revert Hwsat; rewrite big_op_app right_id_L⇒Hwsat.
destruct ef as [e'|].
- destruct (IH (Φs1 ++ Φ :: Φs2 ++ [λ _, uPred_stopped%I])
(robs1 ++ rob2 :: robs2 ++ [rob2'])
(rs1 ++ r2 :: rs2 ++ [r2']) rf0) as (l'&robs'&rs'&Φs'&?&?&?&?&?&?).
{
apply Forall4_app, Forall4_cons,
Forall4_app, Forall4_cons, Forall4_nil; eauto using wptp_le; [| | |];
try (rewrite wp_eq; eauto; done).
× eapply wptp_le; eauto.
eapply wsat_valid in Hwe; auto.
rewrite ?big_op_app in Hwe ×.
simpl. auto.
× eapply wptp_le; eauto.
eapply wsat_valid in Hwe; auto.
rewrite ?big_op_app in Hwe ×.
simpl. auto.
}
{
rewrite -?Permutation_middle.
simpl; rewrite ?right_id_L.
rewrite assoc (assoc _ (rob2)).
rewrite -(assoc _ _ (big_op (rs1 ++ rs2))).
rewrite ?big_op_app in Hwsat ×.
eauto.
}
∃ ((robs1 ++ rob :: robs2, length t1) :: l'), robs', rs',
([λ _, uPred_stopped %I] ++ Φs'); split_and!; auto.
× by rewrite (assoc _ _ _ Φs') -(assoc _ Φs1).
× econstructor; eauto.
eapply (idx_stepN_fork n (length t1) _ _ rob rob2 rob2' robs1 robs2); eauto.
eapply cmra_stepN_le; eauto.
symmetry; eapply Forall4_length_lrr; eauto.
× simpl. subst. auto.
× rewrite map_cons. econstructor; simpl; auto.
× eapply Forall_app; split; auto.
- assert (rob2' ≡{length l + n}≡ ∅) as Hempty by auto.
destruct (IH (Φs1 ++ Φ :: Φs2) (robs1 ++ rob2 :: robs2)
(rs1 ++ r2 ⋅ r2' :: rs2) (rf0)) as (l'&robs'&rs'&Φs'&?&?&?&?&?&?).
{ rewrite /option_list right_id_L.
apply Forall4_app, Forall4_cons; eauto using wptp_le.
× eapply wptp_le; eauto. rewrite ?big_op_app in Hwsat ×. eauto.
× rewrite wp_eq.
apply uPred_mono with r2 rob2; eauto using cmra_includedN_l.
× eapply wptp_le; eauto. rewrite ?big_op_app in Hwsat ×. eauto.
}
{
rewrite Hempty right_id in Hwsat ×.
by rewrite -?Permutation_middle /= ?big_op_app ?assoc.
}
∃ ((robs1 ++ rob :: robs2, length t1) :: l'), robs', rs', Φs'; split_and!; auto.
× rewrite Hempty in Hrs ×. rewrite right_id. intros.
econstructor; [| eauto]. econstructor; eauto.
eapply cmra_stepN_le; eauto; omega.
symmetry; eapply Forall4_length_lrr; eauto.
× simpl. subst. auto.
× simpl. econstructor; eauto.
Qed.
Lemma ht_adequacy_steps P Φ l n e1 t2 σ1 σ2 rob1 r1 rf0:
{{ P }} e1 {{ Φ }} →
isteps idx_step l ([e1],σ1) (t2,σ2) →
1 < n → wsat (length l + n) ⊤ σ1 (r1 ⋅ rf0) rob1 →
P (length l + n) r1 rob1 →
∃ l' robs2 rs2 Φs', wptp n t2 (Φ :: Φs') rs2 robs2
∧ wsat n ⊤ σ2 (big_op rs2 ⋅ rf0) (big_op robs2)
∧ isteps_aux' (idx_stepN n) l' [rob1] robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{n} (big_op rs)) (map fst l')
∧ estop Φs'.
Proof.
intros Hht ????; apply (isteps_wptp [Φ] l n ([e1],σ1) (t2,σ2) [rob1] [r1]);
rewrite /big_op ?right_id; auto.
constructor; last constructor.
rewrite /ht in Hht.
rewrite uPred.relevant_elim uPred.affine_elim in Hht *=>Hht.
eapply uPred.wand_elim_l' in Hht.
rewrite left_id in Hht *=>Hht.
eapply Hht; eauto.
Qed.
Lemma ht_adequacy_own Φ l e1 t2 σ1 m1 m2 σ2 n:
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e1 {{ Φ }} →
isteps idx_step l ([e1],σ1) (t2,σ2) →
∃ l' robs2 rs2 Φs', wptp n t2 (Φ :: Φs') rs2 robs2
∧ wsat n ⊤ σ2 (big_op rs2) (big_op robs2)
∧ isteps_aux' (idx_stepN n) l' [Res ∅ ∅ m1] robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{n} (big_op rs)) (map fst l')
∧ estop Φs'.
Proof.
intros.
cut (∃ l' robs2 rs2 Φs', wptp (S (S n)) t2 (Φ :: Φs') rs2 robs2
∧ wsat (S (S n)) ⊤ σ2 (big_op rs2 ⋅ ∅) (big_op robs2)
∧ isteps_aux' (idx_stepN (S (S n))) l' [Res ∅ ∅ m1] robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{S (S n)} (big_op rs)) (map fst l')
∧ estop Φs').
{
intros (l'&robs2&rs2&Φs'&?&?Hwsat&?&<-&Hf&?).
rewrite right_id in Hwsat ×.
do 4 eexists; split_and!; eauto using wptp_le, wsat_le, isteps_aux'_idx_stepN_le.
eapply wptp_le; eauto.
clear -Hf. induction Hf; eauto.
}
assert (1 < S (S n)) by omega.
eapply ht_adequacy_steps with
(r1 := (Res ∅ (Excl' σ1) m2))
(rob1 := (Res ∅ ∅ m1))
(rf0 := ∅); eauto.
{ replace (length l + (S (S n))) with (S (S (length l + n))) by omega.
rewrite /op /cmra_op /= /res_op //= ?right_id
/op /cmra_op /= /option_op.
apply wsat_init. rewrite (comm op). by apply cmra_valid_validN.
}
uPred.unseal;
∃ (Res ∅ ∅ ∅), (Res ∅ (Excl' σ1) m2), (Res ∅ ∅ m1), (∅ : iRes Λ Σ); split_and?.
- by rewrite Res_op ?left_id ?right_id.
- by rewrite Res_op ?left_id ?right_id.
- by apply ownGl_spec.
- rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
∃ (Res ∅ (Excl' σ1) ∅), (Res ∅ ∅ m2), (∅: iRes Λ Σ), (∅: iRes Λ Σ); split_and?.
× by rewrite Res_op ?left_id ?right_id.
× by rewrite Res_op ?left_id ?right_id.
× rewrite /uPred_holds //= /uPred_holds //=.
× by apply ownG_spec.
Qed.
Theorem ht_adequacy_result E φ l e v t2 σ1 m1 m2 σ2 n:
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e @ E {{ λ v', ■ φ v' }} →
isteps idx_step l ([e], σ1) (of_val v :: t2, σ2) →
φ v ∧
∃ (rob : iRes Λ Σ) robs2, isteps (idx_stepN n) l [Res ∅ ∅ m1] (rob :: robs2).
Proof.
intros Hv ? Hs.
cut (φ v ∧ ∃ (rob: iRes Λ Σ) robs2, isteps (idx_stepN (S (S n))) l [Res ∅ ∅ m1] (rob :: robs2) ∧
✓{ S (S n) } rob).
{
intros (?&?&?&?&?&?); split; auto.
do 2 eexists; eauto using isteps_idx_stepN_le, upred.uPred_closed.
}
destruct (ht_adequacy_own (λ v', ■ φ v')%I l e (of_val v :: t2) σ1 m1 m2 σ2 (S (S n)))
as (l'&robs2&rs2&Qs&Hwptp&?&?&?&?&?); auto.
{ by rewrite -(ht_mask_weaken E ⊤). }
inversion Hwptp as [|?? r rob ?? rs robs Hwp]. clear Hwptp; subst.
move: Hwp. rewrite wp_eq. uPred.unseal⇒ /wp_value_inv Hwp.
rewrite pvs_eq in Hwp.
destruct (Hwp (S (S n)) ∅ σ2 (big_op rs) (big_op robs)) as
[r' (Hconj&?)]; rewrite ?right_id_L; auto.
split; auto.
∃ rob, robs. split; eauto using isteps_aux'_erase.
Qed.
Lemma ht_adequacy_reducible E Φ l e1 e2 t2 σ1 m1 m2 σ2 :
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e1 @ E {{ Φ }} →
isteps idx_step l ([e1], σ1) (t2, σ2) →
e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
Proof.
intros Hv ? Hs [i ?]%elem_of_list_lookup He.
destruct (ht_adequacy_own Φ l e1 t2 σ1 m1 m2 σ2 2) as (l'&robs2&rs2&Φs&?&?&?&?); auto.
{ by rewrite -(ht_mask_weaken E ⊤). }
destruct (Forall4_lookup_l (λ e Φ r rob, wp ⊤ e Φ 2 r rob) t2
(Φ :: Φs) rs2 robs2 i e2) as (Φ'&r2&rob2&?&?&?&Hwp); auto.
destruct (wp_step_inv ⊤ ∅ Φ' e2 1 2 σ2 r2 rob2
(big_op (delete i rs2)) (big_op (delete i robs2))); auto;
first by rewrite -wp_eq.
by rewrite ?right_id_L ?big_op_delete.
Qed.
Theorem ht_adequacy_safe E Φ l e1 t2 σ1 m1 m2 σ2 :
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e1 @ E {{ Φ }} →
isteps idx_step l ([e1], σ1) (t2, σ2) →
Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
intros.
destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
destruct (ht_adequacy_reducible E Φ l e1 e2 t2 σ1 m1 m2 σ2) as (e3&σ3&ef&?);
rewrite ?eq_None_not_Some; auto.
destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
right; ∃ (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
Qed.
End adequacy.
From iris.program_logic Require Export hoare.
From iris.program_logic Require Import wsat ownership.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 100 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
Section adequacy.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
Implicit Types Φs : list (val Λ → iProp Λ Σ).
Implicit Types m : iGst Λ Σ.
Inductive idx_stepN {M: cmraT} (n: nat) (i: nat) (ρ1 ρ2 : list M) : Prop :=
| idx_stepN_atomic r1 r2 t1 t2 t1' t2' :
ρ1 = (t1 ++ r1 :: t2) →
ρ2 = (t1' ++ r2 :: t2') →
stepN n r1 r2 →
length t1 = i →
t1 ≡ t1' →
t2 ≡ t2' →
idx_stepN n i ρ1 ρ2
| idx_stepN_fork r1 r2 rf t1 t2 t1' t2':
ρ1 = (t1 ++ r1 :: t2) →
ρ2 = (t1' ++ r2 :: t2' ++ [rf]) →
stepN n r1 (r2 ⋅ rf) →
length t1 = i →
t1 ≡ t1' →
t2 ≡ t2' →
idx_stepN n i ρ1 ρ2.
Lemma idx_stepN_le {M: cmraT}:
∀ n n' i (rs1 rs2: list M),
n' ≤ n →
idx_stepN n i rs1 rs2 →
idx_stepN n' i rs1 rs2.
Proof.
intros n n' i rs1 rs2 Hlt.
induction 1; econstructor; eauto; eapply cmra_stepN_le; eauto.
Qed.
Lemma isteps_idx_stepN_le {M: cmraT}:
∀ n n' l (rs1 rs2: list M),
n' ≤ n →
isteps (idx_stepN n) l rs1 rs2 →
isteps (idx_stepN n') l rs1 rs2.
Proof.
intros ? ? ? ? ? Hlt. induction 1; econstructor; eauto.
eapply idx_stepN_le; eauto.
Qed.
Lemma isteps_aux'_idx_stepN_le {M: cmraT}:
∀ n n' l (rs1 rs2: list M),
n' ≤ n →
isteps_aux' (idx_stepN n) l rs1 rs2 →
isteps_aux' (idx_stepN n') l rs1 rs2.
Proof.
intros ? ? ? ? ? Hlt. induction 1; econstructor; eauto.
eapply idx_stepN_le; eauto.
Qed.
Notation wptp n := (Forall4 (λ e Φ r rl, uPred_holds (wp ⊤ e Φ) n r rl)).
Notation estop Φs :=
(Forall (λ Φ, (∀ v, upred.uPred_entails (Φ v) upred.uPred_stopped)) Φs).
Lemma wptp_le Φs es rs robs n n' :
✓{n'} (big_op rs) → ✓{n'} (big_op robs) →
wptp n es Φs rs robs → n' ≤ n → wptp n' es Φs rs robs.
Proof. induction 3; constructor; eauto 10 using uPred_closed. Qed.
Lemma isteps_wptp Φs l n tσ1 tσ2 robs1 rs1 rf0:
isteps idx_step l tσ1 tσ2 →
1 < n → wptp (length l + n) (tσ1.1) Φs rs1 robs1 →
wsat (length l + n) ⊤ (tσ1.2) (big_op rs1 ⋅ rf0) (big_op robs1) →
∃ l' robs2 rs2 Φs', wptp n (tσ2.1) (Φs ++ Φs') rs2 robs2
∧ wsat n ⊤ (tσ2.2) (big_op rs2 ⋅ rf0) (big_op robs2)
∧ isteps_aux' (idx_stepN n) l' robs1 robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{n} (big_op rs)) (map fst l')
∧ estop Φs'.
Proof.
intros Hsteps Hn; revert Φs robs1 rs1 rf0.
induction Hsteps as [|i l ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH];
simplify_eq/=; intros Φs robs rs rf0.
{ intros. ∃ [], robs, rs, []. rewrite ?right_id_L.
split_and!; eauto;
try econstructor.
}
intros (Φs1&?&rs1&?&robs1&?&->&->&->&?&
(Φ&Φs2&r&rs2&rob&robs2&->&->&->&Hwp&?
)%Forall4_cons_inv_l)%Forall4_app_inv_l
Hwe.
rewrite wp_eq in Hwp.
destruct (wp_step_inv ⊤ ∅ Φ e1 (length l + n) (S (length l + n)) σ1 r rob
(big_op (rs1 ++ rs2) ⋅ rf0) (big_op (robs1 ++ robs2))) as [_ Hwpstep]; eauto using val_stuck.
{ rewrite right_id_L.
rewrite -?Permutation_middle in Hwe ×.
by rewrite -(assoc _ _ (big_op (rs1 ++ rs2))).
}
destruct (Hwpstep e2 σ2 ef) as (r2&r2'&rob2&rob2'&Hwsat&?&?&?&Hrs); auto; clear Hwpstep.
revert Hwsat; rewrite big_op_app right_id_L⇒Hwsat.
destruct ef as [e'|].
- destruct (IH (Φs1 ++ Φ :: Φs2 ++ [λ _, uPred_stopped%I])
(robs1 ++ rob2 :: robs2 ++ [rob2'])
(rs1 ++ r2 :: rs2 ++ [r2']) rf0) as (l'&robs'&rs'&Φs'&?&?&?&?&?&?).
{
apply Forall4_app, Forall4_cons,
Forall4_app, Forall4_cons, Forall4_nil; eauto using wptp_le; [| | |];
try (rewrite wp_eq; eauto; done).
× eapply wptp_le; eauto.
eapply wsat_valid in Hwe; auto.
rewrite ?big_op_app in Hwe ×.
simpl. auto.
× eapply wptp_le; eauto.
eapply wsat_valid in Hwe; auto.
rewrite ?big_op_app in Hwe ×.
simpl. auto.
}
{
rewrite -?Permutation_middle.
simpl; rewrite ?right_id_L.
rewrite assoc (assoc _ (rob2)).
rewrite -(assoc _ _ (big_op (rs1 ++ rs2))).
rewrite ?big_op_app in Hwsat ×.
eauto.
}
∃ ((robs1 ++ rob :: robs2, length t1) :: l'), robs', rs',
([λ _, uPred_stopped %I] ++ Φs'); split_and!; auto.
× by rewrite (assoc _ _ _ Φs') -(assoc _ Φs1).
× econstructor; eauto.
eapply (idx_stepN_fork n (length t1) _ _ rob rob2 rob2' robs1 robs2); eauto.
eapply cmra_stepN_le; eauto.
symmetry; eapply Forall4_length_lrr; eauto.
× simpl. subst. auto.
× rewrite map_cons. econstructor; simpl; auto.
× eapply Forall_app; split; auto.
- assert (rob2' ≡{length l + n}≡ ∅) as Hempty by auto.
destruct (IH (Φs1 ++ Φ :: Φs2) (robs1 ++ rob2 :: robs2)
(rs1 ++ r2 ⋅ r2' :: rs2) (rf0)) as (l'&robs'&rs'&Φs'&?&?&?&?&?&?).
{ rewrite /option_list right_id_L.
apply Forall4_app, Forall4_cons; eauto using wptp_le.
× eapply wptp_le; eauto. rewrite ?big_op_app in Hwsat ×. eauto.
× rewrite wp_eq.
apply uPred_mono with r2 rob2; eauto using cmra_includedN_l.
× eapply wptp_le; eauto. rewrite ?big_op_app in Hwsat ×. eauto.
}
{
rewrite Hempty right_id in Hwsat ×.
by rewrite -?Permutation_middle /= ?big_op_app ?assoc.
}
∃ ((robs1 ++ rob :: robs2, length t1) :: l'), robs', rs', Φs'; split_and!; auto.
× rewrite Hempty in Hrs ×. rewrite right_id. intros.
econstructor; [| eauto]. econstructor; eauto.
eapply cmra_stepN_le; eauto; omega.
symmetry; eapply Forall4_length_lrr; eauto.
× simpl. subst. auto.
× simpl. econstructor; eauto.
Qed.
Lemma ht_adequacy_steps P Φ l n e1 t2 σ1 σ2 rob1 r1 rf0:
{{ P }} e1 {{ Φ }} →
isteps idx_step l ([e1],σ1) (t2,σ2) →
1 < n → wsat (length l + n) ⊤ σ1 (r1 ⋅ rf0) rob1 →
P (length l + n) r1 rob1 →
∃ l' robs2 rs2 Φs', wptp n t2 (Φ :: Φs') rs2 robs2
∧ wsat n ⊤ σ2 (big_op rs2 ⋅ rf0) (big_op robs2)
∧ isteps_aux' (idx_stepN n) l' [rob1] robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{n} (big_op rs)) (map fst l')
∧ estop Φs'.
Proof.
intros Hht ????; apply (isteps_wptp [Φ] l n ([e1],σ1) (t2,σ2) [rob1] [r1]);
rewrite /big_op ?right_id; auto.
constructor; last constructor.
rewrite /ht in Hht.
rewrite uPred.relevant_elim uPred.affine_elim in Hht *=>Hht.
eapply uPred.wand_elim_l' in Hht.
rewrite left_id in Hht *=>Hht.
eapply Hht; eauto.
Qed.
Lemma ht_adequacy_own Φ l e1 t2 σ1 m1 m2 σ2 n:
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e1 {{ Φ }} →
isteps idx_step l ([e1],σ1) (t2,σ2) →
∃ l' robs2 rs2 Φs', wptp n t2 (Φ :: Φs') rs2 robs2
∧ wsat n ⊤ σ2 (big_op rs2) (big_op robs2)
∧ isteps_aux' (idx_stepN n) l' [Res ∅ ∅ m1] robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{n} (big_op rs)) (map fst l')
∧ estop Φs'.
Proof.
intros.
cut (∃ l' robs2 rs2 Φs', wptp (S (S n)) t2 (Φ :: Φs') rs2 robs2
∧ wsat (S (S n)) ⊤ σ2 (big_op rs2 ⋅ ∅) (big_op robs2)
∧ isteps_aux' (idx_stepN (S (S n))) l' [Res ∅ ∅ m1] robs2
∧ map snd l' = l
∧ Forall (λ rs, ✓{S (S n)} (big_op rs)) (map fst l')
∧ estop Φs').
{
intros (l'&robs2&rs2&Φs'&?&?Hwsat&?&<-&Hf&?).
rewrite right_id in Hwsat ×.
do 4 eexists; split_and!; eauto using wptp_le, wsat_le, isteps_aux'_idx_stepN_le.
eapply wptp_le; eauto.
clear -Hf. induction Hf; eauto.
}
assert (1 < S (S n)) by omega.
eapply ht_adequacy_steps with
(r1 := (Res ∅ (Excl' σ1) m2))
(rob1 := (Res ∅ ∅ m1))
(rf0 := ∅); eauto.
{ replace (length l + (S (S n))) with (S (S (length l + n))) by omega.
rewrite /op /cmra_op /= /res_op //= ?right_id
/op /cmra_op /= /option_op.
apply wsat_init. rewrite (comm op). by apply cmra_valid_validN.
}
uPred.unseal;
∃ (Res ∅ ∅ ∅), (Res ∅ (Excl' σ1) m2), (Res ∅ ∅ m1), (∅ : iRes Λ Σ); split_and?.
- by rewrite Res_op ?left_id ?right_id.
- by rewrite Res_op ?left_id ?right_id.
- by apply ownGl_spec.
- rewrite /ownP; uPred.unseal; rewrite /uPred_holds //=.
∃ (Res ∅ (Excl' σ1) ∅), (Res ∅ ∅ m2), (∅: iRes Λ Σ), (∅: iRes Λ Σ); split_and?.
× by rewrite Res_op ?left_id ?right_id.
× by rewrite Res_op ?left_id ?right_id.
× rewrite /uPred_holds //= /uPred_holds //=.
× by apply ownG_spec.
Qed.
Theorem ht_adequacy_result E φ l e v t2 σ1 m1 m2 σ2 n:
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e @ E {{ λ v', ■ φ v' }} →
isteps idx_step l ([e], σ1) (of_val v :: t2, σ2) →
φ v ∧
∃ (rob : iRes Λ Σ) robs2, isteps (idx_stepN n) l [Res ∅ ∅ m1] (rob :: robs2).
Proof.
intros Hv ? Hs.
cut (φ v ∧ ∃ (rob: iRes Λ Σ) robs2, isteps (idx_stepN (S (S n))) l [Res ∅ ∅ m1] (rob :: robs2) ∧
✓{ S (S n) } rob).
{
intros (?&?&?&?&?&?); split; auto.
do 2 eexists; eauto using isteps_idx_stepN_le, upred.uPred_closed.
}
destruct (ht_adequacy_own (λ v', ■ φ v')%I l e (of_val v :: t2) σ1 m1 m2 σ2 (S (S n)))
as (l'&robs2&rs2&Qs&Hwptp&?&?&?&?&?); auto.
{ by rewrite -(ht_mask_weaken E ⊤). }
inversion Hwptp as [|?? r rob ?? rs robs Hwp]. clear Hwptp; subst.
move: Hwp. rewrite wp_eq. uPred.unseal⇒ /wp_value_inv Hwp.
rewrite pvs_eq in Hwp.
destruct (Hwp (S (S n)) ∅ σ2 (big_op rs) (big_op robs)) as
[r' (Hconj&?)]; rewrite ?right_id_L; auto.
split; auto.
∃ rob, robs. split; eauto using isteps_aux'_erase.
Qed.
Lemma ht_adequacy_reducible E Φ l e1 e2 t2 σ1 m1 m2 σ2 :
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e1 @ E {{ Φ }} →
isteps idx_step l ([e1], σ1) (t2, σ2) →
e2 ∈ t2 → to_val e2 = None → reducible e2 σ2.
Proof.
intros Hv ? Hs [i ?]%elem_of_list_lookup He.
destruct (ht_adequacy_own Φ l e1 t2 σ1 m1 m2 σ2 2) as (l'&robs2&rs2&Φs&?&?&?&?); auto.
{ by rewrite -(ht_mask_weaken E ⊤). }
destruct (Forall4_lookup_l (λ e Φ r rob, wp ⊤ e Φ 2 r rob) t2
(Φ :: Φs) rs2 robs2 i e2) as (Φ'&r2&rob2&?&?&?&Hwp); auto.
destruct (wp_step_inv ⊤ ∅ Φ' e2 1 2 σ2 r2 rob2
(big_op (delete i rs2)) (big_op (delete i robs2))); auto;
first by rewrite -wp_eq.
by rewrite ?right_id_L ?big_op_delete.
Qed.
Theorem ht_adequacy_safe E Φ l e1 t2 σ1 m1 m2 σ2 :
valid (m1 ⋅ m2) →
{{ ownGl m1 ★ ownP σ1 ★ ownG m2 }} e1 @ E {{ Φ }} →
isteps idx_step l ([e1], σ1) (t2, σ2) →
Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
Proof.
intros.
destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
destruct (ht_adequacy_reducible E Φ l e1 e2 t2 σ1 m1 m2 σ2) as (e3&σ3&ef&?);
rewrite ?eq_None_not_Some; auto.
destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
right; ∃ (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto.
Qed.
End adequacy.