#[open] functions and termination

[arnaudgolfouse]

It would be nice to special-case #[open] logical functions during the termination check. To see why, consider the following example:

pub trait Tr: Sized {
    #[logic]
    fn property(self) -> Int;

    #[logic]
    #[requires(bar(self))]
    fn foo(self);
}

#[logic]
#[open]
pub fn bar<T: Tr>(x: T) -> bool {
    x.property() == 42
}

impl Tr for () {
    #[logic]
    #[open]
    fn property(self) -> Int { 1 }

    #[logic]
    #[open]
    #[requires(bar(self))]
    fn foo(self) {}
}

Creusot reject this:

error: Mutually recursive functions: when calling `<() as Tr>::foo`...
  --> test.rs:29:5
   |
29 |     fn foo(self) {}
   |     ^^^^^^^^^^^^
   |
note: then `<() as Tr>::foo` might call `<() as Tr>::foo` via the call to `bar`.
  --> test.rs:28:16
   |
28 |     #[requires(bar(self))]
   |                ^^^^^^^^^

And, well, it is right to: bar is asking for an implementation of <() as Tr>, which we are in the process of defining.

But the function is open... So it would make sense to have its callers 'see' that it only calls specific functions, and not the whole implementation.

[jhjourdan]

Agreed. I think we already discussed this, but I'm not sure we wrote an issue about this.