Constant seL4_PUDIndexBits 

pub const seL4_PUDIndexBits: u32 = 9;