diff --git a/_CoqProject b/_CoqProject
index 3947fdf5816aa9e53982550c1266e8381dad928e..4ff403e8eae165ed93d0a2804291897fe7137230 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -70,25 +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/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 99%
rename from program_logic/auth.v
rename to base_logic/lib/auth.v
index 8696055aee20e1ddf8ad2cb01730547f882f12c3..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.
diff --git a/program_logic/boxes.v b/base_logic/lib/boxes.v
similarity index 99%
rename from program_logic/boxes.v
rename to base_logic/lib/boxes.v
index e7524868f427400face0e4e45f31a00dabba9bb3..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.
diff --git a/program_logic/cancelable_invariants.v b/base_logic/lib/cancelable_invariants.v
similarity index 97%
rename from program_logic/cancelable_invariants.v
rename to base_logic/lib/cancelable_invariants.v
index 59b68d3147a81c8742d41dc6e5f3cff0b88e67a2..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.
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 99%
rename from program_logic/fancy_updates.v
rename to base_logic/lib/fancy_updates.v
index b3423cd74dbcbf6cb9bdf4f68bbcb535caa461fa..18af313b1fd31ff52ee0411cfbce2406857cf3d4 100644
--- a/program_logic/fancy_updates.v
+++ b/base_logic/lib/fancy_updates.v
@@ -1,6 +1,6 @@
 From iris.base_logic.lib Require Export own.
 From iris.prelude Require Export coPset.
-From iris.program_logic Require Import wsat.
+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.
diff --git a/program_logic/invariants.v b/base_logic/lib/invariants.v
similarity index 95%
rename from program_logic/invariants.v
rename to base_logic/lib/invariants.v
index e43a561f91339114b3847e08d0e6cd08c9a09b90..727a8b65998af0bf05be9c6c2cafd9fff12c8091 100644
--- a/program_logic/invariants.v
+++ b/base_logic/lib/invariants.v
@@ -1,6 +1,5 @@
-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.
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 99%
rename from program_logic/sts.v
rename to base_logic/lib/sts.v
index b605e567c36ae5d37f73fc968f0cf03ab5b97e12..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.
diff --git a/program_logic/thread_local.v b/base_logic/lib/thread_local.v
similarity index 98%
rename from program_logic/thread_local.v
rename to base_logic/lib/thread_local.v
index 6b4adae59dfb9ca11f5b25c3f0475c254daf9753..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.
diff --git a/program_logic/viewshifts.v b/base_logic/lib/viewshifts.v
similarity index 98%
rename from program_logic/viewshifts.v
rename to base_logic/lib/viewshifts.v
index d7eef16ad0fb48b1d9c7b7c495114e28f575ed5d..be4a00ef4d523f3f82f2d6bde76fbbfd971d2c95 100644
--- a/program_logic/viewshifts.v
+++ b/base_logic/lib/viewshifts.v
@@ -1,4 +1,4 @@
-From iris.program_logic Require Export invariants.
+From iris.base_logic.lib Require Export invariants.
 From iris.proofmode Require Import tactics.
 
 Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
diff --git a/program_logic/wsat.v b/base_logic/lib/wsat.v
similarity index 100%
rename from program_logic/wsat.v
rename to base_logic/lib/wsat.v
diff --git a/heap_lang/adequacy.v b/heap_lang/adequacy.v
index 6addeac521d21035c73950c0b10f890e5f217afb..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.
 
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 c922ee24f0a00c17d960eb0ab6843df0371b17d2..4fa37193439e1d07a2bd65d48272af6a18ff8b35 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,7 +1,7 @@
 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.
 
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/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 7ff2089acbd74ba59310b668a81c82027a19f212..6b98efa4d050cbbc1f0b58d1f8b81a40dc897dcc 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,4 +1,5 @@
-From iris.program_logic Require Export fancy_updates language.
+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.proofmode Require Import tactics classes.
 From iris.algebra Require Import auth.
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 21811f906ac51a424f89ed5061015b16e5068f8b..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).