Global verification conditions

[adpaco-aws]

Requested feature: Properties/Checks whose status depends on the status of other Kani properties/checks deserves a special section Kani's output. For example, the #[kani::should_panic] attribute could just be one of these, which we're calling "global conditions". This would allow us to keep a uniform UI to report their status and give feedback to users.
Use case: As mentioned, the #[kani::should_panic] attribute can be updated to be a global condition. Another one we have in mind is the option in #2299.
Link to relevant documentation (Rust reference, Nomicon, RFC): the #[kani::should_panic] attribute

Test case: N/A