Skip to main content

lemma_meta_addr_to_index

ostd::specs::mm::frame::meta_specs

Function lemma_meta_addr_to_index 

Source 
pub broadcast proof fn lemma_meta_addr_to_index(i: usize)
Expand description
requires
i < MAX_NR_PAGES,
ensures
#[trigger] frame_to_index(meta_to_frame_spec(meta_addr(i))) == i,

Index round-trip: the slot index recovered from a slot’s metadata address is the original index. Callers holding ptr.addr() == meta_addr(slot_index) (via crate::mm::frame::unique::UniqueFrame::wf) use this to re-derive region facts phrased over frame_to_index(meta_to_frame(ptr.addr)) at slot_index (e.g. recovering ref_count == REF_COUNT_UNIQUE from global_inv).