Macro proof_assert 

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

Inserts a logical assertion into the code

This assertion will not be checked at runtime but only during proofs. However, it can use pearlite syntax.

You can also use the #[trusted] attribute to disable checking a proof_assert!, so it becomes a trusted assumption for the rest of the function.

Example

let x = 1;
let v = vec![x, 2];
let s = snapshot!(v);
proof_assert!(s[0] == 1i32);