Unsound: the `i32::abs` extern spec (`requires(true)`) is violated at `i32::MIN`, so overflowing `abs` verifies as `safe`

[coord-e]

Summary

The trusted extern spec for i32::abs in std.rs (_extern_spec_i32_abs) declares

#[thrust_macros::requires(true)] // TODO: require x != i32::MIN
#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))]
fn _extern_spec_i32_abs(x: i32) -> i32 { i32::abs(x) }

The postcondition result >= 0 && (result == x || result == -x) is false at x == i32::MIN. Under -C debug-assertions=off — which Thrust requires — i32::MIN.abs() does not panic and does not return a non-negative value; it wraps and returns i32::MIN (a negative number), because -i32::MIN == 2147483648 is not representable as an i32.

Because requires(true) lets abs be called on any input, Thrust takes result >= 0 (and, since x < 0 forces the result == -x disjunct, result == 2147483648) as facts even when x == i32::MIN. It then discharges assertions that are false at runtime, i.e. it accepts programs that panic.

The // TODO: require x != i32::MIN on the very same line shows the guard is known to be missing, but there is no tracking issue and — unlike a mere "overflow not modeled" gap — this is an actively incorrect contract on a trusted library function that injects an out-of-i32-range value into the logic. It is the same soundness family as #172 (unsigned subtraction underflow) but a distinct instance.

Reproduction (minimal, no &mut / drop / enum)

abs_repro.rs:

//@compile-flags: -C debug-assertions=off
#[thrust::callable]
fn check(x: i32) {
    if x == i32::MIN {
        let y = x.abs();     // release/debug-assertions=off: returns i32::MIN (negative), not |x|
        assert!(y >= 0);     // runtime: y == i32::MIN < 0  =>  assertion fails (panic)
    }
}
fn main() {}

check(i32::MIN) panics under plain rustc (assertion failed: y >= 0), yet Thrust accepts it:

$ cargo run --quiet -- -Adead_code -C debug-assertions=false abs_repro.rs && echo 'accepted: safe'
accepted: safe

A sharper variant shows the spec forces an impossible i32 value (i32::MAX is 2147483647):

#[thrust::callable]
fn check(x: i32) {
    if x == i32::MIN {
        let y = x.abs();
        assert!(y > 2147483000);   // Thrust proves it (y is pinned to -x == 2147483648); runtime y == i32::MIN -> panic
    }
}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false abs_absurd.rs && echo 'accepted: safe'
accepted: safe

Control

For any non-MIN argument the spec is correct, so the defect is specific to the single overflowing input. The premise is also not made contradictory — assert!(false) after x.abs() on x == i32::MIN is still correctly rejected (Unsat), i.e. the bug produces a wrong value, not false, so it silently accepts exactly those programs whose safety depends on abs's true (wrapped) result.

Root cause

std.rs, _extern_spec_i32_abs:

#[thrust::extern_spec_fn]
#[thrust_macros::requires(true)] // TODO: require x != i32::MIN   <-- missing guard
#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))]
fn _extern_spec_i32_abs(x: i32) -> i32 {
    i32::abs(x)
}

Integer types are modeled as unbounded mathematical Int, so -x at x == i32::MIN evaluates to 2147483648 in-model and satisfies result >= 0; nothing constrains result to the i32 range or excludes the overflowing input. The ensured facts therefore describe a value the real i32 abs never returns.

Why it is unsound

ensures clauses of #[thrust::extern_spec_fn]/#[thrust::trusted] functions are assumed, not checked. So after let y = x.abs(); Thrust has y >= 0 and y == -x in scope. With x == i32::MIN the runtime value is y == i32::MIN (negative, debug-assertions=off), directly contradicting the assumed y >= 0. Any assertion discharged with that assumption (e.g. y >= 0, y > 2147483000) is vacuously valid in-model but fails at runtime — Thrust returns safe for a program that panics.

Expected behavior

abs should not be assumable at the one input where its result is unrepresentable. The fix is exactly the in-code TODO: guard the precondition,

#[thrust_macros::requires(x != i32::MIN)]
#[thrust_macros::ensures(result >= 0 && (result == x || result == -x))]

so a call site that may pass i32::MIN is rejected (precondition unsatisfiable) instead of silently trusting a false postcondition. (i32::abs is documented to overflow only at MIN, so this precondition is exactly the definedness condition.)

Relation to existing issues

• Unsoundness: unsigned subtraction underflow is not modeled, so panicking programs are verified as safe #172 (unsigned subtraction underflow verified as safe) is the same class (an integer overflow that is not modeled and yields an unsound accept), but a different site: that one is the primitive - operator on usize; this one is an incorrect postcondition in a trusted extern spec for the library function i32::abs, and the wrong value it asserts (2147483648) is outside the i32 range.
• Independent of the enum-discriminant (Unsound: enum variants after an explicit discriminant get the wrong datatype_discr value, making match arms vacuously verify #126) and negative-SwitchInt (Unsound: negative SwitchInt match targets are sign-truncated to large positives, making match arms verify under a wrong path assumption #132) unsoundnesses: this needs no enum, no match, and no negative match literal — just a call to i32::abs.

Environment

• thrust @ af7cd99
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 4.16.0, default fixedpoint (spacer) configuration
• Confirmed by running thrust-rustc (not inspection-only): the program above is accepted as safe.