Skip to content

Commit

Permalink
(Re)introduce Invariant trait (rust-lang#3190)
Browse files Browse the repository at this point in the history
This PR reintroduces the `Invariant` trait as a mechanism for the
specification of type safety invariants. The trait is defined in the
Kani library where we also provide `Invariant` implementations for
primitive types.

In contrast to the previous `Invariant` trait, this version doesn't
require the `Arbitrary` bound (i.e., it has the same requirements as
`Arbitrary`). This way, the user isn't required to provide an
`Arbitrary` implementation in addition to the `Invariant` one.

Related rust-lang#3095
  • Loading branch information
adpaco-aws authored Jun 6, 2024
1 parent 9f4fc30 commit a6332fc
Show file tree
Hide file tree
Showing 5 changed files with 207 additions and 3 deletions.
6 changes: 3 additions & 3 deletions library/kani/src/arbitrary.rs
Original file line number Diff line number Diff line change
@@ -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},
Expand Down Expand Up @@ -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);
Expand Down
102 changes: 102 additions & 0 deletions library/kani/src/invariant.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,102 @@
// 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.
///
/// It can also be used in tests. It's a programmatic way to specify (in Rust)
/// properties over your data types. Since it's written in Rust, it can be used
/// for static and dynamic checking.
///
/// 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);
2 changes: 2 additions & 0 deletions library/kani/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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.
Expand Down
38 changes: 38 additions & 0 deletions tests/kani/Invariant/invariant_impls.rs
Original file line number Diff line number Diff line change
@@ -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);
}
62 changes: 62 additions & 0 deletions tests/kani/Invariant/percentage.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
// 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 Percentage {
pub fn try_new(val: u8) -> Result<Self, String> {
if val <= 100 {
Ok(Self(val))
} else {
Err(String::from("error: invalid percentage value"))
}
}

pub fn value(&self) -> u8 {
self.0
}

pub fn increase(&self, other: u8) -> Percentage {
let amount = self.0 + other;
Percentage::try_new(amount.min(100)).unwrap()
}
}

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.value() <= 100);
}

#[kani::proof]
#[kani::should_panic]
fn check_assert_safe() {
let percentage: Percentage = kani::any();
assert!(percentage.is_safe());
}

#[kani::proof]
fn check_increase_safe() {
let percentage: Percentage = kani::any();
kani::assume(percentage.is_safe());
let amount = kani::any();
kani::assume(amount <= 100);
let new_percentage = percentage.increase(amount);
assert!(new_percentage.is_safe());
}

0 comments on commit a6332fc

Please sign in to comment.