diff --git a/kern/arch/x86/vmm/intel/vmx.c b/kern/arch/x86/vmm/intel/vmx.c
index 5384c4e..6f9cef7 100644
--- a/kern/arch/x86/vmm/intel/vmx.c
+++ b/kern/arch/x86/vmm/intel/vmx.c
@@ -1422,3 +1422,8 @@
 	gpc->vmcs_core_id = core_id();
 	PERCPU_VAR(gpc_to_clear_to) = gpc;
 }
+
+uint64_t gpc_get_eptp(struct guest_pcore *gpc)
+{
+	return gpc->proc->env_pgdir.eptp;
+}
diff --git a/kern/arch/x86/vmm/intel/vmx.h b/kern/arch/x86/vmm/intel/vmx.h
index b40bd6f..e6b50ac 100644
--- a/kern/arch/x86/vmm/intel/vmx.h
+++ b/kern/arch/x86/vmm/intel/vmx.h
@@ -58,6 +58,20 @@
 	uint32_t vmentry_ctrl;
 };
 
+struct guest_pcore {
+	int cpu;
+	struct proc *proc;
+	unsigned long *posted_irq_desc;
+	struct vmcs *vmcs;
+	int vmcs_core_id;
+	bool should_vmresume;
+	uint64_t xcr0;
+	uint64_t msr_kern_gs_base;
+	uint64_t msr_star;
+	uint64_t msr_lstar;
+	uint64_t msr_sfmask;
+};
+
 #define NR_AUTOLOAD_MSRS 8
 
 /* the horror. */
@@ -99,15 +113,6 @@
 
 extern char * const VMX_EXIT_REASON_NAMES[];
 
-
-int vmx_init(void);
-void vmx_exit(void);
-int intel_vmm_init(void);
-int intel_vmm_pcpu_init(void);
-int ept_fault_pages(void *dir, uint32_t start, uint32_t end);
-int ept_check_page(void *dir, unsigned long addr);
-int vmx_do_ept_fault(void *dir, unsigned long gpa, unsigned long gva, int fault_flags);
-
 static inline void native_store_idt(pseudodesc_t *dtr);
 static inline unsigned long get_desc_base(const struct desc_struct *desc);
 static inline void native_store_gdt(pseudodesc_t *dtr);
@@ -138,7 +143,6 @@
 static inline void vpid_sync_gpc_single(uint16_t vpid);
 static inline void vpid_sync_gpc_global(void);
 static inline void vpid_sync_context(uint16_t vpid);
-static inline uint64_t gpc_get_eptp(struct guest_pcore *gpc);
 
 /* no way to get around some of this stuff. */
 /* we will do the bare minimum required. */
@@ -338,11 +342,6 @@
 		vpid_sync_gpc_global();
 }
 
-static inline uint64_t gpc_get_eptp(struct guest_pcore *gpc)
-{
-	return gpc->proc->env_pgdir.eptp;
-}
-
 static inline unsigned long vmcs_read(unsigned long field)
 {
 	unsigned long value;
@@ -388,6 +387,9 @@
 	uint32_t try_set_0;
 };
 
+int intel_vmm_init(void);
+int intel_vmm_pcpu_init(void);
 void vmx_load_guest_pcore(struct guest_pcore *gpc);
 void vmx_unload_guest_pcore(struct guest_pcore *gpc);
+uint64_t gpc_get_eptp(struct guest_pcore *gpc);
 void vmx_clear_vmcs(void);
diff --git a/kern/arch/x86/vmm/vmm.h b/kern/arch/x86/vmm/vmm.h
index 5c043fe..9ae840d 100644
--- a/kern/arch/x86/vmm/vmm.h
+++ b/kern/arch/x86/vmm/vmm.h
@@ -1,6 +1,7 @@
 #pragma once
 
 #include <ros/vmm.h>
+#include <arch/vmm/intel/vmx.h>
 
 static inline int cpu_has_vmx(void)
 {
@@ -16,20 +17,6 @@
 
 #define VMM_VMEXIT_NR_TYPES		65
 
-struct guest_pcore {
-	int cpu;
-	struct proc *proc;
-	unsigned long *posted_irq_desc;
-	struct vmcs *vmcs;
-	int vmcs_core_id;
-	bool should_vmresume;
-	uint64_t xcr0;
-	uint64_t msr_kern_gs_base;
-	uint64_t msr_star;
-	uint64_t msr_lstar;
-	uint64_t msr_sfmask;
-};
-
 struct vmm {
 	spinlock_t lock;	/* protects guest_pcore assignment */
 	qlock_t qlock;
@@ -66,9 +53,6 @@
 void __vmm_struct_cleanup(struct proc *p);
 int vmm_poke_guest(struct proc *p, int guest_pcoreid);
 
-int intel_vmx_start(int id);
-int intel_vmx_setup(int nvmcs);
-
 struct guest_pcore *create_guest_pcore(struct proc *p,
                                        struct vmm_gpcore_init *gpci);
 void destroy_guest_pcore(struct guest_pcore *vcpu);