Library iris.program_logic.language
From iris.algebra Require Export cofe step.
From iris.prelude Require Import irelations.
Structure language := Language {
expr : Type;
val : Type;
state : Type;
of_val : val → expr;
to_val : expr → option val;
prim_step : expr → state → expr → state → option expr → Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v → of_val v = e;
val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None
}.
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _.
Arguments to_of_val {_} _.
Arguments of_to_val {_} _ _ _.
Arguments val_stuck {_} _ _ _ _ _ _.
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (expr Λ).
Global Instance stateC_step Σ: StepN (state Σ) := trivial_stepN.
Global Instance stateC_ustep Σ: uStep (stateC Σ) := trivial_stepN_ustep.
Definition cfg (Λ : language) := (list (expr Λ) × state Λ)%type.
Section language.
Context {Λ : language}.
Implicit Types v : val Λ.
Definition reducible (e : expr Λ) (σ : state Λ) :=
∃ e' σ' ef, prim_step e σ e' σ' ef.
Definition atomic (e : expr Λ) : Prop :=
∀ σ e' σ' ef, prim_step e σ e' σ' ef → is_Some (to_val e').
Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1) →
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
prim_step e1 σ1 e2 σ2 ef →
step ρ1 ρ2.
Inductive idx_step (i: nat) (ρ1 ρ2 : cfg Λ) : Prop :=
| idx_step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1) →
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
prim_step e1 σ1 e2 σ2 ef →
length t1 = i →
idx_step i ρ1 ρ2.
Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
Proof. intros <-. by rewrite to_of_val. Qed.
Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
Global Instance: Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Inductive idx_step': nat → cfg Λ → cfg Λ → Prop :=
| idx_step_alt_hd_atomic e1 σ1 e2 σ2 ef t2 :
prim_step e1 σ1 e2 σ2 ef →
idx_step' 0 (e1 :: t2, σ1) (e2 :: t2 ++ option_list ef, σ2)
| idx_step_alt_cons k e0 es1 σ1 es2 σ2:
idx_step' k (es1, σ1) (es2, σ2) →
idx_step' (S k) (e0 :: es1, σ1) (e0 :: es2, σ2).
Lemma idx_step_equiv k es1 es2:
idx_step k es1 es2 ↔ idx_step' k es1 es2.
Proof.
split; intro Hs.
- inversion Hs.
× revert k es1 es2 e1 σ1 e2 σ2 ef t2 H H0 H1 H2 Hs.
induction t1; intros. simpl in ×. subst. econstructor; eauto.
destruct k; simpl in *; try omega.
subst. econstructor.
eapply IHt1; eauto.
econstructor; eauto.
- induction Hs.
× eapply (idx_step_atomic _ _ _ _ _ _ _ _ nil); eauto.
× inversion IHHs.
inversion H. inversion H0. subst.
eapply (idx_step_atomic _ _ _ _ _ _ _ _ (e0 :: t1));
rewrite ?app_comm_cons; simpl; auto.
Qed.
Lemma idx_step_app:
∀ l (σ σ': state Λ) ts ts' i,
idx_step i (ts, σ) (ts', σ') ↔
idx_step (length l + i) (l ++ ts, σ) (l ++ ts', σ').
Proof.
intros. rewrite ?idx_step_equiv.
split.
- intros. induction l; simpl; auto; econstructor; auto.
- induction l; intros; simpl in *; auto.
inversion H. subst. eauto.
Qed.
Lemma idx_step_cons:
∀ i (σ σ': state Λ) ts ts' x,
idx_step i (ts, σ) (ts', σ') ↔
idx_step (S i) (x :: ts, σ) (x :: ts', σ').
Proof.
intros.
replace (x :: ts) with ([x] ++ ts); auto.
replace (x :: ts') with ([x] ++ ts'); auto.
replace (S i) with (length [x] + i); auto.
eapply idx_step_app.
Qed.
Lemma enabled_idx_step_cons:
∀ x l (σ: state Λ) i,
enabled idx_step (x :: l, σ) (S i)
↔ enabled idx_step (l, σ) i.
Proof.
rewrite /enabled. intros; split.
- intros (?&His).
rewrite idx_step_equiv in His ×.
intros His. inversion His. subst.
eexists; rewrite idx_step_equiv; eauto.
- intros (?&His).
rewrite idx_step_equiv in His ×.
intros His.
destruct x0 as (l', σ').
∃ (x :: l', σ'); rewrite idx_step_equiv; econstructor; eauto.
Qed.
Lemma step_idx_step ρ1 ρ2:
step ρ1 ρ2 → ∃ i, idx_step i ρ1 ρ2.
Proof.
inversion 1. ∃ (length t1).
econstructor; eauto.
Qed.
Lemma forall_not_enabled_forall_not_reducible tp σ:
(∀ i, ¬ (enabled idx_step (tp, σ) i)) →
Forall (λ e, ¬ reducible e σ) tp.
Proof.
induction tp; first econstructor.
intros Hne. econstructor.
- intros (?&?&?&?).
eapply (Hne 0). econstructor. rewrite idx_step_equiv.
econstructor; eauto.
- eapply IHtp.
intros i Hne'.
eapply (Hne (S i)).
destruct (Hne') as ((tp'&σ')&Hstep).
∃ (a :: tp', σ'). rewrite ?idx_step_equiv in Hstep *=>Hstep.
econstructor; eauto.
Qed.
Lemma Forall_values_or_some_non (tp: list (expr Λ)):
Forall (λ e, is_Some (to_val e)) tp ∨
∃ e, e ∈ tp ∧ to_val e = None.
Proof.
induction tp as [| e tp]; first left; auto.
rewrite Forall_cons.
case (decide (is_Some (to_val e))) as [l|n]; intros.
- destruct IHtp as [Hvals|(e'&Hin&?)].
** left. split; eauto.
** right. ∃ e'. split; auto; set_solver.
- right; ∃ e. split; first set_solver.
destruct (to_val e); auto.
exfalso; eapply n; eauto.
Qed.
End language.
Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
fill_not_val e :
to_val e = None → to_val (K e) = None;
fill_step e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef →
prim_step (K e1) σ1 (K e2) σ2 ef;
fill_step_inv e1' σ1 e2 σ2 ef :
to_val e1' = None → prim_step (K e1') σ1 e2 σ2 ef →
∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 ef
}.
Lemma length_cfg_idx_step:
∀ {L: language} (c c': cfg L) i, idx_step i c c' → length (fst c) ≤ length (fst c').
Proof.
intros ? ? ? ? Hidx.
inversion Hidx. subst.
repeat (rewrite ?app_length //=).
omega.
Qed.
Lemma length_cfg_idx_step':
∀ {L: language} (c c': cfg L) i, idx_step i c c' → S (length (fst c)) ≥ length (fst c').
Proof.
intros ? ? ? ? Hidx.
inversion Hidx. subst.
repeat (rewrite ?app_length //=).
destruct ef; simpl in *; omega.
Qed.
Lemma length_cfg_idx_step2:
∀ {L: language} (c c': cfg L) i, idx_step i c c' → i < length (fst c).
Proof.
intros ? ? ? ? Hidx.
inversion Hidx. subst.
repeat (rewrite ?app_length //=).
omega.
Qed.
Definition safe_refine {ΛT ΛS: language} (R: val ΛT → val ΛS → Prop)
(e: expr ΛT) (σ: state ΛT) (E: expr ΛS) (Σ: state ΛS) :=
(∀ l tp' σ', isteps idx_step l ([e], σ) (tp', σ')
→ Forall (λ e', is_Some (to_val e') ∨ reducible e' σ') tp') ∧
(∀ l v' tp' σ', isteps idx_step l ([e], σ) (of_val v' :: tp', σ')
→ Forall (λ e', is_Some (to_val e')) tp'
→ ∃ L E' TP' Σ', isteps idx_step L ([E], Σ) (E' :: TP', Σ') ∧
((∃ E'', E'' ∈ (E' :: TP') ∧ ¬ reducible E'' Σ' ∧
to_val E'' = None) ∨
(Forall (λ E'', is_Some (to_val E'')) TP' ∧
∃ V', to_val E' = Some V' ∧ R v' V'))) ∧
(∀ (t: trace idx_step ([e], σ)), weak_fair t
→ ∃ (T: trace idx_step ([E], Σ)), weak_fair T).
Definition safe_refine' {ΛT ΛS: language} (R: val ΛT → val ΛS → Prop)
(e: expr ΛT) (σ: state ΛT) (E: expr ΛS) (Σ: state ΛS) :=
(∀ l tp' σ', isteps idx_step l ([e], σ) (tp', σ')
→ Forall (λ e', is_Some (to_val e') ∨ reducible e' σ') tp') ∧
(∀ l v' tp' σ', isteps idx_step l ([e], σ) (of_val v' :: tp', σ')
→ Forall (λ e', is_Some (to_val e')) tp'
→ ∃ L V' TP' Σ', isteps idx_step L ([E], Σ) (of_val V' :: TP', Σ')
∧ Forall (λ E'', ¬ reducible E'' Σ') TP'
∧ R v' V') ∧
(∀ (t: trace idx_step ([e], σ)), weak_fair t
→ ∃ (T: trace idx_step ([E], Σ)), weak_fair T).
Lemma safe_refine'_to_safe_refine {ΛT ΛS} R (e: expr ΛT) σ (E: expr ΛS) Σ:
safe_refine' R e σ E Σ → safe_refine R e σ E Σ.
Proof.
intros (?&H2&?). split_and!; auto.
intros. edestruct H2 as (L&V'&TP'&Σ'&Histeps&Hnenabled&HR); eauto.
∃ L, (of_val V'), TP', Σ'; split_and!; auto.
edestruct (Forall_values_or_some_non TP') as [Hvalues|(E'&?&?)].
- right. split; auto. eexists; split; eauto using to_of_val.
- left. ∃ E'. split_and!; first set_solver; auto.
eapply Forall_forall in Hnenabled; eauto.
Qed.
Lemma safe_refine_trans {Λ1 Λ2 Λ3}
(R: val Λ1 → val Λ2 → Prop)
(S: val Λ2 → val Λ3 → Prop)
(T: val Λ1 → val Λ3 → Prop)
(e1: expr Λ1) σ1 (e2: expr Λ2) σ2 (e3: expr Λ3) σ3:
(∀ v1 v2 v3, R v1 v2 → S v2 v3 → T v1 v3) →
safe_refine R e1 σ1 e2 σ2 →
safe_refine S e2 σ2 e3 σ3 →
safe_refine T e1 σ1 e3 σ3.
Proof.
intros Htrans (H21&H22&H23) (H31&H32&H33).
split_and!; eauto.
- intros.
edestruct H22 as (?&e2'&?&?&Hs2&[(E&?&Hstuck&?)|(Hsteps2&v2&?&?)]); eauto.
× exfalso. eapply Hstuck.
setoid_rewrite Forall_forall in H31.
edestruct H31 as [(?&?)|?]; eauto; congruence.
× rewrite -(of_to_val e2' v2) in Hs2; last done.
edestruct H32 as (?&e3'&?&?&Hs3&[(E&?&Hstuck&?)|(Hsteps3&v3&?&?)]); eauto.
** do 4 eexists; split; eauto.
** do 4 eexists; split; eauto.
right. split; auto. eexists; split; eauto.
- intros. edestruct H23; eauto.
Qed.
From iris.prelude Require Import irelations.
Structure language := Language {
expr : Type;
val : Type;
state : Type;
of_val : val → expr;
to_val : expr → option val;
prim_step : expr → state → expr → state → option expr → Prop;
to_of_val v : to_val (of_val v) = Some v;
of_to_val e v : to_val e = Some v → of_val v = e;
val_stuck e σ e' σ' ef : prim_step e σ e' σ' ef → to_val e = None
}.
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _.
Arguments to_of_val {_} _.
Arguments of_to_val {_} _ _ _.
Arguments val_stuck {_} _ _ _ _ _ _.
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
Canonical Structure exprC Λ := leibnizC (expr Λ).
Global Instance stateC_step Σ: StepN (state Σ) := trivial_stepN.
Global Instance stateC_ustep Σ: uStep (stateC Σ) := trivial_stepN_ustep.
Definition cfg (Λ : language) := (list (expr Λ) × state Λ)%type.
Section language.
Context {Λ : language}.
Implicit Types v : val Λ.
Definition reducible (e : expr Λ) (σ : state Λ) :=
∃ e' σ' ef, prim_step e σ e' σ' ef.
Definition atomic (e : expr Λ) : Prop :=
∀ σ e' σ' ef, prim_step e σ e' σ' ef → is_Some (to_val e').
Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
| step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1) →
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
prim_step e1 σ1 e2 σ2 ef →
step ρ1 ρ2.
Inductive idx_step (i: nat) (ρ1 ρ2 : cfg Λ) : Prop :=
| idx_step_atomic e1 σ1 e2 σ2 ef t1 t2 :
ρ1 = (t1 ++ e1 :: t2, σ1) →
ρ2 = (t1 ++ e2 :: t2 ++ option_list ef, σ2) →
prim_step e1 σ1 e2 σ2 ef →
length t1 = i →
idx_step i ρ1 ρ2.
Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
Proof. intros <-. by rewrite to_of_val. Qed.
Lemma reducible_not_val e σ : reducible e σ → to_val e = None.
Proof. intros (?&?&?&?); eauto using val_stuck. Qed.
Global Instance: Inj (=) (=) (@of_val Λ).
Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Inductive idx_step': nat → cfg Λ → cfg Λ → Prop :=
| idx_step_alt_hd_atomic e1 σ1 e2 σ2 ef t2 :
prim_step e1 σ1 e2 σ2 ef →
idx_step' 0 (e1 :: t2, σ1) (e2 :: t2 ++ option_list ef, σ2)
| idx_step_alt_cons k e0 es1 σ1 es2 σ2:
idx_step' k (es1, σ1) (es2, σ2) →
idx_step' (S k) (e0 :: es1, σ1) (e0 :: es2, σ2).
Lemma idx_step_equiv k es1 es2:
idx_step k es1 es2 ↔ idx_step' k es1 es2.
Proof.
split; intro Hs.
- inversion Hs.
× revert k es1 es2 e1 σ1 e2 σ2 ef t2 H H0 H1 H2 Hs.
induction t1; intros. simpl in ×. subst. econstructor; eauto.
destruct k; simpl in *; try omega.
subst. econstructor.
eapply IHt1; eauto.
econstructor; eauto.
- induction Hs.
× eapply (idx_step_atomic _ _ _ _ _ _ _ _ nil); eauto.
× inversion IHHs.
inversion H. inversion H0. subst.
eapply (idx_step_atomic _ _ _ _ _ _ _ _ (e0 :: t1));
rewrite ?app_comm_cons; simpl; auto.
Qed.
Lemma idx_step_app:
∀ l (σ σ': state Λ) ts ts' i,
idx_step i (ts, σ) (ts', σ') ↔
idx_step (length l + i) (l ++ ts, σ) (l ++ ts', σ').
Proof.
intros. rewrite ?idx_step_equiv.
split.
- intros. induction l; simpl; auto; econstructor; auto.
- induction l; intros; simpl in *; auto.
inversion H. subst. eauto.
Qed.
Lemma idx_step_cons:
∀ i (σ σ': state Λ) ts ts' x,
idx_step i (ts, σ) (ts', σ') ↔
idx_step (S i) (x :: ts, σ) (x :: ts', σ').
Proof.
intros.
replace (x :: ts) with ([x] ++ ts); auto.
replace (x :: ts') with ([x] ++ ts'); auto.
replace (S i) with (length [x] + i); auto.
eapply idx_step_app.
Qed.
Lemma enabled_idx_step_cons:
∀ x l (σ: state Λ) i,
enabled idx_step (x :: l, σ) (S i)
↔ enabled idx_step (l, σ) i.
Proof.
rewrite /enabled. intros; split.
- intros (?&His).
rewrite idx_step_equiv in His ×.
intros His. inversion His. subst.
eexists; rewrite idx_step_equiv; eauto.
- intros (?&His).
rewrite idx_step_equiv in His ×.
intros His.
destruct x0 as (l', σ').
∃ (x :: l', σ'); rewrite idx_step_equiv; econstructor; eauto.
Qed.
Lemma step_idx_step ρ1 ρ2:
step ρ1 ρ2 → ∃ i, idx_step i ρ1 ρ2.
Proof.
inversion 1. ∃ (length t1).
econstructor; eauto.
Qed.
Lemma forall_not_enabled_forall_not_reducible tp σ:
(∀ i, ¬ (enabled idx_step (tp, σ) i)) →
Forall (λ e, ¬ reducible e σ) tp.
Proof.
induction tp; first econstructor.
intros Hne. econstructor.
- intros (?&?&?&?).
eapply (Hne 0). econstructor. rewrite idx_step_equiv.
econstructor; eauto.
- eapply IHtp.
intros i Hne'.
eapply (Hne (S i)).
destruct (Hne') as ((tp'&σ')&Hstep).
∃ (a :: tp', σ'). rewrite ?idx_step_equiv in Hstep *=>Hstep.
econstructor; eauto.
Qed.
Lemma Forall_values_or_some_non (tp: list (expr Λ)):
Forall (λ e, is_Some (to_val e)) tp ∨
∃ e, e ∈ tp ∧ to_val e = None.
Proof.
induction tp as [| e tp]; first left; auto.
rewrite Forall_cons.
case (decide (is_Some (to_val e))) as [l|n]; intros.
- destruct IHtp as [Hvals|(e'&Hin&?)].
** left. split; eauto.
** right. ∃ e'. split; auto; set_solver.
- right; ∃ e. split; first set_solver.
destruct (to_val e); auto.
exfalso; eapply n; eauto.
Qed.
End language.
Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
fill_not_val e :
to_val e = None → to_val (K e) = None;
fill_step e1 σ1 e2 σ2 ef :
prim_step e1 σ1 e2 σ2 ef →
prim_step (K e1) σ1 (K e2) σ2 ef;
fill_step_inv e1' σ1 e2 σ2 ef :
to_val e1' = None → prim_step (K e1') σ1 e2 σ2 ef →
∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 ef
}.
Lemma length_cfg_idx_step:
∀ {L: language} (c c': cfg L) i, idx_step i c c' → length (fst c) ≤ length (fst c').
Proof.
intros ? ? ? ? Hidx.
inversion Hidx. subst.
repeat (rewrite ?app_length //=).
omega.
Qed.
Lemma length_cfg_idx_step':
∀ {L: language} (c c': cfg L) i, idx_step i c c' → S (length (fst c)) ≥ length (fst c').
Proof.
intros ? ? ? ? Hidx.
inversion Hidx. subst.
repeat (rewrite ?app_length //=).
destruct ef; simpl in *; omega.
Qed.
Lemma length_cfg_idx_step2:
∀ {L: language} (c c': cfg L) i, idx_step i c c' → i < length (fst c).
Proof.
intros ? ? ? ? Hidx.
inversion Hidx. subst.
repeat (rewrite ?app_length //=).
omega.
Qed.
Definition safe_refine {ΛT ΛS: language} (R: val ΛT → val ΛS → Prop)
(e: expr ΛT) (σ: state ΛT) (E: expr ΛS) (Σ: state ΛS) :=
(∀ l tp' σ', isteps idx_step l ([e], σ) (tp', σ')
→ Forall (λ e', is_Some (to_val e') ∨ reducible e' σ') tp') ∧
(∀ l v' tp' σ', isteps idx_step l ([e], σ) (of_val v' :: tp', σ')
→ Forall (λ e', is_Some (to_val e')) tp'
→ ∃ L E' TP' Σ', isteps idx_step L ([E], Σ) (E' :: TP', Σ') ∧
((∃ E'', E'' ∈ (E' :: TP') ∧ ¬ reducible E'' Σ' ∧
to_val E'' = None) ∨
(Forall (λ E'', is_Some (to_val E'')) TP' ∧
∃ V', to_val E' = Some V' ∧ R v' V'))) ∧
(∀ (t: trace idx_step ([e], σ)), weak_fair t
→ ∃ (T: trace idx_step ([E], Σ)), weak_fair T).
Definition safe_refine' {ΛT ΛS: language} (R: val ΛT → val ΛS → Prop)
(e: expr ΛT) (σ: state ΛT) (E: expr ΛS) (Σ: state ΛS) :=
(∀ l tp' σ', isteps idx_step l ([e], σ) (tp', σ')
→ Forall (λ e', is_Some (to_val e') ∨ reducible e' σ') tp') ∧
(∀ l v' tp' σ', isteps idx_step l ([e], σ) (of_val v' :: tp', σ')
→ Forall (λ e', is_Some (to_val e')) tp'
→ ∃ L V' TP' Σ', isteps idx_step L ([E], Σ) (of_val V' :: TP', Σ')
∧ Forall (λ E'', ¬ reducible E'' Σ') TP'
∧ R v' V') ∧
(∀ (t: trace idx_step ([e], σ)), weak_fair t
→ ∃ (T: trace idx_step ([E], Σ)), weak_fair T).
Lemma safe_refine'_to_safe_refine {ΛT ΛS} R (e: expr ΛT) σ (E: expr ΛS) Σ:
safe_refine' R e σ E Σ → safe_refine R e σ E Σ.
Proof.
intros (?&H2&?). split_and!; auto.
intros. edestruct H2 as (L&V'&TP'&Σ'&Histeps&Hnenabled&HR); eauto.
∃ L, (of_val V'), TP', Σ'; split_and!; auto.
edestruct (Forall_values_or_some_non TP') as [Hvalues|(E'&?&?)].
- right. split; auto. eexists; split; eauto using to_of_val.
- left. ∃ E'. split_and!; first set_solver; auto.
eapply Forall_forall in Hnenabled; eauto.
Qed.
Lemma safe_refine_trans {Λ1 Λ2 Λ3}
(R: val Λ1 → val Λ2 → Prop)
(S: val Λ2 → val Λ3 → Prop)
(T: val Λ1 → val Λ3 → Prop)
(e1: expr Λ1) σ1 (e2: expr Λ2) σ2 (e3: expr Λ3) σ3:
(∀ v1 v2 v3, R v1 v2 → S v2 v3 → T v1 v3) →
safe_refine R e1 σ1 e2 σ2 →
safe_refine S e2 σ2 e3 σ3 →
safe_refine T e1 σ1 e3 σ3.
Proof.
intros Htrans (H21&H22&H23) (H31&H32&H33).
split_and!; eauto.
- intros.
edestruct H22 as (?&e2'&?&?&Hs2&[(E&?&Hstuck&?)|(Hsteps2&v2&?&?)]); eauto.
× exfalso. eapply Hstuck.
setoid_rewrite Forall_forall in H31.
edestruct H31 as [(?&?)|?]; eauto; congruence.
× rewrite -(of_to_val e2' v2) in Hs2; last done.
edestruct H32 as (?&e3'&?&?&Hs3&[(E&?&Hstuck&?)|(Hsteps3&v3&?&?)]); eauto.
** do 4 eexists; split; eauto.
** do 4 eexists; split; eauto.
right. split; auto. eexists; split; eauto.
- intros. edestruct H23; eauto.
Qed.