Skip to main content

lemma_frame_to_index_injective

ostd::specs::mm::frame::mapping

Function lemma_frame_to_index_injective 

Source 
pub broadcast proof fn lemma_frame_to_index_injective(p1: Paddr, p2: Paddr)
Expand description
requires
p1 % PAGE_SIZE == 0,
p2 % PAGE_SIZE == 0,
p1 != p2,
ensures
#[trigger] frame_to_index(p1) != #[trigger] frame_to_index(p2),

frame_to_index is injective on page-aligned paddrs.