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.

logic

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

logic

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

logic

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

logic

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

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

logic(open, prophetic, inline)

&^*self

type Target = <T as Fin>::Target

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

Apply a ‘raw’ local update.

This will update the value of the authority/fragment to the provided pair.

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

logic(open, inline)

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)

logic(open, inline)

*self

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

logic

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

Apply a ‘raw’ non-deterministic update.

This changes the state of the resource to one of the values of the mapping, non-deterministically.

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

logic(open, inline)

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

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

logic(open, inline)

self[ch]

requires

self.premise(from)

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

logic

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = Choice

If the update is non-deterministic, it will pick a choice of this type for the update.

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

Apply a ‘raw’ update.

This changes the state of the resource from one value to another. The premise of this change is that no existing composition with the resource is invalidated.

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

logic(open, inline)

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

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

logic(open, inline)

*self

requires

self.premise(from)

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

logic

requires

self.premise(from)

requires

from.op(frame) != None

ensures

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

type Choice = ()

If the update is non-deterministic, it will pick a choice of this type for the update.

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