Invariants on types behave in unexpected ways.

[f4z3r]

When using invariants on types, one would imagine the invariant to hold in all visible states. However, it seems that those invariants are only checked at function boundaries that involve the type. Therefore, performing an operation that is based on the invariant right after construction cannot be verified.

extern crate prusti_contracts;

#[invariant="self.0 >= 0"]
struct MyTuple(i32);

fn main() {
    let mut s = MyTuple(-1);        // no error is raised
    s.0 = -200;                     // still no error raised
    assert!(s.0 >= 0);              // error: "asserted expression might not hold"
}

The preceding example provides an error only on the assert!, the only statement that should actually verify. However, it doesn't complain about the object being in an invalid state, neither after construction, nor after direct modification.