Enable an `#[invariant(...)]` attribute helper for the `#[derive(Invariant)]` macro

[adpaco-aws]

This PR enables an #[invariant(...)] attribute helper for the #[derive(Invariant)] macro.

This allows users to derive more sophisticated invariants for their data types by annotating individual named fields with the #[invariant(<cond>)] attribute, where <cond> represents the predicate to be evaluated for the corresponding field. If the attribute is not provided, the implementation falls back to the default self.#field.is_safe() call.

For example, let's say we are working with the Point type from #3250

#[derive(kani::Invariant)]
struct Point<X, Y> {
    x: X,
    y: Y,
}

and we need to extend it to only allow positive values for both x and y. With the [invariant(...)] attribute, we can achieve this without explicitly writing the impl Invariant for ... as follows:

#[derive(kani::Invariant)]
struct PositivePoint {
    #[invariant(self.x >= 0)]
    x: i32,
    #[invariant(self.y >= 0)]
    y: i32,
}

The PR includes tests to ensure it's working as expected, in addition to UI tests checking for cases where the arguments provided to the macro are incorrect. Happy to add any other cases that you feel are missing.

Related #3095

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

[celinval]

Quick question... wouldn't it make sense to also parse this helper in the #[derive(Arbitrary)] macro?

[adpaco-aws]

I'm not sure about that. How would users create an unsafe value then? This isn't clear to me and I think it's a use-case we should continue to support.

To me, it'd make more sense to have another API kani::any_safe() which combines let x = kani::any()and kani::assume(x.is_safe()) (no need to replicate the parsing code). This way, the code would be explicit about the "safe values" assumption, which I don't think is clear otherwise.

[celinval]

kani::any() is a safe function and it should only return safe values. Anything beyond that is incorrect.