Constant seL4_X86_EPTPDIndexBits 

pub const seL4_X86_EPTPDIndexBits: u32 = 9;