Function vm_space_root_idx 

pub open spec fn vm_space_root_idx(owner: VmSpaceOwner) -> int

{ frame_to_index(owner.page_table_owner.value().meta_slot_paddr()->0) }

The metadata-slot index of a VmSpace’s page-table root node. This is the slot whose owner VmSpace::new (empty_with_owner) rewrites from unused to an active page-table node; the perm itself stays in regions.slots.