diff --git a/cli/lib/isla/allocator.ml b/cli/lib/isla/allocator.ml
index c9f0d986..71e5b507 100644
--- a/cli/lib/isla/allocator.ml
+++ b/cli/lib/isla/allocator.ml
@@ -47,8 +47,6 @@ type t =
     limit : int option
   }
 
-let default_base = 0x1000
-
 let page_size = 0x1000
 
 let big_size = 1 lsl 21
@@ -60,7 +58,7 @@ let align_up addr alignment =
 
 let page_after addr = align_up (addr + 1) page_size
 
-let make ?(base = default_base) ?limit ?(reserved = []) () =
+let make ~base ?limit ?(reserved = []) () =
   let current =
     List.fold_left
       (fun current addr -> max current (page_after addr))
diff --git a/cli/lib/isla/allocator.mli b/cli/lib/isla/allocator.mli
index 819124df..9c0ebd72 100644
--- a/cli/lib/isla/allocator.mli
+++ b/cli/lib/isla/allocator.mli
@@ -50,7 +50,7 @@ val big_size : int
 
 (** Make an allocator, optionally with an exclusive upper limit and reserved
     addresses. Each reserved address blocks the page containing it. *)
-val make : ?base:int -> ?limit:int -> ?reserved:int list -> unit -> t
+val make : base:int -> ?limit:int -> ?reserved:int list -> unit -> t
 
 (** Allocate [size] bytes at an address aligned to [alignment]. *)
 val alloc_aligned : t -> size:int -> alignment:int -> int
diff --git a/cli/lib/isla/converter.ml b/cli/lib/isla/converter.ml
index c050b909..1c7cb2cf 100644
--- a/cli/lib/isla/converter.ml
+++ b/cli/lib/isla/converter.ml
@@ -153,6 +153,11 @@ let checked_virtual_alignment alignment =
       alignment;
   alignment
 
+let checked_mapping_alignment level =
+  try Page_table_desc.level_size level
+  with Invalid_argument _ ->
+    eval_error Page_table_setup "page_table: invalid mapping level: %d" level
+
 let symbolic_va_alignments ir =
   let virtual_names = symbolic_names ir in
   let alignment_requests =
@@ -168,6 +173,8 @@ let symbolic_va_alignments ir =
                )
               names;
             List.map (fun name -> (name, alignment)) names
+        | Page_table_ast.Mapping {va_name; level = Some level; _} ->
+            [(va_name, checked_mapping_alignment level)]
         | _ -> []
         )
       ir.Ir.page_table_setup
@@ -181,15 +188,29 @@ let symbolic_va_alignments ir =
   in
   List.map (fun name -> (name, alignment_for name)) virtual_names
 
+let make_arena ?(reserved = []) base =
+  assert (base land 0x1FFFFF == 0);
+  Allocator.make ~base ~limit:(base + Allocator.big_size) ~reserved ()
+
+(* Layout:
+   - Code: 0-2 MiB
+   - Page tables: 2-4 MiB
+   - Data: >= 4 MiB *)
+let table_base = Allocator.big_size
+
+let data_base = table_base + Allocator.big_size
+
 (* Build assembly input after assigning concrete addresses to every section and
    symbolic location. *)
-let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
+let to_assembly_input ~code_allocator ~symbol_allocator (ir : Ir.t) :
+  Assembler.assembly_input
+  =
   let code_sections =
     List.mapi
       (fun i (thread : Ir.thread) ->
          { Assembler.name = thread_section_name i;
            code = thread.code;
-           addr = Allocator.alloc_page allocator
+           addr = Allocator.alloc_page code_allocator
          }
        )
       ir.threads
@@ -200,7 +221,7 @@ let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
          let addr =
            match sec.address with
            | Some addr -> addr
-           | None -> Allocator.alloc_page allocator
+           | None -> Allocator.alloc_page code_allocator
          in
          {Assembler.name = sec.sec_name; code = sec.code; addr}
        )
@@ -210,7 +231,7 @@ let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
     List.map
       (fun (name, alignment) ->
          let addr =
-           Allocator.alloc_aligned allocator ~size:Allocator.page_size ~alignment
+           Allocator.alloc_aligned symbol_allocator ~size:alignment ~alignment
          in
          {Assembler.name; addr}
        )
@@ -218,6 +239,10 @@ let to_assembly_input allocator (ir : Ir.t) : Assembler.assembly_input =
   in
   {Assembler.sections = code_sections @ named_sections; symbols}
 
+let assemble ~filename ~code_allocator ~symbol_allocator ir =
+  let input = to_assembly_input ~code_allocator ~symbol_allocator ir in
+  (input, Assembler.assemble ~filename input)
+
 (** {2 Thread register construction} *)
 
 let find_section name (asm_result : Assembler.assembly_result) =
@@ -292,34 +317,24 @@ let build_threads
 
 (** {2 Page table setup construction} *)
 
-(* Build the page-table layout from concrete section/symbol VAs.
-   Thread code pages are included so the DSL can request code mappings. *)
-let build_page_table_setup ir allocator asm_result =
-  match ir.Ir.page_table_setup with
-  | [] -> None
-  | page_table_setup -> (
-      if ir.Ir.locations <> [] then
-        eval_error Page_table_setup
-          "page_table: [locations] is not supported with page_table_setup";
-      let symbolic_vas = asm_result.Assembler.symbols in
-      let code_pages =
-        List.map
-          (fun (thread : Ir.thread) ->
-             let sec = find_section (thread_section_name thread.tid) asm_result in
-             sec.addr
-           )
-          ir.Ir.threads
-      in
-      try
-        Some
-          (Page_table_builder.build ~arch:ir.arch ~allocator ~symbolic_vas
-             ~code_pages page_table_setup
-          )
-      with Page_table_builder.Error msg -> eval_error Page_table_setup "%s" msg
-    )
-
-(* Terms may refer to VA-side assembly symbols and PA-side symbols created by
-   page_table_setup. *)
+(* Build the page-table layout from concrete section/symbol VAs. *)
+let build_page_table_setup
+      ir
+      ~symbol_allocator
+      ~table_allocator
+      ~table_block
+      asm_result
+  =
+  if ir.Ir.locations <> [] then
+    eval_error Page_table_setup
+      "page_table: [locations] is not supported with page_table_setup";
+  try
+    Page_table_builder.build ~arch:ir.arch ~symbol_allocator ~table_allocator
+      ~table_block ~symbolic_vas:asm_result.Assembler.symbols ir.page_table_setup
+  with Page_table_builder.Error msg -> eval_error Page_table_setup "%s" msg
+
+(* Terms may refer to assembly symbols denoting virtual addresses and to symbols
+   whose physical addresses are assigned by page_table_setup. *)
 let build_lookup_addr asm_result page_table =
   let page_table_symbols =
     match page_table with
@@ -444,11 +459,32 @@ let build_memory
 
 let to_testrepr ~filename (ir : Ir.t) : Testrepr.t =
   let default_mem_size = default_memory_size () in
-  let reserved_addrs = reserved_section_addrs ir.sections in
-  let allocator = Allocator.make ~reserved:reserved_addrs () in
-  let asm_input = to_assembly_input allocator ir in
-  let asm_result = Assembler.assemble ~filename asm_input in
-  let page_table = build_page_table_setup ir allocator asm_result in
+  let (asm_input, asm_result, page_table) =
+    if ir.page_table_setup = [] then
+      let allocator =
+        Allocator.make ~base:0
+          ~reserved:(0 :: reserved_section_addrs ir.sections)
+          ()
+      in
+      let (asm_input, asm_result) =
+        assemble ~filename ~code_allocator:allocator ~symbol_allocator:allocator
+          ir
+      in
+      (asm_input, asm_result, None)
+    else
+      let reserved_code_pages = reserved_section_addrs ir.sections in
+      let code_allocator = make_arena ~reserved:(0 :: reserved_code_pages) 0 in
+      let symbol_allocator = Allocator.make ~base:data_base () in
+      let (asm_input, asm_result) =
+        assemble ~filename ~code_allocator ~symbol_allocator ir
+      in
+      let page_table =
+        build_page_table_setup ir ~symbol_allocator
+          ~table_allocator:(make_arena table_base) ~table_block:table_base
+          asm_result
+      in
+      (asm_input, asm_result, Some page_table)
+  in
   let page_table_entries =
     Option.map (fun layout -> layout.Page_table_builder.table_entries) page_table
   in
diff --git a/cli/lib/isla/page_table/page_table_ast.ml b/cli/lib/isla/page_table/page_table_ast.ml
index 210a0ddd..4eb54d4d 100644
--- a/cli/lib/isla/page_table/page_table_ast.ml
+++ b/cli/lib/isla/page_table/page_table_ast.ml
@@ -40,10 +40,10 @@
 
 (** Page-table setup AST.
 
-    VA-side names may be declared with [virtual] or the TOML [symbolic] list.
-    [aligned ... virtual ...] statements constrain those VA-side names. PA-side
-    names may be declared with [physical], or allocated on first use by
-    mapping/data-init statements. *)
+    Virtual-address names may be declared with [virtual] or the TOML [symbolic]
+    list. [aligned ... virtual ...] statements constrain those names. Names for
+    physical addresses may be declared with [physical], or allocated on first
+    use by mapping/data-init statements. *)
 type attr =
   | Code
   | Data
@@ -59,16 +59,16 @@ type mapping_target =
   | Table of Z.t
 
 type stmt =
-  (* [virtual x y;] predeclares VA-side names. *)
+  (* [virtual x y;] predeclares virtual-address names. *)
   | Virtual of string list
-  (* [physical pa_x pa_y;] predeclares PA-side names. *)
+  (* [physical pa_x pa_y;] predeclares physical-address names. *)
   | Physical of string list
-  (* [aligned 2097152 virtual x y;] constrains VA-side names. *)
+  (* [aligned 2097152 virtual x y;] constrains virtual-address names. *)
   | AlignedVirtual of
       { alignment : Z.t;
         names : string list
       }
-  (* [x |-> pa_x;] maps an existing symbolic VA to a PA-side target.
+  (* [x |-> pa_x;] maps a symbolic virtual address to a physical-address target.
      Optional [with ... and default] clauses override descriptor fields. *)
   | Mapping of
       { va_name : string;
@@ -83,7 +83,7 @@ type stmt =
         attrs : descriptor_field list;
         level : int option
       }
-  (* [*pa_x = value;] initialises data at a PA-side name. *)
+  (* [*pa_x = value;] initialises data at a named physical address. *)
   | DataInit of
       { pa_name : string;
         value : Z.t
diff --git a/cli/lib/isla/page_table/page_table_builder.ml b/cli/lib/isla/page_table/page_table_builder.ml
index d7ca9d43..5a1e6ac8 100644
--- a/cli/lib/isla/page_table/page_table_builder.ml
+++ b/cli/lib/isla/page_table/page_table_builder.ml
@@ -63,28 +63,29 @@ exception Error of string
 let error fmt = Printf.ksprintf (fun msg -> raise (Error msg)) fmt
 
 type t =
-  { allocator : Allocator.t;
+  { (* Allocates physical addresses for data symbols. *)
+    symbol_allocator : Allocator.t;
+    (* Allocates root and child translation-table pages. *)
+    table_allocator : Allocator.t;
     (* Root translation-table address. *)
     root : pa;
-    (* Next free page in the translation-table pool. *)
-    mutable next_table_pa : pa;
     (* Page-table descriptors, keyed by their physical addresses. *)
     entries : (pa, descriptor) Hashtbl.t;
-    (* PA names declared by [physical]. *)
-    mutable declared_pas : string list;
+    (* Required alignment for each physical-address symbol. *)
+    pa_alignments : (string * int) list;
     (* PA names and their allocated physical addresses. *)
     mutable symbols_pa : (string * pa) list;
     (* Initial data values, keyed by their allocated PAs. *)
     mutable data_inits : (pa * data_value) list
   }
 
-let make allocator ~root =
+let make ~symbol_allocator ~table_allocator ~pa_alignments ~root =
   let entries = Hashtbl.create 256 in
-  { allocator;
+  { symbol_allocator;
+    table_allocator;
     entries;
     root;
-    next_table_pa = root + Allocator.page_size;
-    declared_pas = [];
+    pa_alignments;
     symbols_pa = [];
     data_inits = []
   }
@@ -96,8 +97,12 @@ let check_arch = function
         (Litmus.Arch_id.to_string arch)
 
 let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name =
-  if not (List.mem name builder.declared_pas) then
-    error "page_table: undeclared PA: %s" name;
+  let alignment =
+    max alignment
+      (List.assoc_opt name builder.pa_alignments
+      |> Option.value ~default:Allocator.page_size
+      )
+  in
   match List.assoc_opt name builder.symbols_pa with
   | Some addr -> (
       if addr mod alignment = 0 then addr
@@ -114,7 +119,7 @@ let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name =
     )
   | None ->
       let addr =
-        Allocator.alloc_aligned builder.allocator ~size:Allocator.page_size
+        Allocator.alloc_aligned builder.symbol_allocator ~size:alignment
           ~alignment
       in
       builder.symbols_pa <- (name, addr) :: builder.symbols_pa;
@@ -124,10 +129,10 @@ let alloc_pa ?(alignment = Allocator.page_size) ?mapping_level builder name =
 
 (** Allocate a fresh table page. *)
 let create_table_page builder =
-  if builder.next_table_pa >= builder.root + Allocator.big_size then
-    error "page_table: 2MB page-table pool exhausted";
-  let addr = builder.next_table_pa in
-  builder.next_table_pa <- addr + Allocator.page_size;
+  let addr =
+    try Allocator.alloc_page builder.table_allocator
+    with Failure msg -> error "page_table: %s" msg
+  in
   addr
 
 let entry_addr table_addr idx = table_addr + (idx * Desc.entry_size)
@@ -203,11 +208,6 @@ let add_mapping ?(fields = []) ?(level = Desc.last_level) builder ~va ~pa kind =
   in
   write_descriptor ~level builder ~va desc
 
-let add_code_mappings builder code_pages =
-  List.iter
-    (fun addr -> add_mapping builder ~va:addr ~pa:addr Page_table_ast.Code)
-    code_pages
-
 (** {1 Statement evaluation} *)
 
 let check_table_level = function
@@ -226,6 +226,27 @@ let mapping_alignment level =
   try Desc.level_size level
   with Invalid_argument _ -> error "page_table: invalid mapping level: %d" level
 
+let pa_alignment_requests stmts =
+  let requests =
+    List.filter_map
+      (function
+        | Page_table_ast.Mapping
+            {target = Page_table_ast.PaName name; level = Some level; _} ->
+            Some (name, mapping_alignment level)
+        | _ -> None
+        )
+      stmts
+  in
+  List.fold_left
+    (fun alignments (name, alignment) ->
+       let previous =
+         List.assoc_opt name alignments
+         |> Option.value ~default:Allocator.page_size
+       in
+       (name, max previous alignment) :: List.remove_assoc name alignments
+     )
+    [] requests
+
 let eval_mapping_target ?level ?(attrs = []) builder ~va = function
   | Page_table_ast.PaName pa_name ->
       let alignment = Option.map mapping_alignment level in
@@ -248,8 +269,7 @@ let eval_mapping_target ?level ?(attrs = []) builder ~va = function
 
 let eval_stmt builder ~symbolic_vas = function
   | Page_table_ast.Virtual _ -> ()
-  | Page_table_ast.Physical names ->
-      builder.declared_pas <- builder.declared_pas @ names
+  | Page_table_ast.Physical _ -> ()
   | Page_table_ast.AlignedVirtual _ -> ()
   | Page_table_ast.Mapping {va_name; target; attrs; level} ->
       let va =
@@ -262,9 +282,14 @@ let eval_stmt builder ~symbolic_vas = function
   | Page_table_ast.DataInit {pa_name; value} ->
       let pa = alloc_pa builder pa_name in
       builder.data_inits <- (pa, value) :: builder.data_inits
-  | Page_table_ast.IdentityMapping {addr; attr} ->
+  | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Code} ->
+      let addr = addr_of_z "address" addr in
+      if addr < Allocator.page_size || addr >= Allocator.big_size then
+        error "page_table: identity code address 0x%x is outside the code arena"
+          addr
+  | Page_table_ast.IdentityMapping {addr; attr = Page_table_ast.Data} ->
       let addr = addr_of_z "address" addr in
-      add_mapping builder ~va:addr ~pa:addr attr
+      add_mapping builder ~va:addr ~pa:addr Page_table_ast.Data
 
 (** {1 Layout construction} *)
 
@@ -285,18 +310,29 @@ let to_layout builder =
   let data_inits = builder.data_inits in
   {root; table_entries; symbols_pa; phys_symbols_pa; data_inits}
 
-let build ~arch ~allocator ~symbolic_vas ~code_pages stmts =
+let build
+      ~arch
+      ~symbol_allocator
+      ~table_allocator
+      ~table_block
+      ~symbolic_vas
+      stmts
+  =
   check_arch arch;
   if stmts = [] then error "page_table: empty page_table_setup";
-  (* [root] is the TTBR0 value and the base of the 2MB page-table pool. *)
-  let root = Allocator.alloc_big allocator in
-  let builder = make allocator ~root in
-  (* Page tables are identity-mapped so generated PTE VAs can access them. *)
-  add_mapping ~level:2 builder ~va:root ~pa:root Page_table_ast.Data;
+  let root =
+    try Allocator.alloc_page table_allocator
+    with Failure msg -> error "page_table: %s" msg
+  in
+  let builder =
+    make ~symbol_allocator ~table_allocator
+      ~pa_alignments:(pa_alignment_requests stmts)
+      ~root
+  in
+  add_mapping ~level:2 builder ~va:0 ~pa:0 Page_table_ast.Code;
+  add_mapping ~level:2 builder ~va:table_block ~pa:table_block Page_table_ast.Data;
   (* Evaluate each statement, using symbolic VAs to resolve virtual names. *)
   List.iter (eval_stmt builder ~symbolic_vas) stmts;
-  (* Add code identity mappings after explicit page-table statements. *)
-  add_code_mappings builder code_pages;
   (* Put data initializers back in source order. *)
   builder.data_inits <- List.rev builder.data_inits;
   to_layout builder
diff --git a/cli/lib/isla/page_table/page_table_builder.mli b/cli/lib/isla/page_table/page_table_builder.mli
index 55d9a3ac..948e0d36 100644
--- a/cli/lib/isla/page_table/page_table_builder.mli
+++ b/cli/lib/isla/page_table/page_table_builder.mli
@@ -54,9 +54,9 @@ type data_value = Z.t
 type layout =
   { root : pa;
     table_entries : (pa * descriptor) list;
-    (* Mapping from PA-side symbols to concrete PAs: pa_x -> PA. *)
+    (* Symbol names and their concrete physical addresses. *)
     symbols_pa : (string * pa) list;
-    (* PA-side data symbols, excluding generated root aliases. *)
+    (* Data symbols and their allocated physical addresses. *)
     phys_symbols_pa : (string * pa) list;
     (* [*pa = value] initialisers resolved to concrete PAs. *)
     data_inits : (pa * data_value) list
@@ -67,11 +67,14 @@ exception Error of string
 (** Build a concrete page-table layout from parsed setup. *)
 val build :
    arch:Litmus.Arch_id.t ->
-  allocator:Allocator.t ->
-  (* Maps VA-side symbol names to concrete VAs for explicit mappings *)
+  (* Allocate physical addresses for data symbols. *)
+  symbol_allocator:Allocator.t ->
+  (* Allocate root and child translation-table pages. *)
+  table_allocator:Allocator.t ->
+  (* Base address of the 2 MiB translation-table storage region. *)
+  table_block:pa ->
+  (* Maps virtual-address symbol names to concrete addresses. *)
   symbolic_vas:(string * va) list ->
-  (* Lists built-in thread code pages that should get identity mappings *)
-  code_pages:va list ->
   (* Parsed [page_table_setup] statement list *)
   Page_table_ast.stmt list ->
   layout
diff --git a/cli/tests/arm/vm/LDR+size+VM.litmus.toml b/cli/tests/arm/vm/LDR+size+VM.litmus.toml
index 19fdacff..d3bf41f5 100644
--- a/cli/tests/arm/vm/LDR+size+VM.litmus.toml
+++ b/cli/tests/arm/vm/LDR+size+VM.litmus.toml
@@ -5,8 +5,8 @@ page_table_setup = """
 virtual x y;
 aligned 2097152 virtual x;
 aligned 65536 virtual y;
-physical pa_pad pa_x;
 *pa_pad = 0;
+physical pa_x;
 x |-> pa_x at level 2;
 *pa_x = 0x000000010000000100000001;
 """
diff --git a/cli/tests/converter/expect/arm/vm/Alias+VM.litmus.toml b/cli/tests/converter/expect/arm/vm/Alias+VM.litmus.toml
index 6bb37341..c5a44642 100644
--- a/cli/tests/converter/expect/arm/vm/Alias+VM.litmus.toml
+++ b/cli/tests/converter/expect/arm/vm/Alias+VM.litmus.toml
@@ -24,7 +24,7 @@ name = "Alias+VM"
   kind = "pagetable"
   addr = 0x202000
   step = 8
-  data = 0x203003
+  data = 0x4c1
 
 [[memory]]
   kind = "pagetable"
@@ -34,25 +34,25 @@ name = "Alias+VM"
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203008
+  addr = 0x202010
   step = 8
-  data = 0x14c3
+  data = 0x203003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203010
+  addr = 0x203000
   step = 8
-  data = 0x400443
+  data = 0x403443
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203018
+  addr = 0x203008
   step = 8
-  data = 0x400443
+  data = 0x403443
 
 [[memory]]
   sym = "pa_x"
-  addr = 0x400000
+  addr = 0x403000
   step = 8
   data = 0
 
@@ -64,8 +64,8 @@ name = "Alias+VM"
 [thread."0".regs]
   _PC = 0x1000
   "R0" = 1
-  "R1" = 0x2000
-  "R2" = 0x3000
+  "R1" = 0x400000
+  "R2" = 0x401000
   "TTBR0_EL1" = 0x200000
   "SCTLR_EL1" = 1
   CurrentEL = 1
diff --git a/cli/tests/converter/expect/arm/vm/Inval+LDR.litmus.toml b/cli/tests/converter/expect/arm/vm/Inval+LDR.litmus.toml
index f9d16935..6675c651 100644
--- a/cli/tests/converter/expect/arm/vm/Inval+LDR.litmus.toml
+++ b/cli/tests/converter/expect/arm/vm/Inval+LDR.litmus.toml
@@ -24,7 +24,7 @@ name = "Inval+LDR"
   kind = "pagetable"
   addr = 0x202000
   step = 8
-  data = 0x203003
+  data = 0x4c1
 
 [[memory]]
   kind = "pagetable"
@@ -34,19 +34,19 @@ name = "Inval+LDR"
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203008
+  addr = 0x202010
   step = 8
-  data = 0x14c3
+  data = 0x203003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203010
+  addr = 0x203000
   step = 8
-  data = 0x400443
+  data = 0x402443
 
 [[memory]]
   sym = "pa_x"
-  addr = 0x400000
+  addr = 0x402000
   step = 8
   data = 3
 
@@ -58,8 +58,8 @@ name = "Inval+LDR"
 [thread."0".regs]
   _PC = 0x1000
   "R0" = 0
-  "R1" = 0x203010
-  "R2" = 0x2000
+  "R1" = 0x203000
+  "R2" = 0x400000
   "VBAR_EL1" = 0x4242000
   "SCTLR_EL1" = 1
   "ESR_EL1" = 0
@@ -103,4 +103,4 @@ name = "Inval+LDR"
   DAIF = 0
 
 [final]
-  assertion = {or = [{and = [{"0:PC" = 0x100c}, {"0:X3" = 3}]}, {and = [{"0:PC" = 0x4242400}, {"0:ELR_EL1" = 0x1008}, {"0:FAR_EL1" = 0x2000}, {"0:ESR_EL1" = 0x92000007}]}]}
+  assertion = {or = [{and = [{"0:PC" = 0x100c}, {"0:X3" = 3}]}, {and = [{"0:PC" = 0x4242400}, {"0:ELR_EL1" = 0x1008}, {"0:FAR_EL1" = 0x400000}, {"0:ESR_EL1" = 0x92000007}]}]}
diff --git a/cli/tests/converter/expect/arm/vm/LDR+size+VM.litmus.toml b/cli/tests/converter/expect/arm/vm/LDR+size+VM.litmus.toml
index b43e96d3..c6d6b213 100644
--- a/cli/tests/converter/expect/arm/vm/LDR+size+VM.litmus.toml
+++ b/cli/tests/converter/expect/arm/vm/LDR+size+VM.litmus.toml
@@ -10,43 +10,37 @@ name = "LDR+size+VM"
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x400000
+  addr = 0x200000
   step = 8
-  data = 0x401003
+  data = 0x201003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x401000
+  addr = 0x201000
   step = 8
-  data = 0x402003
+  data = 0x202003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x402000
+  addr = 0x202000
   step = 8
-  data = 0x403003
+  data = 0x4c1
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x402008
+  addr = 0x202008
   step = 8
-  data = 0x800441
-
-[[memory]]
-  kind = "pagetable"
-  addr = 0x402010
-  step = 8
-  data = 0x400441
+  data = 0x200441
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x403008
+  addr = 0x202010
   step = 8
-  data = 0x14c3
+  data = 0x800441
 
 [[memory]]
   sym = "pa_pad"
-  addr = 0x600000
+  addr = 0x610000
   step = 8
   data = 0
 
@@ -63,11 +57,11 @@ name = "LDR+size+VM"
 
 [thread."0".regs]
   _PC = 0x1000
-  "R1" = 0x200000
-  "R2" = 0x210000
+  "R1" = 0x400000
+  "R2" = 0x600000
   "SCTLR_EL1" = 1
   CurrentEL = 1
-  "TTBR0_EL1" = 0x400000
+  "TTBR0_EL1" = 0x200000
   "R0" = 0
   "R3" = 0
   "R4" = 0
@@ -104,4 +98,4 @@ name = "LDR+size+VM"
   DAIF = 0
 
 [final]
-  assertion = {and = [{"0:X0" = 1}, {"0:X2" = 0x210000}, {pa_x = 0x10000000100000001}]}
+  assertion = {and = [{"0:X0" = 1}, {"0:X2" = 0x600000}, {pa_x = 0x10000000100000001}]}
diff --git a/cli/tests/converter/expect/arm/vm/MP+VM.litmus.toml b/cli/tests/converter/expect/arm/vm/MP+VM.litmus.toml
index a62d7873..fadafcf6 100644
--- a/cli/tests/converter/expect/arm/vm/MP+VM.litmus.toml
+++ b/cli/tests/converter/expect/arm/vm/MP+VM.litmus.toml
@@ -31,7 +31,7 @@ name = "MP+VM"
   kind = "pagetable"
   addr = 0x202000
   step = 8
-  data = 0x203003
+  data = 0x4c1
 
 [[memory]]
   kind = "pagetable"
@@ -41,37 +41,31 @@ name = "MP+VM"
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203008
-  step = 8
-  data = 0x14c3
-
-[[memory]]
-  kind = "pagetable"
-  addr = 0x203010
+  addr = 0x202010
   step = 8
-  data = 0x24c3
+  data = 0x203003
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203018
+  addr = 0x203000
   step = 8
-  data = 0x400443
+  data = 0x402443
 
 [[memory]]
   kind = "pagetable"
-  addr = 0x203020
+  addr = 0x203008
   step = 8
-  data = 0x401443
+  data = 0x403443
 
 [[memory]]
   sym = "pa_x"
-  addr = 0x400000
+  addr = 0x402000
   step = 8
   data = 0
 
 [[memory]]
   sym = "pa_y"
-  addr = 0x401000
+  addr = 0x403000
   step = 8
   data = 0
 
@@ -83,9 +77,9 @@ name = "MP+VM"
 [thread."0".regs]
   _PC = 0x1000
   "R0" = 1
-  "R1" = 0x3000
+  "R1" = 0x400000
   "R2" = 1
-  "R3" = 0x4000
+  "R3" = 0x401000
   "SCTLR_EL1" = 1
   CurrentEL = 1
   "TTBR0_EL1" = 0x200000
@@ -127,8 +121,8 @@ name = "MP+VM"
 
 [thread."1".regs]
   _PC = 0x2000
-  "R1" = 0x4000
-  "R3" = 0x3000
+  "R1" = 0x401000
+  "R3" = 0x400000
   "SCTLR_EL1" = 1
   CurrentEL = 1
   "TTBR0_EL1" = 0x200000
diff --git a/cli/tests/errors/errors.t b/cli/tests/errors/errors.t
index 0bbf7456..faef01a3 100644
--- a/cli/tests/errors/errors.t
+++ b/cli/tests/errors/errors.t
@@ -189,7 +189,7 @@ Page table DSL rejects duplicate VA mappings
   $ archsem seq conflicting-page-table-mapping.litmus.toml
   archsem: eval error:
   File "conflicting-page-table-mapping.litmus.toml", path "page_table_setup":
-  page_table: conflicting mapping for VA 0x2000: existing descriptor 0x400443, new descriptor 0x401443
+  page_table: conflicting mapping for VA 0x400000: existing descriptor 0x401443, new descriptor 0x402443
   [1]
 
 Page table DSL rejects locations with page tables