ostd::specs::mm::embedding

Struct VmStore

pub struct VmStore<'rcu> {
    pub regions: MetaRegionOwners,
    pub tlb_model: TlbModel,
    pub vm_spaces: Map<VmSpaceId, VmSpaceOwner>,
    pub cursors: Map<CursorId, CursorEntry<'rcu>>,
    pub vm_ios: Map<VmIoId, VmIoEntry>,
    pub frames: Map<FrameId, FrameEntry>,
    pub segments: Map<SegmentId, SegmentEntry>,
}

Expand description

Resource store: the abstract state visible to a caller of the VmSpace + VmReader/VmWriter API.

tlb_model is the global TLB model; mirrors the per-CPU TlbModel that CursorMut::map/unmap and flusher operate on. We keep one per store on the conservative assumption that any cursor mutation interacts with it.

Fields§

§regions: MetaRegionOwners§tlb_model: TlbModel§vm_spaces: Map<VmSpaceId, VmSpaceOwner>§cursors: Map<CursorId, CursorEntry<'rcu>>§vm_ios: Map<VmIoId, VmIoEntry>§frames: Map<FrameId, FrameEntry>§segments: Map<SegmentId, SegmentEntry>

Implementations§

Source §

impl<'a, 'rcu> VmStore<'rcu>

Source

pub open spec fn inv(self) -> bool

{ self.structural_inv() && self.accounting_inv() }

The store’s top-level invariant.

Decomposed into [structural_inv] (everything generic store helpers can preserve when they only touch one of frames / cursors / vm_ios / vm_spaces) and [accounting_inv] (the exact reference-count equation, which couples frames with regions.slot_owners and can only be re-established by a step that pairs the two changes — see [extract_frame] / [insert_frame] for why the frame-only helpers must require / ensure only the structural part).

Source

pub open spec fn structural_inv(self) -> bool

{
    &&& self.regions.inv()
    &&& forall |idx: usize| {
        idx < max_meta_slots() ==> #[trigger] self.regions.slots.contains_key(idx)
    }
    &&& forall |idx: usize| {
        idx < max_meta_slots()
            ==> #[trigger] self.regions.slot_owners[idx].inner_perms.in_list.value() == 0
    }
    &&& self.tlb_model.inv()
    &&& forall |id: VmSpaceId| {
        #[trigger] self.vm_spaces.dom().contains(id) ==> self.vm_spaces[id].inv()
    }
    &&& forall |id: CursorId| {
        #[trigger] self.cursors.dom().contains(id) ==> self.cursors[id].inv()
    }
    &&& forall |id: CursorId| {
        #[trigger] self.cursors.dom().contains(id)
            ==> self.cursors[id].owner.metaregion_sound(self.regions)
    }
    &&& forall |id: CursorId| {
        #[trigger] self.cursors.dom().contains(id)
            ==> self.vm_spaces.dom().contains(self.cursors[id].vm_space)
    }
    &&& forall |id: VmIoId| {
        #[trigger] self.vm_ios.dom().contains(id) ==> self.vm_ios[id].inv()
    }
    &&& forall |id: VmIoId| {
        #[trigger] self.vm_ios.dom().contains(id)
            ==> (self
                .vm_ios[id]
                .vm_space matches Some(vs) ==> self.vm_spaces.dom().contains(vs))
    }
    &&& forall |id: VmIoId| {
        #[trigger] self.vm_ios.dom().contains(id)
            ==> (self.vm_ios[id].vm_space is Some
                ==> (self.vm_ios[id].vaddr as nat) + (self.vm_ios[id].len as nat)
                    <= MAX_USERSPACE_VADDR as nat)
    }
    &&& forall |fid: FrameId| {
        #[trigger] self.frames.dom().contains(fid)
            ==> has_safe_slot(self.frames[fid].paddr)
    }
    &&& forall |fid: FrameId| {
        #[trigger] self.frames.dom().contains(fid)
            ==> self.regions.slot_owners[frame_to_index(self.frames[fid].paddr)].usage
                == PageUsage::Frame
    }
    &&& self.frames.dom().finite()
    &&& self.segments.dom().finite()
    &&& forall |sid: SegmentId| {
        #[trigger] self.segments.dom().contains(sid)
            ==> {
                let r = self.segments[sid].range;
                &&& r.start % PAGE_SIZE == 0
                &&& r.end % PAGE_SIZE == 0
                &&& r.start < r.end
                &&& r.end <= MAX_PADDR

            }
    }
    &&& forall |sid: SegmentId, paddr: Paddr| {
        self.segments.dom().contains(sid)
            && self.segments[sid].range.start <= paddr < self.segments[sid].range.end
            && paddr % PAGE_SIZE == 0
            ==> self.regions.slot_owners[frame_to_index(paddr)].usage == PageUsage::Frame
    }

}

Everything in [inv] except the accounting equation. Preserved by any helper that touches at most one of frames / regions.slot_owners, since the accounting equation is the only clause that mentions both. Frame-only helpers ([extract_frame] / [insert_frame]) require / ensure this.

Source

pub open spec fn accounting_inv(self) -> bool

{
    &&& forall |idx: usize| {
        idx < max_meta_slots()
            && self.regions.slot_owners[idx].inner_perms.ref_count.value()
                == REF_COUNT_UNUSED
            ==> handle_count(self.frames, idx) == 0
                && self.regions.slot_owners[idx].paths_in_pt.is_empty()
                && segment_cover_count(self.segments, index_to_frame(idx)) == 0
    }
    &&& forall |idx: usize| {
        idx < max_meta_slots() && self.regions.slot_owners[idx].usage == PageUsage::Frame
            && self.regions.slot_owners[idx].inner_perms.ref_count.value()
                != REF_COUNT_UNUSED
            && self.regions.slot_owners[idx].inner_perms.ref_count.value()
                != REF_COUNT_UNIQUE
            ==> handle_count(self.frames, idx) > 0
                || self.regions.slot_owners[idx].paths_in_pt.len() > 0
                || segment_cover_count(self.segments, index_to_frame(idx)) > 0
    }
    &&& forall |idx: usize| {
        idx < max_meta_slots() && self.regions.slot_owners[idx].usage == PageUsage::Frame
            && (handle_count(self.frames, idx) > 0
                || self.regions.slot_owners[idx].paths_in_pt.len() > 0
                || segment_cover_count(self.segments, index_to_frame(idx)) > 0)
            ==> {
                let so = self.regions.slot_owners[idx];
                let rc = so.inner_perms.ref_count.value();
                &&& rc != REF_COUNT_UNUSED
                &&& rc != REF_COUNT_UNIQUE
                &&& rc
                    == handle_count(self.frames, idx) + so.paths_in_pt.len()
                        + segment_cover_count(self.segments, index_to_frame(idx))
                &&& so.inner_perms.storage.is_init()

            }
    }

}

Stage 5 / full #4 — EXACT reference-count accounting.

Scoped to active-head tracked data frames: usage == Frame (excludes PT nodes — different rc semantics — and MMIO), and the slot is an active head (#handles > 0 || #mappings > 0). The active-head restriction sidesteps huge-page sub-page slots (j>0): those have H==0, paths.len()==0, yet rc>0 via frame_sub_pages_valid, so they are not active heads and the equation does not apply to them (and op_pre[FrameDrop] never targets a sub-page — a FrameEntry paddr is always a head).

For an active head: rc is neither sentinel, equals #handles + #mappings, and the slot’s metadata storage is initialised (it is in use).

The exact equation is Frame-scoped. For non-Frame FrameEntry slots, the residual drop_pre obligation (rc/storage/in_list/ paths) is carried directly in op_pre[FrameDrop] (un-doing part of #4) until the deferred main-verification refactor strengthens MetaSlotOwner::inv and adds Frame::wf(state).

Why split from structural_inv: the equation references both self.frames (via handle_count) and self.regions.slot_owners (via rc and paths_in_pt), so any helper that mutates one without the other can break it transiently. The frame-only store helpers [extract_frame] / [insert_frame] therefore cannot ensure this clause alone — a step that pairs a frame change with the matching regions change (via a frame / cursor _embedded axiom) re-establishes it.

Source §

impl<'rcu> VmStore<'rcu>

Source

pub proof fn extract_vm_space(tracked &mut self, vs: VmSpaceId) -> tracked res : VmSpaceOwner

requires

old(self).inv(),

old(self).vm_spaces.dom().contains(vs),

forall |c: CursorId| {
    #[trigger] old(self).cursors.dom().contains(c)
        ==> old(self).cursors[c].vm_space != vs
},

forall |v: VmIoId| {
    #[trigger] old(self).vm_ios.dom().contains(v)
        ==> old(self).vm_ios[v].vm_space != Some(vs)
},

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces.remove(vs),

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames,

final(self).segments == old(self).segments,

res == old(self).vm_spaces[vs],

final(self).inv(),

Removes the VmSpaceOwner at vs from the store and returns it. Requires no cursor or VmIo refers to vs, and no activated ranges remain on vs (otherwise inv would break after the removal).

Source

pub proof fn insert_vm_space(tracked &mut self, vs: VmSpaceId, tracked owner: VmSpaceOwner)

requires

old(self).inv(),

!old(self).vm_spaces.dom().contains(vs),

owner.inv(),

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces.insert(vs, owner),

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames,

final(self).segments == old(self).segments,

final(self).inv(),

Inserts a VmSpaceOwner at the given fresh id. Requires the id is not already used and the owner satisfies its invariant.

Source

pub proof fn extract_cursor(tracked &mut self, c: CursorId) -> tracked res : CursorEntry<'rcu>

requires

old(self).inv(),

old(self).cursors.dom().contains(c),

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors.remove(c),

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames,

final(self).segments == old(self).segments,

res == old(self).cursors[c],

final(self).inv(),

Removes the cursor entry at c from the store and returns it.

Source

pub proof fn insert_cursor(tracked &mut self, c: CursorId, tracked entry: CursorEntry<'rcu>)

requires

old(self).inv(),

!old(self).cursors.dom().contains(c),

entry.inv(),

entry.owner.metaregion_sound(old(self).regions),

old(self).vm_spaces.dom().contains(entry.vm_space),

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors.insert(c, entry),

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames,

final(self).segments == old(self).segments,

final(self).inv(),

Inserts a cursor entry at the given fresh id. Requires the id is not already used, the entry satisfies its inv, the entry’s vm_space is in the store, and the entry’s owner is sound w.r.t. the store’s regions.

Source

pub proof fn extract_vm_io(tracked &mut self, vio: VmIoId) -> tracked res : VmIoEntry

requires

old(self).inv(),

old(self).vm_ios.dom().contains(vio),

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios.remove(vio),

final(self).frames == old(self).frames,

final(self).segments == old(self).segments,

res == old(self).vm_ios[vio],

final(self).inv(),

Removes the VmIo entry at vio from the store and returns it.

Source

pub proof fn insert_vm_io(tracked &mut self, vio: VmIoId, tracked entry: VmIoEntry)

requires

old(self).inv(),

!old(self).vm_ios.dom().contains(vio),

entry.inv(),

entry.vm_space matches Some(vs) ==> old(self).vm_spaces.dom().contains(vs),

entry.vm_space is Some
    ==> (entry.vaddr as nat) + (entry.len as nat) <= MAX_USERSPACE_VADDR as nat,

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios.insert(vio, entry),

final(self).frames == old(self).frames,

final(self).segments == old(self).segments,

final(self).inv(),

Inserts a VmIo entry at the given fresh id. Requires the id is not already used, the entry satisfies its inv, the entry’s vm_space (if Some) refers to a live VmSpace, the range bound holds when vm_space is Some, and (if the entry is activated) its owner range is disjoint from every existing activated entry’s owner range (preserves the pairwise-disjoint invariant in VmStore::inv).

Source

pub proof fn extract_frame(tracked &mut self, fid: FrameId) -> tracked res : FrameEntry

requires

old(self).structural_inv(),

old(self).frames.dom().contains(fid),

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames.remove(fid),

final(self).segments == old(self).segments,

res == old(self).frames[fid],

final(self).structural_inv(),

Removes the FrameEntry at fid from the store.

Requires / ensures only [structural_inv] — not full [inv]. Removing a frame handle without coordinating with the slot’s ref_count breaks [accounting_inv] transiently; the step that calls this is responsible for pairing it with the matching frame::drop_step (or cursor::map_step once Op::Map consumes a tracked frame) and re-establishing accounting at the end.

Source

pub proof fn insert_frame(tracked &mut self, fid: FrameId, tracked entry: FrameEntry)

requires

old(self).structural_inv(),

!old(self).frames.dom().contains(fid),

has_safe_slot(entry.paddr),

old(self).regions.slot_owners[frame_to_index(entry.paddr)].usage == PageUsage::Frame,

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames.insert(fid, entry),

final(self).segments == old(self).segments,

final(self).structural_inv(),

Inserts a FrameEntry at the given fresh id. Requires the entry’s paddr be has_safe_slot — the per-FrameEntry clause of VmStore::inv (#4). Every caller establishes this from the from_* axioms’ !has_safe_slot ==> None (a registered handle is necessarily in-bound).

Requires / ensures only [structural_inv] — see [extract_frame] for the accounting/structural split rationale.

Source

pub proof fn extract_segment(tracked &mut self, sid: SegmentId) -> tracked res : SegmentEntry

requires

old(self).segments.dom().contains(sid),

old(self).segments.dom().finite(),

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames,

final(self).segments == old(self).segments.remove(sid),

res == old(self).segments[sid],

Removes the SegmentEntry at sid from the store. Does NOT ensure structural_inv — extracting a segment without a paired regions decrement breaks the raw_count == segment_cover_count clause at every paddr the segment covered. The caller’s step proof must restore it via [segment::drop_step] before observing s.inv() again.

Source

pub proof fn insert_segment(tracked &mut self, sid: SegmentId, tracked entry: SegmentEntry)

requires

!old(self).segments.dom().contains(sid),

ensures

final(self).regions == old(self).regions,

final(self).tlb_model == old(self).tlb_model,

final(self).vm_spaces == old(self).vm_spaces,

final(self).cursors == old(self).cursors,

final(self).vm_ios == old(self).vm_ios,

final(self).frames == old(self).frames,

final(self).segments == old(self).segments.insert(sid, entry),

Source §

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

Performs the conversion.

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

Performs the conversion.

§

Struct VmStore Copy item path

Fields§

Implementations§

impl<'a, 'rcu> VmStore<'rcu>

pub open spec fn inv(self) -> bool

pub open spec fn structural_inv(self) -> bool

pub open spec fn accounting_inv(self) -> bool

impl<'rcu> VmStore<'rcu>

pub proof fn extract_vm_space(tracked &mut self, vs: VmSpaceId) -> tracked res : VmSpaceOwner

pub proof fn insert_vm_space(tracked &mut self, vs: VmSpaceId, tracked owner: VmSpaceOwner)

pub proof fn extract_cursor(tracked &mut self, c: CursorId) -> tracked res : CursorEntry<'rcu>

pub proof fn insert_cursor(tracked &mut self, c: CursorId, tracked entry: CursorEntry<'rcu>)

pub proof fn extract_vm_io(tracked &mut self, vio: VmIoId) -> tracked res : VmIoEntry

pub proof fn insert_vm_io(tracked &mut self, vio: VmIoId, tracked entry: VmIoEntry)

pub proof fn extract_frame(tracked &mut self, fid: FrameId) -> tracked res : FrameEntry

pub proof fn insert_frame(tracked &mut self, fid: FrameId, tracked entry: FrameEntry)

pub proof fn extract_segment(tracked &mut self, sid: SegmentId) -> tracked res : SegmentEntry

pub proof fn insert_segment(tracked &mut self, sid: SegmentId, tracked entry: SegmentEntry)

Auto Trait Implementations§

impl<'rcu> Freeze for VmStore<'rcu>

impl<'rcu> !RefUnwindSafe for VmStore<'rcu>

impl<'rcu> Send for VmStore<'rcu>

impl<'rcu> Sync for VmStore<'rcu>

impl<'rcu> Unpin for VmStore<'rcu>

impl<'rcu> UnsafeUnpin for VmStore<'rcu>

impl<'rcu> !UnwindSafe for VmStore<'rcu>

Blanket Implementations§

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

fn type_id(&self) -> TypeId

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

fn borrow(&self) -> &T

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

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

impl<T> From<T> for T

fn from(t: T) -> T

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

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

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

fn into(self) -> U

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

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

type Error = Infallible

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

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

fn obeys_try_from_spec() -> bool

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

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

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

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

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__Awhere 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 Twhere U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

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

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

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

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

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

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

Struct VmStore

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

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

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

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

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

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

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

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

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

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

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

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

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,