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_contracts::{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(self) -> Id

Get the id for this resource.

This prevents mixing resources of different origins.

(opaque)

pub fn id_ghost(&self) -> Id

Get the id for this resource.

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

terminates

ghost

ensures

result == self.id()

pub fn val(self) -> R

Get the RA element contained in this resource.

(opaque)

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

Create a new resource

Corresponding reasoning

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

terminates

ghost

ensures

result@ == *r

pub fn core(&self) -> Self

Duplicate the duplicable core of a resource

requires

self@.core() != None

ensures

result.id() == self.id()

ensures

Some(result@) == self@.core()

terminates

ghost

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, γ)

terminates

ghost

requires

R::incl_eq_op(*a, *b, self@)

ensures

result.0.id() == self.id() && result.1.id() == self.id()

ensures

result.0@ == *a

ensures

result.1@ == *b

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.

terminates

ghost

requires

R::incl_eq_op(*a, *b, self@)

ensures

result.0.id() == self.id() && result.1.id() == self.id()

ensures

result.0@ == *a && result.1@ == *b

ensures

(^result.0).id() == self.id() && (^result.1).id() == self.id() ==>
            (^self).id() == self.id() &&
            Some((^self)@) == (^result.0)@.op((^result.1)@)

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

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

terminates

ghost

requires

R::incl_eq_op(*r, *s, self@)

ensures

(^self).id() == self.id() && result.id() == self.id()

ensures

(^self)@ == *s

ensures

result@ == *r

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

Join two owned resources together.

See also [Self::join_mut] and Self::join_shared.

Corresponding reasoning

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

terminates

ghost

requires

self.id() == other.id()

ensures

result.id() == self.id()

ensures

Some(result@) == self@.op(other@)

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

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

terminates

ghost

requires

self.id() == other.id()

ensures

(^self).id() == self.id()

ensures

Some((^self)@) == self@.op(other@)

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, γ)

terminates

ghost

requires

self.id() == other.id()

ensures

result.id() == self.id()

ensures

self@.incl_eq(result@) && other@.incl_eq(result@)

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

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

terminates

ghost

requires

target.incl(self@)

ensures

(^self).id() == self.id()

ensures

(^self)@ == *target

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

Validate the composition of self and other.

terminates

ghost

requires

self.id() == other.id()

ensures

^self == *self

ensures

self@.op(other@) != None

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, γ)

terminates

ghost

requires

upd.premise(self@)

ensures

(^self).id() == self.id()

ensures

(^self)@ == upd.update(self@, *result)

Trait Implementations

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

fn view(self) -> R

(open, inline)

self.val()

type ViewTy = R