Skip to main content

lemma_index_to_frame_biinjective

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

Function lemma_index_to_frame_biinjective 

Source 
pub broadcast proof fn lemma_index_to_frame_biinjective(index: int)
Expand description
requires
0 <= index < max_meta_slots(),
ensures
#[trigger] index_to_frame(index) % PAGE_SIZE == 0,
frame_to_index(index_to_frame(index)) == index,

Converting an in-range metadata-slot index to its frame address and back preserves the index, and the resulting address is page aligned.