Struct VirtPtr 

pub struct VirtPtr {
    pub vaddr: Vaddr,
    pub range: Ghost<Range<Vaddr>>,
}

Specification-level virtual pointer with an associated half-open range.

VirtPtr models a C-like pointer used by verification code:

• vaddr is the current cursor position;
• range is the allocation-like bounds [start, end).

Most operations require is_valid() (i.e., the current pointer is within range and not one-past-end), while offset operations additionally require the computed address to stay inside the same range.

Fields

vaddr: Vaddr

Current virtual address represented by this pointer value.

range: Ghost<Range<Vaddr>>

Logical bounds of the pointer’s valid object/range.

Implementations

impl VirtPtr

pub exec fn new(vaddr: Vaddr, len: usize) -> Self

returns

({
    Self {
        vaddr,
        range: Ghost(Range {
            start: vaddr,
            end: (::vstd::prelude::add(vaddr, len)) as usize,
        }),
    }
}),

Creates a pointer at vaddr with logical range [vaddr, vaddr + len).

pub open spec fn is_defined(self) -> bool

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

Whether the pointer has consistent bounds.

pub open spec fn is_valid(self) -> bool

{
    &&& self.is_defined()
    &&& self.vaddr < self.range@.end

}

Whether dereferencing the current pointer position is allowed.

This excludes the one-past-end position (vaddr == range.end).

pub exec fn read(self, Tracked(mem): Tracked<&MemView>) -> u8

requires

mem.addr_transl(self.vaddr) is Some,

mem
    .memory[(mem.addr_transl(self.vaddr)->0).0]
    .contents[(mem.addr_transl(self.vaddr)->0).1 as int] is Init,

self.is_valid(),

returns

mem.read(self.vaddr).value(),

Reads one byte from self.vaddr in the provided memory view.

Verified Properties

Preconditions

• mem.addr_transl(self.vaddr) is Some.
• Target byte is initialized: mem.memory[mem.addr_transl(self.vaddr).unwrap().0].contents[mem.addr_transl(self.vaddr).unwrap().1 as int] is Init.
• self.is_valid().

Postconditions

• Returns mem.read(self.vaddr).value().

pub exec fn write(self, Tracked(mem): Tracked<&mut MemView>, x: u8)

requires

old(mem).addr_transl(self.vaddr) is Some,

self.is_valid(),

ensures

*final(mem) == old(mem).write(self.vaddr, x),

Writes one byte to self.vaddr in the provided memory view.

Verified Properties

Preconditions

• old(mem).addr_transl(self.vaddr) is Some.
• self.is_valid().

Postconditions

• *mem == old(mem).write(self.vaddr, x).

pub exec fn read_volatile<T: PodOnce>(self, Tracked(mem): Tracked<&MemView>) -> val : T

requires

self.inv(),

core::mem::size_of::<T>() <= self.range@.end - self.vaddr,

self.vaddr % core::mem::align_of::<T>() == 0,

forall |i: usize| {
    self.vaddr <= i < self.vaddr + core::mem::size_of::<T>()
        ==> {
            &&& mem.addr_transl(i) is Some
            &&& mem.memory.contains_key((mem.addr_transl(i)->0).0)
            &&& mem
                .memory[(mem.addr_transl(i)->0).0]
                .contents[(mem.addr_transl(i)->0).1 as int] is Init

        }
},

ensures

pod_bytes(val) == mem.read_bytes(self.vaddr, core::mem::size_of::<T>()),

Reads a PodOnce value using one volatile memory load from a verified memory view.

Verified Properties

Preconditions

• self.inv().
• The readable range [self.vaddr, self.vaddr + size_of::<T>()) must fit in self.range@.
• self.vaddr must satisfy the alignment requirement of T.
• Every byte in that range must translate in mem and be initialized.

Safety

• This function is trusted because the underlying volatile typed read relies on raw-pointer operations that Verus does not yet model directly.

pub exec fn write_volatile<T: Pod>( self, Tracked(mem): Tracked<&mut MemView>, val: T, )

requires

self.inv(),

core::mem::size_of::<T>() <= self.range@.end - self.vaddr,

self.vaddr % core::mem::align_of::<T>() == 0,

forall |i: usize| {
    self.vaddr <= i < self.vaddr + core::mem::size_of::<T>()
        ==> {
            &&& old(mem).addr_transl(i) is Some

        }
},

ensures

*final(mem) == old(mem).write_bytes(self.vaddr, pod_bytes(val)),

final(mem).mappings == old(mem).mappings,

old(mem).memory.dom().subset_of(final(mem).memory.dom()),

forall |va: usize| old(mem).addr_transl(va) == final(mem).addr_transl(va),

Writes a Pod value of size size_of::<T>() bytes using a volatile memory store to a verified memory view.

For T: PodOnce the underlying store is non-tearing (single instruction). For arbitrary T: Pod the store may tear across multiple instructions but completes before this function returns.

Verified Properties

Preconditions

• self.inv().
• The writable range [self.vaddr, self.vaddr + size_of::<T>()) must fit in self.range@.
• self.vaddr must satisfy the alignment requirement of T.
• Every byte in that range must translate in mem.

Postconditions

• The final memory equals old(mem).write_bytes(self.vaddr, pod_bytes(val)).
• mem.mappings is unchanged (derivable from write_bytes, but stated directly for caller convenience).
• mem.memory.dom() can only grow (same).
• addr_transl is preserved for every virtual address (same).

Safety

• This function is trusted because the underlying volatile typed write relies on raw-pointer operations that Verus does not yet model directly.

pub open spec fn add_spec(self, n: usize) -> Self

{
    VirtPtr {
        vaddr: (self.vaddr + n) as usize,
        range: self.range,
    }
}

pub exec fn add(&mut self, n: usize)

requires

0 <= old(self).vaddr + n < usize::MAX,

ensures

*final(self) == old(self).add_spec(n),

Advances the pointer by n bytes.

This operation only updates the cursor; it does not perform memory access.

Verified Properties

Preconditions

• 0 <= old(self).vaddr + n < usize::MAX.

Postconditions

• *self == old(self).add_spec(n).

pub open spec fn sub_spec(self, n: usize) -> Self

{
    VirtPtr {
        vaddr: (self.vaddr - n) as usize,
        range: self.range,
    }
}

pub exec fn sub(self, n: usize) -> res : Self

requires

n <= self.vaddr,

returns

self.sub_spec(n),

Returns a new pointer whose address is self.vaddr rewound by n bytes.

Mirrors the shape of [<*const T>::sub] / [<*mut T>::sub] in the raw-pointer API: takes self by value and returns the new pointer.

Verified Properties

Preconditions

• n <= self.vaddr (no underflow).

Postconditions

• res == self.sub_spec(n).

pub open spec fn wrapping_add_spec(self, n: usize) -> Self

{
    VirtPtr {
        vaddr: self.vaddr.wrapping_add(n),
        range: self.range,
    }
}

pub exec fn wrapping_add(self, n: usize) -> res : Self

returns

self.wrapping_add_spec(n),

Returns a new pointer whose address is self.vaddr advanced by n bytes using wrapping arithmetic.

pub exec fn cast<T>(self) -> res : *mut T

ensures

res as usize == self.vaddr,

Reinterprets self.vaddr as a typed raw pointer to T.

This is purely a type cast; no memory access is performed and no alignment is checked. The returned pointer carries no provenance — it is suitable for runtime checks (e.g., is_aligned) and for unsafe volatile reads/writes whose preconditions are independently verified.

pub open spec fn read_offset_spec(self, mem: MemView, n: usize) -> u8

{ mem.read((self.vaddr + n) as usize).value() }

pub exec fn read_offset(&self, Tracked(mem): Tracked<&MemView>, n: usize) -> u8

requires

self.vaddr + n < usize::MAX,

self.range@.start <= self.vaddr + n < self.range@.end,

mem.addr_transl((self.vaddr + n) as usize) is Some,

mem
    .memory[(mem.addr_transl((self.vaddr + n) as usize)->0).0]
    .contents[(mem.addr_transl((self.vaddr + n) as usize)->0).1 as int] is Init,

returns

self.read_offset_spec(*mem, n),

Reads from self.vaddr + n without mutating self.

Implemented by creating a temporary pointer and calling Self::read. When self.vaddr == self.range.start, this behaves like array indexing.

Verified Properties

Preconditions

• self.vaddr + n < usize::MAX.
• self.range@.start <= self.vaddr + n < self.range@.end.
• mem.addr_transl((self.vaddr + n) as usize) is Some.
• Target byte at offset is initialized.

Postconditions

• Returns self.read_offset_spec(*mem, n).

pub open spec fn write_offset_spec(self, mem: MemView, n: usize, x: u8) -> MemView

{ mem.write((self.vaddr + n) as usize, x) }

pub exec fn write_offset( &self, Tracked(mem): Tracked<&mut MemView>, n: usize, x: u8, )

requires

self.inv(),

self.vaddr + n < usize::MAX,

self.range@.start <= self.vaddr + n < self.range@.end,

old(mem).addr_transl((self.vaddr + n) as usize) is Some,

ensures

*final(mem) == self.write_offset_spec(*old(mem), n, x),

Writes to self.vaddr + n without mutating self.

Verified Properties

Preconditions

• self.inv().
• self.range@.start <= self.vaddr + n < self.range@.end.
• old(mem).addr_transl((self.vaddr + n) as usize) is Some.

pub open spec fn copy_offset_spec( src: Self, dst: Self, mem_src: MemView, mem_dst: MemView, n: usize, ) -> MemView

{
    let x = src.read_offset_spec(mem_src, n);
    dst.write_offset_spec(mem_dst, n, x)
}

pub exec fn copy_offset( src: &Self, dst: &Self, Tracked(mem_src): Tracked<&MemView>, Tracked(mem_dst): Tracked<&mut MemView>, n: usize, )

requires

src.inv(),

dst.inv(),

src.vaddr + n < usize::MAX,

dst.vaddr + n < usize::MAX,

src.range@.start <= src.vaddr + n < src.range@.end,

mem_src.addr_transl((src.vaddr + n) as usize) is Some,

mem_src.memory.contains_key((mem_src.addr_transl((src.vaddr + n) as usize)->0).0),

mem_src
    .memory[(mem_src.addr_transl((src.vaddr + n) as usize)->0).0]
    .contents[(mem_src.addr_transl((src.vaddr + n) as usize)->0).1 as int] is Init,

dst.range@.start <= dst.vaddr + n < dst.range@.end,

old(mem_dst).addr_transl((dst.vaddr + n) as usize) is Some,

ensures

*final(mem_dst) == Self::copy_offset_spec(*src, *dst, *mem_src, *old(mem_dst), n),

final(mem_dst).mappings == old(mem_dst).mappings,

old(mem_dst).memory.dom().subset_of(final(mem_dst).memory.dom()),

Copies one byte from src + n to dst + n.

Source and destination are reasoned about via distinct memory views.

Verified Properties

Preconditions

• src.inv() and dst.inv().
• Source offset and destination offset are both in-range.
• Source offset is mapped and initialized in mem_src.
• Destination offset is mapped in old(mem_dst).

Postconditions

• *mem_dst == Self::copy_offset_spec(*src, *dst, *mem_src, *old(mem_dst), n).
• mem_dst.mappings == old(mem_dst).mappings.
• mem_dst.memory.dom() == old(mem_dst).memory.dom().

pub open spec fn memcpy_spec( src: Self, dst: Self, mem_src: MemView, mem_dst: MemView, n: usize, ) -> MemView

{
    if n == 0 {
        mem_dst
    } else {
        let mem_dst_1 = Self::copy_offset_spec(
            src,
            dst,
            mem_src,
            mem_dst,
            (n - 1) as usize,
        );
        Self::memcpy_spec(src, dst, mem_src, mem_dst_1, (n - 1) as usize)
    }
}

pub exec fn copy_nonoverlapping( src: &Self, dst: &Self, Tracked(mem_src): Tracked<&MemView>, Tracked(mem_dst): Tracked<&mut MemView>, n: usize, )

requires

src.inv(),

dst.inv(),

src.range@.start <= src.vaddr,

src.vaddr + n <= src.range@.end,

forall |i: usize| {
    src.vaddr <= i < src.vaddr + n
        ==> {
            &&& 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

        }
},

dst.range@.start <= dst.vaddr,

dst.vaddr + n <= dst.range@.end,

forall |i: usize| {
    dst.vaddr <= i < dst.vaddr + n
        ==> {
            &&& old(mem_dst).addr_transl(i) is Some

        }
},

ensures

*final(mem_dst) == Self::memcpy_spec(*src, *dst, *mem_src, *old(mem_dst), n),

final(mem_dst).mappings == old(mem_dst).mappings,

old(mem_dst).memory.dom().subset_of(final(mem_dst).memory.dom()),

forall |i: usize| {
    dst.vaddr <= i < dst.vaddr + n
        ==> {
            &&& final(mem_dst).addr_transl(i) is Some

        }
},

Copies n bytes from src to dst in the given memory view.

mem_src and mem_dst are independent tracked memory views — the verifier enforces this by virtue of the &MemView / &mut MemView ownership pattern, so no vaddr-level non-overlap precondition is needed. (mem_src is never mutated during the copy; each byte is read from its original state.)

Verified Properties

Preconditions

• src.inv() and dst.inv().
• Source slice [src.vaddr, src.vaddr + n) is in-range and initialized in mem_src.
• Destination slice [dst.vaddr, dst.vaddr + n) is in-range and mapped in old(mem_dst).

Postconditions

• *mem_dst == Self::memcpy_spec(*src, *dst, *mem_src, *old(mem_dst), n).
• mem_dst.mappings == old(mem_dst).mappings.
• mem_dst.memory.dom() == old(mem_dst).memory.dom().
• Destination slice remains mapped in mem_dst.

pub exec fn from_vaddr(vaddr: usize, len: usize) -> r : Self

requires

len <= usize::MAX - vaddr,

ensures

r.inv(),

r.vaddr == vaddr,

r.range@.start == vaddr,

r.range@.end == (vaddr + len) as usize,

len > 0 ==> r.is_valid(),

Builds a valid VirtPtr from a concrete virtual-address range.

Verified Properties

Preconditions

• len <= usize::MAX - vaddr.

Postconditions

• r.range@.start == vaddr.
• r.range@.end == (vaddr + len) as usize.
• When len > 0, the result is valid for dereferencing.

pub exec fn split(self, n: usize) -> r : (Self, Self)

requires

self.is_valid(),

0 <= n <= self.range@.end - self.range@.start,

self.vaddr == self.range@.start,

ensures

r.0.range@.start == self.range@.start,

r.0.range@.end == self.range@.start + n,

r.0.vaddr == self.range@.start,

r.1.range@.start == self.range@.start + n,

r.1.range@.end == self.range@.end,

r.1.vaddr == self.range@.start + n,

Executable helper to split the VirtPtr into two contiguous ranges.

This updates ghost ranges to match a split operation over the same region.

Verified Properties

Preconditions

• self.is_valid().
• 0 <= n <= self.range@.end - self.range@.start.
• self.vaddr == self.range@.start.

Postconditions

• Left pointer covers [self.range@.start, self.range@.start + n).
• Right pointer covers [self.range@.start + n, self.range@.end).

pub exec fn addr(&self) -> Vaddr

returns

self.vaddr,

Trait Implementations

impl Clone for VirtPtr

exec fn clone(&self) -> res : Self

ensures

res == self,

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for VirtPtr

impl Inv for VirtPtr

open spec fn inv(self) -> bool

{
    &&& self.range@.start <= self.vaddr <= self.range@.end
    &&& self.range@.end >= self.range@.start

}