Struct VmIoOwner 

pub struct VmIoOwner {
    pub id: nat,
    pub range: Range<usize>,
    pub is_fallible: bool,
    pub is_kernel: bool,
    pub mem_view: Option<VmIoMemView>,
}

The owner of a VM I/O operation, which tracks the memory range and the memory view for the operation.

Basically the caller should be only interested in this struct when using VmReader and VmWriter to perform VM I/O operations, since the safety of these operations depends on the validity of the memory range and memory view tracked by this struct.

Fields

id: nat

The unique identifier of this owner.

range: Range<usize>

The virtual address range owned by this owner.

is_fallible: bool

Whether this reader is fallible.

is_kernel: bool

Whether this owner is for kernel space.

mem_view: Option<VmIoMemView>

The mem view associated with this owner.

Implementations

impl VmIoOwner

pub open spec fn inv_wf(self) -> bool

{ self.range.start <= self.range.end }

Structural well-formedness: the range is ordered. Always holds after construction.

impl VmIoOwner

pub open spec fn has_read_view(self) -> bool

{ self.mem_view matches Some(VmIoMemView::ReadView(_)) }

Whether this owner carries a read memory view.

pub open spec fn has_write_view(self) -> bool

{ self.mem_view matches Some(VmIoMemView::WriteView(_)) }

Whether this owner carries a write memory view.

pub open spec fn can_read(self) -> bool

{ self.has_read_view() }

Whether this owner is ready to serve as the readable side of a copy.

pub open spec fn can_write(self) -> bool

{ self.has_write_view() }

Whether this owner is ready to serve as the writable side of a copy.

pub open spec fn read_view_initialized(self) -> bool

{
    match self.mem_view {
        Some(VmIoMemView::ReadView(mem_src)) => {
            forall |i: usize| {
                self.range.start <= i < self.range.end
                    ==> {
                        &&& mem_src.addr_transl(i) is Some
                        &&& mem_src.memory.contains_key((mem_src.addr_transl(i)->0).0)
                        &&& mem_src
                            .memory[(mem_src.addr_transl(i)->0).0]
                            .contents[(mem_src.addr_transl(i)->0).1 as int] is Init

                    }
            }
        }
        _ => false,
    }
}

Whether the read view initializes the entire owner range.

pub open spec fn overlaps(self, other: VmIoOwner) -> bool

{ !self.disjoint(other) }

Checks whether this owner overlaps with another owner.

pub open spec fn overlaps_with_range(self, range: Range<usize>) -> bool

{
    &&& self.range.start <= range.end
    &&& range.start <= self.range.end

}

pub open spec fn disjoint(self, other: VmIoOwner) -> bool

{
    &&& !self.overlaps_with_range(other.range)
    &&& match (self.mem_view, other.mem_view) {
        (Some(lhs), Some(rhs)) => {
            match (lhs, rhs) {
                (VmIoMemView::WriteView(lmv), VmIoMemView::WriteView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
                (VmIoMemView::WriteView(lmv), VmIoMemView::ReadView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
                (VmIoMemView::ReadView(lmv), VmIoMemView::WriteView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
                (VmIoMemView::ReadView(lmv), VmIoMemView::ReadView(rmv)) => {
                    lmv.mappings.disjoint(rmv.mappings)
                }
            }
        }
        _ => true,
    }

}

Checks whether this owner is disjoint with another owner.

pub open spec fn params_eq(self, other: VmIoOwner) -> bool

{
    &&& self.range == other.range
    &&& self.is_fallible == other.is_fallible

}

pub proof fn change_fallible(tracked &mut self, tracked fallible: bool)

requires

old(self).inv(),

old(self).is_fallible != fallible,

ensures

final(self).inv(),

final(self).is_fallible == fallible,

Changes the fallibility of this owner.

Verified Properties

Preconditions

• The owner must satisfy its invariant.
• The new fallibility must differ from the current one.

Postconditions

• The updated owner still satisfies its invariant.
• The is_fallible field is updated to fallible.

pub proof fn advance(tracked &mut self, nbytes: usize) -> tracked res : VmIoMemView

requires

old(self).inv(),

old(self).mem_view is Some,

nbytes <= old(self).range.end - old(self).range.start,

ensures

final(self).inv(),

final(self).range.start == old(self).range.start + nbytes,

final(self).range.end == old(self).range.end,

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

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

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

old(self)
    .mem_view matches Some(
    VmIoMemView::ReadView(_),
) ==> final(self).mem_view matches Some(VmIoMemView::ReadView(_)),

old(self)
    .mem_view matches Some(
    VmIoMemView::WriteView(_),
) ==> final(self).mem_view matches Some(VmIoMemView::WriteView(_)),

old(self).read_view_initialized() ==> final(self).read_view_initialized(),

old(self)
    .mem_view matches Some(
    VmIoMemView::ReadView(_),
) ==> forall |va: usize| {
    old(self).range.start + nbytes <= va < old(self).range.end
        && old(self).read_view_of().addr_transl(va) is Some
        && old(self)
            .read_view_of()
            .memory
            .contains_key((old(self).read_view_of().addr_transl(va)->0).0)
        ==> {
            &&& old(self).read_view_of().addr_transl(va)
                == final(self).read_view_of().addr_transl(va)
            &&& old(self).read_view_of().read(va) == final(self).read_view_of().read(va)

        }
},

Advances the cursor of the reader/writer by the given number of bytes.

Note this will return the advanced VmIoMemView as the previous permission is no longer needed and must be discarded then.

Verified Properties

Preconditions

• The owner must satisfy its invariant.
• The owner must carry a memory view.
• nbytes must not exceed the remaining length of the owned range.

Postconditions

• The updated owner still satisfies its invariant.
• The start of the owned range is advanced by nbytes.
• The end of the owned range and the other owner parameters are preserved.
• The returned VmIoMemView is the portion advanced past.

pub proof fn split(tracked &mut self, nbytes: usize) -> tracked r : VmIoOwner

requires

old(self).inv(),

old(self).mem_view is Some,

nbytes <= old(self).range.end - old(self).range.start,

ensures

r.inv(),

r.range.start == old(self).range.start,

r.range.end == old(self).range.start + nbytes,

r.is_fallible == old(self).is_fallible,

r.is_kernel == old(self).is_kernel,

r.mem_view is Some,

final(self).inv(),

final(self).range.start == old(self).range.start + nbytes,

final(self).range.end == old(self).range.end,

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

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

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

final(self).mem_view is Some,

old(self)
    .mem_view matches Some(
    VmIoMemView::ReadView(_),
) ==> {
    &&& r
        .mem_view matches Some(
        VmIoMemView::ReadView(_),
    ) &&& &&& final(self).mem_view matches Some(VmIoMemView::ReadView(_))


},

old(self)
    .mem_view matches Some(
    VmIoMemView::WriteView(_),
) ==> {
    &&& r
        .mem_view matches Some(
        VmIoMemView::WriteView(_),
    ) &&& &&& final(self).mem_view matches Some(VmIoMemView::WriteView(_))


},

old(self).read_view_initialized()
    ==> {
        &&& r.read_view_initialized()
        &&& final(self).read_view_initialized()

    },

Splits this owner at nbytes, returning the front portion as a new owner and shrinking self to cover the back portion.

Verified Properties

Preconditions

• The owner must satisfy its invariant.
• The owner must carry a memory view.
• nbytes must not exceed the remaining length of the owned range.

Postconditions

• Both the returned front owner and the updated self satisfy their invariants and carry the same kind of memory view as the original.
• The front owner covers [old.start, old.start + nbytes).
• self’s range becomes [old.start + nbytes, old.end).
• is_fallible, is_kernel are preserved on both sides.
• If the original was an initialized read view, both sides remain initialized.

pub proof fn tracked_read_view_unwrap(tracked &self) -> tracked r : &MemView

requires

self.inv(),

self.mem_view matches Some(VmIoMemView::ReadView(_)),

ensures

VmIoMemView::ReadView(*r) == self.mem_view->0,

*r == Self::read_view_of(*self),

Unwraps the read view.

Verified Properties

Preconditions

• The owner must satisfy its invariant.
• The owner must carry a read memory view.

Postconditions

• The returned reference is exactly the read view stored in self.mem_view.

pub open spec fn read_view_of(self) -> MemView

{
    match self.mem_view {
        Some(VmIoMemView::ReadView(mv)) => mv,
        _ => arbitrary(),
    }
}

Spec helper: extract the MemView from a read-view owner.

Defined only when self.mem_view matches Some(ReadView(_)); otherwise returns an arbitrary value. Callers should establish the matching pattern via [has_read_view] before using this.

pub proof fn write_to_read(tracked &mut self)

requires

old(self).inv(),

old(self).mem_view matches Some(VmIoMemView::WriteView(_)),

ensures

final(self).inv(),

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

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

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

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

final(self).mem_view matches Some(VmIoMemView::ReadView(_)),

old(self)
    .mem_view matches Some(
    VmIoMemView::WriteView(mv),
) ==> final(self).mem_view matches Some(VmIoMemView::ReadView(rv)) && rv == mv,

Converts the owner’s VmIoMemView::WriteView into a VmIoMemView::ReadView wrapping the same underlying MemView.

Used after a write-only phase (e.g., VmWriter::fill) to hand the buffer back as a read-only handle.

Verified Properties

Preconditions

• The owner must satisfy its invariant and carry a write memory view.

Postconditions

• The owner still satisfies its invariant.
• All structural fields (range, is_fallible, is_kernel, id) are preserved.
• The memory view is now VmIoMemView::ReadView wrapping the same MemView as the original VmIoMemView::WriteView.

Trait Implementations

impl Inv for VmIoOwner

open spec fn inv(self) -> bool

{
    &&& self.inv_wf()
    &&& match self.mem_view {
        Some(VmIoMemView::WriteView(mv)) => (
            &&& mv.mappings_are_disjoint()
            &&& forall |va: usize| {
                self.range.start <= va < self.range.end
                    ==> {
                        &&& #[trigger] mv.addr_transl(va) is Some

                    }
            }

        ),
        Some(VmIoMemView::ReadView(mv)) => (
            &&& mv.mappings_are_disjoint()
            &&& forall |va: usize| {
                self.range.start <= va < self.range.end
                    ==> {
                        &&& #[trigger] mv.addr_transl(va) is Some

                    }
            }

        ),
        None => true,
    }

}

Full invariant: well-formed AND memory view (if present) covers the range.