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

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:
```rs
#[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

tests/expected/safety-constraint-attribute/abstract-value/abstract-value.rs

@@ -0,0 +1,30 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+//! In this case, we test the attribute on a struct with a generic type `T`
+//! which requires the bound `From<i32>` because of the comparisons in the
+//! `#[safety_constraint(...)]` predicate. The struct represents an abstract
+//! value for which we only track its sign. The actual value is kept private.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint((*positive && *conc_value >= 0.into()) || (!*positive && *conc_value < 0.into()))]
+struct AbstractValue<T>
+where
+ T: PartialOrd + From<i32>,
+{
+ pub positive: bool,
+ conc_value: T,
+}
+
+#[kani::proof]
+fn check_abstract_value() {
+ let value: AbstractValue<i32> = kani::any();
+ assert!(value.is_safe());
+}

tests/expected/safety-constraint-attribute/abstract-value/expected

@@ -0,0 +1,7 @@
+Check 1: check_abstract_value.assertion.1\
+ - Status: SUCCESS\
+ - Description: "assertion failed: value.is_safe()"
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/safety-constraint-attribute/check-arbitrary/check-arbitrary.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint(*x >= 0 && *y >= 0)]
+struct Point {
+ x: i32,
+ y: i32,
+}
+
+#[kani::proof]
+fn check_arbitrary() {
+ let point: Point = kani::any();
+ assert!(point.x >= 0);
+ assert!(point.y >= 0);
+ assert!(point.is_safe());
+}

tests/expected/safety-constraint-attribute/check-arbitrary/expected

@@ -0,0 +1,11 @@
+Check 1: check_arbitrary.assertion.1\
+ - Status: SUCCESS\
+ - Description: "assertion failed: point.x >= 0"
+
+Check 2: check_arbitrary.assertion.2\
+ - Status: SUCCESS\
+ - Description: "assertion failed: point.y >= 0"
+
+Check 3: check_arbitrary.assertion.3\
+ - Status: SUCCESS\
+ - Description: "assertion failed: point.is_safe()"

tests/expected/safety-constraint-attribute/check-invariant/check-invariant.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+extern crate kani;
+use kani::Invariant;
+
+#[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());
+
+ // Assuming `point.x != point.y` here should be like assuming `false`.
+ // The assertion should be unreachable because we're blocking the path.
+ kani::assume(point.x != point.y);
+ assert!(false, "this assertion should be unreachable");
+}

tests/expected/safety-constraint-attribute/check-invariant/expected

@@ -0,0 +1,7 @@
+Check 1: check_invariant.assertion.1\
+ - Status: SUCCESS\
+ - Description: "assertion failed: point.is_safe()"
+
+Check 2: check_invariant.assertion.2\
+ - Status: UNREACHABLE\
+ - Description: ""this assertion should be unreachable""

tests/expected/safety-constraint-attribute/grade-example/expected

@@ -0,0 +1,11 @@
+Grade::check_percentage_safety.assertion.1\
+ - Status: SUCCESS\
+ - Description: "assertion failed: self.percentage <= 100"
+
+check_grade_safe.assertion.1\
+ - Status: SUCCESS\
+ - Description: "assertion failed: grade.is_safe()"
+
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/safety-constraint-attribute/grade-example/grade-example.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `#[safety_constraint(...)]` attribute works as expected when
+//! deriving `Arbitrary` and `Invariant` implementations.
+
+//! In this case, we test the attribute on a struct that represents a hybrid
+//! grade (letter-numerical) which should keep the following equivalences:
+//! - A for 90-100%
+//! - B for 80-89%
+//! - C for 70-79%
+//! - D for 60-69%
+//! - F for 0-59%
+//!
+//! In addition, we explicitly test that `percentage` is 0-100%
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(kani::Arbitrary)]
+#[derive(kani::Invariant)]
+#[safety_constraint((*letter == 'A' && *percentage >= 90 && *percentage <= 100) ||
+ (*letter == 'B' && *percentage >= 80 && *percentage < 90) ||
+ (*letter == 'C' && *percentage >= 70 && *percentage < 80) ||
+ (*letter == 'D' && *percentage >= 60 && *percentage < 70) ||
+ (*letter == 'F' && *percentage < 60))]
+struct Grade {
+ letter: char,
+ percentage: u32,
+}
+
+impl Grade {
+ pub fn check_percentage_safety(&self) {
+ assert!(self.percentage <= 100);
+ }
+}
+
+#[kani::proof]
+fn check_grade_safe() {
+ let grade: Grade = kani::any();
+ assert!(grade.is_safe());
+ grade.check_percentage_safety();
+}

tests/ui/safety-constraint-attribute/double-attribute/double-attribute.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the `#[safety_constraint(...)]`
+//! attribute is used more than once on the same struct.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(Invariant)]
+#[safety_constraint(*x >= 0)]
+#[safety_constraint(*y >= 0)]
+struct Point {
+ x: i32,
+ y: i32,
+}

tests/ui/safety-constraint-attribute/double-attribute/expected

@@ -0,0 +1,6 @@
+error: Cannot derive `Invariant` for `Point`
+ |
+| #[derive(Invariant)]
+ | ^^^^^^^^^
+ |
+note: `#[safety_constraint(...)]` cannot be used more than once.

tests/ui/safety-constraint-attribute/invalid-pred-error/expected

@@ -0,0 +1,19 @@
+error[E0308]: mismatched types
+ |
+| #[safety_constraint(x >= 0 && y >= 0)]
+ | ^ expected `&i32`, found integer
+ |
+help: consider dereferencing the borrow
+ |
+| #[safety_constraint(*x >= 0 && y >= 0)]
+ | +
+
+error[E0308]: mismatched types
+ |
+| #[safety_constraint(x >= 0 && y >= 0)]
+ | ^ expected `&i32`, found integer
+ |
+help: consider dereferencing the borrow
+ |
+| #[safety_constraint(x >= 0 && *y >= 0)]
+ |

tests/ui/safety-constraint-attribute/invalid-pred-error/invalid-pred-error.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the predicate passed to the
+//! `#[safety_constraint(...)]` attribute would result in a compiler error.
+//!
+//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error,
+//! otherwise the `#[safety_constraint(...)]` attribute is ignored.
+
+extern crate kani;
+
+// Note: The struct fields `x` and `y` are references in this context, we should
+// refer to `*x` and `*y` instead.
+#[derive(kani::Invariant)]
+#[safety_constraint(x >= 0 && y >= 0)]
+struct Point {
+ x: i32,
+ y: i32,
+}

tests/ui/safety-constraint-attribute/mixed-attributes/expected

@@ -0,0 +1,6 @@
+error: Cannot derive `Invariant` for `Point`
+ |
+| #[derive(Invariant)]
+ | ^^^^^^^^^
+ |
+note: `#[safety_constraint(...)]` cannot be used in struct and its fields simultaneously

tests/ui/safety-constraint-attribute/mixed-attributes/mixed-attributes.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that there is a compilation error when the `#[safety_constraint(...)]`
+//! attribute for struct and the `#[safety_constraint(...)]` attribute for
+//! fields is used at the same time.
+
+extern crate kani;
+use kani::Invariant;
+
+#[derive(Invariant)]
+#[safety_constraint(*x >= 0)]
+struct Point {
+ x: i32,
+ #[safety_constraint(*y >= 0)]
+ y: i32,
+}

tests/ui/safety-constraint-attribute/no-struct-error/expected

@@ -0,0 +1,6 @@
+error: Cannot derive `Invariant` for `MyEnum`
+ |
+| #[derive(kani::Invariant)]
+ | ^^^^^^^^^^^^^^^
+ |
+note: `#[safety_constraint(...)]` can only be used in structs

tests/ui/safety-constraint-attribute/no-struct-error/no-struct-error.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that Kani raises an error when a derive macro with the
+//! `#[safety_constraint(...)]` attribute is is used in items which are not a
+//! struct.
+//!
+//! Note: the `#[derive(kani::Invariant)]` macro is required for the compiler error,
+//! otherwise the `#[safety_constraint(...)]` attribute is ignored.
+
+extern crate kani;
+
+#[derive(kani::Invariant)]
+#[safety_constraint(true)]
+enum MyEnum {
+ A,
+ B(i32),
+}