(Re)introduce Invariant trait

library/kani/src/invariant.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module introduces the Invariant trait.
+
+/// This trait should be used to specify and check type safety invariants for a
+/// type.
+pub trait Invariant
+where
+    Self: Sized,
+{
+    fn is_valid(&self) -> bool;
+}

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.