Attribute Macro vstd::prelude::verus_verify

#[verus_verify]