Constant seL4_X86_EPTPDPTIndexBits 

pub const seL4_X86_EPTPDPTIndexBits: u32 = 9;