Constant seL4_X86_EPTPML4IndexBits 

pub const seL4_X86_EPTPML4IndexBits: u32 = 9;