Struct FrameContents 

pub struct FrameContents {
    pub contents: Seq<MemContents<u8>>,
    pub size: usize,
    pub range: Range<Paddr>,
}

Byte contents of one physical frame range tracked in a MemView.

This is the physical-memory side of the model: each frame base Paddr maps to a FrameContents value whose metadata (size, range) constrains how contents can be interpreted.

Fields

contents: Seq<MemContents<u8>>

Per-byte initialization/value state for this frame.

size: usize

Frame size in bytes.

range: Range<Paddr>

Physical range covered by this frame, modeled as [start, end).

Trait Implementations

impl Inv for FrameContents

open spec fn inv(self) -> bool

{
    &&& self.contents.len() == self.size@
    &&& self.size@ == self.range.end - self.range.start
    &&& self.range.start % self.size == 0
    &&& self.range.end % self.size == 0
    &&& self.range.start <= self.range.end < MAX_PADDR

}

Well-formedness invariant for FrameContents.

Invariant

• contents.len() == size.
• size == range.end - range.start.
• range.start and range.end are aligned to size.
• range is ordered and remains below MAX_PADDR.