Incompleteness: unsigned integer types (`usize`/`u32`/`u64`) are modeled as unconstrained integers, so their `>= 0` lower bound is not assumed and safe programs are wrongly rejected

[coord-e]

Summary

Unsigned integer parameters are translated to the plain mathematical-integer sort (rty::Type::Int, SMT Int) with no >= 0 refinement. As a result, Thrust models a usize/u32/u64 value as an arbitrary integer that may be negative, and cannot discharge obligations that depend on the non-negativity that the Rust type system guarantees. Trivially-safe programs are rejected with Unsat.

The compiler itself considers x >= 0 on a usize a tautology (it emits warning: comparison is useless due to type limits), yet Thrust reports Unsat for it.

This is a soundness-preserving incompleteness (safe programs are rejected), analogous in flavor to #157 / #128. Non-negativity of unsigned values is needed for a large class of real programs (index/length arithmetic, loop bounds, etc.), so the gap is fairly fundamental.

Reproduction

Minimal:

#[thrust::callable]
fn nonneg(x: usize) {
    assert!(x >= 0);
}
fn main() {}

$ cargo run -- -Adead_code -C debug-assertions=false nonneg.rs
warning: comparison is useless due to type limits    // <- rustc knows x >= 0 always holds
 --> nonneg.rs:3:13
  |
3 |     assert!(x >= 0);
  |             ^^^^^^
error: verification error: Unsat
error: aborting due to 1 previous error; 1 warning emitted

A realistic case that does not trip the lint (does not rely on any overflow reasoning, since Int is mathematical):

#[thrust::callable]
fn check(a: usize, b: usize) {
    let c = a + b;
    assert!(c >= a);   // always true for non-negative a, b
}
fn main() {}

also fails with error: verification error: Unsat.

Reproduced on 6adb56d (Make seq concatenation operate on sequence tuples (#162)) with z3 4.16.0.

Expected vs. actual

• Expected: both programs verify (safe); a usize/u32/u64 value is >= 0 by definition.
• Actual: both are rejected with Unsat.

Root cause

usize, u32, u64 are declared via the int_model! macro in std.rs exactly like the signed types, mapping their model to model::Int:

https://github.com/coord-e/thrust/blob/6adb56d/std.rs#L307-L312

int_model!(isize);
int_model!(i32);
int_model!(i64);
int_model!(usize);   // <- collapsed to model::Int, losing unsignedness
int_model!(u32);
int_model!(u64);

The Model projection erases signedness, so by the time the type reaches TemplateBuilder::model_adt it is just the int model and is translated to an unrefined rty::Type::int():

https://github.com/coord-e/thrust/blob/6adb56d/src/refine/template.rs#L176-L178

No { v: int | v >= 0 } refinement is ever attached to values of unsigned type.

Confirmation of root cause

Adding the missing lower bound by hand makes both programs verify, which pinpoints the missing constraint:

#[thrust_macros::requires(a >= 0 && b >= 0)]   // <- restores the bound the type already guarantees
fn check(a: usize, b: usize) {
    let c = a + b;
    assert!(c >= a);
}
fn main() {}

$ cargo run -- -Adead_code -C debug-assertions=false check_fixed.rs && echo safe
safe

Likewise #[thrust_macros::requires(x >= 0)] on the minimal nonneg example makes it verify.

Suggested direction

Attach a >= 0 refinement to values of unsigned integer type. Because signedness is erased at the Model-projection step, the natural place to reintroduce it is where the Rust type is lowered — e.g. special-case TyKind::Uint(_) in TemplateBuilder::build/model_adt (src/refine/template.rs) to produce a refined { v: int | v >= 0 } instead of a bare rty::Type::int(), or introduce a distinct unsigned model type carrying that invariant. Whichever mechanism is used, the invariant must be assumed for unsigned inputs/results (and it would then also let Thrust reason about unsigned subtraction/underflow more faithfully).

Note: u8/u16 (and i8/i16) are a separate, orthogonal matter — they are not in int_model! at all and currently hit unimplemented!("unrefined_ty: ..") in src/refine/template.rs.