Macro creusot_contracts::macros::snapshot

snapshot!() { /* proc-macro */ }

Create a new Snapshot object.

The inside of snapshot may look like Rust code, but it is in fact pearlite.

Example

let mut x = 1;
let s = snapshot!(x);
x = 2;
proof_assert!(*s == 1i32);

snapshot! and ownership

Snapshots are used to talk about the logical value of an object, and as such they carry no ownership. This means that code like this is perfectly fine:

let v: Vec<i32> = vec![1, 2];
let s = snapshot!(v);
assert!(v[0] == 1); // ok, `s` does not have ownership of `v`
drop(v);
proof_assert!(s[0] == 1i32); // also ok!