Struct Entry Owner &nbsp; Copy item path

impl<C: PageTableConfig> EntryOwner<C>

pub open spec fn from_pte_regions_spec( self, regions: MetaRegionOwners, ) -> MetaRegionOwners

{
    if self.is_node() {
        let index = frame_to_index(self.meta_slot_paddr().unwrap());
        let old_slot = regions.slot_owners[index];
        let new_slot = MetaSlotOwner {
            raw_count: 0usize,
            ..old_slot
        };
        MetaRegionOwners {
            slots: regions.slots.insert(index, self.node.unwrap().meta_perm.points_to),
            slot_owners: regions.slot_owners.insert(index, new_slot),
        }
    } else {
        regions
    }
}

pub open spec fn into_pte_regions_spec( self, regions: MetaRegionOwners, ) -> MetaRegionOwners

{
    if self.is_node() {
        let index = frame_to_index(self.meta_slot_paddr().unwrap());
        let old_slot = regions.slot_owners[index];
        let new_slot = MetaSlotOwner {
            raw_count: (old_slot.raw_count + 1) as usize,
            ..old_slot
        };
        MetaRegionOwners {
            slots: regions.slots,
            slot_owners: regions.slot_owners.insert(index, new_slot),
            ..regions
        }
    } else {
        regions
    }
}

pub open spec fn into_pte_owner_spec(self) -> EntryOwner<C>

{
    EntryOwner {
        in_scope: false,
        ..self
    }
}

pub open spec fn from_pte_owner_spec(self) -> EntryOwner<C>

{
    EntryOwner {
        in_scope: true,
        ..self
    }
}

pub open spec fn pte_invariants(self, pte: C::E, regions: MetaRegionOwners) -> bool

{
    &&& self.inv()
    &&& regions.inv()
    &&& self.match_pte(pte, self.parent_level)
    &&& self.relate_region(regions)
    &&& !self.in_scope

}

This is equivalent to the other invariants relations, combining the inv predicates for each object and the well-formedness relations between them.

impl<C: PageTableConfig> EntryOwner<C>

pub open spec fn is_node(self) -> bool

{ self.node is Some }

pub open spec fn is_frame(self) -> bool

{ self.frame is Some }

pub open spec fn is_locked(self) -> bool

{ self.locked is Some }

pub open spec fn is_absent(self) -> bool

{ self.absent }

pub open spec fn new_absent_spec( path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, ) -> Self

{
    EntryOwner {
        node: None,
        frame: None,
        locked: None,
        absent: true,
        in_scope: true,
        path,
        parent_level,
    }
}

pub open spec fn new_frame_spec( paddr: Paddr, path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, prop: PageProperty, ) -> Self

{
    EntryOwner {
        node: None,
        frame: Some(FrameEntryOwner {
            mapped_pa: paddr,
            size: page_size(parent_level),
            prop,
        }),
        locked: None,
        absent: false,
        in_scope: true,
        path,
        parent_level,
    }
}

pub open spec fn new_node_spec(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> Self

{
    EntryOwner {
        node: Some(node),
        frame: None,
        locked: None,
        absent: false,
        in_scope: true,
        path,
        parent_level: (node.level + 1) as PagingLevel,
    }
}

pub proof fn new_absent(path: TreePath<NR_ENTRIES>, parent_level: PagingLevel) -> tracked Self

pub proof fn new_frame( paddr: Paddr, path: TreePath<NR_ENTRIES>, parent_level: PagingLevel, prop: PageProperty, ) -> tracked Self

pub proof fn new_node(node: NodeOwner<C>, path: TreePath<NR_ENTRIES>) -> tracked Self

pub open spec fn match_pte(self, pte: C::E, parent_level: PagingLevel) -> bool

{
    &&& pte.paddr() % PAGE_SIZE == 0
    &&& pte.paddr() < MAX_PADDR
    &&& !pte.is_present() ==> { self.is_absent() }
    &&& pte.is_present() && !pte.is_last(parent_level)
        ==> {
            &&& self.is_node()
            &&& meta_to_frame(self.node.unwrap().meta_perm.addr()) == pte.paddr()

        }
    &&& pte.is_present() && pte.is_last(parent_level)
        ==> {
            &&& self.is_frame()
            &&& self.frame.unwrap().mapped_pa == pte.paddr()
            &&& self.frame.unwrap().prop == pte.prop()

        }

}

pub proof fn absent_match_pte(owner: Self, pte: C::E, parent_level: PagingLevel)

requires

owner.is_absent(),

pte == C::E::new_absent_spec(),

pte.paddr() % PAGE_SIZE == 0,

pte.paddr() < MAX_PADDR,

ensures

owner.match_pte(pte, parent_level),

When owner is absent and pte is the absent PTE with valid paddr, match_pte holds.

pub open spec fn expected_raw_count(self) -> usize

{ if self.in_scope { 0 } else { 1 } }

pub open spec fn relate_region(self, regions: MetaRegionOwners) -> bool

{
    if self.is_node() {
        let idx = frame_to_index(self.meta_slot_paddr().unwrap());
        &&& regions.slot_owners[idx].inner_perms.ref_count.value() != REF_COUNT_UNUSED
        &&& regions.slot_owners[idx].raw_count == self.expected_raw_count()
        &&& regions.slot_owners[idx].self_addr == self.node.unwrap().meta_perm.addr()
        &&& self.node.unwrap().meta_perm.points_to.value().wf(regions.slot_owners[idx])
        &&& regions.slot_owners[idx].path_if_in_pt is Some
            ==> regions.slot_owners[idx].path_if_in_pt.unwrap() == self.path

    } else if self.is_frame() {
        regions
            .slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())]
            .path_if_in_pt is Some
            ==> regions
                .slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())]
                .path_if_in_pt
                .unwrap() == self.path
    } else {
        true
    }
}

pub proof fn get_path(self) -> tracked TreePath<NR_ENTRIES>

pub open spec fn meta_slot_paddr(self) -> Option<Paddr>

{
    if self.is_node() {
        Some(meta_to_frame(self.node.unwrap().meta_perm.addr()))
    } else if self.is_frame() {
        Some(self.frame.unwrap().mapped_pa)
    } else {
        None
    }
}

pub open spec fn meta_slot_paddr_neq(self, other: Self) -> bool

{
    self.meta_slot_paddr() is Some
        ==> (other.meta_slot_paddr() is Some
            ==> self.meta_slot_paddr().unwrap() != other.meta_slot_paddr().unwrap())
}

pub proof fn nodes_different_paths_different_addrs( self, other: Self, regions: MetaRegionOwners, )

requires

self.is_node(),

other.is_node(),

self.relate_region(regions),

self.meta_slot_paddr() is Some
    ==> regions
        .slot_owners[frame_to_index(self.meta_slot_paddr().unwrap())]
        .path_if_in_pt is Some,

other.meta_slot_paddr() is Some
    ==> regions
        .slot_owners[frame_to_index(other.meta_slot_paddr().unwrap())]
        .path_if_in_pt is Some,

other.relate_region(regions),

self.path != other.path,

ensures

self.node.unwrap().meta_perm.addr() != other.node.unwrap().meta_perm.addr(),

Two nodes satisfying relate_region with the same regions have different addresses if and only if they have different paths.

Trait Implementations§

impl<C: PageTableConfig> Inv for EntryOwner<C>

open spec fn inv(self) -> bool

{
    &&& self.node is Some
        ==> {
            &&& self.frame is None
            &&& self.locked is None
            &&& self.node.unwrap().inv()
            &&& !self.absent

        }
    &&& self.frame is Some
        ==> {
            &&& self.node is None
            &&& self.locked is None
            &&& !self.absent
            &&& self.frame.unwrap().mapped_pa % PAGE_SIZE == 0
            &&& self.frame.unwrap().mapped_pa < MAX_PADDR
            &&& self.frame.unwrap().size == page_size(self.parent_level)

        }
    &&& self.locked is Some
        ==> {
            &&& self.frame is None
            &&& self.node is None
            &&& !self.absent

        }
    &&& self.path.inv()

}

open spec fn default(lv: nat) -> Self

{
    Self {
        in_scope: false,
        path: TreePath::new(Seq::empty()),
        parent_level: (INC_LEVELS - lv + 1) as PagingLevel,
        node: None,
        frame: None,
        locked: None,
        absent: true,
    }
}

proof fn default_preserves_inv()

open spec fn la_inv(self, lv: nat) -> bool

{ self.is_node() ==> lv < L - 1 }

proof fn default_preserves_la_inv()

open spec fn rel_children(self, i: int, child: Option<Self>) -> bool

{
    if self.is_node() {
        &&& child is Some
        &&& child.unwrap().path.len() == self.node.unwrap().tree_level + 1
        &&& child
            .unwrap()
            .match_pte(
                self.node.unwrap().children_perm.value()[i],
                self.node.unwrap().level,
            )
        &&& child.unwrap().path == self.path.push_tail(i as usize)

    } else {
        &&& child is None

    }
}

proof fn default_preserves_rel_children(self, lv: nat)

impl<C: PageTableConfig> View for EntryOwner<C>

open spec fn view(&self) -> <Self as View>::V

{
    if let Some(frame) = self.frame {
        EntryView::Leaf {
            leaf: LeafPageTableEntryView {
                map_va: vaddr(self.path) as int,
                map_to_pa: frame.mapped_pa as int,
                level: self.path.len() as u8,
                prop: frame.prop,
                phantom: PhantomData,
            },
        }
    } else if let Some(node) = self.node {
        EntryView::Intermediate {
            node: IntermediatePageTableEntryView {
                map_va: vaddr(self.path) as int,
                map_to_pa: meta_to_frame(node.meta_perm.addr()) as int,
                level: self.path.len() as u8,
                phantom: PhantomData,
            },
        }
    } else if let Some(view) = self.locked {
        EntryView::LockedSubtree {
            views: view@,
        }
    } else {
        EntryView::Absent
    }
}

type V = EntryView<C>

Auto Trait Implementations§

impl<C> Freeze for EntryOwner<C>

impl<C> !RefUnwindSafe for EntryOwner<C>

impl<C> Send for EntryOwner<C>

impl<C> Sync for EntryOwner<C>

impl<C> Unpin for EntryOwner<C>
where <C as PageTableConfig>::E: Unpin, C: Unpin,

impl<C> UnwindSafe for EntryOwner<C>
where <C as PageTableConfig>::E: UnwindSafe, C: UnwindSafe,

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T, U> TryFrom for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

impl<T, U> TryInto for T
where U: TryFrom<T>,

type Error = >::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, >::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool