Struct Guarded 

#[repr(transparent)]
pub struct Guarded<T, G: Guard<T>> {
    pub inner: T,
    /* private fields */
}

Guarded is a wrapper around an object of type T, which makes sure that a guard (a predicate on T) is satisfied when the guarded object disappears. It works by making the guard part of the type invariant of Guarded, and uses some internal Creusot machinery to ensure that the guard never changes during the lifetime of the Guarded object.

As such, the guard can be broken locally, but it must be restored before the Guarded object is dropped, passed as a parameter, returned or when a borrow of the Guarded is resolved.

The guard is represented by a value guard: G whose type implements the trait Guard<T>. The relation guard.guards(inner, initial) is the property that must be satisfied when the guarded object disappears, where inner is the current value of the guarded object, and initial is its initial value when the Guarded object is created. The initial value is used to guarantee that the guarded object is not replaced with another (it may be mutated, but not replaced with another) using e.g., std::mem::swap.

Guarded is typically used with a T mutable borrow. In this case, Guard<&mut T> guarantees that the prophecies never change, and the guard typically guarantees that the final value of the borrow satisfies some property. Other uses include types that behave like mutable borrows, such as FullBorrow.

Example

use creusot_std::prelude::*;
use creusot_std::invariant::Guarded;

#[ensures(^b == 0i32)]
fn breaks_inv(b: &mut i32) { *b = 0; }

let mut x = 1;
let guarded = Guarded::new_m(&mut x, snapshot!(|x: i32| x == 1i32));
// break the guard...
breaks_inv(&mut *guarded.inner);
// but restore it before we are done
*guarded.inner = 1;

Fields

inner: T

Payload of this Guarded value.

Implementations

impl<T, G: Guard<T>> Guarded<T, G>

pub fn guard(self) -> G

logic(open, inline)

*self._guard

impl<'a, T, G: GuardRef<T>> Guarded<&'a mut T, G>

pub fn new(borrow: &'a mut T, guard: Snapshot<G>) -> Self

Create a new guarded borrow.

The borrow contained in the result is guaranteed to satisfy the guard at the end of its lifetime. Thus, we get the guard for its prophecy.

Note that the type of the second argument may not be inferred during compilation with rustc if it is directly constructed using the snapshot! macro. You may want to spell out the first type argument of Guarded, or use Guarded::new_m if the guard is a Mapping.

requires

guard.guards_ref(*borrow)

ensures

result.inner == borrow

ensures

result.guard() == *guard

ensures

guard.guards_ref(^borrow)

ghost

impl<'a, T> Guarded<&'a mut T, Mapping<T, bool>>

pub fn new_m(borrow: &'a mut T, guard: Snapshot<Mapping<T, bool>>) -> Self

Variant of Guarded::new specialized with Mapping as the guard.

requires

guard.guards_ref(*borrow)

ensures

result.inner == borrow

ensures

result.guard() == *guard

ensures

guard.guards_ref(^borrow)

ghost

impl<'a, T> Guarded<&'a mut Option<T>, IsSome>

pub fn some(borrow: Ghost<&'a mut T>) -> Ghost<Self>

ghost

ensures

*result.inner == Some(**borrow)

ensures

^result.inner == Some(^borrow)

Trait Implementations

impl<T, G: Guard<T>> Invariant for Guarded<T, G>

fn invariant(self) -> bool

logic(open, prophetic, inline)

(*self._guard).guards(*self._initial, self.inner)