kani/
invariant.rs

1// Copyright Kani Contributors
2// SPDX-License-Identifier: Apache-2.0 OR MIT
3
4//! This module introduces the `Invariant` trait as well as its implementation
5//! for primitive types.
6
7/// This trait should be used to specify and check type safety invariants for a
8/// type. For type invariants, we refer to the definitions in the Rust's Unsafe
9/// Code Guidelines Reference:
10/// <https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#validity-and-safety-invariant>
11///
12/// In summary, the reference distinguishes two kinds of type invariants:
13///  - *Validity invariant*: An invariant that all data must uphold any time
14///    it's accessed or copied in a typed manner. This invariant is exploited by
15///    the compiler to perform optimizations.
16///  - *Safety invariant*: An invariant that safe code may assume all data to
17///    uphold. This invariant can be temporarily violated by unsafe code, but
18///    must always be upheld when interfacing with unknown safe code.
19///
20/// Therefore, validity invariants must be upheld at all times, while safety
21/// invariants only need to be upheld at the boundaries to safe code.
22///
23/// Safety invariants are particularly interesting for user-defined types, and
24/// the `Invariant` trait allows you to check them with Kani.
25///
26/// It can also be used in tests. It's a programmatic way to specify (in Rust)
27/// properties over your data types. Since it's written in Rust, it can be used
28/// for static and dynamic checking.
29///
30/// For example, let's say you're creating a type that represents a date:
31///
32/// ```rust
33/// #[derive(kani::Arbitrary)]
34/// pub struct MyDate {
35///   day: u8,
36///   month: u8,
37///   year: i64,
38/// }
39/// ```
40/// You can specify its safety invariant as:
41/// ```rust
42/// # #[derive(kani::Arbitrary)]
43/// # pub struct MyDate {
44/// #  day: u8,
45/// #  month: u8,
46/// #  year: i64,
47/// # }
48/// # fn days_in_month(_: i64, _: u8) -> u8 { 31 }
49///
50/// impl kani::Invariant for MyDate {
51///   fn is_safe(&self) -> bool {
52///     self.month > 0
53///       && self.month <= 12
54///       && self.day > 0
55///       && self.day <= days_in_month(self.year, self.month)
56///   }
57/// }
58/// ```
59/// And use it to check that your APIs are safe:
60/// ```no_run
61/// # use kani::Invariant;
62/// #
63/// # #[derive(kani::Arbitrary)]
64/// # pub struct MyDate {
65/// #  day: u8,
66/// #  month: u8,
67/// #  year: i64,
68/// # }
69/// #
70/// # fn days_in_month(_: i64, _: u8) -> u8 { todo!() }
71/// # fn increase_date(_: &mut MyDate, _: u8) { todo!() }
72/// #
73/// # impl Invariant for MyDate {
74/// #   fn is_safe(&self) -> bool {
75/// #     self.month > 0
76/// #       && self.month <= 12
77/// #       && self.day > 0
78/// #       && self.day <= days_in_month(self.year, self.month)
79/// #   }
80/// # }
81/// #
82/// #[kani::proof]
83/// fn check_increase_date() {
84///   let mut date: MyDate = kani::any();
85///   // Increase date by one day
86///   increase_date(&mut date, 1);
87///   assert!(date.is_safe());
88/// }
89/// ```
90pub trait Invariant
91where
92    Self: Sized,
93{
94    fn is_safe(&self) -> bool;
95}
96
97/// Any value is considered safe for the type
98macro_rules! trivial_invariant {
99    ( $type: ty ) => {
100        impl Invariant for $type {
101            #[inline(always)]
102            fn is_safe(&self) -> bool {
103                true
104            }
105        }
106    };
107}
108
109trivial_invariant!(u8);
110trivial_invariant!(u16);
111trivial_invariant!(u32);
112trivial_invariant!(u64);
113trivial_invariant!(u128);
114trivial_invariant!(usize);
115
116trivial_invariant!(i8);
117trivial_invariant!(i16);
118trivial_invariant!(i32);
119trivial_invariant!(i64);
120trivial_invariant!(i128);
121trivial_invariant!(isize);
122
123// We do not constrain the safety invariant for floating points types.
124// Users can create a new type wrapping the floating point type and define an
125// invariant that checks for NaN, infinite, or subnormal values.
126trivial_invariant!(f32);
127trivial_invariant!(f64);
128trivial_invariant!(f16);
129trivial_invariant!(f128);
130
131trivial_invariant!(());
132trivial_invariant!(bool);
133trivial_invariant!(char);
kani/invariant.rs

kani/
invariant.rs
