Type invariants cause unsound contracts for unspecified functions

[xldenis]

When an external function has no contract, creusot might still add preconditions for type invariants. This interferes with the elaboration which adds requires { false } to those functions, resulting in an unsound contract.

An example is PartialEq::ne

cc @voidc

[voidc]

Why is this unsound? After all false /\ inv(arg) is still false.

[xldenis]

I'm seeing functions where there is no false though?

This is the contract generated for Ne when given no spec:

  val ne (self : self) (other : rhs) : bool
    requires {[#"/Users/xavier/.rustup/toolchains/nightly-2023-06-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/cmp.rs" 226 11 226 15] Inv0.inv self}
    requires {[#"/Users/xavier/.rustup/toolchains/nightly-2023-06-29-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/cmp.rs" 226 17 226 22] Inv1.inv other}
    ```
    
    

[voidc]

There seems to be a more general issue with extern functions. I tested this example:

pub fn test() {
    let mut v = vec![1, 2, 2, 3];
    v.dedup();
    proof_assert! { [email protected]() == 3 };
}

Since there is no extern spec for dedup, I would expect it to get a requires(false). However, the check ctx.externs.get(def_id.krate).is_some() fails because ctx.externs only contains direct dependencies of the current crate. dedup comes from the alloc crate which is a dep of std and thus not direct. The same issue occurs for items from core. I think the fix should be just removing the is_direct check.

[xldenis]

That's weird because it definitely used to work, though perhaps I never tested with transitive dependencies. Your explanation makes sense, I had figured it was because inv was being added and preventing the false check from passing.

[voidc]

Hmm, maybe something changed when updating the rustc version?