Merge branch 'joe/fupd_adequacy' into 'master'

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

See merge request FP/iris-coq!171

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 "#>HP'".
     { 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 "#HP'"; last by (rewrite plainly_elim; iFrame).
     iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!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 as [|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

@@ -13,6 +13,21 @@ Module invG.
     enabled_name : gname;
     disabled_name : gname;
   }.
+
+  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.
+
 End invG.
 Import invG.
 
@@ -175,3 +190,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.
+    rewrite monPred_at_plainly (bi.forall_elim _) fupd_plainly_weak //=.
+  - intros p E1 E2 P; split=>/= i; specialize (later_fupd_plainly p) => HFP.
+    destruct p; simpl; [ unseal | ]; rewrite monPred_at_plainly (bi.forall_elim _); 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_plainly_weak E (P Q : PROP) :
+    (Q ={E}=∗ ■ P) -∗ Q ={E}=∗ Q ∗ P;
+  later_fupd_plainly p E1 E2 (P : PROP) :
+    (▷?p |={E1, E2}=> ■ P) ={E1}=∗ ▷?p ◇ P;
 }.
 Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
 
@@ -271,13 +272,6 @@ Section fupd_derived.
     intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
   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.
-    intros HE. rewrite -(fupd_plain' _ _ E1) //. apply wand_intro_l.
-    by rewrite wand_elim_r -fupd_intro.
-  Qed.
-
   (** Fancy updates that take a step derived rules. *)
   Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}▷=> P) -∗ (P -∗ Q) -∗ |={E1,E2,E3}▷=> Q.
   Proof.
@@ -309,4 +303,96 @@ 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_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.
+
+  Section fupd_plainly_derived.
+    Context `{BiPlainly PROP, !BiFUpdPlainly PROP}.
+
+    Lemma fupd_plain_weak E P Q `{!Plain P}:
+      (Q ={E}=∗ P) -∗ Q ={E}=∗ Q ∗ P.
+    Proof. by rewrite {1}(plain P) fupd_plainly_weak. Qed.
+
+    Lemma later_fupd_plain p E1 E2 P `{!Plain P} :
+      (▷?p |={E1, E2}=> P) ={E1}=∗ ▷?p ◇ P.
+    Proof. by rewrite {1}(plain P) later_fupd_plainly. Qed.
+
+    Lemma fupd_plain_strong E1 E2 P `{!Plain P} :
+      (|={E1, E2}=> P) ={E1}=∗ ◇ P.
+    Proof. by apply (later_fupd_plain false). Qed.
+
+    Lemma fupd_plain' 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 E1 E2 P Q `{!Plain P} :
+      E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+    Proof.
+      intros HE. rewrite -(fupd_plain' _ _ E1) //. apply wand_intro_l.
+        by rewrite wand_elim_r -fupd_intro.
+    Qed.
+
+    Lemma step_fupd_plain 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_fupdN_plain E n P `{!Plain P}:
+      (|={E, ∅}▷=>^n P) ={E}=∗ ▷^n ◇ P.
+    Proof.
+      induction n as [|n IH].
+      - rewrite -fupd_intro. apply except_0_intro.
+      - rewrite Nat_iter_S step_fupd_fupd IH ?fupd_trans step_fupd_plain.
+        apply fupd_mono. destruct n; simpl.
+        * by rewrite except_0_idemp.
+        * by rewrite except_0_later.
+    Qed.
+  End fupd_plainly_derived.
+
 End fupd_derived.

theories/program_logic/adequacy.v

@@ -6,33 +6,6 @@ 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.