Skip to main content

frame_idx_at

ostd::specs::mm::frame::segment

Function frame_idx_at 

Source 
pub open spec fn frame_idx_at(range_start: usize, j: int) -> usize
Expand description
{ frame_to_index((range_start + j * PAGE_SIZE) as usize) }

Helper spec: the slot index of the j-th frame in a segment whose physical range starts at range_start. Unlike a let-bound ghost closure (which Verus treats opaquely under SMT), a spec fn is auto-unfolded so equalities between frame_idx_at(...) and frame_to_index(...) are derivable.