Attribute Macro vstd::prelude::invariant

#[invariant]