diff --git a/iris_check.v b/iris_check.v
index 236ec9d00bbc8937a09cc126bc8a146f3c4ae052..0fba71722866b899304f5bc520bb8a9d9b4eeba7 100644
--- a/iris_check.v
+++ b/iris_check.v
@@ -192,7 +192,7 @@ Module Import HTRules := IrisHTRules TrivialRA StupidLang Res World Core Plog.
 
 (* And now we check for axioms *)
 Print Assumptions adequacy_obs.
-Print Assumptions adequacy_safe.
+(* TODO enable this once it is proven Print Assumptions adequacy_safe. *)
 
 Print Assumptions lift_atomic_det_step.
 Print Assumptions lift_pure_det_step.
diff --git a/iris_core.v b/iris_core.v
index be03783f5c27ca6808057cd55003943ba05d5889..101ca1017ddf964d683949dba67a27a06e554a6f 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -1,7 +1,7 @@
 Require Import Ssreflect.ssreflect Omega.
 Require Import world_prop core_lang.
 Require Import ModuRes.RA ModuRes.SPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap ModuRes.RAConstr ModuRes.Agreement.
-Require Import ModuRes.CMRA.
+Require Import ModuRes.CMRA ModuRes.DecEnsemble.
 
 Set Bullet Behavior "Strict Subproofs".
 
@@ -60,6 +60,7 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
   Local Open Scope iris_scope.
 
   (** Instances for a bunch of types (some don't even have Setoids) *)
+  Instance state_type : Setoid C.state := _.
   Instance state_metr : metric C.state := discreteMetric.
   Instance state_cmetr : cmetric C.state := discreteCMetric.
   
@@ -67,6 +68,11 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
   Instance nat_metr : metric nat := discreteMetric.
   Instance nat_cmetr : cmetric nat := discreteCMetric.
 
+  Definition mask := DecEnsemble nat.
+  Instance mask_type : Setoid mask := _.
+  Instance mask_metr : metric mask := discreteMetric.
+  Instance mask_cmetr : cmetric mask := discreteCMetric.
+
   Instance expr_type : Setoid expr := discreteType.
   Instance expr_metr : metric expr := discreteMetric.
   Instance expr_cmetr : cmetric expr := discreteCMetric.
diff --git a/iris_derived_rules.v b/iris_derived_rules.v
index 89addfbc0399a42df8453e8601db095208a3b193..f3c55be25693013fdc97897e454b67a66a62aa2e 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -295,13 +295,21 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
           rewrite ->and_projL, box_elim, and_projR. apply and_projL.
     Qed.
 
-    Lemma htFrame safe m m' P R e Q (HD : m # m') :
+    Lemma htWeakenMask safe m m' P e Q (HD: m ⊑ m'):
+      ht safe m P e Q ⊑ ht safe m' P e Q.
+    Proof.
+      rewrite {1}/ht. apply htIntro.
+      etransitivity; last by eapply wpWeakenMask.
+      apply and_impl, box_elim.
+    Qed.
+
+    Lemma htFrame safe m m' P R e Q (*HD: m # m' *):
       ht safe m P e Q ⊑ ht safe (m ∪ m') (P * R) e (lift_bin sc Q (umconst R)).
     Proof.
+      etransitivity; first eapply htWeakenMask with (m' := m ∪ m').
+      { de_auto_eq. }
       rewrite {1}/ht. apply htIntro.
       etransitivity; last by eapply wpFrameRes.
-      etransitivity; last first.
-      { eapply sc_pord; last reflexivity. eapply wpFrameMask. assumption. }
       rewrite -box_conj_star assoc. apply sc_pord; last reflexivity.
       rewrite box_conj_star. apply and_impl, box_elim.
     Qed.
@@ -314,13 +322,13 @@ Module Type IRIS_DERIVED_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C)
       rewrite {1}/ht. apply htIntro.
       etransitivity; last (eapply wpAFrameRes; assumption).
       etransitivity; last first.
-      { eapply sc_pord; last reflexivity. eapply wpFrameMask. assumption. }
+      { eapply sc_pord; last reflexivity. eapply wpFrameMask. }
       rewrite -box_conj_star assoc. apply sc_pord; last reflexivity.
       rewrite box_conj_star. apply and_impl, box_elim.
     Qed.
 
     Lemma htFork safe m P R e :
-      ht safe m P e (umconst ⊤) ⊑ ht safe m (▹P * ▹R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
+      ht safe de_full P e (umconst ⊤) ⊑ ht safe m (▹P * ▹R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
     Proof.
       rewrite {1}/ht. apply htIntro.
       etransitivity; last by eapply wpFork.
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 4a02e440d550ed0a994245103664423f98f1b31e..d4c9a8df1ca0602110ea74b81bde1cfdfce664da 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -86,7 +86,7 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
 
     (** Fork **)
     Lemma wpFork safe m R e :
-      ▹wp safe m e (umconst ⊤) * ▹R ⊑ wp safe m (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).	(* PDS: Why sc not and? RJ: 'cause sc is stronger. *)
+      ▹wp safe de_full e (umconst ⊤) * ▹R ⊑ wp safe m (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).	(* PDS: Why sc not and? RJ: 'cause sc is stronger. *)
     Proof.
       intros w n. destruct n; first (intro; exact:bpred).
       intros [[w1 w2] [EQw [Hwp HLR]]].
@@ -195,24 +195,10 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
     Qed.
 
     (** Framing **)
-    Lemma wpFrameMask safe m1 m2 e φ (HD : m1 # m2) :
+    Lemma wpFrameMask safe m1 m2 e φ (*HD : m1 # m2*) :
       wp safe m1 e φ ⊑ wp safe (m1 ∪ m2) e φ.
     Proof.
-      intros w n; revert w e φ; induction n using wf_nat_ind; rename H into HInd; intros w e φ HW.
-      rewrite unfold_wp; rewrite ->unfold_wp in HW; intros wf; intros.
-      edestruct HW with (mf := mf ∪ m2) as [HV [HS [HF HS'] ] ]; try eassumption;
-      [| eapply wsat_equiv, HE; try reflexivity; de_auto_eq |]; first de_auto_eq.
-      clear HW HE; split; [intros HVal; clear HS HF HInd | split; [intros; clear HV HF | split; [intros; clear HV HS | intros; clear HV HS HF] ] ].
-      - specialize (HV HVal); destruct HV as [w'' [Hφ HE]].
-        eexists. split; [eassumption |].
-        eapply wsat_equiv, HE; try reflexivity; clear; de_auto_eq.
-      - edestruct HS as [w'' [HW HE]]; try eassumption; []; clear HS.
-        eexists; split; [eapply HInd, HW; assumption |].
-        eapply wsat_equiv, HE; try reflexivity; clear; de_auto_eq.
-      - destruct (HF _ _ HDec) as [wfk [wret [HWR [HWF HE]]]]; clear HF.
-        do 2 eexists; do 2 (split; [apply HInd; eassumption |]).
-        eapply wsat_equiv, HE; try reflexivity; clear; de_auto_eq.
-      - auto.
+      eapply wpWeakenMask. de_auto_eq.
     Qed.
 
     Lemma wpFrameRes safe m e φ R:
@@ -289,7 +275,7 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
     (* Unsafe and safe weakest-pre *)
     Lemma wpUnsafe {m e φ} : wp true m e φ ⊑ wp false m e φ.
     Proof.
-      move=> w n. move: n w e φ; elim/wf_nat_ind. move=> n IH w e φ He.
+      move=> w n. move: n w e φ m; elim/wf_nat_ind. move=> n IH w e φ m He.
       rewrite unfold_wp; move=> wf k mf σ HLt HD HW.
       move/(_ _ HLt): IH => IH.
       move/unfold_wp/(_ _ _ _ _ HLt HD HW): He => [HV [HS [HF _] ] ] {HLt HD HW}.
diff --git a/iris_meta.v b/iris_meta.v
index c8d91366e8e585cf311f68cdd7f9a26500cd3156..68e0b9c4d09666c33c8eb1e48c50021070a7483a 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -20,25 +20,25 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
 
 
     (* weakest-pre for a threadpool *)
-    Inductive wptp (safe : bool) m n : tpool -> list Wld -> list vPred -> Prop :=
-    | wp_emp : wptp safe m n nil nil nil
+    Inductive wptp (safe : bool) n : tpool -> list Wld -> list vPred -> Prop :=
+    | wp_emp : wptp safe n nil nil nil
     | wp_cons e φ tp w ws φs
-              (WPE  : wp safe m e φ w n)
-              (WPTP : wptp safe m n tp ws φs) :
-        wptp safe m n (e :: tp) (w :: ws) (φ :: φs).
+              (WPE  : wp safe de_full e φ w n)
+              (WPTP : wptp safe n tp ws φs) :
+        wptp safe n (e :: tp) (w :: ws) (φ :: φs).
 
     (* Trivial lemmas about split over append *)
-    Lemma wptp_app safe m n tp1 tp2 ws1 ws2 φs1 φs2
-          (HW1 : wptp safe m n tp1 ws1 φs1)
-          (HW2 : wptp safe m n tp2 ws2 φs2) :
-      wptp safe m n (tp1 ++ tp2) (ws1 ++ ws2) (φs1 ++ φs2).
+    Lemma wptp_app safe n tp1 tp2 ws1 ws2 φs1 φs2
+          (HW1 : wptp safe n tp1 ws1 φs1)
+          (HW2 : wptp safe n tp2 ws2 φs2) :
+      wptp safe n (tp1 ++ tp2) (ws1 ++ ws2) (φs1 ++ φs2).
     Proof.
       induction HW1; [| constructor]; now trivial.
     Qed.
 
-    Lemma wptp_app_tp safe m n t1 t2 ws φs
-          (HW : wptp safe m n (t1 ++ t2) ws φs) :
-      exists ws1 ws2 φs1 φs2, ws1 ++ ws2 = ws /\ φs1 ++ φs2 = φs /\ wptp safe m n t1 ws1 φs1 /\ wptp safe m n t2 ws2 φs2.
+    Lemma wptp_app_tp safe n t1 t2 ws φs
+          (HW : wptp safe n (t1 ++ t2) ws φs) :
+      exists ws1 ws2 φs1 φs2, ws1 ++ ws2 = ws /\ φs1 ++ φs2 = φs /\ wptp safe n t1 ws1 φs1 /\ wptp safe n t2 ws2 φs2.
     Proof.
       revert ws φs HW; induction t1; intros; inversion HW; simpl in *; subst; clear HW.
       - do 4 eexists. split; [|split; [|split; now econstructor]]; reflexivity.
@@ -48,10 +48,10 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
     Qed.
 
     (* Closure under smaller steps *)
-    Lemma wptp_closure safe m n1 n2 tp ws φs
+    Lemma wptp_closure safe n1 n2 tp ws φs
           (HLe : n2 <= n1)
-          (HW : wptp safe m n1 tp ws φs) :
-      wptp safe m n2 tp ws φs.
+          (HW : wptp safe n1 tp ws φs) :
+      wptp safe n2 tp ws φs.
     Proof.
       induction HW; constructor; [| assumption].
       eapply dpred, WPE. assumption.
@@ -76,12 +76,12 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
         reflexivity.
     Qed.
 
-    Lemma preserve_wptp w0 safe m n k tp tp' σ σ' ws φs
+    Lemma preserve_wptp w0 safe n k tp tp' σ σ' ws φs
           (HSN  : stepn n (tp, σ) (tp', σ'))
-          (HWTP : wptp safe m (n + (S k)) tp ws φs)
-          (HE   : wsat σ m (comp_wlist ws w0) (n + (S k))) :
+          (HWTP : wptp safe (n + (S k)) tp ws φs)
+          (HE   : wsat σ de_full (comp_wlist ws w0) (n + (S k))) :
       exists ws' φs',
-        wptp safe m (S k) tp' ws' (φs ++ φs') /\ wsat σ' m (comp_wlist ws' w0) (S k).
+        wptp safe (S k) tp' ws' (φs ++ φs') /\ wsat σ' de_full (comp_wlist ws' w0) (S k).
     Proof.
       revert tp σ w0 ws φs HSN HWTP HE. induction n; intros; inversion HSN; subst; clear HSN.
       (* no step is taken *)
@@ -145,13 +145,15 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
             (HT  : valid (ht safe m P e Q))
             (HSN : stepn n ([e], σ) (tp', σ'))
             (HP  : P w (n + S k))
-            (HE  : wsat σ m w (n + S k)) :
+            (HE  : wsat σ de_full w (n + S k)) :
       exists ws' φs',
-        wptp safe m (S k) tp' ws' (Q :: φs') /\ wsat σ' m (comp_wlist ws' (1 w)) (S k).
+        wptp safe (S k) tp' ws' (Q :: φs') /\ wsat σ' de_full (comp_wlist ws' (1 w)) (S k).
     Proof.
       edestruct (preserve_wptp (1 w)) with (ws := [w]) as [ws' [φs' [HSWTP' HSWS']]]; first eassumption.
       - specialize (HT w (n + S k)). apply (applyImpl HT) in HP; try reflexivity; [|now apply unit_min].
-        econstructor; [|now econstructor]. eassumption.
+        econstructor; [|now econstructor].
+        eapply wpWeakenMask; last eassumption.
+        de_auto_eq.
       - simpl comp_wlist. rewrite ra_op_unit. eassumption.
       - exists ws' φs'. now auto.
     Qed.
@@ -161,7 +163,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
             (HT  : valid (ht safe m (ownS σ) e Q))
             (HSN : steps ([e], σ) (tp', σ')):
       exists w0 ws' φs',
-        wptp safe m (S (S k')) tp' ws' (Q :: φs') /\ wsat σ' m (comp_wlist ws' w0) (S (S k')).
+        wptp safe (S (S k')) tp' ws' (Q :: φs') /\ wsat σ' de_full (comp_wlist ws' w0) (S (S k')).
     Proof.
       destruct (refl_trans_n _ HSN) as [n HSN']. clear HSN.
       destruct (RL.res_vira) as [l Hval].
@@ -207,7 +209,7 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
     Qed.
 
     (* Adequacy for safe triples *)
-    Theorem adequacy_safe m e (Q : vPred) tp' σ σ' e'
+    Theorem adequacy_safe_expr m e (Q : vPred) tp' σ σ' e'
             (HT  : valid (ht true m (ownS σ) e Q))
             (HSN : steps ([e], σ) (tp', σ'))
             (HE  : e' ∈ tp'):
@@ -225,6 +227,14 @@ Module Type IRIS_META (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       - apply HSafe. reflexivity.
     Qed.
 
+    Theorem adequacy_safe m e (Q : vPred) tp' σ σ' e'
+            (HT  : valid (ht true m (ownS σ) e Q))
+            (HSN : steps ([e], σ) (tp', σ')):
+      (forall e', e' ∈ tp' -> is_value e') \/ exists tp'' σ'', step (tp', σ') (tp'', σ'').
+    Proof.
+      (* TODO: Prove this. *)
+    Abort.
+
   End Adequacy.
 
   Section StatefulLifting.
diff --git a/iris_plog.v b/iris_plog.v
index a11329fa96b5496d4189b26ef1d07d5ce317aba2..6e973084f71abddddebfceb05865e81747eb3cc0 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -18,7 +18,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
   Local Open Scope iris_scope.
   Local Open Scope de_scope.
   
-  Implicit Types (P : Props) (u v w : Wld) (n i k : nat) (m : DecEnsemble nat) (r : res) (σ : state) (φ : vPred) (s : nat -f> Wld).
+  Implicit Types (P : Props) (u v w : Wld) (n i k : nat) (m : mask) (r : res) (σ : state) (φ : vPred) (s : nat -f> Wld).
 
   Section WorldSatisfaction.
 
@@ -328,7 +328,7 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
         + reflexivity.
     Qed.
 
-    Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n :=
+    Definition wpFP safe (WP : mask -n> expr -n> vPred -n> Props) m e φ w n :=
       forall wf k mf σ (HLt : S k < n) (HD : mf # m)
              (HE : wsat σ (m ∪ mf) (w · wf) (S (S k))),
         (forall (HV : is_value e),
@@ -336,17 +336,17 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
                     /\ wsat σ (m ∪ mf) (w' · wf) (S (S k))) /\
         (forall σ' ei ei' K (HDec : e = fill K ei)
                 (HStep : prim_step (ei, σ) (ei', σ')),
-            exists w', WP (fill K ei') φ w' (S k)
+            exists w', WP m (fill K ei') φ w' (S k)
                        /\ wsat σ' (m ∪ mf) (w' · wf) (S k)) /\
         (forall e' K (HDec : e = fill K (fork e')),
-            exists wfk wret, WP (fill K fork_ret) φ wret (S k)
-                             /\ WP e' (umconst ⊤) wfk (S k)
+            exists wfk wret, WP m (fill K fork_ret) φ wret (S k)
+                             /\ WP de_full e' (umconst ⊤) wfk (S k)
                              /\ wsat σ (m ∪ mf) (wfk · wret · wf) (S k)) /\
         (forall HSafe : safe = true, safeExpr e σ).
 
     (* Define the function wp will be a fixed-point of *)
-    Program Definition wpF safe m : (expr -n> vPred -n> Props) -> (expr -n> vPred -n> Props) :=
-      fun WP => n[(fun e => n[(fun φ => m[(fun w => p[(wpFP safe m WP e φ w)] )])])].
+    Program Definition wpF safe : (mask -n> expr -n> vPred -n> Props) -> (mask -n> expr -n> vPred -n> Props) :=
+      fun WP => n[(fun m => n[(fun e => n[(fun φ => m[(fun w => p[(wpFP safe WP m e φ w)] )])])])].
     Next Obligation.
       intro. intros. inversion HLt.
     Qed.
@@ -406,20 +406,66 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
         apply EQφ, Hφ; omega.
       - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [Hφ HE']].
         exists w''. split; last assumption.
-        eapply (met_morph_nonexp (WP _)), Hφ; [symmetry; eassumption | omega].
+        eapply (met_morph_nonexp (WP _ _)), Hφ; [symmetry; eassumption | omega].
       - specialize (HF _ _ HDec); destruct HF as [wfk [wret [HWR [HWF HE']]]].
         exists wfk wret. split; last tauto.
-        eapply (met_morph_nonexp (WP _)), HWR; [symmetry; eassumption | omega].
+        eapply (met_morph_nonexp (WP _ _)), HWR; [symmetry; eassumption | omega].
       - auto.
     Qed.
     Next Obligation.
       intros e1 e2 EQe φ w. destruct n as [| n]; first exact:dist_bound.
       simpl in EQe; hnf in EQe; subst e2; reflexivity.
     Qed.
+    Next Obligation.
+      move=>m1 m2 EQm e φ w. destruct n; first exact:dist_bound.
+      move:φ w e. split=>Hwp.
+      - move=>wf; intros.
+        destruct (Hwp wf k mf σ) as (Hval & Hstep & Hfork & Hsafe); [assumption|de_auto_eq|now rewrite EQm|].
+        split; last split; last split; last assumption.
+        + move=>HV. specialize (Hval HV). destruct Hval as (w' & HP & HW).
+          exists w'. split; first assumption. now rewrite -EQm.
+        + move=>? ? ? ? Hfill Hpstep. specialize (Hstep _ _ _ _ Hfill Hpstep).
+          destruct Hstep as (w' & Hwp' & HW). exists w'. split.
+          * eapply spredNE, Hwp'. eapply mmorph_proper; last reflexivity.
+            eapply pcm_dist_inherit, mmorph_proper; last reflexivity.
+            eapply mmorph_proper; last reflexivity. eapply met_morph_nonexp.
+            eapply dist_mono, EQm.
+          * rewrite -EQm. assumption.
+        + move=>? ? Hfill. specialize (Hfork _ _ Hfill).
+          destruct Hfork as (wfk & wret & Hwp' & Hwp'' & HW).
+          exists wfk wret. split; last split.
+          * eapply spredNE, Hwp'. eapply mmorph_proper; last reflexivity.
+            eapply pcm_dist_inherit, mmorph_proper; last reflexivity.
+            eapply mmorph_proper; last reflexivity. eapply met_morph_nonexp.
+            eapply dist_mono, EQm.
+          * assumption. 
+          * now rewrite -EQm.
+      - move=>wf; intros.
+        destruct (Hwp wf k mf σ) as (Hval & Hstep & Hfork & Hsafe); [assumption|de_auto_eq|now rewrite -EQm|].
+        split; last split; last split; last assumption.
+        + move=>HV. specialize (Hval HV). destruct Hval as (w' & HP & HW).
+          exists w'. split; first assumption. now rewrite EQm.
+        + move=>? ? ? ? Hfill Hpstep. specialize (Hstep _ _ _ _ Hfill Hpstep).
+          destruct Hstep as (w' & Hwp' & HW). exists w'. split.
+          * eapply spredNE, Hwp'. eapply mmorph_proper; last reflexivity.
+            eapply pcm_dist_inherit, mmorph_proper; last reflexivity.
+            eapply mmorph_proper; last reflexivity. eapply met_morph_nonexp.
+            symmetry. eapply dist_mono, EQm.
+          * now rewrite EQm.
+        + move=>? ? Hfill. specialize (Hfork _ _ Hfill).
+          destruct Hfork as (wfk & wret & Hwp' & Hwp'' & HW).
+          exists wfk wret. split; last split.
+          * eapply spredNE, Hwp'. eapply mmorph_proper; last reflexivity.
+            eapply pcm_dist_inherit, mmorph_proper; last reflexivity.
+            eapply mmorph_proper; last reflexivity. eapply met_morph_nonexp.
+            symmetry. eapply dist_mono, EQm.
+          * assumption.
+          * now rewrite EQm.
+    Qed.
 
-    Instance contr_wpF safe m : contractive (wpF safe m).
+    Instance contr_wpF safe : contractive (wpF safe).
     Proof.
-      intros n WP1 WP2 EQWP e φ w k HLt.
+      intros n WP1 WP2 EQWP m e φ w k HLt.
       split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
       - split; [assumption | split; [| split]; intros].
         + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [HWP HE']].
@@ -439,52 +485,14 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
         + auto.
     Qed.
 
-    Definition wp safe m : expr -n> vPred -n> Props :=
-      fixp (wpF safe m) (umconst (umconst ⊤)).
+    Definition wp safe : mask -n> expr -n> vPred -n> Props :=
+      fixp (wpF safe) (umconst (umconst (umconst ⊤))).
 
-    Lemma unfold_wp safe m :
-      wp safe m == (wpF safe m) (wp safe m).
+    Lemma unfold_wp safe :
+      wp safe == (wpF safe) (wp safe).
     Proof.
       unfold wp; apply fixp_eq.
     Qed.
-
-    Global Instance wp_mproper safe:
-      Proper (equiv ==> equiv) (wp safe).
-    Proof.
-      move=>m1 m2 EQm e φ w n. move:n φ w e. induction n using wf_nat_ind; intros; rename H into IH.
-      rewrite [wp safe m1]unfold_wp [wp safe m2]unfold_wp.
-      split=>Hwp.
-      - move=>wf; intros.
-        destruct (Hwp wf k mf σ) as (Hval & Hstep & Hfork & Hsafe); [assumption|de_auto_eq|now rewrite EQm|].
-        split; last split; last split; last assumption.
-        + move=>HV. specialize (Hval HV). destruct Hval as (w' & HP & HW).
-          exists w'. split; first assumption. now rewrite -EQm.
-        + move=>? ? ? ? Hfill Hpstep. specialize (Hstep _ _ _ _ Hfill Hpstep).
-          destruct Hstep as (w' & Hwp' & HW). exists w'. split.
-          * erewrite <-IH by assumption. assumption.
-          * now rewrite -EQm.
-        + move=>? ? Hfill. specialize (Hfork _ _ Hfill).
-          destruct Hfork as (wfk & wret & Hwp' & Hwp'' & HW).
-          exists wfk wret. split; last split.
-          * erewrite <-IH by assumption. assumption.
-          * erewrite <-IH by assumption. assumption.
-          * now rewrite -EQm.
-      - move=>wf; intros.
-        destruct (Hwp wf k mf σ) as (Hval & Hstep & Hfork & Hsafe); [assumption|de_auto_eq|now rewrite -EQm|].
-        split; last split; last split; last assumption.
-        + move=>HV. specialize (Hval HV). destruct Hval as (w' & HP & HW).
-          exists w'. split; first assumption. now rewrite EQm.
-        + move=>? ? ? ? Hfill Hpstep. specialize (Hstep _ _ _ _ Hfill Hpstep).
-          destruct Hstep as (w' & Hwp' & HW). exists w'. split.
-          * erewrite ->IH by assumption. assumption.
-          * now rewrite EQm.
-        + move=>? ? Hfill. specialize (Hfork _ _ Hfill).
-          destruct Hfork as (wfk & wret & Hwp' & Hwp'' & HW).
-          exists wfk wret. split; last split.
-          * erewrite ->IH by assumption. assumption.
-          * erewrite ->IH by assumption. assumption.
-          * now rewrite EQm.
-    Qed.
     
     Global Opaque wp.
 
@@ -526,6 +534,27 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       eapply propsMN, Hφ; assumption.
     Qed.
 
+    Lemma wpWeakenMask safe m1 m2 e φ (HD : m1 ⊑ m2) :
+      wp safe m1 e φ ⊑ wp safe m2 e φ.
+    Proof.
+      intros w n; revert w e φ; induction n using wf_nat_ind; rename H into HInd; intros w e φ HW.
+      rewrite unfold_wp; rewrite ->unfold_wp in HW; intros wf; intros.
+      edestruct HW with (mf := mf ∪ (m2 \ m1)) as [HV [HS [HF HS'] ] ]; try eassumption;
+      [| eapply wsat_equiv, HE; try reflexivity; de_auto_eq |]; first de_auto_eq.
+      clear HW HE; split; [intros HVal; clear HS HF HInd | split; [intros; clear HV HF | split; [intros; clear HV HS | intros; clear HV HS HF] ] ].
+      - specialize (HV HVal); destruct HV as [w'' [Hφ HE]].
+        eexists. split; [eassumption |].
+        eapply wsat_equiv, HE; try reflexivity; clear; de_auto_eq.
+      - edestruct HS as [w'' [HW HE]]; try eassumption; []; clear HS.
+        eexists; split; [eapply HInd, HW; assumption |].
+        eapply wsat_equiv, HE; try reflexivity; clear; de_auto_eq.
+      - destruct (HF _ _ HDec) as [wfk [wret [HWR [HWF HE]]]]; clear HF.
+        do 2 eexists. split; [eapply HInd; eassumption|].
+        split; first eassumption.
+        eapply wsat_equiv, HE; try reflexivity; clear; de_auto_eq.
+      - auto.
+    Qed.
+
   End WeakestPre.
 
   Section DerivedForms.
@@ -570,7 +599,9 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       move=>m0 m1 EQm P0 P1 HEQP e0 e1 HEQe Q0 Q1 HEQQ.
       unfold ht. apply box_equiv. apply impl_equiv; first assumption.
       apply equiv_morph; last assumption.
-      hnf in HEQe. subst e1. now rewrite EQm.
+      hnf in HEQe. subst e1.
+      eapply mmorph_inherit. eapply equiv_morph; last reflexivity.
+      eapply mmorph_inherit, morph_resp. assumption.
     Qed.
 
     Lemma htIntro R safe m e P Q: