Struct VirtPtr &nbsp; Copy item path

impl VirtPtr

pub open spec fn is_defined(self) -> bool

{
    &&& self.vaddr != 0
    &&& self.range@.start <= self.vaddr <= self.range@.end

}

pub open spec fn is_valid(self) -> bool

{
    &&& self.is_defined()
    &&& self.vaddr < self.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).unwrap()] is Init,

self.is_valid(),

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

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

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

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

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

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

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

requires

0 < 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).unwrap()] is Init,

Unlike add, we just create a temporary pointer value and read that When self.vaddr == self.range.start this acts like array index notation

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

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

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

requires

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: MemView, n: usize) -> MemView

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

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

requires

src.inv(),

dst.inv(),

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

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

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

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

old(mem).memory.contains_key(old(mem).addr_transl((src.vaddr + n) as usize).unwrap()),

old(mem).memory[old(mem).addr_transl((src.vaddr + n) as usize).unwrap()] is Init,

ensures

*mem == Self::copy_offset_spec(*src, *dst, *old(mem), n),

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

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

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

requires

src.inv(),

dst.inv(),

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

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

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

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

src.range@.end <= dst.range@.start || dst.range@.end <= src.range@.start,

forall |i: usize| {
    src.vaddr <= i < src.vaddr + n
        ==> {
            &&& #[trigger] old(mem).addr_transl(i) is Some
            &&& old(mem).memory.contains_key(old(mem).addr_transl(i).unwrap())
            &&& old(mem).memory[old(mem).addr_transl(i).unwrap()] is Init

        }
},

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

        }
},

ensures

*mem == Self::memcpy_spec(*src, *dst, *old(mem), n),

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

The source and destination must not overlap. copy_nonoverlapping is semantically equivalent to C’s memcpy, but with the source and destination arguments swapped.

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

requires

vaddr != 0,

0 < len <= usize::MAX - vaddr,

ensures

r.is_valid(),

r.range@.start == vaddr,

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

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 struct This updates the ghost ranges to match a MemView::split operation

Trait Implementations§

impl Clone for VirtPtr

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

ensures

res == self,

1.0.0 · Source§

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

Performs copy-assignment from source. Read more

impl Inv for VirtPtr

open spec fn inv(self) -> bool

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

}

impl Copy for VirtPtr

Auto Trait Implementations§

impl UnwindSafe for VirtPtr

Blanket Implementations§

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

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

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

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

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

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

Mutably borrows from an owned value. Read more

impl<T> CloneToUninit for T
where T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

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

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

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

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T> ToOwned for T
where T: Clone,

type Owned = T

The resulting type after obtaining ownership.

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more

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

type Error = Infallible

The type returned in the event of a conversion error.

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

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where 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 for T
where U: TryFrom<T>,

type Error = >::Error

The type returned in the event of a conversion error.

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

Performs the conversion.

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

fn obeys_try_into_spec() -> bool