Struct Resource 

pub struct Resource<R>(/* private fields */);

A ghost wrapper around a resource algebra.

This structure is meant to be manipulated in ghost code.

The usual usage is this:

• Create some ghost resource
• Split it into multiple parts. This may be used to duplicate the resource if we have self.op(self) == self.
• Join these parts later. By exploiting validity of the combination, this allows one to learn information about one part from the other.

Example

use creusot_std::{ghost::resource::Resource, logic::ra::agree::Ag, prelude::*};
let mut res: Ghost<Resource<Ag<Int>>> = Resource::alloc(snapshot!(Ag(1)));

ghost! {
    let part = res.split_off(snapshot!(Ag(1)), snapshot!(Ag(1)));
    // Pass `part` around, forget what it contained...
    let _ = res.join_shared(&part);
    // And now we remember: the only way the above worked is if `part` contained `1`!
    proof_assert!(part@ == Ag(1));
};

Implementations

impl<R: RA> Resource<R>

pub fn id_ghost(&self) -> Id

Get the id for this resource.

This is the same as [Self::id], but for ghost code.

pub fn alloc(r: Snapshot<R>) -> Ghost<Self>

Create a new resource

Corresponding reasoning

⊢ |=> ∃γ, Own(value, γ)

pub fn new_unit(id: Id) -> Self

where R: UnitRA,

Create a unit resource for a given identifier

pub fn core(&self) -> Self

Duplicate the duplicable core of a resource

pub fn split(self, a: Snapshot<R>, b: Snapshot<R>) -> (Self, Self)

Split a resource into two parts, described by a and b.

See also Self::split_mut and Self::split_off.

Corresponding reasoning

⌜a = b ⋅ c⌝ ∧ Own(a, γ) ⊢ Own(b, γ) ∗ Own(c, γ)

pub fn split_mut( &mut self, a: Snapshot<R>, b: Snapshot<R>, ) -> (&mut Self, &mut Self)

Split a resource into two, and join it again once the mutable borrows are dropped.

pub fn split_off(&mut self, r: Snapshot<R>, s: Snapshot<R>) -> Self

Remove r from self and return it, leaving s in self.

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

Join two owned resources together.

See also Self::join_in and Self::join_shared.

Corresponding reasoning

⌜c = a ⋅ b⌝ ∗ Own(a, γ) ∗ Own(b, γ) ⊢ Own(c, γ)

pub fn join_in(&mut self, other: Self)

Same as Self::join, but put the result into self.

pub fn join_shared<'a>(&'a self, other: &'a Self) -> &'a Self

Join two shared resources together.

Corresponding reasoning

⌜a ≼ c⌝ ∧ ⌜b ≼ c⌝ ∧ Own(a, γ) ∧ Own(b, γ) ⊢ Own(c, γ)

pub fn weaken(&mut self, target: Snapshot<R>)

Transforms self into target, given that target is included in self.

pub fn valid_op_lemma(&mut self, other: &Self)

Validate the composition of self and other.

pub fn update<U: Update<R>>(&mut self, upd: U) -> Snapshot<U::Choice>

Perform an update.

Corresponding reasoning

⌜a ⇝ B⌝ ∧ Own(a, γ) ⊢ ∃b∈B, Own(b, γ)

impl<R: UnitRA> Resource<R>

pub fn take(&mut self) -> Self

Trait Implementations

impl<R: UnitRA> From<Resource<View<AuthViewRel<R>>>> for Fragment<R>

fn from(value: Resource<Auth<R>>) -> Self

Converts to this type from the input type.

impl<R: RA> View for Resource<R>

type ViewTy = R

impl<R> Send for Resource<R>