The `#[safety_constraint(...)]` can be specified without deriving `Arbitrary` or `Invariant`

As @zhassan-aws originally posted in https://github.com/model-checking/kani/pull/3270#pullrequestreview-2206199274

> LGTM. The only thing I'm unsure about is that `Invariant` is not derived automatically when the attribute is specified. There's also no warning or error message if neither `Invariant` or `Arbitrary` is derived.
