phanerozoic/Coq-Iris huggingface dataset:
(* iris/program_logic/language.v *)
Lemma step_insert i t2 σ2 e κ e' σ3 efs :
    t2 !! i = Some e →
    prim_step e σ2 κ e' σ3 efs →
    step (t2, σ2) κ (<[i:=e']>t2 ++ efs, σ3).
Proof.
    intros.
    edestruct (list_elem_of_split_length t2) as (t21&t22&?&?);
      first (by eauto using list_elem_of_lookup_2); simplify_eq.
    econstructor; eauto.
    by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
  Qed.
(* iris/program_logic/language.v *)
Lemma erased_step_Permutation (t1 t1' t2 : list (expr Λ)) σ1 σ2 :
    t1 ≡ₚ t1' → erased_step (t1,σ1) (t2,σ2) → ∃ t2', t2 ≡ₚ t2' ∧ erased_step (t1',σ1) (t2',σ2).
Proof.
    intros Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
     (* FIXME: [naive_solver] should be able to handle this *)
  Qed.
(* iris/program_logic/language.v *)
Record pure_step (e1 e2 : expr Λ)
:= {
    pure_step_safe σ1 : reducible_no_obs e1 σ1;
    pure_step_det σ1 κ e2' σ2 efs :
      prim_step e1 σ1 κ e2' σ2 efs → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs = []
  }.
(* iris/program_logic/language.v *)
Notation pure_steps_tp
:= (Forall2 (rtc pure_step)).
(* iris/program_logic/language.v *)
(* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
  succeeding when it did not actually do anything. *)
Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ)
:=
    pure_exec : φ → relations.nsteps pure_step n e1 e2.
(* iris/program_logic/language.v *)
Lemma pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
    pure_step e1 e2 →
    pure_step (K e1) (K e2).
Proof.
    intros [Hred Hstep]. split.
    - unfold reducible_no_obs in *. naive_solver eauto using fill_step.
    - intros σ1 κ e2' σ2 efs Hpstep.
      destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
      + edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
  Qed.
(* iris/program_logic/language.v *)
Lemma pure_step_nsteps_ctx K `{!@LanguageCtx Λ K} n e1 e2 :
    relations.nsteps pure_step n e1 e2 →
    relations.nsteps pure_step n (K e1) (K e2).
Proof. eauto using nsteps_congruence, pure_step_ctx. Qed.
(* iris/program_logic/language.v *)
Lemma rtc_pure_step_ctx K `{!@LanguageCtx Λ K} e1 e2 :
    rtc pure_step e1 e2 → rtc pure_step (K e1) (K e2).
Proof. eauto using rtc_congruence, pure_step_ctx. Qed.
(* iris/program_logic/language.v *)
(* We do not make this an instance because it is awfully general. *)
Lemma pure_exec_ctx K `{!@LanguageCtx Λ K} φ n e1 e2 :
    PureExec φ n e1 e2 →
    PureExec φ n (K e1) (K e2).
Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
(* iris/program_logic/language.v *)
(* This is a family of frequent assumptions for PureExec *)
Class IntoVal (e : expr Λ) (v : val Λ)
:=
    into_val : of_val v = e.
(* iris/program_logic/language.v *)
Class AsVal (e : expr Λ)
:= as_val : ∃ v, of_val v = e.
(* iris/program_logic/language.v *)
(* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
  efficiently since no witness has to be computed. *)
Instance as_vals_of_val vs : TCForall AsVal (of_val <$> vs).
Proof.
    apply TCForall_Forall, Forall_fmap, Forall_true=> v.
    rewrite /AsVal /=; eauto.
  Qed.
(* iris/program_logic/language.v *)
Lemma as_val_is_Some e :
    (∃ v, of_val v = e) → is_Some (to_val e).
Proof. intros [v <-]. rewrite to_of_val. eauto. Qed.
(* iris/program_logic/language.v *)
Lemma prim_step_not_stuck e σ κ e' σ' efs :
    prim_step e σ κ e' σ' efs → not_stuck e σ.
Proof. rewrite /not_stuck /reducible. eauto 10. Qed.
(* iris/program_logic/language.v *)
Lemma rtc_pure_step_val `{!Inhabited (state Λ)} v e :
    rtc pure_step (of_val v) e → to_val e = Some v.
Proof.
    intros ?; rewrite <- to_of_val.
    f_equal; symmetry; eapply rtc_nf; first done.
    intros [e' [Hstep _]].
    destruct (Hstep inhabitant) as (?&?&?&Hval%val_stuck).
    by rewrite to_of_val in Hval.
  Qed.
(* iris/program_logic/language.v *)
(* Let thread pools [t1] and [t3] be such that each thread in [t1] makes
   (zero or more) pure steps to the corresponding thread in [t3]. Furthermore,
   let [t2] be a thread pool such that [t1] under state [σ1] makes a (single)
   step to thread pool [t2] and state [σ2]. In this situation, either the step
   from [t1] to [t2] corresponds to one of the pure steps between [t1] and [t3],
   or, there is an [i] such that [i]th thread does not participate in the
   pure steps between [t1] and [t3] and [t2] corresponds to taking a step in
   the [i]th thread starting from [t1]. *)
Lemma erased_step_pure_step_tp t1 σ1 t2 σ2 t3 :
    erased_step (t1, σ1) (t2, σ2) →
    pure_steps_tp t1 t3 →
    (σ1 = σ2 ∧ pure_steps_tp t2 t3) ∨
    (∃ i e efs e' κ,
      t1 !! i = Some e ∧ t3 !! i = Some e ∧
      t2 = <[i:=e']>t1 ++ efs ∧
      prim_step e σ1 κ e' σ2 efs).
Proof.
    intros [κ [e σ e' σ' efs t11 t12 ?? Hstep]] Hps; simplify_eq/=.
    apply Forall2_app_inv_l in Hps
      as (t31&?&Hpsteps&(e''&t32&Hps&?&->)%Forall2_cons_inv_l&->).
    destruct Hps as [e|e1 e2 e3 [_ Hprs]].
    - right.
      exists (length t11), e, efs, e', κ; split_and!; last done.
      + by rewrite lookup_app_r // Nat.sub_diag.
      + apply Forall2_length in Hpsteps.
        by rewrite lookup_app_r Hpsteps // Nat.sub_diag.
      + by rewrite insert_app_r_alt // Nat.sub_diag /= -assoc_L.
    - edestruct Hprs as (?&?&?&?); first done; simplify_eq.
      left; split; first done.
      rewrite right_id_L.
      eauto using Forall2_app.
  Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_lift_step_fupdN s E Φ e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗
      £ (S $ num_laters_per_step ns)
      ={∅}▷=∗^(S $ num_laters_per_step ns) |={∅,E}=>
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E {{ Φ }} ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof. by rewrite wp_unfold /wp_pre=>->. Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_lift_step_fupd s E Φ e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={∅}=∗ ▷ |={∅,E}=>
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E {{ Φ }} ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (?) "Hwp". rewrite -wp_lift_step_fupdN; [|done].
  iIntros (?????) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)".
  iIntros "!>" (??? ?) "Hcred".
  iPoseProof (lc_weaken 1 with "Hcred") as "Hcred"; first lia.
  simpl. rewrite -step_fupdN_intro; [|done]. rewrite -bi.laterN_intro.
  iMod ("Hwp" with "[//] Hcred") as "Hwp".
  iApply step_fupd_intro; done.
Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_lift_stuck E Φ e :
  to_val e = None →
  (∀ σ ns κs nt, state_interp σ ns κs nt ={E,∅}=∗ ⌜stuck e σ⌝)
  ⊢ WP e @ E ?{{ Φ }}.
Proof.
  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 ns κ κs nt) "Hσ".
  iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
  iIntros (e2 σ2 efs ?). by case: (Hirr κ e2 σ2 efs).
Qed.
(* iris/program_logic/lifting.v *)
(* Derived lifting lemmas. *)
Lemma wp_lift_step s E Φ e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E,∅}=∗
    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={∅,E}=∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E {{ Φ }} ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?????) "Hσ".
  iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % Hcred !> !>". by iApply "H".
Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E E' Φ e1 :
  (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
  (∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
  (|={E}[E']▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ -∗ £ 1 -∗ WP e2 @ s; E {{ Φ }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
  { specialize (Hsafe inhabitant). destruct s; eauto using reducible_not_val. }
  iIntros (σ1 ns κ κs nt) "Hσ". iMod "H".
  iApply fupd_mask_intro; first set_solver. iIntros "Hclose". iSplit.
  { iPureIntro. destruct s; done. }
  iNext. iIntros (e2 σ2 efs ?) "Hcred".
  destruct (Hstep κ σ1 e2 σ2 efs) as (-> & <- & ->); auto.
  iMod (state_interp_mono with "Hσ") as "$".
  iMod "Hclose" as "_". iMod "H". iModIntro.
  by iDestruct ("H" with "[//] Hcred") as "$".
Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_lift_pure_stuck `{!Inhabited (state Λ)} E Φ e :
  (∀ σ, stuck e σ) →
  True ⊢ WP e @ E ?{{ Φ }}.
Proof.
  iIntros (Hstuck) "_". iApply wp_lift_stuck.
  - destruct(to_val e) as [v|] eqn:He; last done.
    rewrite -He. by case: (Hstuck inhabitant).
  - iIntros (σ ns κs nt) "_". iApply fupd_mask_intro; auto with set_solver.
Qed.
(* iris/program_logic/lifting.v *)
(* Atomic steps don't need any mask-changing business here, one can
   use the generic lemmas here. *)
Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E1}=∗
    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
    ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={E1}[E2]▷=∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      from_option Φ False (to_val e2) ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E1 {{ Φ }}.
Proof.
  iIntros (?) "H".
  iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 ns κ κs nt) "Hσ1".
  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
  iApply fupd_mask_intro; first set_solver.
  iIntros "Hclose" (e2 σ2 efs ?) "Hcred". iMod "Hclose" as "_".
  iMod ("H" $! e2 σ2 efs with "[#] Hcred") as "H"; [done|].
  iApply fupd_mask_intro; first set_solver. iIntros "Hclose !>".
  iMod "Hclose" as "_". iMod "H" as "($ & HQ & $)".
  destruct (to_val e2) eqn:?; last by iExFalso.
  iApply wp_value; last done. by apply of_to_val.
Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_lift_atomic_step {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κ κs nt, state_interp σ1 ns (κ ++ κs) nt ={E}=∗
    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
    ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗ £ 1 ={E}=∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      from_option Φ False (to_val e2) ∗
      [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ fork_post }})
  ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
  iIntros (?????) "?". iMod ("H" with "[$]") as "[$ H]".
  iIntros "!> *". iIntros (Hstep) "Hcred !> !>".
  by iApply "H".
Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E E' Φ} e1 e2 :
  (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
    κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
  (|={E}[E']▷=> £ 1 -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step_no_fork s E E'); try done.
  { naive_solver. }
  iApply (step_fupd_wand with "H"); iIntros "H".
  iIntros (κ e' efs' σ (_&?&->&?)%Hpuredet); auto.
Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
  PureExec φ n e1 e2 →
  φ →
  (|={E}[E']▷=>^n £ n -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?] ? IH]; simpl.
  { iMod lc_zero as "Hz". by iApply "Hwp". }
  iApply wp_lift_pure_det_step_no_fork.
  - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
  - done.
  - iApply (step_fupd_wand with "Hwp").
    iIntros "Hwp Hone". iApply "IH".
    iApply (step_fupdN_wand with "Hwp").
    iIntros "Hwp Hc". iApply ("Hwp" with "[Hone Hc]").
    rewrite (lc_succ n). iFrame.
Qed.
(* iris/program_logic/lifting.v *)
Lemma wp_pure_step_later `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
  PureExec φ n e1 e2 →
  φ →
  ▷^n (£ n -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
  intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
  enough (∀ P, ▷^n P ⊢ |={E}▷=>^n P) as Hwp by apply Hwp. intros ?.
  induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
Qed.
(* iris/program_logic/ownp.v *)
(* This module provides an interface to handling ownership of the global state that
works more like Iris 2.0 did.  The state interpretation (in WP) is fixed to be
authoritative ownership of the entire state (using the [excl] RA).  Users can
then put the corresponding fragment into an invariant on their own to establish
a more interesting notion of ownership, such as the standard heap with disjoint
union. *)
Class ownPGS (Λ : language) (Σ : gFunctors)
:= OwnPGS {
  ownP_invG : invGS Σ;
  #[local] ownP_inG :: inG Σ (excl_authR (stateO Λ));
  ownP_name : gname;
}.
(* iris/program_logic/ownp.v *)
Instance ownPG_irisGS `{!ownPGS Λ Σ} : irisGS Λ Σ
:= {
  iris_invGS := ownP_invG;
  state_interp σ _ κs _ := own ownP_name (●E σ)%I;
  fork_post _ := True%I;
  num_laters_per_step _ := 0;
  state_interp_mono _ _ _ _ := fupd_intro _ _
}.
(* iris/program_logic/ownp.v *)
Definition ownPΣ (Λ : language) : gFunctors
:=
  #[invΣ;
    GFunctor (excl_authR (stateO Λ))].
(* iris/program_logic/ownp.v *)
Class ownPGpreS (Λ : language) (Σ : gFunctors) : Set
:= {
  #[global] ownPPre_invG :: invGpreS Σ;
  #[local] ownPPre_state_inG :: inG Σ (excl_authR (stateO Λ))
}.
(* iris/program_logic/ownp.v *)
Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPGpreS Λ Σ.
Proof. solve_inG. Qed.
(* iris/program_logic/ownp.v *)
(* Ownership *)
Definition ownP `{!ownPGS Λ Σ} (σ : state Λ) : iProp Σ
:=
  own ownP_name (◯E σ).
(* iris/program_logic/ownp.v *)
Instance : Params (@ownP) 3
:= {}.
(* iris/program_logic/ownp.v *)
(* Adequacy *)
Theorem ownP_adequacy Σ `{!ownPGpreS Λ Σ} s e σ φ :
  (∀ `{!ownPGS Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
  adequate s e σ (λ v _, φ v).
Proof.
  intros Hwp. apply (wp_adequacy Σ _).
  iIntros (? κs).
  iMod (own_alloc (●E σ ⋅ ◯E σ)) as (γσ) "[Hσ Hσf]";
    first by apply excl_auth_valid.
  iModIntro. iExists (λ σ κs, own γσ (●E σ))%I, (λ _, True%I).
  iFrame "Hσ".
  iApply (Hwp (OwnPGS _ _ _ _ γσ)). rewrite /ownP. iFrame.
Qed.
(* iris/program_logic/ownp.v *)
Theorem ownP_invariance Σ `{!ownPGpreS Λ Σ} s e σ1 t2 σ2 φ :
  (∀ `{!ownPGS Λ Σ},
      ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗
      |={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'⌝) →
  rtc erased_step ([e], σ1) (t2, σ2) →
  φ σ2.
Proof.
  intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
  iIntros (? κs).
  iMod (own_alloc (●E σ1 ⋅ ◯E σ1)) as (γσ) "[Hσ Hσf]";
    first by apply auth_both_valid_discrete.
  iExists (λ σ κs' _, own γσ (●E σ))%I, (λ _, True%I).
  iFrame "Hσ".
  iMod (Hwp (OwnPGS _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
    first by rewrite /ownP; iFrame.
  iIntros "!> Hσ". iExists ∅. iMod "H" as (σ2') "[Hσf %]". rewrite /ownP.
  iCombine "Hσ Hσf"
    gives %[Hp%Excl_included _]%auth_both_valid_discrete; simplify_eq; auto.
Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_eq σ1 ns σ2 κs nt :
    state_interp σ1 ns κs nt -∗ ownP σ2 -∗ ⌜σ1 = σ2⌝.
Proof.
    iIntros "Hσ● Hσ◯". rewrite /ownP.
    by iCombine "Hσ● Hσ◯"
      gives %[->%Excl_included _]%auth_both_valid_discrete.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_state_twice σ1 σ2 : ownP σ1 ∗ ownP σ2 ⊢ False.
Proof.
    rewrite /ownP -own_op own_valid. by iIntros (?%excl_auth_frag_op_valid).
  Qed.
(* iris/program_logic/ownp.v *)
Instance ownP_timeless σ : Timeless (@ownP Λ Σ _ σ).
Proof. rewrite /ownP; apply _. Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_step s E Φ e1 :
    (|={E,∅}=> ∃ σ1, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗
      ▷ ownP σ1 ∗
      ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗
      ownP σ2
            ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    iIntros "H". destruct (to_val e1) as [v|] eqn:EQe1.
    - apply of_to_val in EQe1 as <-. iApply fupd_wp.
      iMod "H" as (σ1) "[Hred _]"; iDestruct "Hred" as %Hred.
      destruct s; last done. apply reducible_not_val in Hred.
      move: Hred; by rewrite to_of_val.
    - iApply wp_lift_step; [done|]; iIntros (σ1 ns κ κs nt) "Hσκs".
      iMod "H" as (σ1' ?) "[>Hσf H]".
      iDestruct (ownP_eq with "Hσκs Hσf") as %<-.
      iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep) "Hcred".
      iDestruct "Hσκs" as "Hσ". rewrite /ownP.
      iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
      { apply excl_auth_update. }
      iFrame "Hσ". iApply ("H" with "[]"); eauto with iFrame.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_stuck E Φ e :
    (|={E,∅}=> ∃ σ, ⌜stuck e σ⌝ ∗ ▷ (ownP σ))
    ⊢ WP e @ E ?{{ Φ }}.
Proof.
    iIntros "H". destruct (to_val e) as [v|] eqn:EQe.
    - apply of_to_val in EQe as <-. iApply fupd_wp.
      iMod "H" as (σ1) "[H _]". iDestruct "H" as %[Hnv _]. exfalso.
      by rewrite to_of_val in Hnv.
    - iApply wp_lift_stuck; [done|]. iIntros (σ1 ns κs nt) "Hσ".
      iMod "H" as (σ1') "(% & >Hσf)".
      by iDestruct (ownP_eq with "Hσ Hσf") as %->.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_pure_step `{!Inhabited (state Λ)} s E Φ e1 :
    (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
    (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1) →
    (▷ ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ →
      WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    iIntros (Hsafe Hstep) "H"; iApply wp_lift_step.
    { specialize (Hsafe inhabitant). destruct s; last done.
      by eapply reducible_not_val. }
    iIntros (σ1 ns κ κs nt) "Hσ". iApply fupd_mask_intro; first set_solver.
    iIntros "Hclose". iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs ?) "Hcred".
    destruct (Hstep σ1 κ e2 σ2 efs); auto; subst.
    by iMod "Hclose"; iModIntro; iFrame; iApply "H".
  Qed.
(* iris/program_logic/ownp.v *)
(* Derived lifting lemmas. *)
Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
    (▷ (ownP σ1) ∗
       ▷ ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ -∗
         ownP σ2 -∗
      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    iIntros (?) "[Hσ H]"; iApply ownP_lift_step.
    iApply fupd_mask_intro; first set_solver.
    iIntros "Hclose". iExists σ1; iFrame; iSplit; first by destruct s.
    iNext; iIntros (κ e2 σ2 efs ?) "Hσ".
    iDestruct ("H" $! κ e2 σ2 efs with "[] [Hσ]") as "[HΦ $]"; [by eauto..|].
    destruct (to_val e2) eqn:?; last by iExFalso.
    iMod "Hclose"; iApply wp_value; last done. by apply of_to_val.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
    (∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
                     σ2' = σ2 ∧ to_val e2' = Some v2 ∧ efs' = efs) →
    ▷ (ownP σ1) ∗ ▷ (ownP σ2 -∗
      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    iIntros (? Hdet) "[Hσ1 Hσ2]"; iApply ownP_lift_atomic_step; try done.
    iFrame; iNext; iIntros (κ' e2' σ2' efs' ?) "Hσ2'".
    edestruct (Hdet κ') as (<-&Hval&<-); first done. rewrite Hval.
    iApply ("Hσ2" with "Hσ2'").
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
    (∀ κ' e2' σ2' efs', prim_step e1 σ1 κ' e2' σ2' efs' →
      σ2' = σ2 ∧ to_val e2' = Some v2 ∧ efs' = []) →
    {{{ ▷ (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
Proof.
    intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
    rewrite big_sepL_nil right_id. iIntros "Hs Hs'".
    iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E Φ} e1 e2 :
    (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
    (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
    ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2) //.
    iIntros "Hwp". iApply step_fupd_intro; first done. iNext. by iIntros "_".
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_base_step s E Φ e1 :
    (|={E,∅}=> ∃ σ1, ⌜base_reducible e1 σ1⌝ ∗ ▷ (ownP σ1) ∗
            ▷ ∀ κ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗
            ownP σ2
            ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    iIntros "H". iApply ownP_lift_step.
    iMod "H" as (σ1 ?) "[>Hσ1 Hwp]". iModIntro. iExists σ1. iSplit.
    { destruct s; try by eauto using reducible_not_val. }
    iFrame. iNext. iIntros (κ e2 σ2 efs ?) "Hσ2".
    iApply ("Hwp" with "[] Hσ2"); eauto.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_base_stuck E Φ e :
    sub_redexes_are_values e →
    (|={E,∅}=> ∃ σ, ⌜base_stuck e σ⌝ ∗ ▷ (ownP σ))
    ⊢ WP e @ E ?{{ Φ }}.
Proof.
    iIntros (?) "H". iApply ownP_lift_stuck. iMod "H" as (σ) "[% >Hσ]".
    iExists σ. iModIntro. by auto with iFrame.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_pure_base_step s E Φ e1 :
    (∀ σ1, base_reducible e1 σ1) →
    (∀ σ1 κ e2 σ2 efs, base_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1) →
    (▷ ∀ κ e2 efs σ, ⌜base_step e1 σ κ e2 σ efs⌝ →
      WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
    iIntros (??) "H".  iApply ownP_lift_pure_step; eauto.
    { by destruct s; auto. }
    iNext. iIntros (?????). iApply "H"; eauto.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_atomic_base_step {s E Φ} e1 σ1 :
    base_reducible e1 σ1 →
    ▷ (ownP σ1) ∗ ▷ (∀ κ e2 σ2 efs,
    ⌜base_step e1 σ1 κ e2 σ2 efs⌝ -∗ ownP σ2 -∗
      from_option Φ False (to_val e2) ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    iIntros (?) "[Hst H]". iApply ownP_lift_atomic_step; eauto.
    { by destruct s; eauto using reducible_not_val. }
    iSplitL "Hst"; first done.
    iNext. iIntros (???? ?) "Hσ". iApply ("H" with "[] Hσ"); eauto.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_atomic_det_base_step {s E Φ e1} σ1 v2 σ2 efs :
    base_reducible e1 σ1 →
    (∀ κ' e2' σ2' efs', base_step e1 σ1 κ' e2' σ2' efs' →
      σ2' = σ2 ∧ to_val e2' = Some v2 ∧ efs' = efs) →
    ▷ (ownP σ1) ∗ ▷ (ownP σ2 -∗
                      Φ v2 ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
    ⊢ WP e1 @ s; E {{ Φ }}.
Proof.
    intros Hr Hs.
    destruct s; apply ownP_lift_atomic_det_step; eauto using reducible_not_val;
    intros; eapply Hs; eauto 10.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_atomic_det_base_step_no_fork {s E e1} σ1 κ v2 σ2 :
    base_reducible e1 σ1 →
    (∀ κ' e2' σ2' efs', base_step e1 σ1 κ' e2' σ2' efs' →
      κ' = κ ∧ σ2' = σ2 ∧ to_val e2' = Some v2 ∧ efs' = []) →
    {{{ ▷ (ownP σ1) }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
Proof.
    intros ???; apply ownP_lift_atomic_det_step_no_fork; last naive_solver.
    by destruct s; eauto using reducible_not_val.
  Qed.
(* iris/program_logic/ownp.v *)
Lemma ownP_lift_pure_det_base_step_no_fork {s E Φ} e1 e2 :
    (∀ σ1, base_reducible e1 σ1) →
    (∀ σ1 κ e2' σ2 efs', base_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
    ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
    iIntros (??) "H"; iApply wp_lift_pure_det_step_no_fork; try by eauto.
    by destruct s; eauto using reducible_not_val.
  Qed.
(* iris/program_logic/total_adequacy.v *)
Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
    (t1 : list (expr Λ)) : iProp Σ
:=
  ∀ t2 σ1 ns κ κs σ2 nt, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
    state_interp σ1 ns κs nt ={⊤}=∗
              ∃ nt', ⌜κ = []⌝ ∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2.