Struct Snapshot 

pub struct Snapshot<T: ?Sized>(/* private fields */);

A copyable snapshot, usable in pearlite.

The Snapshot type contains the logical value of some data, in a purely immutable way. It is zero sized.

Creating a snapshot does not move the ownership of a value.

Pearlite syntax

In executable code, you may create a snapshot with the snapshot! macro. Inside this macro, you may write pearlite code; this code will not run during the normal execution of the program.

Example

let x: Snapshot<Int> = snapshot!(1);
let m: Snapshot<Mapping<Int, Int>> = snapshot!(|x| x + 1);

Implementations

impl<T: ?Sized> Snapshot<T>

pub fn new(value: T) -> Snapshot<T>

Create a new snapshot in logic code.

impl<T> Snapshot<T>

pub fn inner(self) -> T

Get the value of the snapshot.

When possible, you should instead use the dereference operator.

Example

let x = snapshot!(1);
proof_assert!(x.inner() == 1);
proof_assert!(*x == 1); // prefer this

pub fn into_ghost(self) -> Ghost<T>

where T: Plain,

Extract a plain value from a snapshot in ghost code.

ensures

*result == *self

terminates

ghost

Trait Implementations

impl<T: ?Sized> Clone for Snapshot<T>

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<T: ?Sized> Deref for Snapshot<T>

Available on creusot only.

fn deref(&self) -> &Self::Target

type Target = T

The resulting type after dereferencing.

impl<T: ?Sized> DerefMut for Snapshot<T>

Available on creusot only.

fn deref_mut(&mut self) -> &mut Self::Target

impl<T: ?Sized + Fin> Fin for Snapshot<T>

fn fin<'a>(self) -> &'a Self::Target

(open, prophetic, inline)

pearlite! { &^*self }

type Target = <T as Fin>::Target

impl<R: RA> LocalUpdate<R> for Snapshot<(R, R)>

fn premise(self, from_auth: R, from_frag: R) -> bool

(open)

pearlite! {
    forall<f: Option<R>>
        Some(from_frag).op(f) == Some(Some(from_auth)) ==>
        Some(self.1).op(f) == Some(Some(self.0))
}

fn update(self, _: R, _: R) -> (R, R)

(open)

*self

fn frame_preserving(self, from_auth: R, from_frag: R, frame: Option<R>)

requires

LocalUpdate::premise(self, from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = LocalUpdate::update(self, from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))

impl<R: RA, Choice> Update<R> for Snapshot<Mapping<Choice, R>>

fn premise(self, from: R) -> bool

(open)

pearlite! {
    forall<y: R> from.op(y) != None ==>
        exists<ch: Choice> self[ch].op(y) != None
}

fn update(self, from: R, ch: Choice) -> R

(open)

self[ch]

requires

self.premise(from)

fn frame_preserving(self, from: R, frame: R) -> Choice

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = Choice

impl<R: RA> Update<R> for Snapshot<R>

fn premise(self, from: R) -> bool

(open)

pearlite! {
    forall<y: R> from.op(y) != None ==> self.op(y) != None
}

fn update(self, from: R, _: ()) -> R

(open)

*self

requires

self.premise(from)

fn frame_preserving(self, from: R, frame: R)

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = ()

impl<T: ?Sized> Copy for Snapshot<T>