Attribute Macro vstd::prelude::ensures

#[ensures]