Enable an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros

[adpaco-aws]

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

For the Invariant derive macro, this allows users to derive more sophisticated invariants for their data types by annotating individual named fields with the #[safety_constraint(<cond>)] attribute, where <cond> represents the predicate to be evaluated for the corresponding field. In addition, the implementation always checks #field.is_safe() for each field.

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 [safety_constraint(...)] attribute, we can achieve this without explicitly writing the impl Invariant for ... as follows:

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

For the Arbitrary derive macro, this allows users to derive more sophisticated kani::any() generators that respect the specified invariants. In other words, the kani::any() will assume any invariants specified through the #[safety_constraint(...)] attribute helper. Going back to the PositivePoint example, we'd expect this harness to be successful:

#[kani::proof]
fn check_invariant_helper_ok() {
    let pos_point: PositivePoint = kani::any();
    assert!(pos_point.x >= 0);
    assert!(pos_point.y >= 0);
}

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.

[celinval]

Nice! Can you please add a test where the invariant calls a function and one that tries to mutate the object? Thank you

[zhassan-aws]

Thanks. I find it a bit unexpected that #[derive(Arbitrary)] takes invariants from #[invariant] into account but not those from impl Invariant.

[zhassan-aws]

For example, what happens when the field type already has an Arbitrary implementation (e.g. char):

#[derive(Arbitrary)]
struct Foo {
    #[invariant(*c != 'X')]
    c: char,
    #[invariant(*i > 2)]
    i: i32,
}

Would the safety invariant of char still be maintained?

[zhassan-aws]

I would still prefer keeping the Arbitrary implementation independent of the invariants to prevent surprises (e.g. vacuous proofs). I understand this would require manually adding .is_safe() in many places, but it seems safer to me from the soundness perspective.

[adpaco-aws]

Update: On a separate discussion, we agreed on keeping the implementation as is while we ensure that the documentation communicates the danger of over-constraining values generated with kani::any() when using the #[safety_constraint(...)] (yes, we also agreed on a new name because #[invariant(...)] may give the impression that only works for the Invariant trait).

For the documentation, I've added it to the derive functions so that it's visible in the crates documentation. We could add another section to the "Reference" section of our documentation with this, but I don't know how we could keep them sync'd. We also ensure now that is_safe() gets called for each field regardless of whether they have the attribute or not.

[zhassan-aws]

Thanks. Do we check anywhere (or need to check) that the annotated field matches with the variable used in the predicate?

For example, does Kani error out in the following case?

struct Foo {
    #[safety_constraint(*y == 5)]
    x: i32,
    y: i32,
}

If not, perhaps the safety constraints can be added anywhere inside the struct and not necessarily annotated on the individual fields?

[adpaco-aws]

Thanks. Do we check anywhere (or need to check) that the annotated field matches with the variable used in the predicate?

We don't check the expressions for that. In my opinion, that'd be a nice feature to have but it's not needed at this point.

For example, does Kani error out in the following case?

struct Foo {
    #[safety_constraint(*y == 5)]
    x: i32,
    y: i32,
}

If not, perhaps the safety constraints can be added anywhere inside the struct and not necessarily annotated on the individual fields?

No, it doesn't error out. We could change it so the safety constraints can be added somewhere else but I don't know what's the advantage. Also, note that the feature in #3270 is expected to allow constraints relating multiple fields of the struct. But if we're talking about constraints associated to individual fields, I think this feature is more appropriate because the annotations are easier to read.

[celinval]

It looks good to me. Can you please add a test where all the attributes are guarded by kani configuration. I.e.: #[cfg_attr(kani, safety_attribute(/*content*/))].

Other tests that I would like to see is inadvertently specifying an expression with side effect, and mentioning other fields in the invariant expression. Thanks!

[celinval]

Thank you!!