"Closure" error in pearlite

[Armael]

It look like the closure syntax is allowed in pearlite!{} blocks to define Mappings, but when trying to use it in a proof_assert!{} I get an error from creusot.

#[logic]
#[ensures(true)]
fn foo() {
    proof_assert!{
        let f: Mapping<Int,Int> = { |k:Int| 42 };
        true
    };
}

raises the error Closure(path/to/file.rs)

[Armael]

Actually, proof_assert! looks like a red herring here. I'm getting the same issue with the following program:

#[logic]
#[ensures(true)]
fn foo() -> Seq<Int> { pearlite!{
    Seq::create(42, { |k:Int| 42 })
}}

[Armael]

Ah, the #[ensures(true)] seems to be required for the error to appear.

[xldenis]

Yes, the logic vcgenerator doesn't support closures.

[Armael]

I had assumed that adding contracts to a logical function simply generate a proof obligation of the form forall x y z. pre(x,y,z) ==> post(x,y,z,func(x,y,z)), which doesn't seem to require a specific VCgen as long as the definition of func is transparent. Is this not how it works? (and if so, why?)

[xldenis]

the VC it generates is a bit more complex than this, but that is the principle, the issue though is what happens if your closure contains a recursive call? what if it contains an expression with preconditions etc..

the current vc is extremely conservative.

[jhjourdan]

YEah, but we should really do something (even if stupid) with every language construct, including closures.