Define a struct-level #[safety_constraint(...)] attribute

[adpaco-aws]

This PR defines a struct-level #[safety_constraint(<pred>)] macro attribute that allows users to define the type invariant as the predicate passed as an argument to the attribute. This safety constraint is picked up when deriving Arbitrary and Invariant implementations so that the values generated with any() or checked with is_safe() satisfy the constraint.

This attribute is similar to the helper attribute introduced in #3283, and they cannot be used together. It's preferable to use this attribute when the constraint implies some relation between different fields. But, at the moment, there's no practical difference between them because the helper attribute allows users to refer to any fields. If we imposed that restriction, this attribute would be the only way to specify struct-wide invariants.

An example:

#[derive(kani::Arbitrary)]
#[derive(kani::Invariant)]
#[safety_constraint(*x == *y)]
struct SameCoordsPoint {
    x: i32,
    y: i32,
}

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

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 Add a #[derive(Invariant)] macro #3250 and Enable an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros #3283). Here, Kani composes the struct invariant for the user.
2. Declare the invariant for the whole struct through a #[kani::invariant(...)] macro (see Define a struct-level #[safety_constraint(...)] attribute #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.

[adpaco-aws]

Marking this as ready for review after the last changes. This is now rebased on top of #3283 so we can take advantage of some of the functions included there.

A major change is that we now generate both the Arbitrary and the Invariant implementations from the #[kani::invariant(...)] macro. I made this change when working on the tests. That's when I realized that it didn't make sense to derive the Arbitrary implementation with #[derive(Arbitrary)] while using the #[kani::invariant(...)] attribute because the derived implementation wouldn't respect the type invariant.

For example, if we wrote something like this:

#[kani::invariant(*x >= 0 && *y >= 0)]
struct Point {
    x: i32,
    y: i32,
}

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

The harness would fail to verify because the value generated with kani::any() would not ensure *x >= 0 && *y >= 0. With the latest changes, this succeeds.

Aside from that change, I've added a few more tests and moved the code from derive.rs to lib.rs. The code could be moved to derive.rs again because we use a few functions from there, but it's not a problem to change that later.

[adpaco-aws]

This is ready for review again.

I have renamed the attribute and changed it so its behavior is very similar to the #[safety_constraint(...)] helper defined in #3283. The main difference w.r.t. the previous revision is that the attribute doesn't derive Arbitrary nor Invariant per se, but only modifies the behavior of the derive macros. In addition, I've refactored some code and added more tests as requested.

[zhassan-aws]

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.

[adpaco-aws]

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.

This is also a concern of mine, especially the second case where there isn't any feedback when using the attribute without deriving Arbitrary nor Invariant. I have tried exploring solutions to it this morning, and here's what I found out:

1. We would need to define this as a Kani attribute, even if it's only to trigger an error/warning. If I'm not mistaken, this implies that the attribute would become #[kani::safety_constraint(...)].
2. We would need to enforce the attribute being placed on top of the derive macros (not my preferred placement). That's because if the attribute is placed below them, it cannot tell if #[derive(...)] attributes have been specified because they will have already been expanded/processed. This is also not convenient since #[safety_constraint(...)] is currently a helper attribute and using it before the derive macros would trigger a warning (to be a hard error in the future):

warning: derive helper attribute is used before it is introduced
  --> src/main.rs:31:3
   |
31 | #[safety_constraint(x >= 0)]
   |   ^^^^^^^^^^^^^^^^^
32 | #[derive(kani::Arbitrary)]
   |          --------------- the attribute is introduced here
   |
   = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
   = note: for more information, see issue #79202 <https://github.com/rust-lang/rust/issues/79202>
   = note: `#[warn(legacy_derive_helpers)]` on by default

I believe the best option would be to generate some sort of marker from the derive macros. In other words, if we are generating an Arbitrary or Invariant implementation and find #[safety_constraint(...)], we should emit some information that lets us know if the attribute has been picked up by the derive macros. Then, in the macro for the attribute, we could just error out if the marker has not been found. However, I think that'd be out-of-scope for this PR so I've created #3396 to track it.

The rest of comments have been addressed.

[zhassan-aws]

Thanks!

I wonder if it's possible to check from a proc macro whether a type implements a trait.

[adpaco-aws]

I wonder if it's possible to check from a proc macro whether a type implements a trait.

As far as I know, there aren't great solutions to this because proc_macro operates at a syntactic level and doesn't have access to type information. That's because type-checking occurs during the actual compilation, which takes place after macro expansion.