int shouldn't be an executable type

[jonhnet]

Verus passes this test file (verus /tmp/foo.rs --crate-type lib --compile gives 1 verified, 0 errors), but int shouldn't be accessible from executable code. I'm wondering what ended up in the compiled output!

use vstd::prelude::*;

verus!{

struct Point {
    x: int,
    y: int,
}

fn exec_point(p: Point) -> bool
{
    p.x < p.y
}

}

[utaal]

Oh, I didn't look at this closely enough when you sent it on Slack, sorry.

This isn't technically unsound, as it's not possible for verified code to actually construct an exec-mode Point:

fn main() {
    exec_point(Point { x: 3 as int, y: 4 as int });
}

results in:

error[[E0605]](https://doc.rust-lang.org/stable/error_codes/E0605.html): non-primitive cast: `i32` as `vstd::prelude::int`
  --> /playground/src/main.rs:16:27
   |
16 |     exec_point(Point { x: 3 as int, y: 4 as int });
   |                           ^^^^^^^^ an `as` expression can only be used to convert between primitive types or to coerce to a specific trait object

error[[E0605]](https://doc.rust-lang.org/stable/error_codes/E0605.html): non-primitive cast: `i32` as `vstd::prelude::int`
  --> /playground/src/main.rs:16:40
   |
16 |     exec_point(Point { x: 3 as int, y: 4 as int });
   |                                        ^^^^^^^^ an `as` expression can only be used to convert between primitive types or to coerce to a specific trait object

error: aborting due to 2 previous errors

[utaal]

This should help, once I get around to it: https://github.com/verus-lang/verus/pull/323

[jonhnet]

I agree it's not unsound, but it leads to some really confusing and late diagnostics. Lint suggestions in #323 sound good.

I'm also curious what --compile did with this example!