vstd::prelude

Attribute Macro verus_verify

#[verus_verify]