Add module-level #[phantom] attribute to simplify verification-only specifications

Currently definitions that are only meant to be used for specification and verification (not actual execution) can be annotated with the `#[phantom]` attribute to bypass some of Rust's compiler checks. For verification-only use cases, it would be nice to have a module-level annotation.