Define weakest preconditions for total program correctness.

_CoqProject

@@ -56,6 +56,7 @@ theories/base_logic/lib/fancy_updates_from_vs.v
 theories/program_logic/adequacy.v
 theories/program_logic/lifting.v
 theories/program_logic/weakestpre.v
+theories/program_logic/total_weakestpre.v
 theories/program_logic/hoare.v
 theories/program_logic/language.v
 theories/program_logic/ectx_language.v

theories/program_logic/total_weakestpre.v

+From iris.program_logic Require Export weakestpre.
+From iris.proofmode Require Import tactics.
+From iris.base_logic Require Import fixpoint big_op.
+Set Default Proof Using "Type".
+Import uPred.
+
+Definition twp_pre `{irisG Λ Σ} (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,
+     state_interp σ1 ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
+     ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
+       state_interp σ2 ∗ wp E e2 Φ ∗
+       [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
+  end%I.
+
+Lemma twp_pre_mono `{irisG Λ Σ} 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 Φ)%I.
+Proof.
+  iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
+  destruct (to_val e1) as [v|]; first done.
+  iIntros (σ1) "Hσ". iMod ("Hwp" with "Hσ") as "($ & Hwp)"; iModIntro.
+  iIntros (e2 σ2 efs) "Hstep".
+  iMod ("Hwp" with "Hstep") as "($ & Hwp & Hfork)"; iModIntro; iSplitL "Hwp".
+  - by iApply "H".
+  - iApply (@big_sepL_impl with "[$Hfork]"); iIntros "!#" (k e _) "Hwp".
+    by iApply "H".
+Qed.
+
+(* Uncurry [twp_pre] and equip its type with an OFE structure *)
+Definition twp_pre' `{irisG Λ Σ} (s : stuckness) :
+  (prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ) →
+  prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ :=
+    curry3 ∘ twp_pre s ∘ uncurry3.
+
+Local Instance twp_pre_mono' `{irisG Λ Σ} 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 /uncurry3 /twp_pre. do 16 (f_equiv || done). by apply Hwp, pair_ne.
+Qed.
+
+Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
+    (e : expr Λ) (Φ : val Λ → iProp Σ) :
+  iProp Σ := uPred_least_fixpoint (twp_pre' s) (E,e,Φ).
+Definition twp_aux : seal (@twp_def). by eexists. Qed.
+Definition twp := unseal twp_aux.
+Definition twp_eq : @twp = @twp_def := seal_eq twp_aux.
+
+Arguments twp {_ _ _} _ _ _%E _.
+Instance: Params (@twp) 6.
+
+(* Note that using '[[' instead of '[{' results in conflicts with the list
+notations. *)
+Notation "'WP' e @ s ; E [{ Φ } ]" := (twp s E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  s ;  E  [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E [{ Φ } ]" := (twp NotStuck E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  E  [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E ? [{ Φ } ]" := (twp MaybeStuck E e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e [{ Φ } ]" := (twp NotStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' [{  Φ  } ] ']'") : uPred_scope.
+Notation "'WP' e ? [{ Φ } ]" := (twp MaybeStuck ⊤ e%E Φ)
+  (at level 20, e, Φ at level 200,
+   format "'[' 'WP'  e  '/' ? [{  Φ  } ] ']'") : uPred_scope.
+
+Notation "'WP' e @ s ; E [{ v , Q } ]" := (twp s E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  s ;  E  [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E [{ v , Q } ]" := (twp NotStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  E  [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e @ E ? [{ v , Q } ]" := (twp MaybeStuck E e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' @  E  ? [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e [{ v , Q } ]" := (twp NotStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' [{  v ,  Q  } ] ']'") : uPred_scope.
+Notation "'WP' e ? [{ v , Q } ]" := (twp MaybeStuck ⊤ e%E (λ v, Q))
+  (at level 20, e, Q at level 200,
+   format "'[' 'WP'  e  '/' ? [{  v ,  Q  } ] ']'") : uPred_scope.
+
+(* Texan triples *)
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  [[{  x .. y ,   RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])%I
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  ? [[{  x .. y ,   RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
+  (□ ∀ Φ, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])%I
+    (at level 20,
+     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : uPred_scope.
+
+Notation "'[[{' P } ] ] e @ s ; E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E [{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E [{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?[{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e [{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e ? [[{ x .. y , 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _,
+      P -∗ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?[{ Φ }])
+    (at level 20, x closed binder, y closed binder,
+     format "[[{  P  } ] ]  e  ? [[{  x .. y ,  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ s ; E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ s; E [{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  s ;  E  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E [{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e @ E ? [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e @ E ?[{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  @  E  ? [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e [{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+Notation "'[[{' P } ] ] e ? [[{ 'RET' pat ; Q } ] ]" :=
+  (∀ Φ : _ → uPred _, P -∗ (Q -∗ Φ pat%V) -∗ WP e ?[{ Φ }])
+    (at level 20,
+     format "[[{  P  } ] ]  e  ? [[{  RET  pat ;  Q } ] ]") : stdpp_scope.
+
+Section twp.
+Context `{irisG Λ Σ}.
+Implicit Types P : iProp Σ.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
+
+(* Weakest pre *)
+Lemma twp_unfold s E e Φ : WP e @ s; E [{ Φ }] ⊣⊢ twp_pre s (twp s) E e Φ.
+Proof. by rewrite twp_eq /twp_def least_fixpoint_unfold. Qed.
+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 Φ)%I.
+Proof.
+  iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
+  set (Ψ' := curry3 Ψ :
+    prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ).
+  assert (NonExpansive Ψ').
+  { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
+      [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
+  iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
+  iIntros "!#" ([[??] ?]) "H". by iApply "IH".
+Qed.
+
+Global Instance twp_ne s E e n :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@twp Λ Σ _ s E e).
+Proof.
+  intros Φ1 Φ2 HΦ. rewrite !twp_eq. by apply (least_fixpoint_ne _), pair_ne, HΦ.
+Qed.
+Global Instance twp_proper s E e :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@twp Λ Σ _ s E e).
+Proof.
+  by intros Φ Φ' ?; apply equiv_dist=>n; apply twp_ne=>v; apply equiv_dist.
+Qed.
+
+Lemma twp_value' s E Φ v : Φ v -∗ WP of_val v @ s; E [{ Φ }].
+Proof. iIntros "HΦ". rewrite twp_unfold /twp_pre to_of_val. auto. Qed.
+Lemma twp_value_inv s E Φ v : WP of_val v @ s; E [{ Φ }] ={E}=∗ Φ v.
+Proof. by rewrite twp_unfold /twp_pre to_of_val. Qed.
+
+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) "Hσ". iMod (fupd_intro_mask' E2 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 "($ & IH & IHefs)"; auto.
+  iMod "Hclose" as "_"; iModIntro. iSplitR "IHefs".
+  - iDestruct "IH" as "[IH _]". iApply ("IH" with "[//] HΦ").
+  - iApply (big_sepL_impl with "[$IHefs]"); iIntros "!#" (k ef _) "[IH _]".
+    by iApply "IH".
+Qed.
+
+Lemma fupd_wp 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) "Hσ1". iMod "H". by iApply "H".
+Qed.
+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.
+
+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) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
+  iModIntro. iIntros (e2 σ2 efs Hstep).
+  iMod ("H" with "[//]") as "(Hphy & H & $)". 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].
+    iMod (twp_value_inv with "H") as ">H". iFrame "Hphy". by iApply twp_value'.
+Qed.
+
+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_wp. by iApply "HΦ". }
+  rewrite twp_unfold /twp_pre fill_not_val //.
+  iIntros (σ1) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  { iPureIntro. unfold reducible 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 "($ & IH & IHfork)".
+  iModIntro; iSplitR "IHfork".
+  - iDestruct "IH" as "[IH _]". by iApply "IH".
+  - by setoid_rewrite and_elim_r.
+Qed.
+
+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) "Hσ". iMod ("IH" with "[$]") as "[% IH]". iModIntro; iSplit.
+  { destruct s; eauto using reducible_fill. }
+  iIntros (e2 σ2 efs Hstep).
+  iMod ("IH" $! (K e2) σ2 efs with "[]") as "($ & IH & IHfork)"; eauto using fill_step.
+  iModIntro; iSplitR "IHfork".
+  - iDestruct "IH" as "[IH _]". by iApply "IH".
+  - by setoid_rewrite and_elim_r.
+Qed.
+
+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) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iModIntro; iNext.
+  iIntros (e2 σ2 efs) "Hstep".
+  iMod ("H" with "Hstep") as "($ & H & Hfork)"; iModIntro.
+  iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
+  iIntros "!#" (k e' _) "H". by iApply "IH".
+Qed.
+
+(** * 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.
+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.
+Lemma twp_stuck_weaken s E e Φ :
+  WP e @ s; E [{ Φ }] ⊢ WP e @ E ?[{ Φ }].
+Proof. apply twp_stuck_mono. by destruct s. Qed.
+Lemma twp_mask_mono s E1 E2 e Φ :
+  E1 ⊆ E2 → WP e @ s; E1 [{ Φ }] -∗ WP e @ s; E2 [{ Φ }].
+Proof. iIntros (?) "H"; iApply (twp_strong_mono with "H"); auto. Qed.
+Global Instance twp_mono' s E e :
+  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@twp Λ Σ _ s E e).
+Proof. by intros Φ Φ' ?; apply twp_mono. Qed.
+
+Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }].
+Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value'. Qed.
+Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }].
+Proof. intros. by rewrite -twp_fupd -twp_value'. Qed.
+Lemma twp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }].
+Proof. intros. rewrite -twp_fupd -twp_value //. Qed.
+
+Lemma twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, R ∗ Φ v }].
+Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
+Lemma twp_frame_r s E e Φ R : WP e @ s; E [{ Φ }] ∗ R -∗ WP e @ s; E [{ v, Φ v ∗ R }].
+Proof. iIntros "[H ?]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed.
+
+Lemma twp_wand s E e Φ Ψ :
+  WP e @ s; E [{ Φ }] -∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
+Proof.
+  iIntros "H HΦ". iApply (twp_strong_mono with "H"); auto.
+  iIntros (?) "?". by iApply "HΦ".
+Qed.
+Lemma twp_wand_l s E e Φ Ψ :
+  (∀ v, Φ v -∗ Ψ v) ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ Ψ }].
+Proof. iIntros "[H Hwp]". iApply (twp_wand with "Hwp H"). Qed.
+Lemma twp_wand_r s E e Φ Ψ :
+  WP e @ s; E [{ Φ }] ∗ (∀ v, Φ v -∗ Ψ v) -∗ WP e @ s; E [{ Ψ }].
+Proof. iIntros "[Hwp H]". iApply (twp_wand with "Hwp H"). Qed.
+End twp.
+
+(** Proofmode class instances *)
+Section proofmode_classes.
+  Context `{irisG Λ Σ}.
+  Implicit Types P Q : iProp Σ.
+  Implicit Types Φ : val Λ → iProp Σ.
+
+  Global Instance frame_twp p s E e R Φ Ψ :
+    (∀ v, Frame p R (Φ v) (Ψ v)) → Frame p R (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Ψ }]).
+  Proof. rewrite /Frame=> HR. rewrite twp_frame_l. apply twp_mono, HR. Qed.
+
+  Global Instance is_except_0_wp s E e Φ : IsExcept0 (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
+
+  Global Instance elim_modal_bupd_twp s E e P Φ :
+    ElimModal (|==> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
+
+  Global Instance elim_modal_fupd_twp s E e P Φ :
+    ElimModal (|={E}=> P) P (WP e @ s; E [{ Φ }]) (WP e @ s; E [{ Φ }]).
+  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
+
+  (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
+  Global Instance elim_modal_fupd_twp_atomic s E1 E2 e P Φ :
+    Atomic (stuckness_to_atomicity s) e →
+    ElimModal (|={E1,E2}=> P) P
+            (WP e @ s; E1 [{ Φ }]) (WP e @ s; E2 [{ v, |={E2,E1}=> Φ v }])%I | 100.
+  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r twp_atomic. Qed.
+End proofmode_classes.