diff --git a/vmbase/src/memory/dbm.rs b/vmbase/src/memory/dbm.rs
index 333d3f6..a7118bb 100644
--- a/vmbase/src/memory/dbm.rs
+++ b/vmbase/src/memory/dbm.rs
@@ -14,7 +14,7 @@
 
 //! Hardware management of the access flag and dirty state.
 
-use super::page_table::{is_leaf_pte, PT_ASID};
+use super::page_table::{is_leaf_pte, PageTable};
 use super::util::flush_region;
 use crate::{dsb, isb, read_sysreg, tlbi, write_sysreg};
 use aarch64_paging::paging::{Attributes, Descriptor, MemoryRegion};
@@ -91,7 +91,7 @@
         // An ISB instruction is required to ensure the effects of completed TLB maintenance
         // instructions are visible to instructions fetched afterwards.
         // See ARM ARM E2.3.10, and G5.9.
-        tlbi!("vale1", PT_ASID, va_range.start().0);
+        tlbi!("vale1", PageTable::ASID, va_range.start().0);
         dsb!("ish");
         isb!();
         Ok(())
diff --git a/vmbase/src/memory/page_table.rs b/vmbase/src/memory/page_table.rs
index 7196e67..3943b03 100644
--- a/vmbase/src/memory/page_table.rs
+++ b/vmbase/src/memory/page_table.rs
@@ -14,6 +14,7 @@
 
 //! Page table management.
 
+use crate::read_sysreg;
 use aarch64_paging::idmap::IdMap;
 use aarch64_paging::paging::{Attributes, MemoryRegion, PteUpdater};
 use aarch64_paging::MapError;
@@ -35,12 +36,6 @@
 const RODATA: Attributes = DATA.union(Attributes::READ_ONLY);
 const DATA_DBM: Attributes = RODATA.union(Attributes::DBM);
 
-/// Root level is given by the value of TCR_EL1.TG0 and TCR_EL1.T0SZ, set in
-/// entry.S. For 4KB granule and 39-bit VA, the root level is 1.
-const PT_ROOT_LEVEL: usize = 1;
-/// Page table ASID.
-pub(super) const PT_ASID: usize = 1;
-
 type Result<T> = result::Result<T, MapError>;
 
 /// High-level API for managing MMU mappings.
@@ -56,11 +51,30 @@
 
 impl Default for PageTable {
     fn default() -> Self {
-        IdMap::new(PT_ASID, PT_ROOT_LEVEL).into()
+        const TCR_EL1_TG0_MASK: usize = 0x3;
+        const TCR_EL1_TG0_SHIFT: u32 = 14;
+        const TCR_EL1_TG0_SIZE_4KB: usize = 0b00;
+
+        const TCR_EL1_T0SZ_MASK: usize = 0x3f;
+        const TCR_EL1_T0SZ_SHIFT: u32 = 0;
+        const TCR_EL1_T0SZ_39_VA_BITS: usize = 64 - 39;
+
+        // Ensure that entry.S wasn't changed without updating the assumptions about TCR_EL1 here.
+        let tcr_el1 = read_sysreg!("tcr_el1");
+        assert_eq!((tcr_el1 >> TCR_EL1_TG0_SHIFT) & TCR_EL1_TG0_MASK, TCR_EL1_TG0_SIZE_4KB);
+        assert_eq!((tcr_el1 >> TCR_EL1_T0SZ_SHIFT) & TCR_EL1_T0SZ_MASK, TCR_EL1_T0SZ_39_VA_BITS);
+
+        IdMap::new(Self::ASID, Self::ROOT_LEVEL).into()
     }
 }
 
 impl PageTable {
+    /// ASID used for the underlying page table.
+    pub const ASID: usize = 1;
+
+    /// Level of the underlying page table's root page.
+    const ROOT_LEVEL: usize = 1;
+
     /// Activates the page table.
     ///
     /// # Safety