Struct creusot_contracts::snapshot::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

pub fn inner(self) -> T

where T: Sized,

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

Trait Implementations

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

fn clone(&self) -> Self

pure

ensures

result == *self

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

Performs copy-assignment from source.

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

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

logic

type Target = T

The resulting type after dereferencing.

impl<T> IndexLogic<Int> for Snapshot<Seq<T>>

fn index_logic(self, ix: Int) -> Self::Item

logic

pearlite! { (*self)[ix] }

type Item = T

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

fn view(self) -> Self::ViewTy

logic

pearlite! { self.deref().view() }

type ViewTy = <T as View>::ViewTy

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