Function page_size 

pub exec fn page_size<C: PagingConstsTrait>(level: PagingLevel) -> ret : usize

requires

1 <= level <= C::NR_LEVELS() + 1,

ensures

ret == page_size_spec::<C>(level),

is_pow2(ret as int),

ret >= C::BASE_PAGE_SIZE(),

The page size at a given level.