Type Invariants

Overview

Defining a type invariant allows you to constrain a data type's set of valid values with a logical predicate that all values must satisfy. During verification, Creusot enforces that all type invariants are preserved across functions. Inside a function, values subject to type invariants may temporarily break their invariants as long as each value's invariant is restored before the value can be observed by another function.

Type invariants were added to Creusot as part of a Master's thesis available here.

Defining Type Invariants

To attach an invariant to a type, you implement the Invariant trait provided by Creusot. Here is an example:

#![allow(unused)]
fn main() {
struct SumTo10 {
    a: i32,
    b: i32,
}

// The type invariant constrains the set of valid `SumTo10`s to
// only allow values where the sum of both fields is equal to 10.
impl Invariant for SumTo10 {
    #[predicate]
    fn invariant(self) -> bool {
        pearlite! {
            self.a@ + self.b@ == 10
        }
    }
}
}

Enforcement of Type Invariants

Creusot enforces type invariants on function boundaries by generating additional pre- and postconditions based on the types of a function's arguments and return value. The type invariants of a function’s arguments are treated as additional preconditions and a type invariant of the return value corresponds to an extra postcondition. Here is an example:

#![allow(unused)]
fn main() {
// `inv` generically refers to the invariant of some value
#[requires(inv(x))] // generated by Creusot
#[ensures(inv(result))] // generated by Creusot
fn foo(x: SumTo10) -> SumTo10 {
    x
}
}

These generated pre- and postconditions require you to prove the invariants of any values used as arguments in function calls or returned values. Besides the proof obligations at function boundaries, you must also prove the type invariants of mutably borrowed values when the lifetimes of the created references end. When creating a mutable reference r, Creusot requires you to prove the type invariant of its current value at the end of r's lifetime, since r might have been used to break the invariant of the borrowed value. This lets Creusot assume the invariant of the final value ^r holds, simplifying the reasoning about mutable references. Here is an example:

#![allow(unused)]
fn main() {
fn swap() {
    let mut s = SumTo10 { a: 3, b: 7 }
    let r = &mut s;
    // Creusot can prophetically assume inv(^r) holds:
    proof_assert! { inv(^r) };

    let tmp = r.a;
    *r.a = r.b;
    *r.b = tmp;
    // The lifetime of r ends: We must prove inv(*r)

    proof_assert! { inv(v) }; // provable since v = ^r = *r
}
}

Structural Invariants

To determine the invariant of a particular type, Creusot considers both whether the user provided an explicit definition through the Invariant trait, as well as any invariants the can be derived automatically based on the type's definition. We call those automatically derived invariants structural invariants. When neither an explicit definition exists, nor a structural invariant, the type has the trivial invariant, which does not impose any constraints on the set of valid values.

Here are some examples demonstrating structural invariants of various types: