pa_is_valid_pt_address

ostd::specs::mm::page_table::node::entry_view

Function pa_is_valid_pt_address 

Source 
pub open spec fn pa_is_valid_pt_address(pa: int) -> bool
Expand description
{
    &&& pa_is_valid_kernel_address(pa as int)
    &&& pa % PAGE_SIZE() as int == 0

}