ArrayPtr

vstd_extra::array_ptr

Struct ArrayPtr 

Source 
pub struct ArrayPtr<V, const N: usize> {
    pub addr: usize,
    pub index: usize,
    pub _type: PhantomData<[V; N]>,
}
Expand description

Concrete representation of a pointer to an array The length of the array is not stored in the pointer

Fields§

§addr: usize§index: usize§_type: PhantomData<[V; N]>

Implementations§

Source§

impl<V, const N: usize> ArrayPtr<V, N>

Source

pub exec fn addr(&self) -> usize

Impl: cast the pointer to an integer

Source

pub exec fn from_addr(addr: usize) -> res : Self

ensures
res.addr == addr,
res.index == 0,

Impl: cast an integer to the pointer

Source

pub exec fn add(self, off: usize) -> Self

requires
self.index + off <= N,
Source§

impl<V, const N: usize> ArrayPtr<V, N>

Source

pub exec fn empty() -> res : (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)

requires
layout::size_of::<[V; N]>() > 0,
ensures
res.1@.wf(),
res.1@.is_pptr(res.0),
res.1@.is_uninit_all(),
Source

pub exec fn make_as(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V)
where V: Copy,

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_uninit_all(),
ensures
perm.wf(),
perm.is_pptr(*self),
perm.is_init_all(),
forall |i: int| 0 <= i < N ==> perm.opt_value()[i] == raw_ptr::MemContents::Init(value),
Source

pub exec fn new(dft: V) -> res : (ArrayPtr<V, N>, Tracked<PointsTo<V, N>>)
where V: Copy,

requires
layout::size_of::<[V; N]>() > 0,
ensures
res.1@.wf(),
res.1@.is_pptr(res.0),
forall |i: int| {
    0 <= i < N ==> #[trigger] res.1@.opt_value()[i] == raw_ptr::MemContents::Init(dft)
},
Source

pub exec fn free(self, Tracked(perm): Tracked<PointsTo<V, N>>)

requires
perm.wf(),
perm.is_pptr(self),
perm.is_uninit_all(),
Source

pub exec fn insert(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>, value: V)

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_uninit(self.index as int),
self.index < N,
ensures
perm.wf(),
perm.is_pptr(*self),
perm.is_init(self.index as int),
forall |i: int| {
    0 <= i < N && i != self.index ==> perm.opt_value()[i] == old(perm).opt_value()[i]
},
perm.opt_value()[self.index as int] == raw_ptr::MemContents::Init(value),

Insert value at index The value is moved into the array. Requires the slot at index to be uninitialized.

Source

pub exec fn take_at(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> res : V
where V: Copy,

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_init(self.index as int),
self.index < N,
ensures
perm.wf(),
perm.is_pptr(*self),
perm.is_uninit(self.index as int),
forall |i: int| {
    0 <= i < N && i != self.index ==> perm.opt_value()[i] == old(perm).opt_value()[i]
},
res == old(perm).opt_value()[self.index as int].value(),

Take the value at index The value is moved out of the array. Requires the slot at index to be initialized. Afterwards, the slot is uninitialized.

Source

pub exec fn take_all(&self, Tracked(perm): Tracked<&mut PointsTo<V, N>>) -> res : [V; N]

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_init_all(),
ensures
perm.wf(),
perm.is_pptr(*self),
perm.is_uninit_all(),
res@ == old(perm).value(),

Take all the values of the array The values are moved out of the array. Requires all slots to be initialized. Afterwards, all slots are uninitialized.

Source

pub exec fn into_inner(self, Tracked(perm): Tracked<PointsTo<V, N>>) -> res : [V; N]

requires
perm.wf(),
perm.is_pptr(self),
perm.is_init_all(),
ensures
res@ == perm.value(),

Free the memory of the entire array and return the value that was previously stored in the array. Requires all slots to be initialized. Afterwards, all slots are uninitialized.

Source

pub exec fn update( &self, verus_tmp_perm: Tracked<&mut PointsTo<V, N>>, index: usize, value: V, ) -> res : V
where V: Copy,

requires
old(perm).wf(),
old(perm).is_pptr(*self),
old(perm).is_init(index as int),
index < N,
ensures
perm.wf(),
perm.is_pptr(*self),
perm.is_init(index as int),
forall |i: int| {
    0 <= i < N && i != index ==> perm.opt_value()[i] == old(perm).opt_value()[i]
},
perm.opt_value()[index as int] == raw_ptr::MemContents::Init(value),
res == old(perm).opt_value()[index as int].value(),

Update the value at index with value and return the previous value Requires the slot at index to be initialized. Afterwards, the slot is initialized with value. Returns the previous value.

Source

pub exec fn borrow_at<'a>( &self, verus_tmp_perm: Tracked<&'a PointsTo<V, N>>, index: usize, ) -> res : &'a V

requires
perm.wf(),
perm.is_pptr(*self),
perm.is_init(index as int),
index < N,
ensures
res == perm.opt_value()[index as int].value(),

Get the reference of the value at index Borrow the immutable reference of the value at index Requires the slot at index to be initialized. Afterwards, the slot is still initialized. Returns the immutable reference of the value. The reference is valid as long as the permission is alive. The reference is not allowed to be stored.

Source

pub exec fn borrow<'a>( &self, verus_tmp_perm: Tracked<&'a PointsTo<V, N>>, ) -> res : &'a [V; N]

requires
perm.wf(),
perm.is_pptr(*self),
perm.is_init_all(),
ensures
forall |i: int| 0 <= i < N ==> #[trigger] res[i] == perm.opt_value()[i].value(),

Get the reference of the entire array Borrow the immutable reference of the entire array Requires all slots to be initialized. Afterwards, all slots are still initialized. Returns the immutable reference of the entire array. The reference is valid as long as the permission is alive. The reference is not allowed to be stored.

Source

pub exec fn overwrite( &self, verus_tmp_perm: Tracked<&mut PointsTo<V, N>>, index: usize, value: V, )

requires
old(perm).wf(),
old(perm).is_pptr(*self),
index < N,
ensures
perm.wf(),
perm.is_pptr(*self),
perm.is_init(index as int),
forall |i: int| {
    0 <= i < N && i != index ==> perm.opt_value()[i] == old(perm).opt_value()[i]
},
perm.opt_value()[index as int] == raw_ptr::MemContents::Init(value),

Overwrite the entry at index with value The pervious value will be leaked if it was initialized.

Source

pub proof fn tracked_overwrite(tracked &self, tracked perm: &mut PointsTo<V, N>, tracked index: usize, tracked value: V, )

requires
old(perm).wf(),
old(perm).is_pptr(*self),
index < N,
ensures
perm.wf(),
perm.is_pptr(*self),
perm.is_init(index as int),
forall |i: int| {
    0 <= i < N && i != index ==> perm.opt_value()[i] == old(perm).opt_value()[i]
},
perm.opt_value()[index as int] == raw_ptr::MemContents::Init(value),
Source

pub exec fn get(&self, Tracked(perm): Tracked<&PointsTo<V, N>>, index: usize) -> res : V
where V: Copy,

requires
perm.wf(),
perm.is_pptr(*self),
perm.is_init(index as int),
index < N,
ensures
res == perm.opt_value()[index as int].value(),

Get the value at index and return it The value is copied from the array Requires the slot at index to be initialized. Afterwards, the slot is still initialized.

Trait Implementations§

Source§

impl<V, const N: usize> Clone for ArrayPtr<V, N>

Source§

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
Source§

impl<V, const N: usize> Copy for ArrayPtr<V, N>

Auto Trait Implementations§

§

impl<V, const N: usize> Freeze for ArrayPtr<V, N>

§

impl<V, const N: usize> RefUnwindSafe for ArrayPtr<V, N>
where V: RefUnwindSafe,

§

impl<V, const N: usize> Send for ArrayPtr<V, N>
where V: Send,

§

impl<V, const N: usize> Sync for ArrayPtr<V, N>
where V: Sync,

§

impl<V, const N: usize> Unpin for ArrayPtr<V, N>
where V: Unpin,

§

impl<V, const N: usize> UnwindSafe for ArrayPtr<V, N>
where V: UnwindSafe,

Blanket Implementations§

Source§

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

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

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

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

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

Source§

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

Mutably borrows from an owned value. Read more
Source§

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

Source§

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
Source§

impl<T> From<T> for T

Source§

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

Source§

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

Source§

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<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

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

Source§

type Owned = T

The resulting type after obtaining ownership.
Source§

fn to_owned(&self) -> T

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

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

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

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

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::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>

Source§

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

Source§

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

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::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<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

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