Skip to main content

lemma_sign_bit_facts

ostd::specs::mm::page_table::vaddr_range_proofs

Function lemma_sign_bit_facts 

Source 
pub proof fn lemma_sign_bit_facts<C: PageTableConfig>(
    va: Vaddr,
    address_width: usize,
    shift: usize,
    shifted: usize,
    bit: usize,
)
Expand description
requires
address_width == C::ADDRESS_WIDTH(),
shift == address_width - 1,
shifted == va >> shift,
bit == shifted & 1usize,
ensures
(bit != 0) == ((va as int / pow2((C::ADDRESS_WIDTH() - 1) as nat) as int) % 2 == 1),

Facts needed to connect (va >> (ADDRESS_WIDTH - 1)) & 1 with the arithmetic bit-test specification.