Skip to content

fix: Frame::meta #765

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rikosellic merged 4 commits into from
Sep 14, 2026
Merged

fix: Frame::meta #765

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
be4a493
fix: `Frame::meta`
rikosellic Sep 14, 2026
716f23b
fix `PageTableNode::level`
rikosellic Sep 14, 2026
ae2b970
fix `PageTableNode::nr_children`
rikosellic Sep 14, 2026
3bcdfd1
fix: `Entry::is_node`
rikosellic Sep 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 14 additions & 1 deletion ostd/specs/mm/frame/frame_specs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use crate::specs::{
arch::*,
mm::frame::{
mapping::{frame_to_index, meta_to_index},
meta_owners::{FracMetadataPerm, MetadataPerm, PageUsage},
meta_owners::{FracMetadataPerm, MetaSlotStorage, MetadataPerm, PageUsage, typed_meta_wf},
meta_region_owners::MetaRegionOwners,
},
};
Expand Down Expand Up @@ -80,6 +80,19 @@ impl<M: ?Sized> Frame<M> {
}
}

impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M> {
/// Relates an externally stored metadata permission to this frame's slot permission.
pub open spec fn external_meta_wf(
self,
metadata_perm: MetadataPerm,
repr_perm: M::ReprPerm,
) -> bool {
&&& self.ptr_inv()
&&& self.tracked_metadata_perm@ is None
&&& typed_meta_wf::<M>(self.slot_perm(), metadata_perm, repr_perm)
}
}

impl<M: ?Sized> Inv for Frame<M> {
open spec fn inv(self) -> bool {
&&& self.ptr_inv()
Expand Down
1 change: 1 addition & 0 deletions ostd/specs/mm/page_table/node/child.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ impl<'a, C: PageTableConfig> OwnerOf for ChildRef<'a, C> {
&&& owner.is_node()
&&& node.inner@.ptr.addr() == owner.node().meta_vaddr()
&&& node.inner@.ptr_inv()
&&& node.inner@.external_meta_wf(owner.node().frame_permission.resource(), ())
},
Self::Frame(paddr, level, prop) => {
&&& owner.is_frame()
Expand Down
3 changes: 1 addition & 2 deletions ostd/specs/mm/page_table/node/entry.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
) -> bool {
&&& parent_owner.level == owner.parent_level
&&& parent_owner.inv()
&&& guard.inner.inner@.ptr.addr() == parent_owner.meta_vaddr()
&&& guard.inner.inner@.wf(parent_owner)
&&& parent_owner.relate_guard(guard)
&&& owner.match_pte(parent_owner.children_perm.value()[self.idx as int], owner.parent_level)
}

Expand Down
12 changes: 6 additions & 6 deletions ostd/specs/mm/page_table/node/owners.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -285,7 +285,7 @@ impl<C: PageTableConfig> NodeOwner<C> {
)
}

pub open spec fn meta_value(self, regions: MetaRegionOwners) -> PageTablePageMeta<C> {
pub open spec fn meta_value(self) -> PageTablePageMeta<C> {
typed_meta_value::<PageTablePageMeta<C>>(self.frame_permission.resource(), ())
}

Expand All @@ -297,11 +297,10 @@ impl<C: PageTableConfig> NodeOwner<C> {
&&& regions.contains(idx)
&&& self.frame_permission.id() == regions.slot_owners[idx].metadata_perm.id()
&&& self.meta_wf(regions)
&&& self.meta_value(regions).wf(self.meta_own)
&&& self.level == self.meta_value(regions).level
&&& self.meta_own.nr_children.id() == self.meta_value(
regions,
).nr_children.id()
&&& self.meta_value().wf(self.meta_own)
&&& self.level == self.meta_value().level
&&& self.meta_own.nr_children.id()
== self.meta_value().nr_children.id()
// A page-table node's slot is tracked with `PageTable` usage (set at
// allocation via `get_node_from_unused_spec`). This discriminates node
// slots from data-frame slots (`Frame`/MMIO) by `usage` alone, so a
Expand Down Expand Up @@ -362,6 +361,7 @@ impl<'rcu, C: PageTableConfig> NodeOwner<C> {
pub open spec fn relate_guard(self, guard: PageTableGuard<'rcu, C>) -> bool {
&&& guard.inner.inner@.ptr.addr() == self.meta_vaddr()
&&& guard.inner.inner@.wf(self)
&&& guard.inner.inner@.external_meta_wf(self.frame_permission.resource(), ())
}
}

Expand Down
3 changes: 3 additions & 0 deletions ostd/src/mm/frame/frame_ref.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,9 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage>> FrameRef<'_, M> {
ensures
r.inner@.ptr.addr() == frame_to_meta(raw),
r.inner@.ptr_inv(),
r.inner@.tracked_slot_perm@ == slot_perm,
r.inner@.tracked_metadata_perm@ is None,
MetaSlot::perms_related(r.inner@.slot_perm(), metadata_perm.resource()),
)]
pub(in crate::mm) unsafe fn borrow_paddr(raw: Paddr) -> Self {
let frame = Frame::<M> {
Expand Down
37 changes: 28 additions & 9 deletions ostd/src/mm/frame/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -258,24 +258,40 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + OwnerOf> Frame<M> {
/// - By requiring the caller to provide a typed permission, we ensure that the metadata is of type `M`.
/// While a non-verified caller cannot be trusted to obey this interface, all functions that return a `Frame<M>` also
/// return an appropriate permission.
#[verus_spec(
#[verus_spec(ret =>
with
Tracked(points_to): Tracked<&'a vstd::simple_pptr::PointsTo<MetaSlot>>,
Tracked(metadata_perms): Tracked<&'a MetadataPerm>,
Tracked(metadata_perm): Tracked<Option<&'a MetadataPerm>>,
Tracked(repr_perm): Tracked<&'a M::ReprPerm>,
requires
self.ptr == points_to.pptr(),
typed_meta_wf::<M>(*points_to, *metadata_perms, *repr_perm),
returns
typed_meta_value::<M>(*metadata_perms, *repr_perm),
self.ptr_inv(),
{
self.inv() && metadata_perm is None
&& typed_meta_wf::<M>(self.slot_perm(), self.metadata_perm(), *repr_perm) ||
metadata_perm is Some
&& self.external_meta_wf(*metadata_perm->0, *repr_perm)
},
ensures
{
let metadata_perm = if metadata_perm is Some {*metadata_perm -> 0} else
{ self.metadata_perm() };
ret == typed_meta_value::<M>(metadata_perm, *repr_perm)
},
)]
pub fn meta<'a>(&'a self) -> &'a M {
// SAFETY: The type is tracked by the typed storage permission.
// unsafe { &*self.slot().as_meta_ptr::<M>() }
proof_decl! {
let tracked slot_perm = self.tracked_slot_perm.borrow();
let tracked metadata_perm = if metadata_perm is Some {
metadata_perm.tracked_borrow()
} else {
self.tracked_metadata_perm.tracked_borrow().tracked_borrow()
};
}
borrow_meta(
ReprPtr::<MetaSlotStorage, M>::from_pptr(PPtr::from_addr(self.ptr.addr())),
Tracked(points_to),
Tracked(metadata_perms),
Tracked(slot_perm),
Tracked(metadata_perm),
Tracked(repr_perm),
)
}
Expand Down Expand Up @@ -473,6 +489,9 @@ impl<M: AnyFrameMeta + Repr<MetaSlotStorage> + ?Sized> Frame<M> {
ensures
res.inner@.ptr.addr() == self.ptr.addr(),
res.inner@.ptr_inv(),
res.inner@.tracked_slot_perm@ == regions.slots[self.index()],
res.inner@.tracked_metadata_perm@ is None,
MetaSlot::perms_related(res.inner@.slot_perm(), frame_permission.resource()),
)]
pub(in crate::mm) fn borrow_with_permission<'a>(&self) -> FrameRef<'a, M> {
unsafe {
Expand Down
6 changes: 1 addition & 5 deletions ostd/src/mm/page_table/cursor/locking.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,7 @@ pub fn lock_range<'rcu, C: PageTableConfig, A: InAtomicMode>(
assert(regions.contains(cont_slot_idx));
}
let tracked cont_node_owner = cont.entry_own.tracked_borrow_node();
#[verus_spec(with Tracked(cont_node_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(cont_node_owner))]
let guard_level = subtree_root.level();
proof {
cursor_own.guard_level = guard_level;
Expand Down Expand Up @@ -396,9 +396,7 @@ fn try_traverse_and_lock_subtree_root<'rcu, C: PageTableConfig, A: InAtomicMode>

let tracked mut cont = cursor_own.continuations.tracked_remove(cursor_own.level - 1);
let tracked node_owner = cont.entry_own.tracked_borrow_node();
let tracked meta_points_to = regions.slots.tracked_borrow(node_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(node_owner.tracked_borrow_metadata_perm()),
Tracked(&()),
Ghost(node_owner.meta_own.stray.id())
Expand Down Expand Up @@ -483,9 +481,7 @@ fn try_traverse_and_lock_subtree_root<'rcu, C: PageTableConfig, A: InAtomicMode>

let tracked mut cont = cursor_own.continuations.tracked_remove(cursor_own.level - 1);
let tracked node_owner = cont.entry_own.tracked_borrow_node();
let tracked meta_points_to = regions.slots.tracked_borrow(node_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(node_owner.tracked_borrow_metadata_perm()),
Tracked(&()),
Ghost(node_owner.meta_own.stray.id())
Expand Down
4 changes: 3 additions & 1 deletion ostd/src/mm/page_table/cursor/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -597,6 +597,8 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
EntryOwner::<C>::axiom_frame_is_tracked_iff_not_mmio(
owner_before_permission_take.cur_entry_owner(),
);
assert(regions.contains(idx));
assert(old(regions).contains(idx));
}
owner_before_permission_take.lemma_cur_frame_clone_requires(
item,
Expand Down Expand Up @@ -1025,7 +1027,7 @@ impl<'rcu, C: PageTableConfig, A: InAtomicMode> Cursor<'rcu, C, A> {
pt.make_guard_unchecked(rcu_guard)
};

#[verus_spec(with Tracked(&mut child_node_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&mut child_node_owner))]
let nr_children = pt_guard.nr_children();

// `nr_children()` requires `child_node_owner.metaregion_sound_node`,
Expand Down
32 changes: 8 additions & 24 deletions ostd/src/mm/page_table/node/entry.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,21 +119,19 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
#[verus_spec(
with Tracked(owner): Tracked<EntryOwner<C>>,
Tracked(parent_owner): Tracked<&NodeOwner<C>>,
Tracked(regions): Tracked<&MetaRegionOwners>,
requires
owner.inv(),
self.wf(owner),
parent_owner.level == parent_owner.meta_value().level,
parent_owner.relate_guard(*self.node),
parent_owner.inv(),
parent_owner.level == owner.parent_level,
regions.inv(),
parent_owner.metaregion_sound_node(*regions),
returns
owner.is_node(),
)]
pub(in crate::mm) fn is_node(&self) -> bool {
self.pte.is_present() && !self.pte.is_last(
#[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&*parent_owner))]
self.node.level(),
)
}
Expand All @@ -160,7 +158,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
final(regions).inv(),
)]
pub(in crate::mm) fn to_ref(&self) -> ChildRef<'rcu, C> {
#[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&*parent_owner))]
let level = self.node.level();

// SAFETY:
Expand Down Expand Up @@ -381,7 +379,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
// SAFETY:
// - The PTE is not referenced by other `ChildRef`s (since we have `&mut self`).
// - The level matches the current node.
#[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&*parent_owner))]
let level = self.node.level();

let old_child = unsafe {
Expand All @@ -390,9 +388,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
};

if old_child.is_none() && !new_child.is_none() {
let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
&parent_owner.frame_permission,
)),
Expand All @@ -405,9 +401,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
}
nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
} else if !old_child.is_none() && new_child.is_none() {
let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
&parent_owner.frame_permission,
)),
Expand Down Expand Up @@ -635,7 +629,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
// For restoring `count_consistent` after adding the child below.
let ghost cp0 = parent_owner.children_perm.value();

#[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&*parent_owner))]
let level = self.node.level();

if entry_is_present || level <= 1 {
Expand Down Expand Up @@ -706,9 +700,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
self.node.write_pte(self.idx, self.pte)
};

let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
&parent_owner.frame_permission,
)),
Expand Down Expand Up @@ -894,7 +886,7 @@ impl<'a, 'rcu, C: PageTableConfig> Entry<'a, 'rcu, C> {
pub(in crate::mm) fn split_if_mapped_huge<A: InAtomicMode>(&mut self, guard: &'rcu A) -> Option<
PageTableGuard<'rcu, C>,
> {
#[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&*parent_owner))]
let level = self.node.level();

if !(self.pte.is_last(level) && level > 1) {
Expand Down Expand Up @@ -1616,7 +1608,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
self.read_pte(idx)
};

#[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&*parent_owner))]
let level = self.level();

let old_child = unsafe {
Expand All @@ -1628,9 +1620,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
let ghost cp0 = parent_owner.children_perm.value();

if old_child.is_none() && !new_child.is_none() {
let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
&parent_owner.frame_permission,
)),
Expand All @@ -1643,9 +1633,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
}
nr_children.write(Tracked(&mut parent_owner.meta_own.nr_children), _tmp + 1);
} else if !old_child.is_none() && new_child.is_none() {
let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
&parent_owner.frame_permission,
)),
Expand Down Expand Up @@ -1846,7 +1834,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
idx: usize,
guard: &'rcu A,
) -> PageTableGuard<'rcu, C> {
#[verus_spec(with Tracked(&*parent_owner), Tracked(&*regions))]
#[verus_spec(with Tracked(&*parent_owner))]
let level = self.level();

let ghost old_path = owner.value().path;
Expand Down Expand Up @@ -1929,9 +1917,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
// (`alloc` allocates a different slot, `write_pte` leaves regions
// immutable).

let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
&parent_owner.frame_permission,
)),
Expand Down Expand Up @@ -2055,9 +2041,7 @@ impl<'rcu, C: PageTableConfig> PageTableGuard<'rcu, C> {
) {
// For restoring `count_consistent` after the absent→frame install.
let ghost cp0 = parent_owner.children_perm.value();
let tracked meta_points_to = regions.slots.tracked_borrow(parent_owner.slot_index);
#[verus_spec(with
Tracked(meta_points_to),
Tracked(NodeOwner::<C>::tracked_borrow_frame_metadata_perm(
&parent_owner.frame_permission,
)),
Expand Down
Loading
Loading