(Re)introduce Invariant trait

library/kani/src/arbitrary.rs

@@ -1,8 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-//! This module introduces the Arbitrary trait as well as implementation for primitive types and
-//! other std containers.
+//! This module introduces the `Arbitrary` trait as well as implementation for
+//! primitive types and other std containers.
 
 use std::{
     marker::{PhantomData, PhantomPinned},
@@ -66,7 +66,7 @@ trivial_arbitrary!(i64);
 trivial_arbitrary!(i128);
 trivial_arbitrary!(isize);
 
-// We do not constraint floating points values per type spec. Users must add assumptions to their
+// We do not constrain floating points values per type spec. Users must add assumptions to their
 // verification code if they want to eliminate NaN, infinite, or subnormal.
 trivial_arbitrary!(f32);
 trivial_arbitrary!(f64);

library/kani/src/invariant.rs

@@ -0,0 +1,97 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module introduces the `Invariant` trait as well as its implementation
+//! for primitive types.
+
+/// This trait should be used to specify and check type safety invariants for a
+/// type. For type invariants, we refer to the definitions in the Rust's Unsafe
+/// Code Guidelines Reference:
+/// <https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#validity-and-safety-invariant>
+///
+/// In summary, the reference distinguishes two kinds of type invariants:
+///  - *Validity invariant*: An invariant that all data must uphold any time
+///    it's accessed or copied in a typed manner. This invariant is exploited by
+///    the compiler to perform optimizations.
+///  - *Safety invariant*: An invariant that safe code may assume all data to
+///    uphold. This invariant can be temporarily violated by unsafe code, but
+///    must always be upheld when interfacing with unknown safe code.
+///
+/// Therefore, validity invariants must be upheld at all times, while safety
+/// invariants only need to be upheld at the boundaries to safe code.
+///
+/// Safety invariants are particularly interesting for user-defined types, and
+/// the `Invariant` trait allows you to check them with Kani. For example,
+/// let's say you're creating a type that represents a date:
+///
+/// ```rust
+/// #[derive(kani::Arbitrary)]
+/// pub struct MyDate {
+///   day: u8,
+///   month: u8,
+///   year: i64,
+/// }
+/// ```
+/// You can specify its safety invariant as:
+/// ```rust
+/// impl kani::Invariant for MyDate {
+///   fn is_safe(&self) -> bool {
+///     self.month > 0
+///       && self.month <= 12
+///       && self.day > 0
+///       && self.day <= days_in_month(self.year, self.month)
+///   }
+/// }
+/// ```
+/// And use it to check that your APIs are safe:
+/// ```rust
+/// #[kani::proof]
+/// fn check_increase_date() {
+///   let mut date: MyDate = kani::any();
+///   // Increase date by one day
+///   increase_date(date, 1);
+///   assert!(date.is_safe());
+/// }
+/// ```
+pub trait Invariant
+where
+    Self: Sized,
+{
+    fn is_safe(&self) -> bool;
+}
+
+/// Any value is considered safe for the type
+macro_rules! trivial_invariant {
+    ( $type: ty ) => {
+        impl Invariant for $type {
+            #[inline(always)]
+            fn is_safe(&self) -> bool {
+                true
+            }
+        }
+    };
+}
+
+trivial_invariant!(u8);
+trivial_invariant!(u16);
+trivial_invariant!(u32);
+trivial_invariant!(u64);
+trivial_invariant!(u128);
+trivial_invariant!(usize);
+
+trivial_invariant!(i8);
+trivial_invariant!(i16);
+trivial_invariant!(i32);
+trivial_invariant!(i64);
+trivial_invariant!(i128);
+trivial_invariant!(isize);
+
+// We do not constrain the safety invariant for floating points types.
+// Users can create a new type wrapping the floating point type and define an
+// invariant that checks for NaN, infinite, or subnormal values.
+trivial_invariant!(f32);
+trivial_invariant!(f64);
+
+trivial_invariant!(());
+trivial_invariant!(bool);
+trivial_invariant!(char);

library/kani/src/lib.rs

@@ -23,6 +23,7 @@ pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]
 mod concrete_playback;
 pub mod futures;
+pub mod invariant;
 pub mod mem;
 pub mod shadow;
 pub mod slice;
@@ -37,6 +38,7 @@ mod models;
 pub use arbitrary::Arbitrary;
 #[cfg(feature = "concrete_playback")]
 pub use concrete_playback::concrete_playback_run;
+pub use invariant::Invariant;
 
 #[cfg(not(feature = "concrete_playback"))]
 /// NOP `concrete_playback` for type checking during verification mode.

tests/kani/Invariant/invariant_impls.rs

@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check the `Invariant` implementations that we include in the Kani library
+//! with respect to the underlying type invariants.
+extern crate kani;
+use kani::Invariant;
+
+macro_rules! check_safe_type {
+    ( $type: ty ) => {
+        let value: $type = kani::any();
+        assert!(value.is_safe());
+    };
+}
+
+#[kani::proof]
+fn check_safe_impls() {
+    check_safe_type!(u8);
+    check_safe_type!(u16);
+    check_safe_type!(u32);
+    check_safe_type!(u64);
+    check_safe_type!(u128);
+    check_safe_type!(usize);
+
+    check_safe_type!(i8);
+    check_safe_type!(i16);
+    check_safe_type!(i32);
+    check_safe_type!(i64);
+    check_safe_type!(i128);
+    check_safe_type!(isize);
+
+    check_safe_type!(f32);
+    check_safe_type!(f64);
+
+    check_safe_type!(());
+    check_safe_type!(bool);
+    check_safe_type!(char);
+}

tests/kani/Invariant/percentage.rs

@@ -0,0 +1,33 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that the `Invariant` implementation behaves as expected when used on a
+//! custom type.
+
+extern crate kani;
+use kani::Invariant;
+
+// We use the default `Arbitrary` implementation, which allows values that
+// shouldn't be considered safe for the `Percentage` type.
+#[derive(kani::Arbitrary)]
+struct Percentage(u8);
+
+impl kani::Invariant for Percentage {
+    fn is_safe(&self) -> bool {
+        self.0 <= 100
+    }
+}
+
+#[kani::proof]
+fn check_assume_safe() {
+    let percentage: Percentage = kani::any();
+    kani::assume(percentage.is_safe());
+    assert!(percentage.0 <= 100);
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_assert_safe() {
+    let percentage: Percentage = kani::any();
+    assert!(percentage.is_safe());
+}