phanerozoic/Coq-Iris huggingface dataset:
(* iris/program_logic/total_adequacy.v *)
Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
  □ (∀ t, twptp1 t -∗ twptp2 t) -∗
  ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t.
Proof.
  iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
  iIntros (t2 σ1 ns κ κs σ2 nt1) "Hstep Hσ".
  iMod ("Hwp" with "[$] [$]") as (n2) "($ & Hσ & ?)".
  iModIntro. iExists n2. iFrame "Hσ". by iApply "H".
Qed.
(* iris/program_logic/total_adequacy.v *)
Instance twptp_pre_mono' : BiMonoPred twptp_pre.
Proof.
  constructor; first (intros ????; apply twptp_pre_mono).
  intros wp Hwp n t1 t2 ?%(discrete_iff _ _ _)%leibniz_equiv; solve_proper.
Qed.
(* iris/program_logic/total_adequacy.v *)
Definition twptp (t : list (expr Λ)) : iProp Σ
:=
  bi_least_fixpoint twptp_pre t.
(* iris/program_logic/total_adequacy.v *)
Lemma twptp_unfold t : twptp t ⊣⊢ twptp_pre twptp t.
Proof. by rewrite /twptp least_fixpoint_unfold. Qed.
(* iris/program_logic/total_adequacy.v *)
Lemma twptp_ind Ψ :
  ⊢ (□ ∀ t, twptp_pre (λ t, Ψ t ∧ twptp t) t -∗ Ψ t) → ∀ t, twptp t -∗ Ψ t.
Proof.
  iIntros "#IH" (t) "H".
  assert (NonExpansive Ψ).
  { by intros n ?? ->%(discrete_iff _ _ _)%leibniz_equiv. }
  iApply (least_fixpoint_ind _ Ψ with "[] H").
  iIntros "!>" (t') "H". by iApply "IH".
Qed.
(* iris/program_logic/total_adequacy.v *)
Instance twptp_Permutation : Proper ((≡ₚ) ==> (⊢)) twptp.
Proof.
  iIntros (t1 t1' Ht) "Ht1". iRevert (t1' Ht); iRevert (t1) "Ht1".
  iApply twptp_ind; iIntros "!>" (t1) "IH"; iIntros (t1' Ht).
  rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 ns κ κs σ2 nt Hstep) "Hσ".
  destruct (step_Permutation t1' t1 t2 κ σ1 σ2) as (t2'&?&?); [done..|].
  iMod ("IH" $! t2' with "[% //] Hσ") as (n2) "($ & Hσ & IH & _)".
  iModIntro. iExists n2. iFrame "Hσ". by iApply "IH".
Qed.
(* iris/program_logic/total_adequacy.v *)
Lemma twptp_app t1 t2 : twptp t1 -∗ twptp t2 -∗ twptp (t1 ++ t2).
Proof.
  iIntros "H1". iRevert (t2). iRevert (t1) "H1".
  iApply twptp_ind; iIntros "!>" (t1) "IH1". iIntros (t2) "H2".
  iRevert (t1) "IH1"; iRevert (t2) "H2".
  iApply twptp_ind; iIntros "!>" (t2) "IH2". iIntros (t1) "IH1".
  rewrite twptp_unfold /twptp_pre. iIntros (t1'' σ1 ns κ κs σ2 nt Hstep) "Hσ1".
  destruct Hstep as [e1 σ1' e2 σ2' efs' t1' t2' [=Ht ?] ? Hstep]; simplify_eq/=.
  apply app_eq_inv in Ht as [(t&?&?)|(t&?&?)]; subst.
  (* Case distinction on whether [e1] is in [t1] or [t2]. *)
  - destruct t as [|e1' ?]; simplify_eq/=.
    + iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)".
      { by eapply (step_atomic _ _ _ _ _ []). }
      iModIntro. iExists n2. iFrame "Hσ".
      rewrite -{2}(left_id_L [] (++) (e2 :: _)). iApply "IH2".
      by setoid_rewrite (right_id_L [] (++)).
    + iMod ("IH1" with "[%] Hσ1") as (n2) "($ & Hσ & IH1 & _)"; first by econstructor.
      iAssert (twptp t2) with "[IH2]" as "Ht2".
      { rewrite twptp_unfold. iApply (twptp_pre_mono with "[] IH2").
        iIntros "!> * [_ ?] //". }
      iModIntro. iExists n2. iFrame "Hσ".
      rewrite -assoc_L (comm _ t2) !cons_middle !assoc_L. by iApply "IH1".
  - iMod ("IH2" with "[%] Hσ1") as (n2) "($ & Hσ & IH2 & _)"; first by econstructor.
    iModIntro. iExists n2. iFrame "Hσ". rewrite -assoc_L. by iApply "IH2".
Qed.
(* iris/program_logic/total_adequacy.v *)
Lemma twp_twptp s Φ e : WP e @ s; ⊤ [{ Φ }] -∗ twptp [e].
Proof.
  iIntros "He". remember (⊤ : coPset) as E eqn:HE.
  iRevert (HE). iRevert (e E Φ) "He". iApply twp_ind.
  iIntros "!>" (e E Φ); iIntros "IH" (->).
  rewrite twptp_unfold /twptp_pre /twp_pre.
  iIntros (t1' σ1' ns κ κs σ2' nt Hstep) "Hσ1".
  destruct Hstep as [e1 σ1 e2 σ2 efs [|? t1] t2 ?? Hstep];
    simplify_eq/=; try discriminate_list.
  destruct (to_val e1) as [v|] eqn:He1.
  { apply val_stuck in Hstep; naive_solver. }
  iMod ("IH" with "Hσ1") as "[_ IH]".
  iMod ("IH" with "[% //]") as "($ & Hσ & [IH _] & IHfork)".
  iModIntro. iExists (length efs + nt). iFrame "Hσ".
  iApply (twptp_app [_] with "(IH [//])").
  clear. iInduction efs as [|e efs IH]; simpl.
  { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 ns κ κs σ2 nt1 Hstep).
    destruct Hstep; simplify_eq/=; discriminate_list. }
  iDestruct "IHfork" as "[[IH' _] IHfork]".
  iApply (twptp_app [_] with "(IH' [//])"). by iApply "IH".
Qed.
(* iris/program_logic/total_adequacy.v *)
Lemma twptp_total σ ns nt t :
  state_interp σ ns [] nt -∗ twptp t ={⊤|}=∗ ⌜sn erased_step (t, σ)⌝.
Proof.
  iIntros "Hσ Ht". iRevert (σ ns nt) "Hσ". iRevert (t) "Ht".
  iApply twptp_ind; iIntros "!>" (t) "IH"; iIntros (σ ns nt) "Hσ".
  rewrite -(pure_mono _ _ (Acc_intro _)). iIntros ([t' σ'] [κ Hstep]).
  rewrite /twptp_pre.
  iMod ("IH" with "[% //] Hσ") as (n' ->) "[Hσ [H _]]".
  by iApply "H".
Qed.
(* iris/program_logic/total_adequacy.v *)
Theorem twp_total hlc Σ Λ `{!invGpreS Σ} s e σ Φ n m :
  (∀ `{Hinv : !invGS_gen hlc Σ},
     ⊢ |={⊤}=> ∃
         (stateI : state Λ → nat → list (observation Λ) → nat → iProp Σ)
         (** We abstract over any instance of [irisG], and thus any value of
             the field [num_laters_per_step]. This is needed because instances
             of [irisG] (e.g., the one of HeapLang) are shared between WP and
             TWP, where TWP simply ignores [num_laters_per_step]. *)
         (num_laters_per_step : nat → nat)
         (fork_post : val Λ → iProp Σ)
         state_interp_mono,
       let _ : irisGS_gen hlc Λ Σ :=
           IrisG Hinv stateI fork_post num_laters_per_step state_interp_mono
       in
       stateI σ n [] 0 ∗ (£ m -∗ WP e @ s; ⊤ [{ Φ }])) →
  sn erased_step ([e], σ).
(* i.e. ([e], σ) is strongly normalizing *)
Proof.
  intros Hwp. eapply (pure_soundness (PROP:=iPropI Σ)).
  apply (fupd_finally_soundness hlc m ⊤); iIntros (?) "H£".
  iMod (Hwp) as (stateI num_laters_per_step fork_post stateI_mono) "[Hσ H]".
  pose (iG := IrisG _ stateI fork_post num_laters_per_step stateI_mono).
  iApply (@twptp_total _ _ _ iG _ n with "Hσ"). iApply twp_twptp. by iApply "H".
Qed.
(* iris/program_logic/total_ectx_lifting.v *)
Lemma twp_lift_base_step {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E,∅}=∗
    ⌜base_reducible_no_obs e1 σ1⌝ ∗
    ∀ κ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
      ⌜κ = []⌝ ∗
      state_interp σ2 (S ns) κs (length efs + nt) ∗
      WP e2 @ s; E [{ Φ }] ∗
      [∗ list] i ↦ ef ∈ efs, WP ef @ s; ⊤ [{ fork_post }])
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H".
  iApply (twp_lift_step _ E)=>//. iIntros (σ1 ns κs nt) "Hσ".
  iMod ("H" $! σ1 with "Hσ") as "[% H]"; iModIntro.
  iSplit; [destruct s; auto|]. iIntros (κ e2 σ2 efs Hstep).
  iApply "H". by eauto.
Qed.
(* iris/program_logic/total_ectx_lifting.v *)
Lemma twp_lift_pure_base_step_no_fork {s E Φ} e1 :
  (∀ σ1, base_reducible_no_obs e1 σ1) →
  (∀ σ1 κ e2 σ2 efs, base_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
  (|={E}=> ∀ κ e2 efs σ, ⌜base_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }] )
  ⊢ WP e1 @ s; E [{ Φ }].
Proof using Hinh.
  iIntros (??) ">H". iApply twp_lift_pure_step_no_fork; eauto.
  iIntros "!>" (?????). iApply "H"; eauto.
Qed.
(* iris/program_logic/total_ectx_lifting.v *)
Lemma twp_lift_atomic_base_step {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
    ⌜base_reducible_no_obs e1 σ1⌝ ∗
    ∀ κ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={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 twp_lift_atomic_step; eauto.
  iIntros (σ1 ns κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[% H]"; iModIntro.
  iSplit; first by destruct s; auto. iIntros (κ e2 σ2 efs Hstep). iApply "H"; eauto.
Qed.
(* iris/program_logic/total_ectx_lifting.v *)
Lemma twp_lift_atomic_base_step_no_fork {s E Φ} e1 :
  to_val e1 = None →
  (∀ σ1 ns κs nt, state_interp σ1 ns κs nt ={E}=∗
    ⌜base_reducible_no_obs e1 σ1⌝ ∗
    ∀ κ e2 σ2 efs, ⌜base_step e1 σ1 κ e2 σ2 efs⌝ ={E}=∗
      ⌜κ = []⌝ ∗ ⌜efs = []⌝ ∗ state_interp σ2 (S ns) κs nt
                            ∗ from_option Φ False (to_val e2))
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (?) "H". iApply twp_lift_atomic_base_step; eauto.
  iIntros (σ1 ns κs nt) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
  iIntros (κ v2 σ2 efs Hstep).
  iMod ("H" with "[# //]") as "(-> & -> & ? & $) /=". by iFrame.
Qed.
(* iris/program_logic/total_ectx_lifting.v *)
Lemma twp_lift_pure_det_base_step_no_fork {s E Φ} e1 e2 :
  to_val e1 = None →
  (∀ σ1, base_reducible_no_obs 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.
  intros. rewrite -(twp_lift_pure_det_step_no_fork e1 e2); eauto.
Qed.
(* iris/program_logic/total_lifting.v *)
Lemma twp_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_no_obs e1 σ1 else True⌝ ∗
    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,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 twp_unfold /twp_pre=> ->. Qed.
(* iris/program_logic/total_lifting.v *)
(* Derived lifting lemmas. *)
Lemma twp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E Φ e1 :
  (∀ σ1, reducible_no_obs e1 σ1) →
  (∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
  (|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌝ → WP e2 @ s; E [{ Φ }])
  ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (Hsafe Hstep) ">H". iApply twp_lift_step.
  { eapply reducible_not_val, reducible_no_obs_reducible, (Hsafe inhabitant). }
  iIntros (σ1 ns κs n) "Hσ".
  iApply fupd_mask_intro; first by set_solver. iIntros "Hclose". iSplit.
  { iPureIntro. destruct s; auto. }
  iIntros (κ e2 σ2 efs ?). destruct (Hstep σ1 κ e2 σ2 efs) as (->&<-&->); auto.
  iMod (state_interp_mono with "Hσ"). iMod "Hclose" as "_".
  iDestruct ("H" with "[//]") as "H". simpl. by iFrame.
Qed.
(* iris/program_logic/total_lifting.v *)
(* Atomic steps don't need any mask-changing business here, one can
   use the generic lemmas here. *)
Lemma twp_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_no_obs e1 σ1 else True⌝ ∗
    ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={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 (twp_lift_step _ E _ 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) "%". iMod "Hclose" as "_".
  iMod ("H" $! κ e2 σ2 efs with "[#]") as "($ & $ & HΦ & $)"; first by eauto.
  destruct (to_val e2) eqn:?; last by iExFalso.
  iApply twp_value; last done. by apply of_to_val.
Qed.
(* iris/program_logic/total_lifting.v *)
Lemma twp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E Φ} e1 e2 :
  (∀ σ1, reducible_no_obs e1 σ1) →
  (∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
    κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
  (|={E}=> WP e2 @ s; E [{ Φ }]) ⊢ WP e1 @ s; E [{ Φ }].
Proof.
  iIntros (? Hpuredet) ">H". iApply (twp_lift_pure_step_no_fork s E); try done.
  { naive_solver. }
  iIntros "!>" (κ' e' efs' σ (_&_&->&->)%Hpuredet); auto.
Qed.
(* iris/program_logic/total_lifting.v *)
Lemma twp_pure_step `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
  PureExec φ n e1 e2 →
  φ →
  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; first done.
  iApply twp_lift_pure_det_step_no_fork; [done|naive_solver|].
  iModIntro. by iApply "IH".
Qed.
(* iris/program_logic/total_weakestpre.v *)
(* The definition of total weakest preconditions is very similar to the
definition of normal (i.e. partial) weakest precondition, with the exception
that there is no later modality. Hence, instead of taking a Banach's fixpoint,
we take a least fixpoint. *)
Definition twp_pre `{!irisGS_gen hlc Λ Σ} (s : stuckness)
      (wp : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
    coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ
:= λ E e1 Φ,
  match to_val e1 with
  | Some v => |={E}=> Φ v
  | None => ∀ σ1 ns κs nt,
     state_interp σ1 ns κs nt ={E,∅}=∗
       ⌜if s is NotStuck then reducible_no_obs e1 σ1 else True⌝ ∗
       ∀ κ e2 σ2 efs, ⌜prim_step e1 σ1 κ e2 σ2 efs⌝ ={∅,E}=∗
         ⌜κ = []⌝ ∗
         state_interp σ2 (S ns) κs (length efs + nt) ∗
         wp E e2 Φ ∗
         [∗ list] ef ∈ efs, wp ⊤ ef fork_post
  end%I.
(* iris/program_logic/total_weakestpre.v *)
(* This is some uninteresting bookkeeping to prove that [twp_pre_mono] is
monotone. The actual least fixpoint [twp_def] can be found below. *)
Lemma twp_pre_mono `{!irisGS_gen hlc Λ Σ} s
    (wp1 wp2 : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
  ⊢ (□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
    ∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ.
Proof.
  iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
  destruct (to_val e1) as [v|]; first done.
  iIntros (σ1 ns κs nt) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
  iIntros (κ e2 σ2 efs) "Hstep".
  iMod ("Hwp" with "Hstep") as (?) "(Hσ & Hwp & Hfork)".
  iModIntro. iFrame "Hσ". iSplit; first done. iSplitL "Hwp".
  - by iApply "H".
  - iApply (@big_sepL_impl with "Hfork"); iIntros "!>" (k e _) "Hwp".
    by iApply "H".
Qed.
(* iris/program_logic/total_weakestpre.v *)
(* Uncurry [twp_pre] and equip its type with an OFE structure *)
Definition twp_pre' `{!irisGS_gen hlc Λ Σ} (s : stuckness) :
  (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ) →
  prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ
:=
    uncurry3 ∘ twp_pre s ∘ curry3.
(* iris/program_logic/total_weakestpre.v *)
Instance twp_pre_mono' `{!irisGS_gen hlc Λ Σ} s : BiMonoPred (twp_pre' s).
Proof.
  constructor.
  - iIntros (wp1 wp2 ??) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
    iApply twp_pre_mono. iIntros "!>" (E e Φ). iApply ("H" $! (E,e,Φ)).
  - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
    rewrite /curry3 /twp_pre. do 26 (f_equiv || done). by apply pair_ne.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Definition twp_def `{!irisGS_gen hlc Λ Σ} : Twp (iProp Σ) (expr Λ) (val Λ) stuckness
:=
  λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
(* iris/program_logic/total_weakestpre.v *)
Definition twp_aux : seal (@twp_def).
Proof. by eexists. Qed.
(* iris/program_logic/total_weakestpre.v *)
Definition twp'
:= twp_aux.(unseal).
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_unseal `{!irisGS_gen hlc Λ Σ} : twp = @twp_def hlc Λ Σ _.
Proof. rewrite -twp_aux.(seal_eq) //. Qed.
(* iris/program_logic/total_weakestpre.v *)
(* Weakest pre *)
Lemma twp_unfold s E e Φ : WP e @ s; E [{ Φ }] ⊣⊢ twp_pre s (twp s) E e Φ.
Proof. by rewrite twp_unseal /twp_def least_fixpoint_unfold. Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_ind s Ψ :
  (∀ n E e, Proper (pointwise_relation _ (dist n) ==> dist n) (Ψ E e)) →
  □ (∀ e E Φ, twp_pre s (λ E e Φ, Ψ E e Φ ∧ WP e @ s; E [{ Φ }]) E e Φ -∗ Ψ E e Φ) -∗
  ∀ e E Φ, WP e @ s; E [{ Φ }] -∗ Ψ E e Φ.
Proof.
  iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_unseal.
  set (Ψ' := uncurry3 Ψ :
    prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) → iPropO Σ).
  assert (NonExpansive Ψ').
  { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
  iApply (least_fixpoint_ind _ Ψ' with "[] H").
  iIntros "!>" ([[??] ?]) "H". by iApply "IH".
Qed.
(* iris/program_logic/total_weakestpre.v *)
Instance twp_ne s E e n :
  Proper (pointwise_relation _ (dist n) ==> dist n) (twp (PROP:=iProp Σ) s E e).
Proof.
  intros Φ1 Φ2 HΦ. rewrite !twp_unseal. by apply (least_fixpoint_ne _), pair_ne, HΦ.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Instance twp_proper s E e :
  Proper (pointwise_relation _ (≡) ==> (≡)) (twp (PROP:=iProp Σ) s E e).
Proof.
  by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_value_fupd' s E Φ v : WP of_val v @ s; E [{ Φ }] ⊣⊢ |={E}=> Φ v.
Proof. rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_strong_mono s1 s2 E1 E2 e Φ Ψ :
  s1 ⊑ s2 → E1 ⊆ E2 →
  WP e @ s1; E1 [{ Φ }] -∗ (∀ v, Φ v ={E2}=∗ Ψ v) -∗ WP e @ s2; E2 [{ Ψ }].
Proof.
  iIntros (? HE) "H HΦ". iRevert (E2 Ψ HE) "HΦ"; iRevert (e E1 Φ) "H".
  iApply twp_ind; first solve_proper.
  iIntros "!>" (e E1 Φ) "IH"; iIntros (E2 Ψ HE) "HΦ".
  rewrite !twp_unfold /twp_pre. destruct (to_val e) as [v|] eqn:?.
  { iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
  iIntros (σ1 ns κs nt) "Hσ".
  iMod (fupd_mask_subseteq E1) as "Hclose"; first done.
  iMod ("IH" with "[$]") as "[% IH]".
  iModIntro; iSplit; [by destruct s1, s2|]. iIntros (κ e2 σ2 efs Hstep).
  iMod ("IH" with "[//]") as (?) "(Hσ & IH & IHefs)"; auto.
  iMod "Hclose" as "_"; iModIntro.
  iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
  - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
  - iApply (big_sepL_impl with "IHefs"); iIntros "!>" (k ef _) "[IH _]".
    iApply "IH"; auto.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma fupd_twp s E e Φ : (|={E}=> WP e @ s; E [{ Φ }]) ⊢ WP e @ s; E [{ Φ }].
Proof.
  rewrite twp_unfold /twp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
  { by iMod "H". }
  iIntros (σ1 ns κs nt) "Hσ1". iMod "H". by iApply "H".
Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_fupd s E e Φ : WP e @ s; E [{ v, |={E}=> Φ v }] ⊢ WP e @ s; E [{ Φ }].
Proof. iIntros "H". iApply (twp_strong_mono with "H"); auto. Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_atomic s E1 E2 e Φ `{!Atomic (stuckness_to_atomicity s) e} :
  (|={E1,E2}=> WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }]) ⊢ WP e @ s; E1 [{ Φ }].
Proof.
  iIntros "H". rewrite !twp_unfold /twp_pre /=.
  destruct (to_val e) as [v|] eqn:He.
  { by iDestruct "H" as ">>> $". }
  iIntros (σ1 ns κs nt) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
  iModIntro. iIntros (κ e2 σ2 efs Hstep).
  iMod ("H" with "[//]") as (?) "(Hσ & H & Hefs)". destruct s.
  - rewrite !twp_unfold /twp_pre. destruct (to_val e2) as [v2|] eqn:He2.
    + iDestruct "H" as ">> $". by iFrame.
    + iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
      by edestruct (atomic _ _ _ _ _ Hstep).
  - destruct (atomic _ _ _ _ _ Hstep) as [v <-%of_to_val].
    rewrite twp_value_fupd'. iMod "H" as ">H".
    iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value_fupd'.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
  WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] ⊢ WP K e @ s; E [{ Φ }].
Proof.
  revert Φ. cut (∀ Φ', WP e @ s; E [{ Φ' }] -∗ ∀ Φ,
    (∀ v, Φ' v -∗ WP K (of_val v) @ s; E [{ Φ }]) -∗ WP K e @ s; E [{ Φ }]).
  { iIntros (help Φ) "H". iApply (help with "H"); auto. }
  iIntros (Φ') "H". iRevert (e E Φ') "H". iApply twp_ind; first solve_proper.
  iIntros "!>" (e E1 Φ') "IH". iIntros (Φ) "HΦ".
  rewrite /twp_pre. destruct (to_val e) as [v|] eqn:He.
  { apply of_to_val in He as <-. iApply fupd_twp. by iApply "HΦ". }
  rewrite twp_unfold /twp_pre fill_not_val //.
  iIntros (σ1 ns κs nt) "Hσ". iMod ("IH" with "[$]") as "[% IH]".
  iModIntro; iSplit.
  { iPureIntro. unfold reducible_no_obs in *.
    destruct s; naive_solver eauto using fill_step. }
  iIntros (κ e2 σ2 efs Hstep).
  destruct (fill_step_inv e σ1 κ e2 σ2 efs) as (e2'&->&?); auto.
  iMod ("IH" $! κ e2' σ2 efs with "[//]") as (?) "(Hσ & IH & IHefs)".
  iModIntro. iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
  - iDestruct "IH" as "[IH _]". by iApply "IH".
  - by setoid_rewrite and_elim_r.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
  WP K e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }].
Proof.
  iIntros "H". remember (K e) as e' eqn:He'.
  iRevert (e He'). iRevert (e' E Φ) "H". iApply twp_ind; first solve_proper.
  iIntros "!>" (e' E1 Φ) "IH". iIntros (e ->).
  rewrite !twp_unfold {2}/twp_pre. destruct (to_val e) as [v|] eqn:He.
  { iModIntro. apply of_to_val in He as <-. rewrite !twp_unfold.
    iApply (twp_pre_mono with "[] IH"). by iIntros "!>" (E e Φ') "[_ ?]". }
  rewrite /twp_pre fill_not_val //.
  iIntros (σ1 ns κs nt) "Hσ". iMod ("IH" with "[$]") as "[% IH]".
  iModIntro; iSplit.
  { destruct s; eauto using reducible_no_obs_fill_inv. }
  iIntros (κ e2 σ2 efs Hstep).
  iMod ("IH" $! κ (K e2) σ2 efs with "[]")
    as (?) "(Hσ & IH & IHefs)"; eauto using fill_step.
  iModIntro. iFrame "Hσ". iSplit; first done. iSplitR "IHefs".
  - iDestruct "IH" as "[IH _]". by iApply "IH".
  - by setoid_rewrite and_elim_r.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
Proof.
  iIntros "H". iLöb as "IH" forall (E e Φ).
  rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//=.
  iIntros (σ1 ns κ κs nt) "Hσ". iMod ("H" with "Hσ") as "[% H]".
  iIntros "!>". iSplitR.
  { destruct s; eauto using reducible_no_obs_reducible. }
  iIntros (e2 σ2 efs) "Hstep _". iMod ("H" with "Hstep") as (->) "(Hσ & H & Hfork)".
  iApply fupd_mask_intro; [set_solver+|]. iIntros "Hclose".
  iIntros "!>!>". iApply step_fupdN_intro=>//. iModIntro. iMod "Hclose" as "_".
  iModIntro. iFrame "Hσ". iSplitL "H".
  { by iApply "IH". }
  iApply (@big_sepL_impl with "Hfork").
  iIntros "!>" (k ef _) "H". by iApply "IH".
Qed.
(* iris/program_logic/total_weakestpre.v *)
(* This lemma is similar to [wp_step_fupdN_strong], the difference is the TWP
(instead of a WP) in the premise. Since TWPs do not use up later credits, we get
[£ n] in the viewshift in the premise. *)
Lemma twp_wp_fupdN_strong n s E1 E2 e P Φ :
  TCEq (to_val e) None → E2 ⊆ E1 →
  (∀ σ ns κs nt, state_interp σ ns κs nt ={E1,∅}=∗
                 ⌜n ≤ S (num_laters_per_step ns)⌝) ∧
  ((|={E1,E2}=> £ n ={∅}▷=∗^n |={E2,E1}=> P) ∗
    WP e @ s; E2 [{ v, P ={E1}=∗ Φ v }]) -∗
  WP e @ s; E1 {{ Φ }}.
Proof.
  destruct n as [|n].
  { iIntros (_ ?) "/= [_ [HP Hwp]]".
    iApply (wp_strong_mono with "[Hwp]"); [done..|by iApply twp_wp|]; simpl.
    iIntros (v) "H". iApply ("H" with "[>HP]"). iMod "HP".
    iMod lc_zero as "Hlc". by iApply "HP". }
  rewrite wp_unfold twp_unfold /wp_pre /twp_pre. iIntros (-> ?) "H".
  iIntros (σ1 ns κ κs nt) "Hσ".
  destruct (decide (n ≤ num_laters_per_step ns)) as [Hn|Hn]; first last.
  { iDestruct "H" as "[Hn _]". iMod ("Hn" with "Hσ") as %?. lia. }
  iDestruct "H" as "[_ [>HP Hwp]]". iMod ("Hwp" with "[$]") as "[% H]".
  iIntros "!>". iSplitR.
  { destruct s; eauto using reducible_no_obs_reducible. }
  iIntros (e2 σ2 efs Hstep) "Hcred /=".
  iDestruct ("H" $! κ e2 σ2 efs with "[% //]") as "H".
  iMod ("HP" with "[Hcred]") as "HP".
  { iApply (lc_weaken with "Hcred"); lia. }
  iIntros "!> !>". iMod "HP". iModIntro.
  iApply step_fupdN_le; [apply Hn|done|..].
  iApply (step_fupdN_wand with "HP"); iIntros "HP".
  iMod "H" as (->) "($ & Hwp & Hfork)". iMod "HP". iModIntro. iSplitR "Hfork".
  - iApply twp_wp. iApply (twp_strong_mono with "Hwp"); [done|set_solver|].
    iIntros (v) "HΦ". iApply ("HΦ" with "HP").
  - iApply (big_sepL_impl with "Hfork").
    iIntros "!>" (k ef _) "H". by iApply twp_wp.
Qed.
(* iris/program_logic/total_weakestpre.v *)
(* * Derived rules *)
Lemma twp_mono s E e Φ Ψ :
  (∀ v, Φ v ⊢ Ψ v) → WP e @ s; E [{ Φ }] ⊢ WP e @ s; E [{ Ψ }].
Proof.
  iIntros (HΦ) "H"; iApply (twp_strong_mono with "H"); auto.
  iIntros (v) "?". by iApply HΦ.
Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_stuck_mono s1 s2 E e Φ :
  s1 ⊑ s2 → WP e @ s1; E [{ Φ }] ⊢ WP e @ s2; E [{ Φ }].
Proof. iIntros (?) "H". iApply (twp_strong_mono with "H"); auto. Qed.
(* iris/program_logic/total_weakestpre.v *)
Lemma twp_stuck_weaken s E e Φ :
  WP e @ s; E [{ Φ }] ⊢ WP e @ E ?[{ Φ }].
Proof. apply twp_stuck_mono. by destruct s. Qed.