(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,66 @@
+// 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.
+///
+/// Note: Type safety might be checked automatically by Kani in the future.
+pub trait Invariant
+where
+    Self: Sized,
+{
+    fn is_safe(&self) -> bool;
+}
+
+impl Invariant for bool {
+    #[inline(always)]
+    fn is_safe(&self) -> bool {
+        let value = *self as u8;
+        value < 2
+    }
+}
+
+impl Invariant for char {
+    #[inline(always)]
+    fn is_safe(&self) -> bool {
+        let value = *self as u32;
+        value <= 0xD7FF || (0xE000..=0x10FFFF).contains(&value)
+    }
+}
+
+/// 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!(());

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 slice;
 pub mod tuple;
@@ -36,6 +37,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,62 @@
+// 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;
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_unsafe_char() {
+    let unsafe_char = unsafe { char::from_u32_unchecked(0x110000) };
+    assert!(unsafe_char.is_safe());
+}
+
+#[kani::proof]
+fn check_safe_char() {
+    let safe_char: char = kani::any();
+    assert!(safe_char.is_safe());
+}
+
+#[kani::proof]
+#[kani::should_panic]
+fn check_unsafe_bool() {
+    let unsafe_bool: bool = unsafe { std::mem::transmute(2_u8) };
+    assert!(unsafe_bool.is_safe());
+}
+
+#[kani::proof]
+fn check_safe_bool() {
+    let safe_bool: bool = kani::any();
+    assert!(safe_bool.is_safe());
+}
+
+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!(());
+}

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());
+}