From b5917a782aa29ae5859ef88cabd0eb6f120d3edd Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Wed, 6 May 2026 15:14:41 +1000
Subject: [PATCH 01/16] loader(aarch64): pass PTs to enable MMU assembler

As opposed to them being accessed via global variables
directly. The reason to do this is to enable us to vary
the page table placement from the C side without needing
to touch or modify the assembly any further, which will
enable the future commits for making the number of page
page table structures dynamic, which is necessary for
making the loader 1:1 all of RAM.

Also, remove some redundant stack pops/pushs to util64.S.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/aarch64/mmu.c    |  8 ++++----
 loader/src/aarch64/util64.S | 26 ++++++++++++++++----------
 2 files changed, 20 insertions(+), 14 deletions(-)

diff --git a/loader/src/aarch64/mmu.c b/loader/src/aarch64/mmu.c
index 8ef6427ce..15fe83564 100644
--- a/loader/src/aarch64/mmu.c
+++ b/loader/src/aarch64/mmu.c
@@ -12,8 +12,8 @@
 #include "../cutil.h"
 #include "../uart.h"
 
-void el1_mmu_enable(void);
-void el2_mmu_enable(void);
+void el1_mmu_enable(void *a, void *b);
+void el2_mmu_enable(void *a);
 
 /* Paging structures for kernel mapping */
 uint64_t boot_lvl0_upper[1 << 9] ALIGN(1 << 12);
@@ -37,9 +37,9 @@ int arch_mmu_enable(int logical_cpu)
     LDR_PRINT("INFO", logical_cpu, "enabling MMU\n");
     el = current_el();
     if (el == EL1) {
-        el1_mmu_enable();
+        el1_mmu_enable(&boot_lvl0_lower, &boot_lvl0_upper);
     } else if (el == EL2) {
-        el2_mmu_enable();
+        el2_mmu_enable(&boot_lvl0_lower);
     } else {
         LDR_PRINT("ERROR", logical_cpu, "unknown EL for MMU enable\n");
     }
diff --git a/loader/src/aarch64/util64.S b/loader/src/aarch64/util64.S
index ccf1889b0..fd94ebe36 100644
--- a/loader/src/aarch64/util64.S
+++ b/loader/src/aarch64/util64.S
@@ -308,7 +308,6 @@ END_FUNC(el1_mmu_disable)
 
 BEGIN_FUNC(el2_mmu_disable)
     stp     x29, x30, [sp, #-16]!
-    stp     x27, x28, [sp, #-16]!
     mov     x29, sp
 
     /* Disable caches */
@@ -323,14 +322,18 @@ BEGIN_FUNC(el2_mmu_disable)
      */
     bl      invalidate_icache
 
-    ldp     x27, x28, [sp], #16
     ldp     x29, x30, [sp], #16
     ret
 END_FUNC(el2_mmu_disable)
 
+/*
+ * Enables the MMU for EL2.
+ * Takes two arguments the physical address for TTBR0_EL1 (x0) and TTBR1_EL1 (x1).
+ */
 BEGIN_FUNC(el1_mmu_enable)
     stp     x29, x30, [sp, #-16]!
     stp     x27, x28, [sp, #-16]!
+    /* move caller-saved to callee-saved registers */
     mov     x29, sp
     mov     x27, x0
     mov     x28, x1
@@ -358,10 +361,8 @@ BEGIN_FUNC(el1_mmu_enable)
     msr     tcr_el1, x10
 
     /* Setup page tables */
-    adrp    x8, boot_lvl0_lower
-    msr     ttbr0_el1, x8
-    adrp    x8, boot_lvl0_upper
-    msr     ttbr1_el1, x8
+    msr     ttbr0_el1, x27  /* argument 0 */
+    msr     ttbr1_el1, x28  /* argument 1 */
     isb
 
     /* invalidate all TLB entries for EL1 */
@@ -374,12 +375,18 @@ BEGIN_FUNC(el1_mmu_enable)
     ldp     x27, x28, [sp], #16
     ldp     x29, x30, [sp], #16
     ret
-
 END_FUNC(el1_mmu_enable)
 
+/*
+ * Enables the MMU for EL2.
+ * Takes one argument, the physical address for TTBR0_EL2 (x0).
+ */
 BEGIN_FUNC(el2_mmu_enable)
     stp     x29, x30, [sp, #-16]!
+    stp     x27, x28, [sp, #-16]!
+    /* move caller-saved to callee-saved registers */
     mov     x29, sp
+    mov     x28, x0
 
     /* Disable the MMU */
     bl      el2_mmu_disable
@@ -403,8 +410,7 @@ BEGIN_FUNC(el2_mmu_enable)
     isb
 
     /* Setup page tables */
-    adrp    x8, boot_lvl0_lower
-    msr     ttbr0_el2, x8
+    msr     ttbr0_el2, x28  /* argument 0 */
     isb
 
     /* invalidate all TLB entries for EL2 */
@@ -423,9 +429,9 @@ BEGIN_FUNC(el2_mmu_enable)
     dsb     ish
     isb
 
+    ldp     x27, x28, [sp], #16
     ldp     x29, x30, [sp], #16
     ret
-
 END_FUNC(el2_mmu_enable)
 
 .extern arm_secondary_cpu_c_entry

From 75b307c342b15b8d3654b3e1f351cf27c9f29ffd Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Mon, 18 May 2026 17:18:47 +1000
Subject: [PATCH 02/16] loader(aarch64): dynamically allocate PTs

This performs cleanups to the loader code, to remove a bunch of
boilerplate, and also makes the page table entries placed in
the loader binary at the end.

This is in preparation for moving towards mapping all of RAM
in the loader.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/aarch64/mmu.c    |  21 +-
 tool/microkit/src/loader.rs | 375 +++++++++++++++++++++++-------------
 tool/microkit/src/sel4.rs   |   2 +-
 tool/microkit/src/util.rs   |   8 +
 4 files changed, 256 insertions(+), 150 deletions(-)

diff --git a/loader/src/aarch64/mmu.c b/loader/src/aarch64/mmu.c
index 15fe83564..39b4676c8 100644
--- a/loader/src/aarch64/mmu.c
+++ b/loader/src/aarch64/mmu.c
@@ -12,18 +12,13 @@
 #include "../cutil.h"
 #include "../uart.h"
 
-void el1_mmu_enable(void *a, void *b);
-void el2_mmu_enable(void *a);
+void el1_mmu_enable(uint64_t aarch64_pt_ttbr0_el1, uint64_t aarch64_pt_ttbr1_el1);
+void el2_mmu_enable(uint64_t aarch64_pt_ttbr0_el2);
 
-/* Paging structures for kernel mapping */
-uint64_t boot_lvl0_upper[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl1_upper[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl2_upper[1 << 9] ALIGN(1 << 12);
-
-/* Paging structures for identity mapping */
-uint64_t boot_lvl0_lower[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl1_lower[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl2_lower[1 << 9] ALIGN(1 << 12);
+/* Pointers to the top-level paging structures */
+uint64_t aarch64_pt_ttbr0_el1;
+uint64_t aarch64_pt_ttbr1_el1;
+uint64_t aarch64_pt_ttbr0_el2;
 
 int arch_mmu_enable(int logical_cpu)
 {
@@ -37,9 +32,9 @@ int arch_mmu_enable(int logical_cpu)
     LDR_PRINT("INFO", logical_cpu, "enabling MMU\n");
     el = current_el();
     if (el == EL1) {
-        el1_mmu_enable(&boot_lvl0_lower, &boot_lvl0_upper);
+        el1_mmu_enable(aarch64_pt_ttbr0_el1, aarch64_pt_ttbr1_el1);
     } else if (el == EL2) {
-        el2_mmu_enable(&boot_lvl0_lower);
+        el2_mmu_enable(aarch64_pt_ttbr0_el2);
     } else {
         LDR_PRINT("ERROR", logical_cpu, "unknown EL for MMU enable\n");
     }
diff --git a/tool/microkit/src/loader.rs b/tool/microkit/src/loader.rs
index 53a2597e2..fd4519f10 100644
--- a/tool/microkit/src/loader.rs
+++ b/tool/microkit/src/loader.rs
@@ -6,19 +6,38 @@
 use crate::elf::{ElfFile, ElfSegmentData};
 use crate::sel4::{Arch, Config};
 use crate::uimage::uimage_serialise;
-use crate::util::{mb, round_up, struct_to_bytes};
+use crate::util::{align_down, align_up, mask, mb, round_up, struct_to_bytes};
+use std::cmp::min;
 use std::fs::File;
 use std::io::{BufWriter, Write};
+use std::mem;
 use std::ops::Range;
 use std::path::Path;
 
 macro_rules! grab_symbol {
-    ($elf: expr, $symbol_name: literal) => {
+    ($elf: expr, $symbol_name: expr) => {
         $elf.find_symbol($symbol_name)
             .expect(concat!("Could not find '", $symbol_name, "' symbol"))
     };
 }
 
+macro_rules! write_symbol {
+    ($loader_image: expr, $image_vaddr: expr, $elf: expr, $symbol: literal, $symbol_var: expr) => {
+        let (addr, size) = grab_symbol!($elf, $symbol);
+        let addr = usize::try_from(addr).expect("addr fits in usize");
+        let size = usize::try_from(size).expect("size fits in usize");
+        let image_vaddr = usize::try_from($image_vaddr).expect("vaddr fits in usize");
+
+        assert!(addr >= image_vaddr);
+        assert!(size == ::std::mem::size_of_val(&$symbol_var));
+
+        let offset: usize = (addr - image_vaddr);
+        assert!(offset <= $loader_image.len());
+
+        $loader_image[offset..(offset + size)].copy_from_slice(&$symbol_var.to_le_bytes());
+    };
+}
+
 const PAGE_TABLE_SIZE: usize = 4096;
 
 pub mod aarch64 {
@@ -32,6 +51,7 @@ pub mod aarch64 {
     pub const LVL0_BITS: u64 = 9;
     pub const LVL1_BITS: u64 = 9;
     pub const LVL2_BITS: u64 = 9;
+    pub const LVL3_BITS: u64 = 9;
 
     pub fn lvl0_index(addr: u64) -> usize {
         let idx = (addr >> (BLOCK_BITS_2MB + LVL2_BITS + LVL1_BITS)) & mask(LVL0_BITS);
@@ -48,6 +68,11 @@ pub mod aarch64 {
         idx as usize
     }
 
+    pub fn lvl3_index(addr: u64) -> usize {
+        let idx = (addr >> PAGE_BITS_4KB) & mask(LVL3_BITS);
+        idx as usize
+    }
+
     /// Stage 1 translation table page/block descriptors have bits[4:2] containing
     /// AttrIndex[2:0]. The AttrIndex values depends on our configuration of
     /// the `MAIR_EL1` or `MAIR_EL2` registers done in util64.S;
@@ -105,6 +130,11 @@ pub mod aarch64 {
     /// > and the level 2 descriptor n is 21.
     pub const BLOCK_BITS_2MB: u64 = 21;
 
+    // TODO:
+
+    pub const BLOCK_BITS_512GB: u64 = 39;
+    pub const PAGE_BITS_4KB: u64 = 12;
+
     /// Per "Table D8-52 Stage 1 VMSAv8-64 Block and Page descriptor fields" and
     /// "Figure D8-14 VMSAv8-64 Block descriptor formats" of ARM DDI0487L.b;
     /// specifically subfigure "4KB, 16KB, and 64KB granules, 48-bit OA"
@@ -289,18 +319,18 @@ mod riscv64 {
 
 /// Checks that each region in the given list does not overlap with any other region.
 /// Panics upon finding an overlapping region
-fn check_non_overlapping(regions: &Vec<(u64, &[u8])>) {
+fn check_non_overlapping(regions: &Vec<(u64, u64)>) {
     let mut checked: Vec<(u64, u64)> = Vec::new();
-    for (base, data) in regions {
-        let end = base + data.len() as u64;
+    for &(base, size) in regions.iter() {
+        let end = base + size;
         // Check that this does not overlap with any checked regions
-        for (b, e) in &checked {
-            if !(end <= *b || *base >= *e) {
+        for &(b, e) in checked.iter() {
+            if !(end <= b || base >= e) {
                 panic!("Overlapping regions: [{base:x}..{end:x}) overlaps [{b:x}..{e:x})");
             }
         }
 
-        checked.push((*base, end));
+        checked.push((base, end));
     }
 }
 
@@ -330,6 +360,7 @@ pub struct Loader<'a> {
     header: LoaderHeader64,
     region_metadata: Vec<LoaderRegion64>,
     regions: Vec<(u64, &'a [u8])>,
+    page_table_bytes: Vec<u8>,
     word_size: usize,
     elf_machine: u16,
     entry: u64,
@@ -427,28 +458,15 @@ impl<'a> Loader<'a> {
             panic!("INTERNAL: could not determine kernel_first_paddr");
         };
 
-        let pagetable_vars = match config.arch {
-            Arch::Aarch64 => Loader::aarch64_setup_pagetables(
-                config,
-                &loader_elf,
-                kernel_first_vaddr,
-                kernel_first_paddr,
-            ),
-            Arch::Riscv64 => Loader::riscv64_setup_pagetables(
-                config,
-                &loader_elf,
-                kernel_first_vaddr,
-                kernel_first_paddr,
-            ),
-            Arch::X86_64 => unreachable!("x86_64 does not support creating a loader image"),
-        };
-
         let image_segment = loader_elf
             .segments
-            .into_iter()
+            .iter()
             .find(|segment| segment.loadable)
             .expect("Did not find loadable segment");
+
+        // Called "vaddr" but due to 1:1 mapping vaddr == paddr.
         let image_vaddr = image_segment.virt_addr;
+
         // We have to clone here as the image executable is part of this function return object,
         // and the loader ELF is deserialised in this scope, so its lifetime will be shorter than
         // the return object.
@@ -458,14 +476,6 @@ impl<'a> Loader<'a> {
             panic!("The loader entry point must be the first byte in the image");
         }
 
-        for (var_addr, var_size, var_data) in pagetable_vars {
-            let offset = var_addr - image_vaddr;
-            assert!(var_size == var_data.len() as u64);
-            assert!(offset > 0);
-            assert!(offset <= loader_image.len() as u64);
-            loader_image[offset as usize..(offset + var_size) as usize].copy_from_slice(&var_data);
-        }
-
         let kernel_entry = kernel_elf.entry;
 
         // initial task virt + pv_offset == initial task physical, so
@@ -477,11 +487,6 @@ impl<'a> Loader<'a> {
             ui_p_reg_start + (initial_task_vaddr_range.end - initial_task_vaddr_range.start);
         assert!(ui_p_reg_end > ui_p_reg_start);
 
-        // This clone isn't too bad as it is just a Vec<(u64, &[u8])>
-        let mut all_regions_with_loader = regions.clone();
-        all_regions_with_loader.push((image_vaddr, &loader_image));
-        check_non_overlapping(&all_regions_with_loader);
-
         let mut region_metadata = Vec::new();
         let mut offset: u64 = 0;
         for (addr, data) in &regions {
@@ -494,10 +499,63 @@ impl<'a> Loader<'a> {
             offset += data.len() as u64;
         }
 
-        let size = std::mem::size_of::<LoaderHeader64>() as u64
-            + region_metadata.iter().fold(0_u64, |acc, x| {
-                acc + x.size + std::mem::size_of::<LoaderRegion64>() as u64
-            });
+        let partial_size = loader_image.len() as u64
+            + mem::size_of::<LoaderHeader64>() as u64
+            + (region_metadata.len() * mem::size_of::<LoaderRegion64>()) as u64
+            + offset;
+
+        let page_tables_paddr_start = image_vaddr + partial_size;
+
+        let mut page_table_bytes = Vec::<u8>::new();
+        match config.arch {
+            Arch::Aarch64 => {
+                let (ttbr0_el2, ttbr0_el1, ttbr1_el1) = Loader::aarch64_setup_pagetables(
+                    config,
+                    &loader_elf,
+                    kernel_first_vaddr,
+                    kernel_first_paddr,
+                    page_tables_paddr_start,
+                    &mut page_table_bytes,
+                );
+
+                write_symbol!(
+                    loader_image,
+                    image_vaddr,
+                    loader_elf,
+                    "aarch64_pt_ttbr0_el2",
+                    ttbr0_el2
+                );
+                write_symbol!(
+                    loader_image,
+                    image_vaddr,
+                    loader_elf,
+                    "aarch64_pt_ttbr0_el1",
+                    ttbr0_el1
+                );
+                write_symbol!(
+                    loader_image,
+                    image_vaddr,
+                    loader_elf,
+                    "aarch64_pt_ttbr1_el1",
+                    ttbr1_el1
+                );
+            }
+            Arch::Riscv64 => {
+                todo!();
+            }
+            Arch::X86_64 => unreachable!("x86_64 does not support creating a loader image"),
+        };
+
+        let size = partial_size + page_table_bytes.len() as u64;
+
+        let mut all_regions_with_loader: Vec<_> = regions
+            .iter()
+            .map(|&(base, data)| (base, data.len() as u64))
+            .collect();
+        all_regions_with_loader.push((image_vaddr, size));
+        check_non_overlapping(&all_regions_with_loader);
+
+        // TODO: Check contained within real RAM.
 
         let header = LoaderHeader64 {
             magic,
@@ -516,6 +574,7 @@ impl<'a> Loader<'a> {
             header,
             region_metadata,
             regions,
+            page_table_bytes,
             word_size: kernel_elf.word_size,
             elf_machine: kernel_elf.machine,
             entry: loader_elf.entry,
@@ -539,6 +598,10 @@ impl<'a> Loader<'a> {
             bytes.extend_from_slice(data);
         }
 
+        bytes.extend_from_slice(&self.page_table_bytes);
+
+        assert!(bytes.len() as u64 == self.header.size);
+
         bytes
     }
 
@@ -672,7 +735,7 @@ impl<'a> Loader<'a> {
                 boot_lvl2_pt[start..end].copy_from_slice(&lvl3_pt_entry.to_le_bytes());
                 index_lvl2 += 1;
             }
-            let first_paddr_aligned = round_up(first_paddr, 1 << riscv64::BLOCK_BITS_2MB);
+            let first_paddr_aligned = align_up(first_paddr, riscv64::BLOCK_BITS_2MB);
             for (page, i) in (index_lvl2..512).enumerate() {
                 let start = 8 * i;
                 let end = start + 8;
@@ -787,128 +850,168 @@ impl<'a> Loader<'a> {
     /// ```
     ///
     fn aarch64_setup_pagetables(
-        _config: &Config,
+        config: &Config,
         elf: &ElfFile,
-        first_vaddr: u64,
-        first_paddr: u64,
-    ) -> Vec<(u64, u64, [u8; PAGE_TABLE_SIZE])> {
-        use aarch64::s1_mair_attr_index::{MT_DEVICE_nGnRnE, MT_NORMAL};
+        kernel_first_vaddr: u64,
+        kernel_first_paddr: u64,
+        page_tables_paddr_start: u64,
+        page_table_bytes: &mut Vec<u8>,
+    ) -> (u64, u64, u64) {
+        use aarch64::{
+            block_descriptor, lvl0_index, lvl1_index, lvl2_index, lvl3_index, page_descriptor,
+            s1_mair_attr_index::{MT_DEVICE_nGnRnE, MT_NORMAL},
+            table_descriptor, BLOCK_BITS_1GB, BLOCK_BITS_2MB, BLOCK_BITS_512GB, PAGE_BITS_4KB,
+        };
+
+        const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
+
+        let mut serialise_page_table_to_paddr = {
+            let page_tables_paddr_start = {
+                let aligned_pt_paddr_start =
+                    page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64);
+                if aligned_pt_paddr_start != page_tables_paddr_start {
+                    let alignment_diff =
+                        (aligned_pt_paddr_start - page_tables_paddr_start) as usize;
+                    page_table_bytes.resize(alignment_diff, 0);
+                }
+
+                aligned_pt_paddr_start
+            };
 
-        let (boot_lvl1_lower_addr, boot_lvl1_lower_size) = grab_symbol!(elf, "boot_lvl1_lower");
-        let (boot_lvl1_upper_addr, boot_lvl1_upper_size) = grab_symbol!(elf, "boot_lvl1_upper");
-        let (boot_lvl2_upper_addr, boot_lvl2_upper_size) = grab_symbol!(elf, "boot_lvl2_upper");
-        let (boot_lvl0_lower_addr, boot_lvl0_lower_size) = grab_symbol!(elf, "boot_lvl0_lower");
-        let (boot_lvl0_upper_addr, boot_lvl0_upper_size) = grab_symbol!(elf, "boot_lvl0_upper");
-        let (boot_lvl2_lower_addr, boot_lvl2_lower_size) = grab_symbol!(elf, "boot_lvl2_lower");
+            // This maintains the current end of the PT array.
+            let mut next_pt_paddr = page_tables_paddr_start;
+
+            move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
+                let pt_paddr = next_pt_paddr;
+                page_table_bytes.extend(page_table.iter().flat_map(|pte| pte.to_le_bytes()));
+                next_pt_paddr += PAGE_TABLE_SIZE as u64;
+                page_table.fill(0);
+                pt_paddr
+            }
+        };
 
         let (loader_start_addr, _) = grab_symbol!(elf, "_loader_start");
         let (loader_end_addr, _) = grab_symbol!(elf, "_loader_end");
-
-        if aarch64::lvl1_index(loader_start_addr) != aarch64::lvl1_index(loader_end_addr) {
+        if lvl1_index(loader_start_addr) != lvl1_index(loader_end_addr) {
             panic!("We only map 1GiB, but loader paddr range covers multiple GiB");
         }
 
-        let mut boot_lvl0_lower: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-        {
-            let pt_entry = aarch64::table_descriptor(boot_lvl1_lower_addr);
-            boot_lvl0_lower[..8].copy_from_slice(&pt_entry.to_le_bytes());
-        }
-
-        let mut boot_lvl1_lower: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-
-        // map optional UART MMIO in l1 1GB page, only available if CONFIG_PRINTING
-        if let Ok((uart_addr, uart_addr_size)) = elf.find_symbol("uart_addr") {
+        let uart_base = if let Ok((uart_addr, uart_addr_size)) = elf.find_symbol("uart_addr") {
             let data = elf
                 .get_data(uart_addr, uart_addr_size)
                 .expect("uart_addr not initialized");
 
-            let uart_base = u64::from_le_bytes(data[0..8].try_into().unwrap());
+            Some(u64::from_le_bytes(data[0..8].try_into().unwrap()))
+        } else {
+            None
+        };
+
+        // Manufacture the constants as per the diagram.
+        let k = align_down(kernel_first_vaddr, BLOCK_BITS_512GB);
+        let l = align_down(kernel_first_vaddr, BLOCK_BITS_1GB);
+        let m = align_down(kernel_first_vaddr, BLOCK_BITS_2MB);
+        let p = align_down(kernel_first_paddr, BLOCK_BITS_2MB);
+        let i = align_down(loader_start_addr, BLOCK_BITS_1GB);
+        let u = uart_base.map(|addr| align_down(addr, BLOCK_BITS_1GB));
+        let s = align_down(loader_start_addr, BLOCK_BITS_2MB);
+        let t = align_up(loader_end_addr, BLOCK_BITS_2MB);
+
+        // Manufacture the kernel page tables, which is relatively straightforward.
+        let kernel_lvl1_pt_paddr = {
+            // First, the Level 2 Upr table.
+            let lvl2_pt_paddr = {
+                let mut lvl2_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+
+                let mut vaddr = m;
+                let mut paddr = p;
+                while lvl1_index(m) == lvl1_index(vaddr) {
+                    lvl2_pt_kernel[lvl2_index(vaddr)] = block_descriptor(2, paddr, MT_NORMAL);
+
+                    vaddr += 1 << BLOCK_BITS_2MB;
+                    paddr += 1 << BLOCK_BITS_2MB;
+                }
 
-            let lvl1_idx = aarch64::lvl1_index(uart_base);
+                serialise_page_table_to_paddr(&mut lvl2_pt_kernel)
+            };
 
-            let pt_entry = aarch64::block_descriptor(1, uart_base, MT_DEVICE_nGnRnE);
+            // Then, the Level 1 Upr table.
+            let mut lvl1_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+            lvl1_pt_kernel[lvl1_index(l)] = table_descriptor(lvl2_pt_paddr);
 
-            let start = 8 * lvl1_idx;
-            let end = 8 * (lvl1_idx + 1);
-            boot_lvl1_lower[start..end].copy_from_slice(&pt_entry.to_le_bytes());
-        }
+            serialise_page_table_to_paddr(&mut lvl1_pt_kernel)
+        };
 
-        let mut boot_lvl2_lower: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
+        // Manufacture the loader page tables.
+        let loader_lvl1_pt_paddr = {
+            // First, the Level 2 Lwr table
+            let lvl2_pt_paddr = {
+                let mut lvl2_pt_loader = [0u64; PAGE_TABLE_ENTRIES];
 
-        // 1GB lvl1 Table entry
-        let pt_entry = aarch64::table_descriptor(boot_lvl2_lower_addr);
-        let lvl1_idx = aarch64::lvl1_index(loader_start_addr);
-        let start = 8 * lvl1_idx;
-        let end = 8 * (lvl1_idx + 1);
-        boot_lvl1_lower[start..end].copy_from_slice(&pt_entry.to_le_bytes());
+                // Identity mapped: vaddr == paddr.
+                let mut addr = s;
+                while addr < t {
+                    lvl2_pt_loader[lvl2_index(addr)] = block_descriptor(2, addr, MT_DEVICE_nGnRnE);
 
-        // map the loader 1:1 access into 2MB lvl2 Block entries for a 4KB granule
-        let lvl2_idx = aarch64::lvl2_index(loader_start_addr);
-        for i in lvl2_idx..=aarch64::lvl2_index(loader_end_addr) {
-            let entry_idx: u64 =
-                ((i - aarch64::lvl2_index(loader_start_addr)) << aarch64::BLOCK_BITS_2MB) as u64;
+                    addr += 1 << BLOCK_BITS_2MB;
+                }
 
-            let pt_entry =
-                aarch64::block_descriptor(2, loader_start_addr + entry_idx, MT_DEVICE_nGnRnE);
+                // TODO: this is a complete hack specific to BCM2711/Raspberry Pi 4B and
+                // will be reworked with patches that re-do this loader mapping code.
+                if elf.find_symbol("cpus_release_addr").is_ok() {
+                    // Make sure we don't override the loader mappings done above;
+                    // and that this is located at 0x0.
+                    assert!(s != 0);
+                    assert!(i == 0);
 
-            let start = 8 * i;
-            let end = 8 * (i + 1);
-            boot_lvl2_lower[start..end].copy_from_slice(&pt_entry.to_le_bytes());
-        }
+                    lvl2_pt_loader[lvl2_index(0)] = block_descriptor(2, 0, MT_DEVICE_nGnRnE);
+                }
 
-        // TODO: this is a complete hack specific to BCM2711/Raspberry Pi 4B and
-        // will be removed with patches that re-do this loader mapping code.
-        if elf.find_symbol("cpus_release_addr").is_ok() {
-            let lvl2_idx = aarch64::lvl2_index(0);
-            // Make sure we don't override the loader mappings done above.
-            assert!(aarch64::lvl2_index(loader_start_addr) != lvl2_idx);
-            assert!(aarch64::lvl1_index(loader_start_addr) == aarch64::lvl1_index(0));
+                serialise_page_table_to_paddr(&mut lvl2_pt_loader)
+            };
 
-            let pt_entry = aarch64::block_descriptor(2, lvl2_idx as u64, MT_DEVICE_nGnRnE);
+            // Then, the Level 1 Lwr table.
+            let mut lvl1_pt_loader = [0u64; PAGE_TABLE_ENTRIES];
+            lvl1_pt_loader[lvl1_index(i)] = table_descriptor(lvl2_pt_paddr);
 
-            let start = 8 * lvl2_idx;
-            let end = 8 * (lvl2_idx + 1);
-            boot_lvl2_lower[start..end].copy_from_slice(&pt_entry.to_le_bytes());
-        }
+            // map optional UART MMIO in l1 1GB page, only available if CONFIG_PRINTING
+            if let Some(u) = u {
+                // UART no overlap with Loader.
+                assert!(lvl1_index(i) != lvl1_index(u));
+                lvl1_pt_loader[lvl1_index(u)] = block_descriptor(1, u, MT_DEVICE_nGnRnE);
+            }
 
-        let mut boot_lvl0_upper: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-        {
-            let pt_entry = aarch64::table_descriptor(boot_lvl1_upper_addr);
-            let idx = aarch64::lvl0_index(first_vaddr);
-            // For EL2.
-            boot_lvl0_lower[8 * idx..8 * (idx + 1)].copy_from_slice(&pt_entry.to_le_bytes());
-            // For EL1.
-            boot_lvl0_upper[8 * idx..8 * (idx + 1)].copy_from_slice(&pt_entry.to_le_bytes());
-        }
+            serialise_page_table_to_paddr(&mut lvl1_pt_loader)
+        };
 
-        let mut boot_lvl1_upper: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-        {
-            let pt_entry = aarch64::table_descriptor(boot_lvl2_upper_addr);
-            let idx = aarch64::lvl1_index(first_vaddr);
-            boot_lvl1_upper[8 * idx..8 * (idx + 1)].copy_from_slice(&pt_entry.to_le_bytes());
-        }
+        // Depending on whether we are in hypervisor mode, we either need to
+        // return the TTBR0_EL2 or TTBR[0,1]_EL1 values. We return u64::MAX
+        // so as to return garbage - an unaligned address outside of physical
+        // memory.
+        if config.hypervisor {
+            // Manufacture the Level 0 table, containing the kernel table
+            // and the RAM tables.
 
-        let mut boot_lvl2_upper: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
+            let mut ttbr0_el2_pt = [0u64; PAGE_TABLE_ENTRIES];
 
-        let lvl2_idx = aarch64::lvl2_index(first_vaddr);
-        for i in lvl2_idx..512 {
-            let entry_idx: u64 =
-                ((i - aarch64::lvl2_index(first_vaddr)) << aarch64::BLOCK_BITS_2MB) as u64;
+            ttbr0_el2_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
+            ttbr0_el2_pt[lvl0_index(0)] = table_descriptor(loader_lvl1_pt_paddr);
 
-            let pt_entry = aarch64::block_descriptor(2, first_paddr + entry_idx, MT_NORMAL);
+            let ttbr0_el2 = serialise_page_table_to_paddr(&mut ttbr0_el2_pt);
 
-            let start = 8 * i;
-            let end = 8 * (i + 1);
-            boot_lvl2_upper[start..end].copy_from_slice(&pt_entry.to_le_bytes());
-        }
+            (ttbr0_el2, u64::MAX, u64::MAX)
+        } else {
+            let mut ttbr0_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
+            let mut ttbr1_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
 
-        vec![
-            (boot_lvl0_lower_addr, boot_lvl0_lower_size, boot_lvl0_lower),
-            (boot_lvl1_lower_addr, boot_lvl1_lower_size, boot_lvl1_lower),
-            (boot_lvl0_upper_addr, boot_lvl0_upper_size, boot_lvl0_upper),
-            (boot_lvl1_upper_addr, boot_lvl1_upper_size, boot_lvl1_upper),
-            (boot_lvl2_upper_addr, boot_lvl2_upper_size, boot_lvl2_upper),
-            (boot_lvl2_lower_addr, boot_lvl2_lower_size, boot_lvl2_lower),
-        ]
+            // Kernel in TTBR1 (Upper)
+            ttbr1_el1_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
+            // Loader in TTBR0 (Lower)
+            ttbr0_el1_pt[lvl0_index(k)] = table_descriptor(loader_lvl1_pt_paddr);
+
+            let ttbr0_el1 = serialise_page_table_to_paddr(&mut ttbr0_el1_pt);
+            let ttbr1_el1 = serialise_page_table_to_paddr(&mut ttbr1_el1_pt);
+
+            (u64::MAX, ttbr0_el1, ttbr1_el1)
+        }
     }
 }
diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs
index d95084a74..2c30309bd 100644
--- a/tool/microkit/src/sel4.rs
+++ b/tool/microkit/src/sel4.rs
@@ -249,7 +249,7 @@ pub fn emulate_kernel_boot(
     }
 }
 
-#[derive(Deserialize)]
+#[derive(Deserialize, Debug)]
 pub struct PlatformConfigRegion {
     pub start: u64,
     pub end: u64,
diff --git a/tool/microkit/src/util.rs b/tool/microkit/src/util.rs
index 6f2c0e275..211c794d6 100644
--- a/tool/microkit/src/util.rs
+++ b/tool/microkit/src/util.rs
@@ -54,6 +54,14 @@ pub const fn round_down(n: u64, x: u64) -> u64 {
     }
 }
 
+pub const fn align_up(n: u64, bits: u64) -> u64 {
+    round_up(n, 1 << bits)
+}
+
+pub const fn align_down(n: u64, bits: u64) -> u64 {
+    round_down(n, 1 << bits)
+}
+
 pub fn is_power_of_two(n: u64) -> bool {
     assert!(n > 0);
     n & (n - 1) == 0

From e8ee048fc88786c768998b9c8d5e6f09866e2518 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Mon, 18 May 2026 18:28:16 +1000
Subject: [PATCH 03/16] loader(riscv64): apply the aarch64 treatment

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/riscv/mmu.c      |  12 +-
 tool/microkit/src/loader.rs | 262 ++++++++++++++++++++++++++----------
 2 files changed, 191 insertions(+), 83 deletions(-)

diff --git a/loader/src/riscv/mmu.c b/loader/src/riscv/mmu.c
index 7751b25e9..b40350ca7 100644
--- a/loader/src/riscv/mmu.c
+++ b/loader/src/riscv/mmu.c
@@ -8,15 +8,9 @@
 #include <stdint.h>
 
 #include "../arch.h"
-#include "../cutil.h"
-
-/* Paging structures for kernel mapping */
-uint64_t boot_lvl1_pt[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl2_pt[1 << 9] ALIGN(1 << 12);
-uint64_t boot_lvl3_pt[1 << 9] ALIGN(1 << 12);
-/* Paging structures for identity mapping */
-uint64_t boot_lvl2_pt_loader[1 << 9] ALIGN(1 << 12);
 
+/* Pointers to the top-level paging structures */
+uintptr_t riscv64_boot_lvl1_pt;
 
 /*
  * This is the encoding for the MODE field of the satp register when
@@ -36,7 +30,7 @@ int arch_mmu_enable(int logical_cpu)
     asm volatile(
         "csrw satp, %0\n"
         :
-        : "r"(VM_MODE | (uintptr_t)boot_lvl1_pt >> RISCV_PGSHIFT)
+        : "r"(VM_MODE | riscv64_boot_lvl1_pt >> RISCV_PGSHIFT)
         :
     );
     asm volatile("fence.i" ::: "memory");
diff --git a/tool/microkit/src/loader.rs b/tool/microkit/src/loader.rs
index fd4519f10..8205a50e6 100644
--- a/tool/microkit/src/loader.rs
+++ b/tool/microkit/src/loader.rs
@@ -280,6 +280,7 @@ pub mod aarch64 {
 }
 
 mod riscv64 {
+    pub(crate) const BLOCK_BITS_1GB: u64 = 30;
     pub(crate) const BLOCK_BITS_2MB: u64 = 21;
     pub(crate) const PAGE_BITS_4K: u64 = 12;
 
@@ -541,7 +542,21 @@ impl<'a> Loader<'a> {
                 );
             }
             Arch::Riscv64 => {
-                todo!();
+                let boot_lvl1_pt = Loader::riscv64_setup_pagetables(
+                    config,
+                    &loader_elf,
+                    kernel_first_vaddr,
+                    kernel_first_paddr,
+                    page_tables_paddr_start,
+                    &mut page_table_bytes,
+                );
+                write_symbol!(
+                    loader_image,
+                    image_vaddr,
+                    loader_elf,
+                    "riscv64_boot_lvl1_pt",
+                    boot_lvl1_pt
+                );
             }
             Arch::X86_64 => unreachable!("x86_64 does not support creating a loader image"),
         };
@@ -667,95 +682,194 @@ impl<'a> Loader<'a> {
         }
     }
 
+    /// RISC-V 64 page tables for our purposes uses the Sv39 translation scheme
+    /// (3-level page tables).
+    ///
+    /// It is split into two halves: the Upper/Kernel part of the page tables,
+    /// which matches the format seL4 expects. The lower half contains an
+    /// identity mapped region for the loader.
+    ///
+    /// ```txt
+    ///            (512 GiB)
+    ///   512 +---- Level 1 ---+ 2^39
+    ///       |                |
+    ///       |     (empty)    |
+    ///       |                |
+    ///   k+1 +----------------+                   (1 GiB)
+    ///       | Level 2 Kernel | ----------> +---- Level 2 ---+             +-------------+
+    ///     k +----------------+             |                | ----------> | 2 MiB block |
+    ///       |                |         511 |----------------|             +-------------+
+    ///       |                |             |                | ----------> | 2 MiB block |
+    ///       |                |         510 |----------------|             +-------------+
+    ///       |                |             |                | ----------> | 2 MiB block |
+    ///       |                |             |----------------|             +-------------
+    ///       |                |                   (...)           (...)         (...)          Kernel Regions
+    ///       |                |             |----------------|             +-------------+
+    ///       |                |             |                | ----------> | 2 MiB block |
+    ///       |                |         l+1 |----------------|             +-------------+
+    ///       |                |             | Level 3 Kernel | ----+
+    ///       |                |           l |----------------|     |
+    ///       |                |             |                |     |           (2 MiB)
+    ///       |                |             |                |     +-----> +-- Level 3 --+             +------------+
+    ///       |                |             |                |             |             | ----------> | 4 KiB page |
+    ///       |                |             |                |         511 |-------------|             +------------+
+    ///       |                |             |     (empty)    |             |             | ----------> | 4 KiB page |
+    ///       |     (empty)    |             |                |             |-------------|             +------------+
+    ///       |                |             |                |             |             | ----------> | 4 KiB page |
+    ///       |                |             |                |           m |-------------|             +------------+ p
+    ///       |                |             |                |             |   (empty)   |
+    ///       |                |             |                |             +-------------+
+    ///       |                |             |                |
+    ///       |                |           0 +----------------+
+    ///       |                |
+    ///       |                |
+    ///       |                |
+    ///       |                |
+    ///       |                |
+    ///   s+1 +----------------+                  (1 GiB)
+    ///       | Level 2 Loader | ---------->  +-- Level 2 --+             +-------------+
+    ///     s +----------------+              |             | ----------> | 2 MiB block |
+    ///       |                |          511 +-------------+             +-------------+
+    ///       |                |              |             | ----------> | 2 MiB block |
+    ///       |    (empty)     |          510 +-------------+             +-------------+
+    ///       |                |              |             | ----------> | 2 MiB block |
+    ///       |                |              |-------------|             +-------------+
+    ///     0 +----------------+              |             | ----------> | 2 MiB block |
+    ///                                       |-------------|             +-------------+
+    ///                                            (...)         (...)         (...)          Loader Regions
+    ///                                       |-------------|             +-------------+
+    ///                                       |             | ----------> | 2 MiB block |
+    ///                                       |-------------|             +-------------+
+    ///                                       |             | ----------> | 2 MiB block |
+    ///                                     t +-------------+             +-------------+
+    ///                                       |             |
+    ///                                       |   (empty)   |
+    ///                                       |             |
+    ///                                       +-------------+
+    ///
+    ///
+    /// Where:
+    ///      k = align_down(kernel_first_vaddr, 1GiB),
+    ///      l = align_down(kernel_first_vaddr, 2MiB),
+    ///      m = align_down(kernel_first_vaddr, 4KiB),
+    ///      p = align_down(kernel_first_paddr, 4KiB),
+    ///
+    ///      s = align_down(text_addr, 1GiB),
+    ///      t = align_down(text_addr, 2MiB),
+    /// ```
+    ///
     fn riscv64_setup_pagetables(
         config: &Config,
         elf: &ElfFile,
-        first_vaddr: u64,
-        first_paddr: u64,
-    ) -> Vec<(u64, u64, [u8; PAGE_TABLE_SIZE])> {
+        kernel_first_vaddr: u64,
+        kernel_first_paddr: u64,
+        page_tables_paddr_start: u64,
+        page_table_bytes: &mut Vec<u8>,
+    ) -> u64 {
+        use riscv64::{pt_index, pte_leaf, pte_next, BLOCK_BITS_1GB, BLOCK_BITS_2MB, PAGE_BITS_4K};
+
         let (text_addr, _) = grab_symbol!(elf, "_text");
-        let (boot_lvl1_pt_addr, boot_lvl1_pt_size) = grab_symbol!(elf, "boot_lvl1_pt");
-        let (boot_lvl2_pt_addr, boot_lvl2_pt_size) = grab_symbol!(elf, "boot_lvl2_pt");
-        let (boot_lvl3_pt_addr, boot_lvl3_pt_size) = grab_symbol!(elf, "boot_lvl3_pt");
-        let (boot_lvl2_pt_loader_addr, boot_lvl2_pt_loader_size) =
-            grab_symbol!(elf, "boot_lvl2_pt_loader");
 
         // We map the loader using 2MB pages, so make sure the base is actually aligned.
-        assert!(text_addr.is_multiple_of(1 << riscv64::BLOCK_BITS_2MB));
+        assert!(text_addr.is_multiple_of(1 << BLOCK_BITS_2MB));
 
-        let num_pt_levels = config.riscv_pt_levels.unwrap().levels();
+        const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
 
-        let mut boot_lvl1_pt: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-        {
-            let text_index_lvl1 = riscv64::pt_index(num_pt_levels, text_addr, 1);
-            let pt_entry = riscv64::pte_next(boot_lvl2_pt_loader_addr);
-            let start = 8 * text_index_lvl1;
-            let end = start + 8;
-            boot_lvl1_pt[start..end].copy_from_slice(&pt_entry.to_le_bytes());
-        }
+        let mut serialise_page_table_to_paddr = {
+            let page_tables_paddr_start = {
+                let aligned_pt_paddr_start =
+                    page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64);
+                if aligned_pt_paddr_start != page_tables_paddr_start {
+                    let alignment_diff =
+                        (aligned_pt_paddr_start - page_tables_paddr_start) as usize;
+                    page_table_bytes.resize(alignment_diff, 0);
+                }
+
+                aligned_pt_paddr_start
+            };
+
+            // This maintains the current end of the PT array.
+            let mut next_pt_paddr = page_tables_paddr_start;
 
-        let mut boot_lvl2_pt_loader: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-        {
-            let text_index_lvl2 = riscv64::pt_index(num_pt_levels, text_addr, 2);
-            for (page, i) in (text_index_lvl2..512).enumerate() {
-                let start = 8 * i;
-                let end = start + 8;
-                let addr = text_addr + ((page as u64) << riscv64::BLOCK_BITS_2MB);
-                let pt_entry = riscv64::pte_leaf(addr);
-                boot_lvl2_pt_loader[start..end].copy_from_slice(&pt_entry.to_le_bytes());
+            move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
+                let pt_paddr = next_pt_paddr;
+                page_table_bytes.extend(page_table.iter().flat_map(|pte| pte.to_le_bytes()));
+                next_pt_paddr += PAGE_TABLE_SIZE as u64;
+                page_table.fill(0);
+                pt_paddr
             }
-        }
+        };
 
-        {
-            let index = riscv64::pt_index(num_pt_levels, first_vaddr, 1);
-            let start = 8 * index;
-            let end = start + 8;
-            boot_lvl1_pt[start..end]
-                .copy_from_slice(&riscv64::pte_next(boot_lvl2_pt_addr).to_le_bytes());
-        }
+        let num_pt_levels = config.riscv_pt_levels.unwrap().levels();
+        assert!(num_pt_levels == 3);
 
-        let mut boot_lvl3_pt: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-        let mut boot_lvl2_pt: [u8; PAGE_TABLE_SIZE] = [0; PAGE_TABLE_SIZE];
-        {
-            let mut index_lvl2 = riscv64::pt_index(num_pt_levels, first_vaddr, 2);
-            if !first_vaddr.is_multiple_of(1 << riscv64::BLOCK_BITS_2MB) {
-                let index_lvl3 = riscv64::pt_index(num_pt_levels, first_vaddr, 3);
-                for (page, i) in (index_lvl3..512).enumerate() {
-                    let start = 8 * i;
-                    let end = start + 8;
-                    let addr = first_paddr + ((page as u64) << riscv64::PAGE_BITS_4K);
-                    assert!(addr.is_multiple_of(1 << riscv64::PAGE_BITS_4K));
-                    let pt_entry = riscv64::pte_leaf(addr);
-                    boot_lvl3_pt[start..end].copy_from_slice(&pt_entry.to_le_bytes());
+        // Manufacture the constants as per the diagram.
+        let k = align_down(kernel_first_vaddr, BLOCK_BITS_1GB);
+        let l = align_down(kernel_first_vaddr, BLOCK_BITS_2MB);
+        let m = align_down(kernel_first_vaddr, PAGE_BITS_4K);
+        let p = align_down(kernel_first_paddr, PAGE_BITS_4K);
+
+        let s = align_down(text_addr, BLOCK_BITS_1GB);
+        let t = align_down(text_addr, BLOCK_BITS_2MB);
+
+        // Manufacture the kernel page tables
+        let kernel_lvl2_pt_paddr = {
+            let mut lvl2_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+
+            let mut paddr = p;
+            let index_l = pt_index(num_pt_levels, l, 2);
+
+            lvl2_pt_kernel[index_l] = if kernel_first_vaddr.is_multiple_of(1 << BLOCK_BITS_2MB) {
+                assert!(paddr.is_multiple_of(1 << BLOCK_BITS_2MB));
+                let pte = pte_leaf(paddr);
+                paddr += 1 << BLOCK_BITS_2MB;
+                pte
+            } else {
+                let mut lvl3_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+
+                let index_m = pt_index(num_pt_levels, m, 3);
+
+                for index in index_m..512 {
+                    lvl3_pt_kernel[index] = pte_leaf(paddr);
+                    paddr += 1 << PAGE_BITS_4K;
                 }
-                let start = 8 * index_lvl2;
-                let end = start + 8;
-                let lvl3_pt_entry = riscv64::pte_next(boot_lvl3_pt_addr);
-                assert!(boot_lvl3_pt_addr.is_multiple_of(1 << riscv64::PAGE_BITS_4K));
-                boot_lvl2_pt[start..end].copy_from_slice(&lvl3_pt_entry.to_le_bytes());
-                index_lvl2 += 1;
+
+                let kernel_lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt_kernel);
+                pte_next(kernel_lvl3_pt_paddr)
+            };
+
+            for index in (index_l + 1)..512 {
+                lvl2_pt_kernel[index] = pte_leaf(paddr);
+                paddr += 1 << BLOCK_BITS_2MB;
             }
-            let first_paddr_aligned = align_up(first_paddr, riscv64::BLOCK_BITS_2MB);
-            for (page, i) in (index_lvl2..512).enumerate() {
-                let start = 8 * i;
-                let end = start + 8;
-                let addr = first_paddr_aligned + ((page as u64) << riscv64::BLOCK_BITS_2MB);
-                assert!(addr.is_multiple_of(1 << riscv64::BLOCK_BITS_2MB));
-                let pt_entry = riscv64::pte_leaf(addr);
-                boot_lvl2_pt[start..end].copy_from_slice(&pt_entry.to_le_bytes());
+
+            serialise_page_table_to_paddr(&mut lvl2_pt_kernel)
+        };
+
+        // Manufacture the loader page tables, which is relatively straightforward
+        let loader_lvl2_pt_paddr = {
+            let mut lvl2_pt_loader = [0u64; PAGE_TABLE_ENTRIES];
+
+            // Identity mapped, so vaddr == paddr.
+            let mut paddr = t;
+
+            for index in pt_index(num_pt_levels, t, 2)..512 {
+                lvl2_pt_loader[index] = pte_leaf(paddr);
+                paddr += 1 << BLOCK_BITS_2MB;
             }
-        }
 
-        vec![
-            (boot_lvl1_pt_addr, boot_lvl1_pt_size, boot_lvl1_pt),
-            (boot_lvl2_pt_addr, boot_lvl2_pt_size, boot_lvl2_pt),
-            (boot_lvl3_pt_addr, boot_lvl3_pt_size, boot_lvl3_pt),
-            (
-                boot_lvl2_pt_loader_addr,
-                boot_lvl2_pt_loader_size,
-                boot_lvl2_pt_loader,
-            ),
-        ]
+            serialise_page_table_to_paddr(&mut lvl2_pt_loader)
+        };
+
+        // Manufacture the Level 1 table
+        let mut boot_lvl1_pt = [0u64; PAGE_TABLE_ENTRIES];
+
+        let index_s = pt_index(num_pt_levels, s, 1);
+        let index_k = pt_index(num_pt_levels, k, 1);
+        boot_lvl1_pt[index_k] = pte_next(kernel_lvl2_pt_paddr);
+        boot_lvl1_pt[index_s] = pte_next(loader_lvl2_pt_paddr);
+
+        serialise_page_table_to_paddr(&mut boot_lvl1_pt)
     }
 
     /// AArch64 loader page tables have two variations:

From 3aba5722f3f8c393abe79e4386687c5683edbe12 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Fri, 22 May 2026 10:48:45 +1000
Subject: [PATCH 04/16] [WIP] ram

---
 tool/microkit/src/loader.rs | 419 +++++++++++++++++++++++++++++-------
 tool/microkit/src/sel4.rs   |   2 +-
 2 files changed, 337 insertions(+), 84 deletions(-)

diff --git a/tool/microkit/src/loader.rs b/tool/microkit/src/loader.rs
index 8205a50e6..d41225f6a 100644
--- a/tool/microkit/src/loader.rs
+++ b/tool/microkit/src/loader.rs
@@ -4,9 +4,9 @@
 // SPDX-License-Identifier: BSD-2-Clause
 //
 use crate::elf::{ElfFile, ElfSegmentData};
-use crate::sel4::{Arch, Config};
+use crate::sel4::{Arch, Config, PlatformConfigRegion};
 use crate::uimage::uimage_serialise;
-use crate::util::{align_down, align_up, mask, mb, round_up, struct_to_bytes};
+use crate::util::{align_down, mb, round_up, struct_to_bytes};
 use std::cmp::min;
 use std::fs::File;
 use std::io::{BufWriter, Write};
@@ -21,6 +21,18 @@ macro_rules! grab_symbol {
     };
 }
 
+// XX: This could be generic on arbitrary <T> if we could specify T:: implements from_le_bytes,
+// but we can't.
+fn read_symbol_maybe(elf: &ElfFile, symbol_name: &str) -> Option<u64> {
+    let (addr, size) = elf.find_symbol(symbol_name).ok()?;
+
+    let symbol_bytes = elf.get_data(addr, size)?;
+
+    assert!(mem::size_of::<u64>() == symbol_bytes.len());
+
+    Some(u64::from_le_bytes(symbol_bytes.try_into().ok()?))
+}
+
 macro_rules! write_symbol {
     ($loader_image: expr, $image_vaddr: expr, $elf: expr, $symbol: literal, $symbol_var: expr) => {
         let (addr, size) = grab_symbol!($elf, $symbol);
@@ -147,7 +159,7 @@ pub mod aarch64 {
         let shareability = if attr_index == s1_mair_attr_index::MT_NORMAL {
             // Match what the seL4 kernel uses for its page tables, which
             // is especially necessary for SMP booting which relies on it
-            // for coherency.
+            // for coherency. See the comment in seL4 `release_secondary_cpus()`.
             shareability_attributes::INNER_SHAREABLE
         } else {
             // Per $R_{PYFVQ}$:
@@ -922,35 +934,8 @@ impl<'a> Loader<'a> {
     ///       |             |
     ///     1 +-------------+                 (512 GiB)
     ///       | Level 1 Lwr | ---------->  +-- Level 1 --+
-    ///     0 +-------------+              |             |
-    ///                                    |   (empty)   |
-    ///                                    |             |
-    ///                                u+1 +-------------+             +-------------+
-    ///                                    |  uart_base  | ----------> | 1 GiB block |
-    ///                                  u +-------------+             +-------------+
-    ///                                    |             |
-    ///                                    |   (empty)   |
-    ///                                    |             |
-    ///                               i+1  +-------------+                 (1 GiB)
-    ///                                    | Level 2 Lwr | ----------> +-- Level 2 --+
-    ///                                 i  +-------------+             |             |
-    ///                                    |             |             |   (empty)   |
-    ///                                    |   (empty)   |             |             |
-    ///                                    |             |           t +-------------+             +-------------+
-    ///                                    +-------------+             |             | ----------> | 2 MiB block |
-    ///                                                                |-------------|             +-------------+
-    ///                                                                |             | ----------> | 2 MiB block |
-    ///                                                                |-------------|             +-------------+
-    ///                                                Loader Regions       (...)         (...)         (...)
-    ///                                                                |-------------|             +-------------+
-    ///                                                                |             | ----------> | 2 MiB block |
-    ///                                                                |-------------|             +-------------+
-    ///                                                                |             | ----------> | 2 MiB block |
-    ///                                                              s +-------------+             +-------------+
-    ///                                                                |             |
-    ///                                                                |   (empty)   |
-    ///                                                                |             |
-    ///                                                                +-------------+
+    ///     0 +-------------+              TODO: RAM.
+    ///
     ///
     /// Where:
     ///      k = align_down(kernel_first_vaddr, 512GiB),
@@ -958,9 +943,6 @@ impl<'a> Loader<'a> {
     ///      m = align_down(kernel_first_vaddr, 2MiB),
     ///      p = align_down(kernel_first_paddr, 2MiB),
     ///      u = align_down(uart_base, 1GiB),
-    ///      i = align_down(loader_start_addr, 1GiB),
-    ///      s = align_down(loader_start_addr, 2MiB),
-    ///      t = align_up(loader_end_addr, 2MiB),
     /// ```
     ///
     fn aarch64_setup_pagetables(
@@ -1004,20 +986,49 @@ impl<'a> Loader<'a> {
             }
         };
 
-        let (loader_start_addr, _) = grab_symbol!(elf, "_loader_start");
-        let (loader_end_addr, _) = grab_symbol!(elf, "_loader_end");
-        if lvl1_index(loader_start_addr) != lvl1_index(loader_end_addr) {
-            panic!("We only map 1GiB, but loader paddr range covers multiple GiB");
-        }
+        let identity_mapped_regions = {
+            let ram_regions = config
+                .normal_regions
+                .as_ref()
+                .expect("AArch64 should have normal_regions");
+
+            // println!("{:#x?}", ram_regions);
+
+            let mut regions: Vec<_> = ram_regions
+                .iter()
+                .cloned()
+                .map(|region| (region, MT_DEVICE_nGnRnE))
+                .collect();
+
+            // FIXME: Derive from the kernel build system.
+            if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
+                let uart_base = align_down(uart_base, PAGE_BITS_4KB);
+                regions.push((
+                    PlatformConfigRegion {
+                        start: uart_base,
+                        end: uart_base + (1 << PAGE_BITS_4KB),
+                    },
+                    MT_DEVICE_nGnRnE,
+                ));
+            }
+
+            // FIXME: This is currently assuming implementation details of the BCM2711/
+            //        Raspberry Pi 4B spin table implementation, as it is the only
+            //        platform we have that uses spin tables. Specifically, that
+            //        it is always located at the 0 page.
+            if elf.find_symbol("cpus_release_addr").is_ok() {
+                regions.push((
+                    PlatformConfigRegion {
+                        start: 0x0,
+                        end: 1 << PAGE_BITS_4KB,
+                    },
+                    MT_DEVICE_nGnRnE,
+                ));
+            }
 
-        let uart_base = if let Ok((uart_addr, uart_addr_size)) = elf.find_symbol("uart_addr") {
-            let data = elf
-                .get_data(uart_addr, uart_addr_size)
-                .expect("uart_addr not initialized");
+            regions.sort_by_key(|(region, _)| region.start);
 
-            Some(u64::from_le_bytes(data[0..8].try_into().unwrap()))
-        } else {
-            None
+            regions
         };
 
         // Manufacture the constants as per the diagram.
@@ -1025,10 +1036,6 @@ impl<'a> Loader<'a> {
         let l = align_down(kernel_first_vaddr, BLOCK_BITS_1GB);
         let m = align_down(kernel_first_vaddr, BLOCK_BITS_2MB);
         let p = align_down(kernel_first_paddr, BLOCK_BITS_2MB);
-        let i = align_down(loader_start_addr, BLOCK_BITS_1GB);
-        let u = uart_base.map(|addr| align_down(addr, BLOCK_BITS_1GB));
-        let s = align_down(loader_start_addr, BLOCK_BITS_2MB);
-        let t = align_up(loader_end_addr, BLOCK_BITS_2MB);
 
         // Manufacture the kernel page tables, which is relatively straightforward.
         let kernel_lvl1_pt_paddr = {
@@ -1055,46 +1062,291 @@ impl<'a> Loader<'a> {
             serialise_page_table_to_paddr(&mut lvl1_pt_kernel)
         };
 
-        // Manufacture the loader page tables.
-        let loader_lvl1_pt_paddr = {
-            // First, the Level 2 Lwr table
-            let lvl2_pt_paddr = {
-                let mut lvl2_pt_loader = [0u64; PAGE_TABLE_ENTRIES];
+        // Manufacture the RAM page tables, which is a little bit more complicated.
+        // We assume that normal RAM lies between 0 <= paddr < 512GiB, i.e.
+        // that lvl0_index(any ram region addr) = 0.
+        let ram_lvl1_pt_paddr = {
+            // Validation of assumptions about the identity mapped regions.
+            let mut previous_end = None;
+            for (region, _) in identity_mapped_regions.iter() {
+                assert!(lvl0_index(region.start) == 0);
+                assert!(lvl0_index(region.end - 1) == 0);
+                // This is probably an unnecessary assumption.
+                assert!(region.start.is_multiple_of(4096));
+                assert!(region.end.is_multiple_of(4096));
+                // This is definitely necessary.
+                assert!(region.start >= previous_end.unwrap_or(0));
+                previous_end = Some(region.end);
+            }
+
+            // We maintain three active page tables, which contain our previous
+            // known page table data. As we process regions in ascending order,
+            // once we have exceeded the bounds of the current reservation we
+            // can simply push to the page_table_bytes storage and insert into
+            // the parent PT the descriptor.
+            // When the current vaddr (/paddr, as identity mapped) exceeds the
+            // top value we rotate to a new PT.
+
+            let mut lvl1_pt = [0u64; PAGE_TABLE_ENTRIES];
+            let mut lvl2_pt = [0u64; PAGE_TABLE_ENTRIES];
+            let mut lvl3_pt = [0u64; PAGE_TABLE_ENTRIES];
+            // TODO: These should be defines. Note that the top is the size of 1 level of the next level up.
+            // TODO: LVL1_ENTRY_RANGE? idk
+            #[allow(unused_mut)]
+            let mut lvl1_vaddr_top = 1 << BLOCK_BITS_512GB;
+            let mut lvl2_vaddr_top = 1 << BLOCK_BITS_1GB;
+            let mut lvl3_vaddr_top = 1 << BLOCK_BITS_2MB;
+
+            // TODO: Tests...
+            // This is similar to aligned_power_of_two_regions() for the kernel UT,
+            // but we restrict it such that the output always is either 1GB, 2MB, or 4KB
+            // pages.
+
+            // Allowed externally for the final iteration
+            let mut base = 0u64;
+            for &(ref region, attr_index) in identity_mapped_regions.iter() {
+                // println!("RAM Region: {:#x}..{:#x}", base, region.end);
+                // println!(
+                //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
+                //     (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
+                //     lvl1_vaddr_top,
+                //     lvl1_pt.iter().filter(|&&v| v != 0).count()
+                // );
+                // println!(
+                //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
+                //     (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)),
+                //     lvl2_vaddr_top,
+                //     lvl2_pt.iter().filter(|&&v| v != 0).count()
+                // );
+                // println!(
+                //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
+                //     (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
+                //     lvl3_vaddr_top,
+                //     lvl3_pt.iter().filter(|&&v| v != 0).count()
+                // );
+
+                // Handle the fact that the regions are not contiguous and that
+                // we might need to skip PT.
+
+                {
+                    if region.start >= lvl3_vaddr_top {
+                        if lvl3_pt != [0; _] {
+                            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
+                            // println!("[iter] Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
+                            assert!(lvl2_pt[lvl2_index(base)] == 0);
+                            lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+                        }
+
+                        // TODO: just compute it.
+                        while region.start >= lvl3_vaddr_top {
+                            lvl3_vaddr_top += 1 << BLOCK_BITS_2MB;
+                        }
+                    }
 
-                // Identity mapped: vaddr == paddr.
-                let mut addr = s;
-                while addr < t {
-                    lvl2_pt_loader[lvl2_index(addr)] = block_descriptor(2, addr, MT_DEVICE_nGnRnE);
+                    if region.start >= lvl2_vaddr_top {
+                        if lvl2_pt != [0; _] {
+                            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+                            // println!("[iter] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+                            assert!(lvl1_pt[lvl1_index(base)] == 0);
+                            lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+                        }
+
+                        // TODO: just compute it.
+                        while region.start >= lvl2_vaddr_top {
+                            lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
+                        }
+                    }
 
-                    addr += 1 << BLOCK_BITS_2MB;
+                    if region.start >= lvl1_vaddr_top {
+                        unreachable!(
+                            "impossible as everything should fit here: {lvl1_vaddr_top:#x}"
+                        );
+                    }
                 }
 
-                // TODO: this is a complete hack specific to BCM2711/Raspberry Pi 4B and
-                // will be reworked with patches that re-do this loader mapping code.
-                if elf.find_symbol("cpus_release_addr").is_ok() {
-                    // Make sure we don't override the loader mappings done above;
-                    // and that this is located at 0x0.
-                    assert!(s != 0);
-                    assert!(i == 0);
+                // After serialising the old base, update the new one.
+                base = region.start;
+
+                // Inner Loop:
+                // Invariant: the page tables in lvl1_pt, lvl2_pt, lvl3_pt
+                //            are either (1) for the current address range,
+                //            or (2) are empty and for a lower level than the current level.
+                //            Also, the values in lvlXXX_vaddr_top are always correct (even if empty)
+                //            Also contiguous within the loop.
+                // Loop entry: (1) holds by work at the start of each region
+                while base != region.end {
+                    // Condition is !=, but assert that we never skip it.
+                    assert!(base < region.end);
+
+                    let size_bits = region.end.wrapping_sub(base).ilog2();
+                    let align_bits = min(
+                        size_bits,
+                        // FIXME: Once MSRV is > 1.97, use .lowest_one() method.
+                        if base == 0 {
+                            size_bits
+                        } else {
+                            base.trailing_zeros()
+                        },
+                    );
+
+                    // Match the size and alignment of the current region to
+                    // the valid PT region sizes.
+                    let (level, bits) = match u64::from(align_bits) {
+                        BLOCK_BITS_1GB.. => (1, BLOCK_BITS_1GB),
+                        BLOCK_BITS_2MB.. => (2, BLOCK_BITS_2MB),
+                        PAGE_BITS_4KB.. => (3, PAGE_BITS_4KB),
+                        0.. => panic!("impossible; regions should be aligned to 4K at least"),
+                    };
+
+                    let pt_region_size = 1u64 << bits;
+                    let top = base + pt_region_size;
+
+                    // println!("- Aligned PT region: {:#x}..{:#x} (size_bits: {}, align_bits: {}, bits: {})", base, top, size_bits, align_bits, bits);
+                    // println!(
+                    //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
+                    //     (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
+                    //     lvl1_vaddr_top,
+                    //     lvl1_pt.iter().filter(|&&v| v != 0).count()
+                    // );
+                    // println!(
+                    //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
+                    //     (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)),
+                    //     lvl2_vaddr_top,
+                    //     lvl2_pt.iter().filter(|&&v| v != 0).count()
+                    // );
+                    // println!(
+                    //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
+                    //     (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
+                    //     lvl3_vaddr_top,
+                    //     lvl3_pt.iter().filter(|&&v| v != 0).count()
+                    // );
+
+                    match level {
+                        1 => {
+                            // If it belongs in Level 1 PT, then it must go in
+                            // lvl1 pt. By the inavariant, base < lvl1_vaddr_top.
+                            assert!(base < lvl1_vaddr_top);
+                            // top is <= lvl1_vaddr_top (the case where it is the topmost entry)
+                            assert!(top <= lvl1_vaddr_top);
+
+                            assert!(lvl1_pt[lvl1_index(base)] == 0);
+                            lvl1_pt[lvl1_index(base)] = block_descriptor(1, base, attr_index);
+
+                            if top == lvl1_vaddr_top {
+                                // Invariant maintenance: if the new top would be now equal
+                                // the end of the page table's region top, we need a new
+                                // page table object and add it to the list.
+
+                                // This should be possible to handle - we just need to break out of this loop
+                                todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
+                            }
+
+                            // Invariant: Lower levels are empty.
+                            assert!(lvl2_pt == [0; _]);
+                            assert!(lvl3_pt == [0; _]);
+                            // Invariant maintenance: vaddr_top is right range for current PT.
+                            // it's empty so we need to increment the top to be current top (1G aligned) + 2MIB (512 lvl3 entries)
+                            lvl3_vaddr_top = top + (1 << BLOCK_BITS_2MB);
+                            // it's empty so we need to increment the top to be current top (1G aligned) + 1G (512 lvl2 entries)
+                            lvl2_vaddr_top = top + (1 << BLOCK_BITS_1GB);
+                        }
+                        2 => {
+                            // If it is a 2MiB block, it must go in the Level 2 PT;
+                            // by our invariants: base < lvl2_vaddr_top and top <= lvl2_vaddr_top
+                            assert!(base < lvl2_vaddr_top);
+                            assert!(top <= lvl2_vaddr_top);
+
+                            assert!(lvl2_pt[lvl2_index(base)] == 0);
+                            lvl2_pt[lvl2_index(base)] = block_descriptor(2, base, attr_index);
+
+                            if top == lvl2_vaddr_top {
+                                // Invariant maintenance: keep for current address range.
+                                // As we're the top of the range, we can serialise the table.
+
+                                let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+                                // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} up to {lvl2_vaddr_top:#x}");
+                                lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
+
+                                lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+
+                                if top == lvl1_vaddr_top {
+                                    todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
+                                }
+                            }
+
+                            // Invariant: Lower levels are empty.
+                            assert!(lvl3_pt == [0; _]);
+                            // Invariant maintenance: vaddr_top is right range for current PT.
+                            // it's empty so we need to increment the top to be current top (2MIB aligned) + 2MIB (512 lvl3 entries)
+                            lvl3_vaddr_top = top + (1 << BLOCK_BITS_2MB);
+                        }
+                        3 => {
+                            // If it is a 4K page, it must go in the Level 3 PT;
+                            // by our invariants: base < lvl3_vaddr_top and top <= lvl3_vaddr_top
+                            assert!(base < lvl3_vaddr_top);
+                            assert!(top <= lvl3_vaddr_top);
+
+                            assert!(lvl3_pt[lvl3_index(base)] == 0);
+                            lvl3_pt[lvl3_index(base)] = page_descriptor(base, attr_index);
+
+                            if top == lvl3_vaddr_top {
+                                // Invariant maintenance: keep for current address range.
+                                // As we're the top of the range, we can serialise the table.
+
+                                let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
+                                // println!("Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
+                                lvl3_vaddr_top += 1 << BLOCK_BITS_2MB;
+
+                                assert!(lvl2_pt[lvl2_index(base)] == 0);
+                                lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+
+                                if top == lvl2_vaddr_top {
+                                    let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+                                    // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)));
+                                    lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
+
+                                    assert!(lvl1_pt[lvl1_index(base)] == 0);
+                                    lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+
+                                    if top == lvl1_vaddr_top {
+                                        todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
+                                    }
+                                }
+                            }
+
+                            // Invariant: lower levels empty is vacuuously true
+                        }
+                        _ => unreachable!("level is 1..=3"),
+                    }
 
-                    lvl2_pt_loader[lvl2_index(0)] = block_descriptor(2, 0, MT_DEVICE_nGnRnE);
+                    base = base + pt_region_size;
                 }
+            }
 
-                serialise_page_table_to_paddr(&mut lvl2_pt_loader)
-            };
+            // By the loop invariant, we know that anything before has been serialised.
+            // However, as we are at the end of the loop now, we might have
+            // page tables that have been partially filled out, and we need to
+            // serialise these.
 
-            // Then, the Level 1 Lwr table.
-            let mut lvl1_pt_loader = [0u64; PAGE_TABLE_ENTRIES];
-            lvl1_pt_loader[lvl1_index(i)] = table_descriptor(lvl2_pt_paddr);
+            if lvl3_pt != [0; _] {
+                let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
+                // println!("[end] Serialise lvl3 table: {lvl3_pt_paddr:#x}");
+                assert!(lvl2_pt[lvl2_index(base)] == 0);
+                lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+            }
 
-            // map optional UART MMIO in l1 1GB page, only available if CONFIG_PRINTING
-            if let Some(u) = u {
-                // UART no overlap with Loader.
-                assert!(lvl1_index(i) != lvl1_index(u));
-                lvl1_pt_loader[lvl1_index(u)] = block_descriptor(1, u, MT_DEVICE_nGnRnE);
+            if lvl2_pt != [0; _] {
+                let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+                // println!("[end] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+                assert!(lvl1_pt[lvl1_index(base)] == 0);
+                lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
             }
 
-            serialise_page_table_to_paddr(&mut lvl1_pt_loader)
+            // the level1 pt should not be empty. lol.
+            assert!(lvl1_pt != [0; _]);
+
+            // println!("New lvl1 table");
+            serialise_page_table_to_paddr(&mut lvl1_pt)
         };
 
         // Depending on whether we are in hypervisor mode, we either need to
@@ -1107,8 +1359,9 @@ impl<'a> Loader<'a> {
 
             let mut ttbr0_el2_pt = [0u64; PAGE_TABLE_ENTRIES];
 
+            assert!(lvl0_index(k) != lvl0_index(0));
             ttbr0_el2_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
-            ttbr0_el2_pt[lvl0_index(0)] = table_descriptor(loader_lvl1_pt_paddr);
+            ttbr0_el2_pt[lvl0_index(0)] = table_descriptor(ram_lvl1_pt_paddr);
 
             let ttbr0_el2 = serialise_page_table_to_paddr(&mut ttbr0_el2_pt);
 
@@ -1119,8 +1372,8 @@ impl<'a> Loader<'a> {
 
             // Kernel in TTBR1 (Upper)
             ttbr1_el1_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
-            // Loader in TTBR0 (Lower)
-            ttbr0_el1_pt[lvl0_index(k)] = table_descriptor(loader_lvl1_pt_paddr);
+            // Identity-mapped RAM in TTBR0 (Lower)
+            ttbr0_el1_pt[lvl0_index(0)] = table_descriptor(ram_lvl1_pt_paddr);
 
             let ttbr0_el1 = serialise_page_table_to_paddr(&mut ttbr0_el1_pt);
             let ttbr1_el1 = serialise_page_table_to_paddr(&mut ttbr1_el1_pt);
diff --git a/tool/microkit/src/sel4.rs b/tool/microkit/src/sel4.rs
index 2c30309bd..ead67bb04 100644
--- a/tool/microkit/src/sel4.rs
+++ b/tool/microkit/src/sel4.rs
@@ -249,7 +249,7 @@ pub fn emulate_kernel_boot(
     }
 }
 
-#[derive(Deserialize, Debug)]
+#[derive(Deserialize, Debug, Clone)]
 pub struct PlatformConfigRegion {
     pub start: u64,
     pub end: u64,

From 5417be07f78a8e4a2ad5de6d5be533957b1e3945 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Tue, 28 Jul 2026 11:00:01 +1000
Subject: [PATCH 05/16] loader: gc-sections

Useful for rust.

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/Makefile   |  6 ++++--
 loader/aarch64.ld |  7 ++++++-
 loader/riscv64.ld | 13 +++++++++----
 3 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/loader/Makefile b/loader/Makefile
index c08c18bd9..2811fd8f9 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -50,7 +50,7 @@ endif
 CFLAGS := -std=gnu11 -g -O3 -nostdlib -ffreestanding \
 					-MP -MD $(CFLAGS_ARCH) -DBOARD_$(BOARD) -I$(SEL4_SDK)/include \
 					-Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wmissing-declarations \
-					-Wundef -Wno-nonnull -Wnested-externs
+					-Wundef -Wno-nonnull -Wnested-externs -ffunction-sections -fdata-sections
 
 ASM_FLAGS := $(ASM_FLAGS_ARCH) -g -MP -MD -I$(SEL4_SDK)/include
 
@@ -89,5 +89,7 @@ all: $(OBJPROG)
 $(LINKSCRIPT): $(LINKSCRIPT_INPUT)
 	$(CPP) -DLINK_ADDRESS=$(LINK_ADDRESS) $< | grep -v "^#" > $@
 
+LDFLAGS := -T$(LINKSCRIPT) --gc-sections
+
 $(OBJPROG): $(addprefix $(BUILD_DIR)/, $(OBJECTS)) $(LINKSCRIPT)
-	$(LD) -T$(LINKSCRIPT) $(addprefix $(BUILD_DIR)/, $(OBJECTS)) -o $@
+	$(LD) $(LDFLAGS) $(addprefix $(BUILD_DIR)/, $(OBJECTS)) -o $@
diff --git a/loader/aarch64.ld b/loader/aarch64.ld
index 977ccc574..34636e9e4 100644
--- a/loader/aarch64.ld
+++ b/loader/aarch64.ld
@@ -17,9 +17,11 @@ SECTIONS
     .text :
     {
         _text = .;
-        *(.text.start)
+        KEEP(*(.text.start))
         *(.text*)
+        *(.text.*)
         *(.rodata)
+        *(.rodata.*)
         _text_end = .;
     } :all
 
@@ -27,6 +29,8 @@ SECTIONS
     {
         _data = .;
         *(.data)
+        *(.data.*)
+        KEEP(*(.data.uart_addr))
         _data_end = .;
     } :all
 
@@ -34,6 +38,7 @@ SECTIONS
     {
         _bss = .;
         *(.bss)
+        *(.bss.*)
         *(COMMON)
         . = ALIGN(4);
         _bss_end = .;
diff --git a/loader/riscv64.ld b/loader/riscv64.ld
index f7ae1240e..fe98d7450 100644
--- a/loader/riscv64.ld
+++ b/loader/riscv64.ld
@@ -15,9 +15,11 @@ SECTIONS
     .text :
     {
         _text = .;
-        *(.text.start)
+        KEEP(*(.text.start))
         *(.text*)
+        *(.text.*)
         *(.rodata)
+        *(.rodata.*)
         _text_end = .;
     } :all
 
@@ -25,17 +27,20 @@ SECTIONS
     {
         _data = .;
         *(.data)
+        *(.data.*)
         __global_pointer$ = . + 0x800;
-    *(.srodata)
-    *(.sdata)
+        *(.srodata)
+        *(.sdata)
+        KEEP(*(.data.uart_addr))
        _data_end = .;
     } :all
 
     .bss :
     {
         _bss = .;
-    *(.sbss)
+        *(.sbss)
         *(.bss)
+        *(.bss.*)
         *(COMMON)
         . = ALIGN(4);
         _bss_end = .;

From 0557f16ab54b9a60e9202fb105d94cd75946b5e1 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Wed, 29 Jul 2026 15:26:32 +1000
Subject: [PATCH 06/16] move the stuff to runtime (but it breaks it!! need
 fix!!)

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/Makefile             |   23 +-
 loader/aarch64.ld           |   24 +-
 loader/src/aarch64/mmu.c    |   15 +
 loader/src/loader.c         |    1 -
 loader/src/loader.h         |    2 +-
 loader/src/page_tables.rs   | 1090 +++++++++++++++++++++++++++++++++++
 tool/microkit/src/loader.rs | 1083 +---------------------------------
 7 files changed, 1150 insertions(+), 1088 deletions(-)
 create mode 100644 loader/src/page_tables.rs

diff --git a/loader/Makefile b/loader/Makefile
index 2811fd8f9..dd78ce5d9 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -35,15 +35,19 @@ else
   LD = $(TARGET_TRIPLE)-ld
 endif
 
+RUSTC := rustc
+
 ifeq ($(ARCH),aarch64)
 	CFLAGS_AARCH64 := -mcpu=$(GCC_CPU) -mgeneral-regs-only -mstrict-align -mno-outline-atomics
 	CFLAGS_ARCH := $(CFLAGS_AARCH64) -DARCH_aarch64
 	ASM_FLAGS_ARCH := -mcpu=$(GCC_CPU)
 	ARCH_DIR := aarch64
+	RUST_TARGET_TRIPLE := aarch64-unknown-none
 else ifeq ($(ARCH),riscv64)
 	CFLAGS_RISCV64 := -mcmodel=medany -march=rv64imac_zicsr_zifencei -mabi=lp64
 	CFLAGS_ARCH := $(CFLAGS_RISCV64) -DARCH_riscv64
 	ASM_FLAGS_ARCH := -march=rv64imac_zicsr_zifencei -mabi=lp64
+	RUST_TARGET_TRIPLE := riscv64gc-unknown-none-elf
 	ARCH_DIR := riscv
 endif
 
@@ -54,8 +58,10 @@ CFLAGS := -std=gnu11 -g -O3 -nostdlib -ffreestanding \
 
 ASM_FLAGS := $(ASM_FLAGS_ARCH) -g -MP -MD -I$(SEL4_SDK)/include
 
+RUSTFLAGS := --target $(RUST_TARGET_TRIPLE) --edition 2024 -g -C opt-level=2
+
 PROGS := loader.elf
-OBJECTS := loader.o crt0.o uart.o cutil.o
+OBJECTS := loader.o crt0.o uart.o cutil.o libpage_tables.a
 
 ifeq ($(ARCH),aarch64)
 	OBJECTS += util64.o el.o exceptions.o init.o mmu.o cpus.o
@@ -80,7 +86,19 @@ $(BUILD_DIR)/%.o : src/$(ARCH_DIR)/%.c
 $(BUILD_DIR)/%.o : src/%.c
 	$(CC) -c $(CFLAGS) $< -o $@
 
+# Note: having multiple rlib with staticlib will give duplicate linker symbol
+# issues. Use "--crate-type rlib" instead, but then we need to link a single
+# copy of the rust corelibs.
+$(BUILD_DIR)/lib%.a : src/%.rs
+	$(RUSTC) $(RUSTFLAGS) \
+		--emit dep-info,metadata,link \
+		--out-dir $(BUILD_DIR) -L dependency=$(BUILD_DIR) \
+		--crate-type staticlib \
+		--crate-name $(patsubst lib%.a,%,$(notdir $@)) \
+		$<
+
 -include $(BUILD_DIR)/*.d
+-include $(BUILD_DIR)/mmu.d
 
 OBJPROG = $(addprefix $(BUILD_DIR)/, $(PROGS))
 
@@ -92,4 +110,5 @@ $(LINKSCRIPT): $(LINKSCRIPT_INPUT)
 LDFLAGS := -T$(LINKSCRIPT) --gc-sections
 
 $(OBJPROG): $(addprefix $(BUILD_DIR)/, $(OBJECTS)) $(LINKSCRIPT)
-	$(LD) $(LDFLAGS) $(addprefix $(BUILD_DIR)/, $(OBJECTS)) -o $@
+	$(LD) $(LDFLAGS) --start-group $(addprefix $(BUILD_DIR)/, $(OBJECTS)) --end-group -o $@
+
diff --git a/loader/aarch64.ld b/loader/aarch64.ld
index 34636e9e4..2454398a3 100644
--- a/loader/aarch64.ld
+++ b/loader/aarch64.ld
@@ -8,6 +8,12 @@ PHDRS
     all PT_LOAD AT (LINK_ADDRESS);
 }
 
+
+//    text PT_LOAD FLAGS(5); /* RX */
+//    rodata PT_LOAD FLAGS(4); /* RO */
+//    data PT_LOAD FLAGS(6); /* RW */
+//    bss PT_LOAD FLAGS(6); /* RW */
+
 SECTIONS
 {
     . = LINK_ADDRESS;
@@ -17,20 +23,26 @@ SECTIONS
     .text :
     {
         _text = .;
+
         KEEP(*(.text.start))
-        *(.text*)
-        *(.text.*)
-        *(.rodata)
-        *(.rodata.*)
+        *(.text .text.*)
+
         _text_end = .;
     } :all
 
+    .rodata :
+    {
+        *(.rodata .rodata.* .rodata..Lanon.*)
+    } :all
+
     .data :
     {
         _data = .;
-        *(.data)
+        *(.data .data.*)
         *(.data.*)
+
         KEEP(*(.data.uart_addr))
+
         _data_end = .;
     } :all
 
@@ -44,5 +56,7 @@ SECTIONS
         _bss_end = .;
     } :all
 
+
+
     _loader_end = .;
 }
diff --git a/loader/src/aarch64/mmu.c b/loader/src/aarch64/mmu.c
index 39b4676c8..2fbdcc150 100644
--- a/loader/src/aarch64/mmu.c
+++ b/loader/src/aarch64/mmu.c
@@ -20,8 +20,23 @@ uint64_t aarch64_pt_ttbr0_el1;
 uint64_t aarch64_pt_ttbr1_el1;
 uint64_t aarch64_pt_ttbr0_el2;
 
+struct ret {
+    uint64_t a;
+    uint64_t b;
+    uint64_t c;
+};
+
+extern struct ret aarch64_setup_pagetables(uint64_t kernel_first_vaddr, uint64_t kernel_first_paddr, uint64_t page_tables_paddr_start);
+
 int arch_mmu_enable(int logical_cpu)
 {
+    puts("setup1\n");
+    struct ret x = aarch64_setup_pagetables(0, 0, 0);
+    aarch64_pt_ttbr0_el1 = x.a;
+    aarch64_pt_ttbr1_el1 = x.b;
+    aarch64_pt_ttbr0_el2 = x.c;
+    puts("setup\n");
+
     int r;
     enum el el;
     r = ensure_correct_el(logical_cpu);
diff --git a/loader/src/loader.c b/loader/src/loader.c
index 67c09b149..45a21de04 100644
--- a/loader/src/loader.c
+++ b/loader/src/loader.c
@@ -100,7 +100,6 @@ static int print_lock = 0;
 
 void start_kernel(int logical_cpu)
 {
-    LDR_PRINT("INFO", logical_cpu, "enabling MMU\n");
     int r = arch_mmu_enable(logical_cpu);
     if (r != 0) {
         LDR_PRINT("ERROR", logical_cpu, "failed to enable MMU: ");
diff --git a/loader/src/loader.h b/loader/src/loader.h
index c144381aa..d1a0e79d3 100644
--- a/loader/src/loader.h
+++ b/loader/src/loader.h
@@ -7,7 +7,7 @@
 
 #pragma once
 
-#define STACK_SIZE 4096
+#define STACK_SIZE 40960
 
 #define REGION_TYPE_DATA 1
 #define REGION_TYPE_ZERO 2
diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
new file mode 100644
index 000000000..31bcca1c9
--- /dev/null
+++ b/loader/src/page_tables.rs
@@ -0,0 +1,1090 @@
+//
+// Copyright 2026, UNSW
+//
+// SPDX-License-Identifier: BSD-2-Clause
+//
+
+#![no_std]
+
+use core::cmp::min;
+use core::ffi::c_char;
+use core::fmt;
+use core::fmt::Write;
+use core::mem;
+use core::panic::PanicInfo;
+
+unsafe extern "C" {
+    safe fn fail() -> !;
+    // safe fn putc(c: c_char);
+    unsafe fn puts(s: *const c_char);
+}
+
+#[panic_handler]
+fn panic(info: &PanicInfo) -> ! {
+    unsafe { puts(c"panicked\n".as_ptr()) };
+
+    struct DebugWriter;
+    impl fmt::Write for DebugWriter {
+        fn write_str(&mut self, s: &str) -> fmt::Result {
+            for c in s.bytes() {
+                unsafe {
+                    puts(core::ffi::CStr::from_bytes_with_nul_unchecked(&[c.into(), 0]).as_ptr())
+                };
+            }
+
+            Ok(())
+        }
+    }
+
+    if let Err(_) = writeln!(DebugWriter, "{}", info) {
+        // If writeln!() fails (which it should never as our fmt::Write) never
+        // fails, then just don't print the extra information.
+        unsafe { puts(c"panicked (information unknown)\n".as_ptr()) };
+    }
+
+    fail();
+}
+
+const PAGE_TABLE_SIZE: usize = 4096;
+
+const fn divmod(x: u64, y: u64) -> (u64, u64) {
+    (x / y, x % y)
+}
+
+const fn mask(n: u64) -> u64 {
+    (1 << n) - 1
+}
+
+const fn round_up(n: u64, x: u64) -> u64 {
+    let (_, m) = divmod(n, x);
+    if m == 0 {
+        n
+    } else {
+        n + x - m
+    }
+}
+
+const fn round_down(n: u64, x: u64) -> u64 {
+    let (_, m) = divmod(n, x);
+    if m == 0 {
+        n
+    } else {
+        n - m
+    }
+}
+
+const fn align_up(n: u64, bits: u64) -> u64 {
+    round_up(n, 1 << bits)
+}
+
+const fn align_down(n: u64, bits: u64) -> u64 {
+    round_down(n, 1 << bits)
+}
+
+unsafe extern "C" {
+    static mut _text: u8;
+}
+
+pub mod aarch64 {
+    //! For AArch64, our page tables use the Stage 1 descriptor formats
+    //! for both EL2 (TTBR0_EL2) and EL1 (TTBR0_EL1/TTBR1_EL1).
+    //! Stage 2 descriptors are only used when in the EL1&0 regime; which is not
+    //! the case when in EL2.
+
+    use crate::mask;
+
+    pub const LVL0_BITS: u64 = 9;
+    pub const LVL1_BITS: u64 = 9;
+    pub const LVL2_BITS: u64 = 9;
+    pub const LVL3_BITS: u64 = 9;
+
+    pub fn lvl0_index(addr: u64) -> usize {
+        let idx = (addr >> (BLOCK_BITS_2MB + LVL2_BITS + LVL1_BITS)) & mask(LVL0_BITS);
+        idx as usize
+    }
+
+    pub fn lvl1_index(addr: u64) -> usize {
+        let idx = (addr >> (BLOCK_BITS_2MB + LVL2_BITS)) & mask(LVL1_BITS);
+        idx as usize
+    }
+
+    pub fn lvl2_index(addr: u64) -> usize {
+        let idx = (addr >> (BLOCK_BITS_2MB)) & mask(LVL2_BITS);
+        idx as usize
+    }
+
+    pub fn lvl3_index(addr: u64) -> usize {
+        let idx = (addr >> PAGE_BITS_4KB) & mask(LVL3_BITS);
+        idx as usize
+    }
+
+    /// Stage 1 translation table page/block descriptors have bits[4:2] containing
+    /// AttrIndex[2:0]. The AttrIndex values depends on our configuration of
+    /// the `MAIR_EL1` or `MAIR_EL2` registers done in util64.S;
+    /// This also needs to match the values that seL4 uses.
+    #[allow(non_upper_case_globals, reason = "matching ARM naming convention")]
+    pub mod s1_mair_attr_index {
+        pub const MT_DEVICE_nGnRnE: u64 = 0b000;
+        pub const MT_DEVICE_nGnRE: u64 = 0b001;
+        pub const MT_DEVICE_GRE: u64 = 0b010;
+        pub const MT_NORMAL_NC: u64 = 0b011;
+        pub const MT_NORMAL: u64 = 0b100;
+    }
+
+    pub mod descriptor_type {
+        //! The translation table descriptor formats, as per §D8.3 "Translation
+        //! table descriptor formats" of ARM DDI 0487 L.b. Specifically,
+        //! as per "Table D8-48 Determination of descriptor type"
+
+        /// Descriptor type: Table. Condition is lookup level != 3.
+        pub const TABLE: u64 = 0b11;
+        /// Descriptor type: Page. Condition is lookup level == 3.
+        pub const PAGE: u64 = 0b11;
+        /// Descriptor type: Block. Condition is lookup level != 3.
+        pub const BLOCK: u64 = 0b01;
+        /// Descriptor type: Invalid. Strictly speaking bit[1] does not matter.
+        pub const INVALID: u64 = 0b00;
+    }
+
+    pub mod shareability_attributes {
+        //! Per §D8.6.2 "Stage 1 Shareability attributes", these contain the
+        //! shareability attributes of the descriptor OA for normal-cacheable
+        //! memory.
+
+        /// Non-shareable
+        pub const NON_SHAREABLE: u64 = 0b00;
+        /// Outer-shareable
+        pub const OUTER_SHAREABLE: u64 = 0b10;
+        /// Inner-shareable
+        pub const INNER_SHAREABLE: u64 = 0b11;
+    }
+
+    /// Per "Figure D8-14 VMSAv8-64 Block descriptor formats" of ARM DDI0487L.b,
+    /// subfigure "4KB, 16KB, and 64KB granules, 48-bit OA", the Output address
+    /// is bits [47:n], and:
+    ///
+    /// > For the 4KB granule size, the level 1 descriptor n is 30,
+    /// > and the level 2 descriptor n is 21.
+    pub const BLOCK_BITS_1GB: u64 = 30;
+
+    /// Per "Figure D8-14 VMSAv8-64 Block descriptor formats" of ARM DDI0487L.b,
+    /// subfigure "4KB, 16KB, and 64KB granules, 48-bit OA", the Output address
+    /// is bits [47:n], and:
+    ///
+    /// > For the 4KB granule size, the level 1 descriptor n is 30,
+    /// > and the level 2 descriptor n is 21.
+    pub const BLOCK_BITS_2MB: u64 = 21;
+
+    // TODO:
+
+    pub const BLOCK_BITS_512GB: u64 = 39;
+    pub const PAGE_BITS_4KB: u64 = 12;
+
+    /// Per "Table D8-52 Stage 1 VMSAv8-64 Block and Page descriptor fields" and
+    /// "Figure D8-14 VMSAv8-64 Block descriptor formats" of ARM DDI0487L.b;
+    /// specifically subfigure "4KB, 16KB, and 64KB granules, 48-bit OA"
+    pub fn block_descriptor(level: usize, addr: u64, attr_index: u64) -> u64 {
+        // Per Table D8-48, Condition for descriptor_type::BLOCK is level != 3.
+        assert!(level != 3);
+
+        let upper_attributes: u64 = 0;
+
+        let shareability = if attr_index == s1_mair_attr_index::MT_NORMAL {
+            // Match what the seL4 kernel uses for its page tables, which
+            // is especially necessary for SMP booting which relies on it
+            // for coherency. See the comment in seL4 `release_secondary_cpus()`.
+            shareability_attributes::INNER_SHAREABLE
+        } else {
+            // Per $R_{PYFVQ}$:
+            // > If a region is mapped as Device memory or Normal Non-cacheable
+            // > memory after all enabled translation stages, then the region
+            // > has an effective Shareability attribute of Outer Shareable.
+            //
+            // We override the value we place in here to OUTER_SHAREABLE to match
+            // how the hardware behaves. This is not necessary but for clarity.
+            shareability_attributes::OUTER_SHAREABLE
+        };
+
+        // AP[2:1], which we set as 0b00 for read/write access:
+        //   stage 1: 0b00 is {PrivRead, PrivWrite} and we are EL1
+        //   stage 2: 0b00 is RW for EL2 and no perms for EL1.
+        const AP_KERNEL_RW: u64 = 0b00;
+
+        // bit[11] is the not global (nG) field, we leave as 0 (global).
+        // bit[10] is the access flag; depending on FEAT_HAFDBS, when software
+        //         manages the AF memory accesses to the page/block when AF=0
+        //         raise an Access Fault; when hardware manages the AF it will
+        //         become 1.
+        // bit[9:8] is SH[1:0] containing stage 1 shareability attributes
+        // bit[7:6] contains AP[2:1]
+        // bit[5] is RES0
+        // bit[4:2] contains AttrIndex
+        let lower_attributes: u64 =
+            (1 << 10) | (AP_KERNEL_RW << 6) | (shareability << 8) | (attr_index << 2);
+
+        // bits[47:n]
+        let output_address: u64 = addr
+            & !mask(match level {
+                1 => BLOCK_BITS_1GB,
+                2 => BLOCK_BITS_2MB,
+                _ => panic!("unsupported level {level} for block descriptor"),
+            });
+
+        // address must not have bits above 47 set.
+        assert!(addr & mask(48) == addr);
+
+        // bits[63:50] describing the "Upper attributes" are left at 0.
+        // bits[49:48] are RES0
+        // bits[47:n] contain the Output address
+        // bits[n-1:12] are RES0
+        // bits[11:2] contain the "Lower attributes"
+        // bits[1:0] contains the descriptor type
+        upper_attributes | output_address | lower_attributes | descriptor_type::BLOCK
+    }
+
+    /// Per "Table D8-52 Stage 1 VMSAv8-64 Block and Page descriptor fields" and
+    /// "Figure D8-15 VMSAv8-64 Page descriptor formats" of ARM DDI0487L.b;
+    /// specifically subfigure "4KB granule 48-bit OA".
+    pub fn page_descriptor(addr: u64, attr_index: u64) -> u64 {
+        // The main difference between a page descriptor and block descriptor
+        // is in the size of the output address (OA) and in the descriptor type.
+
+        let upper_attributes: u64 = 0;
+
+        let shareability = if attr_index == s1_mair_attr_index::MT_NORMAL {
+            // Match what the seL4 kernel uses for its page tables, which
+            // is especially necessary for SMP booting which relies on it
+            // for coherency.
+            shareability_attributes::INNER_SHAREABLE
+        } else {
+            // Per $R_{PYFVQ}$:
+            // > If a region is mapped as Device memory or Normal Non-cacheable
+            // > memory after all enabled translation stages, then the region
+            // > has an effective Shareability attribute of Outer Shareable.
+            // We override the value we place in here to OUTER_SHAREABLE to match
+            // how the hardware behaves.
+            shareability_attributes::OUTER_SHAREABLE
+        };
+
+        // AP[2:1], which we set as 0b00 for read/write access:
+        //   stage 1: 0b00 is {PrivRead, PrivWrite} and we are EL1/El2 (priv)
+        const AP_KERNEL_RW: u64 = 0b00;
+
+        // bit[11] is the not global (nG) field, we leave as 0 (global).
+        // bit[10] is the access flag; depending on FEAT_HAFDBS, when software
+        //         manages the AF memory accesses to the page/block when AF=0
+        //         raise an Access Fault; when hardware manages the AF it will
+        //         become 1.
+        // bit[9:8] is SH[1:0] containing stage 1 shareability attributes
+        // bit[7:6] contains AP[2:1]
+        // bit[5] is RES0
+        // bit[4:2] contains AttrIndex
+        let lower_attributes: u64 =
+            (1 << 10) | (AP_KERNEL_RW << 6) | (shareability << 8) | (attr_index << 2);
+
+        // bits[47:12]
+        let output_address: u64 = addr & !mask(12);
+
+        // address must not have bits above 47 set.
+        assert!(addr & mask(48) == addr);
+
+        // bits[63:50] describing the "Upper attributes" are left at 0.
+        // bits[49:48] are RES0
+        // bits[47:12] contain the Output address
+        // bits[11:2] contain the "Lower attributes"
+        // bits[1:0] contains the descriptor type
+        upper_attributes | output_address | lower_attributes | descriptor_type::PAGE
+    }
+
+    /// Per "Table D8-50 Stage 1 VMSAv8-64 Table descriptor fields" and
+    /// "Figure D8-12 VMSAv8-64 Table descriptor formats" of ARM DDI0487L.b;
+    /// specifically subfigure "4KB, 16KB, and 64KB granules, 48-bit OA"
+    pub fn table_descriptor(addr: u64) -> u64 {
+        // Per Table D8-48, Condition for descriptor_type::TABLE is level != 3.
+
+        // We don't set any of these attributes, most are hardware-feature conditional
+        let attributes: u64 = 0;
+
+        // address must not have bits above 47 or below 12 set
+        assert!(addr & mask(12) == 0x0);
+        assert!(addr & mask(48) == addr);
+
+        let next_level_table_address = addr;
+
+        // bits[63:59] are "Attributes"
+        // bits[58:51] are ignored
+        // bits[50:48] are RES0
+        // bits[47:m] is the next-level table address
+        //  note: here m=12 for 4KB granule
+        // bits[m-1:12] are RES0
+        //  so this doesn't exist for 4KB granule
+        // bits[11:2] are ignored
+        // bits[1:0] contain the descriptor type
+        attributes | next_level_table_address | descriptor_type::TABLE
+    }
+}
+
+mod riscv64 {
+    pub(crate) const BLOCK_BITS_1GB: u64 = 30;
+    pub(crate) const BLOCK_BITS_2MB: u64 = 21;
+    pub(crate) const PAGE_BITS_4K: u64 = 12;
+
+    pub(crate) const PAGE_TABLE_INDEX_BITS: u64 = 9;
+    pub(crate) const PAGE_SHIFT: u64 = 12;
+    /// This sets the page table entry bits: D,A,X,W,R.
+    pub(crate) const PTE_TYPE_BITS: u64 = 0b11001110;
+    // TODO: where does this come from?
+    pub(crate) const PTE_TYPE_TABLE: u64 = 0;
+    pub(crate) const PTE_TYPE_VALID: u64 = 1;
+
+    pub(crate) const PTE_PPN0_SHIFT: u64 = 10;
+
+    /// Due to RISC-V having various virtual memory setups, we have this generic function to
+    /// figure out the page-table index given the total number of page table levels for the
+    /// platform and which level we are currently looking at.
+    pub fn pt_index(pt_levels: usize, addr: u64, level: usize) -> usize {
+        let pt_index_bits = PAGE_TABLE_INDEX_BITS * (pt_levels - level) as u64;
+        let idx = (addr >> (pt_index_bits + PAGE_SHIFT)) % 512;
+
+        idx as usize
+    }
+
+    /// Generate physical page number given an address
+    pub fn pte_ppn(addr: u64) -> u64 {
+        (addr >> PAGE_SHIFT) << PTE_PPN0_SHIFT
+    }
+
+    pub fn pte_next(addr: u64) -> u64 {
+        pte_ppn(addr) | PTE_TYPE_TABLE | PTE_TYPE_VALID
+    }
+
+    pub fn pte_leaf(addr: u64) -> u64 {
+        pte_ppn(addr) | PTE_TYPE_BITS | PTE_TYPE_VALID
+    }
+}
+
+/// RISC-V 64 page tables for our purposes uses the Sv39 translation scheme
+/// (3-level page tables).
+///
+/// It is split into two halves: the Upper/Kernel part of the page tables,
+/// which matches the format seL4 expects. The lower half contains an
+/// identity mapped region for the loader.
+///
+/// ```txt
+///            (512 GiB)
+///   512 +---- Level 1 ---+ 2^39
+///       |                |
+///       |     (empty)    |
+///       |                |
+///   k+1 +----------------+                   (1 GiB)
+///       | Level 2 Kernel | ----------> +---- Level 2 ---+             +-------------+
+///     k +----------------+             |                | ----------> | 2 MiB block |
+///       |                |         511 |----------------|             +-------------+
+///       |                |             |                | ----------> | 2 MiB block |
+///       |                |         510 |----------------|             +-------------+
+///       |                |             |                | ----------> | 2 MiB block |
+///       |                |             |----------------|             +-------------
+///       |                |                   (...)           (...)         (...)          Kernel Regions
+///       |                |             |----------------|             +-------------+
+///       |                |             |                | ----------> | 2 MiB block |
+///       |                |         l+1 |----------------|             +-------------+
+///       |                |             | Level 3 Kernel | ----+
+///       |                |           l |----------------|     |
+///       |                |             |                |     |           (2 MiB)
+///       |                |             |                |     +-----> +-- Level 3 --+             +------------+
+///       |                |             |                |             |             | ----------> | 4 KiB page |
+///       |                |             |                |         511 |-------------|             +------------+
+///       |                |             |     (empty)    |             |             | ----------> | 4 KiB page |
+///       |     (empty)    |             |                |             |-------------|             +------------+
+///       |                |             |                |             |             | ----------> | 4 KiB page |
+///       |                |             |                |           m |-------------|             +------------+ p
+///       |                |             |                |             |   (empty)   |
+///       |                |             |                |             +-------------+
+///       |                |             |                |
+///       |                |           0 +----------------+
+///       |                |
+///       |                |
+///       |                |
+///       |                |
+///       |                |
+///   s+1 +----------------+                  (1 GiB)
+///       | Level 2 Loader | ---------->  +-- Level 2 --+             +-------------+
+///     s +----------------+              |             | ----------> | 2 MiB block |
+///       |                |          511 +-------------+             +-------------+
+///       |                |              |             | ----------> | 2 MiB block |
+///       |    (empty)     |          510 +-------------+             +-------------+
+///       |                |              |             | ----------> | 2 MiB block |
+///       |                |              |-------------|             +-------------+
+///     0 +----------------+              |             | ----------> | 2 MiB block |
+///                                       |-------------|             +-------------+
+///                                            (...)         (...)         (...)          Loader Regions
+///                                       |-------------|             +-------------+
+///                                       |             | ----------> | 2 MiB block |
+///                                       |-------------|             +-------------+
+///                                       |             | ----------> | 2 MiB block |
+///                                     t +-------------+             +-------------+
+///                                       |             |
+///                                       |   (empty)   |
+///                                       |             |
+///                                       +-------------+
+///
+///
+/// Where:
+///      k = align_down(kernel_first_vaddr, 1GiB),
+///      l = align_down(kernel_first_vaddr, 2MiB),
+///      m = align_down(kernel_first_vaddr, 4KiB),
+///      p = align_down(kernel_first_paddr, 4KiB),
+///
+///      s = align_down(text_addr, 1GiB),
+///      t = align_down(text_addr, 2MiB),
+/// ```
+///
+#[unsafe(no_mangle)]
+pub extern "C" fn riscv64_setup_pagetables(
+    kernel_first_vaddr: u64,
+    kernel_first_paddr: u64,
+    page_tables_paddr_start: u64,
+) -> u64 {
+    use riscv64::{pt_index, pte_leaf, pte_next, BLOCK_BITS_1GB, BLOCK_BITS_2MB, PAGE_BITS_4K};
+
+    let text_addr = &raw const _text as u64;
+
+    // We map the loader using 2MB pages, so make sure the base is actually aligned.
+    assert!(text_addr.is_multiple_of(1 << BLOCK_BITS_2MB));
+
+    const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
+
+    let mut serialise_page_table_to_paddr = {
+        assert!(
+            page_tables_paddr_start
+                == page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64)
+        );
+
+        // This maintains the current end of the PT array.
+        let mut next_pt_paddr = page_tables_paddr_start;
+
+        move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
+            let pt_paddr = next_pt_paddr;
+            // page_table_bytes.extend(page_table.iter().flat_map(|pte| pte.to_le_bytes()));
+            next_pt_paddr += PAGE_TABLE_SIZE as u64;
+            page_table.fill(0);
+            pt_paddr
+        }
+    };
+
+    struct Config {
+        riscv_pt_levels: usize,
+    }
+    let config = Config { riscv_pt_levels: 3 };
+
+    let num_pt_levels = config.riscv_pt_levels;
+    assert!(num_pt_levels == 3);
+
+    // Manufacture the constants as per the diagram.
+    let k = align_down(kernel_first_vaddr, BLOCK_BITS_1GB);
+    let l = align_down(kernel_first_vaddr, BLOCK_BITS_2MB);
+    let m = align_down(kernel_first_vaddr, PAGE_BITS_4K);
+    let p = align_down(kernel_first_paddr, PAGE_BITS_4K);
+
+    let s = align_down(text_addr, BLOCK_BITS_1GB);
+    let t = align_down(text_addr, BLOCK_BITS_2MB);
+
+    // Manufacture the kernel page tables
+    let kernel_lvl2_pt_paddr = {
+        let mut lvl2_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+
+        let mut paddr = p;
+        let index_l = pt_index(num_pt_levels, l, 2);
+
+        lvl2_pt_kernel[index_l] = if kernel_first_vaddr.is_multiple_of(1 << BLOCK_BITS_2MB) {
+            assert!(paddr.is_multiple_of(1 << BLOCK_BITS_2MB));
+            let pte = pte_leaf(paddr);
+            paddr += 1 << BLOCK_BITS_2MB;
+            pte
+        } else {
+            let mut lvl3_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+
+            let index_m = pt_index(num_pt_levels, m, 3);
+
+            for index in index_m..512 {
+                lvl3_pt_kernel[index] = pte_leaf(paddr);
+                paddr += 1 << PAGE_BITS_4K;
+            }
+
+            let kernel_lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt_kernel);
+            pte_next(kernel_lvl3_pt_paddr)
+        };
+
+        for index in (index_l + 1)..512 {
+            lvl2_pt_kernel[index] = pte_leaf(paddr);
+            paddr += 1 << BLOCK_BITS_2MB;
+        }
+
+        serialise_page_table_to_paddr(&mut lvl2_pt_kernel)
+    };
+
+    // Manufacture the loader page tables, which is relatively straightforward
+    let loader_lvl2_pt_paddr = {
+        let mut lvl2_pt_loader = [0u64; PAGE_TABLE_ENTRIES];
+
+        // Identity mapped, so vaddr == paddr.
+        let mut paddr = t;
+
+        for index in pt_index(num_pt_levels, t, 2)..512 {
+            lvl2_pt_loader[index] = pte_leaf(paddr);
+            paddr += 1 << BLOCK_BITS_2MB;
+        }
+
+        serialise_page_table_to_paddr(&mut lvl2_pt_loader)
+    };
+
+    // Manufacture the Level 1 table
+    let mut boot_lvl1_pt = [0u64; PAGE_TABLE_ENTRIES];
+
+    let index_s = pt_index(num_pt_levels, s, 1);
+    let index_k = pt_index(num_pt_levels, k, 1);
+    boot_lvl1_pt[index_k] = pte_next(kernel_lvl2_pt_paddr);
+    boot_lvl1_pt[index_s] = pte_next(loader_lvl2_pt_paddr);
+
+    serialise_page_table_to_paddr(&mut boot_lvl1_pt)
+}
+
+/// AArch64 loader page tables have two variations:
+///  - Loader in EL2, then Stage 1 translations in use, so we have the
+///    singular TTBR0_EL2 register containing the Level 0 table;
+///    this allows virtual address in the range [0,2^48).
+///  - Loader in EL1, then Stage 1 translations are in use, so we have both
+///    the TTBR0_EL1 (covering vaddr in range [0,2^48)) and TTBR1_EL2 (
+///    (covering vaddr in the range [2^64-2^48,2^64)), and containing
+///    the "Level 0 Lower" page table, and "Level 0 Upper" page table
+///    physical addresses respectively.
+///
+/// Thus, for EL2 loader, the singular Level 0 page table contains the table
+/// descriptors for the "Level 1 Upper" and "Level 1 Lower" page tables.
+/// For the EL1 loader, we instead have two Level 0 page tables, and
+/// "Level 0 Lower" contains the "Level 1 Lower" descriptor, and "Level 0
+/// Upper" contains the "Level 1 Upper" descriptor.
+/// Otherwise, the page tables layout from Level 1 downwards are identical
+/// (but not necessarily the layout within the page/table/block descriptors).
+///
+/// ```txt
+///          (256 TiB)
+///   512 +-- Level 0 --+ 2^48
+///       |             |
+///       |   (empty)   |
+///       |             |
+///   k+1 +-------------+                 (512 GiB)
+///       | Level 1 Upr | ---------->  +-- Level 1 --+
+///     k +-------------+              |             |
+///       |             |              |   (empty)   |
+///       |             |              |             |
+///       |             |         l+1  +-------------+                 (1 GiB)
+///       |             |              | Level 2 Upr | ----------> +-- Level 2 --+             +-------------+
+///       |             |           l  +-------------+             |             | ----------> | 2 MiB block |
+///       |             |              |             |         511 |-------------|             +-------------+
+///       |             |              |   (empty)   |             |             | ----------> | 2 MiB block |
+///       |             |              |             |         510 |-------------|             +-------------+
+///       |             |              +-------------+             |             | ----------> | 2 MiB block |
+///       |             |                                          |-------------|             +-------------+
+///       |   (empty)   |                          Kernel Regions       (...)         (...)         (...)
+///       |             |                                          |-------------|             +-------------+
+///       |             |                                          |             | ----------> | 2 MiB block |
+///       |             |                                        m |-------------|             +-------------+ p
+///       |             |                                          |             |
+///       |             |                                          |   (empty)   |
+///       |             |                                          |             |
+///       |             |                                        0 +-------------+
+///       |             |
+///       |             |
+///       |             |
+///     1 +-------------+                 (512 GiB)
+///       | Level 1 Lwr | ---------->  +-- Level 1 --+
+///     0 +-------------+              TODO: RAM.
+///
+///
+/// Where:
+///      k = align_down(kernel_first_vaddr, 512GiB),
+///      l = align_down(kernel_first_vaddr, 1GiB),
+///      m = align_down(kernel_first_vaddr, 2MiB),
+///      p = align_down(kernel_first_paddr, 2MiB),
+///      u = align_down(uart_base, 1GiB),
+/// ```
+///
+#[unsafe(no_mangle)]
+pub extern "C" fn aarch64_setup_pagetables(
+    kernel_first_vaddr: u64,
+    kernel_first_paddr: u64,
+    page_tables_paddr_start: u64,
+) -> (u64, u64, u64) {
+    use aarch64::{
+        block_descriptor, lvl0_index, lvl1_index, lvl2_index, lvl3_index, page_descriptor,
+        s1_mair_attr_index::{MT_DEVICE_nGnRnE, MT_NORMAL},
+        table_descriptor, BLOCK_BITS_1GB, BLOCK_BITS_2MB, BLOCK_BITS_512GB, PAGE_BITS_4KB,
+    };
+
+    const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
+
+    let mut serialise_page_table_to_paddr = {
+        assert!(
+            page_tables_paddr_start
+                == page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64)
+        );
+
+        // This maintains the current end of the PT array.
+        let mut next_pt_paddr = page_tables_paddr_start;
+
+        move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
+            let pt_paddr = next_pt_paddr;
+            // page_table_bytes.extend(page_table.iter().flat_map(|pte| pte.to_le_bytes()));
+            next_pt_paddr += PAGE_TABLE_SIZE as u64;
+            page_table.fill(0);
+            pt_paddr
+        }
+    };
+
+    struct Region {
+        start: u64,
+        end: u64,
+    }
+
+    let identity_mapped_regions: &[(Region, u64)] = &[];
+    // let identity_mapped_regions = {
+    //     let ram_regions = config
+    //         .normal_regions
+    //         .as_ref()
+    //         .expect("AArch64 should have normal_regions");
+
+    //     // println!("{:#x?}", ram_regions);
+
+    //     let mut regions: Vec<_> = ram_regions
+    //         .iter()
+    //         .cloned()
+    //         .map(|region| (region, MT_DEVICE_nGnRnE))
+    //         .collect();
+
+    //     // FIXME: Derive from the kernel build system.
+    //     if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
+    //         let uart_base = align_down(uart_base, PAGE_BITS_4KB);
+    //         regions.push((
+    //             PlatformConfigRegion {
+    //                 start: uart_base,
+    //                 end: uart_base + (1 << PAGE_BITS_4KB),
+    //             },
+    //             MT_DEVICE_nGnRnE,
+    //         ));
+    //     }
+
+    //     // FIXME: This is currently assuming implementation details of the BCM2711/
+    //     //        Raspberry Pi 4B spin table implementation, as it is the only
+    //     //        platform we have that uses spin tables. Specifically, that
+    //     //        it is always located at the 0 page.
+    //     if elf.find_symbol("cpus_release_addr").is_ok() {
+    //         regions.push((
+    //             PlatformConfigRegion {
+    //                 start: 0x0,
+    //                 end: 1 << PAGE_BITS_4KB,
+    //             },
+    //             MT_DEVICE_nGnRnE,
+    //         ));
+    //     }
+
+    //     regions.sort_by_key(|(region, _)| region.start);
+
+    //     regions
+    // };
+
+    // Manufacture the constants as per the diagram.
+    let k = align_down(kernel_first_vaddr, BLOCK_BITS_512GB);
+    let l = align_down(kernel_first_vaddr, BLOCK_BITS_1GB);
+    let m = align_down(kernel_first_vaddr, BLOCK_BITS_2MB);
+    let p = align_down(kernel_first_paddr, BLOCK_BITS_2MB);
+
+    // Manufacture the kernel page tables, which is relatively straightforward.
+    let kernel_lvl1_pt_paddr = {
+        // First, the Level 2 Upr table.
+        let lvl2_pt_paddr = {
+            let mut lvl2_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+
+            let mut vaddr = m;
+            let mut paddr = p;
+            while lvl1_index(m) == lvl1_index(vaddr) {
+                lvl2_pt_kernel[lvl2_index(vaddr)] = block_descriptor(2, paddr, MT_NORMAL);
+
+                vaddr += 1 << BLOCK_BITS_2MB;
+                paddr += 1 << BLOCK_BITS_2MB;
+            }
+
+            serialise_page_table_to_paddr(&mut lvl2_pt_kernel)
+        };
+
+        // Then, the Level 1 Upr table.
+        let mut lvl1_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
+        lvl1_pt_kernel[lvl1_index(l)] = table_descriptor(lvl2_pt_paddr);
+
+        serialise_page_table_to_paddr(&mut lvl1_pt_kernel)
+    };
+
+    // Manufacture the RAM page tables, which is a little bit more complicated.
+    // We assume that normal RAM lies between 0 <= paddr < 512GiB, i.e.
+    // that lvl0_index(any ram region addr) = 0.
+    let ram_lvl1_pt_paddr = {
+        // Validation of assumptions about the identity mapped regions.
+        let mut previous_end = None;
+        for (region, _) in identity_mapped_regions.iter() {
+            assert!(lvl0_index(region.start) == 0);
+            assert!(lvl0_index(region.end - 1) == 0);
+            // This is probably an unnecessary assumption.
+            assert!(region.start.is_multiple_of(4096));
+            assert!(region.end.is_multiple_of(4096));
+            // This is definitely necessary.
+            assert!(region.start >= previous_end.unwrap_or(0));
+            previous_end = Some(region.end);
+        }
+
+        // We maintain three active page tables, which contain our previous
+        // known page table data. As we process regions in ascending order,
+        // once we have exceeded the bounds of the current reservation we
+        // can simply push to the page_table_bytes storage and insert into
+        // the parent PT the descriptor.
+        // When the current vaddr (/paddr, as identity mapped) exceeds the
+        // top value we rotate to a new PT.
+
+        struct PageTableConstructor<const LEVELS: usize, const ENTRIES: usize, PTE, Addr> {
+            invalid: PTE,
+            levels: [[PTE; ENTRIES]; LEVELS],
+            level_top: [Addr; LEVELS],
+        }
+
+        impl<const LEVELS: usize, const ENTRIES: usize, PTE: Copy + PartialEq, Addr>
+            PageTableConstructor<LEVELS, ENTRIES, PTE, Addr>
+        {
+            const fn new(invalid: PTE, level_top: [Addr; LEVELS]) -> Self {
+                Self {
+                    invalid,
+                    levels: [[invalid; ENTRIES]; LEVELS],
+                    level_top: level_top,
+                }
+            }
+
+            fn lvl(&mut self, lvl: usize) -> &mut [PTE; ENTRIES] {
+                assert!(lvl < LEVELS);
+                &mut self.levels[lvl]
+            }
+
+            fn lvl_top(&mut self, lvl: usize) -> &mut Addr {
+                assert!(lvl < LEVELS);
+                &mut self.level_top[lvl]
+            }
+
+            fn lvl_is_empty(&self, lvl: usize) -> bool {
+                assert!(lvl < LEVELS);
+                self.levels[lvl] != [self.invalid; ENTRIES]
+            }
+        }
+
+        static mut PTS: PageTableConstructor<4, PAGE_TABLE_ENTRIES, u64, u64> =
+            PageTableConstructor::new(
+                0,
+                [
+                    u64::MAX,
+                    1 << BLOCK_BITS_512GB,
+                    1 << BLOCK_BITS_1GB,
+                    1 << BLOCK_BITS_2MB,
+                ],
+            );
+
+        // SAFETY: Trust me. This function is not, and can not, be reentrant,
+        // and more than that, can only be called once.
+        #[allow(static_mut_refs)]
+        let pts = unsafe { &mut PTS };
+
+        // TODO: Tests...
+        // This is similar to aligned_power_of_two_regions() for the kernel UT,
+        // but we restrict it such that the output always is either 1GB, 2MB, or 4KB
+        // pages.
+
+        // Allowed externally for the final iteration
+        let mut base = 0u64;
+        for &(ref region, attr_index) in identity_mapped_regions.iter() {
+            // println!("RAM Region: {:#x}..{:#x}", base, region.end);
+            // println!(
+            //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
+            //     (*pts.lvl_top(1) - (1 << BLOCK_BITS_512GB)),
+            //     *pts.lvl_top(1),
+            //     lvl1_pt.iter().filter(|&&v| v != 0).count()
+            // );
+            // println!(
+            //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
+            //     (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)),
+            //     *pts.lvl_top(2),
+            //     lvl2_pt.iter().filter(|&&v| v != 0).count()
+            // );
+            // println!(
+            //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
+            //     (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
+            //     lvl3_vaddr_top,
+            //     lvl3_pt.iter().filter(|&&v| v != 0).count()
+            // );
+
+            // Handle the fact that the regions are not contiguous and that
+            // we might need to skip PT.
+
+            {
+                if region.start >= *pts.lvl_top(3) {
+                    if !pts.lvl_is_empty(3) {
+                        let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(3));
+                        // println!("[iter] Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{pts.lvl_top(3):#x}", (pts.lvl_top(3) - (1 << BLOCK_BITS_2MB)));
+                        assert!(pts.lvl(2)[lvl2_index(base)] == 0);
+                        pts.lvl(2)[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+                    }
+
+                    // TODO: just compute it.
+                    while region.start >= *pts.lvl_top(3) {
+                        *pts.lvl_top(3) += 1 << BLOCK_BITS_2MB;
+                    }
+                }
+
+                if region.start >= *pts.lvl_top(2) {
+                    if !pts.lvl_is_empty(2) {
+                        let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
+                        // println!("[iter] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{*pts.lvl_top(2):#x}, base: {:#x} lvl1_index(base): {:#x}", (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+                        assert!(pts.lvl(1)[lvl1_index(base)] == 0);
+                        pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+                    }
+
+                    // TODO: just compute it.
+                    while region.start >= *pts.lvl_top(2) {
+                        *pts.lvl_top(2) += 1 << BLOCK_BITS_1GB;
+                    }
+                }
+
+                if region.start >= *pts.lvl_top(1) {
+                    unreachable!(
+                        "impossible as everything should fit here: {:#x}",
+                        *pts.lvl_top(1)
+                    );
+                }
+            }
+
+            // After serialising the old base, update the new one.
+            base = region.start;
+
+            // Inner Loop:
+            // Invariant: the page tables in lvl1_pt, lvl2_pt, lvl3_pt
+            //            are either (1) for the current address range,
+            //            or (2) are empty and for a lower level than the current level.
+            //            Also, the values in lvlXXX_vaddr_top are always correct (even if empty)
+            //            Also contiguous within the loop.
+            // Loop entry: (1) holds by work at the start of each region
+            while base != region.end {
+                // Condition is !=, but assert that we never skip it.
+                assert!(base < region.end);
+
+                let size_bits = region.end.wrapping_sub(base).ilog2();
+                let align_bits = min(
+                    size_bits,
+                    // FIXME: Once MSRV is > 1.97, use .lowest_one() method.
+                    if base == 0 {
+                        size_bits
+                    } else {
+                        base.trailing_zeros()
+                    },
+                );
+
+                // Match the size and alignment of the current region to
+                // the valid PT region sizes.
+                let (level, bits) = match u64::from(align_bits) {
+                    BLOCK_BITS_1GB.. => (1, BLOCK_BITS_1GB),
+                    BLOCK_BITS_2MB.. => (2, BLOCK_BITS_2MB),
+                    PAGE_BITS_4KB.. => (3, PAGE_BITS_4KB),
+                    0.. => panic!("impossible; regions should be aligned to 4K at least"),
+                };
+
+                let pt_region_size = 1u64 << bits;
+                let top = base + pt_region_size;
+
+                // println!("- Aligned PT region: {:#x}..{:#x} (size_bits: {}, align_bits: {}, bits: {})", base, top, size_bits, align_bits, bits);
+                // println!(
+                //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
+                //     (*pts.lvl_top(1) - (1 << BLOCK_BITS_512GB)),
+                //     *pts.lvl_top(1),
+                //     lvl1_pt.iter().filter(|&&v| v != 0).count()
+                // );
+                // println!(
+                //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
+                //     (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)),
+                //     *pts.lvl_top(2),
+                //     lvl2_pt.iter().filter(|&&v| v != 0).count()
+                // );
+                // println!(
+                //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
+                //     (pts.lvl_top(3) - (1 << BLOCK_BITS_2MB)),
+                //     pts.lvl_top(3),
+                //     lvl3_pt.iter().filter(|&&v| v != 0).count()
+                // );
+
+                match level {
+                    1 => {
+                        // If it belongs in Level 1 PT, then it must go in
+                        // lvl1 pt. By the inavariant, base < *pts.lvl_top(1).
+                        assert!(base < *pts.lvl_top(1));
+                        // top is <= *pts.lvl_top(1) (the case where it is the topmost entry)
+                        assert!(top <= *pts.lvl_top(1));
+
+                        assert!(pts.lvl(1)[lvl1_index(base)] == 0);
+                        pts.lvl(1)[lvl1_index(base)] = block_descriptor(1, base, attr_index);
+
+                        if top == *pts.lvl_top(1) {
+                            // Invariant maintenance: if the new top would be now equal
+                            // the end of the page table's region top, we need a new
+                            // page table object and add it to the list.
+
+                            // This should be possible to handle - we just need to break out of this loop
+                            todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
+                        }
+
+                        // Invariant: Lower levels are empty.
+                        assert!(pts.lvl_is_empty(2));
+                        assert!(pts.lvl_is_empty(3));
+                        // Invariant maintenance: vaddr_top is right range for current PT.
+                        // it's empty so we need to increment the top to be current top (1G aligned) + 2MIB (512 lvl3 entries)
+                        *pts.lvl_top(3) = top + (1 << BLOCK_BITS_2MB);
+                        // it's empty so we need to increment the top to be current top (1G aligned) + 1G (512 lvl2 entries)
+                        *pts.lvl_top(2) = top + (1 << BLOCK_BITS_1GB);
+                    }
+                    2 => {
+                        // If it is a 2MiB block, it must go in the Level 2 PT;
+                        // by our invariants: base < *pts.lvl_top(2) and top <= *pts.lvl_top(2)
+                        assert!(base < *pts.lvl_top(2));
+                        assert!(top <= *pts.lvl_top(2));
+
+                        assert!(pts.lvl(2)[lvl2_index(base)] == 0);
+                        pts.lvl(2)[lvl2_index(base)] = block_descriptor(2, base, attr_index);
+
+                        if top == *pts.lvl_top(2) {
+                            // Invariant maintenance: keep for current address range.
+                            // As we're the top of the range, we can serialise the table.
+
+                            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
+                            // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} up to {*pts.lvl_top(2):#x}");
+                            *pts.lvl_top(2) += 1 << BLOCK_BITS_1GB;
+
+                            pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+
+                            if top == *pts.lvl_top(1) {
+                                todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
+                            }
+                        }
+
+                        // Invariant: Lower levels are empty.
+                        assert!(pts.lvl_is_empty(3));
+                        // Invariant maintenance: vaddr_top is right range for current PT.
+                        // it's empty so we need to increment the top to be current top (2MIB aligned) + 2MIB (512 lvl3 entries)
+                        *pts.lvl_top(3) = top + (1 << BLOCK_BITS_2MB);
+                    }
+                    3 => {
+                        // If it is a 4K page, it must go in the Level 3 PT;
+                        // by our invariants: base < pts.lvl_top(3) and top <= pts.lvl_top(3)
+                        assert!(base < *pts.lvl_top(3));
+                        assert!(top <= *pts.lvl_top(3));
+
+                        assert!(pts.lvl(3)[lvl3_index(base)] == 0);
+                        pts.lvl(3)[lvl3_index(base)] = page_descriptor(base, attr_index);
+
+                        if top == *pts.lvl_top(3) {
+                            // Invariant maintenance: keep for current address range.
+                            // As we're the top of the range, we can serialise the table.
+
+                            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(3));
+                            // println!("Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{pts.lvl_top(3):#x}", (pts.lvl_top(3) - (1 << BLOCK_BITS_2MB)));
+                            *pts.lvl_top(3) += 1 << BLOCK_BITS_2MB;
+
+                            assert!(pts.lvl(2)[lvl2_index(base)] == 0);
+                            pts.lvl(2)[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+
+                            if top == *pts.lvl_top(2) {
+                                let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
+                                // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{*pts.lvl_top(2):#x}", (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)));
+                                *pts.lvl_top(2) += 1 << BLOCK_BITS_1GB;
+
+                                assert!(pts.lvl(1)[lvl1_index(base)] == 0);
+                                pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+
+                                if top == *pts.lvl_top(1) {
+                                    todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
+                                }
+                            }
+                        }
+
+                        // Invariant: lower levels empty is vacuuously true
+                    }
+                    _ => unreachable!("level is 1..=3"),
+                }
+
+                base = base + pt_region_size;
+            }
+        }
+
+        // By the loop invariant, we know that anything before has been serialised.
+        // However, as we are at the end of the loop now, we might have
+        // page tables that have been partially filled out, and we need to
+        // serialise these.
+
+        if !pts.lvl_is_empty(3) {
+            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(3));
+            // println!("[end] Serialise lvl3 table: {lvl3_pt_paddr:#x}");
+            assert!(pts.lvl(2)[lvl2_index(base)] == 0);
+            pts.lvl(2)[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+        }
+
+        if !pts.lvl_is_empty(2) {
+            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
+            // println!("[end] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{*pts.lvl_top(2):#x}, base: {:#x} lvl1_index(base): {:#x}", (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+            assert!(pts.lvl(1)[lvl1_index(base)] == 0);
+            pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+        }
+
+        // the level1 pt should not be empty. lol.
+        assert!(!pts.lvl_is_empty(1));
+
+        // println!("New lvl1 table");
+        serialise_page_table_to_paddr(pts.lvl(1))
+    };
+
+    struct Config {
+        hypervisor: bool,
+    }
+    let config = Config { hypervisor: true };
+
+    // Depending on whether we are in hypervisor mode, we either need to
+    // return the TTBR0_EL2 or TTBR[0,1]_EL1 values. We return u64::MAX
+    // so as to return garbage - an unaligned address outside of physical
+    // memory.
+    if config.hypervisor {
+        // Manufacture the Level 0 table, containing the kernel table
+        // and the RAM tables.
+
+        let mut ttbr0_el2_pt = [0u64; PAGE_TABLE_ENTRIES];
+
+        assert!(lvl0_index(k) != lvl0_index(0));
+        ttbr0_el2_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
+        ttbr0_el2_pt[lvl0_index(0)] = table_descriptor(ram_lvl1_pt_paddr);
+
+        let ttbr0_el2 = serialise_page_table_to_paddr(&mut ttbr0_el2_pt);
+
+        (ttbr0_el2, u64::MAX, u64::MAX)
+    } else {
+        let mut ttbr0_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
+        let mut ttbr1_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
+
+        // Kernel in TTBR1 (Upper)
+        ttbr1_el1_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
+        // Identity-mapped RAM in TTBR0 (Lower)
+        ttbr0_el1_pt[lvl0_index(0)] = table_descriptor(ram_lvl1_pt_paddr);
+
+        let ttbr0_el1 = serialise_page_table_to_paddr(&mut ttbr0_el1_pt);
+        let ttbr1_el1 = serialise_page_table_to_paddr(&mut ttbr1_el1_pt);
+
+        (u64::MAX, ttbr0_el1, ttbr1_el1)
+    }
+}
diff --git a/tool/microkit/src/loader.rs b/tool/microkit/src/loader.rs
index d41225f6a..2c12b1101 100644
--- a/tool/microkit/src/loader.rs
+++ b/tool/microkit/src/loader.rs
@@ -4,332 +4,15 @@
 // SPDX-License-Identifier: BSD-2-Clause
 //
 use crate::elf::{ElfFile, ElfSegmentData};
-use crate::sel4::{Arch, Config, PlatformConfigRegion};
+use crate::sel4::{Arch, Config};
 use crate::uimage::uimage_serialise;
-use crate::util::{align_down, mb, round_up, struct_to_bytes};
-use std::cmp::min;
+use crate::util::{mb, round_up, struct_to_bytes};
 use std::fs::File;
 use std::io::{BufWriter, Write};
 use std::mem;
 use std::ops::Range;
 use std::path::Path;
 
-macro_rules! grab_symbol {
-    ($elf: expr, $symbol_name: expr) => {
-        $elf.find_symbol($symbol_name)
-            .expect(concat!("Could not find '", $symbol_name, "' symbol"))
-    };
-}
-
-// XX: This could be generic on arbitrary <T> if we could specify T:: implements from_le_bytes,
-// but we can't.
-fn read_symbol_maybe(elf: &ElfFile, symbol_name: &str) -> Option<u64> {
-    let (addr, size) = elf.find_symbol(symbol_name).ok()?;
-
-    let symbol_bytes = elf.get_data(addr, size)?;
-
-    assert!(mem::size_of::<u64>() == symbol_bytes.len());
-
-    Some(u64::from_le_bytes(symbol_bytes.try_into().ok()?))
-}
-
-macro_rules! write_symbol {
-    ($loader_image: expr, $image_vaddr: expr, $elf: expr, $symbol: literal, $symbol_var: expr) => {
-        let (addr, size) = grab_symbol!($elf, $symbol);
-        let addr = usize::try_from(addr).expect("addr fits in usize");
-        let size = usize::try_from(size).expect("size fits in usize");
-        let image_vaddr = usize::try_from($image_vaddr).expect("vaddr fits in usize");
-
-        assert!(addr >= image_vaddr);
-        assert!(size == ::std::mem::size_of_val(&$symbol_var));
-
-        let offset: usize = (addr - image_vaddr);
-        assert!(offset <= $loader_image.len());
-
-        $loader_image[offset..(offset + size)].copy_from_slice(&$symbol_var.to_le_bytes());
-    };
-}
-
-const PAGE_TABLE_SIZE: usize = 4096;
-
-pub mod aarch64 {
-    //! For AArch64, our page tables use the Stage 1 descriptor formats
-    //! for both EL2 (TTBR0_EL2) and EL1 (TTBR0_EL1/TTBR1_EL1).
-    //! Stage 2 descriptors are only used when in the EL1&0 regime; which is not
-    //! the case when in EL2.
-
-    use crate::util::mask;
-
-    pub const LVL0_BITS: u64 = 9;
-    pub const LVL1_BITS: u64 = 9;
-    pub const LVL2_BITS: u64 = 9;
-    pub const LVL3_BITS: u64 = 9;
-
-    pub fn lvl0_index(addr: u64) -> usize {
-        let idx = (addr >> (BLOCK_BITS_2MB + LVL2_BITS + LVL1_BITS)) & mask(LVL0_BITS);
-        idx as usize
-    }
-
-    pub fn lvl1_index(addr: u64) -> usize {
-        let idx = (addr >> (BLOCK_BITS_2MB + LVL2_BITS)) & mask(LVL1_BITS);
-        idx as usize
-    }
-
-    pub fn lvl2_index(addr: u64) -> usize {
-        let idx = (addr >> (BLOCK_BITS_2MB)) & mask(LVL2_BITS);
-        idx as usize
-    }
-
-    pub fn lvl3_index(addr: u64) -> usize {
-        let idx = (addr >> PAGE_BITS_4KB) & mask(LVL3_BITS);
-        idx as usize
-    }
-
-    /// Stage 1 translation table page/block descriptors have bits[4:2] containing
-    /// AttrIndex[2:0]. The AttrIndex values depends on our configuration of
-    /// the `MAIR_EL1` or `MAIR_EL2` registers done in util64.S;
-    /// This also needs to match the values that seL4 uses.
-    #[allow(non_upper_case_globals, reason = "matching ARM naming convention")]
-    pub mod s1_mair_attr_index {
-        pub const MT_DEVICE_nGnRnE: u64 = 0b000;
-        pub const MT_DEVICE_nGnRE: u64 = 0b001;
-        pub const MT_DEVICE_GRE: u64 = 0b010;
-        pub const MT_NORMAL_NC: u64 = 0b011;
-        pub const MT_NORMAL: u64 = 0b100;
-    }
-
-    pub mod descriptor_type {
-        //! The translation table descriptor formats, as per §D8.3 "Translation
-        //! table descriptor formats" of ARM DDI 0487 L.b. Specifically,
-        //! as per "Table D8-48 Determination of descriptor type"
-
-        /// Descriptor type: Table. Condition is lookup level != 3.
-        pub const TABLE: u64 = 0b11;
-        /// Descriptor type: Page. Condition is lookup level == 3.
-        pub const PAGE: u64 = 0b11;
-        /// Descriptor type: Block. Condition is lookup level != 3.
-        pub const BLOCK: u64 = 0b01;
-        /// Descriptor type: Invalid. Strictly speaking bit[1] does not matter.
-        pub const INVALID: u64 = 0b00;
-    }
-
-    pub mod shareability_attributes {
-        //! Per §D8.6.2 "Stage 1 Shareability attributes", these contain the
-        //! shareability attributes of the descriptor OA for normal-cacheable
-        //! memory.
-
-        /// Non-shareable
-        pub const NON_SHAREABLE: u64 = 0b00;
-        /// Outer-shareable
-        pub const OUTER_SHAREABLE: u64 = 0b10;
-        /// Inner-shareable
-        pub const INNER_SHAREABLE: u64 = 0b11;
-    }
-
-    /// Per "Figure D8-14 VMSAv8-64 Block descriptor formats" of ARM DDI0487L.b,
-    /// subfigure "4KB, 16KB, and 64KB granules, 48-bit OA", the Output address
-    /// is bits [47:n], and:
-    ///
-    /// > For the 4KB granule size, the level 1 descriptor n is 30,
-    /// > and the level 2 descriptor n is 21.
-    pub const BLOCK_BITS_1GB: u64 = 30;
-
-    /// Per "Figure D8-14 VMSAv8-64 Block descriptor formats" of ARM DDI0487L.b,
-    /// subfigure "4KB, 16KB, and 64KB granules, 48-bit OA", the Output address
-    /// is bits [47:n], and:
-    ///
-    /// > For the 4KB granule size, the level 1 descriptor n is 30,
-    /// > and the level 2 descriptor n is 21.
-    pub const BLOCK_BITS_2MB: u64 = 21;
-
-    // TODO:
-
-    pub const BLOCK_BITS_512GB: u64 = 39;
-    pub const PAGE_BITS_4KB: u64 = 12;
-
-    /// Per "Table D8-52 Stage 1 VMSAv8-64 Block and Page descriptor fields" and
-    /// "Figure D8-14 VMSAv8-64 Block descriptor formats" of ARM DDI0487L.b;
-    /// specifically subfigure "4KB, 16KB, and 64KB granules, 48-bit OA"
-    pub fn block_descriptor(level: usize, addr: u64, attr_index: u64) -> u64 {
-        // Per Table D8-48, Condition for descriptor_type::BLOCK is level != 3.
-        assert!(level != 3);
-
-        let upper_attributes: u64 = 0;
-
-        let shareability = if attr_index == s1_mair_attr_index::MT_NORMAL {
-            // Match what the seL4 kernel uses for its page tables, which
-            // is especially necessary for SMP booting which relies on it
-            // for coherency. See the comment in seL4 `release_secondary_cpus()`.
-            shareability_attributes::INNER_SHAREABLE
-        } else {
-            // Per $R_{PYFVQ}$:
-            // > If a region is mapped as Device memory or Normal Non-cacheable
-            // > memory after all enabled translation stages, then the region
-            // > has an effective Shareability attribute of Outer Shareable.
-            //
-            // We override the value we place in here to OUTER_SHAREABLE to match
-            // how the hardware behaves. This is not necessary but for clarity.
-            shareability_attributes::OUTER_SHAREABLE
-        };
-
-        // AP[2:1], which we set as 0b00 for read/write access:
-        //   stage 1: 0b00 is {PrivRead, PrivWrite} and we are EL1
-        //   stage 2: 0b00 is RW for EL2 and no perms for EL1.
-        const AP_KERNEL_RW: u64 = 0b00;
-
-        // bit[11] is the not global (nG) field, we leave as 0 (global).
-        // bit[10] is the access flag; depending on FEAT_HAFDBS, when software
-        //         manages the AF memory accesses to the page/block when AF=0
-        //         raise an Access Fault; when hardware manages the AF it will
-        //         become 1.
-        // bit[9:8] is SH[1:0] containing stage 1 shareability attributes
-        // bit[7:6] contains AP[2:1]
-        // bit[5] is RES0
-        // bit[4:2] contains AttrIndex
-        let lower_attributes: u64 =
-            (1 << 10) | (AP_KERNEL_RW << 6) | (shareability << 8) | (attr_index << 2);
-
-        // bits[47:n]
-        let output_address: u64 = addr
-            & !mask(match level {
-                1 => BLOCK_BITS_1GB,
-                2 => BLOCK_BITS_2MB,
-                _ => panic!("unsupported level {level} for block descriptor"),
-            });
-
-        // address must not have bits above 47 set.
-        assert!(addr & mask(48) == addr);
-
-        // bits[63:50] describing the "Upper attributes" are left at 0.
-        // bits[49:48] are RES0
-        // bits[47:n] contain the Output address
-        // bits[n-1:12] are RES0
-        // bits[11:2] contain the "Lower attributes"
-        // bits[1:0] contains the descriptor type
-        upper_attributes | output_address | lower_attributes | descriptor_type::BLOCK
-    }
-
-    /// Per "Table D8-52 Stage 1 VMSAv8-64 Block and Page descriptor fields" and
-    /// "Figure D8-15 VMSAv8-64 Page descriptor formats" of ARM DDI0487L.b;
-    /// specifically subfigure "4KB granule 48-bit OA".
-    pub fn page_descriptor(addr: u64, attr_index: u64) -> u64 {
-        // The main difference between a page descriptor and block descriptor
-        // is in the size of the output address (OA) and in the descriptor type.
-
-        let upper_attributes: u64 = 0;
-
-        let shareability = if attr_index == s1_mair_attr_index::MT_NORMAL {
-            // Match what the seL4 kernel uses for its page tables, which
-            // is especially necessary for SMP booting which relies on it
-            // for coherency.
-            shareability_attributes::INNER_SHAREABLE
-        } else {
-            // Per $R_{PYFVQ}$:
-            // > If a region is mapped as Device memory or Normal Non-cacheable
-            // > memory after all enabled translation stages, then the region
-            // > has an effective Shareability attribute of Outer Shareable.
-            // We override the value we place in here to OUTER_SHAREABLE to match
-            // how the hardware behaves.
-            shareability_attributes::OUTER_SHAREABLE
-        };
-
-        // AP[2:1], which we set as 0b00 for read/write access:
-        //   stage 1: 0b00 is {PrivRead, PrivWrite} and we are EL1/El2 (priv)
-        const AP_KERNEL_RW: u64 = 0b00;
-
-        // bit[11] is the not global (nG) field, we leave as 0 (global).
-        // bit[10] is the access flag; depending on FEAT_HAFDBS, when software
-        //         manages the AF memory accesses to the page/block when AF=0
-        //         raise an Access Fault; when hardware manages the AF it will
-        //         become 1.
-        // bit[9:8] is SH[1:0] containing stage 1 shareability attributes
-        // bit[7:6] contains AP[2:1]
-        // bit[5] is RES0
-        // bit[4:2] contains AttrIndex
-        let lower_attributes: u64 =
-            (1 << 10) | (AP_KERNEL_RW << 6) | (shareability << 8) | (attr_index << 2);
-
-        // bits[47:12]
-        let output_address: u64 = addr & !mask(12);
-
-        // address must not have bits above 47 set.
-        assert!(addr & mask(48) == addr);
-
-        // bits[63:50] describing the "Upper attributes" are left at 0.
-        // bits[49:48] are RES0
-        // bits[47:12] contain the Output address
-        // bits[11:2] contain the "Lower attributes"
-        // bits[1:0] contains the descriptor type
-        upper_attributes | output_address | lower_attributes | descriptor_type::PAGE
-    }
-
-    /// Per "Table D8-50 Stage 1 VMSAv8-64 Table descriptor fields" and
-    /// "Figure D8-12 VMSAv8-64 Table descriptor formats" of ARM DDI0487L.b;
-    /// specifically subfigure "4KB, 16KB, and 64KB granules, 48-bit OA"
-    pub fn table_descriptor(addr: u64) -> u64 {
-        // Per Table D8-48, Condition for descriptor_type::TABLE is level != 3.
-
-        // We don't set any of these attributes, most are hardware-feature conditional
-        let attributes: u64 = 0;
-
-        // address must not have bits above 47 or below 12 set
-        assert!(addr & mask(12) == 0x0);
-        assert!(addr & mask(48) == addr);
-
-        let next_level_table_address = addr;
-
-        // bits[63:59] are "Attributes"
-        // bits[58:51] are ignored
-        // bits[50:48] are RES0
-        // bits[47:m] is the next-level table address
-        //  note: here m=12 for 4KB granule
-        // bits[m-1:12] are RES0
-        //  so this doesn't exist for 4KB granule
-        // bits[11:2] are ignored
-        // bits[1:0] contain the descriptor type
-        attributes | next_level_table_address | descriptor_type::TABLE
-    }
-}
-
-mod riscv64 {
-    pub(crate) const BLOCK_BITS_1GB: u64 = 30;
-    pub(crate) const BLOCK_BITS_2MB: u64 = 21;
-    pub(crate) const PAGE_BITS_4K: u64 = 12;
-
-    pub(crate) const PAGE_TABLE_INDEX_BITS: u64 = 9;
-    pub(crate) const PAGE_SHIFT: u64 = 12;
-    /// This sets the page table entry bits: D,A,X,W,R.
-    pub(crate) const PTE_TYPE_BITS: u64 = 0b11001110;
-    // TODO: where does this come from?
-    pub(crate) const PTE_TYPE_TABLE: u64 = 0;
-    pub(crate) const PTE_TYPE_VALID: u64 = 1;
-
-    pub(crate) const PTE_PPN0_SHIFT: u64 = 10;
-
-    /// Due to RISC-V having various virtual memory setups, we have this generic function to
-    /// figure out the page-table index given the total number of page table levels for the
-    /// platform and which level we are currently looking at.
-    pub fn pt_index(pt_levels: usize, addr: u64, level: usize) -> usize {
-        let pt_index_bits = PAGE_TABLE_INDEX_BITS * (pt_levels - level) as u64;
-        let idx = (addr >> (pt_index_bits + PAGE_SHIFT)) % 512;
-
-        idx as usize
-    }
-
-    /// Generate physical page number given an address
-    pub fn pte_ppn(addr: u64) -> u64 {
-        (addr >> PAGE_SHIFT) << PTE_PPN0_SHIFT
-    }
-
-    pub fn pte_next(addr: u64) -> u64 {
-        pte_ppn(addr) | PTE_TYPE_TABLE | PTE_TYPE_VALID
-    }
-
-    pub fn pte_leaf(addr: u64) -> u64 {
-        pte_ppn(addr) | PTE_TYPE_BITS | PTE_TYPE_VALID
-    }
-}
-
 /// Checks that each region in the given list does not overlap with any other region.
 /// Panics upon finding an overlapping region
 fn check_non_overlapping(regions: &Vec<(u64, u64)>) {
@@ -373,7 +56,6 @@ pub struct Loader<'a> {
     header: LoaderHeader64,
     region_metadata: Vec<LoaderRegion64>,
     regions: Vec<(u64, &'a [u8])>,
-    page_table_bytes: Vec<u8>,
     word_size: usize,
     elf_machine: u16,
     entry: u64,
@@ -463,14 +145,6 @@ impl<'a> Loader<'a> {
             }
         }
 
-        let Some(kernel_first_vaddr) = kernel_first_vaddr else {
-            panic!("INTERNAL: could not determine kernel_first_vaddr");
-        };
-
-        let Some(kernel_first_paddr) = kernel_first_paddr else {
-            panic!("INTERNAL: could not determine kernel_first_paddr");
-        };
-
         let image_segment = loader_elf
             .segments
             .iter()
@@ -483,7 +157,7 @@ impl<'a> Loader<'a> {
         // We have to clone here as the image executable is part of this function return object,
         // and the loader ELF is deserialised in this scope, so its lifetime will be shorter than
         // the return object.
-        let mut loader_image = image_segment.data().clone();
+        let loader_image = image_segment.data().clone();
 
         if image_vaddr != loader_elf.entry {
             panic!("The loader entry point must be the first byte in the image");
@@ -512,69 +186,11 @@ impl<'a> Loader<'a> {
             offset += data.len() as u64;
         }
 
-        let partial_size = loader_image.len() as u64
+        let size = loader_image.len() as u64
             + mem::size_of::<LoaderHeader64>() as u64
             + (region_metadata.len() * mem::size_of::<LoaderRegion64>()) as u64
             + offset;
 
-        let page_tables_paddr_start = image_vaddr + partial_size;
-
-        let mut page_table_bytes = Vec::<u8>::new();
-        match config.arch {
-            Arch::Aarch64 => {
-                let (ttbr0_el2, ttbr0_el1, ttbr1_el1) = Loader::aarch64_setup_pagetables(
-                    config,
-                    &loader_elf,
-                    kernel_first_vaddr,
-                    kernel_first_paddr,
-                    page_tables_paddr_start,
-                    &mut page_table_bytes,
-                );
-
-                write_symbol!(
-                    loader_image,
-                    image_vaddr,
-                    loader_elf,
-                    "aarch64_pt_ttbr0_el2",
-                    ttbr0_el2
-                );
-                write_symbol!(
-                    loader_image,
-                    image_vaddr,
-                    loader_elf,
-                    "aarch64_pt_ttbr0_el1",
-                    ttbr0_el1
-                );
-                write_symbol!(
-                    loader_image,
-                    image_vaddr,
-                    loader_elf,
-                    "aarch64_pt_ttbr1_el1",
-                    ttbr1_el1
-                );
-            }
-            Arch::Riscv64 => {
-                let boot_lvl1_pt = Loader::riscv64_setup_pagetables(
-                    config,
-                    &loader_elf,
-                    kernel_first_vaddr,
-                    kernel_first_paddr,
-                    page_tables_paddr_start,
-                    &mut page_table_bytes,
-                );
-                write_symbol!(
-                    loader_image,
-                    image_vaddr,
-                    loader_elf,
-                    "riscv64_boot_lvl1_pt",
-                    boot_lvl1_pt
-                );
-            }
-            Arch::X86_64 => unreachable!("x86_64 does not support creating a loader image"),
-        };
-
-        let size = partial_size + page_table_bytes.len() as u64;
-
         let mut all_regions_with_loader: Vec<_> = regions
             .iter()
             .map(|&(base, data)| (base, data.len() as u64))
@@ -601,7 +217,6 @@ impl<'a> Loader<'a> {
             header,
             region_metadata,
             regions,
-            page_table_bytes,
             word_size: kernel_elf.word_size,
             elf_machine: kernel_elf.machine,
             entry: loader_elf.entry,
@@ -625,8 +240,6 @@ impl<'a> Loader<'a> {
             bytes.extend_from_slice(data);
         }
 
-        bytes.extend_from_slice(&self.page_table_bytes);
-
         assert!(bytes.len() as u64 == self.header.size);
 
         bytes
@@ -693,692 +306,4 @@ impl<'a> Loader<'a> {
             Err(e) => panic!("Could not create '{}': {}", path.display(), e),
         }
     }
-
-    /// RISC-V 64 page tables for our purposes uses the Sv39 translation scheme
-    /// (3-level page tables).
-    ///
-    /// It is split into two halves: the Upper/Kernel part of the page tables,
-    /// which matches the format seL4 expects. The lower half contains an
-    /// identity mapped region for the loader.
-    ///
-    /// ```txt
-    ///            (512 GiB)
-    ///   512 +---- Level 1 ---+ 2^39
-    ///       |                |
-    ///       |     (empty)    |
-    ///       |                |
-    ///   k+1 +----------------+                   (1 GiB)
-    ///       | Level 2 Kernel | ----------> +---- Level 2 ---+             +-------------+
-    ///     k +----------------+             |                | ----------> | 2 MiB block |
-    ///       |                |         511 |----------------|             +-------------+
-    ///       |                |             |                | ----------> | 2 MiB block |
-    ///       |                |         510 |----------------|             +-------------+
-    ///       |                |             |                | ----------> | 2 MiB block |
-    ///       |                |             |----------------|             +-------------
-    ///       |                |                   (...)           (...)         (...)          Kernel Regions
-    ///       |                |             |----------------|             +-------------+
-    ///       |                |             |                | ----------> | 2 MiB block |
-    ///       |                |         l+1 |----------------|             +-------------+
-    ///       |                |             | Level 3 Kernel | ----+
-    ///       |                |           l |----------------|     |
-    ///       |                |             |                |     |           (2 MiB)
-    ///       |                |             |                |     +-----> +-- Level 3 --+             +------------+
-    ///       |                |             |                |             |             | ----------> | 4 KiB page |
-    ///       |                |             |                |         511 |-------------|             +------------+
-    ///       |                |             |     (empty)    |             |             | ----------> | 4 KiB page |
-    ///       |     (empty)    |             |                |             |-------------|             +------------+
-    ///       |                |             |                |             |             | ----------> | 4 KiB page |
-    ///       |                |             |                |           m |-------------|             +------------+ p
-    ///       |                |             |                |             |   (empty)   |
-    ///       |                |             |                |             +-------------+
-    ///       |                |             |                |
-    ///       |                |           0 +----------------+
-    ///       |                |
-    ///       |                |
-    ///       |                |
-    ///       |                |
-    ///       |                |
-    ///   s+1 +----------------+                  (1 GiB)
-    ///       | Level 2 Loader | ---------->  +-- Level 2 --+             +-------------+
-    ///     s +----------------+              |             | ----------> | 2 MiB block |
-    ///       |                |          511 +-------------+             +-------------+
-    ///       |                |              |             | ----------> | 2 MiB block |
-    ///       |    (empty)     |          510 +-------------+             +-------------+
-    ///       |                |              |             | ----------> | 2 MiB block |
-    ///       |                |              |-------------|             +-------------+
-    ///     0 +----------------+              |             | ----------> | 2 MiB block |
-    ///                                       |-------------|             +-------------+
-    ///                                            (...)         (...)         (...)          Loader Regions
-    ///                                       |-------------|             +-------------+
-    ///                                       |             | ----------> | 2 MiB block |
-    ///                                       |-------------|             +-------------+
-    ///                                       |             | ----------> | 2 MiB block |
-    ///                                     t +-------------+             +-------------+
-    ///                                       |             |
-    ///                                       |   (empty)   |
-    ///                                       |             |
-    ///                                       +-------------+
-    ///
-    ///
-    /// Where:
-    ///      k = align_down(kernel_first_vaddr, 1GiB),
-    ///      l = align_down(kernel_first_vaddr, 2MiB),
-    ///      m = align_down(kernel_first_vaddr, 4KiB),
-    ///      p = align_down(kernel_first_paddr, 4KiB),
-    ///
-    ///      s = align_down(text_addr, 1GiB),
-    ///      t = align_down(text_addr, 2MiB),
-    /// ```
-    ///
-    fn riscv64_setup_pagetables(
-        config: &Config,
-        elf: &ElfFile,
-        kernel_first_vaddr: u64,
-        kernel_first_paddr: u64,
-        page_tables_paddr_start: u64,
-        page_table_bytes: &mut Vec<u8>,
-    ) -> u64 {
-        use riscv64::{pt_index, pte_leaf, pte_next, BLOCK_BITS_1GB, BLOCK_BITS_2MB, PAGE_BITS_4K};
-
-        let (text_addr, _) = grab_symbol!(elf, "_text");
-
-        // We map the loader using 2MB pages, so make sure the base is actually aligned.
-        assert!(text_addr.is_multiple_of(1 << BLOCK_BITS_2MB));
-
-        const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
-
-        let mut serialise_page_table_to_paddr = {
-            let page_tables_paddr_start = {
-                let aligned_pt_paddr_start =
-                    page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64);
-                if aligned_pt_paddr_start != page_tables_paddr_start {
-                    let alignment_diff =
-                        (aligned_pt_paddr_start - page_tables_paddr_start) as usize;
-                    page_table_bytes.resize(alignment_diff, 0);
-                }
-
-                aligned_pt_paddr_start
-            };
-
-            // This maintains the current end of the PT array.
-            let mut next_pt_paddr = page_tables_paddr_start;
-
-            move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
-                let pt_paddr = next_pt_paddr;
-                page_table_bytes.extend(page_table.iter().flat_map(|pte| pte.to_le_bytes()));
-                next_pt_paddr += PAGE_TABLE_SIZE as u64;
-                page_table.fill(0);
-                pt_paddr
-            }
-        };
-
-        let num_pt_levels = config.riscv_pt_levels.unwrap().levels();
-        assert!(num_pt_levels == 3);
-
-        // Manufacture the constants as per the diagram.
-        let k = align_down(kernel_first_vaddr, BLOCK_BITS_1GB);
-        let l = align_down(kernel_first_vaddr, BLOCK_BITS_2MB);
-        let m = align_down(kernel_first_vaddr, PAGE_BITS_4K);
-        let p = align_down(kernel_first_paddr, PAGE_BITS_4K);
-
-        let s = align_down(text_addr, BLOCK_BITS_1GB);
-        let t = align_down(text_addr, BLOCK_BITS_2MB);
-
-        // Manufacture the kernel page tables
-        let kernel_lvl2_pt_paddr = {
-            let mut lvl2_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
-
-            let mut paddr = p;
-            let index_l = pt_index(num_pt_levels, l, 2);
-
-            lvl2_pt_kernel[index_l] = if kernel_first_vaddr.is_multiple_of(1 << BLOCK_BITS_2MB) {
-                assert!(paddr.is_multiple_of(1 << BLOCK_BITS_2MB));
-                let pte = pte_leaf(paddr);
-                paddr += 1 << BLOCK_BITS_2MB;
-                pte
-            } else {
-                let mut lvl3_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
-
-                let index_m = pt_index(num_pt_levels, m, 3);
-
-                for index in index_m..512 {
-                    lvl3_pt_kernel[index] = pte_leaf(paddr);
-                    paddr += 1 << PAGE_BITS_4K;
-                }
-
-                let kernel_lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt_kernel);
-                pte_next(kernel_lvl3_pt_paddr)
-            };
-
-            for index in (index_l + 1)..512 {
-                lvl2_pt_kernel[index] = pte_leaf(paddr);
-                paddr += 1 << BLOCK_BITS_2MB;
-            }
-
-            serialise_page_table_to_paddr(&mut lvl2_pt_kernel)
-        };
-
-        // Manufacture the loader page tables, which is relatively straightforward
-        let loader_lvl2_pt_paddr = {
-            let mut lvl2_pt_loader = [0u64; PAGE_TABLE_ENTRIES];
-
-            // Identity mapped, so vaddr == paddr.
-            let mut paddr = t;
-
-            for index in pt_index(num_pt_levels, t, 2)..512 {
-                lvl2_pt_loader[index] = pte_leaf(paddr);
-                paddr += 1 << BLOCK_BITS_2MB;
-            }
-
-            serialise_page_table_to_paddr(&mut lvl2_pt_loader)
-        };
-
-        // Manufacture the Level 1 table
-        let mut boot_lvl1_pt = [0u64; PAGE_TABLE_ENTRIES];
-
-        let index_s = pt_index(num_pt_levels, s, 1);
-        let index_k = pt_index(num_pt_levels, k, 1);
-        boot_lvl1_pt[index_k] = pte_next(kernel_lvl2_pt_paddr);
-        boot_lvl1_pt[index_s] = pte_next(loader_lvl2_pt_paddr);
-
-        serialise_page_table_to_paddr(&mut boot_lvl1_pt)
-    }
-
-    /// AArch64 loader page tables have two variations:
-    ///  - Loader in EL2, then Stage 1 translations in use, so we have the
-    ///    singular TTBR0_EL2 register containing the Level 0 table;
-    ///    this allows virtual address in the range [0,2^48).
-    ///  - Loader in EL1, then Stage 1 translations are in use, so we have both
-    ///    the TTBR0_EL1 (covering vaddr in range [0,2^48)) and TTBR1_EL2 (
-    ///    (covering vaddr in the range [2^64-2^48,2^64)), and containing
-    ///    the "Level 0 Lower" page table, and "Level 0 Upper" page table
-    ///    physical addresses respectively.
-    ///
-    /// Thus, for EL2 loader, the singular Level 0 page table contains the table
-    /// descriptors for the "Level 1 Upper" and "Level 1 Lower" page tables.
-    /// For the EL1 loader, we instead have two Level 0 page tables, and
-    /// "Level 0 Lower" contains the "Level 1 Lower" descriptor, and "Level 0
-    /// Upper" contains the "Level 1 Upper" descriptor.
-    /// Otherwise, the page tables layout from Level 1 downwards are identical
-    /// (but not necessarily the layout within the page/table/block descriptors).
-    ///
-    /// ```txt
-    ///          (256 TiB)
-    ///   512 +-- Level 0 --+ 2^48
-    ///       |             |
-    ///       |   (empty)   |
-    ///       |             |
-    ///   k+1 +-------------+                 (512 GiB)
-    ///       | Level 1 Upr | ---------->  +-- Level 1 --+
-    ///     k +-------------+              |             |
-    ///       |             |              |   (empty)   |
-    ///       |             |              |             |
-    ///       |             |         l+1  +-------------+                 (1 GiB)
-    ///       |             |              | Level 2 Upr | ----------> +-- Level 2 --+             +-------------+
-    ///       |             |           l  +-------------+             |             | ----------> | 2 MiB block |
-    ///       |             |              |             |         511 |-------------|             +-------------+
-    ///       |             |              |   (empty)   |             |             | ----------> | 2 MiB block |
-    ///       |             |              |             |         510 |-------------|             +-------------+
-    ///       |             |              +-------------+             |             | ----------> | 2 MiB block |
-    ///       |             |                                          |-------------|             +-------------+
-    ///       |   (empty)   |                          Kernel Regions       (...)         (...)         (...)
-    ///       |             |                                          |-------------|             +-------------+
-    ///       |             |                                          |             | ----------> | 2 MiB block |
-    ///       |             |                                        m |-------------|             +-------------+ p
-    ///       |             |                                          |             |
-    ///       |             |                                          |   (empty)   |
-    ///       |             |                                          |             |
-    ///       |             |                                        0 +-------------+
-    ///       |             |
-    ///       |             |
-    ///       |             |
-    ///     1 +-------------+                 (512 GiB)
-    ///       | Level 1 Lwr | ---------->  +-- Level 1 --+
-    ///     0 +-------------+              TODO: RAM.
-    ///
-    ///
-    /// Where:
-    ///      k = align_down(kernel_first_vaddr, 512GiB),
-    ///      l = align_down(kernel_first_vaddr, 1GiB),
-    ///      m = align_down(kernel_first_vaddr, 2MiB),
-    ///      p = align_down(kernel_first_paddr, 2MiB),
-    ///      u = align_down(uart_base, 1GiB),
-    /// ```
-    ///
-    fn aarch64_setup_pagetables(
-        config: &Config,
-        elf: &ElfFile,
-        kernel_first_vaddr: u64,
-        kernel_first_paddr: u64,
-        page_tables_paddr_start: u64,
-        page_table_bytes: &mut Vec<u8>,
-    ) -> (u64, u64, u64) {
-        use aarch64::{
-            block_descriptor, lvl0_index, lvl1_index, lvl2_index, lvl3_index, page_descriptor,
-            s1_mair_attr_index::{MT_DEVICE_nGnRnE, MT_NORMAL},
-            table_descriptor, BLOCK_BITS_1GB, BLOCK_BITS_2MB, BLOCK_BITS_512GB, PAGE_BITS_4KB,
-        };
-
-        const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
-
-        let mut serialise_page_table_to_paddr = {
-            let page_tables_paddr_start = {
-                let aligned_pt_paddr_start =
-                    page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64);
-                if aligned_pt_paddr_start != page_tables_paddr_start {
-                    let alignment_diff =
-                        (aligned_pt_paddr_start - page_tables_paddr_start) as usize;
-                    page_table_bytes.resize(alignment_diff, 0);
-                }
-
-                aligned_pt_paddr_start
-            };
-
-            // This maintains the current end of the PT array.
-            let mut next_pt_paddr = page_tables_paddr_start;
-
-            move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
-                let pt_paddr = next_pt_paddr;
-                page_table_bytes.extend(page_table.iter().flat_map(|pte| pte.to_le_bytes()));
-                next_pt_paddr += PAGE_TABLE_SIZE as u64;
-                page_table.fill(0);
-                pt_paddr
-            }
-        };
-
-        let identity_mapped_regions = {
-            let ram_regions = config
-                .normal_regions
-                .as_ref()
-                .expect("AArch64 should have normal_regions");
-
-            // println!("{:#x?}", ram_regions);
-
-            let mut regions: Vec<_> = ram_regions
-                .iter()
-                .cloned()
-                .map(|region| (region, MT_DEVICE_nGnRnE))
-                .collect();
-
-            // FIXME: Derive from the kernel build system.
-            if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
-                let uart_base = align_down(uart_base, PAGE_BITS_4KB);
-                regions.push((
-                    PlatformConfigRegion {
-                        start: uart_base,
-                        end: uart_base + (1 << PAGE_BITS_4KB),
-                    },
-                    MT_DEVICE_nGnRnE,
-                ));
-            }
-
-            // FIXME: This is currently assuming implementation details of the BCM2711/
-            //        Raspberry Pi 4B spin table implementation, as it is the only
-            //        platform we have that uses spin tables. Specifically, that
-            //        it is always located at the 0 page.
-            if elf.find_symbol("cpus_release_addr").is_ok() {
-                regions.push((
-                    PlatformConfigRegion {
-                        start: 0x0,
-                        end: 1 << PAGE_BITS_4KB,
-                    },
-                    MT_DEVICE_nGnRnE,
-                ));
-            }
-
-            regions.sort_by_key(|(region, _)| region.start);
-
-            regions
-        };
-
-        // Manufacture the constants as per the diagram.
-        let k = align_down(kernel_first_vaddr, BLOCK_BITS_512GB);
-        let l = align_down(kernel_first_vaddr, BLOCK_BITS_1GB);
-        let m = align_down(kernel_first_vaddr, BLOCK_BITS_2MB);
-        let p = align_down(kernel_first_paddr, BLOCK_BITS_2MB);
-
-        // Manufacture the kernel page tables, which is relatively straightforward.
-        let kernel_lvl1_pt_paddr = {
-            // First, the Level 2 Upr table.
-            let lvl2_pt_paddr = {
-                let mut lvl2_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
-
-                let mut vaddr = m;
-                let mut paddr = p;
-                while lvl1_index(m) == lvl1_index(vaddr) {
-                    lvl2_pt_kernel[lvl2_index(vaddr)] = block_descriptor(2, paddr, MT_NORMAL);
-
-                    vaddr += 1 << BLOCK_BITS_2MB;
-                    paddr += 1 << BLOCK_BITS_2MB;
-                }
-
-                serialise_page_table_to_paddr(&mut lvl2_pt_kernel)
-            };
-
-            // Then, the Level 1 Upr table.
-            let mut lvl1_pt_kernel = [0u64; PAGE_TABLE_ENTRIES];
-            lvl1_pt_kernel[lvl1_index(l)] = table_descriptor(lvl2_pt_paddr);
-
-            serialise_page_table_to_paddr(&mut lvl1_pt_kernel)
-        };
-
-        // Manufacture the RAM page tables, which is a little bit more complicated.
-        // We assume that normal RAM lies between 0 <= paddr < 512GiB, i.e.
-        // that lvl0_index(any ram region addr) = 0.
-        let ram_lvl1_pt_paddr = {
-            // Validation of assumptions about the identity mapped regions.
-            let mut previous_end = None;
-            for (region, _) in identity_mapped_regions.iter() {
-                assert!(lvl0_index(region.start) == 0);
-                assert!(lvl0_index(region.end - 1) == 0);
-                // This is probably an unnecessary assumption.
-                assert!(region.start.is_multiple_of(4096));
-                assert!(region.end.is_multiple_of(4096));
-                // This is definitely necessary.
-                assert!(region.start >= previous_end.unwrap_or(0));
-                previous_end = Some(region.end);
-            }
-
-            // We maintain three active page tables, which contain our previous
-            // known page table data. As we process regions in ascending order,
-            // once we have exceeded the bounds of the current reservation we
-            // can simply push to the page_table_bytes storage and insert into
-            // the parent PT the descriptor.
-            // When the current vaddr (/paddr, as identity mapped) exceeds the
-            // top value we rotate to a new PT.
-
-            let mut lvl1_pt = [0u64; PAGE_TABLE_ENTRIES];
-            let mut lvl2_pt = [0u64; PAGE_TABLE_ENTRIES];
-            let mut lvl3_pt = [0u64; PAGE_TABLE_ENTRIES];
-            // TODO: These should be defines. Note that the top is the size of 1 level of the next level up.
-            // TODO: LVL1_ENTRY_RANGE? idk
-            #[allow(unused_mut)]
-            let mut lvl1_vaddr_top = 1 << BLOCK_BITS_512GB;
-            let mut lvl2_vaddr_top = 1 << BLOCK_BITS_1GB;
-            let mut lvl3_vaddr_top = 1 << BLOCK_BITS_2MB;
-
-            // TODO: Tests...
-            // This is similar to aligned_power_of_two_regions() for the kernel UT,
-            // but we restrict it such that the output always is either 1GB, 2MB, or 4KB
-            // pages.
-
-            // Allowed externally for the final iteration
-            let mut base = 0u64;
-            for &(ref region, attr_index) in identity_mapped_regions.iter() {
-                // println!("RAM Region: {:#x}..{:#x}", base, region.end);
-                // println!(
-                //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
-                //     (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
-                //     lvl1_vaddr_top,
-                //     lvl1_pt.iter().filter(|&&v| v != 0).count()
-                // );
-                // println!(
-                //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
-                //     (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)),
-                //     lvl2_vaddr_top,
-                //     lvl2_pt.iter().filter(|&&v| v != 0).count()
-                // );
-                // println!(
-                //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
-                //     (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
-                //     lvl3_vaddr_top,
-                //     lvl3_pt.iter().filter(|&&v| v != 0).count()
-                // );
-
-                // Handle the fact that the regions are not contiguous and that
-                // we might need to skip PT.
-
-                {
-                    if region.start >= lvl3_vaddr_top {
-                        if lvl3_pt != [0; _] {
-                            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
-                            // println!("[iter] Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
-                            assert!(lvl2_pt[lvl2_index(base)] == 0);
-                            lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
-                        }
-
-                        // TODO: just compute it.
-                        while region.start >= lvl3_vaddr_top {
-                            lvl3_vaddr_top += 1 << BLOCK_BITS_2MB;
-                        }
-                    }
-
-                    if region.start >= lvl2_vaddr_top {
-                        if lvl2_pt != [0; _] {
-                            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
-                            // println!("[iter] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
-                            assert!(lvl1_pt[lvl1_index(base)] == 0);
-                            lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
-                        }
-
-                        // TODO: just compute it.
-                        while region.start >= lvl2_vaddr_top {
-                            lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
-                        }
-                    }
-
-                    if region.start >= lvl1_vaddr_top {
-                        unreachable!(
-                            "impossible as everything should fit here: {lvl1_vaddr_top:#x}"
-                        );
-                    }
-                }
-
-                // After serialising the old base, update the new one.
-                base = region.start;
-
-                // Inner Loop:
-                // Invariant: the page tables in lvl1_pt, lvl2_pt, lvl3_pt
-                //            are either (1) for the current address range,
-                //            or (2) are empty and for a lower level than the current level.
-                //            Also, the values in lvlXXX_vaddr_top are always correct (even if empty)
-                //            Also contiguous within the loop.
-                // Loop entry: (1) holds by work at the start of each region
-                while base != region.end {
-                    // Condition is !=, but assert that we never skip it.
-                    assert!(base < region.end);
-
-                    let size_bits = region.end.wrapping_sub(base).ilog2();
-                    let align_bits = min(
-                        size_bits,
-                        // FIXME: Once MSRV is > 1.97, use .lowest_one() method.
-                        if base == 0 {
-                            size_bits
-                        } else {
-                            base.trailing_zeros()
-                        },
-                    );
-
-                    // Match the size and alignment of the current region to
-                    // the valid PT region sizes.
-                    let (level, bits) = match u64::from(align_bits) {
-                        BLOCK_BITS_1GB.. => (1, BLOCK_BITS_1GB),
-                        BLOCK_BITS_2MB.. => (2, BLOCK_BITS_2MB),
-                        PAGE_BITS_4KB.. => (3, PAGE_BITS_4KB),
-                        0.. => panic!("impossible; regions should be aligned to 4K at least"),
-                    };
-
-                    let pt_region_size = 1u64 << bits;
-                    let top = base + pt_region_size;
-
-                    // println!("- Aligned PT region: {:#x}..{:#x} (size_bits: {}, align_bits: {}, bits: {})", base, top, size_bits, align_bits, bits);
-                    // println!(
-                    //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
-                    //     (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
-                    //     lvl1_vaddr_top,
-                    //     lvl1_pt.iter().filter(|&&v| v != 0).count()
-                    // );
-                    // println!(
-                    //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
-                    //     (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)),
-                    //     lvl2_vaddr_top,
-                    //     lvl2_pt.iter().filter(|&&v| v != 0).count()
-                    // );
-                    // println!(
-                    //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
-                    //     (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
-                    //     lvl3_vaddr_top,
-                    //     lvl3_pt.iter().filter(|&&v| v != 0).count()
-                    // );
-
-                    match level {
-                        1 => {
-                            // If it belongs in Level 1 PT, then it must go in
-                            // lvl1 pt. By the inavariant, base < lvl1_vaddr_top.
-                            assert!(base < lvl1_vaddr_top);
-                            // top is <= lvl1_vaddr_top (the case where it is the topmost entry)
-                            assert!(top <= lvl1_vaddr_top);
-
-                            assert!(lvl1_pt[lvl1_index(base)] == 0);
-                            lvl1_pt[lvl1_index(base)] = block_descriptor(1, base, attr_index);
-
-                            if top == lvl1_vaddr_top {
-                                // Invariant maintenance: if the new top would be now equal
-                                // the end of the page table's region top, we need a new
-                                // page table object and add it to the list.
-
-                                // This should be possible to handle - we just need to break out of this loop
-                                todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
-                            }
-
-                            // Invariant: Lower levels are empty.
-                            assert!(lvl2_pt == [0; _]);
-                            assert!(lvl3_pt == [0; _]);
-                            // Invariant maintenance: vaddr_top is right range for current PT.
-                            // it's empty so we need to increment the top to be current top (1G aligned) + 2MIB (512 lvl3 entries)
-                            lvl3_vaddr_top = top + (1 << BLOCK_BITS_2MB);
-                            // it's empty so we need to increment the top to be current top (1G aligned) + 1G (512 lvl2 entries)
-                            lvl2_vaddr_top = top + (1 << BLOCK_BITS_1GB);
-                        }
-                        2 => {
-                            // If it is a 2MiB block, it must go in the Level 2 PT;
-                            // by our invariants: base < lvl2_vaddr_top and top <= lvl2_vaddr_top
-                            assert!(base < lvl2_vaddr_top);
-                            assert!(top <= lvl2_vaddr_top);
-
-                            assert!(lvl2_pt[lvl2_index(base)] == 0);
-                            lvl2_pt[lvl2_index(base)] = block_descriptor(2, base, attr_index);
-
-                            if top == lvl2_vaddr_top {
-                                // Invariant maintenance: keep for current address range.
-                                // As we're the top of the range, we can serialise the table.
-
-                                let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
-                                // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} up to {lvl2_vaddr_top:#x}");
-                                lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
-
-                                lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
-
-                                if top == lvl1_vaddr_top {
-                                    todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
-                                }
-                            }
-
-                            // Invariant: Lower levels are empty.
-                            assert!(lvl3_pt == [0; _]);
-                            // Invariant maintenance: vaddr_top is right range for current PT.
-                            // it's empty so we need to increment the top to be current top (2MIB aligned) + 2MIB (512 lvl3 entries)
-                            lvl3_vaddr_top = top + (1 << BLOCK_BITS_2MB);
-                        }
-                        3 => {
-                            // If it is a 4K page, it must go in the Level 3 PT;
-                            // by our invariants: base < lvl3_vaddr_top and top <= lvl3_vaddr_top
-                            assert!(base < lvl3_vaddr_top);
-                            assert!(top <= lvl3_vaddr_top);
-
-                            assert!(lvl3_pt[lvl3_index(base)] == 0);
-                            lvl3_pt[lvl3_index(base)] = page_descriptor(base, attr_index);
-
-                            if top == lvl3_vaddr_top {
-                                // Invariant maintenance: keep for current address range.
-                                // As we're the top of the range, we can serialise the table.
-
-                                let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
-                                // println!("Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
-                                lvl3_vaddr_top += 1 << BLOCK_BITS_2MB;
-
-                                assert!(lvl2_pt[lvl2_index(base)] == 0);
-                                lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
-
-                                if top == lvl2_vaddr_top {
-                                    let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
-                                    // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)));
-                                    lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
-
-                                    assert!(lvl1_pt[lvl1_index(base)] == 0);
-                                    lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
-
-                                    if top == lvl1_vaddr_top {
-                                        todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
-                                    }
-                                }
-                            }
-
-                            // Invariant: lower levels empty is vacuuously true
-                        }
-                        _ => unreachable!("level is 1..=3"),
-                    }
-
-                    base = base + pt_region_size;
-                }
-            }
-
-            // By the loop invariant, we know that anything before has been serialised.
-            // However, as we are at the end of the loop now, we might have
-            // page tables that have been partially filled out, and we need to
-            // serialise these.
-
-            if lvl3_pt != [0; _] {
-                let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
-                // println!("[end] Serialise lvl3 table: {lvl3_pt_paddr:#x}");
-                assert!(lvl2_pt[lvl2_index(base)] == 0);
-                lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
-            }
-
-            if lvl2_pt != [0; _] {
-                let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
-                // println!("[end] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
-                assert!(lvl1_pt[lvl1_index(base)] == 0);
-                lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
-            }
-
-            // the level1 pt should not be empty. lol.
-            assert!(lvl1_pt != [0; _]);
-
-            // println!("New lvl1 table");
-            serialise_page_table_to_paddr(&mut lvl1_pt)
-        };
-
-        // Depending on whether we are in hypervisor mode, we either need to
-        // return the TTBR0_EL2 or TTBR[0,1]_EL1 values. We return u64::MAX
-        // so as to return garbage - an unaligned address outside of physical
-        // memory.
-        if config.hypervisor {
-            // Manufacture the Level 0 table, containing the kernel table
-            // and the RAM tables.
-
-            let mut ttbr0_el2_pt = [0u64; PAGE_TABLE_ENTRIES];
-
-            assert!(lvl0_index(k) != lvl0_index(0));
-            ttbr0_el2_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
-            ttbr0_el2_pt[lvl0_index(0)] = table_descriptor(ram_lvl1_pt_paddr);
-
-            let ttbr0_el2 = serialise_page_table_to_paddr(&mut ttbr0_el2_pt);
-
-            (ttbr0_el2, u64::MAX, u64::MAX)
-        } else {
-            let mut ttbr0_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
-            let mut ttbr1_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
-
-            // Kernel in TTBR1 (Upper)
-            ttbr1_el1_pt[lvl0_index(k)] = table_descriptor(kernel_lvl1_pt_paddr);
-            // Identity-mapped RAM in TTBR0 (Lower)
-            ttbr0_el1_pt[lvl0_index(0)] = table_descriptor(ram_lvl1_pt_paddr);
-
-            let ttbr0_el1 = serialise_page_table_to_paddr(&mut ttbr0_el1_pt);
-            let ttbr1_el1 = serialise_page_table_to_paddr(&mut ttbr1_el1_pt);
-
-            (u64::MAX, ttbr0_el1, ttbr1_el1)
-        }
-    }
 }

From 30cc89eef743cb71ed677c16e9c9410775f3e4ac Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Wed, 29 Jul 2026 17:17:45 +1000
Subject: [PATCH 07/16] fixes

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/aarch64/mmu.c    |   8 +--
 loader/src/page_tables.rs   | 133 ++++++++++++++++++++++--------------
 tool/microkit/src/loader.rs |   3 +
 3 files changed, 88 insertions(+), 56 deletions(-)

diff --git a/loader/src/aarch64/mmu.c b/loader/src/aarch64/mmu.c
index 2fbdcc150..ad511615b 100644
--- a/loader/src/aarch64/mmu.c
+++ b/loader/src/aarch64/mmu.c
@@ -30,12 +30,10 @@ extern struct ret aarch64_setup_pagetables(uint64_t kernel_first_vaddr, uint64_t
 
 int arch_mmu_enable(int logical_cpu)
 {
-    puts("setup1\n");
     struct ret x = aarch64_setup_pagetables(0, 0, 0);
-    aarch64_pt_ttbr0_el1 = x.a;
-    aarch64_pt_ttbr1_el1 = x.b;
-    aarch64_pt_ttbr0_el2 = x.c;
-    puts("setup\n");
+    aarch64_pt_ttbr0_el2 = x.a;
+    aarch64_pt_ttbr0_el1 = x.b;
+    aarch64_pt_ttbr1_el1 = x.c;
 
     int r;
     enum el el;
diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index 31bcca1c9..d3ebfe3a1 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -622,9 +622,21 @@ pub extern "C" fn aarch64_setup_pagetables(
         table_descriptor, BLOCK_BITS_1GB, BLOCK_BITS_2MB, BLOCK_BITS_512GB, PAGE_BITS_4KB,
     };
 
+    let kernel_first_vaddr = 551366426624;
+    let kernel_first_paddr = 1610612736;
+
     const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
 
     let mut serialise_page_table_to_paddr = {
+        #[repr(align(4096))]
+        struct PtBytes([[u8; 4096]; 100]);
+        static mut PAGE_TABLE_BYTES: PtBytes = PtBytes([[0; _]; _]);
+        // SAFETY: Trust me (lol)
+        #[allow(static_mut_refs)]
+        let mut page_table_bytes = unsafe { &mut PAGE_TABLE_BYTES.0 };
+
+        let page_tables_paddr_start = &raw mut PAGE_TABLE_BYTES as u64;
+
         assert!(
             page_tables_paddr_start
                 == page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64)
@@ -632,11 +644,18 @@ pub extern "C" fn aarch64_setup_pagetables(
 
         // This maintains the current end of the PT array.
         let mut next_pt_paddr = page_tables_paddr_start;
+        let mut i = 0;
 
         move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
             let pt_paddr = next_pt_paddr;
-            // page_table_bytes.extend(page_table.iter().flat_map(|pte| pte.to_le_bytes()));
+            page_table
+                .iter()
+                .flat_map(|pte| pte.to_le_bytes())
+                .zip(page_table_bytes[i].iter_mut())
+                .for_each(|(byte, dest)| *dest = byte);
+
             next_pt_paddr += PAGE_TABLE_SIZE as u64;
+            i += 0;
             page_table.fill(0);
             pt_paddr
         }
@@ -646,52 +665,64 @@ pub extern "C" fn aarch64_setup_pagetables(
         start: u64,
         end: u64,
     }
+    let ram_regions = [
+        Region { start: 0x60000000, end: 0xc0000000 },
+    ];
+
+    const MAX_NUM_REGIONS: usize = 16;
+
+    let mut regions = [const { core::mem::MaybeUninit::uninit() }; MAX_NUM_REGIONS];
+    let identity_mapped_regions: &mut [(Region, _)] = {
+        // Conceptually want we want is an 'arrayvec', but to not pull in more
+        // code we implement this less-efficiently MaybeUninit.
+        // We implement something very similar to the currently-unstable
+        // write_iter implementation:
+        // https://github.com/rust-lang/rust/blob/1.97.1/library/core/src/mem/maybe_uninit.rs#L1384-L1406
+        let mut regions_len = 0;
+
+        assert!(ram_regions.len() <= regions.len());
+
+        let ram_regions_it = ram_regions.into_iter().map(|r| (r, MT_DEVICE_nGnRnE));
+
+        let all_regions_it = ram_regions_it.chain([(Region { start: 0x9000000, end: 0x9001000 }, MT_DEVICE_nGnRnE)]);
+
+        //     // FIXME: Derive from the kernel build system.
+        //     if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
+        //         let uart_base = align_down(uart_base, PAGE_BITS_4KB);
+        //         regions.push((
+        //             PlatformConfigRegion {
+        //                 start: uart_base,
+        //                 end: uart_base + (1 << PAGE_BITS_4KB),
+        //             },
+        //             MT_DEVICE_nGnRnE,
+        //         ));
+        //     }
+        //     // FIXME: This is currently assuming implementation details of the BCM2711/
+        //     //        Raspberry Pi 4B spin table implementation, as it is the only
+        //     //        platform we have that uses spin tables. Specifically, that
+        //     //        it is always located at the 0 page.
+        //     if elf.find_symbol("cpus_release_addr").is_ok() {
+        //         regions.push((
+        //             PlatformConfigRegion {
+        //                 start: 0x0,
+        //                 end: 1 << PAGE_BITS_4KB,
+        //             },
+        //             MT_DEVICE_nGnRnE,
+        //         ));
+        //     }
+
+        for (entry, region) in regions.iter_mut().zip(all_regions_it) {
+            entry.write(region);
+            regions_len += 1;
+        }
+
+        let regions = unsafe { (&mut regions[0..regions_len]).assume_init_mut() };
 
-    let identity_mapped_regions: &[(Region, u64)] = &[];
-    // let identity_mapped_regions = {
-    //     let ram_regions = config
-    //         .normal_regions
-    //         .as_ref()
-    //         .expect("AArch64 should have normal_regions");
-
-    //     // println!("{:#x?}", ram_regions);
-
-    //     let mut regions: Vec<_> = ram_regions
-    //         .iter()
-    //         .cloned()
-    //         .map(|region| (region, MT_DEVICE_nGnRnE))
-    //         .collect();
-
-    //     // FIXME: Derive from the kernel build system.
-    //     if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
-    //         let uart_base = align_down(uart_base, PAGE_BITS_4KB);
-    //         regions.push((
-    //             PlatformConfigRegion {
-    //                 start: uart_base,
-    //                 end: uart_base + (1 << PAGE_BITS_4KB),
-    //             },
-    //             MT_DEVICE_nGnRnE,
-    //         ));
-    //     }
-
-    //     // FIXME: This is currently assuming implementation details of the BCM2711/
-    //     //        Raspberry Pi 4B spin table implementation, as it is the only
-    //     //        platform we have that uses spin tables. Specifically, that
-    //     //        it is always located at the 0 page.
-    //     if elf.find_symbol("cpus_release_addr").is_ok() {
-    //         regions.push((
-    //             PlatformConfigRegion {
-    //                 start: 0x0,
-    //                 end: 1 << PAGE_BITS_4KB,
-    //             },
-    //             MT_DEVICE_nGnRnE,
-    //         ));
-    //     }
-
-    //     regions.sort_by_key(|(region, _)| region.start);
-
-    //     regions
-    // };
+        // Need to use 'sort_unstable_by_key' as sort_by_key is not in-place.
+        regions.sort_unstable_by_key(|(region, _)| region.start);
+
+        regions
+    };
 
     // Manufacture the constants as per the diagram.
     let k = align_down(kernel_first_vaddr, BLOCK_BITS_512GB);
@@ -750,7 +781,7 @@ pub extern "C" fn aarch64_setup_pagetables(
         // top value we rotate to a new PT.
 
         struct PageTableConstructor<const LEVELS: usize, const ENTRIES: usize, PTE, Addr> {
-            invalid: PTE,
+            empty: PTE,
             levels: [[PTE; ENTRIES]; LEVELS],
             level_top: [Addr; LEVELS],
         }
@@ -758,10 +789,10 @@ pub extern "C" fn aarch64_setup_pagetables(
         impl<const LEVELS: usize, const ENTRIES: usize, PTE: Copy + PartialEq, Addr>
             PageTableConstructor<LEVELS, ENTRIES, PTE, Addr>
         {
-            const fn new(invalid: PTE, level_top: [Addr; LEVELS]) -> Self {
+            const fn new(empty: PTE, level_top: [Addr; LEVELS]) -> Self {
                 Self {
-                    invalid,
-                    levels: [[invalid; ENTRIES]; LEVELS],
+                    empty,
+                    levels: [[empty; ENTRIES]; LEVELS],
                     level_top: level_top,
                 }
             }
@@ -778,7 +809,7 @@ pub extern "C" fn aarch64_setup_pagetables(
 
             fn lvl_is_empty(&self, lvl: usize) -> bool {
                 assert!(lvl < LEVELS);
-                self.levels[lvl] != [self.invalid; ENTRIES]
+                self.levels[lvl] == [self.empty; ENTRIES]
             }
         }
 
diff --git a/tool/microkit/src/loader.rs b/tool/microkit/src/loader.rs
index 2c12b1101..860caca70 100644
--- a/tool/microkit/src/loader.rs
+++ b/tool/microkit/src/loader.rs
@@ -159,6 +159,9 @@ impl<'a> Loader<'a> {
         // the return object.
         let loader_image = image_segment.data().clone();
 
+        println!("kernel_first_vaddr: {kernel_first_vaddr:?}");
+        println!("kernel_first_paddr: {kernel_first_paddr:?}");
+
         if image_vaddr != loader_elf.entry {
             panic!("The loader entry point must be the first byte in the image");
         }

From aaaa69a0f4c60b2be145293a12b7b27611c0b5ef Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Wed, 29 Jul 2026 17:25:07 +1000
Subject: [PATCH 08/16] back to old style

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/page_tables.rs | 314 +++++++++++++++++++-------------------
 1 file changed, 156 insertions(+), 158 deletions(-)

diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index d3ebfe3a1..00e8cad4e 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -549,6 +549,43 @@ pub extern "C" fn riscv64_setup_pagetables(
     serialise_page_table_to_paddr(&mut boot_lvl1_pt)
 }
 
+pub struct Writer;
+
+impl fmt::Write for Writer {
+    fn write_str(&mut self, s: &str) -> Result<(), fmt::Error> {
+        for c in s.bytes() {
+            unsafe {
+                puts(core::ffi::CStr::from_bytes_with_nul_unchecked(&[c.into(), 0]).as_ptr())
+            };
+        }
+        Ok(())
+    }
+}
+
+#[allow(unused)]
+pub fn print(args: fmt::Arguments) {
+    use fmt::Write;
+    Writer{}.write_fmt(args).unwrap();
+}
+
+#[macro_export]
+macro_rules! print {
+    ($($arg:tt)*) => {{
+        print(format_args!($($arg)*));
+    }}
+}
+
+#[macro_export]
+macro_rules! println {
+    () => {{
+        print!("\n");
+    }};
+
+    ($($arg:tt)*) => {{
+        print!("{}\n", format_args!($($arg)*));
+    }}
+}
+
 /// AArch64 loader page tables have two variations:
 ///  - Loader in EL2, then Stage 1 translations in use, so we have the
 ///    singular TTBR0_EL2 register containing the Level 0 table;
@@ -780,54 +817,15 @@ pub extern "C" fn aarch64_setup_pagetables(
         // When the current vaddr (/paddr, as identity mapped) exceeds the
         // top value we rotate to a new PT.
 
-        struct PageTableConstructor<const LEVELS: usize, const ENTRIES: usize, PTE, Addr> {
-            empty: PTE,
-            levels: [[PTE; ENTRIES]; LEVELS],
-            level_top: [Addr; LEVELS],
-        }
-
-        impl<const LEVELS: usize, const ENTRIES: usize, PTE: Copy + PartialEq, Addr>
-            PageTableConstructor<LEVELS, ENTRIES, PTE, Addr>
-        {
-            const fn new(empty: PTE, level_top: [Addr; LEVELS]) -> Self {
-                Self {
-                    empty,
-                    levels: [[empty; ENTRIES]; LEVELS],
-                    level_top: level_top,
-                }
-            }
-
-            fn lvl(&mut self, lvl: usize) -> &mut [PTE; ENTRIES] {
-                assert!(lvl < LEVELS);
-                &mut self.levels[lvl]
-            }
-
-            fn lvl_top(&mut self, lvl: usize) -> &mut Addr {
-                assert!(lvl < LEVELS);
-                &mut self.level_top[lvl]
-            }
-
-            fn lvl_is_empty(&self, lvl: usize) -> bool {
-                assert!(lvl < LEVELS);
-                self.levels[lvl] == [self.empty; ENTRIES]
-            }
-        }
-
-        static mut PTS: PageTableConstructor<4, PAGE_TABLE_ENTRIES, u64, u64> =
-            PageTableConstructor::new(
-                0,
-                [
-                    u64::MAX,
-                    1 << BLOCK_BITS_512GB,
-                    1 << BLOCK_BITS_1GB,
-                    1 << BLOCK_BITS_2MB,
-                ],
-            );
-
-        // SAFETY: Trust me. This function is not, and can not, be reentrant,
-        // and more than that, can only be called once.
-        #[allow(static_mut_refs)]
-        let pts = unsafe { &mut PTS };
+        let mut lvl1_pt = [0u64; PAGE_TABLE_ENTRIES];
+        let mut lvl2_pt = [0u64; PAGE_TABLE_ENTRIES];
+        let mut lvl3_pt = [0u64; PAGE_TABLE_ENTRIES];
+        // TODO: These should be defines. Note that the top is the size of 1 level of the next level up.
+        // TODO: LVL1_ENTRY_RANGE? idk
+        #[allow(unused_mut)]
+        let mut lvl1_vaddr_top = 1 << BLOCK_BITS_512GB;
+        let mut lvl2_vaddr_top = 1 << BLOCK_BITS_1GB;
+        let mut lvl3_vaddr_top = 1 << BLOCK_BITS_2MB;
 
         // TODO: Tests...
         // This is similar to aligned_power_of_two_regions() for the kernel UT,
@@ -837,62 +835,62 @@ pub extern "C" fn aarch64_setup_pagetables(
         // Allowed externally for the final iteration
         let mut base = 0u64;
         for &(ref region, attr_index) in identity_mapped_regions.iter() {
-            // println!("RAM Region: {:#x}..{:#x}", base, region.end);
-            // println!(
-            //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
-            //     (*pts.lvl_top(1) - (1 << BLOCK_BITS_512GB)),
-            //     *pts.lvl_top(1),
-            //     lvl1_pt.iter().filter(|&&v| v != 0).count()
-            // );
-            // println!(
-            //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
-            //     (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)),
-            //     *pts.lvl_top(2),
-            //     lvl2_pt.iter().filter(|&&v| v != 0).count()
-            // );
-            // println!(
-            //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
-            //     (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
-            //     lvl3_vaddr_top,
-            //     lvl3_pt.iter().filter(|&&v| v != 0).count()
-            // );
+            println!("RAM Region: {:#x}..{:#x}", base, region.end);
+            println!(
+                "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
+                (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
+                lvl1_vaddr_top,
+                lvl1_pt.iter().filter(|&&v| v != 0).count()
+            );
+            println!(
+                "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
+                (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)),
+                lvl2_vaddr_top,
+                lvl2_pt.iter().filter(|&&v| v != 0).count()
+            );
+            println!(
+                "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
+                (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
+                lvl3_vaddr_top,
+                lvl3_pt.iter().filter(|&&v| v != 0).count()
+            );
 
             // Handle the fact that the regions are not contiguous and that
             // we might need to skip PT.
 
             {
-                if region.start >= *pts.lvl_top(3) {
-                    if !pts.lvl_is_empty(3) {
-                        let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(3));
-                        // println!("[iter] Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{pts.lvl_top(3):#x}", (pts.lvl_top(3) - (1 << BLOCK_BITS_2MB)));
-                        assert!(pts.lvl(2)[lvl2_index(base)] == 0);
-                        pts.lvl(2)[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+                if region.start >= lvl3_vaddr_top {
+                    if lvl3_pt != [0; _] {
+                        let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
+                        println!("[iter] Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
+                        assert!(lvl2_pt[lvl2_index(base)] == 0);
+                        lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
                     }
 
                     // TODO: just compute it.
-                    while region.start >= *pts.lvl_top(3) {
-                        *pts.lvl_top(3) += 1 << BLOCK_BITS_2MB;
+                    while region.start >= lvl3_vaddr_top {
+                        lvl3_vaddr_top += 1 << BLOCK_BITS_2MB;
                     }
                 }
 
-                if region.start >= *pts.lvl_top(2) {
-                    if !pts.lvl_is_empty(2) {
-                        let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
-                        // println!("[iter] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{*pts.lvl_top(2):#x}, base: {:#x} lvl1_index(base): {:#x}", (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
-                        assert!(pts.lvl(1)[lvl1_index(base)] == 0);
-                        pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+                if region.start >= lvl2_vaddr_top {
+                    if lvl2_pt != [0; _] {
+                        let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+                        println!("[iter] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+                        assert!(lvl1_pt[lvl1_index(base)] == 0);
+                        lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
                     }
 
                     // TODO: just compute it.
-                    while region.start >= *pts.lvl_top(2) {
-                        *pts.lvl_top(2) += 1 << BLOCK_BITS_1GB;
+                    while region.start >= lvl2_vaddr_top {
+                        lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
                     }
                 }
 
-                if region.start >= *pts.lvl_top(1) {
+                if region.start >= lvl1_vaddr_top {
                     unreachable!(
                         "impossible as everything should fit here: {:#x}",
-                        *pts.lvl_top(1)
+                        lvl1_vaddr_top
                     );
                 }
             }
@@ -934,38 +932,38 @@ pub extern "C" fn aarch64_setup_pagetables(
                 let pt_region_size = 1u64 << bits;
                 let top = base + pt_region_size;
 
-                // println!("- Aligned PT region: {:#x}..{:#x} (size_bits: {}, align_bits: {}, bits: {})", base, top, size_bits, align_bits, bits);
-                // println!(
-                //     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
-                //     (*pts.lvl_top(1) - (1 << BLOCK_BITS_512GB)),
-                //     *pts.lvl_top(1),
-                //     lvl1_pt.iter().filter(|&&v| v != 0).count()
-                // );
-                // println!(
-                //     "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
-                //     (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)),
-                //     *pts.lvl_top(2),
-                //     lvl2_pt.iter().filter(|&&v| v != 0).count()
-                // );
-                // println!(
-                //     "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
-                //     (pts.lvl_top(3) - (1 << BLOCK_BITS_2MB)),
-                //     pts.lvl_top(3),
-                //     lvl3_pt.iter().filter(|&&v| v != 0).count()
-                // );
+                println!("- Aligned PT region: {:#x}..{:#x} (size_bits: {}, align_bits: {}, bits: {})", base, top, size_bits, align_bits, bits);
+                println!(
+                    "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
+                    (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
+                    lvl1_vaddr_top,
+                    lvl1_pt.iter().filter(|&&v| v != 0).count()
+                );
+                println!(
+                    "  - Current Lvl2: {:#x}..{:#x}, entries: {}",
+                    (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)),
+                    lvl2_vaddr_top,
+                    lvl2_pt.iter().filter(|&&v| v != 0).count()
+                );
+                println!(
+                    "  - Current Lvl3: {:#x}..{:#x}, entries: {}",
+                    (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)),
+                    lvl3_vaddr_top,
+                    lvl3_pt.iter().filter(|&&v| v != 0).count()
+                );
 
                 match level {
                     1 => {
                         // If it belongs in Level 1 PT, then it must go in
-                        // lvl1 pt. By the inavariant, base < *pts.lvl_top(1).
-                        assert!(base < *pts.lvl_top(1));
-                        // top is <= *pts.lvl_top(1) (the case where it is the topmost entry)
-                        assert!(top <= *pts.lvl_top(1));
+                        // lvl1 pt. By the inavariant, base < lvl1_vaddr_top.
+                        assert!(base < lvl1_vaddr_top);
+                        // top is <= lvl1_vaddr_top (the case where it is the topmost entry)
+                        assert!(top <= lvl1_vaddr_top);
 
-                        assert!(pts.lvl(1)[lvl1_index(base)] == 0);
-                        pts.lvl(1)[lvl1_index(base)] = block_descriptor(1, base, attr_index);
+                        assert!(lvl1_pt[lvl1_index(base)] == 0);
+                        lvl1_pt[lvl1_index(base)] = block_descriptor(1, base, attr_index);
 
-                        if top == *pts.lvl_top(1) {
+                        if top == lvl1_vaddr_top {
                             // Invariant maintenance: if the new top would be now equal
                             // the end of the page table's region top, we need a new
                             // page table object and add it to the list.
@@ -975,73 +973,73 @@ pub extern "C" fn aarch64_setup_pagetables(
                         }
 
                         // Invariant: Lower levels are empty.
-                        assert!(pts.lvl_is_empty(2));
-                        assert!(pts.lvl_is_empty(3));
+                        assert!(lvl2_pt == [0; _]);
+                        assert!(lvl3_pt == [0; _]);
                         // Invariant maintenance: vaddr_top is right range for current PT.
                         // it's empty so we need to increment the top to be current top (1G aligned) + 2MIB (512 lvl3 entries)
-                        *pts.lvl_top(3) = top + (1 << BLOCK_BITS_2MB);
+                        lvl3_vaddr_top = top + (1 << BLOCK_BITS_2MB);
                         // it's empty so we need to increment the top to be current top (1G aligned) + 1G (512 lvl2 entries)
-                        *pts.lvl_top(2) = top + (1 << BLOCK_BITS_1GB);
+                        lvl2_vaddr_top = top + (1 << BLOCK_BITS_1GB);
                     }
                     2 => {
                         // If it is a 2MiB block, it must go in the Level 2 PT;
-                        // by our invariants: base < *pts.lvl_top(2) and top <= *pts.lvl_top(2)
-                        assert!(base < *pts.lvl_top(2));
-                        assert!(top <= *pts.lvl_top(2));
+                        // by our invariants: base < lvl2_vaddr_top and top <= lvl2_vaddr_top
+                        assert!(base < lvl2_vaddr_top);
+                        assert!(top <= lvl2_vaddr_top);
 
-                        assert!(pts.lvl(2)[lvl2_index(base)] == 0);
-                        pts.lvl(2)[lvl2_index(base)] = block_descriptor(2, base, attr_index);
+                        assert!(lvl2_pt[lvl2_index(base)] == 0);
+                        lvl2_pt[lvl2_index(base)] = block_descriptor(2, base, attr_index);
 
-                        if top == *pts.lvl_top(2) {
+                        if top == lvl2_vaddr_top {
                             // Invariant maintenance: keep for current address range.
                             // As we're the top of the range, we can serialise the table.
 
-                            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
-                            // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} up to {*pts.lvl_top(2):#x}");
-                            *pts.lvl_top(2) += 1 << BLOCK_BITS_1GB;
+                            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+                            // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} up to {lvl2_vaddr_top:#x}");
+                            lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
 
-                            pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+                            lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
 
-                            if top == *pts.lvl_top(1) {
+                            if top == lvl1_vaddr_top {
                                 todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
                             }
                         }
 
                         // Invariant: Lower levels are empty.
-                        assert!(pts.lvl_is_empty(3));
+                        assert!(lvl3_pt == [0; _]);
                         // Invariant maintenance: vaddr_top is right range for current PT.
                         // it's empty so we need to increment the top to be current top (2MIB aligned) + 2MIB (512 lvl3 entries)
-                        *pts.lvl_top(3) = top + (1 << BLOCK_BITS_2MB);
+                        lvl3_vaddr_top = top + (1 << BLOCK_BITS_2MB);
                     }
                     3 => {
                         // If it is a 4K page, it must go in the Level 3 PT;
-                        // by our invariants: base < pts.lvl_top(3) and top <= pts.lvl_top(3)
-                        assert!(base < *pts.lvl_top(3));
-                        assert!(top <= *pts.lvl_top(3));
+                        // by our invariants: base < lvl3_vaddr_top and top <= lvl3_vaddr_top
+                        assert!(base < lvl3_vaddr_top);
+                        assert!(top <= lvl3_vaddr_top);
 
-                        assert!(pts.lvl(3)[lvl3_index(base)] == 0);
-                        pts.lvl(3)[lvl3_index(base)] = page_descriptor(base, attr_index);
+                        assert!(lvl3_pt[lvl3_index(base)] == 0);
+                        lvl3_pt[lvl3_index(base)] = page_descriptor(base, attr_index);
 
-                        if top == *pts.lvl_top(3) {
+                        if top == lvl3_vaddr_top {
                             // Invariant maintenance: keep for current address range.
                             // As we're the top of the range, we can serialise the table.
 
-                            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(3));
-                            // println!("Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{pts.lvl_top(3):#x}", (pts.lvl_top(3) - (1 << BLOCK_BITS_2MB)));
-                            *pts.lvl_top(3) += 1 << BLOCK_BITS_2MB;
+                            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
+                            println!("Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
+                            lvl3_vaddr_top += 1 << BLOCK_BITS_2MB;
 
-                            assert!(pts.lvl(2)[lvl2_index(base)] == 0);
-                            pts.lvl(2)[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+                            assert!(lvl2_pt[lvl2_index(base)] == 0);
+                            lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
 
-                            if top == *pts.lvl_top(2) {
-                                let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
-                                // println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{*pts.lvl_top(2):#x}", (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)));
-                                *pts.lvl_top(2) += 1 << BLOCK_BITS_1GB;
+                            if top == lvl2_vaddr_top {
+                                let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+                                println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)));
+                                lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
 
-                                assert!(pts.lvl(1)[lvl1_index(base)] == 0);
-                                pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+                                assert!(lvl1_pt[lvl1_index(base)] == 0);
+                                lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
 
-                                if top == *pts.lvl_top(1) {
+                                if top == lvl1_vaddr_top {
                                     todo!("handle the case where top of lvl1 is occupied - this would be near the top of 512GiB");
                                 }
                             }
@@ -1061,25 +1059,25 @@ pub extern "C" fn aarch64_setup_pagetables(
         // page tables that have been partially filled out, and we need to
         // serialise these.
 
-        if !pts.lvl_is_empty(3) {
-            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(3));
-            // println!("[end] Serialise lvl3 table: {lvl3_pt_paddr:#x}");
-            assert!(pts.lvl(2)[lvl2_index(base)] == 0);
-            pts.lvl(2)[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
+        if lvl3_pt != [0; _] {
+            let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
+            println!("[end] Serialise lvl3 table: {lvl3_pt_paddr:#x}");
+            assert!(lvl2_pt[lvl2_index(base)] == 0);
+            lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
         }
 
-        if !pts.lvl_is_empty(2) {
-            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut pts.lvl(2));
-            // println!("[end] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{*pts.lvl_top(2):#x}, base: {:#x} lvl1_index(base): {:#x}", (*pts.lvl_top(2) - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
-            assert!(pts.lvl(1)[lvl1_index(base)] == 0);
-            pts.lvl(1)[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
+        if lvl2_pt != [0; _] {
+            let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
+            println!("[end] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+            assert!(lvl1_pt[lvl1_index(base)] == 0);
+            lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
         }
 
         // the level1 pt should not be empty. lol.
-        assert!(!pts.lvl_is_empty(1));
+        assert!(lvl1_pt != [0; _]);
 
         // println!("New lvl1 table");
-        serialise_page_table_to_paddr(pts.lvl(1))
+        serialise_page_table_to_paddr(&mut lvl1_pt)
     };
 
     struct Config {

From 807aa036a72635adc7355643e7c8f442590d4be6 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Wed, 29 Jul 2026 17:35:47 +1000
Subject: [PATCH 09/16] FIX

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/page_tables.rs | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index 00e8cad4e..e451ebd56 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -685,14 +685,12 @@ pub extern "C" fn aarch64_setup_pagetables(
 
         move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
             let pt_paddr = next_pt_paddr;
-            page_table
-                .iter()
-                .flat_map(|pte| pte.to_le_bytes())
-                .zip(page_table_bytes[i].iter_mut())
-                .for_each(|(byte, dest)| *dest = byte);
+            for (j, byte) in page_table.iter().flat_map(|pte| pte.to_le_bytes()).enumerate() {
+                page_table_bytes[i][j] = byte;
+            }
 
             next_pt_paddr += PAGE_TABLE_SIZE as u64;
-            i += 0;
+            i += 1;
             page_table.fill(0);
             pt_paddr
         }

From 8a87d9da27f34601cba6ad2ce34ac4128c0e1eea Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Fri, 31 Jul 2026 16:32:01 +1000
Subject: [PATCH 10/16] minor makefile touchups

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/Makefile | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/loader/Makefile b/loader/Makefile
index dd78ce5d9..50d0e31a3 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -86,9 +86,9 @@ $(BUILD_DIR)/%.o : src/$(ARCH_DIR)/%.c
 $(BUILD_DIR)/%.o : src/%.c
 	$(CC) -c $(CFLAGS) $< -o $@
 
-# Note: having multiple rlib with staticlib will give duplicate linker symbol
+# Note: having multiple libs with staticlib will give duplicate linker symbol
 # issues. Use "--crate-type rlib" instead, but then we need to link a single
-# copy of the rust corelibs.
+# copy of the rust corelibs. For now this is fine.
 $(BUILD_DIR)/lib%.a : src/%.rs
 	$(RUSTC) $(RUSTFLAGS) \
 		--emit dep-info,metadata,link \
@@ -98,7 +98,6 @@ $(BUILD_DIR)/lib%.a : src/%.rs
 		$<
 
 -include $(BUILD_DIR)/*.d
--include $(BUILD_DIR)/mmu.d
 
 OBJPROG = $(addprefix $(BUILD_DIR)/, $(PROGS))
 

From 0890270817d100818320f02b4817261c2df9d7e5 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Tue, 18 Aug 2026 12:11:16 +1000
Subject: [PATCH 11/16] tests + return struct

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/Makefile           |  13 ++-
 loader/src/c_interop.rs   |  75 +++++++++++++
 loader/src/page_tables.rs | 214 ++++++++++++++++++--------------------
 3 files changed, 187 insertions(+), 115 deletions(-)
 create mode 100644 loader/src/c_interop.rs

diff --git a/loader/Makefile b/loader/Makefile
index 50d0e31a3..376e68849 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -58,7 +58,7 @@ CFLAGS := -std=gnu11 -g -O3 -nostdlib -ffreestanding \
 
 ASM_FLAGS := $(ASM_FLAGS_ARCH) -g -MP -MD -I$(SEL4_SDK)/include
 
-RUSTFLAGS := --target $(RUST_TARGET_TRIPLE) --edition 2024 -g -C opt-level=2
+RUSTFLAGS := --edition 2024 -g -C opt-level=2
 
 PROGS := loader.elf
 OBJECTS := loader.o crt0.o uart.o cutil.o libpage_tables.a
@@ -93,6 +93,7 @@ $(BUILD_DIR)/lib%.a : src/%.rs
 	$(RUSTC) $(RUSTFLAGS) \
 		--emit dep-info,metadata,link \
 		--out-dir $(BUILD_DIR) -L dependency=$(BUILD_DIR) \
+		--target $(RUST_TARGET_TRIPLE) \
 		--crate-type staticlib \
 		--crate-name $(patsubst lib%.a,%,$(notdir $@)) \
 		$<
@@ -101,7 +102,7 @@ $(BUILD_DIR)/lib%.a : src/%.rs
 
 OBJPROG = $(addprefix $(BUILD_DIR)/, $(PROGS))
 
-all: $(OBJPROG)
+all: $(OBJPROG) test
 
 $(LINKSCRIPT): $(LINKSCRIPT_INPUT)
 	$(CPP) -DLINK_ADDRESS=$(LINK_ADDRESS) $< | grep -v "^#" > $@
@@ -111,3 +112,11 @@ LDFLAGS := -T$(LINKSCRIPT) --gc-sections
 $(OBJPROG): $(addprefix $(BUILD_DIR)/, $(OBJECTS)) $(LINKSCRIPT)
 	$(LD) $(LDFLAGS) --start-group $(addprefix $(BUILD_DIR)/, $(OBJECTS)) --end-group -o $@
 
+test:
+	$(RUSTC) $(RUSTFLAGS) \
+		--emit dep-info,metadata,link \
+		--out-dir $(BUILD_DIR) -L dependency=$(BUILD_DIR) \
+		--test \
+		--crate-name test_page_tables \
+		src/page_tables.rs
+	$(BUILD_DIR)/test_page_tables
diff --git a/loader/src/c_interop.rs b/loader/src/c_interop.rs
new file mode 100644
index 000000000..8fd6b7406
--- /dev/null
+++ b/loader/src/c_interop.rs
@@ -0,0 +1,75 @@
+#[cfg(not(test))]
+mod real_hardware {
+    use core::ffi::c_char;
+    use core::ffi::CStr;
+    use core::fmt;
+    use core::fmt::Write;
+    use core::panic::PanicInfo;
+
+    unsafe extern "C" {
+        safe fn fail() -> !;
+        // safe fn putc(c: c_char);
+        unsafe fn puts(s: *const c_char);
+    }
+
+    /// Exposed only for print macro.
+    #[doc(hidden)]
+    pub(crate) struct Writer;
+
+    impl fmt::Write for Writer {
+        fn write_str(&mut self, s: &str) -> Result<(), fmt::Error> {
+            for c in s.bytes() {
+                unsafe {
+                    puts(CStr::from_bytes_with_nul_unchecked(&[c.into(), 0]).as_ptr())
+                };
+            }
+            Ok(())
+        }
+    }
+
+    #[macro_export]
+    macro_rules! __print {
+        ($($arg:tt)*) => {{
+            use core::fmt::Write;
+            $crate::c_interop::Writer{}.write_fmt(format_args!($($arg)*)).unwrap()
+        }}
+    }
+
+    #[macro_export]
+    macro_rules! __println {
+        () => {{
+            $crate::__print!("\n");
+        }};
+
+        ($($arg:tt)*) => {{
+            $crate::__print!("{}\n", format_args!($($arg)*));
+        }}
+    }
+
+    pub(crate) use __println as println;
+
+    #[panic_handler]
+    fn panic(info: &PanicInfo) -> ! {
+        println!("panicked");
+
+        if let Err(_) = writeln!(Writer, "{}", info) {
+            // If writeln!() fails (which it should never as our fmt::Write) never
+            // fails, then just don't print the extra information.
+            println!("panicked (information unknown)");
+        }
+
+        fail();
+    }
+}
+
+#[cfg(test)]
+mod for_tests {
+    extern crate std;
+    pub(crate) use std::println;
+}
+
+#[cfg(test)]
+pub(crate) use for_tests::*;
+
+#[cfg(not(test))]
+pub(crate) use real_hardware::*;
diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index e451ebd56..b98b626d1 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -6,44 +6,13 @@
 
 #![no_std]
 
+mod c_interop;
+
 use core::cmp::min;
-use core::ffi::c_char;
-use core::fmt;
-use core::fmt::Write;
 use core::mem;
-use core::panic::PanicInfo;
-
-unsafe extern "C" {
-    safe fn fail() -> !;
-    // safe fn putc(c: c_char);
-    unsafe fn puts(s: *const c_char);
-}
-
-#[panic_handler]
-fn panic(info: &PanicInfo) -> ! {
-    unsafe { puts(c"panicked\n".as_ptr()) };
-
-    struct DebugWriter;
-    impl fmt::Write for DebugWriter {
-        fn write_str(&mut self, s: &str) -> fmt::Result {
-            for c in s.bytes() {
-                unsafe {
-                    puts(core::ffi::CStr::from_bytes_with_nul_unchecked(&[c.into(), 0]).as_ptr())
-                };
-            }
-
-            Ok(())
-        }
-    }
+use core::mem::MaybeUninit;
 
-    if let Err(_) = writeln!(DebugWriter, "{}", info) {
-        // If writeln!() fails (which it should never as our fmt::Write) never
-        // fails, then just don't print the extra information.
-        unsafe { puts(c"panicked (information unknown)\n".as_ptr()) };
-    }
-
-    fail();
-}
+use c_interop::println;
 
 const PAGE_TABLE_SIZE: usize = 4096;
 
@@ -55,15 +24,6 @@ const fn mask(n: u64) -> u64 {
     (1 << n) - 1
 }
 
-const fn round_up(n: u64, x: u64) -> u64 {
-    let (_, m) = divmod(n, x);
-    if m == 0 {
-        n
-    } else {
-        n + x - m
-    }
-}
-
 const fn round_down(n: u64, x: u64) -> u64 {
     let (_, m) = divmod(n, x);
     if m == 0 {
@@ -73,10 +33,6 @@ const fn round_down(n: u64, x: u64) -> u64 {
     }
 }
 
-const fn align_up(n: u64, bits: u64) -> u64 {
-    round_up(n, 1 << bits)
-}
-
 const fn align_down(n: u64, bits: u64) -> u64 {
     round_down(n, 1 << bits)
 }
@@ -91,7 +47,7 @@ pub mod aarch64 {
     //! Stage 2 descriptors are only used when in the EL1&0 regime; which is not
     //! the case when in EL2.
 
-    use crate::mask;
+    use super::*;
 
     pub const LVL0_BITS: u64 = 9;
     pub const LVL1_BITS: u64 = 9;
@@ -299,9 +255,11 @@ pub mod aarch64 {
     /// Per "Table D8-50 Stage 1 VMSAv8-64 Table descriptor fields" and
     /// "Figure D8-12 VMSAv8-64 Table descriptor formats" of ARM DDI0487L.b;
     /// specifically subfigure "4KB, 16KB, and 64KB granules, 48-bit OA"
-    pub fn table_descriptor(addr: u64) -> u64 {
+    pub fn table_descriptor(addr: *const u8) -> u64 {
         // Per Table D8-48, Condition for descriptor_type::TABLE is level != 3.
 
+        let addr: u64 = addr.addr().try_into().expect("usize in u64");
+
         // We don't set any of these attributes, most are hardware-feature conditional
         let attributes: u64 = 0;
 
@@ -549,41 +507,18 @@ pub extern "C" fn riscv64_setup_pagetables(
     serialise_page_table_to_paddr(&mut boot_lvl1_pt)
 }
 
-pub struct Writer;
-
-impl fmt::Write for Writer {
-    fn write_str(&mut self, s: &str) -> Result<(), fmt::Error> {
-        for c in s.bytes() {
-            unsafe {
-                puts(core::ffi::CStr::from_bytes_with_nul_unchecked(&[c.into(), 0]).as_ptr())
-            };
-        }
-        Ok(())
-    }
+/// Note that "0" is a valid return value; instead the invalid value is
+/// '-1', or usize::MAX.
+#[repr(C)]
+#[derive(Debug)]
+pub struct AArch64ReturnValue {
+    ttbr0_el2: *const u8,
+    ttbr0_el1: *const u8,
+    ttbr1_el1: *const u8,
 }
 
-#[allow(unused)]
-pub fn print(args: fmt::Arguments) {
-    use fmt::Write;
-    Writer{}.write_fmt(args).unwrap();
-}
-
-#[macro_export]
-macro_rules! print {
-    ($($arg:tt)*) => {{
-        print(format_args!($($arg)*));
-    }}
-}
-
-#[macro_export]
-macro_rules! println {
-    () => {{
-        print!("\n");
-    }};
-
-    ($($arg:tt)*) => {{
-        print!("{}\n", format_args!($($arg)*));
-    }}
+impl AArch64ReturnValue {
+    const INVALID: *const u8 = usize::MAX as *const _;
 }
 
 /// AArch64 loader page tables have two variations:
@@ -651,8 +586,8 @@ macro_rules! println {
 pub extern "C" fn aarch64_setup_pagetables(
     kernel_first_vaddr: u64,
     kernel_first_paddr: u64,
-    page_tables_paddr_start: u64,
-) -> (u64, u64, u64) {
+    page_table_bytes: &mut [[MaybeUninit<u8>; PAGE_TABLE_SIZE]; 100],
+) -> AArch64ReturnValue {
     use aarch64::{
         block_descriptor, lvl0_index, lvl1_index, lvl2_index, lvl3_index, page_descriptor,
         s1_mair_attr_index::{MT_DEVICE_nGnRnE, MT_NORMAL},
@@ -665,31 +600,28 @@ pub extern "C" fn aarch64_setup_pagetables(
     const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
 
     let mut serialise_page_table_to_paddr = {
-        #[repr(align(4096))]
-        struct PtBytes([[u8; 4096]; 100]);
-        static mut PAGE_TABLE_BYTES: PtBytes = PtBytes([[0; _]; _]);
-        // SAFETY: Trust me (lol)
-        #[allow(static_mut_refs)]
-        let mut page_table_bytes = unsafe { &mut PAGE_TABLE_BYTES.0 };
-
-        let page_tables_paddr_start = &raw mut PAGE_TABLE_BYTES as u64;
+        let page_tables_paddr_start: *const u8 = page_table_bytes.as_ptr().cast();
 
         assert!(
-            page_tables_paddr_start
-                == page_tables_paddr_start.next_multiple_of(PAGE_TABLE_SIZE as u64)
+            (page_tables_paddr_start as usize)
+                == (page_tables_paddr_start as usize).next_multiple_of(PAGE_TABLE_SIZE)
         );
 
         // This maintains the current end of the PT array.
         let mut next_pt_paddr = page_tables_paddr_start;
         let mut i = 0;
 
-        move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> u64 {
+        move |page_table: &mut [u64; PAGE_TABLE_ENTRIES]| -> *const _ {
             let pt_paddr = next_pt_paddr;
-            for (j, byte) in page_table.iter().flat_map(|pte| pte.to_le_bytes()).enumerate() {
-                page_table_bytes[i][j] = byte;
+            for (j, byte) in page_table
+                .iter()
+                .flat_map(|pte| pte.to_le_bytes())
+                .enumerate()
+            {
+                page_table_bytes[i][j].write(byte);
             }
 
-            next_pt_paddr += PAGE_TABLE_SIZE as u64;
+            next_pt_paddr = next_pt_paddr.wrapping_add(PAGE_TABLE_SIZE);
             i += 1;
             page_table.fill(0);
             pt_paddr
@@ -700,13 +632,14 @@ pub extern "C" fn aarch64_setup_pagetables(
         start: u64,
         end: u64,
     }
-    let ram_regions = [
-        Region { start: 0x60000000, end: 0xc0000000 },
-    ];
+    let ram_regions = [Region {
+        start: 0x60000000,
+        end: 0xc0000000,
+    }];
 
     const MAX_NUM_REGIONS: usize = 16;
 
-    let mut regions = [const { core::mem::MaybeUninit::uninit() }; MAX_NUM_REGIONS];
+    let mut regions = [const { MaybeUninit::uninit() }; MAX_NUM_REGIONS];
     let identity_mapped_regions: &mut [(Region, _)] = {
         // Conceptually want we want is an 'arrayvec', but to not pull in more
         // code we implement this less-efficiently MaybeUninit.
@@ -719,7 +652,13 @@ pub extern "C" fn aarch64_setup_pagetables(
 
         let ram_regions_it = ram_regions.into_iter().map(|r| (r, MT_DEVICE_nGnRnE));
 
-        let all_regions_it = ram_regions_it.chain([(Region { start: 0x9000000, end: 0x9001000 }, MT_DEVICE_nGnRnE)]);
+        let all_regions_it = ram_regions_it.chain([(
+            Region {
+                start: 0x9000000,
+                end: 0x9001000,
+            },
+            MT_DEVICE_nGnRnE,
+        )]);
 
         //     // FIXME: Derive from the kernel build system.
         //     if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
@@ -860,7 +799,11 @@ pub extern "C" fn aarch64_setup_pagetables(
                 if region.start >= lvl3_vaddr_top {
                     if lvl3_pt != [0; _] {
                         let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
-                        println!("[iter] Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
+                        println!(
+                            "[iter] Serialise lvl3 table: {:#x} for to {:#x}..{lvl3_vaddr_top:#x}",
+                            lvl3_pt_paddr as usize,
+                            (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB))
+                        );
                         assert!(lvl2_pt[lvl2_index(base)] == 0);
                         lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
                     }
@@ -874,7 +817,7 @@ pub extern "C" fn aarch64_setup_pagetables(
                 if region.start >= lvl2_vaddr_top {
                     if lvl2_pt != [0; _] {
                         let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
-                        println!("[iter] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+                        println!("[iter] Serialise lvl2 table: {:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", lvl2_pt_paddr as usize, (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
                         assert!(lvl1_pt[lvl1_index(base)] == 0);
                         lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
                     }
@@ -930,7 +873,10 @@ pub extern "C" fn aarch64_setup_pagetables(
                 let pt_region_size = 1u64 << bits;
                 let top = base + pt_region_size;
 
-                println!("- Aligned PT region: {:#x}..{:#x} (size_bits: {}, align_bits: {}, bits: {})", base, top, size_bits, align_bits, bits);
+                println!(
+                    "- Aligned PT region: {:#x}..{:#x} (size_bits: {}, align_bits: {}, bits: {})",
+                    base, top, size_bits, align_bits, bits
+                );
                 println!(
                     "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
                     (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
@@ -1023,7 +969,11 @@ pub extern "C" fn aarch64_setup_pagetables(
                             // As we're the top of the range, we can serialise the table.
 
                             let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
-                            println!("Serialise lvl3 table: {lvl3_pt_paddr:#x} for to {:#x}..{lvl3_vaddr_top:#x}", (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB)));
+                            println!(
+                                "Serialise lvl3 table: {:#x} for to {:#x}..{lvl3_vaddr_top:#x}",
+                                lvl3_pt_paddr as usize,
+                                (lvl3_vaddr_top - (1 << BLOCK_BITS_2MB))
+                            );
                             lvl3_vaddr_top += 1 << BLOCK_BITS_2MB;
 
                             assert!(lvl2_pt[lvl2_index(base)] == 0);
@@ -1031,7 +981,11 @@ pub extern "C" fn aarch64_setup_pagetables(
 
                             if top == lvl2_vaddr_top {
                                 let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
-                                println!("Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)));
+                                println!(
+                                    "Serialise lvl2 table: {:#x} for to {:#x}..{lvl2_vaddr_top:#x}",
+                                    lvl2_pt_paddr as usize,
+                                    (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB))
+                                );
                                 lvl2_vaddr_top += 1 << BLOCK_BITS_1GB;
 
                                 assert!(lvl1_pt[lvl1_index(base)] == 0);
@@ -1059,14 +1013,14 @@ pub extern "C" fn aarch64_setup_pagetables(
 
         if lvl3_pt != [0; _] {
             let lvl3_pt_paddr = serialise_page_table_to_paddr(&mut lvl3_pt);
-            println!("[end] Serialise lvl3 table: {lvl3_pt_paddr:#x}");
+            println!("[end] Serialise lvl3 table: {:#x}", lvl3_pt_paddr as usize);
             assert!(lvl2_pt[lvl2_index(base)] == 0);
             lvl2_pt[lvl2_index(base)] = table_descriptor(lvl3_pt_paddr);
         }
 
         if lvl2_pt != [0; _] {
             let lvl2_pt_paddr = serialise_page_table_to_paddr(&mut lvl2_pt);
-            println!("[end] Serialise lvl2 table: {lvl2_pt_paddr:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
+            println!("[end] Serialise lvl2 table: {:#x} for to {:#x}..{lvl2_vaddr_top:#x}, base: {:#x} lvl1_index(base): {:#x}", lvl2_pt_paddr as usize, (lvl2_vaddr_top - (1 << BLOCK_BITS_1GB)), base, lvl1_index(base));
             assert!(lvl1_pt[lvl1_index(base)] == 0);
             lvl1_pt[lvl1_index(base)] = table_descriptor(lvl2_pt_paddr);
         }
@@ -1099,7 +1053,11 @@ pub extern "C" fn aarch64_setup_pagetables(
 
         let ttbr0_el2 = serialise_page_table_to_paddr(&mut ttbr0_el2_pt);
 
-        (ttbr0_el2, u64::MAX, u64::MAX)
+        AArch64ReturnValue {
+            ttbr0_el2,
+            ttbr0_el1: AArch64ReturnValue::INVALID,
+            ttbr1_el1: AArch64ReturnValue::INVALID,
+        }
     } else {
         let mut ttbr0_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
         let mut ttbr1_el1_pt = [0u64; PAGE_TABLE_ENTRIES];
@@ -1112,6 +1070,36 @@ pub extern "C" fn aarch64_setup_pagetables(
         let ttbr0_el1 = serialise_page_table_to_paddr(&mut ttbr0_el1_pt);
         let ttbr1_el1 = serialise_page_table_to_paddr(&mut ttbr1_el1_pt);
 
-        (u64::MAX, ttbr0_el1, ttbr1_el1)
+        AArch64ReturnValue {
+            ttbr0_el2: AArch64ReturnValue::INVALID,
+            ttbr0_el1,
+            ttbr1_el1,
+        }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn it_works() {
+        assert_eq!(2 + 2, 4);
+    }
+
+    #[test]
+    fn aaaaaaaaaaaaaaaaaaaaaa() {
+        #[repr(align(4096))]
+        struct PtBytes([[MaybeUninit<u8>; 4096]; 100]);
+
+        let mut page_table_bytes = PtBytes([[MaybeUninit::uninit(); _]; _]);
+        let pt_bases = aarch64_setup_pagetables(0, 0, &mut page_table_bytes.0);
+        panic!("{pt_bases:#x?}");
+    }
+
+    // #[test]
+    // fn bbbbbbbbbbbbbbbbbbbbbbb() {
+    //     let d = riscv64_setup_pagetables(0, 0, 0);
+    //     // panic!("{a:#x} {b:#x} {c:#x}");
+    // }
+}

From 62651ed443fe099a993776a3b7d19c8673c38ce9 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Tue, 18 Aug 2026 12:53:17 +1000
Subject: [PATCH 12/16] work again for qemu

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/aarch64/mmu.c  |  56 ++++++++++-----
 loader/src/page_tables.rs | 143 +++++++++++++++++++++-----------------
 2 files changed, 118 insertions(+), 81 deletions(-)

diff --git a/loader/src/aarch64/mmu.c b/loader/src/aarch64/mmu.c
index ad511615b..4d2d34c20 100644
--- a/loader/src/aarch64/mmu.c
+++ b/loader/src/aarch64/mmu.c
@@ -12,28 +12,46 @@
 #include "../cutil.h"
 #include "../uart.h"
 
-void el1_mmu_enable(uint64_t aarch64_pt_ttbr0_el1, uint64_t aarch64_pt_ttbr1_el1);
-void el2_mmu_enable(uint64_t aarch64_pt_ttbr0_el2);
-
-/* Pointers to the top-level paging structures */
-uint64_t aarch64_pt_ttbr0_el1;
-uint64_t aarch64_pt_ttbr1_el1;
-uint64_t aarch64_pt_ttbr0_el2;
-
-struct ret {
-    uint64_t a;
-    uint64_t b;
-    uint64_t c;
+void el1_mmu_enable(uint64_t ttbr0_el1, uint64_t ttbr1_el1);
+void el2_mmu_enable(uint64_t ttbr0_el2);
+
+struct AArch64ReturnValue {
+    uintptr_t ttbr0_el2;
+    uintptr_t ttbr0_el1;
+    uintptr_t ttbr1_el1;
+};
+
+struct Region {
+    uint64_t start;
+    uint64_t end;
+};
+
+const struct Region ram_regions[] = {
+    { .start = 0x60000000, .end = 0xc0000000 },
+};
+
+const struct Region device_regions[] = {
+    { .start = 0x9000000, .end = 0x9000000 + 4096 },
 };
 
-extern struct ret aarch64_setup_pagetables(uint64_t kernel_first_vaddr, uint64_t kernel_first_paddr, uint64_t page_tables_paddr_start);
+uint8_t page_table_bytes[4096][64] ALIGN(4096);
+uint8_t regions[16 * 4] ALIGN(16);
+
+extern struct AArch64ReturnValue aarch64_setup_pagetables(
+    uint64_t kernel_first_vaddr, uint64_t kernel_first_paddr,
+    const void *ram_regions_ptr, uintptr_t ram_regions_len,
+    const void *device_regions_ptr, uintptr_t device_regions_len,
+    uint8_t page_table_bytes[4096][64],
+    uint8_t regions[16 * 4]);
 
 int arch_mmu_enable(int logical_cpu)
 {
-    struct ret x = aarch64_setup_pagetables(0, 0, 0);
-    aarch64_pt_ttbr0_el2 = x.a;
-    aarch64_pt_ttbr0_el1 = x.b;
-    aarch64_pt_ttbr1_el1 = x.c;
+    struct AArch64ReturnValue pt = aarch64_setup_pagetables(
+        0x8060000000, 0x60000000,
+        &ram_regions, ARRAY_SIZE(ram_regions),
+        &device_regions, ARRAY_SIZE(device_regions),
+        page_table_bytes, regions
+    );
 
     int r;
     enum el el;
@@ -45,9 +63,9 @@ int arch_mmu_enable(int logical_cpu)
     LDR_PRINT("INFO", logical_cpu, "enabling MMU\n");
     el = current_el();
     if (el == EL1) {
-        el1_mmu_enable(aarch64_pt_ttbr0_el1, aarch64_pt_ttbr1_el1);
+        el1_mmu_enable(pt.ttbr0_el1, pt.ttbr1_el1);
     } else if (el == EL2) {
-        el2_mmu_enable(aarch64_pt_ttbr0_el2);
+        el2_mmu_enable(pt.ttbr0_el2);
     } else {
         LDR_PRINT("ERROR", logical_cpu, "unknown EL for MMU enable\n");
     }
diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index b98b626d1..e56d8129c 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -11,6 +11,7 @@ mod c_interop;
 use core::cmp::min;
 use core::mem;
 use core::mem::MaybeUninit;
+use core::slice;
 
 use c_interop::println;
 
@@ -512,15 +513,24 @@ pub extern "C" fn riscv64_setup_pagetables(
 #[repr(C)]
 #[derive(Debug)]
 pub struct AArch64ReturnValue {
-    ttbr0_el2: *const u8,
-    ttbr0_el1: *const u8,
-    ttbr1_el1: *const u8,
+    pub ttbr0_el2: *const u8,
+    pub ttbr0_el1: *const u8,
+    pub ttbr1_el1: *const u8,
 }
 
 impl AArch64ReturnValue {
     const INVALID: *const u8 = usize::MAX as *const _;
 }
 
+#[derive(Debug, Copy, Clone)]
+pub struct Region {
+    pub start: u64,
+    pub end: u64,
+}
+
+pub const MAX_NUM_PAGE_TABLES: usize = 64;
+pub const MAX_NUM_REGIONS: usize = 16;
+
 /// AArch64 loader page tables have two variations:
 ///  - Loader in EL2, then Stage 1 translations in use, so we have the
 ///    singular TTBR0_EL2 register containing the Level 0 table;
@@ -586,7 +596,13 @@ impl AArch64ReturnValue {
 pub extern "C" fn aarch64_setup_pagetables(
     kernel_first_vaddr: u64,
     kernel_first_paddr: u64,
-    page_table_bytes: &mut [[MaybeUninit<u8>; PAGE_TABLE_SIZE]; 100],
+    ram_regions_ptr: *const Region,
+    ram_regions_len: usize,
+    device_regions_ptr: *const Region,
+    device_regions_len: usize,
+    // Both of these are out-params / storage used.
+    page_table_bytes: &mut [[MaybeUninit<u8>; PAGE_TABLE_SIZE]; MAX_NUM_PAGE_TABLES],
+    regions: &mut [MaybeUninit<(Region, u64)>; MAX_NUM_REGIONS],
 ) -> AArch64ReturnValue {
     use aarch64::{
         block_descriptor, lvl0_index, lvl1_index, lvl2_index, lvl3_index, page_descriptor,
@@ -594,8 +610,11 @@ pub extern "C" fn aarch64_setup_pagetables(
         table_descriptor, BLOCK_BITS_1GB, BLOCK_BITS_2MB, BLOCK_BITS_512GB, PAGE_BITS_4KB,
     };
 
-    let kernel_first_vaddr = 551366426624;
-    let kernel_first_paddr = 1610612736;
+    let ram_regions = unsafe { slice::from_raw_parts(ram_regions_ptr, ram_regions_len) };
+    let device_regions = unsafe { slice::from_raw_parts(device_regions_ptr, device_regions_len) };
+
+    println!("{:#x?}", ram_regions);
+    println!("{:#x?}", device_regions);
 
     const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
 
@@ -628,18 +647,6 @@ pub extern "C" fn aarch64_setup_pagetables(
         }
     };
 
-    struct Region {
-        start: u64,
-        end: u64,
-    }
-    let ram_regions = [Region {
-        start: 0x60000000,
-        end: 0xc0000000,
-    }];
-
-    const MAX_NUM_REGIONS: usize = 16;
-
-    let mut regions = [const { MaybeUninit::uninit() }; MAX_NUM_REGIONS];
     let identity_mapped_regions: &mut [(Region, _)] = {
         // Conceptually want we want is an 'arrayvec', but to not pull in more
         // code we implement this less-efficiently MaybeUninit.
@@ -651,42 +658,12 @@ pub extern "C" fn aarch64_setup_pagetables(
         assert!(ram_regions.len() <= regions.len());
 
         let ram_regions_it = ram_regions.into_iter().map(|r| (r, MT_DEVICE_nGnRnE));
+        let device_regions_it = device_regions.into_iter().map(|r| (r, MT_DEVICE_nGnRnE));
 
-        let all_regions_it = ram_regions_it.chain([(
-            Region {
-                start: 0x9000000,
-                end: 0x9001000,
-            },
-            MT_DEVICE_nGnRnE,
-        )]);
-
-        //     // FIXME: Derive from the kernel build system.
-        //     if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
-        //         let uart_base = align_down(uart_base, PAGE_BITS_4KB);
-        //         regions.push((
-        //             PlatformConfigRegion {
-        //                 start: uart_base,
-        //                 end: uart_base + (1 << PAGE_BITS_4KB),
-        //             },
-        //             MT_DEVICE_nGnRnE,
-        //         ));
-        //     }
-        //     // FIXME: This is currently assuming implementation details of the BCM2711/
-        //     //        Raspberry Pi 4B spin table implementation, as it is the only
-        //     //        platform we have that uses spin tables. Specifically, that
-        //     //        it is always located at the 0 page.
-        //     if elf.find_symbol("cpus_release_addr").is_ok() {
-        //         regions.push((
-        //             PlatformConfigRegion {
-        //                 start: 0x0,
-        //                 end: 1 << PAGE_BITS_4KB,
-        //             },
-        //             MT_DEVICE_nGnRnE,
-        //         ));
-        //     }
+        let all_regions_it = ram_regions_it.chain(device_regions_it);
 
         for (entry, region) in regions.iter_mut().zip(all_regions_it) {
-            entry.write(region);
+            entry.write((*region.0, region.1));
             regions_len += 1;
         }
 
@@ -772,7 +749,7 @@ pub extern "C" fn aarch64_setup_pagetables(
         // Allowed externally for the final iteration
         let mut base = 0u64;
         for &(ref region, attr_index) in identity_mapped_regions.iter() {
-            println!("RAM Region: {:#x}..{:#x}", base, region.end);
+            println!("Identity-Mapped Region: {:#x}..{:#x}", region.start, region.end);
             println!(
                 "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
                 (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
@@ -1088,18 +1065,60 @@ mod tests {
     }
 
     #[test]
-    fn aaaaaaaaaaaaaaaaaaaaaa() {
+    fn qemu_aarch64() {
         #[repr(align(4096))]
-        struct PtBytes([[MaybeUninit<u8>; 4096]; 100]);
+        struct PtBytes([[MaybeUninit<u8>; 4096]; MAX_NUM_PAGE_TABLES]);
+
+        let ram_regions = [Region {
+            start: 0x60000000,
+            end: 0xc0000000,
+        }];
+
+        let device_regions = [
+            // UART
+            Region {
+                start: 0x9000000,
+                end: 0x9001000,
+            },
+        ];
+
+        //     // FIXME: Derive from the kernel build system.
+        //     if let Some(uart_base) = read_symbol_maybe(elf, "uart_addr") {
+        //         let uart_base = align_down(uart_base, PAGE_BITS_4KB);
+        //         regions.push((
+        //             PlatformConfigRegion {
+        //                 start: uart_base,
+        //                 end: uart_base + (1 << PAGE_BITS_4KB),
+        //             },
+        //             MT_DEVICE_nGnRnE,
+        //         ));
+        //     }
+        //     // FIXME: This is currently assuming implementation details of the BCM2711/
+        //     //        Raspberry Pi 4B spin table implementation, as it is the only
+        //     //        platform we have that uses spin tables. Specifically, that
+        //     //        it is always located at the 0 page.
+        //     if elf.find_symbol("cpus_release_addr").is_ok() {
+        //         regions.push((
+        //             PlatformConfigRegion {
+        //                 start: 0x0,
+        //                 end: 1 << PAGE_BITS_4KB,
+        //             },
+        //             MT_DEVICE_nGnRnE,
+        //         ));
+        //     }
 
         let mut page_table_bytes = PtBytes([[MaybeUninit::uninit(); _]; _]);
-        let pt_bases = aarch64_setup_pagetables(0, 0, &mut page_table_bytes.0);
-        panic!("{pt_bases:#x?}");
+        let mut regions_storage = [MaybeUninit::uninit(); MAX_NUM_REGIONS];
+
+        let pt_bases = aarch64_setup_pagetables(
+            /* kernel_first_vaddr */ 0x8060000000,
+            /* kernel_first_paddr */ 0x60000000,
+            ram_regions.as_ptr(),
+            ram_regions.len(),
+            device_regions.as_ptr(),
+            device_regions.len(),
+            &mut page_table_bytes.0,
+            &mut regions_storage,
+        );
     }
-
-    // #[test]
-    // fn bbbbbbbbbbbbbbbbbbbbbbb() {
-    //     let d = riscv64_setup_pagetables(0, 0, 0);
-    //     // panic!("{a:#x} {b:#x} {c:#x}");
-    // }
 }

From 2ccf7c21275d14adcb53e077d4d124a82acd7ceb Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Tue, 18 Aug 2026 13:31:13 +1000
Subject: [PATCH 13/16] make it easier

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/src/aarch64/mmu.c  |  31 ++++++------
 loader/src/page_tables.rs | 100 ++++++++++++++++++++------------------
 2 files changed, 70 insertions(+), 61 deletions(-)

diff --git a/loader/src/aarch64/mmu.c b/loader/src/aarch64/mmu.c
index 4d2d34c20..75ceba86b 100644
--- a/loader/src/aarch64/mmu.c
+++ b/loader/src/aarch64/mmu.c
@@ -6,6 +6,7 @@
  */
 
 #include <stdint.h>
+#include <stdbool.h>
 
 #include "el.h"
 #include "../arch.h"
@@ -21,36 +22,38 @@ struct AArch64ReturnValue {
     uintptr_t ttbr1_el1;
 };
 
+union RegionArchAttrs {
+    bool is_ram;
+    uint64_t raw;
+};
+
 struct Region {
     uint64_t start;
     uint64_t end;
+    union RegionArchAttrs arch_attrs;
 };
 
-const struct Region ram_regions[] = {
-    { .start = 0x60000000, .end = 0xc0000000 },
+struct Region regions[] = {
+    { .start = 0x60000000, .end = 0xc0000000, .arch_attrs.is_ram = true },
+    { .start = 0x9000000, .end = 0x9000000 + 4096, .arch_attrs.is_ram = false },
 };
 
-const struct Region device_regions[] = {
-    { .start = 0x9000000, .end = 0x9000000 + 4096 },
-};
+#define PAGE_TABLE_SIZE 4096
+#define MAX_NUM_PAGE_TABLES 64
 
-uint8_t page_table_bytes[4096][64] ALIGN(4096);
-uint8_t regions[16 * 4] ALIGN(16);
+uint8_t page_table_bytes[PAGE_TABLE_SIZE][MAX_NUM_PAGE_TABLES] ALIGN(4096);
 
 extern struct AArch64ReturnValue aarch64_setup_pagetables(
     uint64_t kernel_first_vaddr, uint64_t kernel_first_paddr,
-    const void *ram_regions_ptr, uintptr_t ram_regions_len,
-    const void *device_regions_ptr, uintptr_t device_regions_len,
-    uint8_t page_table_bytes[4096][64],
-    uint8_t regions[16 * 4]);
+    void *regions_ptr, uintptr_t regions_len,
+    uint8_t page_table_bytes[4096][64]);
 
 int arch_mmu_enable(int logical_cpu)
 {
     struct AArch64ReturnValue pt = aarch64_setup_pagetables(
         0x8060000000, 0x60000000,
-        &ram_regions, ARRAY_SIZE(ram_regions),
-        &device_regions, ARRAY_SIZE(device_regions),
-        page_table_bytes, regions
+        &regions, ARRAY_SIZE(regions),
+        page_table_bytes
     );
 
     int r;
diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index e56d8129c..803f40b0c 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -9,6 +9,7 @@
 mod c_interop;
 
 use core::cmp::min;
+use core::fmt;
 use core::mem;
 use core::mem::MaybeUninit;
 use core::slice;
@@ -522,14 +523,31 @@ impl AArch64ReturnValue {
     const INVALID: *const u8 = usize::MAX as *const _;
 }
 
+#[derive(Copy, Clone)]
+#[repr(C)]
+pub union RegionArchAttrs {
+    pub is_ram: bool,
+    pub raw: u64,
+}
+
+impl fmt::Debug for RegionArchAttrs {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
+        f.debug_struct("RegionArchAttrs")
+            // SAFETY: raw contains all valid bitpatterns
+            .field("raw", unsafe { &self.raw })
+            .finish()
+    }
+}
+
 #[derive(Debug, Copy, Clone)]
+#[repr(C)]
 pub struct Region {
     pub start: u64,
     pub end: u64,
+    pub arch_attrs: RegionArchAttrs,
 }
 
 pub const MAX_NUM_PAGE_TABLES: usize = 64;
-pub const MAX_NUM_REGIONS: usize = 16;
 
 /// AArch64 loader page tables have two variations:
 ///  - Loader in EL2, then Stage 1 translations in use, so we have the
@@ -596,13 +614,11 @@ pub const MAX_NUM_REGIONS: usize = 16;
 pub extern "C" fn aarch64_setup_pagetables(
     kernel_first_vaddr: u64,
     kernel_first_paddr: u64,
-    ram_regions_ptr: *const Region,
-    ram_regions_len: usize,
-    device_regions_ptr: *const Region,
-    device_regions_len: usize,
-    // Both of these are out-params / storage used.
+    // In-out param; storage and input
+    regions_ptr: *mut Region,
+    regions_len: usize,
+    // Storage used for page tables
     page_table_bytes: &mut [[MaybeUninit<u8>; PAGE_TABLE_SIZE]; MAX_NUM_PAGE_TABLES],
-    regions: &mut [MaybeUninit<(Region, u64)>; MAX_NUM_REGIONS],
 ) -> AArch64ReturnValue {
     use aarch64::{
         block_descriptor, lvl0_index, lvl1_index, lvl2_index, lvl3_index, page_descriptor,
@@ -610,12 +626,6 @@ pub extern "C" fn aarch64_setup_pagetables(
         table_descriptor, BLOCK_BITS_1GB, BLOCK_BITS_2MB, BLOCK_BITS_512GB, PAGE_BITS_4KB,
     };
 
-    let ram_regions = unsafe { slice::from_raw_parts(ram_regions_ptr, ram_regions_len) };
-    let device_regions = unsafe { slice::from_raw_parts(device_regions_ptr, device_regions_len) };
-
-    println!("{:#x?}", ram_regions);
-    println!("{:#x?}", device_regions);
-
     const PAGE_TABLE_ENTRIES: usize = PAGE_TABLE_SIZE / mem::size_of::<u64>();
 
     let mut serialise_page_table_to_paddr = {
@@ -647,30 +657,23 @@ pub extern "C" fn aarch64_setup_pagetables(
         }
     };
 
-    let identity_mapped_regions: &mut [(Region, _)] = {
-        // Conceptually want we want is an 'arrayvec', but to not pull in more
-        // code we implement this less-efficiently MaybeUninit.
-        // We implement something very similar to the currently-unstable
-        // write_iter implementation:
-        // https://github.com/rust-lang/rust/blob/1.97.1/library/core/src/mem/maybe_uninit.rs#L1384-L1406
-        let mut regions_len = 0;
+    let identity_mapped_regions: &mut [Region] = {
+        let regions = unsafe { slice::from_raw_parts_mut(regions_ptr, regions_len) };
 
-        assert!(ram_regions.len() <= regions.len());
+        println!("{:#x?}", regions);
 
-        let ram_regions_it = ram_regions.into_iter().map(|r| (r, MT_DEVICE_nGnRnE));
-        let device_regions_it = device_regions.into_iter().map(|r| (r, MT_DEVICE_nGnRnE));
-
-        let all_regions_it = ram_regions_it.chain(device_regions_it);
-
-        for (entry, region) in regions.iter_mut().zip(all_regions_it) {
-            entry.write((*region.0, region.1));
-            regions_len += 1;
+        for region in regions.iter_mut() {
+            // SAFETY: We expect users to set is_ram appropriately.
+            region.arch_attrs.raw = if unsafe { region.arch_attrs.is_ram } {
+                // FIXME: For now, RAM is also mapped as DEVICE memory.
+                MT_DEVICE_nGnRnE
+            } else {
+                MT_DEVICE_nGnRnE
+            };
         }
 
-        let regions = unsafe { (&mut regions[0..regions_len]).assume_init_mut() };
-
         // Need to use 'sort_unstable_by_key' as sort_by_key is not in-place.
-        regions.sort_unstable_by_key(|(region, _)| region.start);
+        regions.sort_unstable_by_key(|region| region.start);
 
         regions
     };
@@ -712,7 +715,7 @@ pub extern "C" fn aarch64_setup_pagetables(
     let ram_lvl1_pt_paddr = {
         // Validation of assumptions about the identity mapped regions.
         let mut previous_end = None;
-        for (region, _) in identity_mapped_regions.iter() {
+        for region in identity_mapped_regions.iter() {
             assert!(lvl0_index(region.start) == 0);
             assert!(lvl0_index(region.end - 1) == 0);
             // This is probably an unnecessary assumption.
@@ -748,8 +751,14 @@ pub extern "C" fn aarch64_setup_pagetables(
 
         // Allowed externally for the final iteration
         let mut base = 0u64;
-        for &(ref region, attr_index) in identity_mapped_regions.iter() {
-            println!("Identity-Mapped Region: {:#x}..{:#x}", region.start, region.end);
+        for region in identity_mapped_regions.iter() {
+            // SAFETY: We went through and initialised raw before.
+            let attr_index = unsafe { region.arch_attrs.raw };
+
+            println!(
+                "Identity-Mapped Region: {:#x}..{:#x}",
+                region.start, region.end
+            );
             println!(
                 "  - Current Lvl1: {:#x}..{:#x}, entries: {}",
                 (lvl1_vaddr_top - (1 << BLOCK_BITS_512GB)),
@@ -1069,16 +1078,17 @@ mod tests {
         #[repr(align(4096))]
         struct PtBytes([[MaybeUninit<u8>; 4096]; MAX_NUM_PAGE_TABLES]);
 
-        let ram_regions = [Region {
-            start: 0x60000000,
-            end: 0xc0000000,
-        }];
-
-        let device_regions = [
+        let mut regions = [
+            Region {
+                start: 0x60000000,
+                end: 0xc0000000,
+                arch_attrs: RegionArchAttrs { is_ram: true },
+            },
             // UART
             Region {
                 start: 0x9000000,
                 end: 0x9001000,
+                arch_attrs: RegionArchAttrs { is_ram: false },
             },
         ];
 
@@ -1108,17 +1118,13 @@ mod tests {
         //     }
 
         let mut page_table_bytes = PtBytes([[MaybeUninit::uninit(); _]; _]);
-        let mut regions_storage = [MaybeUninit::uninit(); MAX_NUM_REGIONS];
 
         let pt_bases = aarch64_setup_pagetables(
             /* kernel_first_vaddr */ 0x8060000000,
             /* kernel_first_paddr */ 0x60000000,
-            ram_regions.as_ptr(),
-            ram_regions.len(),
-            device_regions.as_ptr(),
-            device_regions.len(),
+            regions.as_mut_ptr(),
+            regions.len(),
             &mut page_table_bytes.0,
-            &mut regions_storage,
         );
     }
 }

From 5577520f429c3ee384a7d6f6b17c86cced79c16c Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Tue, 18 Aug 2026 14:39:59 +1000
Subject: [PATCH 14/16] tests part of build

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 build_sdk.py    | 15 +++++++++++++++
 loader/Makefile | 13 ++++++++-----
 2 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/build_sdk.py b/build_sdk.py
index 92cc5bfcb..b9adcddda 100644
--- a/build_sdk.py
+++ b/build_sdk.py
@@ -796,6 +796,19 @@ def build_sel4(
             json_dst.chmod(0o744)
 
 
+def test_loader(build_dir: Path) -> None:
+    build_dir = build_dir / "loader"
+    build_dir.mkdir(exist_ok=True, parents=True)
+
+    make_args = f"BUILD_DIR={build_dir.absolute()} ARCH=dummy BOARD=dummy SEL4_SDK=dummy TARGET_TRIPLE=dummy LLVM=False LINK_ADDRESS=0"
+
+    r = system(
+        f"make -C loader tests {make_args}"
+    )
+    if r != 0:
+        raise Exception(f"Tests failed: loader")
+
+
 def build_elf_component(
     component_name: str,
     sdk_dir: Path,
@@ -1094,6 +1107,8 @@ def main() -> None:
 
     if not args.skip_run_time:
         build_dir = Path("build")
+        test_loader(build_dir)
+
         for (board, configs) in build_goals:
             for config in configs:
                 if not args.skip_sel4:
diff --git a/loader/Makefile b/loader/Makefile
index 376e68849..bcd5f7d73 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -102,7 +102,7 @@ $(BUILD_DIR)/lib%.a : src/%.rs
 
 OBJPROG = $(addprefix $(BUILD_DIR)/, $(PROGS))
 
-all: $(OBJPROG) test
+all: $(OBJPROG)
 
 $(LINKSCRIPT): $(LINKSCRIPT_INPUT)
 	$(CPP) -DLINK_ADDRESS=$(LINK_ADDRESS) $< | grep -v "^#" > $@
@@ -112,11 +112,14 @@ LDFLAGS := -T$(LINKSCRIPT) --gc-sections
 $(OBJPROG): $(addprefix $(BUILD_DIR)/, $(OBJECTS)) $(LINKSCRIPT)
 	$(LD) $(LDFLAGS) --start-group $(addprefix $(BUILD_DIR)/, $(OBJECTS)) --end-group -o $@
 
-test:
+rusttest_%: src/%.rs
 	$(RUSTC) $(RUSTFLAGS) \
 		--emit dep-info,metadata,link \
 		--out-dir $(BUILD_DIR) -L dependency=$(BUILD_DIR) \
+		-Awarnings \
 		--test \
-		--crate-name test_page_tables \
-		src/page_tables.rs
-	$(BUILD_DIR)/test_page_tables
+		--crate-name "$@" \
+		$<
+
+tests: rusttest_page_tables
+	$(BUILD_DIR)/rusttest_page_tables

From ac001d0c2df2edf035ab86d6ca1e9763812782f0 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Tue, 18 Aug 2026 15:19:06 +1000
Subject: [PATCH 15/16] clippy

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 loader/Makefile           | 13 ++++++++++++-
 loader/src/c_interop.rs   |  4 +---
 loader/src/page_tables.rs | 29 ++++++++++++++++-------------
 3 files changed, 29 insertions(+), 17 deletions(-)

diff --git a/loader/Makefile b/loader/Makefile
index bcd5f7d73..fb2868cb3 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -36,6 +36,7 @@ else
 endif
 
 RUSTC := rustc
+CLIPPY := clippy-driver
 
 ifeq ($(ARCH),aarch64)
 	CFLAGS_AARCH64 := -mcpu=$(GCC_CPU) -mgeneral-regs-only -mstrict-align -mno-outline-atomics
@@ -121,5 +122,15 @@ rusttest_%: src/%.rs
 		--crate-name "$@" \
 		$<
 
-tests: rusttest_page_tables
+rustclippy_%: src/%.rs
+	$(CLIPPY) $(RUSTFLAGS) \
+		--emit dep-info,metadata,link \
+		--out-dir $(BUILD_DIR) -L dependency=$(BUILD_DIR) \
+		-Dwarnings \
+		-Cpanic=abort \
+		--crate-type staticlib \
+		--crate-name "$@" \
+		$<
+
+tests: rusttest_page_tables rustclippy_page_tables
 	$(BUILD_DIR)/rusttest_page_tables
diff --git a/loader/src/c_interop.rs b/loader/src/c_interop.rs
index 8fd6b7406..98a63662f 100644
--- a/loader/src/c_interop.rs
+++ b/loader/src/c_interop.rs
@@ -19,9 +19,7 @@ mod real_hardware {
     impl fmt::Write for Writer {
         fn write_str(&mut self, s: &str) -> Result<(), fmt::Error> {
             for c in s.bytes() {
-                unsafe {
-                    puts(CStr::from_bytes_with_nul_unchecked(&[c.into(), 0]).as_ptr())
-                };
+                unsafe { puts(CStr::from_bytes_with_nul_unchecked(&[c, 0]).as_ptr()) };
             }
             Ok(())
         }
diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index 803f40b0c..b6e947e44 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -610,8 +610,12 @@ pub const MAX_NUM_PAGE_TABLES: usize = 64;
 ///      u = align_down(uart_base, 1GiB),
 /// ```
 ///
+/// # Safety
+/// - regions_ptr must be valid for as long as this function runs,
+///   and regions_len must repsent its length
+///
 #[unsafe(no_mangle)]
-pub extern "C" fn aarch64_setup_pagetables(
+pub unsafe extern "C" fn aarch64_setup_pagetables(
     kernel_first_vaddr: u64,
     kernel_first_paddr: u64,
     // In-out param; storage and input
@@ -631,10 +635,7 @@ pub extern "C" fn aarch64_setup_pagetables(
     let mut serialise_page_table_to_paddr = {
         let page_tables_paddr_start: *const u8 = page_table_bytes.as_ptr().cast();
 
-        assert!(
-            (page_tables_paddr_start as usize)
-                == (page_tables_paddr_start as usize).next_multiple_of(PAGE_TABLE_SIZE)
-        );
+        assert!((page_tables_paddr_start as usize).is_multiple_of(PAGE_TABLE_SIZE));
 
         // This maintains the current end of the PT array.
         let mut next_pt_paddr = page_tables_paddr_start;
@@ -988,7 +989,7 @@ pub extern "C" fn aarch64_setup_pagetables(
                     _ => unreachable!("level is 1..=3"),
                 }
 
-                base = base + pt_region_size;
+                base += pt_region_size;
             }
         }
 
@@ -1119,12 +1120,14 @@ mod tests {
 
         let mut page_table_bytes = PtBytes([[MaybeUninit::uninit(); _]; _]);
 
-        let pt_bases = aarch64_setup_pagetables(
-            /* kernel_first_vaddr */ 0x8060000000,
-            /* kernel_first_paddr */ 0x60000000,
-            regions.as_mut_ptr(),
-            regions.len(),
-            &mut page_table_bytes.0,
-        );
+        let pt_bases = unsafe {
+            aarch64_setup_pagetables(
+                /* kernel_first_vaddr */ 0x8060000000,
+                /* kernel_first_paddr */ 0x60000000,
+                regions.as_mut_ptr(),
+                regions.len(),
+                &mut page_table_bytes.0,
+            )
+        };
     }
 }

From 61604b1f3340a40cd8f01b7008943301e5c09be7 Mon Sep 17 00:00:00 2001
From: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Date: Tue, 18 Aug 2026 15:30:00 +1000
Subject: [PATCH 16/16] clippy

Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
---
 .github/workflows/pr.yml  |  2 ++
 build_sdk.py              |  7 +++++++
 loader/Makefile           | 11 ++++++++---
 loader/src/c_interop.rs   |  2 +-
 loader/src/page_tables.rs |  3 +++
 5 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml
index 8593a4ef0..63fd4bedc 100644
--- a/.github/workflows/pr.yml
+++ b/.github/workflows/pr.yml
@@ -27,6 +27,8 @@ jobs:
       - name: Run Clippy
         # Make sure CI fails on all warnings, including Clippy lints
         run: nix develop --ignore-environment -c bash -c "cd tool/microkit && cargo-clippy --all-targets --all-features -- -D warnings -Wclippy::get_unwrap"
+      - name: Run Clippy (Loader)
+        run: nix develop --ignore-environment -c bash -c 'make -C loader clippy CLIPPYFLAGS="-D warnings -Wclippy::get_unwrap" BUILD_DIR=$(mktemp -d) ARCH=dummy BOARD=dummy SEL4_SDK=dummy TARGET_TRIPLE=dummy LLVM=False LINK_ADDRESS=0'
 
   rustfmt_check:
     runs-on: [self-hosted, macos, ARM64]
diff --git a/build_sdk.py b/build_sdk.py
index b9adcddda..dd5b4f9cf 100644
--- a/build_sdk.py
+++ b/build_sdk.py
@@ -808,6 +808,13 @@ def test_loader(build_dir: Path) -> None:
     if r != 0:
         raise Exception(f"Tests failed: loader")
 
+    # We don't pass CLIPPYARGS, so this is warning-only
+    r = system(
+        f"make -C loader clippy {make_args}"
+    )
+    if r != 0:
+        raise Exception(f"Clippy failed: loader")
+
 
 def build_elf_component(
     component_name: str,
diff --git a/loader/Makefile b/loader/Makefile
index fb2868cb3..d106e3261 100644
--- a/loader/Makefile
+++ b/loader/Makefile
@@ -122,15 +122,20 @@ rusttest_%: src/%.rs
 		--crate-name "$@" \
 		$<
 
+tests: rusttest_page_tables
+	$(BUILD_DIR)/rusttest_page_tables
+
+
+CLIPPYFLAGS ?=
+
 rustclippy_%: src/%.rs
 	$(CLIPPY) $(RUSTFLAGS) \
 		--emit dep-info,metadata,link \
 		--out-dir $(BUILD_DIR) -L dependency=$(BUILD_DIR) \
-		-Dwarnings \
+		$(CLIPPYFLAGS) \
 		-Cpanic=abort \
 		--crate-type staticlib \
 		--crate-name "$@" \
 		$<
 
-tests: rusttest_page_tables rustclippy_page_tables
-	$(BUILD_DIR)/rusttest_page_tables
+clippy: rustclippy_page_tables
diff --git a/loader/src/c_interop.rs b/loader/src/c_interop.rs
index 98a63662f..526ec80f0 100644
--- a/loader/src/c_interop.rs
+++ b/loader/src/c_interop.rs
@@ -50,7 +50,7 @@ mod real_hardware {
     fn panic(info: &PanicInfo) -> ! {
         println!("panicked");
 
-        if let Err(_) = writeln!(Writer, "{}", info) {
+        if writeln!(Writer, "{}", info).is_err() {
             // If writeln!() fails (which it should never as our fmt::Write) never
             // fails, then just don't print the extra information.
             println!("panicked (information unknown)");
diff --git a/loader/src/page_tables.rs b/loader/src/page_tables.rs
index b6e947e44..6322e8323 100644
--- a/loader/src/page_tables.rs
+++ b/loader/src/page_tables.rs
@@ -6,6 +6,9 @@
 
 #![no_std]
 
+// We prefer indices as it matches the semantics of PT indices
+#![allow(clippy::needless_range_loop)]
+
 mod c_interop;
 
 use core::cmp::min;