Attribute Macro verus_spec 

#[verus_spec]