An unsuffixed integer literal in a specification is typed `i32`, so `requires(x > -9223372036854775807 - 1)` on an `i64` is rejected as out of range

[coeff-aij]

Summary

In a specification, a program variable of any integer type is lowered to thrust_models::model::Int. The comparison and arithmetic operators on Int are the generic impls impl<T> PartialEq<T> for Int where T: Model<Ty = Self>, and likewise for PartialOrd, Add, Sub and Mul (std.rs:15-54). An unsuffixed integer literal on the other side therefore has several candidate types (isize, i32, i64, usize, u32, u64). rustc cannot pick one and falls back to i32. Any literal outside the i32 range is rejected by the overflowing_literals lint (deny by default), even when the variable it is compared with is an i64 or a u64.

Minimal reproduction

unsuffixed.rs:

#[thrust_macros::requires(x > -9223372036854775807 - 1)]
fn f(x: i64) -> i64 {
    x
}

fn main() {
    f(0);
}

On main e112206:

$ export LD_LIBRARY_PATH=$(rustc --print sysroot)/lib
$ target/debug/thrust-rustc -Adead_code -Aunused -C debug-assertions=false --edition 2021 unsuffixed.rs
error: literal out of range for `i32`
 --> unsuffixed.rs:1:31
  |
1 | #[thrust_macros::requires(x > -9223372036854775807 - 1)]
  |                               ^^^^^^^^^^^^^^^^^^^^
  |
  = note: the literal `-9223372036854775807` does not fit into the type `i32` whose range is `-2147483648..=2147483647`
  = help: consider using the type `i64` instead
  = note: `#[deny(overflowing_literals)]` on by default

error: aborting due to 1 previous error

With the literal suffixed (-9223372036854775807i64 - 1) the same program verifies (exit status 0). requires(x < 3000000000) fails the same way, for x: i64 and for x: u64.

Expected

An unsuffixed literal in a specification denotes a mathematical integer (its model is Int). It is accepted at any magnitude, or at least at the type of the variable it is compared with.

Notes

Possible directions:

• The annotation macros could rewrite an unsuffixed integer literal into an Int-typed expression, so that no Rust integer type is inferred. Since Represent integer terms with arbitrary precision #279 the term side is arbitrary precision.
• Alternatively, they could give it the widest modeled type (e.g. i128 once it has a Model impl).

#296 (merged) lets i64::MIN be written in annotations, which is a workaround for the bounds but not for other large literals.

I searched the tracker for literal and i32 issues in annotations and found none.