Macro creusot_contracts::macros::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.

Example

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