Define a `kani::invariant` attribute

[adpaco-aws]

This PR defines a #[kani::invariant(<pred>)] macro attribute that allows users to define the type invariant as the predicate passed as an argument to the attribute. This relieves users from writing the whole impl kani::Invariant ... for their types and helps keep the type and its invariant as close as possible.

An example:

#[derive(kani::Arbitrary)]
#[kani::invariant(self.x.is_safe() && self.y.is_safe())]
struct Point {
    x: i32,
    y: i32,
}

#[kani::proof]
fn check_invariant() {
    let point: Point = kani::any();
    assert!(point.is_safe());
}

Keeping this as a draft while we:

• Handle cases that I didn't initially anticipate (e.g., what happens with two kani::invariant annotations?).
• ~Extend its functionality a little more (I'd like to check if we can use helper attributes to directly define the invariants on fields) or discuss other features to be implemented now or later.~
• Fix other trivial issues like code placement.

Resolves #3095

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[adpaco-aws]

I've decided to add the helper attribute #[invariant(..)] in #3283 because it makes more sense to have it be part of the #[derive(Invariant)] macro than this one. So I'm hoping to give our users three options:

1. Derive the Invariant implementation through the derive macro, adding #[invariant(..)] to fields which require stronger invariants (see #3250 and #3283). Here, Kani composes the struct invariant for the user.
2. Declare the invariant for the whole struct through a #[kani::invariant(...)] macro (see #3270). Here, Kani just embeds the condition you pass it.
3. Write the implementation for Invariant explicitly.

Therefore, this PR only needs a little better error handling (we should parse expressions like we're doing in #3283) and some cleanup.