(* iris_heap_lang/proph_erasure.v *)
From iris.program_logic Require Export adequacy
From iris.heap_lang Require Export lang notation tactics
From iris.prelude Require Import options

Definition erase_base_lit(l : base_lit) : base_lit :=
  match l with
  | LitProphecy p => LitPoison
  | _ => l
  end.

Definition erase_resolve(e0 e1 e2 : expr) : expr := Fst (Fst (e0, e1, e2)).

Definition erased_new_proph: expr := (λ: <>, #LitPoison)%V #().

Fixpoint erase_expr(e : expr) : expr :=
  match e with
  | Val v => Val (erase_val v)
  | Var x => Var x
  | Rec f x e => Rec f x (erase_expr e)
  | App e1 e2 => App (erase_expr e1) (erase_expr e2)
  | UnOp op e => UnOp op (erase_expr e)
  | BinOp op e1 e2 => BinOp op (erase_expr e1) (erase_expr e2)
  | If e0 e1 e2 => If (erase_expr e0) (erase_expr e1) (erase_expr e2)
  | Pair e1 e2 => Pair (erase_expr e1) (erase_expr e2)
  | Fst e => Fst (erase_expr e)
  | Snd e => Snd (erase_expr e)
  | InjL e => InjL (erase_expr e)
  | InjR e => InjR (erase_expr e)
  | Case e0 e1 e2 => Case (erase_expr e0) (erase_expr e1) (erase_expr e2)
  | Fork e => Fork (erase_expr e)
  | AllocN e1 e2 => AllocN (erase_expr e1) (erase_expr e2)
  | Free e => Free (erase_expr e)
  | Load e => Load (erase_expr e)
  | Xchg e1 e2 => Xchg (erase_expr e1) (erase_expr e2)
  | Store e1 e2 => Store (erase_expr e1) (erase_expr e2)
  | CmpXchg e0 e1 e2 => CmpXchg (erase_expr e0) (erase_expr e1) (erase_expr e2)
  | FAA e1 e2 => FAA (erase_expr e1) (erase_expr e2)
  | NewProph => erased_new_proph
  | Resolve e0 e1 e2 =>
    erase_resolve (erase_expr e0) (erase_expr e1) (erase_expr e2)
  end
with
erase_val (v : val) : val :=
  match v with
  | LitV l => LitV (erase_base_lit l)
  | RecV f x e => RecV f x (erase_expr e)
  | PairV v1 v2 => PairV (erase_val v1) (erase_val v2)
  | InjLV v => InjLV (erase_val v)
  | InjRV v => InjRV (erase_val v)
  end.

Lemma erase_expr_substx v e :
  erase_expr (subst x v e) = subst x (erase_val v) (erase_expr e)
with
erase_val_subst x v (w : val) :
  erase_expr (subst x v w) = subst x (erase_val v) (erase_val w).
Proof.
  - destruct e; simpl; try case_decide;
      rewrite ?erase_expr_subst ?erase_val_subst; auto.
  - by destruct v.
Qed.

Lemma erase_expr_subst'x v e :
  erase_expr (subst' x v e) = subst' x (erase_val v) (erase_expr e).
Proof. destruct x; eauto using erase_expr_subst. Qed.

Lemma erase_val_subst'x v (w : val) :
  erase_expr (subst x v w) = subst x (erase_val v) (erase_val w).
Proof. destruct x; eauto using erase_val_subst. Qed.

Fixpoint erase_ectx_item(Ki : ectx_item) : list ectx_item :=
  match Ki with
  | AppLCtx v2 => [AppLCtx (erase_val v2)]
  | AppRCtx e1 => [AppRCtx (erase_expr e1)]
  | UnOpCtx op => [UnOpCtx op]
  | BinOpLCtx op v2 => [BinOpLCtx op (erase_val v2)]
  | BinOpRCtx op e1 => [BinOpRCtx op (erase_expr e1)]
  | IfCtx e1 e2 => [IfCtx (erase_expr e1) (erase_expr e2)]
  | PairLCtx v2 => [PairLCtx (erase_val v2)]
  | PairRCtx e1 => [PairRCtx (erase_expr e1)]
  | FstCtx => [FstCtx]
  | SndCtx => [SndCtx]
  | InjLCtx => [InjLCtx]
  | InjRCtx => [InjRCtx]
  | CaseCtx e1 e2 => [CaseCtx (erase_expr e1) (erase_expr e2)]
  | AllocNLCtx v2 => [AllocNLCtx (erase_val v2)]
  | AllocNRCtx e1 => [AllocNRCtx (erase_expr e1)]
  | FreeCtx => [FreeCtx]
  | LoadCtx => [LoadCtx]
  | XchgLCtx v2 => [XchgLCtx (erase_val v2)]
  | XchgRCtx e1 => [XchgRCtx (erase_expr e1)]
  | StoreLCtx v2 => [StoreLCtx (erase_val v2)]
  | StoreRCtx e1 => [StoreRCtx (erase_expr e1)]
  | CmpXchgLCtx v1 v2 => [CmpXchgLCtx (erase_val v1) (erase_val v2)]
  | CmpXchgMCtx e0 v2 => [CmpXchgMCtx (erase_expr e0) (erase_val v2)]
  | CmpXchgRCtx e0 e1 => [CmpXchgRCtx (erase_expr e0) (erase_expr e1)]
  | FaaLCtx v2 => [FaaLCtx (erase_val v2)]
  | FaaRCtx e1 => [FaaRCtx (erase_expr e1)]
  | ResolveLCtx ctx v1 v2 =>
    erase_ectx_item ctx ++
    [PairLCtx (erase_val v1); PairLCtx (erase_val v2); FstCtx; FstCtx]
  | ResolveMCtx e0 v2 =>
    [PairRCtx (erase_expr e0); PairLCtx (erase_val v2); FstCtx; FstCtx]
  | ResolveRCtx e0 e1 =>
    [PairRCtx (erase_expr e0, er
...

Definition erase_ectx(K : ectx heap_ectx_lang) : ectx heap_ectx_lang :=
  mbind erase_ectx_item K.

Definition erase_tp(tp : list expr) : list expr := erase_expr <$> tp.

Definition erase_heap(h : gmap loc (option val)) : gmap loc (option val) :=
  (λ ov : option val, erase_val <$> ov) <$> h.

Definition erase_state(σ : state) : state :=
  {| heap := erase_heap (heap σ); used_proph_id := ∅ |}.

Definition erase_cfg(ρ : cfg heap_lang) : cfg heap_lang :=
  (erase_tp ρ.1, erase_state ρ.2).

Lemma erase_to_vale v :
  to_val (erase_expr e) = Some v → ∃ v', to_val e = Some v' ∧ erase_val v' = v.
Proof. destruct e; naive_solver. Qed.

Lemma erase_not_vale : to_val e = None → to_val (erase_expr e) = None.
Proof. by destruct e. Qed.

Lemma erase_ectx_appK K' : erase_ectx (K ++ K') = erase_ectx K ++ erase_ectx K'.
Proof. by rewrite /erase_ectx bind_app. Qed.

Lemma erase_ectx_exprK e :
  erase_expr (fill K e) = fill (erase_ectx K) (erase_expr e).
Proof.
  revert e.
  induction K as [|Ki K IHK] using rev_ind; simplify_eq/=; first done.
  intros e.
  rewrite !erase_ectx_app !fill_app /= -IHK {IHK}.
  induction Ki; rewrite /= ?fill_app /= /erase_resolve; eauto with f_equal.
Qed.

Lemma val_is_unboxed_erasedv :
  val_is_unboxed (erase_val v) ↔ val_is_unboxed v.
Proof.
  destruct v; rewrite /= /lit_is_unboxed; repeat (done || simpl; case_match).
Qed.

Lemma vals_compare_safe_erasev1 v2 :
  vals_compare_safe (erase_val v1) (erase_val v2) ↔
  vals_compare_safe v1 v2.
Proof. rewrite /vals_compare_safe !val_is_unboxed_erased. done. Qed.

Lemma erase_val_inj_iffv1 v2 :
  vals_compare_safe v1 v2 → erase_val v1 = erase_val v2 ↔ v1 = v2.
Proof.
  destruct v1, v2; rewrite /= /lit_is_unboxed;
    repeat (done || (by intros [[] | []]) || simpl; case_match).
Qed.

Lemma un_op_eval_eraseop v v' :
  un_op_eval op (erase_val v) = Some v' ↔
  ∃ w, un_op_eval op v = Some w ∧ erase_val w = v'.
Proof.
  destruct op; simpl; repeat case_match; naive_solver.
Qed.

Lemma bin_op_eval_eraseop v1 v2 v' :
  bin_op_eval op (erase_val v1) (erase_val v2) = Some v' ↔
  ∃ w, bin_op_eval op v1 v2 = Some w ∧ erase_val w = v'.
Proof.
  rewrite /bin_op_eval /bin_op_eval_int /bin_op_eval_bool /bin_op_eval_loc;
    split; [intros ?|intros (?&?&?)];
      repeat (case_match; simplify_eq/=); eauto.
  - eexists _; split; eauto; simpl.
    erewrite bool_decide_ext; first by eauto.
    rewrite erase_val_inj_iff; done.
  - by assert (vals_compare_safe v1 v2) by by apply vals_compare_safe_erase.
  - by erewrite bool_decide_ext; last apply erase_val_inj_iff.
  - by assert (vals_compare_safe (erase_val v1) (erase_val v2))
      by by apply vals_compare_safe_erase.
Qed.

Lemma lookup_erase_heap_Noneh l : erase_heap h !! l = None ↔ h !! l = None.
Proof. rewrite lookup_fmap; by destruct (h !! l). Qed.

Lemma lookup_erase_heaph l : erase_heap h !! l = (λ ov, erase_val <$> ov) <$> h !! l.
Proof. by rewrite lookup_fmap. Qed.

Lemma erase_heap_insert_Someh l v :
  erase_heap (<[l := Some v]> h) = <[l := Some $ erase_val v]> (erase_heap h).
Proof.
  by rewrite /erase_heap fmap_insert.
Qed.

Lemma erase_heap_insert_Noneh l v :
  erase_heap (<[l := None]> h) = <[l := None]> (erase_heap h).
Proof.
  by rewrite /erase_heap fmap_insert.
Qed.

Lemma fmap_heap_array(f : val → val) l vs :
  (λ ov : option val, f <$> ov) <$> heap_array l vs = heap_array l (f <$> vs).
Proof.
  revert l; induction vs as [|v vs IHvs]; intros l;
    first by rewrite /= fmap_empty.
  by rewrite /= -!insert_union_singleton_l !fmap_insert IHvs.
Qed.

Lemma erase_heap_arrayl i v h :
  erase_heap (heap_array l (replicate i v) ∪ h) =
  heap_array l (replicate i (erase_val v)) ∪ erase_heap h.
Proof.
  apply map_eq => l'.
  rewrite /erase_heap lookup_fmap !lookup_union -fmap_replicate
  - fmap_heap_array !lookup_fmap.
    by destruct (heap_array l (replicate i v) !! l'); destruct (h !! l').
Qed.

Lemma erase_state_initl n v σ:
  erase_state (state_init_heap l n v σ) =
  state_init_heap l n (erase_val v) (erase_state σ).
Proof. by rewrite /erase_state /state_init_heap /= erase_heap_array. Qed.

Definition base_steps_to_erasure_of(e1 : expr) (σ1 : state) (e2 : expr)
           (σ2 : state) (efs : list expr) :=
  ∃ κ' e2' σ2' efs',
    base_step e1 σ1 κ' e2' σ2' efs' ∧
    erase_expr e2' = e2 ∧ erase_state σ2' = σ2 ∧ erase_tp efs' = efs.

Lemma erased_base_step_base_step_recf x e v σ :
  base_steps_to_erasure_of ((rec: f x := e)%V v) σ
    (subst' x (erase_val v)
            (subst' f (rec: f x := erase_expr e) (erase_expr e)))
    (erase_state σ) [].
Proof. by repeat econstructor; rewrite !erase_expr_subst'. Qed.

Lemma erased_base_step_base_step_NewProphσ :
  base_steps_to_erasure_of NewProph σ #LitPoison (erase_state σ) [].
Proof. eexists _, _, _, _; split; first eapply new_proph_id_fresh; done. Qed.

Lemma erased_base_step_base_step_AllocNn v σ l :
  (0 < n)%Z →
  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → erase_heap (heap σ) !! (l +ₗ i) = None) →
  base_steps_to_erasure_of
    (AllocN #n v) σ #l (state_init_heap l n (erase_val v) (erase_state σ)) [].
Proof.
  eexists _, _, _, _; simpl; split;
    first econstructor; try setoid_rewrite <- lookup_erase_heap_None;
      rewrite ?erase_heap_insert /=; eauto using erase_state_init.
Qed.

Lemma erased_base_step_base_step_Freel v σ :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (Free #l) σ #()
   {| heap := <[l:=None]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
  rewrite /state_upd_heap /erase_state /= erase_heap_insert_None //.
Qed.

Lemma erased_base_step_base_step_Loadl σ v :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (! #l) σ v (erase_state σ) [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; eauto.
Qed.

Lemma erased_base_step_base_step_Xchgl v w σ :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (Xchg #l w) σ v
   {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
  rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
Qed.

Lemma erased_base_step_base_step_Storel v w σ :
  erase_heap (heap σ) !! l = Some (Some v) →
  base_steps_to_erasure_of (#l <- w) σ #()
   {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ)); used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[|]|] eqn:?; simplify_eq/=.
  eexists _, _, _, _; simpl; split; first econstructor; repeat split; eauto.
  rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some //.
Qed.

Lemma erased_base_step_base_step_CmpXchgl v w σ vl :
  erase_heap (heap σ) !! l = Some (Some vl) →
  vals_compare_safe vl (erase_val v) →
  base_steps_to_erasure_of
    (CmpXchg #l v w) σ
    (vl, #(bool_decide (vl = erase_val v)))%V
    (if bool_decide (vl = erase_val v)
     then {| heap := <[l:=Some $ erase_val w]> (erase_heap (heap σ));
             used_proph_id := ∅ |}
     else erase_state σ) [].
Proof.
  intros Hl Hvl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[u|]|] eqn:?; simplify_eq/=.
  rewrite -> vals_compare_safe_erase in Hvl.
  destruct (decide (u = v)) as [->|Hneq].
  - eexists _, _, _, _; simpl; split.
    { econstructor; eauto. }
    rewrite !bool_decide_eq_true_2; eauto using erase_val_inj_iff; [].
    rewrite -?erase_heap_insert_Some.
    split_and!; auto.
  - eexists _, _, _, _; simpl; split.
    { econstructor; eauto. }
    rewrite !bool_decide_eq_false_2; eauto; [].
    by rewrite erase_val_inj_iff.
Qed.

Lemma erased_base_step_base_step_FAAl n m σ :
  erase_heap (heap σ) !! l = Some (Some #n) →
  base_steps_to_erasure_of
    (FAA #l #m) σ #n
    {| heap := <[l:= Some #(n + m)]> (erase_heap (heap σ));
       used_proph_id := ∅ |} [].
Proof.
  intros Hl.
  rewrite lookup_erase_heap in Hl.
  destruct (heap σ !! l) as [[[[]| | | |]|]|] eqn:?; simplify_eq/=.
  repeat econstructor; first by eauto.
  by rewrite /state_upd_heap /erase_state /= erase_heap_insert_Some.
Qed.

Lemma erased_base_step_base_stepe1 σ1 κ e2 σ2 efs:
  base_step (erase_expr e1) (erase_state σ1) κ e2 σ2 efs →
  base_steps_to_erasure_of e1 σ1 e2 σ2 efs.
Proof.
  intros Hhstep.
  inversion Hhstep; simplify_eq/=;
    repeat match goal with
           | H : _ = erase_expr ?e |- _ => destruct e; simplify_eq/=
           | H : _ = erase_val ?v |- _ => destruct v; simplify_eq/=
           | H : _ = erase_base_lit ?l |- _ => destruct l; simplify_eq/=
           | H : context [erased_new_proph] |- _ => unfold erased_new_proph in H
           | H : un_op_eval _ (erase_val _) = Some _ |- _ =>
             apply un_op_eval_erase in H as [? [? ?]]
           | H : bin_op_eval _ (erase_val _) (erase_val _) = Some _ |- _ =>
             apply bin_op_eval_erase in H as [? [? ?]]
           | H : val_is_unboxed (erase_val _) |- _ =>
             apply -> val_is_unboxed_erased in H
           end; simplify_eq/=;
    try (by repeat econstructor);
  eauto using erased_base_step_base_step_rec,
    erased_base_step_base_step_NewProph,
    erased_base_step_base_step_AllocN,
    erased_base_step_base_step_Free,
    erased_base_step_base_step_Load,
    erased_base_step_base_step_Xchg,
    erased_base_step_base_step_Store,
    erased_base_step_base_step_CmpXchg,
    erased_base_step_base_step_FAA.
Qed.

Lemma fill_to_resolvee v1 v2 K e' :
  to_val e' = None →
  Resolve e v1 v2 = fill K e' →
  K = [] ∨ ∃ K' Ki, K = K' ++ [ResolveLCtx Ki v1 v2].
Proof.
  intros Hnv Hrs; simpl in *.
  assert (∀ v K, fill K e' ≠ v) as Hcontr.
  { intros w K' Hw.
    assert (to_val (of_val w) = to_val (fill K' e')) as He'
        by (by rewrite Hw).
    rewrite fill_not_val in He'; by eauto. }
  destruct K as [|Ki K _] using rev_ind; first by left.
  rewrite fill_app in Hrs.
  destruct Ki; simplify_eq/=; eauto;
    try exfalso; eapply Hcontr; eauto.
Qed.

Lemma projs_pure_steps(v0 v1 v2 : val) :
  rtc pure_step (Fst (Fst (v0, v1, v2))) v0.
Proof.
  etrans; first apply (rtc_pure_step_ctx (fill [PairLCtx _; FstCtx; FstCtx])).
  { apply rtc_once.
    apply pure_base_step_pure_step.
    split; first repeat econstructor.
    intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto. }
  simpl.
  etrans; first apply (rtc_pure_step_ctx (fill [FstCtx; FstCtx])).
  { apply rtc_once.
    apply pure_base_step_pure_step.
    split; first repeat econstructor.
    intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto. }
  simpl.
  etrans; first apply (rtc_pure_step_ctx (fill [FstCtx])).
  { apply rtc_once.
    apply pure_base_step_pure_step.
    split; first repeat econstructor.
    intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto. }
  simpl.
  apply rtc_once.
  apply pure_base_step_pure_step.
  split; first repeat econstructor.
  intros ????? Hhstep; inversion Hhstep; simplify_eq/=; eauto.
Qed.

Lemma Resolve_3_vals_base_stuckv0 v1 v2 σ κ e σ' efs :
  ¬ base_step (Resolve v0 v1 v2) σ κ e σ' efs.
Proof.
  intros Hhstep.
  inversion Hhstep; simplify_eq/=.
  apply (eq_None_not_Some (to_val (Val v0))); last eauto.
  by eapply val_base_stuck.
Qed.

Lemma Resolve_3_vals_unsafe(v0 v1 v2 : val) σ :
  ¬ not_stuck (Resolve v0 v1 v2) σ.
Proof.
  assert(∀ w K e, Val w = fill K e → is_Some (to_val e)) as Hvfill.
  { intros ? K ? Heq; eapply (fill_val K); rewrite /= -Heq; eauto. }
  apply not_not_stuck.
  split; first done.
  intros ???? [K e1' e2' Hrs Hhstep]; simplify_eq/=.
  destruct K as [|Ki K _] using rev_ind.
  { simplify_eq/=.
    eapply Resolve_3_vals_base_stuck; eauto. }
  rewrite fill_app in Hrs.
  destruct Ki; simplify_eq/=.
  - rename select ectx_item into Ki.
    pose proof (fill_item_val Ki (fill K e1')) as Hnv.
    apply fill_val in Hnv as [? Hnv]; last by rewrite -Hrs; eauto.
    by erewrite val_base_stuck in Hnv.
  - edestruct Hvfill as [? Heq]; eauto.
    by erewrite val_base_stuck in Heq.
  - edestruct Hvfill as [? Heq]; eauto.
    by erewrite val_base_stuck in Heq.
Qed.

Definition prim_step_matched_by_erased_stepse1 σ1 e2 σ2 efs :=
  ∃ e2' σ2' κ' efs' e2'',
    prim_step e1 σ1 κ' e2' σ2' efs' ∧ rtc pure_step e2 e2'' ∧
    erase_expr e2' = e2'' ∧ erase_state σ2' = σ2 ∧ erase_tp efs' = efs.

Lemma prim_step_matched_by_erased_steps_ectxK e1 σ1 e2 σ2 efs :
  prim_step_matched_by_erased_steps e1 σ1 e2 σ2 efs →
  prim_step_matched_by_erased_steps (fill K e1) σ1 (fill (erase_ectx K) e2) σ2 efs.
Proof.
  intros (?&?&?&?&?&?&?&?&?&?); simplify_eq/=.
  eexists _, _, _, _, _; repeat split.
  - by apply fill_prim_step.
  - rewrite erase_ectx_expr.
    by eapply (rtc_pure_step_ctx (fill (erase_ectx K))).
Qed.

Definition is_Resolve(e : expr) :=
  match e with Resolve _ _ _ => True | _ => False end.

Global Instanceis_Resolve_dec e : Decision (is_Resolve e).
Proof. destruct e; solve_decision. Qed.

Lemma non_resolve_prim_step_matched_by_erased_steps_ectx_itemKi e1 e1' σ1 e2 σ2 efs :
  to_val e1' = None →
  ¬ is_Resolve e1 →
  not_stuck e1 σ1 →
  erase_expr e1 = fill_item Ki e1' →
  (∀ e1, erase_expr e1 = e1' → not_stuck e1 σ1 →
         prim_step_matched_by_erased_steps e1 σ1 e2 σ2 efs) →
  prim_step_matched_by_erased_steps e1 σ1 (fill_item Ki e2) σ2 efs.
Proof.
  intros Hnv Hnr Hsf He1 IH.
  destruct Ki; simplify_eq/=;
    repeat
      match goal with
      | H : erase_expr ?e = _ |- _ => destruct e; simplify_eq/=; try done
      | H : context [erased_new_proph] |- _ =>
        rewrite /erased_new_proph in H; simplify_eq/=
      | |- prim_step_matched_by_erased_steps ?e _ _ _ _ =>
        let tac K e :=
            lazymatch K with
            | [] => fail
            | _ => apply (prim_step_matched_by_erased_steps_ectx K);
                    apply IH; [done| by eapply (not_stuck_fill_inv (fill K))]
            end
        in
        reshape_expr e tac
      end.
Qed.

Lemma prim_step_matched_by_erased_steps_ectx_itemKi K e1 e1' σ1 e2 σ2 efs κ :
  base_step e1' (erase_state σ1) κ e2 σ2 efs →
  not_stuck e1 σ1 →
  erase_expr e1 = fill_item Ki (fill K e1') →
  (∀ K' e1, length K' ≤ length K →
     erase_expr e1 = (fill K' e1') → not_stuck e1 σ1 →
     prim_step_matched_by_erased_steps e1 σ1 (fill K' e2) σ2 efs) →
  prim_step_matched_by_erased_steps e1 σ1 (fill_item Ki (fill K e2)) σ2 efs.
Proof.
  intros Hhstp Hsf He1 IH; simpl in *.

Lemma erased_prim_step_prim_stepe1 σ1 κ e2 σ2 efs:
  prim_step (erase_expr e1) (erase_state σ1) κ e2 σ2 efs → not_stuck e1 σ1 →
  prim_step_matched_by_erased_steps e1 σ1 e2 σ2 efs.
Proof.
  intros Hstp He1sf.
  inversion Hstp as [K e1' e2' He1 ? Hhstp]; clear Hstp; simplify_eq/=.
  set (len := length K); assert (length K = len) as Hlen by done; clearbody len.
  revert K Hlen e1 He1 He1sf.
  induction len as [m IHm]using lt_wf_ind; intros K Hlen e1 He1 He1sf;
    simplify_eq.
  destruct K as [|Ki K _] using rev_ind; simplify_eq/=.
  { apply erased_base_step_base_step in Hhstp as (?&?&?&?&?&<-&?&<-).
    eexists _, _, _, _, _; repeat split;
      first (by apply base_prim_step); auto using rtc_refl. }
  rewrite length_app in IHm; simpl in *.
  rewrite fill_app /=; rewrite fill_app /= in He1.
  eapply prim_step_matched_by_erased_steps_ectx_item; eauto; [].
  { intros K' **; simpl in *. apply (IHm (length K')); auto with lia. }
Qed.

Lemma base_step_erased_prim_step_CmpXchgv1 v2 σ l vl:
  heap σ !! l = Some (Some vl) →
  vals_compare_safe vl v1 →
  ∃ e2' σ2' ef', prim_step (CmpXchg #l (erase_val v1)
                             (erase_val v2)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hl Hv.
  destruct (bool_decide (vl = v1)) eqn:Heqvls.
  - do 3 eexists; apply base_prim_step;
      econstructor; [|by apply vals_compare_safe_erase|by eauto].
      by rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl.
  - do 3 eexists; apply base_prim_step;
        econstructor; [|by apply vals_compare_safe_erase|by eauto].
      by rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl.
Qed.

Lemma base_step_erased_prim_step_resolvee w σ :
  (∃ e2' σ2' ef', prim_step (erase_expr e) (erase_state σ) [] e2' σ2' ef') →
  ∃ e2' σ2' ef',
    prim_step (erase_resolve (erase_expr e) #LitPoison (erase_val w))
              (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros (?&?&?&?).
  by eexists _, _, _;
    apply (fill_prim_step [PairLCtx _; PairLCtx _;FstCtx; FstCtx]).
Qed.

Lemma base_step_erased_prim_step_un_opσ op v v':
  un_op_eval op v = Some v' →
  ∃ e2' σ2' ef', prim_step (UnOp op (erase_val v)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor.
  apply un_op_eval_erase; eauto.
Qed.

Lemma base_step_erased_prim_step_bin_opσ op v1 v2 v':
  bin_op_eval op v1 v2 = Some v' →
  ∃ e2' σ2' ef', prim_step (BinOp op (erase_val v1) (erase_val v2))
                           (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor.
  apply bin_op_eval_erase; eauto.
Qed.

Lemma base_step_erased_prim_step_allocNσ l n v:
  (0 < n)%Z →
  (∀ i : Z, (0 ≤ i)%Z → (i < n)%Z → heap σ !! (l +ₗ i) = None) →
  ∃ e2' σ2' ef',
    prim_step (AllocN #n (erase_val v)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor; eauto.
  intros; rewrite lookup_erase_heap_None; eauto.
Qed.

Lemma base_step_erased_prim_step_freeσ l v :
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (Free #l) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hw. do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
Qed.

Lemma base_step_erased_prim_step_loadσ l v:
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (! #l) (erase_state σ) [] e2' σ2' ef'.
Proof.
  do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap.
  by destruct lookup; simplify_eq.
Qed.

Lemma base_step_erased_prim_step_xchgσ l v w :
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (Xchg #l (erase_val w)) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hl. do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl; eauto.
Qed.

Lemma base_step_erased_prim_step_storeσ l v w :
  heap σ !! l = Some (Some v) →
  ∃ e2' σ2' ef', prim_step (#l <- erase_val w) (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hw. do 3 eexists; apply base_prim_step; econstructor.
  rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hw; eauto.
Qed.

Lemma base_step_erased_prim_step_FAAσ l n n':
  heap σ !! l = Some (Some #n) →
  ∃ e2' σ2' ef', prim_step (FAA #l #n') (erase_state σ) [] e2' σ2' ef'.
Proof.
  intros Hl.
  do 3 eexists; apply base_prim_step. econstructor.
  by rewrite /erase_state /state_upd_heap /= lookup_erase_heap Hl.
Qed.

Lemma base_step_erased_prim_stepe1 σ1 κ e2 σ2 ef:
  base_step e1 σ1 κ e2 σ2 ef →
  ∃ e2' σ2' ef', prim_step (erase_expr e1) (erase_state σ1) [] e2' σ2' ef'.
Proof.
  induction 1; simplify_eq/=;
    eauto using base_step_erased_prim_step_CmpXchg,
                base_step_erased_prim_step_resolve,
                base_step_erased_prim_step_un_op,
                base_step_erased_prim_step_bin_op,
                base_step_erased_prim_step_allocN,
                base_step_erased_prim_step_free,
                base_step_erased_prim_step_load,
                base_step_erased_prim_step_store,
                base_step_erased_prim_step_xchg,
                base_step_erased_prim_step_FAA;
    by do 3 eexists; apply base_prim_step; econstructor.
Qed.

Lemma reducible_erased_reduciblee σ :
  reducible e σ → reducible (erase_expr e) (erase_state σ).
Proof.
  intros (?&?&?&?&Hpstp); simpl in *.
  inversion Hpstp; simplify_eq/=.
  rewrite erase_ectx_expr.
  edestruct base_step_erased_prim_step as (?&?&?&?); first done; simpl in *.
  eexists _, _, _, _; eapply fill_prim_step; eauto.
Qed.

Lemma pure_step_tp_safet1 t2 e1 σ :
  (∀ e2, e2 ∈ t2 → not_stuck e2 σ) → pure_steps_tp t1 (erase_tp t2) →
  e1 ∈ t1 → not_stuck e1 (erase_state σ).
Proof.
  intros Ht2 Hpr [i He1]%list_elem_of_lookup_1.
  eapply Forall2_lookup_l in Hpr as [e2' [He2' Hpr]]; simpl in *; eauto.
  rewrite /erase_tp list_lookup_fmap in He2'.
  destruct (t2 !! i) eqn:He2; simplify_eq/=.
  apply list_elem_of_lookup_2, Ht2 in He2.
  clear -Hpr He2.
  inversion Hpr as [|??? [? _]]; simplify_eq.
  - destruct He2 as [[? ?%of_to_val]|]; simplify_eq/=; first by left; eauto.
    by right; apply reducible_erased_reducible.
  - right; eauto using reducible_no_obs_reducible.
Qed.

Theorem erasuree σ φ :
  adequate NotStuck e σ φ →
  adequate NotStuck (erase_expr e) (erase_state σ)
           (λ v σ, ∃ v' σ', erase_val v' = v ∧ erase_state σ' = σ ∧ φ v' σ').
Proof.
  simpl; intros Hade; simpl in *.
  cut (∀ t2 σ2,
          rtc erased_step ([erase_expr e], erase_state σ) (t2, σ2) →
          (∃ t2' t2'' σ2',
              rtc erased_step ([e], σ) (t2'', σ2') ∧
              t2' = erase_tp t2'' ∧ σ2 = erase_state σ2' ∧
              pure_steps_tp t2 t2')).
  { intros Hreach; split; simpl in *.
    - intros ? ? ? Hrtc; edestruct (Hreach _ _ Hrtc) as
          (t2'&t2''&σ2'&Hos&Ht2'&Hσ2&Hptp); simplify_eq/=.
      apply Forall2_cons_inv_l in Hptp as (oe&t3&Hoe%rtc_pure_step_val&_&?);
        destruct t2''; simplify_eq/=.
      apply erase_to_val in Hoe as (?&?%of_to_val&?); simplify_eq.
      pose proof (adequate_result _ _ _ _ Hade _ _ _ Hos); eauto.
    - intros ? ? ? Hs Hrtc He2; edestruct (Hreach _ _ Hrtc) as
          (t2'&t2''&σ2'&Hos&Ht2'&Hσ2&Hptp); simplify_eq/=.
      eapply pure_step_tp_safe; [|done..].
      intros e2' He2'.
      apply (adequate_not_stuck _ _ _ _ Hade _ _ _ eq_refl Hos He2'). }
  intros t2 σ2 [n Hstps]%rtc_nsteps; simpl in *; revert t2 σ2 Hstps.
  induction n as [|n IHn].
  { intros t2 σ2 Hstps; inversion Hstps; simplify_eq /=.
    repeat econstructor. }
  intros t2 σ2 Hstps.
  apply nsteps_inv_r in Hstps as [[t3 σ3] [Hstps Hρ]]; simpl in *.
  destruct (IHn _ _ Hstps) as (t2'&t2''&σ2'&Hostps&?&?&Hprstps); simplify_eq.
  edestruct @erased_step
...