Constant seL4_PGDIndexBits 

pub const seL4_PGDIndexBits: u32 = 9;