Skip to main content

axiom_leading_bits_bounded

ostd::specs::mm::page_table

Function axiom_leading_bits_bounded 

Source 
pub proof fn axiom_leading_bits_bounded<C: PageTableConfig>()
Expand description
ensures
C::LEADING_BITS_spec() < 0x1_0000_usize,

Runtime bound on LEADING_BITS_spec: every valid config uses at most the 16 high bits.

Axiomatized because the trait doesn’t enforce it structurally — the two configs in this codebase (UserPtConfig with 0 and KernelPtConfig with 0xffff) both satisfy it, and any future config that wants the vaddr_of / Mapping arithmetic to work without wrap must too.