diff --git a/Makefile b/Makefile
index 9a069d7689496c599d9d0b0c3ca15487b84837c7..1d0c327fcdc94bb01421088f1469a5771574b13b 100644
--- a/Makefile
+++ b/Makefile
@@ -85,6 +85,7 @@ VFILES:=core_lang.v\
   iris_meta.v\
   iris_vs.v\
   iris_wp.v\
+  iris_wp_rules.v\
   lang.v\
   masks.v\
   world_prop.v
diff --git a/iris_core.v b/iris_core.v
index 2b4a74b21f34f9e8b75eebb9fd85f26bc72e545b..eacbbe38661aaf9bd1bad60b71e5f19fd3545712 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -4,7 +4,11 @@ Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finma
 
 Set Bullet Behavior "Strict Subproofs".
 
-Module IrisRes (RL : RA_T) (C : CORE_LANG) <: RA_T.
+(* Because Coq has a restriction of how to apply functors, we have to hack a bit here.
+   The hack that involves least work, is to duplicate the definition of our final
+   resource type, as a module type (which is how we can use it, circumventing the
+   Coq restrictions) and as a module (to show the type can be instantiated). *)
+Module Type IRIS_RES (RL : RA_T) (C : CORE_LANG) <: RA_T.
   Instance state_type : Setoid C.state := discreteType.
   
   Definition res := (ra_res_ex C.state * RL.res)%type.
@@ -16,12 +20,15 @@ Module IrisRes (RL : RA_T) (C : CORE_LANG) <: RA_T.
 
   (* The order on (ra_pos res) is inferred correctly, but this one is not *)
   Instance res_pord: preoType res := ra_preo res.
+End IRIS_RES.
+Module IrisRes (RL : RA_T) (C : CORE_LANG) <: IRIS_RES RL C.
+  Include IRIS_RES RL C. (* I cannot believe Coq lets me do this... *)
 End IrisRes.
 
-Module IrisCore (RL : RA_T) (C : CORE_LANG).
+Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R).
   Export C.
-  Module Export R  := IrisRes RL C.
-  Module Export WP := WorldProp R.
+  Export R.
+  Export WP.
 
   Delimit Scope iris_scope with iris.
   Local Open Scope ra_scope.
@@ -441,4 +448,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
 
   Ltac wsatM H := solve [done | apply (wsatM H); solve [done | omega] ].
 
+End IRIS_CORE.
+
+Module IrisCore (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) : IRIS_CORE RL C R WP.
+  Include IRIS_CORE RL C R WP.
 End IrisCore.
diff --git a/iris_meta.v b/iris_meta.v
index effbc85828a4502591f5217bc3c16fbc4324ccbc..6c2f6b323fae2c274e545bb365a2318fb50bd092 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -1,11 +1,12 @@
 Require Import ssreflect.
-Require Import core_lang masks iris_wp.
+Require Import core_lang masks world_prop iris_core iris_vs iris_wp.
 Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Set Bullet Behavior "Strict Subproofs".
 
-Module IrisMeta (RL : RA_T) (C : CORE_LANG).
-  Module Export WP := IrisWP RL C.
+Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE).
+  Export VS.
+  Export HT.
 
   Local Open Scope lang_scope.
   Local Open Scope ra_scope.
@@ -201,6 +202,8 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
   Set Bullet Behavior "None".	(* PDS: Ridiculous. *)
   Section RobustSafety.
 
+    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
+
     Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres) (w : Wld) (σ : state).
 
     Program Definition restrictV (Q : expr -n> Props) : vPred :=
@@ -385,4 +388,8 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
 
   End Lifting.
 
+End IRIS_META.
+
+Module IrisMeta (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE) : IRIS_META RL C R WP CORE VS HT.
+  Include IRIS_META RL C R WP CORE VS HT.
 End IrisMeta.
diff --git a/iris_vs.v b/iris_vs.v
index 9a2ba7f9c619a849fa29607645683303ee951438..c9edec2f038f9eef43ab0b99cc8e56d3042a6077 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -4,8 +4,8 @@ Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finma
 
 Set Bullet Behavior "Strict Subproofs".
 
-Module IrisVS (RL : RA_T) (C : CORE_LANG).
-  Module Export CORE := IrisCore RL C.
+Module Type IRIS_VS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP).
+  Export CORE.
 
   Local Open Scope ra_scope.
   Local Open Scope bi_scope.
@@ -79,8 +79,6 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
 
   Section ViewShiftProps.
 
-    Definition mask_sing i := mask_set mask_emp i True.
-
     Lemma vsTimeless m P :
       timeless P ⊑ vs m m (▹P) P.
     Proof.
@@ -332,4 +330,8 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
 
   End ViewShiftProps.
 
+End IRIS_VS.
+
+Module IrisVS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_VS RL C R WP CORE.
+  Include IRIS_VS RL C R WP CORE.
 End IrisVS.
diff --git a/iris_wp.v b/iris_wp.v
index 508ad887ddf6244180acfcceea61f43ed443b674..7dd2fd703493d3504ddf35021dd64ad0ad2b06fb 100644
--- a/iris_wp.v
+++ b/iris_wp.v
@@ -1,12 +1,12 @@
 Require Import ssreflect.
-Require Import world_prop core_lang lang masks iris_vs.
+Require Import world_prop core_lang lang masks iris_core.
 Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Set Bullet Behavior "Strict Subproofs".
 
-Module IrisWP (RL : RA_T) (C : CORE_LANG).
+Module Type IRIS_HT (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP).
+  Export CORE.
   Module Export L  := Lang C.
-  Module Export VS := IrisVS RL C.
 
   Local Open Scope lang_scope.
   Local Open Scope ra_scope.
@@ -197,391 +197,17 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
 
     Opaque wp.
 
-    Definition ht safe m P e Q := □(P → wp safe m e Q).
-
-  End HoareTriples.
-  
-  Section HoareTripleProperties.
-
-    Existing Instance LP_isval.
-
-    Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres).
-
-    (** Ret **)
-    Program Definition eqV v : vPred :=
-      n[(fun v' : value => v === v')].
-    Next Obligation.
-      intros v1 v2 EQv w m r HLt; destruct n as [| n]; [now inversion HLt | simpl in *].
-      split; congruence.
-    Qed.
-
-    Lemma htRet e (HV : is_value e) safe m :
-      valid (ht safe m ⊤ e (eqV (exist _ e HV))).
-    Proof.
-      intros w' nn rr w _ n r' _ _ _; clear w' nn rr.
-      rewrite unfold_wp; intros w'; intros; split; [| split; [| split] ]; intros.
-      - exists w' r'; split; [reflexivity | split; [| assumption] ].
-        simpl; reflexivity.
-      - contradiction (values_stuck _ HV _ _ HDec).
-        repeat eexists; eassumption.
-      - subst e; assert (HT := fill_value _ _ HV); subst K.
-        revert HV; rewrite fill_empty; intros.
-        contradiction (fork_not_value _ HV).
-      - unfold safeExpr. auto.
-    Qed.
-
     Lemma wpO {safe m e Q w r} : wp safe m e Q w O r.
     Proof.
       rewrite unfold_wp; intros w'; intros; now inversion HLt.
     Qed.
 
-    (** Bind **)
-
-    (** Quantification in the logic works over nonexpansive maps, so
-        we need to show that plugging the value into the postcondition
-        and context is nonexpansive. *)
-    Program Definition plugV safe m Q Q' K :=
-      n[(fun v : value => ht safe m (Q v) (K [[` v]]) Q')].
-    Next Obligation.
-      intros v1 v2 EQv; unfold ht; eapply (met_morph_nonexp _ _ box).
-      eapply (impl_dist (ComplBI := Props_BI)).
-      - apply Q; assumption.
-      - destruct n as [| n]; [apply dist_bound | simpl in EQv].
-        rewrite EQv; reflexivity.
-    Qed.
-
-    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
-    Lemma htBind P Q R K e safe m :
-      ht safe m P e Q ∧ all (plugV safe m Q R K) ⊑ ht safe m P (K [[ e ]]) R.
-    Proof.
-      intros wz nz rz [He HK] w HSw n r HLe _ HP.
-      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
-      rewrite ->HSw, <- HLe in HK; clear wz nz HSw HLe HP.
-      revert e w r He HK; induction n using wf_nat_ind; intros; rename H into IH.
-      rewrite ->unfold_wp in He; rewrite unfold_wp.
-      destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
-      - intros w'; intros; edestruct He as [HV _]; try eassumption; [].
-        clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ HE] ] ] ].
-        (* Fold the goal back into a wp *)
-        setoid_rewrite HSw'.
-        assert (HT : wp safe m (K [[ e ]]) R w'' (S k) r');
-          [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
-        clear HE; specialize (HK (exist _ e HVal)).
-        do 30 red in HK; unfold proj1_sig in HK.
-        apply HK; [etransitivity; eassumption | apply HLt | apply unit_min | assumption].
-      - intros w'; intros; edestruct He as [_ [HS [HF HS'] ] ]; try eassumption; [].
-        split; [intros HVal; contradiction HNVal; assert (HT := fill_value _ _ HVal);
-                subst K; rewrite fill_empty in HVal; assumption | split; [| split]; intros].
-        + clear He HF HE; edestruct step_by_value as [K' EQK];
-          [eassumption | repeat eexists; eassumption | eassumption |].
-          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
-          edestruct HS as [w'' [r' [HSw' [He HE] ] ] ]; try eassumption; [].
-          subst e; clear HStep HS.
-          do 2 eexists; split; [eassumption | split; [| eassumption] ].
-          rewrite <- fill_comp. apply IH; try assumption; [].
-          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
-        + clear He HS HE; edestruct fork_by_value as [K' EQK]; try eassumption; [].
-          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
-          edestruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE] ] ] ] ] ];
-            try eassumption; []; subst e; clear HF.
-          do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
-          rewrite <- fill_comp; apply IH; try assumption; [].
-          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
-        + clear IH He HS HE HF; specialize (HS' HSafe); clear HSafe.
-          destruct HS' as [HV | [HS | HF] ].
-          { contradiction. }
-          { right; left; destruct HS as [σ' [ei [ei' [K0 [HE HS] ] ] ] ].
-            exists σ' ei ei' (K ∘ K0); rewrite -> HE, fill_comp. auto. }
-          { right; right; destruct HF as [e' [K0 HE] ].
-            exists e' (K ∘ K0). rewrite -> HE, fill_comp. auto. }
-    Qed.
-
-    (** Consequence **)
-
-    (** Much like in the case of the plugging, we need to show that
-        the map from a value to a view shift between the applied
-        postconditions is nonexpansive *)
-    Program Definition vsLift m1 m2 (φ φ' : vPred) :=
-      n[(fun v => vs m1 m2 (φ v) (φ' v))].
-    Next Obligation.
-      intros v1 v2 EQv; unfold vs.
-      rewrite ->EQv; reflexivity.
-    Qed.
-
-    Lemma htCons P P' Q Q' safe m e :
-      vs m m P P' ∧ ht safe m P' e Q' ∧ all (vsLift m m Q' Q) ⊑ ht safe m P e Q.
-    Proof.
-      intros wz nz rz [ [HP He] HQ] w HSw n r HLe _ Hp.
-      specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
-      rewrite <- HLe, HSw in He, HQ; clear wz nz HSw HLe Hp.
-      intros w'; intros; edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [now rewrite mask_union_idem |].
-      clear HP HE; rewrite ->HSw in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
-      setoid_rewrite HSw'.
-      assert (HT : wp safe m e Q w'' (S k) r');
-        [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
-      unfold lt in HLt; rewrite ->HSw, HSw', <- HLt in HQ; clear - He HQ.
-      (* Second phase of the proof: got rid of the preconditions,
-         now induction takes care of the evaluation. *)
-      rename r' into r; rename w'' into w.
-      revert w r e He HQ; generalize (S k) as n; clear k; induction n using wf_nat_ind.
-      rename H into IH; intros; rewrite ->unfold_wp; rewrite ->unfold_wp in He.
-      intros w'; intros; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
-      split; [intros HVal; clear HS HF IH HS' | split; intros; [clear HV HF HS' | split; [intros; clear HV HS HS' | clear HV HS HF ] ] ].
-      - clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [HQ' HE] ] ] ].
-        eapply HQ in HQ'; [| etransitivity; eassumption | apply HLt | apply unit_min].
-        clear w n HSw HQ HLt; edestruct HQ' as [w [r'' [HSw [HQ HE'] ] ] ];
-        [reflexivity | apply le_n | rewrite mask_union_idem; eassumption | eassumption |].
-        exists w r''; split; [etransitivity; eassumption | split; assumption].
-      - clear HE He; edestruct HS as [w'' [r' [HSw' [He HE] ] ] ];
-        try eassumption; clear HS.
-        do 2 eexists; split; [eassumption | split; [| eassumption] ].
-        apply IH; try assumption; [].
-        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HQ.
-      - clear HE He; edestruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ]; [eassumption |].
-        clear HF; do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
-        apply IH; try assumption; [].
-        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HQ.
-      - assumption.
-    Qed.
-
-    Lemma htACons safe m m' e P P' Q Q'
-          (HAt   : atomic e)
-          (HSub  : m' ⊆ m) :
-      vs m m' P P' ∧ ht safe m' P' e Q' ∧ all (vsLift m' m Q' Q) ⊑ ht safe m P e Q.
-    Proof.
-      intros wz nz rz [ [HP He] HQ] w HSw n r HLe _ Hp.
-      specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
-      split; [intros HV; contradiction (atomic_not_value e) |].
-      edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [|]; clear HP.
-      { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
-        destruct Hmm'; [| apply HSub]; assumption.
-      }
-      split; [| split; [intros; subst; contradiction (fork_not_atomic K e') |] ].
-      - intros; rewrite <- HLe, HSw in He, HQ; clear wz nz HSw HLe Hp.
-        clear HE; rewrite ->HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
-        unfold lt in HLt; rewrite ->HSw0, <- HLt in HQ; clear w n HSw0 HLt Hp'.
-        rewrite ->unfold_wp in He; edestruct He as [_ [HS _] ];
-          [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
-        edestruct HS as [w [r'' [HSw [He' HE] ] ] ]; try eassumption; clear He HS HE'.
-        destruct k as [| k]; [exists w' r'; split; [reflexivity | split; [apply wpO | exact I] ] |].
-        assert (HNV : ~ is_value ei)
-          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
-        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
-        rewrite ->fill_empty in *; rename ei into e.
-        setoid_rewrite HSw'; setoid_rewrite HSw.
-        assert (HVal := atomic_step _ _ _ _ HAt HStep).
-        rewrite ->HSw', HSw in HQ; clear - HE He' HQ HSub HVal HD.
-        rewrite ->unfold_wp in He'; edestruct He' as [HV _];
-        [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
-        clear HE He'; specialize (HV HVal); destruct HV as [w' [r [HSw [HQ' HE] ] ] ].
-        eapply HQ in HQ'; [| assumption | apply Le.le_n_Sn | apply unit_min].
-        clear HQ; edestruct HQ' as [w'' [r' [HSw' [HQ HE'] ] ] ];
-          [reflexivity | apply le_n | | eassumption |].
-        { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
-          destruct Hmm'; [apply HSub |]; assumption.
-        }
-        clear HQ' HE; exists w'' r'; split;
-        [etransitivity; eassumption | split; [| eassumption] ].
-        clear - HQ; rewrite ->unfold_wp; intros w; intros; split; [intros HVal' | split; intros; [intros; exfalso|split; [intros |] ] ].
-        + do 2 eexists; split; [reflexivity | split; [| eassumption] ].
-          unfold lt in HLt; rewrite ->HLt, <- HSw.
-          eapply Q, HQ; [| apply le_n]; simpl; reflexivity.
-        + eapply values_stuck; [.. | repeat eexists]; eassumption.
-        + clear - HDec HVal; subst; assert (HT := fill_value _ _ HVal); subst.
-          rewrite ->fill_empty in HVal; now apply fork_not_value in HVal.
-        + intros; left; assumption.
-      - clear HQ; intros; rewrite <- HLe, HSw in He; clear HLe HSw.
-        specialize (He w'' (transitivity HSw0 HSw') _ r' HLt (unit_min _ _) Hp').
-        rewrite ->unfold_wp in He; edestruct He as [_ [_ [_ HS'] ] ];
-          [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
-        auto.
-    Qed.
-
-    (** Framing **)
-
-    (** Helper lemma to weaken the region mask *)
-    Lemma wp_mask_weaken 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 φ r HW.
-      rewrite unfold_wp; rewrite ->unfold_wp in HW; intros w'; intros.
-      edestruct HW with (mf := mf ∪ m2) as [HV [HS [HF HS'] ] ]; try eassumption;
-      [| eapply wsat_equiv, HE; try reflexivity; [] |].
-      { intros j [ [Hmf | Hm'] Hm]; [unfold mcup in HD0; apply (HD0 j) | apply (HD j) ]; tauto.
-      }
-      { clear; intros j; unfold mcup; tauto.
-      }
-      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'' [r' [HSW [Hφ HE] ] ] ].
-        do 2 eexists; split; [eassumption | split; [eassumption |] ].
-        eapply wsat_equiv, HE; try reflexivity; [].
-        intros j; unfold mcup; tauto.
-      - edestruct HS as [w'' [r' [HSW [HW HE] ] ] ]; try eassumption; []; clear HS.
-        do 2 eexists; split; [eassumption | split; [eapply HInd, HW; assumption |] ].
-        eapply wsat_equiv, HE; try reflexivity; [].
-        intros j; unfold mcup; tauto.
-      - destruct (HF _ _ HDec) as [w'' [rfk [rret [HSW [HWR [HWF HE] ] ] ] ] ]; clear HF.
-        do 3 eexists; split; [eassumption |].
-        do 2 (split; [apply HInd; eassumption |]).
-        eapply wsat_equiv, HE; try reflexivity; [].
-        intros j; unfold mcup; tauto.
-      - auto.
-    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.
-      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
-      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
-      clear P w n rz HSw HLe HP; rename w' into w; rename n' into n.
-      apply wp_mask_weaken; [assumption |]; revert e w r1 r EQr HLR He.
-      induction n using wf_nat_ind; intros; rename H into IH.
-      rewrite ->unfold_wp; rewrite ->unfold_wp in He; intros w'; intros.
-      rewrite <- EQr, <- assoc in HE; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
-      clear He; split; [intros HVal; clear HS HF IH HE | split; [clear HV HF HE | clear HV HS HE; split; [clear HS' | clear HF] ]; intros ].
-      - specialize (HV HVal); destruct HV as [w'' [r1' [HSw' [Hφ HE] ] ] ].
-        rewrite ->assoc in HE. exists w''.
-        exists↓ (ra_proj r1' · ra_proj r2).
-        { apply wsat_valid in HE. auto_valid. }
-        split; [eassumption | split; [| eassumption ] ].
-        exists r1' r2; split; [reflexivity | split; [assumption |] ].
-        unfold lt in HLt; rewrite ->HLt, <- HSw', <- HSw; apply HLR.
-      - edestruct HS as [w'' [r1' [HSw' [He HE] ] ] ]; try eassumption; []; clear HS.
-        destruct k as [| k]; [exists w' r1'; split; [reflexivity | split; [apply wpO | exact I] ] |].
-        rewrite ->assoc in HE. exists w''. exists↓ (ra_proj r1' · ra_proj r2).
-        { apply wsat_valid in HE. auto_valid. }
-        split; [eassumption | split; [| eassumption] ].
-        eapply IH; try eassumption; [ reflexivity |].
-        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
-      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ].
-        destruct k as [| k]; [exists w' rfk rret; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
-        rewrite ->assoc, <- (assoc (_ rfk)) in HE.
-        exists w''. exists rfk. exists↓ (ra_proj rret · ra_proj r2).
-        { clear- HE. apply wsat_valid in HE. eapply ra_op_valid2, ra_op_valid; try now apply _. eassumption. }
-        split; [eassumption | split; [| split; eassumption] ].
-        eapply IH; try eassumption; [ reflexivity |].
-        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
-      - auto.
-    Qed.
-
-    Lemma htAFrame safe m m' P R e Q
-          (HD  : m # m')
-          (HAt : atomic e) :
-      ht safe m P e Q ⊑ ht safe (m ∪ m') (P * ▹R) e (lift_bin sc Q (umconst R)).
-    Proof.
-      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
-      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
-      clear rz n HLe; apply wp_mask_weaken; [assumption |]; rewrite ->unfold_wp.
-      clear w HSw; rename n' into n; rename w' into w; intros w'; intros.
-      split; [intros; exfalso | split; intros; [| split; intros; [exfalso| ] ] ].
-      - contradiction (atomic_not_value e).
-      - destruct k as [| k];
-        [exists w' r; split; [reflexivity | split; [apply wpO | exact I] ] |].
-        rewrite ->unfold_wp in He; rewrite <- EQr, <- assoc in HE.
-        edestruct He as [_ [HeS _] ]; try eassumption; [].
-        edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
-        clear HE He HeS; rewrite ->assoc in HE'.
-        exists w''. exists↓ (ra_proj r1' · ra_proj r2).
-        { clear- HE'. apply wsat_valid in HE'. auto_valid. }
-        split; [eassumption | split; [| eassumption] ].
-        assert (HNV : ~ is_value ei)
-          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
-        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
-        rewrite ->fill_empty in *.
-        unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; simpl in HLR.
-        assert (HVal := atomic_step _ _ _ _ HAt HStep).
-        clear - He' HVal HLR; rename w'' into w; rewrite ->unfold_wp; intros w'; intros.
-        split; [intros HV; clear HVal | split; intros; [exfalso| split; intros; [exfalso |] ] ].
-        + rewrite ->unfold_wp in He'. rewrite ra_proj_cancel in HE. rewrite <-assoc in HE.
-          edestruct He' as [HVal _]; try eassumption; [].
-          specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
-          rewrite ->assoc in HE'.
-          exists w''. exists↓ (ra_proj r1'' · ra_proj r2).
-          { clear- HE'. apply wsat_valid in HE'. auto_valid. }
-          split; [eassumption | split; [| eassumption] ].
-          exists r1'' r2; split; [reflexivity | split; [assumption |] ].
-          unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
-        + eapply values_stuck; [.. | repeat eexists]; eassumption.
-        + subst; clear -HVal.
-          assert (HT := fill_value _ _ HVal); subst K; rewrite ->fill_empty in HVal.
-          contradiction (fork_not_value e').
-        + unfold safeExpr. now auto.
-      - subst; eapply fork_not_atomic; eassumption.
-      - rewrite <- EQr, <- assoc in HE; rewrite ->unfold_wp in He.
-        specialize (He w' k (ra_proj r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
-        destruct He as [_ [_ [_ HS'] ] ]; auto.
-    Qed.
-
-    (** Fork **)
-    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)).
-    Proof.
-      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
-      destruct n' as [| n']; [apply wpO |].
-      simpl in HP; specialize (He _ HSw _ _ (Le.le_Sn_le _ _ HLe) (unit_min _ _) HP).
-      clear rz n HLe; rewrite ->unfold_wp.
-      clear w HSw HP; rename n' into n; rename w' into w; intros w'; intros.
-      split; [intros; contradiction (fork_not_value e) | split; intros; [exfalso | split; intros ] ].
-      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec; subst.
-        eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
-      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec.
-        apply fork_inj in HDec; subst e'; rewrite <- EQr in HE.
-        unfold lt in HLt; rewrite <- (le_S_n _ _ HLt), HSw in He.
-        simpl in HLR; rewrite <- Le.le_n_Sn in HE.
-        do 3 eexists; split; [reflexivity | split; [| split; eassumption] ].
-        rewrite ->fill_empty; rewrite ->unfold_wp; rewrite <- (le_S_n _ _ HLt), HSw in HLR.
-        clear - HLR; intros w''; intros; split; [intros | split; intros; [exfalso | split; intros; [exfalso |] ] ].
-        + do 2 eexists; split; [reflexivity | split; [| eassumption] ].
-          exists (ra_pos_unit) r2; split; [unfold ra_pos_unit; simpl; now erewrite ra_op_unit by apply _ |].
-          split; [| unfold lt in HLt; rewrite <- HLt, HSw in HLR; apply HLR].
-          simpl; reflexivity.
-        + eapply values_stuck; [exact fork_ret_is_value | eassumption | repeat eexists; eassumption].
-        + assert (HV := fork_ret_is_value); rewrite ->HDec in HV; clear HDec.
-          assert (HT := fill_value _ _ HV);subst K; rewrite ->fill_empty in HV.
-          eapply fork_not_value; eassumption.
-        + left; apply fork_ret_is_value.
-      - right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.
-    Qed.
-
-    Set Bullet Behavior "None".	(* PDS: Ridiculous. *)
-
-    Lemma htUnsafe {m P e Q} : ht true m P e Q ⊑ ht false m P e Q.
-    Proof.
-      move=> wz nz rz He w HSw n r HLe Hr HP.
-      move: {He P wz nz rz HSw HLe Hr HP} (He _ HSw _ _ HLe Hr HP).
-      move: n e Q w r; elim/wf_nat_ind; move=> n IH e Q w r He.
-      rewrite unfold_wp; move=> w' k rf mf σ HSw HLt HD Hw.
-      move: {IH} (IH _ HLt) => IH.
-      move: He => /unfold_wp He; move: {He HSw HLt HD Hw} (He _ _ _ _ _ HSw HLt HD Hw) => [HV [HS [HF _] ] ].
-      split; [done | clear HV; split; [clear HF | split; [clear HS | done] ] ].
-      - move=> σ' ei ei' K HK Hs.
-        move: {HS HK Hs} (HS _ _ _ _ HK Hs) => [w'' [r' [HSw' [He' Hw'] ] ] ].
-        exists w'' r'; split; [done | split; [exact: IH | done] ].
-      move=> e' K HK.
-      move: {HF HK} (HF _ _ HK) => [w'' [rfk [rret [HSw' [Hk [He' Hw'] ] ] ] ] ].
-      exists w'' rfk rret; split; [done | split; [exact: IH | split; [exact: IH | done] ] ].
-    Qed.
-    
-    Set Bullet Behavior "Strict Subproofs".
-
-  End HoareTripleProperties.
-
-  Section DerivedRules.
-
-    Existing Instance LP_isval.
-
-    Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (r : res).
+    Definition ht safe m P e Q := □(P → wp safe m e Q).
 
-    Lemma vsFalse m1 m2 :
-      valid (vs m1 m2 ⊥ ⊥).
-    Proof.
-      rewrite ->valid_iff, box_top.
-      unfold vs; apply box_intro.
-      rewrite <- and_impl, and_projR.
-      apply bot_false.
-    Qed.
+  End HoareTriples.
 
-  End DerivedRules.
+End IRIS_HT.
 
-End IrisWP.
+Module IrisHT (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_HT RL C R WP CORE.
+  Include IRIS_HT RL C R WP CORE.
+End IrisHT.
diff --git a/iris_wp_rules.v b/iris_wp_rules.v
new file mode 100644
index 0000000000000000000000000000000000000000..fcb65a786592cb028c2a694e801b778ca9f80ec9
--- /dev/null
+++ b/iris_wp_rules.v
@@ -0,0 +1,398 @@
+Require Import ssreflect.
+Require Import world_prop core_lang lang masks iris_core iris_vs iris_wp.
+Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
+
+Set Bullet Behavior "Strict Subproofs".
+
+Module Type IRIS_WP_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE).
+  Export VS.
+  Export HT.
+
+  Local Open Scope lang_scope.
+  Local Open Scope ra_scope.
+  Local Open Scope bi_scope.
+  Local Open Scope iris_scope.
+  
+  Section HoareTripleProperties.
+
+    Existing Instance LP_isval.
+
+    Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres).
+
+    (** Ret **)
+    Program Definition eqV v : vPred :=
+      n[(fun v' : value => v === v')].
+    Next Obligation.
+      intros v1 v2 EQv w m r HLt; destruct n as [| n]; [now inversion HLt | simpl in *].
+      split; congruence.
+    Qed.
+
+    Lemma htRet e (HV : is_value e) safe m :
+      valid (ht safe m ⊤ e (eqV (exist _ e HV))).
+    Proof.
+      intros w' nn rr w _ n r' _ _ _; clear w' nn rr.
+      rewrite unfold_wp; intros w'; intros; split; [| split; [| split] ]; intros.
+      - exists w' r'; split; [reflexivity | split; [| assumption] ].
+        simpl; reflexivity.
+      - contradiction (values_stuck _ HV _ _ HDec).
+        repeat eexists; eassumption.
+      - subst e; assert (HT := fill_value _ _ HV); subst K.
+        revert HV; rewrite fill_empty; intros.
+        contradiction (fork_not_value _ HV).
+      - unfold safeExpr. auto.
+    Qed.
+
+    (** Bind **)
+
+    (** Quantification in the logic works over nonexpansive maps, so
+        we need to show that plugging the value into the postcondition
+        and context is nonexpansive. *)
+    Program Definition plugV safe m Q Q' K :=
+      n[(fun v : value => ht safe m (Q v) (K [[` v]]) Q')].
+    Next Obligation.
+      intros v1 v2 EQv; unfold ht; eapply (met_morph_nonexp _ _ box).
+      eapply (impl_dist (ComplBI := Props_BI)).
+      - apply Q; assumption.
+      - destruct n as [| n]; [apply dist_bound | simpl in EQv].
+        rewrite EQv; reflexivity.
+    Qed.
+
+    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
+
+    Lemma htBind P Q R K e safe m :
+      ht safe m P e Q ∧ all (plugV safe m Q R K) ⊑ ht safe m P (K [[ e ]]) R.
+    Proof.
+      intros wz nz rz [He HK] w HSw n r HLe _ HP.
+      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
+      rewrite ->HSw, <- HLe in HK; clear wz nz HSw HLe HP.
+      revert e w r He HK; induction n using wf_nat_ind; intros; rename H into IH.
+      rewrite ->unfold_wp in He; rewrite unfold_wp.
+      destruct (is_value_dec e) as [HVal | HNVal]; [clear IH |].
+      - intros w'; intros; edestruct He as [HV _]; try eassumption; [].
+        clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [Hφ HE] ] ] ].
+        (* Fold the goal back into a wp *)
+        setoid_rewrite HSw'.
+        assert (HT : wp safe m (K [[ e ]]) R w'' (S k) r');
+          [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | unfold lt; reflexivity | eassumption | eassumption] ].
+        clear HE; specialize (HK (exist _ e HVal)).
+        do 30 red in HK; unfold proj1_sig in HK.
+        apply HK; [etransitivity; eassumption | apply HLt | apply unit_min | assumption].
+      - intros w'; intros; edestruct He as [_ [HS [HF HS'] ] ]; try eassumption; [].
+        split; [intros HVal; contradiction HNVal; assert (HT := fill_value _ _ HVal);
+                subst K; rewrite fill_empty in HVal; assumption | split; [| split]; intros].
+        + clear He HF HE; edestruct step_by_value as [K' EQK];
+          [eassumption | repeat eexists; eassumption | eassumption |].
+          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
+          edestruct HS as [w'' [r' [HSw' [He HE] ] ] ]; try eassumption; [].
+          subst e; clear HStep HS.
+          do 2 eexists; split; [eassumption | split; [| eassumption] ].
+          rewrite <- fill_comp. apply IH; try assumption; [].
+          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
+        + clear He HS HE; edestruct fork_by_value as [K' EQK]; try eassumption; [].
+          subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
+          edestruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE] ] ] ] ] ];
+            try eassumption; []; subst e; clear HF.
+          do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
+          rewrite <- fill_comp; apply IH; try assumption; [].
+          unfold lt in HLt; rewrite <- HSw', <- HSw, Le.le_n_Sn, HLt; apply HK.
+        + clear IH He HS HE HF; specialize (HS' HSafe); clear HSafe.
+          destruct HS' as [HV | [HS | HF] ].
+          { contradiction. }
+          { right; left; destruct HS as [σ' [ei [ei' [K0 [HE HS] ] ] ] ].
+            exists σ' ei ei' (K ∘ K0); rewrite -> HE, fill_comp. auto. }
+          { right; right; destruct HF as [e' [K0 HE] ].
+            exists e' (K ∘ K0). rewrite -> HE, fill_comp. auto. }
+    Qed.
+
+    (** Consequence **)
+
+    (** Much like in the case of the plugging, we need to show that
+        the map from a value to a view shift between the applied
+        postconditions is nonexpansive *)
+    Program Definition vsLift m1 m2 (φ φ' : vPred) :=
+      n[(fun v => vs m1 m2 (φ v) (φ' v))].
+    Next Obligation.
+      intros v1 v2 EQv; unfold vs.
+      rewrite ->EQv; reflexivity.
+    Qed.
+
+    Lemma htCons P P' Q Q' safe m e :
+      vs m m P P' ∧ ht safe m P' e Q' ∧ all (vsLift m m Q' Q) ⊑ ht safe m P e Q.
+    Proof.
+      intros wz nz rz [ [HP He] HQ] w HSw n r HLe _ Hp.
+      specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
+      rewrite <- HLe, HSw in He, HQ; clear wz nz HSw HLe Hp.
+      intros w'; intros. edestruct HP with (mf:=mf) as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [now rewrite mask_union_idem |].
+      clear HP HE; rewrite ->HSw in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
+      setoid_rewrite HSw'.
+      assert (HT : wp safe m e Q w'' (S k) r');
+        [| rewrite ->unfold_wp in HT; eapply HT; [reflexivity | apply le_n | eassumption | eassumption] ].
+      unfold lt in HLt; rewrite ->HSw, HSw', <- HLt in HQ; clear - He HQ.
+      (* Second phase of the proof: got rid of the preconditions,
+         now induction takes care of the evaluation. *)
+      rename r' into r; rename w'' into w.
+      revert w r e He HQ; generalize (S k) as n; clear k; induction n using wf_nat_ind.
+      rename H into IH; intros; rewrite ->unfold_wp; rewrite ->unfold_wp in He.
+      intros w'; intros; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
+      split; [intros HVal; clear HS HF IH HS' | split; intros; [clear HV HF HS' | split; [intros; clear HV HS HS' | clear HV HS HF ] ] ].
+      - clear He HE; specialize (HV HVal); destruct HV as [w'' [r' [HSw' [HQ' HE] ] ] ].
+        eapply HQ in HQ'; [| etransitivity; eassumption | apply HLt | apply unit_min].
+        clear w n HSw HQ HLt; edestruct HQ' as [w [r'' [HSw [HQ HE'] ] ] ];
+        [reflexivity | apply le_n | rewrite mask_union_idem; eassumption | eassumption |].
+        exists w r''; split; [etransitivity; eassumption | split; assumption].
+      - clear HE He; edestruct HS as [w'' [r' [HSw' [He HE] ] ] ];
+        try eassumption; clear HS.
+        do 2 eexists; split; [eassumption | split; [| eassumption] ].
+        apply IH; try assumption; [].
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HQ.
+      - clear HE He; edestruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ]; [eassumption |].
+        clear HF; do 3 eexists; split; [eassumption | split; [| split; eassumption] ].
+        apply IH; try assumption; [].
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HQ.
+      - assumption.
+    Qed.
+
+    Lemma htACons safe m m' e P P' Q Q'
+          (HAt   : atomic e)
+          (HSub  : m' ⊆ m) :
+      vs m m' P P' ∧ ht safe m' P' e Q' ∧ all (vsLift m' m Q' Q) ⊑ ht safe m P e Q.
+    Proof.
+      intros wz nz rz [ [HP He] HQ] w HSw n r HLe _ Hp.
+      specialize (HP _ HSw _ _ HLe (unit_min _ _) Hp); rewrite unfold_wp.
+      split; [intros HV; contradiction (atomic_not_value e) |].
+      edestruct HP as [w'' [r' [HSw' [Hp' HE'] ] ] ]; try eassumption; [|]; clear HP.
+      { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
+        destruct Hmm'; [| apply HSub]; assumption.
+      }
+      split; [| split; [intros; subst; contradiction (fork_not_atomic K e') |] ].
+      - intros; rewrite <- HLe, HSw in He, HQ; clear wz nz HSw HLe Hp.
+        clear HE; rewrite ->HSw0 in He; specialize (He w'' HSw' _ r' HLt (unit_min _ _) Hp').
+        unfold lt in HLt; rewrite ->HSw0, <- HLt in HQ; clear w n HSw0 HLt Hp'.
+        rewrite ->unfold_wp in He; edestruct He as [_ [HS _] ];
+          [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
+        edestruct HS as [w [r'' [HSw [He' HE] ] ] ]; try eassumption; clear He HS HE'.
+        destruct k as [| k]; [exists w' r'; split; [reflexivity | split; [apply wpO | exact I] ] |].
+        assert (HNV : ~ is_value ei)
+          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
+        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
+        rewrite ->fill_empty in *; rename ei into e.
+        setoid_rewrite HSw'; setoid_rewrite HSw.
+        assert (HVal := atomic_step _ _ _ _ HAt HStep).
+        rewrite ->HSw', HSw in HQ; clear - HE He' HQ HSub HVal HD.
+        rewrite ->unfold_wp in He'; edestruct He' as [HV _];
+        [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
+        clear HE He'; specialize (HV HVal); destruct HV as [w' [r [HSw [HQ' HE] ] ] ].
+        eapply HQ in HQ'; [| assumption | apply Le.le_n_Sn | apply unit_min].
+        clear HQ; edestruct HQ' as [w'' [r' [HSw' [HQ HE'] ] ] ];
+          [reflexivity | apply le_n | | eassumption |].
+        { intros j [Hmf Hmm']; apply (HD j); split; [assumption |].
+          destruct Hmm'; [apply HSub |]; assumption.
+        }
+        clear HQ' HE; exists w'' r'; split;
+        [etransitivity; eassumption | split; [| eassumption] ].
+        clear - HQ; rewrite ->unfold_wp; intros w; intros; split; [intros HVal' | split; intros; [intros; exfalso|split; [intros |] ] ].
+        + do 2 eexists; split; [reflexivity | split; [| eassumption] ].
+          unfold lt in HLt; rewrite ->HLt, <- HSw.
+          eapply Q, HQ; [| apply le_n]; simpl; reflexivity.
+        + eapply values_stuck; [.. | repeat eexists]; eassumption.
+        + clear - HDec HVal; subst; assert (HT := fill_value _ _ HVal); subst.
+          rewrite ->fill_empty in HVal; now apply fork_not_value in HVal.
+        + intros; left; assumption.
+      - clear HQ; intros; rewrite <- HLe, HSw in He; clear HLe HSw.
+        specialize (He w'' (transitivity HSw0 HSw') _ r' HLt (unit_min _ _) Hp').
+        rewrite ->unfold_wp in He; edestruct He as [_ [_ [_ HS'] ] ];
+          [reflexivity | apply le_n | rewrite ->HSub; eassumption | eassumption |].
+        auto.
+    Qed.
+
+    (** Framing **)
+
+    (** Helper lemma to weaken the region mask *)
+    Lemma wp_mask_weaken 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 φ r HW.
+      rewrite unfold_wp; rewrite ->unfold_wp in HW; intros w'; intros.
+      edestruct HW with (mf := mf ∪ m2) as [HV [HS [HF HS'] ] ]; try eassumption;
+      [| eapply wsat_equiv, HE; try reflexivity; [] |].
+      { intros j [ [Hmf | Hm'] Hm]; [unfold mcup in HD0; apply (HD0 j) | apply (HD j) ]; tauto.
+      }
+      { clear; intros j; unfold mcup; tauto.
+      }
+      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'' [r' [HSW [Hφ HE] ] ] ].
+        do 2 eexists; split; [eassumption | split; [eassumption |] ].
+        eapply wsat_equiv, HE; try reflexivity; [].
+        intros j; unfold mcup; tauto.
+      - edestruct HS as [w'' [r' [HSW [HW HE] ] ] ]; try eassumption; []; clear HS.
+        do 2 eexists; split; [eassumption | split; [eapply HInd, HW; assumption |] ].
+        eapply wsat_equiv, HE; try reflexivity; [].
+        intros j; unfold mcup; tauto.
+      - destruct (HF _ _ HDec) as [w'' [rfk [rret [HSW [HWR [HWF HE] ] ] ] ] ]; clear HF.
+        do 3 eexists; split; [eassumption |].
+        do 2 (split; [apply HInd; eassumption |]).
+        eapply wsat_equiv, HE; try reflexivity; [].
+        intros j; unfold mcup; tauto.
+      - auto.
+    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.
+      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
+      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
+      clear P w n rz HSw HLe HP; rename w' into w; rename n' into n.
+      apply wp_mask_weaken; [assumption |]; revert e w r1 r EQr HLR He.
+      induction n using wf_nat_ind; intros; rename H into IH.
+      rewrite ->unfold_wp; rewrite ->unfold_wp in He; intros w'; intros.
+      rewrite <- EQr, <- assoc in HE; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
+      clear He; split; [intros HVal; clear HS HF IH HE | split; [clear HV HF HE | clear HV HS HE; split; [clear HS' | clear HF] ]; intros ].
+      - specialize (HV HVal); destruct HV as [w'' [r1' [HSw' [Hφ HE] ] ] ].
+        rewrite ->assoc in HE. exists w''.
+        exists↓ (ra_proj r1' · ra_proj r2).
+        { apply wsat_valid in HE. auto_valid. }
+        split; [eassumption | split; [| eassumption ] ].
+        exists r1' r2; split; [reflexivity | split; [assumption |] ].
+        unfold lt in HLt; rewrite ->HLt, <- HSw', <- HSw; apply HLR.
+      - edestruct HS as [w'' [r1' [HSw' [He HE] ] ] ]; try eassumption; []; clear HS.
+        destruct k as [| k]; [exists w' r1'; split; [reflexivity | split; [apply wpO | exact I] ] |].
+        rewrite ->assoc in HE. exists w''. exists↓ (ra_proj r1' · ra_proj r2).
+        { apply wsat_valid in HE. auto_valid. }
+        split; [eassumption | split; [| eassumption] ].
+        eapply IH; try eassumption; [ reflexivity |].
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
+      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ].
+        destruct k as [| k]; [exists w' rfk rret; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
+        rewrite ->assoc, <- (assoc (_ rfk)) in HE.
+        exists w''. exists rfk. exists↓ (ra_proj rret · ra_proj r2).
+        { clear- HE. apply wsat_valid in HE. eapply ra_op_valid2, ra_op_valid; try now apply _. eassumption. }
+        split; [eassumption | split; [| split; eassumption] ].
+        eapply IH; try eassumption; [ reflexivity |].
+        unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
+      - auto.
+    Qed.
+
+    Lemma htAFrame safe m m' P R e Q
+          (HD  : m # m')
+          (HAt : atomic e) :
+      ht safe m P e Q ⊑ ht safe (m ∪ m') (P * ▹R) e (lift_bin sc Q (umconst R)).
+    Proof.
+      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
+      specialize (He _ HSw _ _ HLe (unit_min _ _) HP).
+      clear rz n HLe; apply wp_mask_weaken; [assumption |]; rewrite ->unfold_wp.
+      clear w HSw; rename n' into n; rename w' into w; intros w'; intros.
+      split; [intros; exfalso | split; intros; [| split; intros; [exfalso| ] ] ].
+      - contradiction (atomic_not_value e).
+      - destruct k as [| k];
+        [exists w' r; split; [reflexivity | split; [apply wpO | exact I] ] |].
+        rewrite ->unfold_wp in He; rewrite <- EQr, <- assoc in HE.
+        edestruct He as [_ [HeS _] ]; try eassumption; [].
+        edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
+        clear HE He HeS; rewrite ->assoc in HE'.
+        exists w''. exists↓ (ra_proj r1' · ra_proj r2).
+        { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+        split; [eassumption | split; [| eassumption] ].
+        assert (HNV : ~ is_value ei)
+          by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
+        subst e; assert (HT := atomic_fill _ _ HAt HNV); subst K; clear HNV.
+        rewrite ->fill_empty in *.
+        unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; simpl in HLR.
+        assert (HVal := atomic_step _ _ _ _ HAt HStep).
+        clear - He' HVal HLR; rename w'' into w; rewrite ->unfold_wp; intros w'; intros.
+        split; [intros HV; clear HVal | split; intros; [exfalso| split; intros; [exfalso |] ] ].
+        + rewrite ->unfold_wp in He'. rewrite ra_proj_cancel in HE. rewrite <-assoc in HE.
+          edestruct He' as [HVal _]; try eassumption; [].
+          specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
+          rewrite ->assoc in HE'.
+          exists w''. exists↓ (ra_proj r1'' · ra_proj r2).
+          { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+          split; [eassumption | split; [| eassumption] ].
+          exists r1'' r2; split; [reflexivity | split; [assumption |] ].
+          unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
+        + eapply values_stuck; [.. | repeat eexists]; eassumption.
+        + subst; clear -HVal.
+          assert (HT := fill_value _ _ HVal); subst K; rewrite ->fill_empty in HVal.
+          contradiction (fork_not_value e').
+        + unfold safeExpr. now auto.
+      - subst; eapply fork_not_atomic; eassumption.
+      - rewrite <- EQr, <- assoc in HE; rewrite ->unfold_wp in He.
+        specialize (He w' k (ra_proj r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
+        destruct He as [_ [_ [_ HS'] ] ]; auto.
+    Qed.
+
+    (** Fork **)
+    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)).
+    Proof.
+      intros w n rz He w' HSw n' r HLe _ [r1 [r2 [EQr [HP HLR] ] ] ].
+      destruct n' as [| n']; [apply wpO |].
+      simpl in HP; specialize (He _ HSw _ _ (Le.le_Sn_le _ _ HLe) (unit_min _ _) HP).
+      clear rz n HLe; rewrite ->unfold_wp.
+      clear w HSw HP; rename n' into n; rename w' into w; intros w'; intros.
+      split; [intros; contradiction (fork_not_value e) | split; intros; [exfalso | split; intros ] ].
+      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec; subst.
+        eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
+      - assert (HT := fill_fork _ _ _ HDec); subst K; rewrite ->fill_empty in HDec.
+        apply fork_inj in HDec; subst e'; rewrite <- EQr in HE.
+        unfold lt in HLt; rewrite <- (le_S_n _ _ HLt), HSw in He.
+        simpl in HLR; rewrite <- Le.le_n_Sn in HE.
+        do 3 eexists; split; [reflexivity | split; [| split; eassumption] ].
+        rewrite ->fill_empty; rewrite ->unfold_wp; rewrite <- (le_S_n _ _ HLt), HSw in HLR.
+        clear - HLR; intros w''; intros; split; [intros | split; intros; [exfalso | split; intros; [exfalso |] ] ].
+        + do 2 eexists; split; [reflexivity | split; [| eassumption] ].
+          exists (ra_pos_unit) r2; split; [unfold ra_pos_unit; simpl; now erewrite ra_op_unit by apply _ |].
+          split; [| unfold lt in HLt; rewrite <- HLt, HSw in HLR; apply HLR].
+          simpl; reflexivity.
+        + eapply values_stuck; [exact fork_ret_is_value | eassumption | repeat eexists; eassumption].
+        + assert (HV := fork_ret_is_value); rewrite ->HDec in HV; clear HDec.
+          assert (HT := fill_value _ _ HV);subst K; rewrite ->fill_empty in HV.
+          eapply fork_not_value; eassumption.
+        + left; apply fork_ret_is_value.
+      - right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.
+    Qed.
+
+    Set Bullet Behavior "None".	(* PDS: Ridiculous. *)
+
+    Lemma htUnsafe {m P e Q} : ht true m P e Q ⊑ ht false m P e Q.
+    Proof.
+      move=> wz nz rz He w HSw n r HLe Hr HP.
+      move: {He P wz nz rz HSw HLe Hr HP} (He _ HSw _ _ HLe Hr HP).
+      move: n e Q w r; elim/wf_nat_ind; move=> n IH e Q w r He.
+      rewrite unfold_wp; move=> w' k rf mf σ HSw HLt HD Hw.
+      move: {IH} (IH _ HLt) => IH.
+      move: He => /unfold_wp He; move: {He HSw HLt HD Hw} (He _ _ _ _ _ HSw HLt HD Hw) => [HV [HS [HF _] ] ].
+      split; [done | clear HV; split; [clear HF | split; [clear HS | done] ] ].
+      - move=> σ' ei ei' K HK Hs.
+        move: {HS HK Hs} (HS _ _ _ _ HK Hs) => [w'' [r' [HSw' [He' Hw'] ] ] ].
+        exists w'' r'; split; [done | split; [exact: IH | done] ].
+      move=> e' K HK.
+      move: {HF HK} (HF _ _ HK) => [w'' [rfk [rret [HSw' [Hk [He' Hw'] ] ] ] ] ].
+      exists w'' rfk rret; split; [done | split; [exact: IH | split; [exact: IH | done] ] ].
+    Qed.
+    
+    Set Bullet Behavior "Strict Subproofs".
+
+  End HoareTripleProperties.
+
+  Section DerivedRules.
+
+    Existing Instance LP_isval.
+
+    Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (r : res).
+
+    Lemma vsFalse m1 m2 :
+      valid (vs m1 m2 ⊥ ⊥).
+    Proof.
+      rewrite ->valid_iff, box_top.
+      unfold vs; apply box_intro.
+      rewrite <- and_impl, and_projR.
+      apply bot_false.
+    Qed.
+
+  End DerivedRules.
+
+End IRIS_WP_RULES.
+
+Module IrisWPRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (VS: IRIS_VS RL C R WP CORE) (HT: IRIS_HT RL C R WP CORE) : IRIS_WP_RULES RL C R WP CORE VS HT.
+  Include IRIS_WP_RULES RL C R WP CORE VS HT.
+End IrisWPRules.
diff --git a/masks.v b/masks.v
index baae9e2a8cc8a4751faf0348001169f29c2f2e94..1cc6960e789f224766f24db91de9aa6ebc6b7958 100644
--- a/masks.v
+++ b/masks.v
@@ -130,3 +130,5 @@ Proof.
   intros m1 m1' EQm1 m2 m2' EQm2; split; intros Hd k [Hm1 Hm2];
   apply (Hd k); (split; [apply EQm1, Hm1 | apply EQm2, Hm2]).
 Qed.
+
+Definition mask_sing i := mask_set mask_emp i True.