Skip to main content

CursorOwner

ostd::specs::mm::page_table::cursor::owners

Struct CursorOwner 

Source 
pub struct CursorOwner<'rcu, C: PageTableConfig> {
    pub level: PagingLevel,
    pub continuations: Map<int, CursorContinuation<'rcu, C>>,
    pub va: Vaddr,
    pub guard_level: PagingLevel,
    pub prefix: Vaddr,
    pub popped_too_high: bool,
}

Fields§

§level: PagingLevel§continuations: Map<int, CursorContinuation<'rcu, C>>§va: Vaddr§guard_level: PagingLevel§prefix: Vaddr§popped_too_high: bool

Implementations§

Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

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

requires
self.inv(),
self.in_locked_range(),
!self.popped_too_high,
self.metaregion_sound(regions),
self.cur_entry_owner().is_frame(),
other.cur_entry_owner().is_frame(),
other.cur_entry_owner().inv(),
other.cur_entry_owner().frame().mapped_pa == self.cur_entry_owner().frame().mapped_pa,
other.cur_entry_owner().path == self.cur_entry_owner().path,
other.cur_entry_owner().parent_level == self.cur_entry_owner().parent_level,
self.level == other.level,
self.guard_level == other.guard_level,
self.va == other.va,
self.prefix == other.prefix,
self.popped_too_high == other.popped_too_high,
forall |i: int| {
    self.level <= i < NR_LEVELS
        ==> #[trigger] self.continuations[i] == other.continuations[i]
},
other.continuations[self.level - 1].inv(),
other.continuations[self.level - 1].all_some(),
other.continuations[self.level - 1].idx == self.continuations[self.level - 1].idx,
other.continuations[self.level - 1].entry_own.parent_level
    == self.continuations[self.level - 1].entry_own.parent_level,
other.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
    == self.continuations[self.level - 1].guard.inner.inner@.ptr.addr(),
other.continuations[self.level - 1].path() == self.continuations[self.level - 1].path(),
other.continuations.dom() =~= self.continuations.dom(),
forall |j: int| {
    0 <= j < NR_ENTRIES && j != self.continuations[self.level - 1].idx
        ==> #[trigger] other.continuations[self.level - 1].children[j]
            == self.continuations[self.level - 1].children[j]
},
({
    let new_child = other
        .continuations[self.level - 1]
        .children[other.continuations[self.level - 1].idx as int]->0;
    let new_path = other
        .continuations[self.level - 1]
        .path()
        .push_tail(other.continuations[self.level - 1].idx as int);
    new_child
        .subtree_satisfies(new_path, PageTableOwner::<C>::metaregion_sound_pred(regions))
}),
other.continuations[self.level - 1].entry_own.metaregion_sound(regions),
ensures
other.inv(),
other.metaregion_sound(regions),
Source

pub proof fn map_branch_none_inv_holds(self, owner0: Self)

requires
owner0.inv(),
self.in_locked_range(),
!self.popped_too_high,
forall |j: int| {
    0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx
        ==> (#[trigger] self.continuations[self.level - 1].children[j])
            == owner0.continuations[owner0.level - 1].children[j]
},
self.level == owner0.level,
self.va == owner0.va,
self.guard_level == owner0.guard_level,
self.prefix == owner0.prefix,
self.popped_too_high == owner0.popped_too_high,
forall |i: int| {
    self.level <= i < NR_LEVELS
        ==> #[trigger] self.continuations[i] == owner0.continuations[i]
},
self.continuations[self.level - 1].inv(),
self.continuations[self.level - 1].all_some(),
self.continuations[self.level - 1].idx == owner0.continuations[owner0.level - 1].idx,
self.continuations[self.level - 1].entry_own.parent_level
    == owner0.continuations[owner0.level - 1].entry_own.parent_level,
self.continuations[self.level - 1].guard.inner.inner@.ptr.addr()
    == owner0.continuations[owner0.level - 1].guard.inner.inner@.ptr.addr(),
self.continuations[self.level - 1].path()
    == owner0.continuations[owner0.level - 1].path(),
pte_index_spec::<C>(self.cur_va(), (self.level - 1 + 1) as PagingLevel)
    == self.continuations[self.level - 1].idx,
self.continuations.dom() =~= owner0.continuations.dom(),
ensures
self.inv(),
Source

pub proof fn map_branch_none_no_new_mappings(self, owner0: Self)

requires
owner0.inv(),
owner0.in_locked_range(),
self.inv(),
self.in_locked_range(),
self.level == owner0.level,
self.va == owner0.va,
forall |i: int| {
    self.level <= i < NR_LEVELS
        ==> #[trigger] self.continuations[i] == owner0.continuations[i]
},
owner0
    .continuations[owner0.level - 1]
    .children[owner0.continuations[owner0.level - 1].idx as int] is Some,
owner0
    .continuations[owner0.level - 1]
    .children[owner0.continuations[owner0.level - 1].idx as int]->0
    .value()
    .is_absent(),
self
    .continuations[self.level - 1]
    .children[self.continuations[self.level - 1].idx as int] is Some,
self
    .continuations[self.level - 1]
    .children[self.continuations[self.level - 1].idx as int]->0
    .value()
    .is_node(),
self.continuations[self.level - 1].path()
    == owner0.continuations[owner0.level - 1].path(),
forall |j: int| {
    0 <= j < NR_ENTRIES && j != owner0.continuations[owner0.level - 1].idx as int
        ==> #[trigger] self.continuations[self.level - 1].children[j]
            == owner0.continuations[owner0.level - 1].children[j]
},
PageTableOwner(
        self
            .continuations[self.level - 1]
            .children[self.continuations[self.level - 1].idx as int]->0,
    )
    .view_rec(
        self
            .continuations[self.level - 1]
            .path()
            .push_tail(self.continuations[self.level - 1].idx as int),
    ) =~= Set::<Mapping>::empty(),
ensures
self.view_mappings() == owner0.view_mappings(),

After alloc_if_none (absent->node), view_mappings is unchanged (both contribute zero mappings).

Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub open spec fn max_steps_subtree(level: usize) -> nat

{
    if level <= 1 {
        NR_ENTRIES as nat
    } else {
        (NR_ENTRIES as nat) * (Self::max_steps_subtree((level - 1) as usize) + 1)
    }
}

The number of steps it will take to walk through every node of a full page table at level level

Source

pub open spec fn max_steps_partial(self, level: usize) -> nat

{
    if level > NR_LEVELS {
        0
    } else {
        let cont = self.continuations[level - 1];
        let count: nat = (NR_ENTRIES - cont.idx - 1) as nat;
        let steps = Self::max_steps_subtree(level) * count;
        let remaining_steps = self.max_steps_partial((level + 1) as usize);
        steps + remaining_steps
    }
}

Per-level “above-current” contribution: count NR_ENTRIES - cont.idx - 1 at every level (the entry at cont.idx is being descended into; its work is captured at lower levels in the recursion). max_steps() adds back one subtree(self.level) to count the current level’s in-progress entry.

The base case is level > NR_LEVELS (not == NR_LEVELS) so that level == NR_LEVELS itself contributes a non-zero term. This avoids degenerate behavior at the root: without it, max_steps collapses to 0 at the root and push_level from the root cannot decrease (and the popped_too_high q at NR_LEVELS would dominate self).

Source

pub open spec fn max_steps(self) -> nat

{
    (self.max_steps_partial(self.level as usize)
        + Self::max_steps_subtree(self.level as usize)) as nat
}
Source

pub proof fn max_steps_partial_eq(self, other: Self, start: usize)

requires
1 <= start <= NR_LEVELS + 1,
forall |k: int| {
    start - 1 <= k < NR_LEVELS
        ==> #[trigger] self.continuations[k].idx == other.continuations[k].idx
},
ensures
self.max_steps_partial(start) == other.max_steps_partial(start),

Two owners with the same idx values from start upward have the same max_steps_partial.

Source

pub proof fn max_steps_partial_inv(self, other: Self, level: usize)

requires
self.inv(),
other.inv(),
self.level == other.level,
self.level <= level <= NR_LEVELS + 1,
forall |i: int| {
    self.level - 1 <= i < NR_LEVELS
        ==> self.continuations[i].idx == other.continuations[i].idx
},
ensures
self.max_steps_partial(level) == other.max_steps_partial(level),
Source

pub open spec fn push_level_owner(self, guard: PageTableGuard<'rcu, C>) -> Self

{
    let cont = self.continuations[self.level - 1];
    let (child, cont) = cont
        .make_cont(
            pte_index_spec::<C>(self.cur_va(), (self.level - 1) as PagingLevel),
            guard,
        );
    let new_continuations = self
        .continuations
        .insert(self.level - 1, cont)
        .insert(self.level - 2, child);
    let new_level = (self.level - 1) as u8;
    Self {
        continuations: new_continuations,
        level: new_level,
        popped_too_high: false,
        ..self
    }
}
Source

pub proof fn push_level_owner_decreases_steps(self, guard: PageTableGuard<'rcu, C>)

requires
self.inv(),
self.level > 1,
ensures
self.push_level_owner(guard).max_steps() < self.max_steps(),
Source

pub proof fn push_level_owner_preserves_mappings(self, guard: PageTableGuard<'rcu, C>)

requires
self.inv(),
self.level > 1,
self.cur_entry_owner().is_node(),
ensures
self.push_level_owner(guard)@.mappings == self@.mappings,
Source

pub proof fn push_level_owner_preserves_inv(self, guard: PageTableGuard<'rcu, C>)

requires
self.inv(),
self.level > 1,
!self.popped_too_high,
self.level <= self.guard_level,
self.in_locked_range(),
self.cur_entry_owner().is_node(),
self.cur_entry_owner().node().relate_guard(guard),
forall |i: int| {
    self.level - 1 <= i < NR_LEVELS
        ==> self.continuations[i].guard.inner.inner@.ptr.addr()
            != guard.inner.inner@.ptr.addr()
},
ensures
self.push_level_owner(guard).inv(),
Source

pub proof fn push_level_owner_preserves_invs( self, guard: PageTableGuard<'rcu, C>, regions: MetaRegionOwners, guards: Guards, )

requires
self.inv(),
self.level > 1,
!self.popped_too_high,
self.level <= self.guard_level,
self.in_locked_range(),
self.only_current_locked(guards),
self.nodes_locked(guards),
self.metaregion_sound(regions),
self.cur_entry_owner().is_node(),
self.cur_entry_owner().node().relate_guard(guard),
guards.lock_held(guard.inner.inner@.ptr.addr()),
ensures
self.push_level_owner(guard).inv(),
self.push_level_owner(guard).children_not_locked(guards),
self.push_level_owner(guard).nodes_locked(guards),
self.push_level_owner(guard).metaregion_sound(regions),
Source

pub proof fn tracked_push_level_owner(tracked &mut self, guard: PageTableGuard<'rcu, C>)

requires
old(self).inv(),
old(self).level > 1,
ensures
*final(self) == old(self).push_level_owner(guard),
Source

pub open spec fn pop_level_owner(self) -> (Self, PageTableGuard<'rcu, C>)

{
    let child = self.continuations[self.level - 1];
    let cont = self.continuations[self.level as int];
    let (new_cont, guard) = cont.restore(child);
    let new_continuations = self
        .continuations
        .insert(self.level as int, new_cont)
        .remove(self.level - 1);
    let new_level = (self.level + 1) as u8;
    let popped_too_high = if new_level >= self.guard_level { true } else { false };
    (
        Self {
            continuations: new_continuations,
            level: new_level,
            popped_too_high: popped_too_high,
            ..self
        },
        guard,
    )
}
Source

pub proof fn pop_level_owner_preserves_invs( self, guards: Guards, regions: MetaRegionOwners, )

requires
self.inv(),
self.level < NR_LEVELS,
self.children_not_locked(guards),
self.nodes_locked(guards),
self.metaregion_sound(regions),
ensures
self.pop_level_owner().0.inv(),
self.pop_level_owner().0.only_current_locked(guards),
self.pop_level_owner().0.nodes_locked(guards),
self.pop_level_owner().0.metaregion_sound(regions),
Source

pub open spec fn move_forward_owner_spec(self) -> Self

{
    if self.index() + 1 < NR_ENTRIES {
        self.inc_index().zero_below_level()
    } else if self.level < NR_LEVELS {
        self.pop_level_owner().0.move_forward_owner_spec()
    } else {
        Self {
            va: (self.va + page_size::<C>(C::NR_LEVELS())) as Vaddr,
            popped_too_high: false,
            ..self
        }
    }
}
Source

pub proof fn move_forward_increases_va(self)

requires
self.inv(),
self.level <= NR_LEVELS,
self.in_locked_range(),
!self.popped_too_high,
ensures
self.move_forward_owner_spec().va > self.va,
Source

pub proof fn move_forward_not_popped_too_high(self)

requires
self.inv(),
self.level <= NR_LEVELS,
self.in_locked_range(),
ensures
!self.move_forward_owner_spec().popped_too_high,
Source

pub proof fn move_forward_owner_popped_too_high_decreases(self)

requires
self.inv(),
self.level <= NR_LEVELS,
self.in_locked_range(),
self.popped_too_high,
self.continuations[NR_LEVELS - 1].idx + 1 < NR_ENTRIES,
ensures
self.move_forward_owner_spec().max_steps() + Self::max_steps_subtree(self.level as usize)
    <= self.max_steps(),

Variant of move_forward_owner_decreases_steps for the popped_too_high case. Same postcondition, but precondition allows popped_too_high. Used by the main lemma’s case 2b to handle the chain of pops that move_forward_owner_spec does internally when popped_too_high.

Source

pub proof fn move_forward_owner_decreases_steps(self)

requires
self.inv(),
self.level <= NR_LEVELS,
self.in_locked_range(),
!self.popped_too_high,
self.continuations[NR_LEVELS - 1].idx + 1 < NR_ENTRIES,
ensures
self.move_forward_owner_spec().max_steps() + Self::max_steps_subtree(self.level as usize)
    <= self.max_steps(),
self.move_forward_owner_spec().max_steps() < self.max_steps(),
Source

pub proof fn move_forward_va_is_align_up(self)

requires
self.inv(),
self.level <= NR_LEVELS,
self.in_locked_range(),
!self.popped_too_high,
self.level == self.guard_level ==> self.index() + 1 < NR_ENTRIES,
ensures
self.move_forward_owner_spec().va
    == self@.align_up_spec(page_size::<PagingConsts>(self.level)),

Advancing the cursor reaches the next slot boundary, including carries to a parent.

Source

pub proof fn pop_level_owner_preserves_mappings(self)

requires
self.inv(),
self.level < NR_LEVELS,
self.in_locked_range(),
ensures
self.pop_level_owner().0@.mappings == self@.mappings,

After popping a level, the total view_mappings is preserved. The restored parent at index self.level absorbs the child’s mappings, and both are within the view_mappings range [self.level, NR_LEVELS).

Source

pub proof fn move_forward_owner_preserves_mappings(self)

requires
self.inv(),
self.in_locked_range(),
ensures
self.move_forward_owner_spec()@.mappings == self@.mappings,
Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub open spec fn no_node_at_idx(self, idx: int) -> bool

{
    &&& self
        .map_full_tree(|e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>| {
            e.is_node() && e.meta_slot_paddr() is Some
                ==> frame_to_index(e.meta_slot_paddr()->0) != idx
        })
    &&& forall |i: int| {
        self.level - 1 <= i < NR_LEVELS
            ==> {
                let e = self.continuations[i].entry_own;
                e.is_node() && e.meta_slot_paddr() is Some
                    ==> frame_to_index(e.meta_slot_paddr()->0) != idx
            }
    }

}

Tree-wide predicate: no page-table node in either the cursor’s tree children or its continuation path has metadata slot index idx. Used as the “sanity” precondition of the path-insert preservation lemma: the only kind of entry it can touch with the new path is a frame. Callers satisfy it by observing that page-table node metadata lives in FRAME_METADATA_RANGE, which is disjoint from any data-frame paddr (where paths_in_pt inserts happen).

Source

pub proof fn and_map_full_tree( self, f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, guard: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, )

requires
self.inv(),
self.map_full_tree(f),
self.map_full_tree(guard),
ensures
self.map_full_tree(|e: EntryOwner<C>, p: TreePath<NR_ENTRIES>| f(e, p) && guard(e, p)),

Pointwise conjunction of two tree-wide predicates: if self.map_full_tree(f) and self.map_full_tree(guard) hold, then self.map_full_tree(f && guard) holds. A thin wrapper around OwnerSubtree::lemma_subtree_satisfies_implies_and applied per continuation + per child; extracted so callers don’t have to re-derive the same nested assert forall ... by { lemma_subtree_satisfies_implies_and(...) } block.

Source

pub proof fn no_node_at_idx_from_slot_key( self, regions: MetaRegionOwners, changed_idx: int, )

requires
self.inv(),
regions.inv(),
self.metaregion_sound(regions),
regions.contains(changed_idx),
regions.slot_owners[changed_idx].usage !is PageTable,
ensures
self.no_node_at_idx(changed_idx),

Discharge no_node_at_idx(changed_idx) from the observation that changed_idx is not a page-table slot. Active node entries always occupy metadata slots whose usage is PageTable, so any node in the cursor tree must have a different slot index than changed_idx.

Callers doing a paths_in_pt.insert at a frame’s data-slot (e.g., map and the huge-page split) use this helper to satisfy the precondition of Self::metaregion_preserved_under_path_insert.

Source

pub proof fn metaregion_preserved_under_path_insert( self, regions0: MetaRegionOwners, regions1: MetaRegionOwners, changed_idx: int, new_path: TreePath<NR_ENTRIES>, )

requires
self.inv(),
self.metaregion_sound(regions0),
regions0.inv(),
regions0.contains(changed_idx),
regions1.slots == regions0.slots,
regions1.slot_owners.dom() =~= regions0.slot_owners.dom(),
forall |i: int| i != changed_idx ==> regions0.slot_owners[i] == regions1.slot_owners[i],
regions1.slot_owners[changed_idx].same_permissions(regions0.slot_owners[changed_idx]),
regions1.slot_owners[changed_idx].slot_vaddr
    == regions0.slot_owners[changed_idx].slot_vaddr,
regions1.slot_owners[changed_idx].usage == regions0.slot_owners[changed_idx].usage,
regions1.slot_owners[changed_idx].paths_in_pt
    == regions0.slot_owners[changed_idx].paths_in_pt.insert(new_path),
self.no_node_at_idx(changed_idx),
ensures
self.metaregion_sound(regions1),

Preservation of the cursor-level metaregion invariants when the only change to regions is the insertion of a new path into the paths_in_pt set at a single slot.

Source

pub open spec fn path_removable_at_idx( self, idx: int, removed_path: TreePath<NR_ENTRIES>, ) -> bool

{
    &&& self
        .map_full_tree(|e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>| (
            e.meta_slot_paddr() is Some && frame_to_index(e.meta_slot_paddr()->0) == idx
                ==> !e.is_node() && (e.is_frame() ==> e.path != removed_path)
        ))
    &&& forall |i: int| {
        self.level - 1 <= i < NR_LEVELS
            ==> {
                let e = self.continuations[i].entry_own;
                e.meta_slot_paddr() is Some
                    && frame_to_index(e.meta_slot_paddr()->0) == idx
                    ==> !e.is_node() && (e.is_frame() ==> e.path != removed_path)
            }
    }

}

Tree-wide guard for the removal of removed_path from paths_in_pt[changed_idx]. Mirror of Self::no_node_at_idx but also rules out any frame entry that still maps changed_idx through exactly removed_path — removing that path would break such an entry’s metaregion_sound (paths_in_pt.contains(path)). A node at changed_idx is also excluded (its paths_in_pt is a singleton, so removal would falsify == set![path]). Callers (the unmap site) satisfy this because the entry whose path is being removed has just left the cursor tree.

Source

pub open spec fn no_frame_with_path(self, removed_path: TreePath<NR_ENTRIES>) -> bool

{
    &&& self
        .map_full_tree(|e: EntryOwner<C>, _p: TreePath<NR_ENTRIES>| {
            e.is_frame() ==> e.path != removed_path
        })
    &&& forall |i: int| {
        self.level - 1 <= i < NR_LEVELS
            ==> {
                let e = self.continuations[i].entry_own;
                e.is_frame() ==> e.path != removed_path
            }
    }

}

Tree-wide predicate: no frame entry in the cursor tree has tree path exactly removed_path. After unmap’s replace_cur_entry(Child::None), the entry at the cursor path (== removed_path) is absent, so by tree-path correctness no frame entry can carry that path. This is the one structural residual of the paths_in_pt-removal refactor.

Source

pub proof fn no_frame_with_path_from_no_view_mapping( self, removed_path: TreePath<NR_ENTRIES>, )

requires
self.inv(),
forall |m: Mapping| (
    self@.mappings.contains(m) ==> m.va_range.start != vaddr_of::<C>(removed_path)
),
ensures
self.no_frame_with_path(removed_path),

Establishes Self::no_frame_with_path from the observation that no current view mapping starts at vaddr_of(removed_path).

This is the standalone “lift path_correct_pred + uniqueness over the cursor tree” lemma the unmap site needs. Each continuation child subtree is pt_inv + path-correct (via PageTableOwner::pt_inv_implies_path_correct), and its mappings all bubble up into self@.mappings; so by PageTableOwner::no_frame_with_path_rec a frame entry carrying removed_path would force a mapping starting at vaddr_of(removed_path) into self@.mappings — exactly what the hypothesis forbids. Continuation entries are nodes, so the continuations conjunct is vacuous.

Source

pub proof fn path_removable_from_no_node_and_no_frame_path( self, idx: int, removed_path: TreePath<NR_ENTRIES>, )

requires
self.inv(),
self.no_node_at_idx(idx),
self.no_frame_with_path(removed_path),
ensures
self.path_removable_at_idx(idx, removed_path),

Bridge: path_removable_at_idx follows from the (mechanically dischargeable) no-node-at-idx fact plus the structural no-frame-with-removed_path fact. Per entry mapping idx: no_node_at_idx forces !is_node, and no_frame_with_path forces is_frame ==> path != removed_path — exactly the path_removable_at_idx conjunction.

Source

pub proof fn metaregion_preserved_under_path_remove( self, regions0: MetaRegionOwners, regions1: MetaRegionOwners, changed_idx: int, removed_path: TreePath<NR_ENTRIES>, )

requires
self.inv(),
self.metaregion_sound(regions0),
regions0.inv(),
regions0.contains(changed_idx),
regions1.slots == regions0.slots,
regions1.slot_owners.dom() =~= regions0.slot_owners.dom(),
forall |i: int| i != changed_idx ==> regions0.slot_owners[i] == regions1.slot_owners[i],
regions1.slot_owners[changed_idx].same_permissions(regions0.slot_owners[changed_idx]),
regions1.slot_owners[changed_idx].slot_vaddr
    == regions0.slot_owners[changed_idx].slot_vaddr,
regions1.slot_owners[changed_idx].usage == regions0.slot_owners[changed_idx].usage,
regions1.slot_owners[changed_idx].paths_in_pt
    == regions0.slot_owners[changed_idx].paths_in_pt.remove(removed_path),
self.path_removable_at_idx(changed_idx, removed_path),
ensures
self.metaregion_sound(regions1),

Preservation of the cursor-level metaregion invariants when the only change to regions is the removal of removed_path from the paths_in_pt set at a single slot. Dual of Self::metaregion_preserved_under_path_insert; the missing half of the deferred paths_in_pt refactor that unmap needs.

Removal is not monotone (unlike insert): the guard Self::path_removable_at_idx is what makes it sound — no live tree entry still needs removed_path at changed_idx.

Source

pub proof fn take_next_remove_path_preserves_metaregion( self, owner_before_replace: Self, regions0: MetaRegionOwners, regions1: MetaRegionOwners, removed_idx: int, removed_path: TreePath<NR_ENTRIES>, target: Mapping, )

requires
self.inv(),
owner_before_replace.inv(),
owner_before_replace.in_locked_range(),
self.metaregion_sound(regions0),
regions0.inv(),
regions0.contains(removed_idx),
regions0.slot_owners[removed_idx].usage !is PageTable,
self@.mappings
    == owner_before_replace@.mappings
        - PageTableOwner(owner_before_replace.cur_subtree())@.mappings,
PageTableOwner(owner_before_replace.cur_subtree())@.mappings == set![target],
owner_before_replace.cur_subtree().value().path == removed_path,
regions1.slots == regions0.slots,
regions1.slot_owners.dom() =~= regions0.slot_owners.dom(),
forall |i: int| i != removed_idx ==> regions0.slot_owners[i] == regions1.slot_owners[i],
regions1.slot_owners[removed_idx].same_permissions(regions0.slot_owners[removed_idx]),
regions1.slot_owners[removed_idx].slot_vaddr
    == regions0.slot_owners[removed_idx].slot_vaddr,
regions1.slot_owners[removed_idx].usage == regions0.slot_owners[removed_idx].usage,
regions1.slot_owners[removed_idx].paths_in_pt
    == regions0.slot_owners[removed_idx].paths_in_pt.remove(removed_path),
ensures
self.metaregion_sound(regions1),

Packages the take_next frame-unmap preservation proof after paths_in_pt removes the unmapped frame path from one metadata slot.

Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub proof fn cur_subtree_eq_filtered_mappings_path(self)

requires
self.inv(),
self.in_locked_range(),
ensures
({
    let subtree_va = vaddr_of::<C>(self.cur_subtree().value().path) as int;
    let size = page_size::<PagingConsts>(self.level) as int;
    PageTableOwner(self.cur_subtree())@.mappings
        == self@
            .mappings
            .filter(|m: Mapping| subtree_va <= m.va_range.start < subtree_va + size)
}),

The current subtree’s mappings equal the filter over [subtree_va, subtree_va + page_size(level)) where subtree_va = vaddr(cur_subtree path).

Source

pub proof fn cur_subtree_eq_filtered_mappings(self)

requires
self.inv(),
self.in_locked_range(),
ensures
({
    let start = nat_align_down(
        self@.cur_va as nat,
        page_size::<PagingConsts>(self.level) as nat,
    ) as Vaddr;
    let size = page_size::<PagingConsts>(self.level);
    PageTableOwner(self.cur_subtree())@.mappings
        == self@.mappings.filter(|m: Mapping| start <= m.va_range.start < start + size)
}),

Version using nat_align_down(cur_va, page_size(level)) in the filter. Uses the shared canonical subtree boundary rather than reconstructing the VA path.

Source

pub proof fn subtree_va_ranges_disjoint(self, j: int)

requires
self.inv(),
self.in_locked_range(),
0 <= j < NR_ENTRIES,
j != self.index(),
self.continuations[self.level - 1].children[j] is Some,
ensures
vaddr(self.continuations[self.level - 1].path().push_tail(j))
    + vaddr_upper_part_spec::<C>(self.cur_va())
    + page_size::<PagingConsts>(self.level as PagingLevel) <= self.cur_va()
    || self.cur_va()
        < vaddr(self.continuations[self.level - 1].path().push_tail(j))
            + vaddr_upper_part_spec::<C>(self.cur_va()),

Subtrees at different indices have disjoint VA ranges.

Source

pub proof fn higher_level_children_disjoint(self, i: int, j: int)

requires
self.inv(),
self.in_locked_range(),
self.level - 1 < i < NR_LEVELS,
0 <= j < NR_ENTRIES,
j != self.continuations[i].idx,
self.continuations[i].children[j] is Some,
ensures
vaddr(self.continuations[i].path().push_tail(j))
    + vaddr_upper_part_spec::<C>(self.cur_va())
    + page_size::<PagingConsts>((i + 1) as PagingLevel) <= self.cur_va()
    || self.cur_va()
        < vaddr(self.continuations[i].path().push_tail(j))
            + vaddr_upper_part_spec::<C>(self.cur_va()),

Children of higher-level continuations have VA ranges that don’t include cur_va, because cur_va’s indices at those levels match the path to the current position.

Source

pub proof fn mapping_covering_cur_va_from_cur_subtree(self, m: Mapping)

requires
self.inv(),
self.in_locked_range(),
self.view_mappings().contains(m),
m.va_range.start <= self.cur_va() < m.va_range.end,
ensures
PageTableOwner(self.cur_subtree()).view_rec(self.cur_subtree().value().path).contains(m),

Any mapping that covers cur_va must come from the current subtree. This follows from the disjointness of VA ranges and the fact that cur_va falls within the current subtree’s VA range.

Source

pub proof fn view_mappings_replace_lowest( old_self: Self, new_self: Self, old_cont: CursorContinuation<'rcu, C>, new_cont: CursorContinuation<'rcu, C>, )

requires
old_self.inv(),
old_self.in_locked_range(),
new_self.inv(),
old_self.level == new_self.level,
old_self.continuations[old_self.level - 1] == old_cont,
new_self.continuations[new_self.level - 1] == new_cont,
forall |i: int| {
    old_self.level <= i < NR_LEVELS
        ==> old_self.continuations[i] == new_self.continuations[i]
},
ensures
new_self.view_mappings()
    == (old_self.view_mappings() - old_cont.view_mappings())
        .union(new_cont.view_mappings()),

Combined replace: swap the lowest continuation, relating old and new mapping sets. Avoids the Map::remove phantom key issue by requiring both old and new to have inv().

Source

pub proof fn as_page_table_owner_preserves_view_mappings(self)

requires
self.inv(),
ensures
self.as_page_table_owner().view_rec(self.continuations[3].path()) == self.view_mappings(),
self.as_page_table_owner().0.inv(),
self.as_page_table_owner().0.level() == self.continuations[3].tree_level,
self.as_page_table_owner().pt_inv(),
Source

pub proof fn view_mapping_inv(self)

requires
self.inv(),
ensures
forall |m: Mapping| self.view_mappings().contains(m) ==> #[trigger] m.inv(),

Every mapping in the cursor view satisfies Mapping::inv().

Collapses the cursor view into a single-root view_rec and applies view_rec_mapping_inv. Inherits the latter’s two narrow assumes on vaddr(path) arithmetic.

Source

pub proof fn as_page_table_owner_view_non_overlapping(self)

requires
self.inv(),
ensures
self@.non_overlapping(),

Non-overlapping mappings in the cursor view.

Collapses the union-over-continuations view_mappings into a single view_rec rooted at the reconstructed root page table, then applies view_rec_disjoint_vaddrs on that single subtree. Follows from tree structure alone.

Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub open spec fn node_unlocked( guards: Guards, ) -> FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>

{
    |owner: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
        owner.is_node() ==> guards.unlocked(owner.node().slot_vaddr())
    }
}
Source

pub open spec fn node_unlocked_except( guards: Guards, addr: usize, ) -> FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>

{
    |owner: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
        owner.is_node()
            ==> (owner.node().slot_vaddr() != addr
                ==> guards.unlocked(owner.node().slot_vaddr()))
    }
}
Source

pub open spec fn map_full_tree( self, f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, ) -> bool

{
    forall |i: int| {
        self.level - 1 <= i < NR_LEVELS ==> { self.continuations[i].map_children(f) }
    }
}
Source

pub open spec fn map_only_children( self, f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, ) -> bool

{
    forall |i: int| {
        self.level - 1 <= i < NR_LEVELS ==> self.continuations[i].map_children(f)
    }
}
Source

pub open spec fn children_not_locked(self, guards: Guards) -> bool

{ self.map_only_children(Self::node_unlocked(guards)) }
Source

pub proof fn lemma_children_not_locked_unroll(self, guards: Guards)

requires
self.children_not_locked(guards),
ensures
forall |i: int| {
    self.level - 1 <= i < NR_LEVELS
        ==> self.continuations[i].map_children(Self::node_unlocked(guards))
},
Source

pub open spec fn only_current_locked(self, guards: Guards) -> bool

{
    self.map_only_children(
        Self::node_unlocked_except(guards, self.cur_entry_owner().node().slot_vaddr()),
    )
}
Source

pub proof fn lemma_never_drop_restores_children_not_locked( self, guard: PageTableGuard<'rcu, C>, guards0: Guards, guards1: Guards, )

requires
self.inv(),
self.only_current_locked(guards0),
guards0.lock_held(guard.inner.inner@.ptr.addr()),
guards1.guards == guards0.guards.remove(guard.inner.inner@.ptr.addr()),
self.cur_entry_owner().is_node(),
guard.inner.inner@.ptr.addr() == self.cur_entry_owner().node().slot_vaddr(),
ensures
self.children_not_locked(guards1),
Source

pub open spec fn nodes_locked(self, guards: Guards) -> bool

{
    forall |i: int| {
        self.level - 1 <= i < self.guard_level
            ==> { self.continuations[i].node_locked(guards) }
    }
}

After a protect operation that only modifies frame.prop of the current entry, CursorOwner::inv() and metaregion_sound are preserved.

Safety: protect changes only frame.prop and updates parent.children_perm to match. EntryOwner::inv() is preserved (from protect postcondition). metaregion_sound is preserved because it doesn’t use frame.prop. rel_children holds via match_pte (from protect’s wf/node_matching postconditions).

The axiom requires only the semantic properties of the modified entry that are checked by inv and metaregion_sound; the structural identity of other continuations is trusted to hold from the tracked restore operations in the caller.

Source

pub open spec fn index(self) -> usize

{ self.continuations[self.level - 1].idx }
Source

pub open spec fn inc_index(self) -> Self

{
    Self {
        continuations: self
            .continuations
            .insert(self.level - 1, self.continuations[self.level - 1].inc_index()),
        va: vaddr_replace_pte_index_spec::<
            C,
        >(
            self.va,
            self.level,
            self.continuations[self.level - 1].inc_index().idx as int,
        ),
        popped_too_high: false,
        ..self
    }
}
Source

pub proof fn do_inc_index(tracked &mut self)

requires
old(self).inv(),
old(self).level <= old(self).guard_level,
old(self).in_locked_range(),
old(self).continuations[old(self).level - 1].idx + 1 < NR_ENTRIES,
old(self).level == NR_LEVELS
    ==> (old(self).continuations[old(self).level - 1].idx + 1)
        <= C::TOP_LEVEL_INDEX_RANGE().end,
ensures
final(self).inv(),
*final(self) == old(self).inc_index(),
Source

pub proof fn lemma_inv_continuation(self, i: int)

requires
self.inv(),
self.level - 1 <= i <= NR_LEVELS - 1,
ensures
self.continuations.contains_key(i),
self.continuations[i].inv(),
self.continuations[i].children.len() == NR_ENTRIES,
Source

pub open spec fn view_mappings(self) -> Set<Mapping>

{
    self.continuations
        .filter_keys(|k| self.level - 1 <= k < NR_LEVELS)
        .map_values(|cont: CursorContinuation<'rcu, C>| cont.view_mappings())
        .values()
        .flatten()
}
Source

pub broadcast proof fn lemma_view_mappings_contains(self)

requires
1 <= self.level <= NR_LEVELS,
ensures
forall |m: Mapping| {
    #[trigger] self.view_mappings().contains(m)
        ==> exists |i: int| {
            self.level - 1 <= i < NR_LEVELS
                && self.continuations[i].view_mappings().contains(m)
        }
},
Source

pub broadcast proof fn lemma_view_mappings_intro(self, m: Mapping, i: int)

requires
1 <= self.level <= NR_LEVELS,
self.level - 1 <= i < NR_LEVELS,
self.continuations.contains_key(i),
#[trigger] self.continuations[i].view_mappings().contains(m),
ensures
self.view_mappings().contains(m),
Source

pub open spec fn as_page_table_owner(self) -> PageTableOwner<C>

{
    if self.level == 1 {
        let l1 = self.continuations[0];
        let l2 = self.continuations[1].restore(l1).0;
        let l3 = self.continuations[2].restore(l2).0;
        let l4 = self.continuations[3].restore(l3).0;
        l4.as_page_table_owner()
    } else if self.level == 2 {
        let l2 = self.continuations[1];
        let l3 = self.continuations[2].restore(l2).0;
        let l4 = self.continuations[3].restore(l3).0;
        l4.as_page_table_owner()
    } else if self.level == 3 {
        let l3 = self.continuations[2];
        let l4 = self.continuations[3].restore(l3).0;
        l4.as_page_table_owner()
    } else {
        let l4 = self.continuations[3];
        l4.as_page_table_owner()
    }
}
Source

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

{ self.cur_subtree().value() }
Source

pub open spec fn cur_subtree(self) -> OwnerSubtree<C>

{ self.continuations[self.level - 1].children[self.index() as int]->0 }
Source

pub proof fn lemma_cur_frame_clone_requires( self, item: C::Item, pa: Paddr, level: PagingLevel, prop: PageProperty, regions: MetaRegionOwners, )

requires
self.inv(),
regions.inv(),
self.metaregion_sound(regions),
self.cur_entry_owner().is_frame(),
pa == self.cur_entry_owner().frame().mapped_pa,
C::item_from_raw(pa, level, prop, C::item_into_raw(item).3) == item,
C::item_into_raw(item).3@ == self.cur_entry_owner().frame_permission(),
valid_frame_paddr(pa),
C::raw_item_well_formed((pa, level, prop, C::item_into_raw(item).3)),
(C::item_into_raw(item).3@ is Some) == self.cur_entry_owner().frame_is_tracked(),
C::item_into_raw(item).3@ is Some
    ==> (regions.slot_owner(pa).ref_count() < REF_COUNT_MAX || may_panic()),
ensures
item.clone_requires(regions),

Axiom: the item reconstructed from the current frame’s physical address satisfies clone_requires.

Safety: When metaregion_sound holds for a frame entry, the item reconstructed via item_from_raw(pa, ...) is the original frame item. The frame’s slot permission (owned by the cursor) has the correct address, is initialised, and its ref count is in the valid clonable range (> 0, < REF_COUNT_MAX), so clone_requires is satisfied.

This is a trait-level axiom: C::Item::clone_requires is fully generic in the PageTableConfig trait, so the postcondition cannot be discharged without knowing the concrete item type. It holds for every PageTableConfig used in ostd because item_from_raw always returns a freshly-constructed Frame<M> handle whose Frame::<M>::clone_requires unfolds to slot-address equality, initialisation, and a bounded ref-count — all delivered by metaregion_sound for frame entries.

Source

pub proof fn lemma_clone_item_preserves_invariants( self, old_regions: MetaRegionOwners, new_regions: MetaRegionOwners, idx: int, )

requires
self.inv(),
self.metaregion_sound(old_regions),
old_regions.inv(),
self.cur_entry_owner().is_frame(),
idx == frame_to_index(self.cur_entry_owner().frame().mapped_pa),
old_regions.slot_owners.contains_key(idx),
new_regions.slot_owners.contains_key(idx),
new_regions.ref_count(idx) == old_regions.ref_count(idx) + 1,
new_regions.slot_owners[idx].ref_count_perm.id()
    == old_regions.slot_owners[idx].ref_count_perm.id(),
new_regions.slot_owners[idx].metadata_perm.id()
    == old_regions.slot_owners[idx].metadata_perm.id(),
new_regions.slot_owners[idx].metadata_perm.frac() + 1
    == old_regions.slot_owners[idx].metadata_perm.frac(),
new_regions.slot_owners[idx].in_list_perm == old_regions.slot_owners[idx].in_list_perm,
new_regions.slot_owners[idx].paths_in_pt == old_regions.slot_owners[idx].paths_in_pt,
new_regions.slot_owners[idx].slot_vaddr == old_regions.slot_owners[idx].slot_vaddr,
new_regions.slot_owners[idx].usage == old_regions.slot_owners[idx].usage,
new_regions.slot_owners.dom() == old_regions.slot_owners.dom(),
forall |i: int| {
    i != idx && old_regions.slot_owners.contains_key(i)
        ==> new_regions.slot_owners[i] == old_regions.slot_owners[i]
},
new_regions.slots == old_regions.slots,
new_regions.inv(),
0 < old_regions.ref_count(idx),
old_regions.ref_count(idx) + 1 <= REF_COUNT_MAX,
ensures
new_regions.inv(),
self.metaregion_sound(new_regions),

Incrementing the ref count of the current frame preserves regions.inv() and self.metaregion_sound(new_regions).

Source

pub proof fn lemma_new_child_mappings_eq_target( self, new_subtree: OwnerSubtree<C>, pa: Paddr, level: PagingLevel, prop: PageProperty, )

requires
self.inv(),
self.in_locked_range(),
level == self.level,
new_subtree.inv(),
new_subtree.value().is_frame(),
new_subtree.value().path
    == self
        .continuations[self.level - 1]
        .path()
        .push_tail(self.continuations[self.level - 1].idx as int),
new_subtree.value().frame().mapped_pa == pa,
new_subtree.value().frame().prop == prop,
ensures
PageTableOwner(new_subtree)@.mappings
    == set![
        Mapping { va_range : self @.cur_slot_range(page_size::< PagingConsts > (level)),
        pa_range : pa.. (pa + page_size::< PagingConsts > (level)) as usize, page_size :
        page_size::< PagingConsts > (level), property : prop, }
    ],

A new frame subtree at the current position has mappings equal to the singleton mapping covering the current slot range.

Source

pub open spec fn locked_range(self) -> Range<Vaddr>

{
    let size = page_size::<C>(self.guard_level) as nat;
    let start = nat_align_down(self.prefix as nat, size);
    Range {
        start: start as Vaddr,
        end: (start + size) as Vaddr,
    }
}

The guard-level slot containing the numeric prefix, with its end excluded.

Source

pub open spec fn in_locked_range(self) -> bool

{ self.locked_range().start <= self.va < self.locked_range().end }
Source

pub open spec fn above_locked_range(self) -> bool

{ self.va >= self.locked_range().end }
Source

pub proof fn lemma_prefix_in_locked_range(self)

requires
self.inv(),
!self.popped_too_high,
self.level < self.guard_level,
ensures
self.in_locked_range(),
Source

pub proof fn lemma_in_locked_range_guard_index_eq_prefix(self)

requires
self.inv(),
1 <= self.guard_level <= NR_LEVELS,
self.in_locked_range(),
ensures
pte_index_spec::<C>(self.va, (self.guard_level - 1 + 1) as PagingLevel)
    == pte_index_spec::<C>(self.prefix, (self.guard_level - 1 + 1) as PagingLevel),

The cursor and prefix select the same guard-level entry within the locked range.

Source

pub proof fn lemma_in_locked_range_level_le_nr_levels(self)

requires
self.inv(),
self.in_locked_range(),
!self.popped_too_high,
ensures
self.level <= NR_LEVELS,
Source

pub proof fn lemma_in_locked_range_top_index_lt_top_end(self)

requires
self.inv(),
self.in_locked_range(),
!self.popped_too_high,
ensures
pte_index_spec::<C>(self.va, (NR_LEVELS - 1 + 1) as PagingLevel)
    < C::TOP_LEVEL_INDEX_RANGE().end,

When the cursor is in the locked range and not popped, its top-level index is strictly less than TOP_LEVEL_INDEX_RANGE.end (the relaxed inv only allows <=, but the operational state is strict).

Source

pub proof fn lemma_in_locked_range_level_le_guard_level(self)

requires
self.inv(),
self.in_locked_range(),
!self.popped_too_high,
ensures
self.level <= self.guard_level,
Source

pub proof fn lemma_locked_range_span(self)

requires
self.inv(),
ensures
self.locked_range().start as nat
    == nat_align_down(
        self.prefix as nat,
        page_size::<PagingConsts>(self.guard_level as PagingLevel) as nat,
    ),
self.locked_range().start == self.prefix,
self.locked_range().end == self.prefix + page_size::<PagingConsts>(self.guard_level),
self.locked_range().start as nat
    % page_size::<PagingConsts>(self.guard_level as PagingLevel) as nat == 0,
self.locked_range().end - self.locked_range().start
    == page_size::<PagingConsts>(self.guard_level as PagingLevel),

The locked range spans exactly one guard-level node: end - start == page_size(guard_level).

Source

pub proof fn lemma_prefix_aligned_to_guard_level(self)

requires
self.inv(),
ensures
self.prefix as nat % page_size::<PagingConsts>(self.guard_level) as nat == 0,

The cursor’s prefix is aligned to page_size(self.guard_level), since the cursor invariant makes the prefix base-page-aligned and zeros all indices below self.guard_level.

Source

pub proof fn lemma_in_node_holds_at_top( self, self_va: Vaddr, va: Vaddr, node_size: usize, )

requires
self.inv(),
self_va == self.va,
self.guard_level == NR_LEVELS,
node_size == page_size::<PagingConsts>((NR_LEVELS + 1) as PagingLevel),
self.locked_range().start <= va < self.locked_range().end,
ensures
nat_align_down(self_va as nat, node_size as nat) <= va as nat,
(va as nat) - nat_align_down(self_va as nat, node_size as nat) < node_size as nat,

At the top guard level, the node determined by the cursor’s upper address bits contains the entire locked range, even after the cursor leaves that range.

Source

pub proof fn lemma_prefix_plus_ps_no_overflow(self)

requires
self.inv(),
ensures
self.prefix + page_size::<PagingConsts>(self.guard_level) <= usize::MAX,

prefix + page_size(guard_level) <= usize::MAX.

The prefix is aligned to a parent slot, leaving a complete fanout of slots before machine-word wrap.

Source

pub proof fn lemma_va_plus_page_size_no_overflow(self, level: PagingLevel)

requires
self.inv(),
self.in_locked_range(),
1 <= level <= self.guard_level,
ensures
self.va + page_size::<PagingConsts>(level) <= usize::MAX,

self.va + page_size(level) <= usize::MAX for any level <= self.guard_level, whenever the cursor is in the locked range.

Derived from the cursor invariant: in_locked_range says self.va < locked_range().end = prefix + page_size(guard_level) and parent-slot alignment leaves enough slack for one more configured slot, since page_size(level) <= page_size(gl).

Source

pub proof fn lemma_locked_range_page_aligned(self)

requires
self.inv(),
ensures
self.locked_range().end % PAGE_SIZE == 0,
self.locked_range().start % PAGE_SIZE == 0,
Source

pub proof fn lemma_cur_subtree_inv(self)

requires
self.inv(),
ensures
self.cur_subtree().inv(),
Source

pub proof fn lemma_cur_entry_absent_not_present(self)

requires
self.inv(),
self.in_locked_range(),
self.cur_entry_owner().is_absent(),
ensures
!self@.present(),

If the current entry is absent, !self@.present().

Source

pub proof fn lemma_cur_subtree_empty_not_present(self)

requires
self.inv(),
self.in_locked_range(),
PageTableOwner(self.cur_subtree()).view_rec(self.cur_subtree().value().path) =~= set![],
ensures
!self@.present(),

Generalises lemma_cur_entry_absent_not_present to any empty subtree.

Source

pub proof fn lemma_cur_entry_frame_present(self)

requires
self.inv(),
self.in_locked_range(),
self.cur_entry_owner().is_frame(),
ensures
self@.present(),
self@
    .query(
        self.cur_entry_owner().frame().mapped_pa,
        page_size::<PagingConsts>(self.cur_entry_owner().parent_level),
        self.cur_entry_owner().frame().prop,
    ),
Source

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

{
    forall |i: int| {
        self.level - 1 <= i < NR_LEVELS
            ==> self.continuations[i].entry_own.metaregion_sound(regions)
    }
}

The entry_own at each continuation level satisfies metaregion_sound.

Source

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

{
    &&& self
        .map_full_tree(|entry_owner: EntryOwner<C>, path: TreePath<NR_ENTRIES>| {
            entry_owner.metaregion_sound(regions)
        })
    &&& self.path_metaregion_sound(regions)

}
Source

pub proof fn lemma_metaregion_preserved( self, other: Self, regions0: MetaRegionOwners, regions1: MetaRegionOwners, )

requires
self.inv(),
self.metaregion_sound(regions0),
self.level == other.level,
self.continuations =~= other.continuations,
OwnerSubtree::implies(
    PageTableOwner::<C>::metaregion_sound_pred(regions0),
    PageTableOwner::<C>::metaregion_sound_pred(regions1),
),
ensures
other.metaregion_sound(regions1),
Source

pub proof fn lemma_metaregion_slot_owners_preserved( self, regions0: MetaRegionOwners, regions1: MetaRegionOwners, )

requires
self.inv(),
self.metaregion_sound(regions0),
regions0.slot_owners =~= regions1.slot_owners,
forall |k: int| {
    regions0.slots.contains_key(k) ==> #[trigger] regions1.slots.contains_key(k)
},
forall |k: int| {
    regions0.slots.contains_key(k) ==> regions0.slots[k] == #[trigger] regions1.slots[k]
},
ensures
self.metaregion_sound(regions1),

Transfers metaregion_sound when slot_owners is preserved.

Source

pub proof fn lemma_metaregion_slot_owners_rc_increment( self, regions0: MetaRegionOwners, regions1: MetaRegionOwners, idx: int, )

requires
self.inv(),
self.metaregion_sound(regions0),
regions0.inv(),
regions1.slots == regions0.slots,
regions1.slot_owners.dom() == regions0.slot_owners.dom(),
regions1.ref_count(idx) == regions0.ref_count(idx) + 1,
regions1.slot_owners[idx].ref_count_perm.id()
    == regions0.slot_owners[idx].ref_count_perm.id(),
regions1.slot_owners[idx].metadata_perm.id()
    == regions0.slot_owners[idx].metadata_perm.id(),
regions1.slot_owners[idx].metadata_perm.frac() + 1
    == regions0.slot_owners[idx].metadata_perm.frac(),
regions1.slot_owners[idx].in_list_perm == regions0.slot_owners[idx].in_list_perm,
regions1.slot_owners[idx].paths_in_pt == regions0.slot_owners[idx].paths_in_pt,
regions1.slot_owners[idx].slot_vaddr == regions0.slot_owners[idx].slot_vaddr,
regions1.slot_owners[idx].usage == regions0.slot_owners[idx].usage,
regions1.ref_count(idx) != REF_COUNT_UNUSED,
regions1.ref_count(idx) <= REF_COUNT_MAX,
regions1.inv(),
forall |i: int| {
    i != idx && regions0.slot_owners.contains_key(i)
        ==> regions1.slot_owners[i] == regions0.slot_owners[i]
},
ensures
self.metaregion_sound(regions1),
Source

pub proof fn lemma_cont_entry_metaregion_at(self, regions: MetaRegionOwners, i: int)

requires
self.inv(),
self.metaregion_sound(regions),
self.level - 1 <= i < NR_LEVELS,
ensures
self.continuations[i].entry_own.metaregion_sound(regions),

The continuation entry at i satisfies metaregion_sound.

Source

pub open spec fn new( owner_subtree: OwnerSubtree<C>, idx: usize, guard: PageTableGuard<'rcu, C>, ) -> Self

{
    let va = (C::LEADING_BITS_spec() as int
        * pow2(page_table_vaddr_bits_spec::<C>() as nat)
        + idx * pow2(pte_index_bit_offset_spec::<C>(C::NR_LEVELS()) as nat)) as Vaddr;
    Self {
        level: C::NR_LEVELS(),
        continuations: Map::empty()
            .insert(
                C::NR_LEVELS() - 1,
                CursorContinuation::new(owner_subtree, idx, guard),
            ),
        va,
        guard_level: C::NR_LEVELS(),
        prefix: va,
        popped_too_high: false,
    }
}
Source

pub proof fn tracked_new( tracked owner_subtree: OwnerSubtree<C>, idx: usize, guard: PageTableGuard<'rcu, C>, ) -> tracked Self

returns
Self::new(owner_subtree, idx, guard),
Source

pub broadcast group fn group_lemmas()

broadcast group
Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub proof fn view_non_overlapping(self)

requires
self.inv(),
ensures
self@.non_overlapping(),

The cursor’s view has non-overlapping mappings. This follows from the tree structure alone: as_page_table_owner_preserves_view_mappings collapses the union-over-continuations view into a single root-rooted view_rec, after which view_rec_disjoint_vaddrs gives pairwise disjointness directly.

Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub proof fn split_while_huge_node_noop(self)

requires
self.inv(),
self.in_locked_range(),
self.cur_entry_owner().is_node(),
self.level > 1,
ensures
self@.split_while_huge(page_size::<PagingConsts>((self.level - 1) as PagingLevel))
    == self@,
Source

pub proof fn split_while_huge_absent_noop(self, size: usize)

requires
self.inv(),
self.in_locked_range(),
self.cur_entry_owner().is_absent(),
ensures
self@.split_while_huge(size) == self@,

When the current entry is absent, there is no mapping at cur_va in the abstract view, so split_while_huge finds nothing to split and is a no-op for any target size.

Source

pub proof fn split_while_huge_at_level_noop(self)

requires
self.inv(),
self.in_locked_range(),
ensures
self@.split_while_huge(page_size::<PagingConsts>(self.level as PagingLevel)) == self@,
Source

pub proof fn find_next_split_push_equals_split_while_huge( self, old_view: CursorView<C>, )

requires
self.inv(),
old_view.inv(),
self.cur_entry_owner().is_frame(),
self@.cur_va == old_view.cur_va,
old_view.present(),
old_view.query_mapping().page_size > page_size::<PagingConsts>(self.level as PagingLevel),
old_view.query_mapping().page_size / NR_ENTRIES
    == page_size::<PagingConsts>(self.level as PagingLevel),
old_view.query_mapping().page_size % page_size::<PagingConsts>(self.level as PagingLevel)
    == 0,
self@.mappings
    =~= old_view
        .split_if_mapped_huge_spec(page_size::<PagingConsts>(self.level as PagingLevel))
        .mappings,
ensures
self@.mappings
    == old_view
        .split_while_huge(page_size::<PagingConsts>(self.level as PagingLevel))
        .mappings,

After split_if_mapped_huge + push_level, the mappings equal old_view.split_while_huge(page_size(current_level)).

Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub proof fn map_children_implies( self, f: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, g: FnSpec<(EntryOwner<C>, TreePath<NR_ENTRIES>), bool>, )

requires
self.inv(),
OwnerSubtree::implies(f, g),
forall |i: int| self.level - 1 <= i < NR_LEVELS ==> self.continuations[i].map_children(f),
ensures
forall |i: int| self.level - 1 <= i < NR_LEVELS ==> self.continuations[i].map_children(g),
Source

pub proof fn cur_entry_node_implies_level_gt_1(self)

requires
self.inv(),
self.cur_entry_owner().is_node(),
ensures
self.level > 1,
Source

pub proof fn frame_not_fits_implies_level_gt_1( self, cur_entry_fits_range: bool, cur_va: Vaddr, end: Vaddr, )

requires
self.inv(),
self.cur_entry_owner().is_frame(),
!cur_entry_fits_range,
cur_va < end,
cur_va == self.cur_va(),
cur_entry_fits_range
    == (cur_va == self.cur_va_range().start && self.cur_va_range().end <= end),
cur_va as nat % PAGE_SIZE as nat == 0,
end as nat % PAGE_SIZE as nat == 0,
ensures
self.level > 1,

A frame entry at the cursor’s current level that doesn’t fit the aligned range [cur_va, end) must be at level > 1. Justification: At level 1, page_size(1) == BASE_PAGE_SIZE. Since the cursor VA and end are BASE_PAGE_SIZE-aligned and cur_va < end, we have cur_va + page_size(1) <= end, so a level-1 frame always fits. Therefore !cur_entry_fits_range implies level > 1.

Source§

impl<'rcu, C: PageTableConfig> CursorOwner<'rcu, C>

Source

pub open spec fn zero_below_level(self) -> Self

recommends
1 <= self.level <= C::NR_LEVELS(),
{
    Self {
        va: nat_align_down(self.va as nat, page_size::<C>(self.level) as nat) as Vaddr,
        ..self
    }
}
Source

pub open spec fn cur_va(self) -> Vaddr

{ self.va }
Source

pub open spec fn prefix_vaddr(self) -> Vaddr

{ self.prefix }
Source

pub open spec fn cur_va_range(self) -> Range<Vaddr>

{
    let size = page_size::<PagingConsts>(self.level);
    let start = nat_align_down(self.cur_va() as nat, size as nat) as Vaddr;
    Range {
        start,
        end: (start + size) as Vaddr,
    }
}
Source

pub open spec fn set_va_in_node(self, new_va: Vaddr) -> Self

{
    let old_cont = self.continuations[self.level - 1];
    Self {
        va: new_va,
        continuations: self
            .continuations
            .insert(
                self.level - 1,
                CursorContinuation {
                    idx: pte_index_spec::<C>(new_va, self.level),
                    ..old_cont
                },
            ),
        popped_too_high: false,
        ..self
    }
}
Source

pub proof fn do_zero_below_level(tracked &mut self)

requires
old(self).inv(),
old(self).level <= old(self).guard_level,
ensures
*final(self) == old(self).zero_below_level(),
final(self).inv(),
Source

pub proof fn zero_preserves_all_but_va(self)

ensures
self.zero_below_level().level == self.level,
self.zero_below_level().continuations == self.continuations,
self.zero_below_level().guard_level == self.guard_level,
self.zero_below_level().prefix == self.prefix,
self.zero_below_level().popped_too_high == self.popped_too_high,
Source

pub proof fn lemma_inc_index_va(self)

requires
self.inv(),
self.in_locked_range(),
self.index() + 1 < NR_ENTRIES,
ensures
self.inc_index().va == self.va + page_size::<C>(self.level),

Incrementing the selected nonterminal entry advances by one slot without overflow.

Source

pub proof fn inc_and_zero_increases_va(self)

requires
self.inv(),
self.in_locked_range(),
self.index() + 1 < NR_ENTRIES,
ensures
self.inc_index().zero_below_level().va > self.va,
self.inc_index().zero_below_level().va
    == self@.align_up_spec(page_size::<PagingConsts>(self.level)),

Incrementing a nonterminal index and aligning down reaches the next slot boundary.

Source

pub proof fn cur_va_in_subtree_range(self)

requires
self.inv(),
self.in_locked_range(),
ensures
vaddr_of::<C>(self.cur_subtree().value().path) <= self.cur_va()
    < vaddr_of::<C>(self.cur_subtree().value().path)
        + page_size::<PagingConsts>(self.level),
vaddr_of::<C>(self.cur_subtree().value().path)
    == nat_align_down(self.cur_va() as nat, page_size::<PagingConsts>(self.level) as nat),

The current subtree starts at the cursor’s aligned slot boundary and contains its VA.

Source

pub proof fn lemma_locked_range_vaddr_prefix_match(self, new_va: Vaddr)

requires
self.inv(),
new_va % C::BASE_PAGE_SIZE() == 0,
vaddr_upper_bits_spec::<C>(new_va) == vaddr_upper_bits_spec::<C>(self.prefix_vaddr()),
self.locked_range().start <= new_va < self.locked_range().end,
ensures
pte_index_spec::<C>(new_va, self.guard_level)
    == pte_index_spec::<C>(self.prefix, self.guard_level),
forall |i: int| {
    self.guard_level - 1 <= i < C::NR_LEVELS()
        ==> (#[trigger] pte_index_spec::<C>(new_va, (i + 1) as PagingLevel))
            == pte_index_spec::<C>(self.prefix_vaddr(), (i + 1) as PagingLevel)
},

Addresses in the locked block share the guard-level and higher indices.

Source

pub proof fn lemma_cur_pte_index(self)

requires
self.inv(),
self.in_locked_range(),
ensures
1 <= self.level <= C::NR_LEVELS(),
pte_index_spec::<C>(self.cur_va(), self.level) == self.continuations[self.level - 1].idx,
pte_index_spec::<C>(self.cur_va(), self.level) < NR_ENTRIES,

The entry selected by the cursor’s concrete VA is the entry owned by its current continuation. This is the architecture-parameterized replacement for exposing the decomposed address stored in CursorOwner.

Source

pub proof fn tracked_set_vaddr_in_node(tracked &mut self, new_va: Vaddr)

requires
old(self).inv(),
new_va % C::BASE_PAGE_SIZE() == 0,
vaddr_upper_bits_spec::<C>(new_va) == vaddr_upper_bits_spec::<C>(old(self).cur_va()),
forall |i: int| {
    old(self).level <= i < C::NR_LEVELS()
        ==> (#[trigger] pte_index_spec::<C>(new_va, (i + 1) as PagingLevel))
            == pte_index_spec::<C>(old(self).cur_va(), (i + 1) as PagingLevel)
},
old(self).locked_range().start <= new_va < old(self).locked_range().end,
old(self).level <= old(self).guard_level,
ensures
*final(self) == old(self).set_va_in_node(new_va),
final(self).inv(),

Architecture-parameterized entry point for repositioning a cursor inside its current page-table node.

Trait Implementations§

Source§

impl<'rcu, C: PageTableConfig> Inv for CursorOwner<'rcu, C>

Source§

open spec fn inv(self) -> bool

{
    &&& self.va % C::BASE_PAGE_SIZE() == 0
    &&& 1 <= self.level <= NR_LEVELS
    &&& 1 <= self.guard_level <= NR_LEVELS
    &&& C::TOP_LEVEL_INDEX_RANGE().start
        <= pte_index_spec::<C>(self.va, (NR_LEVELS - 1 + 1) as PagingLevel)
    &&& pte_index_spec::<C>(self.va, (NR_LEVELS - 1 + 1) as PagingLevel)
        <= C::TOP_LEVEL_INDEX_RANGE().end
    &&& self.in_locked_range() || self.above_locked_range()
    &&& self.popped_too_high ==> self.level >= self.guard_level
    &&& !self.popped_too_high
        ==> self.level <= self.guard_level || self.above_locked_range()
    &&& self.continuations[self.level - 1].all_some()
    &&& forall |i: int| {
        self.level <= i < NR_LEVELS
            ==> { (#[trigger] self.continuations[i]).all_but_index_some() }
    }
    &&& self.level <= NR_LEVELS - 1
        ==> {
            &&& C::TOP_LEVEL_INDEX_RANGE().start <= self.continuations[NR_LEVELS - 1].idx
            &&& self.continuations[NR_LEVELS - 1].idx < C::TOP_LEVEL_INDEX_RANGE().end

        }
    &&& forall |j: int| {
        0 <= j < NR_ENTRIES
            && !(C::TOP_LEVEL_INDEX_RANGE().start <= j < C::TOP_LEVEL_INDEX_RANGE().end)
            ==> (self.continuations[NR_LEVELS - 1].children[j] is Some
                ==> (self
                    .continuations[NR_LEVELS - 1]
                    .children[j]
                    .unwrap()
                    .value()
                    .is_borrowed()
                    || self
                        .continuations[NR_LEVELS - 1]
                        .children[j]
                        .unwrap()
                        .value()
                        .is_absent()))
    }
    &&& self.prefix % C::BASE_PAGE_SIZE() == 0
    &&& forall |i: int| {
        1 <= i <= self.guard_level
            ==> #[trigger] pte_index_spec::<C>(self.prefix, i as PagingLevel) == 0
    }
    &&& pte_index_spec::<C>(self.prefix, (NR_LEVELS - 1 + 1) as PagingLevel)
        >= C::TOP_LEVEL_INDEX_RANGE().start
    &&& pte_index_spec::<C>(self.prefix, (NR_LEVELS - 1 + 1) as PagingLevel)
        < C::TOP_LEVEL_INDEX_RANGE().end
    &&& pte_index_spec::<C>(self.prefix, (NR_LEVELS - 1 + 1) as PagingLevel) + 1
        < NR_ENTRIES
    &&& self.locked_range().end <= vaddr_range_spec::<C>().end + 1
    &&& self.locked_range().end <= C::LOCKED_END_BOUND_spec()
    &&& vaddr_upper_bits_spec::<C>(self.va) == vaddr_upper_bits_spec::<C>(self.prefix)
    &&& vaddr_upper_bits_spec::<C>(self.prefix) == C::LEADING_BITS_spec()
    &&& self.level <= self.guard_level
        ==> forall |i: int| {
            self.guard_level <= i < NR_LEVELS
                ==> self.continuations[i].idx
                    == pte_index_spec::<C>(self.prefix, (i + 1) as PagingLevel)
        }
    &&& !self.popped_too_high
        && (self.in_locked_range() || self.level < self.guard_level)
        ==> forall |i: int| {
            self.guard_level <= i < NR_LEVELS
                ==> #[trigger] pte_index_spec::<C>(self.va, (i + 1) as PagingLevel)
                    == pte_index_spec::<C>(self.prefix, (i + 1) as PagingLevel)
        }
    &&& !self.popped_too_high && self.guard_level >= 1 && self.level < self.guard_level
        ==> pte_index_spec::<C>(self.va, (self.guard_level - 1 + 1) as PagingLevel)
            == pte_index_spec::<
                C,
            >(self.prefix, (self.guard_level - 1 + 1) as PagingLevel)
    &&& self.level <= 4
        ==> {
            &&& self.continuations.contains_key(3)
            &&& self.continuations[3].inv()
            &&& self.continuations[3].level() == 4
            &&& self.continuations[3].entry_own.parent_level == 5
            &&& self.in_locked_range()
                ==> pte_index_spec::<C>(self.va, (3 + 1) as PagingLevel)
                    == self.continuations[3].idx

        }
    &&& self.level <= 3
        ==> {
            &&& self.continuations.contains_key(2)
            &&& self.continuations[2].inv()
            &&& self.continuations[2].level() == 3
            &&& self.continuations[2].entry_own.parent_level == 4
            &&& self.in_locked_range()
                ==> pte_index_spec::<C>(self.va, (2 + 1) as PagingLevel)
                    == self.continuations[2].idx
            &&& self.continuations[2].guard.inner.inner@.ptr.addr()
                != self.continuations[3].guard.inner.inner@.ptr.addr()
            &&& self.continuations[2].path()
                == self
                    .continuations[3]
                    .path()
                    .push_tail(self.continuations[3].idx as int)
            &&& self.continuations[2].entry_own.path.len()
                == self.continuations[3].entry_own.node().tree_level + 1
            &&& self
                .continuations[2]
                .entry_own
                .match_pte(
                    self
                        .continuations[3]
                        .entry_own
                        .node()
                        .children_perm
                        .value()[self.continuations[3].idx as int],
                    self.continuations[3].entry_own.node().level(),
                )
            &&& self.continuations[2].entry_own.parent_level
                == self.continuations[3].entry_own.node().level()

        }
    &&& self.level <= 2
        ==> {
            &&& self.continuations.contains_key(1)
            &&& self.continuations[1].inv()
            &&& self.continuations[1].level() == 2
            &&& self.continuations[1].entry_own.parent_level == 3
            &&& self.in_locked_range()
                ==> pte_index_spec::<C>(self.va, (1 + 1) as PagingLevel)
                    == self.continuations[1].idx
            &&& self.continuations[1].guard.inner.inner@.ptr.addr()
                != self.continuations[2].guard.inner.inner@.ptr.addr()
            &&& self.continuations[1].guard.inner.inner@.ptr.addr()
                != self.continuations[3].guard.inner.inner@.ptr.addr()
            &&& self.continuations[1].path()
                == self
                    .continuations[2]
                    .path()
                    .push_tail(self.continuations[2].idx as int)
            &&& self.continuations[1].entry_own.path.len()
                == self.continuations[2].entry_own.node().tree_level + 1
            &&& self
                .continuations[1]
                .entry_own
                .match_pte(
                    self
                        .continuations[2]
                        .entry_own
                        .node()
                        .children_perm
                        .value()[self.continuations[2].idx as int],
                    self.continuations[2].entry_own.node().level(),
                )
            &&& self.continuations[1].entry_own.parent_level
                == self.continuations[2].entry_own.node().level()

        }
    &&& self.level == 1
        ==> {
            &&& self.continuations.contains_key(0)
            &&& self.continuations[0].inv()
            &&& self.continuations[0].level() == 1
            &&& self.continuations[0].entry_own.parent_level == 2
            &&& self.in_locked_range()
                ==> pte_index_spec::<C>(self.va, (0 + 1) as PagingLevel)
                    == self.continuations[0].idx
            &&& self.continuations[0].guard.inner.inner@.ptr.addr()
                != self.continuations[1].guard.inner.inner@.ptr.addr()
            &&& self.continuations[0].guard.inner.inner@.ptr.addr()
                != self.continuations[2].guard.inner.inner@.ptr.addr()
            &&& self.continuations[0].guard.inner.inner@.ptr.addr()
                != self.continuations[3].guard.inner.inner@.ptr.addr()
            &&& self.continuations[0].path()
                == self
                    .continuations[1]
                    .path()
                    .push_tail(self.continuations[1].idx as int)
            &&& self.continuations[0].entry_own.path.len()
                == self.continuations[1].entry_own.node().tree_level + 1
            &&& self
                .continuations[0]
                .entry_own
                .match_pte(
                    self
                        .continuations[1]
                        .entry_own
                        .node()
                        .children_perm
                        .value()[self.continuations[1].idx as int],
                    self.continuations[1].entry_own.node().level(),
                )
            &&& self.continuations[0].entry_own.parent_level
                == self.continuations[1].entry_own.node().level()

        }

}
Source§

impl<'rcu, C: PageTableConfig> InvView for CursorOwner<'rcu, C>

Source§

proof fn view_preserves_inv(self)

Source§

impl<'rcu, C: PageTableConfig> View for CursorOwner<'rcu, C>

Source§

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

{
    CursorView {
        cur_va: self.cur_va(),
        mappings: self.view_mappings(),
        phantom: PhantomData,
    }
}
Source§

type V = CursorView<C>

Auto Trait Implementations§

§

impl<'rcu, C> !RefUnwindSafe for CursorOwner<'rcu, C>

§

impl<'rcu, C> !UnwindSafe for CursorOwner<'rcu, C>

§

impl<'rcu, C> Freeze for CursorOwner<'rcu, C>

§

impl<'rcu, C> Send for CursorOwner<'rcu, C>
where <C as PageTableConfig>::Perm: Send,

§

impl<'rcu, C> Sync for CursorOwner<'rcu, C>
where <C as PageTableConfig>::Perm: Sync,

§

impl<'rcu, C> Unpin for CursorOwner<'rcu, C>
where <C as PageTableConfig>::Perm: Unpin, <C as PageTableConfig>::E: Unpin, C: Unpin,

§

impl<'rcu, C> UnsafeUnpin for CursorOwner<'rcu, C>

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
§

impl<T> Conv for T

§

fn conv<T>(self) -> T
where Self: Into<T>,

Converts self into T using Into<T>. Read more
§

impl<T> FmtForward for T

§

fn fmt_binary(self) -> FmtBinary<Self>
where Self: Binary,

Causes self to use its Binary implementation when Debug-formatted.
§

fn fmt_display(self) -> FmtDisplay<Self>
where Self: Display,

Causes self to use its Display implementation when Debug-formatted.
§

fn fmt_lower_exp(self) -> FmtLowerExp<Self>
where Self: LowerExp,

Causes self to use its LowerExp implementation when Debug-formatted.
§

fn fmt_lower_hex(self) -> FmtLowerHex<Self>
where Self: LowerHex,

Causes self to use its LowerHex implementation when Debug-formatted.
§

fn fmt_octal(self) -> FmtOctal<Self>
where Self: Octal,

Causes self to use its Octal implementation when Debug-formatted.
§

fn fmt_pointer(self) -> FmtPointer<Self>
where Self: Pointer,

Causes self to use its Pointer implementation when Debug-formatted.
§

fn fmt_upper_exp(self) -> FmtUpperExp<Self>
where Self: UpperExp,

Causes self to use its UpperExp implementation when Debug-formatted.
§

fn fmt_upper_hex(self) -> FmtUpperHex<Self>
where Self: UpperHex,

Causes self to use its UpperHex implementation when Debug-formatted.
§

fn fmt_list(self) -> FmtList<Self>
where &'a Self: for<'a> IntoIterator,

Formats each item in a sequence. 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

§

impl<T> FromSpecImpl<T> for T

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> T

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

§

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

§

fn pipe<R>(self, func: impl FnOnce(Self) -> R) -> R
where Self: Sized,

Pipes by value. This is generally the method you want to use. Read more
§

fn pipe_ref<'a, R>(&'a self, func: impl FnOnce(&'a Self) -> R) -> R
where R: 'a,

Borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_ref_mut<'a, R>(&'a mut self, func: impl FnOnce(&'a mut Self) -> R) -> R
where R: 'a,

Mutably borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_borrow<'a, B, R>(&'a self, func: impl FnOnce(&'a B) -> R) -> R
where Self: Borrow<B>, B: 'a + ?Sized, R: 'a,

Borrows self, then passes self.borrow() into the pipe function. Read more
§

fn pipe_borrow_mut<'a, B, R>( &'a mut self, func: impl FnOnce(&'a mut B) -> R, ) -> R
where Self: BorrowMut<B>, B: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.borrow_mut() into the pipe function. Read more
§

fn pipe_as_ref<'a, U, R>(&'a self, func: impl FnOnce(&'a U) -> R) -> R
where Self: AsRef<U>, U: 'a + ?Sized, R: 'a,

Borrows self, then passes self.as_ref() into the pipe function.
§

fn pipe_as_mut<'a, U, R>(&'a mut self, func: impl FnOnce(&'a mut U) -> R) -> R
where Self: AsMut<U>, U: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.as_mut() into the pipe function.
§

fn pipe_deref<'a, T, R>(&'a self, func: impl FnOnce(&'a T) -> R) -> R
where Self: Deref<Target = T>, T: 'a + ?Sized, R: 'a,

Borrows self, then passes self.deref() into the pipe function.
§

fn pipe_deref_mut<'a, T, R>( &'a mut self, func: impl FnOnce(&'a mut T) -> R, ) -> R
where Self: DerefMut<Target = T> + Deref, T: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.deref_mut() into the pipe function.
§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A

§

impl<T> Tap for T

§

fn tap(self, func: impl FnOnce(&Self)) -> Self

Immutable access to a value. Read more
§

fn tap_mut(self, func: impl FnOnce(&mut Self)) -> Self

Mutable access to a value. Read more
§

fn tap_borrow<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Immutable access to the Borrow<B> of a value. Read more
§

fn tap_borrow_mut<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Mutable access to the BorrowMut<B> of a value. Read more
§

fn tap_ref<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Immutable access to the AsRef<R> view of a value. Read more
§

fn tap_ref_mut<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Mutable access to the AsMut<R> view of a value. Read more
§

fn tap_deref<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Immutable access to the Deref::Target of a value. Read more
§

fn tap_deref_mut<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Mutable access to the Deref::Target of a value. Read more
§

fn tap_dbg(self, func: impl FnOnce(&Self)) -> Self

Calls .tap() only in debug builds, and is erased in release builds.
§

fn tap_mut_dbg(self, func: impl FnOnce(&mut Self)) -> Self

Calls .tap_mut() only in debug builds, and is erased in release builds.
§

fn tap_borrow_dbg<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Calls .tap_borrow() only in debug builds, and is erased in release builds.
§

fn tap_borrow_mut_dbg<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Calls .tap_borrow_mut() only in debug builds, and is erased in release builds.
§

fn tap_ref_dbg<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Calls .tap_ref() only in debug builds, and is erased in release builds.
§

fn tap_ref_mut_dbg<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Calls .tap_ref_mut() only in debug builds, and is erased in release builds.
§

fn tap_deref_dbg<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Calls .tap_deref() only in debug builds, and is erased in release builds.
§

fn tap_deref_mut_dbg<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Calls .tap_deref_mut() only in debug builds, and is erased in release builds.
§

impl<T> TryConv for T

§

fn try_conv<T>(self) -> Result<T, Self::Error>
where Self: TryInto<T>,

Attempts to convert self into T using TryInto<T>. Read more
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>