Disallow nat and int in exec-mode

[matthias-brun]

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]

work in progress here: #323

[utaal]

Merged with #170, closing.