Unsound: unsigned integer constants with the high bit set (e.g. `u8 = 200`) are decoded as negative in `const_value_ty`, so always-panicking programs verify as `safe`

[coord-e]

Summary

const_value_ty (src/analyze/basic_block.rs:383–391) decodes both signed and unsigned integer constants with ScalarInt::to_int, which sign-extends the raw bit pattern from the scalar's width:

(
    mir_ty::TyKind::Int(_) | mir_ty::TyKind::Uint(_),
    ConstValue::Scalar(Scalar::Int(val)),
) => {
    let val = val.to_int(val.size());          // ← sign-extends, even for Uint
    PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(val.try_into().unwrap()))
}

For an unsigned constant whose top bit (of its own type width) is set, this produces a negative CHC term. Because Thrust models integers as unbounded mathematical Int, that negative value then satisfies comparisons the real (non-negative) value never could — and Thrust accepts programs that panic on every execution.

This is the soundness consequence of the sign-extension already reported in #110. #110 is framed as an incompleteness ("would fail to verify even though it is clearly correct") plus a panic on values ≥ 2⁶³. This report is the opposite, more severe failure mode of the same decode: Thrust returns safe for programs that always panic, and it triggers on small, ordinary in-range values (u8 = 128, u16 = 32768, u32 ≥ 2³¹), not just the ≥ 2⁶³ values in #110. It is not an overflow / numeric-range issue — 200 is a perfectly valid u8; the constant's value is corrupted, independent of any range limit.

Reproduction (unsound accept)

u8_repro.rs — the only unsigned constant in the program is 200, so this isolates the bug to const_value_ty:

//@compile-flags: -C debug-assertions=off
fn main() {
    let x: u8 = 200;
    assert!(x < 100);   // runtime: 200 < 100 is false  =>  assertion ALWAYS fails => panic
}

The program panics under plain rustc (the assertion can never hold), yet Thrust accepts it:

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

SMT evidence

The emitted CHC (THRUST_OUTPUT_DIR) models x as -56 (= 200 reinterpreted as i8), so the panic obligation's premise is unsatisfiable and the assertion failure is vacuously discharged:

; panic obligation: requires (< x 100) == false under x == -56
(assert (forall ((v0 Bool) (v1 Int))
  (=> (and (= v0 (< v1 100)) (= v1 -56) p2 (= v0 false) true) false)))

With v1 == -56, (< -56 100) is true, forcing v0 == true, which contradicts the required (= v0 false). The clause body is unsatisfiable, so the genuine panic is never seen.

The defect is exactly the sign bit of the type width

Keeping the program identical and varying only the constant (assert!(x < 0), which is false for any u8, so a correct verifier must always reject):

program	model value of x	Thrust verdict	correct verdict
let x: u8 = 127; assert!(x < 0);	127	rejected (Unsat) ✓	reject
let x: u8 = 128; assert!(x < 0);	-128	accepted (safe) ✗	reject

127 (top bit clear) decodes correctly; 128 (top bit set) decodes to -128. The same boundary appears for u16 (32768) and u32 (3_000_000_000), both accepted as safe for assert!(x < 0).

Root cause

ScalarInt::to_int(size) interprets the width-sized bit pattern as signed. For Uint(_) the value must be read as unsigned (to_uint), otherwise every unsigned constant ≥ 2^(width-1) becomes negative in the logic. const_bytes_ty already avoids this by only handling TyKind::Int(_); the const_value_ty scalar path does not distinguish the two.

Expected behavior

Uint(_) constants should be decoded with to_uint (non-negative), so let x: u8 = 200 is modeled as 200 and assert!(x < 100) / assert!(x < 0) are correctly reported as verification failures instead of safe.

Relation to existing issues

• Unsigned integer constants sign-extended incorrectly in const_value_ty, causing wrong CHC terms and potential panic #110 identifies the same to_int line but characterizes the impact as incompleteness (correct programs rejected) and a panic on u64/u128 values ≥ 2⁶³. Filing separately because (a) the practical effect is unsoundness — the highest-severity class for a verifier, and the opposite of what Unsigned integer constants sign-extended incorrectly in const_value_ty, causing wrong CHC terms and potential panic #110 describes — and (b) it fires on small everyday unsigned values (u8 = 128), not only the large values in Unsigned integer constants sign-extended incorrectly in const_value_ty, causing wrong CHC terms and potential panic #110. The fix is shared (to_uint for Uint(_)), so resolving Unsigned integer constants sign-extended incorrectly in const_value_ty, causing wrong CHC terms and potential panic #110 resolves this; the intent here is to flag the soundness severity and the small-value trigger.
• Independent of the negative-SwitchInt unsoundness (Unsound: negative SwitchInt match targets are sign-truncated to large positives, making match arms verify under a wrong path assumption #132): the reproduction contains no match and no negative literal — only an unsigned constant and a < comparison against a positive/0 bound.

Environment

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