Recursive definitions and invariant

[jhjourdan]

extern crate creusot_contracts;
use creusot_contracts::{*, invariant::{Invariant, inv}};

struct S { }

impl Invariant for S {
    #[predicate]
    #[open]
    fn invariant(self) -> bool {
        !inv(self)
    }
}

This leads to an absurd axiom.

Basically, we need to check that inv is not used (directly or not) in the definition of invariant.

Note that, for this reason, Why3 refuses recursive types with invariants:

use option.Option

type t = {
    x : option t
}
invariant { not (x = None) }

is refused by Why3.

Also, Why3 rejects the following:

use option.Option

type t 'a = {
    x : option 'a
}
invariant { not (x = None) }

type u = { y : t u }

By telling that u is not used in a strictly positive fashion in its definition (i.e., a type with an invariant has no strictly positive type parameters).

Depending on the solution we find for this bug, we may need to take into account those problems in Creusot too.

[voidc]

Good catch! The problem also exists with an invariant like forall<x: S> false. I'm not sure what the best way to fix this is.

[xldenis]

The solution @jhjourdan has proposed is to remove the implicit invariant assumption in quantifiers.