Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd...

Modify adequacy proof to not break the 'fancy update' abstraction. Modify fupd plainly interface and add new derived results.

theories/base_logic/lib/fancy_updates.v

 From iris.base_logic.lib Require Export own.
 From stdpp Require Export coPset.
 From iris.base_logic.lib Require Import wsat.
+From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Export invG.
@@ -40,13 +41,50 @@ Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed
 Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
 Proof.
   split.
-  - iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
-    rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
-    iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
-    iAssert (◇ P)%I as "#HP".
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q ?) "HQP HQ [Hw HE]".
+    iAssert (◇ P)%I as "#>$".
     { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
-    iMod "HP". iFrame. auto.
-  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
-    iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
+    by iFrame.
+  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (p E1 E2 P ?) "HP [Hw HE]".
+    iAssert (▷?p ◇ P)%I with "[-]" as "#$"; last by iFrame.
     iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma fupd_plain_soundness `{invPreG Σ} E (P: iPropSI Σ) `{!Plain P}:
+  (∀ `{Hinv: invG Σ}, (|={⊤, E}=> P)%I) → (▷ P)%I.
+Proof.
+  iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
+  iPoseProof (Hfupd Hinv) as "H".
+  rewrite uPred_fupd_eq /uPred_fupd_def.
+  iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
+Qed.
+
+Lemma step_fupdN_soundness `{invPreG Σ} φ n :
+  (∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n |={⊤, ∅}=> ⌜ φ ⌝ : iProp Σ)%I) →
+  φ.
+Proof.
+  iIntros (Hiter).
+  eapply (soundness (M:=iResUR Σ) _  (S (S n))).
+  eapply (fupd_plain_soundness ⊤); first by apply _.
+  intros Hinv. rewrite -/sbi_laterN.
+  iPoseProof (Hiter Hinv) as "H".
+  destruct n.
+  - rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'".
+    do 2 iMod "H'"; iModIntro; auto.
+  - iPoseProof (step_fupdN_mono _ _ _ _ (|={⊤}=> ◇ ⌜φ⌝)%I with "H") as "H'".
+    { iIntros "H". iMod (fupd_plain_strong with "H"); auto. }
+    rewrite -step_fupdN_S_fupd.
+    iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
+    rewrite -later_laterN laterN_later.
+    iNext. by do 2 iMod "Hφ".
+Qed.
+
+Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
+  (∀ `{Hinv: invG Σ}, (|={⊤, ∅}▷=>^n ⌜ φ ⌝ : iProp Σ)%I)  →
+  φ.
+Proof.
+  iIntros (Hiter). eapply (step_fupdN_soundness _ n).
+  iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
+  iApply (step_fupdN_mono with "Hiter").
+  iIntros (?). iMod (fupd_intro_mask' _ ∅) as "_"; auto.
+Qed.

theories/base_logic/lib/wsat.v

@@ -16,6 +16,20 @@ Module invG.
 End invG.
 Import invG.
 
+Definition invΣ : gFunctors :=
+  #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
+    GFunctor coPset_disjUR;
+    GFunctor (gset_disjUR positive)].
+
+Class invPreG (Σ : gFunctors) : Set := WsatPreG {
+  inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+  enabled_inPreG :> inG Σ coPset_disjR;
+  disabled_inPreG :> inG Σ (gset_disjR positive);
+}.
+
+Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
+Proof. solve_inG. Qed.
+
 Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
   to_agree (Next (iProp_unfold P)).
 Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
@@ -175,3 +189,15 @@ Proof.
   iFrame "HI". by iRight.
 Qed.
 End wsat.
+
+(* Allocation of an initial world *)
+Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
+Proof.
+  iIntros.
+  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
+  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
+  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
+  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
+  rewrite /wsat /ownE -lock; iFrame.
+  iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
+Qed.

theories/bi/monpred.v

@@ -957,9 +957,10 @@ Proof. move => [] /(_ i). rewrite /Plain monPred_at_plainly bi.forall_elim //. Q
 Global Instance monPred_bi_fupd_plainly `{BiFUpdPlainly PROP} : BiFUpdPlainly monPredSI.
 Proof.
   split; rewrite monPred_fupd_eq; unseal.
-  - intros E1 E2 E2' P Q ? HE12. split=>/= i. do 3 f_equiv.
-    apply fupd_plain'; [apply _|done].
-  - intros E P ?. split=>/= i. apply later_fupd_plain, _.
+  - intros E P Q ?. split=>/= i. do 3 f_equiv.
+    apply fupd_plain_weak; apply _.
+  - intros p E1 E2 P ?. split=>/= i. specialize (later_fupd_plain p) => HFP.
+    destruct p; simpl; [ unseal | ]; apply HFP, _.
 Qed.
 
 Global Instance plainly_objective `{BiPlainly PROP} P : Objective (■ P).

theories/bi/notation.v

@@ -87,6 +87,8 @@ Reserved Notation "|={ E }▷=> Q"
 Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "'[' P  '/' ={ E }▷=∗  Q ']'").
+Reserved Notation "|={ E1 , E2 }▷=>^ n Q"
+  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200).
 
 (** Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"

theories/bi/updates.v

@@ -28,9 +28,11 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) : stdpp_scope.
 Notation "|={ E1 , E2 , E3 }▷=> Q" := (|={E1,E2}=> (▷ |={E2,E3}=> Q))%I : bi_scope.
 Notation "P ={ E1 , E2 , E3 }▷=∗ Q" := (P -∗ |={ E1,E2,E3 }▷=> Q)%I : bi_scope.
 Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2,E1}▷=> Q)%I : bi_scope.
+Notation "P ={ E1 , E2 }▷=∗ Q" := (P ⊢ |={ E1 , E2, E1 }▷=> Q) (only parsing) : stdpp_scope.
 Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_scope.
 Notation "|={ E }▷=> Q" := (|={E,E}▷=> Q)%I : bi_scope.
 Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
+Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}▷=> P) Q)%I : bi_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
@@ -76,11 +78,10 @@ Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
 Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
 
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
-  fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
-    E1 ⊆ E2 →
-    (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P;
-  later_fupd_plain E (P : PROP) `{!Plain P} :
-    (▷ |={E}=> P) ={E}=∗ ▷ ◇ P;
+  fupd_plain_weak E (P Q : PROP) `{!Plain P} :
+    (Q ={E}=∗ P) -∗ Q ={E}=∗ Q ∗ P;
+  later_fupd_plain p E1 E2 (P : PROP) `{!Plain P} :
+    (▷?p |={E1, E2}=> P) ={E1}=∗ ▷?p ◇ P;
 }.
 Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
@@ -271,6 +272,23 @@ Section fupd_derived.
     intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
   Qed.
 
+  Lemma fupd_plain_strong `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P `{!Plain P} :
+    (|={E1, E2}=> P) ={E1}=∗ ◇ P.
+  Proof. by apply (later_fupd_plain false). Qed.
+
+  Lemma fupd_plain' `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 E2' P Q `{!Plain P} :
+    E1 ⊆ E2 →
+    (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+  Proof.
+    intros (E3&->&HE)%subseteq_disjoint_union_L.
+    apply wand_intro_l. rewrite fupd_frame_r.
+    rewrite fupd_plain_strong fupd_except_0 fupd_plain_weak wand_elim_r.
+    rewrite (fupd_mask_mono E1 (E1 ∪ E3)); last by set_solver+.
+    rewrite fupd_trans -(fupd_trans E1 (E1 ∪ E3) E1).
+    apply fupd_mono. rewrite -fupd_frame_r.
+    apply sep_mono; auto. apply fupd_intro_mask; set_solver+.
+  Qed.
+
   Lemma fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P Q `{!Plain P} :
     E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
   Proof.
@@ -309,4 +327,60 @@ Section fupd_derived.
 
   Lemma step_fupd_intro E1 E2 P : E2 ⊆ E1 → ▷ P -∗ |={E1,E2}▷=> P.
   Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
+
+  Lemma step_fupd_frame_l E1 E2 R Q :
+    (R ∗ |={E1, E2}▷=> Q) -∗ |={E1, E2}▷=> (R ∗ Q).
+  Proof.
+    rewrite fupd_frame_l.
+    apply fupd_mono.
+    rewrite [P in P ∗ _ ⊢ _](later_intro R) -later_sep fupd_frame_l.
+    by apply later_mono, fupd_mono.
+  Qed.
+
+  Lemma step_fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E P `{!Plain P} :
+    (|={E, ∅}▷=> P) ={E}=∗ ▷ ◇ P.
+  Proof.
+    specialize (later_fupd_plain true ∅ E P) => //= ->.
+    rewrite fupd_trans fupd_plain_strong. apply fupd_mono, except_0_later.
+  Qed.
+
+  Lemma step_fupd_fupd E P:
+    (|={E, ∅}▷=> P) ⊣⊢ (|={E, ∅}▷=> |={E}=> P).
+  Proof.
+    apply (anti_symm (⊢)).
+    - by rewrite -fupd_intro.
+    - by rewrite fupd_trans.
+  Qed.
+
+  Lemma step_fupdN_mono E1 E2 n P Q :
+    (P ⊢ Q) → (|={E1, E2}▷=>^n P) ⊢ (|={E1, E2}▷=>^n Q).
+  Proof.
+    intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
+  Qed.
+
+  Lemma step_fupdN_S_fupd n E P:
+    (|={E, ∅}▷=>^(S n) P) ⊣⊢ (|={E, ∅}▷=>^(S n) |={E}=> P).
+  Proof.
+    apply (anti_symm (⊢)); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
+      rewrite -step_fupd_fupd //.
+  Qed.
+
+  Lemma step_fupdN_frame_l E1 E2 n R Q :
+    (R ∗ |={E1, E2}▷=>^n Q) -∗ |={E1, E2}▷=>^n (R ∗ Q).
+  Proof.
+    induction n as [|n IH]; simpl; [done|].
+    rewrite step_fupd_frame_l IH //=.
+  Qed.
+
+  Lemma step_fupdN_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E n P `{!Plain P}:
+    (|={E, ∅}▷=>^n P) ={E}=∗ ▷^n ◇ P.
+  Proof.
+    induction n as [| n].
+    - rewrite -fupd_intro. apply except_0_intro.
+    - rewrite Nat_iter_S step_fupd_fupd IHn ?fupd_trans step_fupd_plain.
+      apply fupd_mono. destruct n; simpl.
+      * by rewrite except_0_idemp.
+      * by rewrite except_0_later.
+  Qed.
+
 End fupd_derived.

theories/program_logic/adequacy.v

 From stdpp Require Import namespaces.
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset.
-From iris.base_logic.lib Require Import wsat.
+From iris.base_logic.lib Require Export wsat.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-(* Global functor setup *)
-Definition invΣ : gFunctors :=
-  #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
-    GFunctor coPset_disjUR;
-    GFunctor (gset_disjUR positive)].
-
-Class invPreG (Σ : gFunctors) : Set := WsatPreG {
-  inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
-  enabled_inPreG :> inG Σ coPset_disjR;
-  disabled_inPreG :> inG Σ (gset_disjR positive);
-}.
-
-Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
-Proof. solve_inG. Qed.
-
-(* Allocation *)
-Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
-Proof.
-  iIntros.
-  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
-  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
-  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
-  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
-  rewrite /wsat /ownE -lock; iFrame.
-  iExists ∅. rewrite fmap_empty big_opM_empty. by iFrame.
-Qed.
-
 (* Program logic adequacy *)
 Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ)
     (φ : val Λ → state Λ → Prop) := {
@@ -66,28 +39,25 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types Φs : list (val Λ → iProp Σ).
 
-Notation world' E σ κs := (wsat ∗ ownE E ∗ state_interp σ κs)%I (only parsing).
-Notation world σ κs := (world' ⊤ σ κs) (only parsing).
-
 Notation wptp s t := ([∗ list] ef ∈ t, WP ef @ s; ⊤ {{ _, True }})%I.
 
 Lemma wp_step s E e1 σ1 κ κs e2 σ2 efs Φ :
   prim_step e1 σ1 κ e2 σ2 efs →
-  world' E σ1 (κ ++ κs) ∗ WP e1 @ s; E {{ Φ }}
-  ==∗  ▷ |==> ◇ (world' E σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
+  state_interp σ1 (κ ++ κs) ∗ WP e1 @ s; E {{ Φ }}
+  ={E, ∅}▷=∗ (state_interp σ2 κs ∗ WP e2 @ s; E {{ Φ }} ∗ wptp s efs).
 Proof.
-  rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
-  rewrite (val_stuck e1 σ1 κ e2 σ2 efs) // uPred_fupd_eq.
-  iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
-  iMod ("H" $! e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
-  iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
+  rewrite {1}wp_unfold /wp_pre. iIntros (?) "[Hσ H]".
+  rewrite (val_stuck e1 σ1 κ e2 σ2 efs) //.
+  iMod ("H" $! σ1 with "Hσ") as "(_ & H)".
+  iMod ("H" $! e2 σ2 efs with "[//]") as "H".
+  by iIntros "!> !>".
 Qed.
 
 Lemma wptp_step s e1 t1 t2 κ κs σ1 σ2 Φ :
   step (e1 :: t1,σ1) κ (t2, σ2) →
-  world σ1 (κ ++ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  state_interp σ1 (κ ++ κs) ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
   ==∗ ∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ ▷ |==> ◇ (world σ2 κs ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+    ⌜t2 = e2 :: t2'⌝ ∗ |={⊤, ∅}▷=> (state_interp σ2 κs ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   iIntros (Hstep) "(HW & He & Ht)".
   destruct Hstep as [e1' σ1' e2' σ2' efs [|? t1'] t2' ?? Hstep]; simplify_eq/=.
@@ -100,77 +70,70 @@ Qed.
 
 Lemma wptp_steps s n e1 t1 κs κs' t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  world σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
-  Nat.iter (S n) (λ P, |==> ▷ P) (∃ e2 t2',
-    ⌜t2 = e2 :: t2'⌝ ∗ world σ2 κs' ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
+  state_interp σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1 ⊢
+  |={⊤, ∅}▷=>^n (∃ e2 t2',
+    ⌜t2 = e2 :: t2'⌝ ∗ state_interp σ2 κs' ∗ WP e2 @ s; ⊤ {{ Φ }} ∗ wptp s t2').
 Proof.
   revert e1 t1 κs κs' t2 σ1 σ2; simpl; induction n as [|n IH]=> e1 t1 κs κs' t2 σ1 σ2 /=.
-  { inversion_clear 1; iIntros "?"; eauto 10. }
+  { inversion_clear 1; iIntros "(?&?&?)"; iExists e1, t1; iFrame; eauto 10. }
   iIntros (Hsteps) "H". inversion_clear Hsteps as [|?? [t1' σ1']].
   rewrite <- app_assoc.
-  iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first by eauto; simplify_eq.
-  subst. iModIntro; iNext; iMod "H" as ">H". by iApply IH.
-Qed.
-
-Lemma bupd_iter_laterN_mono n P Q `{!Plain Q} :
-  (P ⊢ Q) → Nat.iter n (λ P, |==> ▷ P)%I P ⊢ ▷^n Q.
-Proof.
-  intros HPQ. induction n as [|n IH]=> //=. by rewrite IH bupd_plain.
-Qed.
-
-Lemma bupd_iter_frame_l n R Q :
-  R ∗ Nat.iter n (λ P, |==> ▷ P) Q ⊢ Nat.iter n (λ P, |==> ▷ P) (R ∗ Q).
-Proof.
-  induction n as [|n IH]; simpl; [done|].
-  by rewrite bupd_frame_l {1}(later_intro R) -later_sep IH.
+  iMod (wptp_step with "H") as (e1' t1'') "[% H]"; first eauto; simplify_eq.
+  iMod "H". iModIntro; iNext. iMod "H". iModIntro.
+  by iApply IH.
 Qed.
 
 Lemma wptp_result s n e1 t1 κs κs' v2 t2 σ1 σ2 φ :
   nsteps n (e1 :: t1, σ1) κs (of_val v2 :: t2, σ2) →
-  world σ1 (κs ++ κs') ∗
+  state_interp σ1 (κs ++ κs') ∗
   WP e1 @ s; ⊤ {{ v, ∀ σ, state_interp σ κs' ={⊤,∅}=∗ ⌜φ v σ⌝ }} ∗
-  wptp s t1
-  ⊢ ▷^(S (S n)) ⌜φ v2 σ2⌝.
+  wptp s t1 ⊢
+  |={⊤, ∅}▷=>^(S n) ⌜φ v2 σ2⌝.
 Proof.
-  intros. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
-  iDestruct 1 as (e2 t2' ?) "((Hw & HE & Hσ) & H & _)"; simplify_eq.
-  iDestruct (wp_value_inv' with "H") as "H". rewrite uPred_fupd_eq.
-  iMod ("H" with "[$]") as ">(Hw & HE & H)".
-  iMod ("H" with "Hσ [$]") as ">(_ & _ & $)".
+  intros. rewrite Nat_iter_S_r wptp_steps //.
+  apply step_fupdN_mono.
+  iDestruct 1 as (e2 t2' ?) "(Hσ & H & _)"; simplify_eq.
+  iMod (wp_value_inv' with "H") as "H".
+  iMod (later_fupd_plain false ⊤ ∅ (⌜φ v2 σ2⌝)%I with "[H Hσ]") as ">#%".
+  { rewrite //=. by iMod ("H" with "Hσ") as "$". }
+  iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
 Qed.
 
 Lemma wp_safe E e σ κs Φ :
-  world' E σ κs -∗ WP e @ E {{ Φ }} ==∗ ▷ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
+  state_interp σ κs -∗ WP e @ E {{ Φ }} ={E, ∅}▷=∗ ⌜is_Some (to_val e) ∨ reducible e σ⌝.
 Proof.
-  rewrite wp_unfold /wp_pre. iIntros "(Hw&HE&Hσ) H".
+  rewrite wp_unfold /wp_pre. iIntros "Hσ H".
   destruct (to_val e) as [v|] eqn:?.
-  { iIntros "!> !> !%". left. by exists v. }
-  rewrite uPred_fupd_eq. iMod ("H" $! _ [] with "Hσ [-]") as ">(?&?&%&?)"; first by iFrame.
-  iIntros "!> !> !%". by right.
+  { iApply (step_fupd_mask_mono ∅ _ _ ∅); eauto. set_solver. }
+  iMod (later_fupd_plain false E ∅ (⌜reducible e σ⌝)%I with "[H Hσ]") as ">#%".
+  { rewrite //=. by iMod ("H" $! σ [] κs with "Hσ") as "($&H)". }
+  iApply step_fupd_intro; first by set_solver+. 
+  iIntros "!> !%". by right.
 Qed.
 
 Lemma wptp_safe n e1 κs κs' e2 t1 t2 σ1 σ2 Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) → e2 ∈ t2 →
-  world σ1 (κs ++ κs') ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
-  ⊢ ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
+  state_interp σ1 (κs ++ κs') ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
+  ⊢ |={⊤, ∅}▷=>^(S n) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
-  intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
+  intros ? He2. rewrite Nat_iter_S_r wptp_steps //.
+  apply step_fupdN_mono.
   iDestruct 1 as (e2' t2' ?) "(Hw & H & Htp)"; simplify_eq.
   apply elem_of_cons in He2 as [<-|?].
-  - iMod (wp_safe with "Hw H") as "$".
-  - iMod (wp_safe with "Hw [Htp]") as "$". by iApply (big_sepL_elem_of with "Htp").
+  - iMod (wp_safe with "Hw H") as "$"; auto.
+  - iMod (wp_safe with "Hw [Htp]") as "$"; auto. by iApply (big_sepL_elem_of with "Htp").
 Qed.
 
 Lemma wptp_invariance s n e1 κs κs' e2 t1 t2 σ1 σ2 φ Φ :
   nsteps n (e1 :: t1, σ1) κs (t2, σ2) →
-  (state_interp σ2 κs' ={⊤,∅}=∗ ⌜φ⌝) ∗ world σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
-  ⊢ ▷^(S (S n)) ⌜φ⌝.
+  (state_interp σ2 κs' ={⊤,∅}=∗ ⌜φ⌝) ∗ state_interp σ1 (κs ++ κs') ∗ WP e1 @ s; ⊤ {{ Φ }} ∗ wptp s t1
+  ⊢ |={⊤, ∅}▷=>^(S n) |={⊤,∅}=> ⌜φ⌝.
 Proof.
-  intros ?. rewrite wptp_steps // bupd_iter_frame_l laterN_later.
-  apply: bupd_iter_laterN_mono.
-  iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[(Hw&HE&Hσ) _]".
-  rewrite uPred_fupd_eq.
-  iMod ("Hback" with "Hσ [$Hw $HE]") as "> (_ & _ & $)"; auto.
+  intros ?. rewrite Nat_iter_S_r wptp_steps // step_fupdN_frame_l.
+  apply step_fupdN_mono.
+  iIntros "[Hback H]"; iDestruct "H" as (e2' t2' ->) "[Hσ _]".
+  iSpecialize ("Hback" with "Hσ").
+  iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
 Qed.
 End adequacy.
 
@@ -183,17 +146,18 @@ Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
 Proof.
   intros Hwp; split.
   - intros t2 σ2 v2 [n [κs ?]]%erased_steps_nsteps.
-    eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
-    rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
-    iDestruct "Hwp" as (Istate) "[HI Hwp]".
-    iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); first by eauto.
-    rewrite app_nil_r. eauto with iFrame.
+    eapply (step_fupdN_soundness' _ (S (S n))).
+    iIntros (Hinv).
+    rewrite Nat_iter_S.
+    iMod Hwp as (Istate) "[HI Hwp]".
+    iApply (step_fupd_mask_mono ∅ _ _ ∅); auto. iModIntro. iNext; iModIntro.
+    iApply (@wptp_result _ _ (IrisG _ _ _ Hinv Istate) _ _ _ _ _ []); eauto with iFrame.
   - destruct s; last done. intros t2 σ2 e2 _ [n [κs ?]]%erased_steps_nsteps ?.
-    eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-    iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs).
-    rewrite uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
-    iDestruct "Hwp" as (Istate) "[HI Hwp]".
+    eapply (step_fupdN_soundness' _ (S (S n))).
+    iIntros (Hinv).
+    rewrite Nat_iter_S.
+    iMod Hwp as (Istate) "[HI Hwp]".
+    iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
     iApply (@wptp_safe _ _ (IrisG _ _ _ Hinv Istate) _ _ _ []); [by eauto..|].
     rewrite app_nil_r. eauto with iFrame.
 Qed.
@@ -220,10 +184,11 @@ Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
   φ.
 Proof.
   intros Hwp [n [κs ?]]%erased_steps_nsteps.
-  eapply (soundness (M:=iResUR Σ) _ (S (S n))).
-  iMod wsat_alloc as (Hinv) "[Hw HE]". specialize (Hwp _ κs []).
-  rewrite {1}uPred_fupd_eq in Hwp; iMod (Hwp with "[$Hw $HE]") as ">(Hw & HE & Hwp)".
-  iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
+  eapply (step_fupdN_soundness _ (S (S n))).
+  iIntros (Hinv).
+  rewrite Nat_iter_S.
+  iMod (Hwp Hinv κs []) as (Istate) "(HIstate & Hwp & Hclose)".
+  iApply (step_fupd_mask_mono ∅ _ _ ∅); auto.
   iApply (@wptp_invariance _ _ (IrisG _ _ _ Hinv Istate)); eauto with iFrame.
 Qed.