#[derive(Invariant)]
{
// Attributes available to this derive:
#[safety_constraint]
}
Expand description
Allow users to auto generate Invariant
implementations by using
#[derive(Invariant)]
macro.
§Type safety specification with the #[safety_constraint(...)]
attribute
When using #[derive(Invariant)]
on a struct, the
#[safety_constraint(<cond>)]
attribute can be added to either the struct
or its fields (but not both) to indicate a type safety invariant condition
<cond>
. This will ensure that the type-safety condition gets additionally
checked when using the is_safe()
method automatically generated by the
#[derive(Invariant)]
macro.
For example, the check_positive
harness in this code is expected to
fail:
#[derive(kani::Invariant)]
struct AlwaysPositive {
#[safety_constraint(*inner >= 0)]
inner: i32,
}
#[kani::proof]
fn check_positive() {
let val = AlwaysPositive { inner: -1 };
assert!(val.is_safe());
}
This is not too surprising since the type safety invariant that we indicated
is not being taken into account when we create the AlwaysPositive
object.
As mentioned, the is_safe()
methods generated by the
#[derive(Invariant)]
macro check the corresponding is_safe()
method for
each field in addition to any type safety invariants specified through the
#[safety_constraint(...)]
attribute.
For example, for the AlwaysPositive
struct from above, we will generate
the following implementation:
impl kani::Invariant for AlwaysPositive {
fn is_safe(&self) -> bool {
let obj = self;
let inner = &obj.inner;
true && *inner >= 0 && inner.is_safe()
}
}
Note: the assignments to obj
and inner
are made so that we can treat the
fields as if they were references.
§Adding #[safety_constraint(...)]
to the struct as opposed to its fields
As mentioned earlier, the #[safety_constraint(...)]
attribute can be added
to either the struct or its fields, but not to both. Adding the
#[safety_constraint(...)]
attribute to both the struct and its fields will
result in an error.
In practice, only one type of specification is need. If the condition for
the type safety invariant involves a relation between two or more struct
fields, the struct-level attribute should be used. Otherwise, using the
#[safety_constraint(...)]
is recommended since it helps with readability.
For example, if we were defining a custom vector MyVector
and wanted to
specify that the inner vector’s length is always less than or equal to its
capacity, we should do it as follows:
#[derive(Invariant)]
#[safety_constraint(vector.len() <= *capacity)]
struct MyVector<T> {
vector: Vec<T>,
capacity: usize,
}
However, if we were defining a struct whose fields are not related in any
way, we would prefer using the #[safety_constraint(...)]
attribute on its
fields:
#[derive(Invariant)]
struct PositivePoint {
#[safety_constraint(*x >= 0)]
x: i32,
#[safety_constraint(*y >= 0)]
y: i32,
}