Constant seL4_X86_EPTPTIndexBits 

pub const seL4_X86_EPTPTIndexBits: u32 = 9;