builtin_macros: skip VERUS_SPEC__ trait-method splitting for external traits

[Marti2203]

Fixes #783.

visit_item_trait_mut() unconditionally called visit_trait_items_prefilter(), which clones every trait method into a shadow VERUS_SPEC__<name> item (used to carry requires/ensures separately from the body for verification). This even applies to #[verifier::external] traits, which are never verified and whose items are entirely ignored by VIR construction anyway.

The generated clone always gets a default body ({ ::builtin::no_method_body() }), unlike the original declaration. For a method shaped like fn f() -> Self; (no receiver, Self-typed return, no body), that's a real behavioral difference: a bodyless trait method with an unsized return type compiles fine in real Rust, but the same signature WITH a body requires an explicit Self: Sized bound (confirmed directly against plain rustc). split_trait_method() already has a special case that adds that bound for a by-value self receiver, but not for this shape, so external traits with this pattern failed to compile with a spurious E0277, even though the user's own declaration was fine as written.

Fix: skip the trait-item prefilter/split entirely when the trait itself is marked #[verifier::external] (mirrors the existing is_external() guard used for unerased-proxy generation in unerased_proxies.rs).

Verified:

• new regression test issue_783_no_verus_spec_split_for_external_trait in rust_verify_test/tests/external_traits.rs (external trait with fn f() -> Self;); confirmed it fails with E0277 without the fix and passes with it
• vstd still verifies fully (2045 verified, 0 errors), unchanged
• full external_traits.rs suite passes (39/39)
• full traits.rs suite passes (214 passed, 0 failed, 2 ignored, matching the pre-existing baseline)

Assisted-by: Claude Code:claude-sonnet-5

_{By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.}