warning if the user attempts arithmetic with bounded int types in spec/proof

[tjhance]

This is almost always a mistake - it's idiomatic to convert to an int first in spec code

[parno]

This may be controversial, but should we consider "reversing the polarity"; i.e., automatically casting bounded int types to int in spec/proof? It's pretty easy for specs (e.g., in requires/ensures) to get sufficiently cluttered with as int that they obscure the intended meaning. We could still support some annotation to indicate "no I really want these to stay bounded".

[tjhance]

Though I'm not morally opposed - doing all those casts is really annoying - it's not technically obvious how to do it. The Rust typechecker runs before mode-checking, so a rule like "cast to int in spec code" can't be implemented easily.

Also, since bit-vector arithmetic exists, we don't always want to cast up to an int. We really only want to do that in arithmetic settings instead of bit settings. It might be reasonable to have a rule "cast the arguments to (+, -, *, /) to an int". But that still runs into the problem above.

One thing we might be able to do is abuse the fact that int only exists in spec code, and thus change the typechecking rules only in context where ints are expected; for example, in the following:

#[spec] let a: u8 = 5;
#[spec] let b: u8 = 8;
#[spec] let x: int = a + b;

Rust currently doesn't allow this (it infers that a+b is a u8, then refuses to cast without an explicit cast). So maybe we could change it to automatically insert casts:

#[spec] let x: int = a as int + b as int;

I don't know if it's an easy change, but it'd probably be a controversial one 😅

[Chris-Hawblitzel]

I like int in specs. I'd like to encourage arithmetic on int in specs, either by automatic coercions, warnings, or errors. Right now, there are already some automatic coercions. If a: u8 and b: int, then a + b automatically promotes a to int before doing the +. This is part of our extension to Rust's type checking.

We have some support for early mode analysis in rust_verify/src/typecheck.rs. We use it for autoview. It's not complete, but it covers a lot of convenient cases. We could use it to insert some as int coercions in specs if we wanted.

Some people like nat in specs. If n: nat, should n - 1 be an int? I think we could easily implement nat->int coercions like this because they are only relevant to specs and we control the type-checking of nat and int.

What annotation should we use to say "I know what I'm doing, and I don't want to expand to an int"? Should people write a.add(b) instead of a + b to mean non-int addition in specs?

[tjhance]

What annotation should we use to say "I know what I'm doing, and I don't want to expand to an int"? Should people write a.add(b) instead of a + b to mean non-int addition in specs?

They can always use wrapping_add if they're looking for wrapping behavior.

Is there a case where someone might actually want the "clipped, but arbitrary" behavior?

[parno]

I think a.add(b) and wrapping_add are both reasonable ways of indicating the desire for a non-coerced operation.