Skip to main content

Resource

vstd::resource::algebra

Struct Resource 

Source 
pub struct Resource<RA: ResourceAlgebra> { /* private fields */ }
Expand description

Interface for Resource Algebra ghost state.

Implementations§

Source§

impl<RA: ResourceAlgebra> Resource<RA>

Source

pub proof fn as_ref(tracked &self) -> tracked r : ResourceRef<'_, RA>

ensures
self.loc() == r.loc(),
self.value() == r.value(),
Source§

impl<RA: ResourceAlgebra> Resource<RA>

Implementation of a Resource based on a ResourceAlgebra

Source

pub closed spec fn value(self) -> RA

The underlying value of the resource

Source

pub closed spec fn loc(self) -> Loc

The location of the resource

Source

pub proof fn alloc(value: RA) -> tracked out : Self

requires
value.valid(),
ensures
out.value() == value,

Allocate a new resource at a fresh location

Source

pub proof fn join(tracked self, tracked other: Self) -> tracked out : Self

requires
self.loc() == other.loc(),
ensures
out.loc() == self.loc(),
out.value() == RA::op(self.value(), other.value()),

We can join together two resources at the same location, where we obtain the combination of the two

Source

pub proof fn split(tracked self, left: RA, right: RA) -> tracked out : (Self, Self)

requires
self.value() == RA::op(left, right),
ensures
out.0.loc() == self.loc(),
out.1.loc() == self.loc(),
out.0.value() == left,
out.1.value() == right,

If a resource holds the result of a composition, we can split it into the components

Source

pub proof fn validate(tracked &self)

ensures
self.value().valid(),

Whenever we have a resource, that resource is valid. This intuitively (and inductively) holds because: 1. We only create valid resources (via alloc); 2. We can only update the value of a resource via a frame_preserving_update_opt (see update for more details. Because of the requirement of that updates are frame preserving this means that joins remain valid.

Source

pub proof fn update_nondeterministic(tracked self, new_values: Set<RA>) -> tracked out : Self

requires
frame_preserving_update_nondeterministic_opt(self.value(), new_values),
ensures
out.loc() == self.loc(),
new_values.contains(out.value()),

This is a more general version of update.

Source

pub proof fn update(tracked self, new_value: RA) -> tracked out : Self

requires
frame_preserving_update_opt(self.value(), new_value),
ensures
out.loc() == self.loc(),
out.value() == new_value,

Update a resource to a new value. This can only be done if the update is frame preserving (i.e., any value that could be composed with the original value can still be composed with the new value).

See frame_preserving_update for more information.

Source

pub proof fn extract(tracked &mut self) -> tracked other : Self

ensures
other.loc() == old(self).loc(),
other.value() == old(self).value(),

Extracts the resource from r, leaving r unspecified and returning a new resource holding the previous value of r.

Source

pub proof fn validate_2(tracked &mut self, tracked other: &ResourceRef<'_, RA>)

requires
old(self).loc() == other.loc(),
ensures
*self == *old(self),
RA::op(self.value(), other.value()).valid(),

Validate two items at once. If we have two resources at the same location then its composition is valid.

Source

pub proof fn update_nondeterministic_with_shared(tracked self, tracked other: &ResourceRef<'_, RA>, new_values: Set<RA>, ) -> tracked out : Self

requires
self.loc() == other.loc(),
frame_preserving_update_nondeterministic_opt(
    RA::op(self.value(), other.value()),
    set_op(new_values, other.value()),
),
ensures
out.loc() == self.loc(),
new_values.contains(out.value()),

We can do a similar update to update_with_shared for non-deterministic updates

Source

pub proof fn update_with_shared(tracked self, tracked other: &ResourceRef<'_, RA>, new_value: RA, ) -> tracked out : Self

requires
self.loc() == other.loc(),
frame_preserving_update_opt(
    RA::op(self.value(), other.value()),
    RA::op(new_value, other.value()),
),
ensures
out.loc() == self.loc(),
out.value() == new_value,

If x · y --> x · z is a frame-perserving update, and we have a shared reference to x, we can update the y resource to z.

Auto Trait Implementations§

§

impl<RA> Freeze for Resource<RA>

§

impl<RA> RefUnwindSafe for Resource<RA>
where RA: RefUnwindSafe,

§

impl<RA> Send for Resource<RA>
where RA: Send,

§

impl<RA> Sync for Resource<RA>
where RA: Sync,

§

impl<RA> Unpin for Resource<RA>
where RA: Unpin,

§

impl<RA> UnsafeUnpin for Resource<RA>

§

impl<RA> UnwindSafe for Resource<RA>
where RA: 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> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

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

Source§

exec fn obeys_from_spec() -> bool

Source§

exec 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.

Source§

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

Source§

exec fn obeys_into_spec() -> bool

Source§

exec fn into_spec(self) -> T

Source§

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

Source§

open spec fn obeys_into_spec() -> bool

{ <U as FromSpec<Self>>::obeys_from_spec() }
Source§

open spec fn into_spec(self) -> U

{ U::from_spec(self) }
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.
Source§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

Source§

exec fn obeys_try_from_spec() -> bool

Source§

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

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

Source§

exec fn obeys_try_into_spec() -> bool

Source§

exec fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

Source§

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

Source§

open spec fn obeys_try_into_spec() -> bool

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }
Source§

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

{ <U as TryFromSpec<Self>>::try_from_spec(self) }