diff --git a/inc/hf/addr.h b/inc/hf/addr.h
index b67e1c2..c37601d 100644
--- a/inc/hf/addr.h
+++ b/inc/hf/addr.h
@@ -19,7 +19,7 @@
 #include <stddef.h>
 #include <stdint.h>
 
-#include "hf/arch/addr.h"
+#include "hf/arch/types.h"
 
 /** An opaque type for a physical address. */
 typedef struct {
diff --git a/src/arch/aarch64/inc/hf/arch/barriers.h b/inc/hf/arch/barriers.h
similarity index 61%
copy from src/arch/aarch64/inc/hf/arch/barriers.h
copy to inc/hf/arch/barriers.h
index 7b855a6..a22d1d1 100644
--- a/src/arch/aarch64/inc/hf/arch/barriers.h
+++ b/inc/hf/arch/barriers.h
@@ -16,17 +16,20 @@
 
 #pragma once
 
-static inline void dmb(void)
-{
-	__asm__ volatile("dmb sy");
-}
+/**
+ * Ensures all explicit memory accesses before this point are completed before
+ * any later memory accesses are performed.
+ */
+void dmb(void);
 
-static inline void dsb(void)
-{
-	__asm__ volatile("dsb sy");
-}
+/**
+ * Ensure all explicit memory access and management instructions have completed
+ * before continuing.
+ */
+void dsb(void);
 
-static inline void isb(void)
-{
-	__asm__ volatile("isb");
-}
+/**
+ * Flushes the instruction pipeline so that instructions are fetched from
+ * memory.
+ */
+void isb(void);
diff --git a/inc/hf/arch.h b/inc/hf/arch/console.h
similarity index 92%
rename from inc/hf/arch.h
rename to inc/hf/arch/console.h
index a07b180..94cbaba 100644
--- a/inc/hf/arch.h
+++ b/inc/hf/arch/console.h
@@ -16,6 +16,5 @@
 
 #pragma once
 
-#include "hf/cpu.h"
-
+/** Put a single character on the console. */
 void arch_putchar(char c);
diff --git a/inc/hf/arch/cpu.h b/inc/hf/arch/cpu.h
new file mode 100644
index 0000000..24f00c0
--- /dev/null
+++ b/inc/hf/arch/cpu.h
@@ -0,0 +1,56 @@
+/*
+ * Copyright 2018 Google LLC
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     https://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#pragma once
+
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+
+#include "hf/addr.h"
+
+/**
+ * Disables interrutps.
+ */
+void arch_irq_disable(void);
+
+/**
+ * Enables interrupts.
+ */
+void arch_irq_enable(void);
+
+/**
+ * Initializes the register state for a VM.
+ */
+void arch_regs_init(struct arch_regs *r, bool is_primary, uint64_t vmid,
+		    paddr_t table, uint32_t index);
+
+/**
+ * Updates the given registers so that when a vcpu runs, it starts off at the
+ * given address (pc) with the given argument.
+ *
+ * This function must only be called on an arch_regs that is known not be in use
+ * by any other physical CPU.
+ */
+void arch_regs_set_pc_arg(struct arch_regs *r, ipaddr_t pc, uintreg_t arg);
+
+/**
+ * Updates the register holding the return value of a function.
+ *
+ * This function must only be called on an arch_regs that is known not be in use
+ * by any other physical CPU.
+ */
+void arch_regs_set_retval(struct arch_regs *r, uintreg_t v);
diff --git a/src/arch/aarch64/inc/hf/arch/mm.h b/inc/hf/arch/mm.h
similarity index 67%
rename from src/arch/aarch64/inc/hf/arch/mm.h
rename to inc/hf/arch/mm.h
index 653538e..0939498 100644
--- a/src/arch/aarch64/inc/hf/arch/mm.h
+++ b/inc/hf/arch/mm.h
@@ -21,28 +21,33 @@
 
 #include "hf/addr.h"
 
-/**
- * A page table entry (PTE).
- *
- * It will take one of the following forms:
+/*
+ * A page table entry (PTE) will take one of the following forms:
  *
  *  1. absent        : There is no mapping.
  *  2. invalid block : Represents a block that is not in the address space.
  *  3. valid block   : Represents a block that is in the address space.
  *  4. table         : Represents a reference to a table of PTEs.
  */
-typedef uint64_t pte_t;
 
-#define PAGE_LEVEL_BITS 9
-
-/*
- * TODO: move the arch_mm_* declarations to a shared header. That header can
- * also check that the specific implementation defines everything it needs to
- * too.
+/**
+ * Creates an absent PTE.
  */
 pte_t arch_mm_absent_pte(uint8_t level);
+
+/**
+ * Createa a table PTE.
+ */
 pte_t arch_mm_table_pte(uint8_t level, paddr_t pa);
+
+/**
+ * Creates a block PTE.
+ */
 pte_t arch_mm_block_pte(uint8_t level, paddr_t pa, uint64_t attrs);
+
+/**
+ * Chceks whether a block is allowed at the given level of the page table.
+ */
 bool arch_mm_is_block_allowed(uint8_t level);
 
 /**
@@ -69,16 +74,66 @@
  */
 bool arch_mm_pte_is_table(pte_t pte, uint8_t level);
 
+/**
+ * Clears the bits of an address that are ignored by the page table. In effect,
+ * the address is rounded down to the start of the corresponding PTE range.
+ */
 paddr_t arch_mm_clear_pa(paddr_t pa);
+
+/**
+ * Extracts the start address if the PTE range.
+ */
 paddr_t arch_mm_block_from_pte(pte_t pte, uint8_t level);
+
+/**
+ * Extracts the address of the table referenced by the PTE/.
+ */
 paddr_t arch_mm_table_from_pte(pte_t pte, uint8_t level);
+
+/**
+ * Extracts the atrobutes of the PTE.
+ */
 uint64_t arch_mm_pte_attrs(pte_t pte, uint8_t level);
+
+/**
+ * Merge the attributes of a block into those of its containing table.
+ */
 uint64_t arch_mm_combine_table_entry_attrs(uint64_t table_attrs,
 					   uint64_t block_attrs);
+
+/**
+ * Invalidates hte given range of stage-1 TLB.
+ */
 void arch_mm_invalidate_stage1_range(vaddr_t va_begin, vaddr_t va_end);
+
+/**
+ * Invalidates hte given range of stage-2 TLB.
+ */
 void arch_mm_invalidate_stage2_range(ipaddr_t va_begin, ipaddr_t va_end);
+
+/**
+ * Writes the given range of virtual memory back to the point of unification so
+ * all cores and devices will see the updated values.
+ */
 void arch_mm_write_back_dcache(void *base, size_t size);
+
+/**
+ * Gets teh maximum level allowed in the page table for the given mode.
+ */
 uint8_t arch_mm_max_level(int mode);
+
+/**
+ * Gets the number of concatenated page tables used at the root for the given
+ * mode.
+ */
 uint8_t arch_mm_root_table_count(int mode);
+
+/**
+ * Converts the mode into attributes for a block PTE.
+ */
 uint64_t arch_mm_mode_to_attrs(int mode);
+
+/**
+ * Initialized the arch specific memory management state.
+ */
 bool arch_mm_init(paddr_t table, bool first);
diff --git a/src/arch/aarch64/BUILD.gn b/src/arch/aarch64/BUILD.gn
index e9d2926..0f94b8d 100644
--- a/src/arch/aarch64/BUILD.gn
+++ b/src/arch/aarch64/BUILD.gn
@@ -38,6 +38,8 @@
 # Implementation of the arch interface for aarch64.
 source_set("arch") {
   sources = [
+    "barriers.c",
+    "cpu.c",
     "mm.c",
   ]
 }
@@ -62,5 +64,9 @@
     sources = [
       "pl011.c",
     ]
+
+    deps = [
+      ":arch",
+    ]
   }
 }
diff --git a/src/arch/aarch64/inc/hf/arch/barriers.h b/src/arch/aarch64/barriers.c
similarity index 86%
rename from src/arch/aarch64/inc/hf/arch/barriers.h
rename to src/arch/aarch64/barriers.c
index 7b855a6..14721fb 100644
--- a/src/arch/aarch64/inc/hf/arch/barriers.h
+++ b/src/arch/aarch64/barriers.c
@@ -14,19 +14,17 @@
  * limitations under the License.
  */
 
-#pragma once
-
-static inline void dmb(void)
+void dmb(void)
 {
 	__asm__ volatile("dmb sy");
 }
 
-static inline void dsb(void)
+void dsb(void)
 {
 	__asm__ volatile("dsb sy");
 }
 
-static inline void isb(void)
+void isb(void)
 {
 	__asm__ volatile("isb");
 }
diff --git a/src/arch/aarch64/cpu.c b/src/arch/aarch64/cpu.c
new file mode 100644
index 0000000..49ab032
--- /dev/null
+++ b/src/arch/aarch64/cpu.c
@@ -0,0 +1,83 @@
+/*
+ * Copyright 2018 Google LLC
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     https://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdint.h>
+
+#include "hf/addr.h"
+
+void arch_irq_disable(void)
+{
+	__asm__ volatile("msr DAIFSet, #0xf");
+}
+
+void arch_irq_enable(void)
+{
+	__asm__ volatile("msr DAIFClr, #0xf");
+}
+
+void arch_regs_init(struct arch_regs *r, bool is_primary, uint64_t vmid,
+		    paddr_t table, uint32_t index)
+{
+	uintreg_t hcr;
+	uintreg_t cptr;
+	uintreg_t cnthctl;
+
+	/* TODO: Determine if we need to set TSW. */
+	hcr = (1u << 31) | /* RW bit. */
+	      (1u << 21) | /* TACR, trap access to ACTRL_EL1. */
+	      (1u << 19) | /* TSC, trap SMC instructions. */
+	      (1u << 20) | /* TIDCP, trap impl-defined funct. */
+	      (1u << 2) |  /* PTW, Protected Table Walk. */
+	      (1u << 0);   /* VM: enable stage-2 translation. */
+
+	cptr = 0;
+	cnthctl = 0;
+
+	if (is_primary) {
+		cnthctl |=
+			(1u << 0) | /* EL1PCTEN, don't trap phys cnt access. */
+			(1u << 1);  /* EL1PCEN, don't trap phys timer access. */
+	} else {
+		hcr |= (7u << 3) |  /* AMO, IMO, FMO bits. */
+		       (1u << 9) |  /* FB bit. */
+		       (1u << 10) | /* BSU bits set to inner-sh. */
+		       (3u << 13);  /* TWI, TWE bits. */
+
+		cptr |= (1u << 10); /* TFP, trap fp access. */
+	}
+
+	r->lazy.hcr_el2 = hcr;
+	r->lazy.cptr_el2 = cptr;
+	r->lazy.cnthctl_el2 = cnthctl;
+	r->lazy.vttbr_el2 = pa_addr(table) | (vmid << 48);
+	r->lazy.vmpidr_el2 = index;
+	/* TODO: Use constant here. */
+	r->spsr = 5 |	 /* M bits, set to EL1h. */
+		  (0xf << 6); /* DAIF bits set; disable interrupts. */
+}
+
+void arch_regs_set_pc_arg(struct arch_regs *r, ipaddr_t pc, uintreg_t arg)
+{
+	r->pc = ipa_addr(pc);
+	r->r[0] = arg;
+}
+
+void arch_regs_set_retval(struct arch_regs *r, uintreg_t v)
+{
+	r->r[0] = v;
+}
diff --git a/src/arch/aarch64/inc/hf/arch/addr.h b/src/arch/aarch64/inc/hf/arch/addr.h
deleted file mode 100644
index 61483ed..0000000
--- a/src/arch/aarch64/inc/hf/arch/addr.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * Copyright 2018 Google LLC
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- *     https://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-
-#pragma once
-
-#include <stdint.h>
-
-#define PAGE_BITS 12
-
-/** Integer type large enough to hold a physical address. */
-typedef uintptr_t uintpaddr_t;
-
-/** Integer type large enough to hold a virtual address. */
-typedef uintptr_t uintvaddr_t;
diff --git a/src/arch/aarch64/inc/hf/arch/cpu.h b/src/arch/aarch64/inc/hf/arch/cpu.h
deleted file mode 100644
index 12a7207..0000000
--- a/src/arch/aarch64/inc/hf/arch/cpu.h
+++ /dev/null
@@ -1,139 +0,0 @@
-/*
- * Copyright 2018 Google LLC
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- *     https://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-
-#pragma once
-
-#include <stdbool.h>
-#include <stddef.h>
-#include <stdint.h>
-
-#include "hf/addr.h"
-
-typedef uint64_t uintreg_t;
-
-struct arch_regs {
-	/* General purpose registers. */
-	uintreg_t r[31];
-	uintreg_t pc;
-	uintreg_t spsr;
-
-	/* TODO: We need to save virtual timer state. */
-	struct {
-		uintreg_t vmpidr_el2;
-		uintreg_t csselr_el1;
-		uintreg_t sctlr_el1;
-		uintreg_t actlr_el1;
-		uintreg_t cpacr_el1;
-		uintreg_t ttbr0_el1;
-		uintreg_t ttbr1_el1;
-		uintreg_t tcr_el1;
-		uintreg_t esr_el1;
-		uintreg_t afsr0_el1;
-		uintreg_t afsr1_el1;
-		uintreg_t far_el1;
-		uintreg_t mair_el1;
-		uintreg_t vbar_el1;
-		uintreg_t contextidr_el1;
-		uintreg_t tpidr_el0;
-		uintreg_t tpidrro_el0;
-		uintreg_t tpidr_el1;
-		uintreg_t amair_el1;
-		uintreg_t cntkctl_el1;
-		uintreg_t sp_el0;
-		uintreg_t sp_el1;
-		uintreg_t par_el1;
-		uintreg_t hcr_el2;
-		uintreg_t cptr_el2;
-		uintreg_t cnthctl_el2;
-		uintreg_t vttbr_el2;
-	} lazy;
-};
-
-static inline void arch_irq_disable(void)
-{
-	__asm__ volatile("msr DAIFSet, #0xf");
-}
-
-static inline void arch_irq_enable(void)
-{
-	__asm__ volatile("msr DAIFClr, #0xf");
-}
-
-static inline void arch_regs_init(struct arch_regs *r, bool is_primary,
-				  uint64_t vmid, paddr_t table, uint32_t index)
-{
-	uintreg_t hcr;
-	uintreg_t cptr;
-	uintreg_t cnthctl;
-
-	/* TODO: Determine if we need to set TSW. */
-	hcr = (1u << 31) | /* RW bit. */
-	      (1u << 21) | /* TACR, trap access to ACTRL_EL1. */
-	      (1u << 19) | /* TSC, trap SMC instructions. */
-	      (1u << 20) | /* TIDCP, trap impl-defined funct. */
-	      (1u << 2) |  /* PTW, Protected Table Walk. */
-	      (1u << 0);   /* VM: enable stage-2 translation. */
-
-	cptr = 0;
-	cnthctl = 0;
-
-	if (is_primary) {
-		cnthctl |=
-			(1u << 0) | /* EL1PCTEN, don't trap phys cnt access. */
-			(1u << 1);  /* EL1PCEN, don't trap phys timer access. */
-	} else {
-		hcr |= (7u << 3) |  /* AMO, IMO, FMO bits. */
-		       (1u << 9) |  /* FB bit. */
-		       (1u << 10) | /* BSU bits set to inner-sh. */
-		       (3u << 13);  /* TWI, TWE bits. */
-
-		cptr |= (1u << 10); /* TFP, trap fp access. */
-	}
-
-	r->lazy.hcr_el2 = hcr;
-	r->lazy.cptr_el2 = cptr;
-	r->lazy.cnthctl_el2 = cnthctl;
-	r->lazy.vttbr_el2 = pa_addr(table) | (vmid << 48);
-	r->lazy.vmpidr_el2 = index;
-	/* TODO: Use constant here. */
-	r->spsr = 5 |	 /* M bits, set to EL1h. */
-		  (0xf << 6); /* DAIF bits set; disable interrupts. */
-}
-
-/**
- * Updates the given registers so that when a vcpu runs, it starts off at the
- * given address (pc) with the given argument.
- *
- * This function must only be called on an arch_regs that is known not be in use
- * by any other physical CPU.
- */
-static inline void arch_regs_set_pc_arg(struct arch_regs *r, ipaddr_t pc,
-					uintreg_t arg)
-{
-	r->pc = ipa_addr(pc);
-	r->r[0] = arg;
-}
-
-/**
- * Updates the register holding the return value of a function.
- *
- * This function must only be called on an arch_regs that is known not be in use
- * by any other physical CPU.
- */
-static inline void arch_regs_set_retval(struct arch_regs *r, uintreg_t v)
-{
-	r->r[0] = v;
-}
diff --git a/src/arch/aarch64/inc/hf/arch/types.h b/src/arch/aarch64/inc/hf/arch/types.h
new file mode 100644
index 0000000..e028adc
--- /dev/null
+++ b/src/arch/aarch64/inc/hf/arch/types.h
@@ -0,0 +1,73 @@
+/*
+ * Copyright 2018 Google LLC
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     https://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#pragma once
+
+#include <stdint.h>
+
+#define PAGE_BITS 12
+#define PAGE_LEVEL_BITS 9
+
+/** The type of a page table entry (PTE). */
+typedef uint64_t pte_t;
+
+/** Integer type large enough to hold a physical address. */
+typedef uintptr_t uintpaddr_t;
+
+/** Integer type large enough to hold a virtual address. */
+typedef uintptr_t uintvaddr_t;
+
+/** The integer large corresponding to the native register size. */
+typedef uint64_t uintreg_t;
+
+/** Type to represent the register state of a VM.  */
+struct arch_regs {
+	/* General purpose registers. */
+	uintreg_t r[31];
+	uintreg_t pc;
+	uintreg_t spsr;
+
+	/* TODO: We need to save virtual timer state. */
+	struct {
+		uintreg_t vmpidr_el2;
+		uintreg_t csselr_el1;
+		uintreg_t sctlr_el1;
+		uintreg_t actlr_el1;
+		uintreg_t cpacr_el1;
+		uintreg_t ttbr0_el1;
+		uintreg_t ttbr1_el1;
+		uintreg_t tcr_el1;
+		uintreg_t esr_el1;
+		uintreg_t afsr0_el1;
+		uintreg_t afsr1_el1;
+		uintreg_t far_el1;
+		uintreg_t mair_el1;
+		uintreg_t vbar_el1;
+		uintreg_t contextidr_el1;
+		uintreg_t tpidr_el0;
+		uintreg_t tpidrro_el0;
+		uintreg_t tpidr_el1;
+		uintreg_t amair_el1;
+		uintreg_t cntkctl_el1;
+		uintreg_t sp_el0;
+		uintreg_t sp_el1;
+		uintreg_t par_el1;
+		uintreg_t hcr_el2;
+		uintreg_t cptr_el2;
+		uintreg_t cnthctl_el2;
+		uintreg_t vttbr_el2;
+	} lazy;
+};
diff --git a/src/arch/aarch64/msr.h b/src/arch/aarch64/msr.h
index fbc7188..2eeda06 100644
--- a/src/arch/aarch64/msr.h
+++ b/src/arch/aarch64/msr.h
@@ -18,7 +18,7 @@
 
 #include <stddef.h>
 
-#include "inc/hf/arch/cpu.h"
+#include <hf/arch/cpu.h>
 
 #define read_msr(name)                                          \
 	__extension__({                                         \
diff --git a/src/arch/fake/BUILD.gn b/src/arch/fake/BUILD.gn
index 59a02e4..cc0a0ad 100644
--- a/src/arch/fake/BUILD.gn
+++ b/src/arch/fake/BUILD.gn
@@ -14,6 +14,7 @@
 
 source_set("fake") {
   sources = [
+    "cpu.c",
     "mm.c",
   ]
 }
diff --git a/src/arch/fake/cpu.c b/src/arch/fake/cpu.c
new file mode 100644
index 0000000..afd9cd5
--- /dev/null
+++ b/src/arch/fake/cpu.c
@@ -0,0 +1,48 @@
+/*
+ * Copyright 2018 Google LLC
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     https://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+#include <hf/arch/cpu.h>
+
+void arch_irq_disable(void)
+{
+	/* TODO */
+}
+
+void arch_irq_enable(void)
+{
+	/* TODO */
+}
+
+void arch_regs_init(struct arch_regs *r, bool is_primary, uint64_t vmid,
+		    paddr_t table, uint32_t index)
+{
+	/* TODO */
+	(void)is_primary;
+	(void)vmid;
+	(void)table;
+	r->vcpu_index = index;
+}
+
+void arch_regs_set_pc_arg(struct arch_regs *r, ipaddr_t pc, uintreg_t arg)
+{
+	(void)pc;
+	r->r[0] = arg;
+}
+
+void arch_regs_set_retval(struct arch_regs *r, uintreg_t v)
+{
+	r->r[0] = v;
+}
diff --git a/src/arch/fake/inc/hf/arch/cpu.h b/src/arch/fake/inc/hf/arch/cpu.h
deleted file mode 100644
index 291a005..0000000
--- a/src/arch/fake/inc/hf/arch/cpu.h
+++ /dev/null
@@ -1,62 +0,0 @@
-/*
- * Copyright 2018 Google LLC
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- *     https://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-
-#pragma once
-
-#include <stdbool.h>
-#include <stdint.h>
-
-#include "hf/addr.h"
-
-typedef uint64_t uintreg_t;
-
-struct arch_regs {
-	uintreg_t r[5];
-	uintreg_t vcpu_index;
-	bool virtual_interrupt;
-};
-
-static inline void arch_irq_disable(void)
-{
-	/* TODO */
-}
-
-static inline void arch_irq_enable(void)
-{
-	/* TODO */
-}
-
-static inline void arch_regs_init(struct arch_regs *r, bool is_primary,
-				  uint64_t vmid, paddr_t table, uint64_t index)
-{
-	/* TODO */
-	(void)is_primary;
-	(void)vmid;
-	(void)table;
-	r->vcpu_index = index;
-}
-
-static inline void arch_regs_set_pc_arg(struct arch_regs *r, ipaddr_t pc,
-					uintreg_t arg)
-{
-	(void)pc;
-	r->r[0] = arg;
-}
-
-static inline void arch_regs_set_retval(struct arch_regs *r, uintreg_t v)
-{
-	r->r[0] = v;
-}
diff --git a/src/arch/fake/inc/hf/arch/mm.h b/src/arch/fake/inc/hf/arch/mm.h
deleted file mode 100644
index 13064b5..0000000
--- a/src/arch/fake/inc/hf/arch/mm.h
+++ /dev/null
@@ -1,52 +0,0 @@
-/*
- * Copyright 2018 Google LLC
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- *     https://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-
-#pragma once
-
-#include <stdbool.h>
-
-#include "hf/addr.h"
-
-/** A page table entry. */
-typedef uint64_t pte_t;
-
-#define PAGE_LEVEL_BITS 9
-
-/*
- * TODO: move the arch_mm_* declarations to a shared header. That header can
- * also check that the specific implementation defines everything it needs to
- * too.
- */
-pte_t arch_mm_absent_pte(uint8_t level);
-pte_t arch_mm_table_pte(uint8_t level, paddr_t pa);
-pte_t arch_mm_block_pte(uint8_t level, paddr_t pa, uint64_t attrs);
-bool arch_mm_is_block_allowed(uint8_t level);
-bool arch_mm_pte_is_present(pte_t pte, uint8_t level);
-bool arch_mm_pte_is_valid(pte_t pte, uint8_t level);
-bool arch_mm_pte_is_table(pte_t pte, uint8_t level);
-bool arch_mm_pte_is_block(pte_t pte, uint8_t level);
-paddr_t arch_mm_clear_pa(paddr_t pa);
-paddr_t arch_mm_block_from_pte(pte_t pte, uint8_t level);
-paddr_t arch_mm_table_from_pte(pte_t pte, uint8_t level);
-uint64_t arch_mm_pte_attrs(pte_t pte, uint8_t level);
-uint64_t arch_mm_combine_table_entry_attrs(uint64_t table_attrs,
-					   uint64_t block_attrs);
-void arch_mm_invalidate_stage1_range(vaddr_t va_begin, vaddr_t va_end);
-void arch_mm_invalidate_stage2_range(ipaddr_t va_begin, ipaddr_t va_end);
-uint8_t arch_mm_max_level(int mode);
-uint8_t arch_mm_root_table_count(int mode);
-uint64_t arch_mm_mode_to_attrs(int mode);
-bool arch_mm_init(paddr_t table, bool first);
diff --git a/src/arch/fake/inc/hf/arch/addr.h b/src/arch/fake/inc/hf/arch/types.h
similarity index 70%
rename from src/arch/fake/inc/hf/arch/addr.h
rename to src/arch/fake/inc/hf/arch/types.h
index 61483ed..d2cec75 100644
--- a/src/arch/fake/inc/hf/arch/addr.h
+++ b/src/arch/fake/inc/hf/arch/types.h
@@ -16,12 +16,27 @@
 
 #pragma once
 
+#include <stdbool.h>
 #include <stdint.h>
 
 #define PAGE_BITS 12
+#define PAGE_LEVEL_BITS 9
+
+/** The type of a page table entry (PTE). */
+typedef uint64_t pte_t;
 
 /** Integer type large enough to hold a physical address. */
 typedef uintptr_t uintpaddr_t;
 
 /** Integer type large enough to hold a virtual address. */
 typedef uintptr_t uintvaddr_t;
+
+/** The integer large corresponding to the native register size. */
+typedef uint64_t uintreg_t;
+
+/** Type to represent the register state of a VM.  */
+struct arch_regs {
+	uintreg_t r[5];
+	uintreg_t vcpu_index;
+	bool virtual_interrupt;
+};
diff --git a/src/dlog.c b/src/dlog.c
index 9471cea..51ba6fb 100644
--- a/src/dlog.c
+++ b/src/dlog.c
@@ -19,7 +19,8 @@
 #include <stdbool.h>
 #include <stddef.h>
 
-#include "hf/arch.h"
+#include "hf/arch/console.h"
+
 #include "hf/spinlock.h"
 #include "hf/std.h"