Function index_to_frame_spec Copy item path

pub open spec fn index_to_frame_spec(index: usize) -> Paddr

{ (index * PAGE_SIZE()) as usize }