Users should be able to create contracts suitable for verification but not stubbing

[celinval]

Requested feature: Enable contract verification for functions that Kani cannot use as stub today.
Use case: Verification of functions that return types that do not implement Arbitrary.
Link to relevant documentation (Rust reference, Nomicon, RFC):

Test case:

impl<T> NonNull<T> {
    pub unsafe fn as_ref<'a>(&self) -> &'a T { /* body */ }

Context

Kani today automatically synthesize the contract into a verification wrapper and a stub. The stub, however, rely on the fact that the return value, and the target for the modifies clauses, to implement Arbitrary trait. Thus, writing a simple contract for the example above would fail to compile.

Possible solution

As discussed with @JustusAdam, one possible solution is to create a new intrinsic for Kani, which tries to instantiate kani::any() for the return / modifies type. If the instantiation fails, we can trigger a compilation error. This will only fails if a harness tries to instantiate the generated stub.

[JustusAdam]

Since the intrinsic is only internal I want to propose the name conjure, because it evokes creation but also magic, which this is in a way given that it's only implementable with compiler magic.

I think you should include in the description that we would want to emit a warning though or perhaps fail at compile time if we find that conjure is reachable.

[celinval]

Unfortunately, the intrinsic will have to be marked as public with hidden documentation.