vstd::prelude

Attribute Macro verus_spec

#[verus_spec]