diff --git a/Makefile b/Makefile
index 1d0c327fcdc94bb01421088f1469a5771574b13b..a7e4ef57a2757b935584da3cecd8bb7c8d64b677 100644
--- a/Makefile
+++ b/Makefile
@@ -1,21 +1,5 @@
-#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.4pl4     ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris_core.v iris_meta.v iris_vs.v iris_wp.v lang.v masks.v world_prop.v -o Makefile 
-#
+# This Makefile started being auto-generated, but now it's hand-crafted and automatically finds all the files.
+# YOU SHOULD NOT HAVE TO EDIT THIS FILE.
 
 .DEFAULT_GOAL := all
 
@@ -80,15 +64,7 @@ endif
 #                    #
 ######################
 
-VFILES:=core_lang.v\
-  iris_core.v\
-  iris_meta.v\
-  iris_vs.v\
-  iris_wp.v\
-  iris_wp_rules.v\
-  lang.v\
-  masks.v\
-  world_prop.v
+VFILES:=$(wildcard *.v)
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))
diff --git a/iris_core.v b/iris_core.v
index eacbbe38661aaf9bd1bad60b71e5f19fd3545712..5609f3f4484f0d58ffeec7eab6ab0e560b3677bb 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -25,6 +25,9 @@ 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.
 
+(* This instantiates the framework(s) provided by ModuRes to obtain a higher-order
+   separation logic with ownership, later, necessitation and equality.
+   The logic has "worlds" in its model, but nothing here uses them yet. *)
 Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R).
   Export C.
   Export R.
@@ -160,33 +163,6 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
   Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope.
 
-  Section Invariants.
-
-    (** Invariants **)
-    Definition invP i P w : UPred pres :=
-      intEqP (w i) (Some (ı' P)).
-    Program Definition inv i : Props -n> Props :=
-      n[(fun P => m[(invP i P)])].
-    Next Obligation.
-      intros w1 w2 EQw; unfold invP; simpl morph.
-      destruct n; [apply dist_bound |].
-      apply intEq_dist; [apply EQw | reflexivity].
-    Qed.
-    Next Obligation.
-      intros w1 w2 Sw; unfold invP; simpl morph.
-      intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
-      destruct (w1 i) as [μ1 |]; [| contradiction].
-      destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
-      rewrite <- Sw; assumption.
-    Qed.
-    Next Obligation.
-      intros p1 p2 EQp w; unfold invP; simpl morph.
-      apply intEq_dist; [reflexivity |].
-      apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
-    Qed.
-
-  End Invariants.
-
   Section Timeless.
   
     Definition timelessP P w n :=
@@ -292,130 +268,6 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
   End Ownership.
 
-  Section WorldSatisfaction.
-
-    (* First, we need to compose the resources of a finite map. This won't be pretty, for
-       now, since the library does not provide enough
-       constructs. Hopefully we can provide a fold that'd work for
-       that at some point
-     *)
-    Fixpoint comp_list (xs : list pres) : res :=
-      match xs with
-        | nil => 1
-        | (x :: xs)%list => ra_proj x · comp_list xs
-      end.
-
-    Lemma comp_list_app rs1 rs2 :
-      comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
-    Proof.
-      induction rs1; simpl comp_list; [now rewrite ->ra_op_unit by apply _ |].
-      now rewrite ->IHrs1, assoc.
-    Qed.
-
-    Definition cod (m : nat -f> pres) : list pres := List.map snd (findom_t m).
-    Definition comp_map (m : nat -f> pres) : res := comp_list (cod m).
-
-    Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i == Some r) :
-      comp_map rs == ra_proj r · comp_map (fdRemove i rs).
-    Proof.
-      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
-      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
-      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; reflexivity | contradiction |].
-      simpl comp_list; rewrite ->IHrs by eauto using SS_tail.
-      rewrite-> !assoc, (comm (_ s)); reflexivity.
-    Qed.
-
-    Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i == None) :
-      ra_proj r · comp_map rs == comp_map (fdUpdate i r rs).
-    Proof.
-      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
-      induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
-      destruct (comp i j); [contradiction | reflexivity |].
-      simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
-      rewrite-> !assoc, (comm (_ r)); reflexivity.
-    Qed.
-
-    Lemma comp_map_insert_old (rs : nat -f> pres) i r1 r2 r
-          (HLu : rs i == Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
-      ra_proj r2 · comp_map rs == comp_map (fdUpdate i r rs).
-    Proof.
-      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
-      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
-      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; clear HLu | contradiction |].
-      - simpl comp_list; rewrite ->assoc, (comm (_ r2)), <- HEq; reflexivity.
-      - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
-        rewrite-> !assoc, (comm (_ r2)); reflexivity.
-    Qed.
-
-    Definition state_sat (r: res) σ: Prop := ↓r /\
-      match fst r with
-        | ex_own s => s = σ
-        | _ => True
-      end.
-
-    Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
-    Proof.
-      intros [ [s1| |] r1] [ [s2| |] r2] [EQs EQr] σ1 σ2 EQσ; unfold state_sat; simpl in *; try tauto; try rewrite !EQs; try rewrite !EQr; try rewrite !EQσ; reflexivity.
-    Qed.
-
-    Global Instance preo_unit : preoType () := disc_preo ().
-
-    Program Definition wsat σ m (r : res) w : UPred () :=
-      â–¹ (mkUPred (fun n _ => exists rs : nat -f> pres,
-                    state_sat (r · (comp_map rs)) σ
-                      /\ forall i (Hm : m i),
-                           (i ∈ dom rs <-> i ∈ dom w) /\
-                           forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
-                             ı π w n ri) _).
-    Next Obligation.
-      intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
-      setoid_rewrite HLe; eassumption.
-    Qed.
-
-    Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv) (wsat σ).
-    Proof.
-      intros m1 m2 EQm r r' EQr w1 w2 EQw [| n] []; [reflexivity |].
-      split; intros [rs [HE HM] ]; exists rs.
-      - split; [rewrite <-EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
-        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
-        rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
-      - split; [rewrite EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
-        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
-        rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
-    Qed.
-
-    Global Instance wsat_dist n σ m u : Proper (dist n ==> dist n) (wsat σ m u).
-    Proof.
-      intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
-      split; intros [rs [HE HM] ]; exists rs.
-      - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
-        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
-        assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
-        destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
-        apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
-        apply HR; [reflexivity | assumption].
-      - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
-        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
-        assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
-        destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
-        apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
-        apply HR; [reflexivity | assumption].
-    Qed.
-
-    Lemma wsat_valid σ m (r: res) w k :
-      wsat σ m r w (S k) tt -> ↓r.
-    Proof.
-      intros [rs [HD _] ]. destruct HD as [VAL _].
-      eapply ra_op_valid; [now apply _|]. eassumption.
-    Qed.
-
-  End WorldSatisfaction.
-
-  Notation " P @ k " := ((P : UPred ()) k tt) (at level 60, no associativity).
-
-
   Lemma valid_iff P :
     valid P <-> (⊤ ⊑ P).
   Proof.
@@ -424,30 +276,6 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     - intros w n r; apply Hp; exact I.
   Qed.
 
-  (*
-	Simple monotonicity tactics for props and wsat.
-
-	The tactic propsM H proves P w' n' r' given H : P w n r when
-		w ⊑ w', n' <= n, r ⊑ r'
-	are immediate.
-
-	The tactic wsatM is similar.
-  *)
-
-  Lemma propsM {P w n r w' n' r'}
-      (HP : P w n r) (HSw : w ⊑ w') (HLe : n' <= n) (HSr : r ⊑ r') :
-    P w' n' r'.
-  Proof. by apply: (mu_mono _ _ P _ _ HSw); exact: (uni_pred _ _ _ _ _ HLe HSr). Qed.
-
-  Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ].
-
-  Lemma wsatM {σ m} {r : res} {w n k}
-      (HW : wsat σ m r w @ n) (HLe : k <= n) :
-    wsat σ m r w @ k.
-  Proof. by exact: (uni_pred _ _ _ _ _ HLe). Qed.
-
-  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.
diff --git a/iris_derived_rules.v b/iris_derived_rules.v
new file mode 100644
index 0000000000000000000000000000000000000000..3d4b04cb8e1c18277f63989d811460bb2931940a
--- /dev/null
+++ b/iris_derived_rules.v
@@ -0,0 +1,37 @@
+Require Import ssreflect.
+Require Import world_prop core_lang lang masks iris_core iris_plog iris_vs_rules iris_ht_rules.
+Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
+
+Set Bullet Behavior "Strict Subproofs".
+
+Module Type IRIS_DERIVED_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) (VS_RULES: IRIS_VS_RULES RL C R WP CORE PLOG) (HT_RULES: IRIS_HT_RULES RL C R WP CORE PLOG).
+  Export VS_RULES.
+  Export HT_RULES.
+
+  Local Open Scope lang_scope.
+  Local Open Scope ra_scope.
+  Local Open Scope bi_scope.
+  Local Open Scope iris_scope.
+
+  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_DERIVED_RULES.
+
+Module IrisDerivedRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) (VS_RULES: IRIS_VS_RULES RL C R WP CORE PLOG) (HT_RULES: IRIS_HT_RULES RL C R WP CORE PLOG) : IRIS_DERIVED_RULES RL C R WP CORE PLOG VS_RULES HT_RULES.
+  Include IRIS_DERIVED_RULES RL C R WP CORE PLOG VS_RULES HT_RULES.
+End IrisDerivedRules.
diff --git a/iris_wp_rules.v b/iris_ht_rules.v
similarity index 95%
rename from iris_wp_rules.v
rename to iris_ht_rules.v
index fcb65a786592cb028c2a694e801b778ca9f80ec9..7d5f1e5f4b00a2571d8a8488c91d03986bac923a 100644
--- a/iris_wp_rules.v
+++ b/iris_ht_rules.v
@@ -1,12 +1,11 @@
 Require Import ssreflect.
-Require Import world_prop core_lang lang masks iris_core iris_vs iris_wp.
+Require Import world_prop core_lang lang masks iris_core iris_plog.
 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.
+Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE).
+  Export PLOG.
 
   Local Open Scope lang_scope.
   Local Open Scope ra_scope.
@@ -374,25 +373,8 @@ Module Type IRIS_WP_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
 
   End HoareTripleProperties.
 
-  Section DerivedRules.
+End IRIS_HT_RULES.
 
-    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.
+Module IrisHTRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) : IRIS_HT_RULES RL C R WP CORE PLOG.
+  Include IRIS_HT_RULES RL C R WP CORE PLOG.
+End IrisHTRules.
diff --git a/iris_meta.v b/iris_meta.v
index 6c2f6b323fae2c274e545bb365a2318fb50bd092..47d850365199ef3f353ce26a6a55b88bcef04347 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -1,12 +1,11 @@
 Require Import ssreflect.
-Require Import core_lang masks world_prop iris_core iris_vs iris_wp.
+Require Import core_lang masks world_prop iris_core iris_plog.
 Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Set Bullet Behavior "Strict Subproofs".
 
-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.
+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) (PLOG: IRIS_PLOG RL C R WP CORE).
+  Export PLOG.
 
   Local Open Scope lang_scope.
   Local Open Scope ra_scope.
@@ -390,6 +389,6 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
 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.
+Module IrisMeta (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE) : IRIS_META RL C R WP CORE PLOG.
+  Include IRIS_META RL C R WP CORE PLOG.
 End IrisMeta.
diff --git a/iris_plog.v b/iris_plog.v
new file mode 100644
index 0000000000000000000000000000000000000000..b6f23949b53f6ccd31486d5c93842a9f6958726c
--- /dev/null
+++ b/iris_plog.v
@@ -0,0 +1,458 @@
+Require Import ssreflect.
+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".
+
+(* This enriches the Iris core logic with program logic features:
+   Invariants, View Shifts, and Hoare Triples. The last two make use
+   of a notion of "world satisfaction" (which you can also think of
+   as the erasure from logical states to physical ones). *)
+Module Type IRIS_PLOG (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.
+
+  Local Open Scope lang_scope.
+  Local Open Scope ra_scope.
+  Local Open Scope bi_scope.
+  Local Open Scope iris_scope.
+  
+  Implicit Types (P : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (u v : res) (σ : state) (φ : vPred).
+
+
+
+  Section Invariants.
+
+    (** Invariants **)
+    Definition invP i P w : UPred pres :=
+      intEqP (w i) (Some (ı' P)).
+    Program Definition inv i : Props -n> Props :=
+      n[(fun P => m[(invP i P)])].
+    Next Obligation.
+      intros w1 w2 EQw; unfold invP; simpl morph.
+      destruct n; [apply dist_bound |].
+      apply intEq_dist; [apply EQw | reflexivity].
+    Qed.
+    Next Obligation.
+      intros w1 w2 Sw; unfold invP; simpl morph.
+      intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
+      destruct (w1 i) as [μ1 |]; [| contradiction].
+      destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
+      rewrite <- Sw; assumption.
+    Qed.
+    Next Obligation.
+      intros p1 p2 EQp w; unfold invP; simpl morph.
+      apply intEq_dist; [reflexivity |].
+      apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
+    Qed.
+
+  End Invariants.
+
+  Section WorldSatisfaction.
+
+    (* First, we need to compose the resources of a finite map. This won't be pretty, for
+       now, since the library does not provide enough
+       constructs. Hopefully we can provide a fold that'd work for
+       that at some point
+     *)
+    Fixpoint comp_list (xs : list pres) : res :=
+      match xs with
+        | nil => 1
+        | (x :: xs)%list => ra_proj x · comp_list xs
+      end.
+
+    Lemma comp_list_app rs1 rs2 :
+      comp_list (rs1 ++ rs2) == comp_list rs1 · comp_list rs2.
+    Proof.
+      induction rs1; simpl comp_list; [now rewrite ->ra_op_unit by apply _ |].
+      now rewrite ->IHrs1, assoc.
+    Qed.
+
+    Definition cod (m : nat -f> pres) : list pres := List.map snd (findom_t m).
+    Definition comp_map (m : nat -f> pres) : res := comp_list (cod m).
+
+    Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i == Some r) :
+      comp_map rs == ra_proj r · comp_map (fdRemove i rs).
+    Proof.
+      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
+      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
+      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; reflexivity | contradiction |].
+      simpl comp_list; rewrite ->IHrs by eauto using SS_tail.
+      rewrite-> !assoc, (comm (_ s)); reflexivity.
+    Qed.
+
+    Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i == None) :
+      ra_proj r · comp_map rs == comp_map (fdUpdate i r rs).
+    Proof.
+      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
+      induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
+      destruct (comp i j); [contradiction | reflexivity |].
+      simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
+      rewrite-> !assoc, (comm (_ r)); reflexivity.
+    Qed.
+
+    Lemma comp_map_insert_old (rs : nat -f> pres) i r1 r2 r
+          (HLu : rs i == Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
+      ra_proj r2 · comp_map rs == comp_map (fdUpdate i r rs).
+    Proof.
+      destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
+      induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
+      destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; clear HLu | contradiction |].
+      - simpl comp_list; rewrite ->assoc, (comm (_ r2)), <- HEq; reflexivity.
+      - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
+        rewrite-> !assoc, (comm (_ r2)); reflexivity.
+    Qed.
+
+    Definition state_sat (r: res) σ: Prop := ↓r /\
+      match fst r with
+        | ex_own s => s = σ
+        | _ => True
+      end.
+
+    Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
+    Proof.
+      intros [ [s1| |] r1] [ [s2| |] r2] [EQs EQr] σ1 σ2 EQσ; unfold state_sat; simpl in *; try tauto; try rewrite !EQs; try rewrite !EQr; try rewrite !EQσ; reflexivity.
+    Qed.
+
+    Global Instance preo_unit : preoType () := disc_preo ().
+
+    Program Definition wsat σ m (r : res) w : UPred () :=
+      â–¹ (mkUPred (fun n _ => exists rs : nat -f> pres,
+                    state_sat (r · (comp_map rs)) σ
+                      /\ forall i (Hm : m i),
+                           (i ∈ dom rs <-> i ∈ dom w) /\
+                           forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
+                             ı π w n ri) _).
+    Next Obligation.
+      intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
+      setoid_rewrite HLe; eassumption.
+    Qed.
+
+    Global Instance wsat_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv) (wsat σ).
+    Proof.
+      intros m1 m2 EQm r r' EQr w1 w2 EQw [| n] []; [reflexivity |].
+      split; intros [rs [HE HM] ]; exists rs.
+      - split; [rewrite <-EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
+        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
+        rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
+      - split; [rewrite EQr; assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
+        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
+        rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
+    Qed.
+
+    Global Instance wsat_dist n σ m u : Proper (dist n ==> dist n) (wsat σ m u).
+    Proof.
+      intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
+      split; intros [rs [HE HM] ]; exists rs.
+      - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
+        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
+        assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
+        destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
+        apply ı in EQπ; apply EQπ; [now auto with arith |].
+        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
+        apply HR; [reflexivity | assumption].
+      - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
+        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
+        assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
+        destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
+        apply ı in EQπ; apply EQπ; [now auto with arith |].
+        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [omega |].
+        apply HR; [reflexivity | assumption].
+    Qed.
+
+    Lemma wsat_valid σ m (r: res) w k :
+      wsat σ m r w (S k) tt -> ↓r.
+    Proof.
+      intros [rs [HD _] ]. destruct HD as [VAL _].
+      eapply ra_op_valid; [now apply _|]. eassumption.
+    Qed.
+
+  End WorldSatisfaction.
+
+  Notation " P @ k " := ((P : UPred ()) k tt) (at level 60, no associativity).
+
+  (*
+	Simple monotonicity tactics for props and wsat.
+
+	The tactic propsM H proves P w' n' r' given H : P w n r when
+		w ⊑ w', n' <= n, r ⊑ r'
+	are immediate.
+
+	The tactic wsatM is similar.
+   *)
+
+  Lemma propsM {P w n r w' n' r'}
+      (HP : P w n r) (HSw : w ⊑ w') (HLe : n' <= n) (HSr : r ⊑ r') :
+    P w' n' r'.
+  Proof. by apply: (mu_mono _ _ P _ _ HSw); exact: (uni_pred _ _ _ _ _ HLe HSr). Qed.
+
+  Ltac propsM H := solve [ done | apply (propsM H); solve [ done | reflexivity | omega ] ].
+
+  Lemma wsatM {σ m} {r : res} {w n k}
+      (HW : wsat σ m r w @ n) (HLe : k <= n) :
+    wsat σ m r w @ k.
+  Proof. by exact: (uni_pred _ _ _ _ _ HLe). Qed.
+
+  Ltac wsatM H := solve [done | apply (wsatM H); solve [done | omega] ].
+
+  Section ViewShifts.
+    Local Obligation Tactic := intros.
+
+    Program Definition preVS m1 m2 P w : UPred pres :=
+      mkUPred (fun n r => forall w1 (rf: res) mf σ k (HSub : w ⊑ w1) (HLe : k < n)
+                                 (HD : mf # m1 ∪ m2)
+                                 (HE : wsat σ (m1 ∪ mf) (ra_proj r · rf) w1 @ S k),
+                          exists w2 r',
+                            w1 ⊑ w2 /\ P w2 (S k) r'
+                            /\ wsat σ (m2 ∪ mf) (r' · rf) w2 @ S k) _.
+    Next Obligation.
+      intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
+      destruct (HP w1 (rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
+        try assumption; [now eauto with arith | |].
+      - eapply wsat_equiv, HE; try reflexivity.
+        rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
+      - rewrite ->assoc, (comm (_ r1')) in HE'.
+        exists w2. exists↓ (rd · ra_proj r1').
+        { apply wsat_valid in HE'. auto_valid. }
+        split; [assumption | split; [| assumption] ].
+        eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
+    Qed.
+
+    Program Definition pvs m1 m2 : Props -n> Props :=
+      n[(fun P => m[(preVS m1 m2 P)])].
+    Next Obligation.
+      intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
+      - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
+        assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
+        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
+        + eapply wsat_dist, HE; [symmetry; eassumption | omega].
+        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
+          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
+          exists (extend w1'' w2') r'; split; [assumption | split].
+          * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
+          * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
+      - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
+        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
+        + eapply wsat_dist, HE; [symmetry; eassumption | omega].
+        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
+          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
+          exists (extend w1'' w2') r'; split; [assumption | split].
+          * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
+          * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
+    Qed.
+    Next Obligation.
+      intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
+      etransitivity; eassumption.
+    Qed.
+    Next Obligation.
+      intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
+      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
+        clear HP; repeat (eexists; try eassumption); [].
+        apply EQp; [now eauto with arith | assumption].
+      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
+        clear HP; repeat (eexists; try eassumption); [].
+        apply EQp; [now eauto with arith | assumption].
+    Qed.
+
+    Definition vs m1 m2 P Q : Props :=
+      □(P → pvs m1 m2 Q).
+
+  End ViewShifts.
+
+
+  Section HoareTriples.
+  (* Quadruples, really *)
+
+    Instance LP_isval : LimitPreserving is_value.
+    Proof.
+      intros σ σc HC; apply HC.
+    Qed.
+
+    Local Obligation Tactic := intros; eauto with typeclass_instances.
+
+    Definition safeExpr e σ :=
+      is_value e \/
+         (exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
+         (exists e' K, e = K [[ fork e' ]]).
+
+    Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n r :=
+      forall w' k rf mf σ (HSw : w ⊑ w') (HLt : k < n) (HD : mf # m)
+             (HE : wsat σ (m ∪ mf) (ra_proj r · rf) w' @ S k),
+        (forall (HV : is_value e),
+         exists w'' r', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
+                           /\ wsat σ (m ∪ mf) (ra_proj r' · rf) w'' @ S k) /\
+        (forall σ' ei ei' K (HDec : e = K [[ ei ]])
+                (HStep : prim_step (ei, σ) (ei', σ')),
+         exists w'' r', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
+                           /\ wsat σ' (m ∪ mf) (ra_proj r' · rf) w'' @ k) /\
+        (forall e' K (HDec : e = K [[ fork e' ]]),
+         exists w'' rfk rret, w' ⊑ w''
+                                 /\ WP (K [[ fork_ret ]]) φ w'' k rret
+                                 /\ WP e' (umconst ⊤) w'' k rfk
+                                 /\ wsat σ (m ∪ mf) (ra_proj rfk · ra_proj rret · rf) w'' @ 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 => mkUPred (wpFP safe m WP e φ w) _)])])].
+    Next Obligation.
+      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k rf mf σ HSw HLt HD HE.
+      rewrite <- EQr, (comm rd), <- assoc in HE.
+      specialize (Hp w' k (rd · rf) mf σ); destruct Hp as [HV [HS [HF HS' ] ] ];
+      [| omega | ..]; try assumption; [].      
+      split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
+      - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
+        rewrite ->assoc, (comm (_ r1')) in HE'.
+        exists w''. exists↓ (rd · ra_proj r1').
+        { clear -HE'. apply wsat_valid in HE'. auto_valid. }
+        split; [assumption | split; [| assumption] ].
+        eapply uni_pred, Hφ; [| exists rd]; reflexivity.
+      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
+        rewrite ->assoc, (comm (_ r1')) in HE'. exists w''.
+        destruct k as [| k]; [exists r1'; simpl wsat; tauto |].
+        exists↓ (rd · ra_proj r1').
+        { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+        split; [assumption | split; [| assumption] ].
+        eapply uni_pred, HWP; [| exists rd]; reflexivity.
+      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
+        destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
+        rewrite ->assoc, <- (assoc (_ rfk)) in HE'.
+        exists w''. exists rfk. exists↓ (rd · ra_proj rret1).
+        { clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _.
+          rewrite ->(comm (_ rfk)) in HE'. eassumption. }
+        repeat (split; try assumption).
+        + eapply uni_pred, HWR; [| exists rd]; reflexivity.
+        + clear -HE'. unfold ra_proj. rewrite ->(comm _ rd) in HE'. exact HE'.
+      - auto.
+    Qed.
+    Next Obligation.
+      intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
+      - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
+        edestruct (Hp (extend w2' w1)) as [HV [HS [HF HS'] ] ]; try eassumption;
+        [eapply wsat_dist, HE; [eassumption | omega] |].
+        split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
+        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
+          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+          exists (extend w1'' w2') r'; split; [assumption |].
+          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
+        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
+          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+          exists (extend w1'' w2') r'; split; [assumption |].
+          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
+        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
+          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+          exists (extend w1'' w2') rfk rret; split; [assumption |].
+          split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
+          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
+        + auto.
+      - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
+        edestruct (Hp (extend w2' w2)) as [HV [HS [HF HS'] ] ]; try eassumption;
+        [eapply wsat_dist, HE; [eassumption | omega] |].
+        split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF] ] ]; intros.
+        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
+          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+          exists (extend w1'' w2') r'; split; [assumption |].
+          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
+        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
+          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+          exists (extend w1'' w2') r'; split; [assumption |].
+          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
+          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
+        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
+          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
+          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
+          exists (extend w1'' w2') rfk rret; split; [assumption |].
+          split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
+          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
+        + auto.
+    Qed.
+    Next Obligation.
+      intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
+      etransitivity; eassumption.
+    Qed.
+    Next Obligation.
+      intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
+      split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
+      - split; [| split; [| split] ]; intros.
+        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
+          apply EQφ, Hφ; omega.
+        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
+          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | omega].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret ; repeat (split; try assumption); [].
+          eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | omega].
+        + auto.
+      - split; [| split; [| split] ]; intros.
+        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
+          apply EQφ, Hφ; omega.
+        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
+          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | omega].
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; repeat (split; try assumption); [].
+          eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | omega].
+        + auto.
+    Qed.
+    Next Obligation.
+      intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
+      simpl in EQe; subst e2; reflexivity.
+    Qed.
+
+    Instance contr_wpF safe m : contractive (wpF safe m).
+    Proof.
+      intros n WP1 WP2 EQWP e φ w k r 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'' [r' [HSw' [HWP HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
+          eapply EQWP, HWP; omega.
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; split; [assumption |].
+          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
+        + auto.
+      - split; [assumption | split; [| split]; intros].
+        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
+          exists w'' r'; split; [assumption | split; [| assumption] ].
+          eapply EQWP, HWP; omega.
+        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
+          exists w'' rfk rret; split; [assumption |].
+          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
+        + auto.
+    Qed.
+
+    Definition wp safe m : expr -n> vPred -n> Props :=
+      fixp (wpF safe m) (umconst (umconst ⊤)).
+
+    Lemma unfold_wp safe m :
+      wp safe m == (wpF safe m) (wp safe m).
+    Proof.
+      unfold wp; apply fixp_eq.
+    Qed.
+
+    Opaque wp.
+
+    Lemma wpO {safe m e φ w r} : wp safe m e φ w O r.
+    Proof.
+      rewrite unfold_wp; intros w'; intros; now inversion HLt.
+    Qed.
+
+    Definition ht safe m P e Q := □(P → wp safe m e Q).
+
+  End HoareTriples.
+
+End IRIS_PLOG.
+
+Module IrisPlog (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_PLOG RL C R WP CORE.
+  Include IRIS_PLOG RL C R WP CORE.
+End IrisPlog.
diff --git a/iris_vs.v b/iris_vs_rules.v
similarity index 77%
rename from iris_vs.v
rename to iris_vs_rules.v
index c9edec2f038f9eef43ab0b99cc8e56d3042a6077..5b905802b583ae68295efbeed8b366afe33df548 100644
--- a/iris_vs.v
+++ b/iris_vs_rules.v
@@ -1,11 +1,11 @@
 Require Import ssreflect.
-Require Import world_prop core_lang masks iris_core.
+Require Import world_prop core_lang masks iris_core iris_plog.
 Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
 Set Bullet Behavior "Strict Subproofs".
 
-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.
+Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE).
+  Export PLOG.
 
   Local Open Scope ra_scope.
   Local Open Scope bi_scope.
@@ -13,70 +13,6 @@ Module Type IRIS_VS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PR
 
   Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (σ : state).
 
-  Section ViewShifts.
-    Local Obligation Tactic := intros.
-
-    Program Definition preVS m1 m2 P w : UPred pres :=
-      mkUPred (fun n r => forall w1 (rf: res) mf σ k (HSub : w ⊑ w1) (HLe : k < n)
-                                 (HD : mf # m1 ∪ m2)
-                                 (HE : wsat σ (m1 ∪ mf) (ra_proj r · rf) w1 @ S k),
-                          exists w2 r',
-                            w1 ⊑ w2 /\ P w2 (S k) r'
-                            /\ wsat σ (m2 ∪ mf) (r' · rf) w2 @ S k) _.
-    Next Obligation.
-      intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
-      destruct (HP w1 (rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
-        try assumption; [now eauto with arith | |].
-      - eapply wsat_equiv, HE; try reflexivity.
-        rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
-      - rewrite ->assoc, (comm (_ r1')) in HE'.
-        exists w2. exists↓ (rd · ra_proj r1').
-        { apply wsat_valid in HE'. auto_valid. }
-        split; [assumption | split; [| assumption] ].
-        eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
-    Qed.
-
-    Program Definition pvs m1 m2 : Props -n> Props :=
-      n[(fun P => m[(preVS m1 m2 P)])].
-    Next Obligation.
-      intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
-      - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
-        assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
-        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
-        + eapply wsat_dist, HE; [symmetry; eassumption | omega].
-        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
-          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
-          exists (extend w1'' w2') r'; split; [assumption | split].
-          * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
-          * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
-      - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
-        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
-        + eapply wsat_dist, HE; [symmetry; eassumption | omega].
-        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
-          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
-          exists (extend w1'' w2') r'; split; [assumption | split].
-          * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
-          * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
-    Qed.
-    Next Obligation.
-      intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
-      etransitivity; eassumption.
-    Qed.
-    Next Obligation.
-      intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
-      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
-        clear HP; repeat (eexists; try eassumption); [].
-        apply EQp; [now eauto with arith | assumption].
-      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
-        clear HP; repeat (eexists; try eassumption); [].
-        apply EQp; [now eauto with arith | assumption].
-    Qed.
-
-    Definition vs m1 m2 P Q : Props :=
-      □(P → pvs m1 m2 Q).
-
-  End ViewShifts.
-
   Section ViewShiftProps.
 
     Lemma vsTimeless m P :
@@ -330,8 +266,8 @@ Module Type IRIS_VS (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PR
 
   End ViewShiftProps.
 
-End IRIS_VS.
+End IRIS_VS_RULES.
 
-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.
+Module IrisVSRules (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) (PLOG: IRIS_PLOG RL C R WP CORE): IRIS_VS_RULES RL C R WP CORE PLOG.
+  Include IRIS_VS_RULES RL C R WP CORE PLOG.
+End IrisVSRules.
diff --git a/iris_wp.v b/iris_wp.v
deleted file mode 100644
index 7dd2fd703493d3504ddf35021dd64ad0ad2b06fb..0000000000000000000000000000000000000000
--- a/iris_wp.v
+++ /dev/null
@@ -1,213 +0,0 @@
-Require Import ssreflect.
-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 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.
-
-  Local Open Scope lang_scope.
-  Local Open Scope ra_scope.
-  Local Open Scope bi_scope.
-  Local Open Scope iris_scope.
-
-  Section HoareTriples.
-  (* Quadruples, really *)
-
-    Instance LP_isval : LimitPreserving is_value.
-    Proof.
-      intros σ σc HC; apply HC.
-    Qed.
-
-    Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : vPred) (r : pres).
-
-    Local Obligation Tactic := intros; eauto with typeclass_instances.
-
-    Definition safeExpr e σ :=
-      is_value e \/
-         (exists σ' ei ei' K, e = K [[ ei ]] /\ prim_step (ei, σ) (ei', σ')) \/
-         (exists e' K, e = K [[ fork e' ]]).
-
-    Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n r :=
-      forall w' k rf mf σ (HSw : w ⊑ w') (HLt : k < n) (HD : mf # m)
-             (HE : wsat σ (m ∪ mf) (ra_proj r · rf) w' @ S k),
-        (forall (HV : is_value e),
-         exists w'' r', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
-                           /\ wsat σ (m ∪ mf) (ra_proj r' · rf) w'' @ S k) /\
-        (forall σ' ei ei' K (HDec : e = K [[ ei ]])
-                (HStep : prim_step (ei, σ) (ei', σ')),
-         exists w'' r', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
-                           /\ wsat σ' (m ∪ mf) (ra_proj r' · rf) w'' @ k) /\
-        (forall e' K (HDec : e = K [[ fork e' ]]),
-         exists w'' rfk rret, w' ⊑ w''
-                                 /\ WP (K [[ fork_ret ]]) φ w'' k rret
-                                 /\ WP e' (umconst ⊤) w'' k rfk
-                                 /\ wsat σ (m ∪ mf) (ra_proj rfk · ra_proj rret · rf) w'' @ 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 => mkUPred (wpFP safe m WP e φ w) _)])])].
-    Next Obligation.
-      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k rf mf σ HSw HLt HD HE.
-      rewrite <- EQr, (comm rd), <- assoc in HE.
-      specialize (Hp w' k (rd · rf) mf σ); destruct Hp as [HV [HS [HF HS' ] ] ];
-      [| omega | ..]; try assumption; [].      
-      split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
-      - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
-        rewrite ->assoc, (comm (_ r1')) in HE'.
-        exists w''. exists↓ (rd · ra_proj r1').
-        { clear -HE'. apply wsat_valid in HE'. auto_valid. }
-        split; [assumption | split; [| assumption] ].
-        eapply uni_pred, Hφ; [| exists rd]; reflexivity.
-      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
-        rewrite ->assoc, (comm (_ r1')) in HE'. exists w''.
-        destruct k as [| k]; [exists r1'; simpl wsat; tauto |].
-        exists↓ (rd · ra_proj r1').
-        { clear- HE'. apply wsat_valid in HE'. auto_valid. }
-        split; [assumption | split; [| assumption] ].
-        eapply uni_pred, HWP; [| exists rd]; reflexivity.
-      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
-        destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
-        rewrite ->assoc, <- (assoc (_ rfk)) in HE'.
-        exists w''. exists rfk. exists↓ (rd · ra_proj rret1).
-        { clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _.
-          rewrite ->(comm (_ rfk)) in HE'. eassumption. }
-        repeat (split; try assumption).
-        + eapply uni_pred, HWR; [| exists rd]; reflexivity.
-        + clear -HE'. unfold ra_proj. rewrite ->(comm _ rd) in HE'. exact HE'.
-      - auto.
-    Qed.
-    Next Obligation.
-      intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
-      - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
-        edestruct (Hp (extend w2' w1)) as [HV [HS [HF HS'] ] ]; try eassumption;
-        [eapply wsat_dist, HE; [eassumption | omega] |].
-        split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
-        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
-          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
-          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r'; split; [assumption |].
-          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
-          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
-        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
-          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
-          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r'; split; [assumption |].
-          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
-          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
-        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
-          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
-          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') rfk rret; split; [assumption |].
-          split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
-          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
-        + auto.
-      - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
-        edestruct (Hp (extend w2' w2)) as [HV [HS [HF HS'] ] ]; try eassumption;
-        [eapply wsat_dist, HE; [eassumption | omega] |].
-        split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF] ] ]; intros.
-        + specialize (HV HV0); destruct HV as [w1'' [r' [HSw'' [Hφ HE'] ] ] ].
-          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
-          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r'; split; [assumption |].
-          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
-          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | omega].
-        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [HSw'' [HWP HE'] ] ] ].
-          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
-          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') r'; split; [assumption |].
-          split; [| eapply wsat_dist, HE'; [eassumption | omega] ].
-          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | omega].
-        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [HSw'' [HWR [HWF HE'] ] ] ] ] ].
-          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
-          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
-          exists (extend w1'' w2') rfk rret; split; [assumption |].
-          split; [| split; [| eapply wsat_dist, HE'; [eassumption | omega] ] ];
-          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; omega.
-        + auto.
-    Qed.
-    Next Obligation.
-      intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
-      etransitivity; eassumption.
-    Qed.
-    Next Obligation.
-      intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
-      split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
-      - split; [| split; [| split] ]; intros.
-        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
-          exists w'' r'; split; [assumption | split; [| assumption] ].
-          apply EQφ, Hφ; omega.
-        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
-          exists w'' r'; split; [assumption | split; [| assumption] ].
-          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | omega].
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
-          exists w'' rfk rret ; repeat (split; try assumption); [].
-          eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | omega].
-        + auto.
-      - split; [| split; [| split] ]; intros.
-        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [HSw' [Hφ HE'] ] ] ].
-          exists w'' r'; split; [assumption | split; [| assumption] ].
-          apply EQφ, Hφ; omega.
-        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [Hφ HE'] ] ] ].
-          exists w'' r'; split; [assumption | split; [| assumption] ].
-          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | omega].
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
-          exists w'' rfk rret; repeat (split; try assumption); [].
-          eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | omega].
-        + auto.
-    Qed.
-    Next Obligation.
-      intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
-      simpl in EQe; subst e2; reflexivity.
-    Qed.
-
-    Instance contr_wpF safe m : contractive (wpF safe m).
-    Proof.
-      intros n WP1 WP2 EQWP e φ w k r 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'' [r' [HSw' [HWP HE'] ] ] ].
-          exists w'' r'; split; [assumption | split; [| assumption] ].
-          eapply EQWP, HWP; omega.
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
-          exists w'' rfk rret; split; [assumption |].
-          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
-        + auto.
-      - split; [assumption | split; [| split]; intros].
-        + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [HSw' [HWP HE'] ] ] ].
-          exists w'' r'; split; [assumption | split; [| assumption] ].
-          eapply EQWP, HWP; omega.
-        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWR [HWF HE'] ] ] ] ] ].
-          exists w'' rfk rret; split; [assumption |].
-          split; [| split; [| assumption] ]; eapply EQWP; try eassumption; omega.
-        + auto.
-    Qed.
-
-    Definition wp safe m : expr -n> vPred -n> Props :=
-      fixp (wpF safe m) (umconst (umconst ⊤)).
-
-    Lemma unfold_wp safe m :
-      wp safe m == (wpF safe m) (wp safe m).
-    Proof.
-      unfold wp; apply fixp_eq.
-    Qed.
-
-    Opaque wp.
-
-    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.
-
-    Definition ht safe m P e Q := □(P → wp safe m e Q).
-
-  End HoareTriples.
-
-End IRIS_HT.
-
-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.