diff --git a/_CoqProject b/_CoqProject
index 86318883076ffecaeec7094bef60e110f8a45d1d..4ff403e8eae165ed93d0a2804291897fe7137230 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -70,26 +70,25 @@ base_logic/double_negation.v
 base_logic/lib/iprop.v
 base_logic/lib/own.v
 base_logic/lib/saved_prop.v
+base_logic/lib/namespaces.v
+base_logic/lib/wsat.v
+base_logic/lib/invariants.v
+base_logic/lib/fancy_updates.v
+base_logic/lib/viewshifts.v
+base_logic/lib/auth.v
+base_logic/lib/sts.v
+base_logic/lib/boxes.v
+base_logic/lib/thread_local.v
+base_logic/lib/cancelable_invariants.v
+base_logic/lib/counter_examples.v
 program_logic/adequacy.v
 program_logic/lifting.v
-program_logic/invariants.v
-program_logic/wsat.v
 program_logic/weakestpre.v
-program_logic/fancy_updates.v
 program_logic/hoare.v
-program_logic/viewshifts.v
 program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
 program_logic/ectx_lifting.v
-program_logic/auth.v
-program_logic/sts.v
-program_logic/namespaces.v
-program_logic/boxes.v
-program_logic/counter_examples.v
-program_logic/iris.v
-program_logic/thread_local.v
-program_logic/cancelable_invariants.v
 heap_lang/lang.v
 heap_lang/tactics.v
 heap_lang/wp_tactics.v
diff --git a/program_logic/auth.v b/base_logic/lib/auth.v
similarity index 96%
rename from program_logic/auth.v
rename to base_logic/lib/auth.v
index 7c2d805297984fe443433be68e8639b3f4546351..fd0ab02fabbd9b4e2ce1f34b90aa466292f5be39 100644
--- a/program_logic/auth.v
+++ b/base_logic/lib/auth.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export auth.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
@@ -16,7 +16,7 @@ Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A
 Proof. intros ?%subG_inG ?. by split. Qed.
 
 Section definitions.
-  Context `{irisG Λ Σ, authG Σ A} {T : Type} (γ : gname).
+  Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
 
   Definition auth_own (a : A) : iProp Σ :=
     own γ (◯ a).
@@ -57,10 +57,10 @@ End definitions.
 Typeclasses Opaque auth_own auth_inv auth_ctx.
 Instance: Params (@auth_own) 4.
 Instance: Params (@auth_inv) 5.
-Instance: Params (@auth_ctx) 8.
+Instance: Params (@auth_ctx) 7.
 
 Section auth.
-  Context `{irisG Λ Σ, authG Σ A}.
+  Context `{invG Σ, authG Σ A}.
   Context {T : Type} `{!Inhabited T}.
   Context (f : T → A) (φ : T → iProp Σ).
   Implicit Types N : namespace.
@@ -146,4 +146,4 @@ Section auth.
   Qed.
 End auth.
 
-Arguments auth_open {_ _ _ _} [_] {_} [_] _ _ _ _ _ _ _.
+Arguments auth_open {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.
diff --git a/program_logic/boxes.v b/base_logic/lib/boxes.v
similarity index 96%
rename from program_logic/boxes.v
rename to base_logic/lib/boxes.v
index 03db8da2a658997873cdabedc3d0d495db509d17..a55d1c8a994617f53fa854a6ca8bf5f2210e64f2 100644
--- a/program_logic/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Import auth gmap agree.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
@@ -11,7 +11,7 @@ Class boxG Σ :=
     (optionR (agreeR (laterC (iPreProp Σ))))).
 
 Section box_defs.
-  Context `{irisG Λ Σ, boxG Σ} (N : namespace).
+  Context `{invG Σ, boxG Σ} (N : namespace).
 
   Definition slice_name := gname.
 
@@ -34,14 +34,13 @@ Section box_defs.
                          inv N (slice_inv γ (Φ γ)))%I.
 End box_defs.
 
-Instance: Params (@box_own_auth) 5.
-Instance: Params (@box_own_prop) 5.
-Instance: Params (@slice_inv) 5.
-Instance: Params (@slice) 6.
-Instance: Params (@box) 6.
+Instance: Params (@box_own_prop) 3.
+Instance: Params (@slice_inv) 3.
+Instance: Params (@slice) 5.
+Instance: Params (@box) 5.
 
 Section box.
-Context `{irisG Λ Σ, boxG Σ} (N : namespace).
+Context `{invG Σ, boxG Σ} (N : namespace).
 Implicit Types P Q : iProp Σ.
 
 Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
diff --git a/program_logic/cancelable_invariants.v b/base_logic/lib/cancelable_invariants.v
similarity index 94%
rename from program_logic/cancelable_invariants.v
rename to base_logic/lib/cancelable_invariants.v
index 5f7b0796304abf8b7972e830df16b937abdcd731..1cbdefa77769f0dc45d9edd2da1025993578f343 100644
--- a/program_logic/cancelable_invariants.v
+++ b/base_logic/lib/cancelable_invariants.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export frac.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -6,7 +6,7 @@ Import uPred.
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
 
 Section defs.
-  Context `{irisG Λ Σ, cinvG Σ}.
+  Context `{invG Σ, cinvG Σ}.
 
   Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
 
@@ -14,11 +14,11 @@ Section defs.
     inv N (P ∨ cinv_own γ 1%Qp)%I.
 End defs.
 
-Instance: Params (@cinv) 6.
+Instance: Params (@cinv) 5.
 Typeclasses Opaque cinv_own cinv.
 
 Section proofs.
-  Context `{irisG Λ Σ, cinvG Σ}.
+  Context `{invG Σ, cinvG Σ}.
 
   Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.
diff --git a/program_logic/counter_examples.v b/base_logic/lib/counter_examples.v
similarity index 100%
rename from program_logic/counter_examples.v
rename to base_logic/lib/counter_examples.v
diff --git a/program_logic/fancy_updates.v b/base_logic/lib/fancy_updates.v
similarity index 95%
rename from program_logic/fancy_updates.v
rename to base_logic/lib/fancy_updates.v
index f5ed4c41a2ce8d6a76cec1df20dee65859c1f937..18af313b1fd31ff52ee0411cfbce2406857cf3d4 100644
--- a/program_logic/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -1,18 +1,20 @@
-From iris.program_logic Require Export iris.
-From iris.program_logic Require Import wsat.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Export coPset.
+From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
+Export invG.
 Import uPred.
 
-Program Definition fupd_def `{irisG Λ Σ}
+Program Definition fupd_def `{invG Σ}
     (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ★ ownE E1 ==★ ◇ (wsat ★ ownE E2 ★ P))%I.
 Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed.
 Definition fupd := proj1_sig fupd_aux.
 Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux.
-Arguments fupd {_ _ _} _ _ _%I.
-Instance: Params (@fupd) 5.
+Arguments fupd {_ _} _ _ _%I.
+Instance: Params (@fupd) 4.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
   (at level 99, E1, E2 at level 50, Q at level 200,
@@ -46,12 +48,12 @@ Notation "P ={ E }▷=★ Q" := (P ={E,E}▷=★ Q)%I
    format "P  ={ E }▷=★  Q") : uPred_scope.
 
 Section fupd.
-Context `{irisG Λ Σ}.
+Context `{invG Σ}.
 Implicit Types P Q : iProp Σ.
 
-Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Λ Σ _ E1 E2).
+Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Σ _ E1 E2).
 Proof. rewrite fupd_eq. solve_proper. Qed.
-Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Λ Σ _ E1 E2).
+Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Σ _ E1 E2).
 Proof. apply ne_proper, _. Qed.
 
 Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
@@ -92,10 +94,10 @@ Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q.
 Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
 
 (** * Derived rules *)
-Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Λ Σ _ E1 E2).
+Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
 Global Instance fupd_flip_mono' E1 E2 :
-  Proper (flip (⊢) ==> flip (⊢)) (@fupd Λ Σ _ E1 E2).
+  Proper (flip (⊢) ==> flip (⊢)) (@fupd Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
 
 Lemma fupd_intro E P : P ={E}=★ P.
@@ -148,7 +150,7 @@ End fupd.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{irisG Λ Σ}.
+  Context `{invG Σ}.
   Implicit Types P Q : iProp Σ.
 
   Global Instance from_pure_fupd E P φ : FromPure P φ → FromPure (|={E}=> P) φ.
diff --git a/program_logic/invariants.v b/base_logic/lib/invariants.v
similarity index 90%
rename from program_logic/invariants.v
rename to base_logic/lib/invariants.v
index 5398da27639cc217abca5a13c45c1fd838efc87a..727a8b65998af0bf05be9c6c2cafd9fff12c8091 100644
--- a/program_logic/invariants.v
+++ b/base_logic/lib/invariants.v
@@ -1,25 +1,23 @@
-From iris.program_logic Require Export fancy_updates.
-From iris.program_logic Require Export namespaces.
-From iris.program_logic Require Import wsat.
+From iris.base_logic.lib Require Export fancy_updates namespaces.
+From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
-Definition inv_def `{irisG Λ Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   (∃ i, ■ (i ∈ nclose N) ∧ ownI i P)%I.
 Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
-Definition inv {Λ Σ i} := proj1_sig inv_aux Λ Σ i.
+Definition inv {Σ i} := proj1_sig inv_aux Σ i.
 Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
-Instance: Params (@inv) 4.
+Instance: Params (@inv) 3.
 Typeclasses Opaque inv.
 
 Section inv.
-Context `{irisG Λ Σ}.
+Context `{invG Σ}.
 Implicit Types i : positive.
 Implicit Types N : namespace.
 Implicit Types P Q R : iProp Σ.
-Implicit Types Φ : val Λ → iProp Σ.
 
 Global Instance inv_contractive N : Contractive (inv N).
 Proof.
diff --git a/program_logic/namespaces.v b/base_logic/lib/namespaces.v
similarity index 100%
rename from program_logic/namespaces.v
rename to base_logic/lib/namespaces.v
diff --git a/program_logic/sts.v b/base_logic/lib/sts.v
similarity index 95%
rename from program_logic/sts.v
rename to base_logic/lib/sts.v
index 862d3a5c0836878df5d73d8e53cbcc21d04063bf..47c79df7eb134b2d998a44925fee933bc3f57ea0 100644
--- a/program_logic/sts.v
+++ b/base_logic/lib/sts.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export sts.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -15,7 +15,7 @@ Instance subG_stsΣ Σ sts :
 Proof. intros ?%subG_inG ?. by split. Qed.
 
 Section definitions.
-  Context `{irisG Λ Σ, stsG Σ sts} (γ : gname).
+  Context `{invG Σ, stsG Σ sts} (γ : gname).
 
   Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
     own γ (sts_frag S T).
@@ -51,13 +51,13 @@ Section definitions.
 End definitions.
 
 Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
-Instance: Params (@sts_inv) 5.
-Instance: Params (@sts_ownS) 5.
-Instance: Params (@sts_own) 6.
+Instance: Params (@sts_inv) 4.
+Instance: Params (@sts_ownS) 4.
+Instance: Params (@sts_own) 5.
 Instance: Params (@sts_ctx) 6.
 
 Section sts.
-  Context `{irisG Λ Σ, stsG Σ sts} (φ : sts.state sts → iProp Σ).
+  Context `{invG Σ, stsG Σ sts} (φ : sts.state sts → iProp Σ).
   Implicit Types N : namespace.
   Implicit Types P Q R : iProp Σ.
   Implicit Types γ : gname.
@@ -115,7 +115,7 @@ Section sts.
       ■ sts.frame_steps T s0 s ★ ▷ φ s ★ ∀ s' T',
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'.
   Proof. by apply sts_accS. Qed.
-    
+
   Lemma sts_openS E N γ S T :
     nclose N ⊆ E →
     sts_ctx γ N φ ★ sts_ownS γ S T ={E,E∖N}=★ ∃ s,
diff --git a/program_logic/thread_local.v b/base_logic/lib/thread_local.v
similarity index 95%
rename from program_logic/thread_local.v
rename to base_logic/lib/thread_local.v
index 78c8a0bd6ccc573c5ceb2735fdbaf66a663723f0..be3dca1744eeb0b18b51991c9fded4443ab7206c 100644
--- a/program_logic/thread_local.v
+++ b/base_logic/lib/thread_local.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.algebra Require Export gmap gset coPset.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -10,7 +10,7 @@ Class thread_localG Σ :=
   tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
 
 Section defs.
-  Context `{irisG Λ Σ, thread_localG Σ}.
+  Context `{invG Σ, thread_localG Σ}.
 
   Definition tl_own (tid : thread_id) (E : coPset) : iProp Σ :=
     own tid (CoPset E, ∅).
@@ -20,11 +20,11 @@ Section defs.
           inv tlN (P ★ own tid (∅, GSet {[i]}) ∨ tl_own tid {[i]}))%I.
 End defs.
 
-Instance: Params (@tl_inv) 4.
+Instance: Params (@tl_inv) 3.
 Typeclasses Opaque tl_own tl_inv.
 
 Section proofs.
-  Context `{irisG Λ Σ, thread_localG Σ}.
+  Context `{invG Σ, thread_localG Σ}.
 
   Global Instance tl_own_timeless tid E : TimelessP (tl_own tid E).
   Proof. rewrite /tl_own; apply _. Qed.
diff --git a/program_logic/viewshifts.v b/base_logic/lib/viewshifts.v
similarity index 92%
rename from program_logic/viewshifts.v
rename to base_logic/lib/viewshifts.v
index cb8a2c66bc9cf571c5b0e3005a9987cec00c2416..be4a00ef4d523f3f82f2d6bde76fbbfd971d2c95 100644
--- a/program_logic/viewshifts.v
+++ b/base_logic/lib/viewshifts.v
@@ -1,11 +1,11 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
 
-Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P -★ |={E1,E2}=> Q))%I.
-Arguments vs {_ _ _} _ _ _%I _%I.
+Arguments vs {_ _} _ _ _%I _%I.
 
-Instance: Params (@vs) 5.
+Instance: Params (@vs) 4.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
@@ -21,7 +21,7 @@ Notation "P ={ E }=> Q" := (True ⊢ P ={E}=> Q)%I
    format "P  ={ E }=>  Q") : C_scope.
 
 Section vs.
-Context `{irisG Λ Σ}.
+Context `{invG Σ}.
 Implicit Types P Q R : iProp Σ.
 Implicit Types N : namespace.
 
diff --git a/program_logic/wsat.v b/base_logic/lib/wsat.v
similarity index 71%
rename from program_logic/wsat.v
rename to base_logic/lib/wsat.v
index d10e72dea41913b0c5a5cc38ac68a8a017fc897a..949897352fed4fc33431335d4950f9b41f796ebc 100644
--- a/program_logic/wsat.v
+++ b/base_logic/lib/wsat.v
@@ -1,79 +1,50 @@
-From iris.program_logic Require Export iris.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 
+Module invG.
+  Class invG (Σ : gFunctors) : Set := WsatG {
+    inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+    enabled_inG :> inG Σ coPset_disjR;
+    disabled_inG :> inG Σ (gset_disjR positive);
+    invariant_name : gname;
+    enabled_name : gname;
+    disabled_name : gname;
+  }.
+End invG.
+Import invG.
+
 Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
   to_agree (Next (iProp_unfold P)).
-Definition ownI `{irisG Λ Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
-Arguments ownI {_ _ _} _ _%I.
+Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
-Instance: Params (@ownI) 4.
-
-Definition ownP `{irisG Λ Σ} (σ : state Λ) : iProp Σ :=
-  own state_name (◯ (Excl' σ)).
-Typeclasses Opaque ownP.
-Instance: Params (@ownP) 4.
-
-Definition ownP_auth `{irisG Λ Σ} (σ : state Λ) : iProp Σ :=
-  own state_name (● (Excl' σ)).
-Typeclasses Opaque ownP_auth.
-Instance: Params (@ownP_auth) 4.
+Instance: Params (@ownI) 3.
 
-Definition ownE `{irisG Λ Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
   own enabled_name (CoPset E).
 Typeclasses Opaque ownE.
-Instance: Params (@ownE) 4.
+Instance: Params (@ownE) 3.
 
-Definition ownD `{irisG Λ Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
   own disabled_name (GSet E).
 Typeclasses Opaque ownD.
-Instance: Params (@ownD) 4.
+Instance: Params (@ownD) 3.
 
-Definition wsat `{irisG Λ Σ} : iProp Σ :=
+Definition wsat `{invG Σ} : iProp Σ :=
   (∃ I : gmap positive (iProp Σ),
     own invariant_name (● (invariant_unfold <$> I : gmap _ _)) ★
     [★ map] i ↦ Q ∈ I, ▷ Q ★ ownD {[i]} ∨ ownE {[i]})%I.
 
-Section ownership.
-Context `{irisG Λ Σ}.
-Implicit Types σ : state Λ.
+Section wsat.
+Context `{invG Σ}.
 Implicit Types P : iProp Σ.
 
-(* Allocation *)
-Lemma iris_alloc `{irisPreG Λ Σ} σ :
-  True ==★ ∃ _ : irisG Λ Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
-Proof.
-  iIntros.
-  iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσ']"; first done.
-  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
-  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
-  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
-  iModIntro; iExists (IrisG _ _ _ γσ γI γE γD).
-  rewrite /wsat /ownE /ownP_auth /ownP; iFrame.
-  iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
-Qed.
-
-(* Physical state *)
-Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ False.
-Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed.
-Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ _ σ).
-Proof. rewrite /ownP; apply _. Qed.
-
-Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ★ ownP σ2 ⊢ σ1 = σ2.
-Proof.
-  rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
-  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
-Qed.
-Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 ==★ ownP_auth σ2 ★ ownP σ2.
-Proof.
-  rewrite /ownP -!own_op.
-  by apply own_update, auth_update, option_local_update, exclusive_local_update.
-Qed.
-
 (* Invariants *)
-Global Instance ownI_contractive i : Contractive (@ownI Λ Σ _ i).
+Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
 Proof.
   intros n P Q HPQ. rewrite /ownI /invariant_unfold. do 4 f_equiv.
   apply Next_contractive=> j ?; by rewrite (HPQ j).
@@ -111,7 +82,7 @@ Qed.
 Lemma ownD_singleton_twice i : ownD {[i]} ★ ownD {[i]} ⊢ False.
 Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
 
-Lemma invariant_lookup `{irisG Λ Σ} (I : gmap positive (iProp Σ)) i P :
+Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
   own invariant_name (● (invariant_unfold <$> I : gmap _ _)) ★
   own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
   ∃ Q, I !! i = Some Q ★ ▷ (Q ≡ P).
@@ -171,4 +142,4 @@ Proof.
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
-End ownership.
+End wsat.
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index b71175c1f0b7659bc48e9da821804058daf6ed6f..01aecda22ec0f9c94b1f160ec847a275b79e5afa 100644
--- a/heap_lang/adequacy.v
+++ b/heap_lang/adequacy.v
@@ -1,7 +1,7 @@
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Export heap.
 From iris.algebra Require Import auth.
-From iris.program_logic Require Import wsat auth.
+From iris.base_logic.lib Require Import wsat auth.
 From iris.heap_lang Require Import proofmode notation.
 From iris.proofmode Require Import tactics.
 
@@ -11,7 +11,7 @@ Class heapPreG Σ := HeapPreG {
 }.
 
 Definition heapΣ : gFunctors :=
-  #[irisΣ heap_lang; authΣ heapUR].
+  #[irisΣ state; authΣ heapUR].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. intros [? ?]%subG_inv. split; apply _. Qed.
 
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 03576859a74534bd1f5db47812a9d3a4417fc0a1..388bcf99c9fe554a83b29b131a550026c469c90e 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -1,7 +1,7 @@
 From iris.heap_lang Require Export lifting.
 From iris.algebra Require Import auth gmap frac dec_agree.
-From iris.program_logic Require Export invariants.
-From iris.program_logic Require Import wsat auth.
+From iris.base_logic.lib Require Export invariants.
+From iris.base_logic.lib Require Import wsat auth.
 From iris.proofmode Require Import tactics.
 Import uPred.
 (* TODO: The entire construction could be generalized to arbitrary languages that have
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 59057fc9a733f2f06b432a98efadb9328046dab8..9436c07e1bd22d0433797b8262ffab1a4d2682e9 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -2,8 +2,7 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Export barrier.
 From iris.prelude Require Import functions.
-From iris.base_logic Require Import big_op lib.saved_prop.
-From iris.program_logic Require Import sts.
+From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.
 
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index a2d7729d85e6a1592df7a691e7ac3933e57bd129..2d2e5be870f440c0c6c28cf9719b6546ee6e2a1a 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import wsat ectx_lifting. (* for ownP *)
+From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 0da50c86363f671b645eddc6747089731ab68bb9..4fa37193439e1d07a2bd65d48272af6a18ff8b35 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,10 +1,66 @@
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op soundness.
-From iris.program_logic Require Import wsat.
+From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
+(* Global functor setup *)
+Definition invΣ : gFunctors :=
+  #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
+    GFunctor (constRF coPset_disjUR);
+    GFunctor (constRF (gset_disjUR positive))].
+
+Class invPreG (Σ : gFunctors) : Set := WsatPreG {
+  inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+  enabled_inPreG :> inG Σ coPset_disjR;
+  disabled_inPreG :> inG Σ (gset_disjR positive);
+}.
+
+Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
+Proof.
+  intros [?%subG_inG [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv; by constructor.
+Qed.
+
+
+Definition irisΣ (Λstate : Type) : gFunctors :=
+  #[invΣ;
+    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].
+
+Class irisPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
+  inv_inG :> invPreG Σ;
+  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
+}.
+Notation irisPreG Λ Σ := (irisPreG' (state Λ) Σ).
+
+Instance subG_irisΣ {Λstate Σ} : subG (irisΣ Λstate) Σ → irisPreG' Λstate Σ.
+Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
+
+
+(* Allocation *)
+Lemma wsat_alloc `{invPreG Σ} : True ==★ ∃ _ : invG Σ, wsat ★ ownE ⊤.
+Proof.
+  iIntros.
+  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
+  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
+  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
+  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
+  rewrite /wsat /ownE; iFrame.
+  iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
+Qed.
+
+Lemma iris_alloc `{irisPreG' Λstate Σ} σ :
+  True ==★ ∃ _ : irisG' Λstate Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
+Proof.
+  iIntros.
+  iMod wsat_alloc as (?) "[Hws HE]".
+  iMod (own_alloc (● (Excl' (σ:leibnizC Λstate)) ⋅ ◯ (Excl' σ)))
+    as (γσ) "[Hσ Hσ']"; first done.
+  iModIntro; iExists (IrisG _ _ _ _ γσ). rewrite /ownP_auth /ownP; iFrame.
+Qed.
+
+
+(* Program logic adequacy *)
 Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
    rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 9ec7f68782c3cb03ced8d5feb06144c2be18127b..99df308b6349a696739113de8675c689a07faef9 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -1,6 +1,5 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.program_logic Require Export ectx_language weakestpre lifting.
-From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 
 Section wp.
diff --git a/program_logic/hoare.v b/program_logic/hoare.v
index 30250418794f31a8554b4abc67c5cf0a26e0e13e..4ce26dd3a8c469430df623db72edb34e6f4c014f 100644
--- a/program_logic/hoare.v
+++ b/program_logic/hoare.v
@@ -1,4 +1,5 @@
-From iris.program_logic Require Export weakestpre viewshifts.
+From iris.program_logic Require Export weakestpre.
+From iris.base_logic.lib Require Export viewshifts.
 From iris.proofmode Require Import tactics.
 
 Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
diff --git a/program_logic/iris.v b/program_logic/iris.v
deleted file mode 100644
index 7abeea65beafa2b452e8c654ec78b8a8a9ac128c..0000000000000000000000000000000000000000
--- a/program_logic/iris.v
+++ /dev/null
@@ -1,31 +0,0 @@
-From iris.base_logic Require Export lib.own.
-From iris.program_logic Require Export language.
-From iris.prelude Require Export coPset.
-From iris.algebra Require Import gmap auth agree gset coPset.
-
-Class irisPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
-  state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
-  invariant_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
-  enabled_inG :> inG Σ coPset_disjR;
-  disabled_inG :> inG Σ (gset_disjR positive);
-}.
-
-Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
-  iris_pre_inG :> irisPreG Λ Σ;
-  state_name : gname;
-  invariant_name : gname;
-  enabled_name : gname;
-  disabled_name : gname;
-}.
-
-Definition irisΣ (Λ : language) : gFunctors :=
-  #[GFunctor (constRF (authUR (optionUR (exclR (stateC Λ)))));
-    GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
-    GFunctor (constRF coPset_disjUR);
-    GFunctor (constRF (gset_disjUR positive))].
-
-Instance subG_irisΣ {Σ Λ} : subG (irisΣ Λ) Σ → irisPreG Λ Σ.
-Proof.
-  intros [?%subG_inG [?%subG_inG
-    [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv]%subG_inv; by constructor.
-Qed.
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index adad69e3166b214297925901e3fc022bd15be188..8b05a82900fd167ef8c0e56d1d29d2fe362867e4 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,4 @@
 From iris.program_logic Require Export weakestpre.
-From iris.program_logic Require Import wsat.
 From iris.base_logic Require Export big_op.
 From iris.proofmode Require Import tactics.
 
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 4865f544b02b5de3031547a71cff6dd15324307b..6b98efa4d050cbbc1f0b58d1f8b81a40dc897dcc 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,10 +1,27 @@
-From iris.program_logic Require Export fancy_updates.
-From iris.program_logic Require Import wsat.
+From iris.base_logic.lib Require Export fancy_updates.
+From iris.program_logic Require Export language.
 From iris.base_logic Require Import big_op.
-From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics classes.
+From iris.algebra Require Import auth.
 Import uPred.
 
+Class irisG' (Λstate : Type) (Σ : gFunctors) : Set := IrisG {
+  iris_invG :> invG Σ;
+  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
+  state_name : gname;
+}.
+Notation irisG Λ Σ := (irisG' (state Λ) Σ).
+
+Definition ownP `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
+  own state_name (◯ (Excl' σ)).
+Typeclasses Opaque ownP.
+Instance: Params (@ownP) 3.
+
+Definition ownP_auth `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
+  own state_name (● (Excl' (σ:leibnizC Λstate))).
+Typeclasses Opaque ownP_auth.
+Instance: Params (@ownP_auth) 4.
+
 Definition wp_pre `{irisG Λ Σ}
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ, (
@@ -96,6 +113,24 @@ Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
+(* Physical state *)
+Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ False.
+Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed.
+Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
+Proof. rewrite /ownP; apply _. Qed.
+
+Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ★ ownP σ2 ⊢ σ1 = σ2.
+Proof.
+  rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
+  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
+Qed.
+Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 ==★ ownP_auth σ2 ★ ownP σ2.
+Proof.
+  rewrite /ownP -!own_op.
+  by apply own_update, auth_update, option_local_update, exclusive_local_update.
+Qed.
+
+(* Weakest pre *)
 Lemma wp_unfold E e Φ : WP e @ E {{ Φ }} ⊣⊢ wp_pre wp E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.
 
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index d18943ad0c29c4d1944093874db1780ff6148e3c..5f05dd6f3f0bc60d80101eed65f9f1d9b464df96 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,6 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import adequacy.
-From iris.program_logic Require Import wsat.
 From iris.heap_lang Require Import proofmode notation.
 
 Section LiftingTests.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7466cef64c69b80d2876b5500d58224d0db54815..fa970acf34daa9a565051e03e291b8028cf2d1af 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Import tactics.
-From iris.program_logic Require Import invariants.
+From iris.base_logic.lib Require Import invariants.
 
 Lemma demo_0 {M : ucmraT} (P Q : uPred M) :
   □ (P ∨ Q) ⊢ (∀ x, x = 0 ∨ x = 1) → (Q ∨ P).
@@ -85,7 +85,7 @@ Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ★ (Q1 ∧ Q2) ⊢ P ★ Q1.
 Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
 
 Section iris.
-  Context `{irisG Λ Σ}.
+  Context `{invG Σ}.
   Implicit Types E : coPset.
   Implicit Types P Q : iProp Σ.