Closure inference (again)

[xldenis]

Adds support for inferring the specifications of closures through Coma's novel extspec mechanism.

Using this, you can exclude a contract for your closure and Creusot will instead infer its contract as roughly the WP and SP for the pre and post conditions respectively. I've updated some of our iterator tests to use this feature.

[jhjourdan]

I don't understand all the details, but I find quite suspicious that there is no special case here when postcond_kind is FnMut.

More generally, I would have expected to only generate the term when closure_kind is equal to postcond_kind, and rely on the various compatibility laws to let the provers deduce the other cases.

[xldenis]

That's because what matters here is mainly the underlying type of the closure:

• If it's FnOnce it cannot have an FnMut
• If its Fn then its FnMut instance ignores the result (since it must be equal to the initial parameter), this fact being provided by the compatibility law.

[jhjourdan]

this fact being provided by the compatibility law.

Well, then, why not relying fully on the compatibility law for the whole post-condition?

[arnaudgolfouse]

I tried using the branch, and ran into a crash. Here is a minimal example:

pub fn foo() {
    let my_closure = |x: Option<i32>| match x {
        Some(y) => y,
        None => unreachable!("unwrapped None"),
    };
}

This crashes with error: internal compiler error: compiler/rustc_middle/src/ty/mod.rs:1607:13: item_name: no name for DefPath { data: [DisambiguatedDefPathData { data: ValueNs("foo"), disambiguator: 0 }, DisambiguatedDefPathData { data: Closure, disambiguator: 0 }], krate: crate0 }. It seems some code is trying to fetch the name of the type of the closure from rustc (but it does not exists).

[xldenis]

Does that crash happen on master?

[arnaudgolfouse]

Yes, it does 😕

[arnaudgolfouse]

I tried using the branch, and ran into a crash. Here is a minimal example:

pub fn foo() {
    let my_closure = |x: Option<i32>| match x {
        Some(y) => y,
        None => unreachable!("unwrapped None"),
    };
}

This crashes with error: internal compiler error: compiler/rustc_middle/src/ty/mod.rs:1607:13: item_name: no name for DefPath { data: [DisambiguatedDefPathData { data: ValueNs("foo"), disambiguator: 0 }, DisambiguatedDefPathData { data: Closure, disambiguator: 0 }], krate: crate0 }. It seems some code is trying to fetch the name of the type of the closure from rustc (but it does not exists).

I opened #1312 to track this.

[arnaudgolfouse]

This is the second definition of self_, so this one can be removed (and the let mut csubst just below can be moved inside the if to avoid a borrow checker error)

[arnaudgolfouse]

Maybe related to @jhjourdan's remark: it seems code using spec inference with FnMut does not work:

extern crate creusot_contracts;
use creusot_contracts::*;

#[requires(f.precondition((2i32,)))]
#[ensures(exists<f_fin: F> f.postcondition_mut((2i32,), f_fin, result) && resolve(&f_fin))]
fn uses_closure_mut<F: FnMut(i32) -> i32>(mut f: F) -> i32 {
    f(2)
}

#[requires(f.precondition((2i32,)))]
#[ensures(f.postcondition((2i32,), result))]
fn uses_closure<F: Fn(i32) -> i32>(mut f: F) -> i32 {
    f(2)
}

fn foo() {
    let f = 
    // #[requires(x@ + 1 <= i32::MAX@)] // works with the explicit spec
    // #[ensures(result@ == x@ + 1)]
    |x| x + 1;

    let y = uses_closure_mut(f); // works with `uses_closure`
    assert!(y == 3);
}

The postcondition_mut'0 does not use the generated closure0'0'post predicate.

[xldenis]

ok I'm trying to get this passing but the creusot-contracts test won't pass and now I get:

 cargo test --test creusot-contracts
   Compiling creusot v0.3.0 (/Users/xavier/Code/creusot/creusot)
    Finished `test` profile [unoptimized + debuginfo] target(s) in 8.28s
     Running tests/creusot-contracts.rs (target/debug/deps/creusot_contracts-b4bcaa68001d2a7b)
Testing creusot-contracts ... failure
Error: Please run 'cargo creusot setup status' to diagnostic and fix the issue(s)
thread 'main' panicked at creusot/tests/creusot-contracts.rs:120:9:
output of creusot-contracts failed
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: test failed, to rerun pass `-p creusot --test creusot-contracts`

[jhjourdan]

Obvious question: have you tried to reset creusot's config ?

[xldenis]

Yea I tried via a new cargo creusot setup install, however it doesn't seem to work.

[jhjourdan]

Then @Armael , any idea where this could come from?

[xldenis]

ok I've gotten the tests building locally but I can't replicate the failure of CI on creusot-contracts. it seems to be complaining about uint64 being used instead of uint16?

[xldenis]

oof, it comes from the hash brown crate which does a cfg per architecture for SIMD reasons...

[xldenis]

@arnaudgolfouse can you update the tests using your computer?

[arnaudgolfouse]

Ok, I finally got to do that !

[arnaudgolfouse]

oof, it comes from the hash brown crate which does a cfg per architecture for SIMD reasons...

This (ideally) should not be visible to Creusot, no?

[xldenis]

This (ideally) should not be visible to Creusot, no?

I don't see how that can be avoided? The best thing would be to specify the target triple in the test suite so that we are all compiling proofs for x86-64.

[xldenis]

I'm going to go ahead and merge this and I'll work on the missing / broken cases separately.