Derive Macro Invariant

#[derive(Invariant)]
{
    // Attributes available to this derive:
    #[safety_constraint]
}

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,
}