Attribute Macro verus_enum_synthesize

#[verus_enum_synthesize]