Warn when declaring variables, parameters, and return values with a type with an incompatible mode

[utaal]

From #167

E.g.

fn myfun(map: Map<i32, i32>)

where map is exec, but Map's constructor is restricted to spec.

---

#167 (comment)

Should we also make it an error to use Map (and other spec/proof-only types) as an exec variable in the first place?

#167 (comment)

Ultimately, the error for something like fn myfun(map: Map<i32, i32>) will be that you can't actually allocate an exec mode Map<i32, i32> value, so you can't call myfun. We might also try to flag map: Map<i32, i32> as an error directly, as an additional sanity check. It may be hard to be complete with this check, though, since you can declare something like fn myfun<A>(map: A) and then instantiate A with Map<i32, i32>. Catching the instantiation of A = Map<i32, i32>, and similar instantiations, might require more elaborate traits. Maybe a warning would be good enough, in cases where a parameter or datatype field clearly can never be instantiated?

#167 (comment)

I didn't think about the generics, but I think error/warning in this situation will always be helpful and result in a more relevant span (and help new users in situations like this one). I've frequently found it surprising when these errors wouldn't caught and I would end up getting an error while trying to call a function that had a parameter accidentally marked as exec.

For the generics, I think we could catch it when it's instantiated, like when we instantiate myfun::<Map<i32, i32>> we see that this is a function that takes an exec argument of proof type. (Or we could just rely on the fact that the user just won't be able to call that function without another mode error occurring earlier).

[utaal]

Also encountered by @matthias-brun, who reported the following in #290:

Currently one can use nat and int in exec mode functions. This shouldn't be allowed.

use builtin::*;
use builtin_macros::*;

verus! {
exec fn f(i: nat) -> nat {
    i
}
fn main() {
}
}

fhs m: page-table ν ./tools/rust-verify.sh /st/verus/test.rs
note: verifying root module

verification results:: verified: 2 errors: 0

[utaal]

There's a PR for this, which has been on the back burner for a bit: #323