Merge pull request #1888 from verus-lang/exec-spec-contrib

Macro to compile spec structs/enums/fns to exec items

Author: zhengyao-lin