Attribute Macro vstd::prelude::decreases

#[decreases]