PageTableOwner

ostd::specs::mm::page_table

Struct PageTableOwner 

Source 
pub struct PageTableOwner<C: PageTableConfig>(pub OwnerSubtree<C>);

Tuple Fields§

§0: OwnerSubtree<C>

Implementations§

Source§

impl<C: PageTableConfig> PageTableOwner<C>

Source

pub uninterp fn new_cursor_owner_spec<'rcu>(self) -> (Self, CursorOwner<'rcu, C>)

Source§

impl<C: PageTableConfig> PageTableOwner<C>

Source

pub open spec fn view_rec(self, path: TreePath<CONST_NR_ENTRIES>) -> Set<Mapping>

{
    if self.0.value.is_frame() {
        let vaddr = vaddr(path);
        let pt_level = INC_LEVELS() - path.len();
        let page_size = page_size(pt_level as PagingLevel);
        set![
            Mapping { va_range : Range { start : vaddr, end : (vaddr + page_size) as
            Vaddr }, pa_range : Range { start : self.0.value.frame.unwrap().mapped_pa,
            end : (self.0.value.frame.unwrap().mapped_pa + page_size) as Paddr, },
            page_size : page_size, property : self.0.value.frame.unwrap().prop, }
        ]
    } else if self.0.value.is_node() && path.len() < INC_LEVELS() - 1 {
        Set::new(|m: Mapping| {
            exists |i: int| {
                0 <= i < self.0.children.len() && self.0.children[i] is Some
                    && PageTableOwner(self.0.children[i].unwrap())
                        .view_rec(path.push_tail(i as usize))
                        .contains(m)
            }
        })
    } else {
        set![]
    }
}
Source

pub proof fn view_rec_contains(self, path: TreePath<CONST_NR_ENTRIES>, m: Mapping)

requires
self.0.inv(),
path.len() < INC_LEVELS() - 1,
path.len() == self.0.level,
self.view_rec(path).contains(m),
self.0.value.is_node(),
ensures
exists |i: int| {
    0 <= i < self.0.children.len() && self.0.children[i] is Some
        && PageTableOwner(self.0.children[i].unwrap())
            .view_rec(path.push_tail(i as usize))
            .contains(m)
},
Source

pub proof fn view_rec_contains_choose( self, path: TreePath<CONST_NR_ENTRIES>, m: Mapping, ) -> i : int

requires
self.0.inv(),
path.len() < INC_LEVELS() - 1,
path.len() == self.0.level,
self.view_rec(path).contains(m),
self.0.value.is_node(),
ensures
0 <= i < self.0.children.len() && self.0.children[i] is Some
    && PageTableOwner(self.0.children[i].unwrap())
        .view_rec(path.push_tail(i as usize))
        .contains(m),
Source

pub proof fn view_rec_vaddr_range(self, path: TreePath<CONST_NR_ENTRIES>, m: Mapping)

requires
self.0.inv(),
path.len() <= INC_LEVELS() - 1,
path.len() == self.0.level,
self.view_rec(path).contains(m),
ensures
vaddr(path) <= m.va_range.start < m.va_range.end
    <= vaddr(path) + page_size(path.len() as PagingLevel),
Source

pub proof fn view_rec_disjoint_vaddrs( self, path: TreePath<CONST_NR_ENTRIES>, m1: Mapping, m2: Mapping, )

requires
self.0.inv(),
path.len() <= INC_LEVELS() - 1,
path.len() == self.0.level,
self.view_rec(path).contains(m1),
self.view_rec(path).contains(m2),
m1 != m2,
ensures
m1.va_range.end <= m2.va_range.start || m2.va_range.end <= m1.va_range.start,
Source

pub open spec fn relate_region_rec( self, path: TreePath<CONST_NR_ENTRIES>, regions: MetaRegionOwners, ) -> bool

{
    if self.0.value.is_node() {
        &&& self.0.value.node.unwrap().path == path
        &&& self.0.value.node.unwrap().relate_region(regions)
        &&& forall |i: int| {
            0 <= i < self.0.children.len() && self.0.children[i] is Some
                ==> PageTableOwner(self.0.children[i].unwrap())
                    .relate_region_rec(path.push_tail(i as usize), regions)
        }

    } else {
        true
    }
}
Source

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

{ self.relate_region_rec(TreePath::new(Seq::empty()), regions) }

Trait Implementations§

Source§

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

Source§

open spec fn inv(self) -> bool

{
    &&& self.0.inv()

}
Source§

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

Source§

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

{
    let mappings = self.view_rec(TreePath::new(Seq::empty()));
    PageTableView { mappings }
}
Source§

type V = PageTableView

Auto Trait Implementations§

§

impl<C> Freeze for PageTableOwner<C>

§

impl<C> !RefUnwindSafe for PageTableOwner<C>

§

impl<C> Send for PageTableOwner<C>

§

impl<C> Sync for PageTableOwner<C>

§

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

§

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

Blanket Implementations§

Source§

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

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

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

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

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

Source§

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

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

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

Source§

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

Source§

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<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

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

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::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>

Source§

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

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::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<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>