Unsoundness: unsigned subtraction underflow is not modeled, so panicking programs are verified as `safe`

[coord-e]

Summary

Unsigned integer types (usize/u32/u64) are modeled as the unbounded mathematical integer sort (model::Int → SMT Int), and subtraction is translated to mathematical subtraction. Because the fixed-width wraparound (underflow) semantics of unsigned subtraction are not modeled, Thrust computes 0usize - 1 as -1 in its model, whereas the real program (with -C debug-assertions=off, exactly the mode Thrust requires) evaluates it to usize::MAX = 18446744073709551615.

This lets Thrust verify programs that actually panic at runtime — a genuine soundness violation, not merely incompleteness. Both a bounds-checked slice access and a plain assert! can be proven safe while the compiled program aborts.

This is distinct from #165. That issue is the incompleteness direction (the >= 0 lower bound of unsigned values is not assumed, so some safe programs are rejected) and is explicitly "soundness-preserving." The bug here is the opposite, more severe direction: an unsafe program is accepted. As shown under "Relationship to #165" below, applying the fix suggested there does not fix this.

Reproduced on 5648fd2 (Merge pull request #171 …exclude-zero-is_pos_neg) with z3 4.16.0.

Reproduction 1 — slice access out of bounds proven safe

#[thrust::callable]
fn last(s: &[i32]) {
    let n = s.len();       // usize
    let i = n - 1;         // when n == 0, wraps to usize::MAX in release
    let _x = s[i];         // out-of-bounds access when n == 0
}
fn main() {}

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

Thrust reasons i = n - 1, and for the bounds check i < len(s) with n == 0 it has i = -1 < 0, which holds — so the access is "in bounds." But the runtime index is usize::MAX, not -1. Actual execution:

fn last(s: &[i32]) { let n = s.len(); let i = n - 1; let _x = s[i]; }
fn main() { let empty: [i32; 0] = []; last(&empty); }

$ rustc -C debug-assertions=off -o last_run last_run.rs && ./last_run
thread 'main' panicked at last_run.rs:1: index out of bounds: the len is 0 but the index is 18446744073709551615

Reproduction 2 — assert! proven safe but fails at runtime

A self-contained version with no slices, isolating the arithmetic:

#[thrust::callable]
fn f(a: usize) {
    if a == 0 {
        let c = a - 1;      // release: wraps to usize::MAX
        assert!(c < 100);   // Thrust models c = -1, so "true"; runtime value is 1.8e19
    }
}
fn main() {}

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

Actual execution of the same logic:

fn f(a: usize) { if a == 0 { let c = a - 1; assert!(c < 100); } }
fn main() { f(0); }

$ rustc -C debug-assertions=off -o f_run f_run.rs && ./f_run
thread 'main' panicked at f_run.rs:1: assertion failed: c < 100

Expected vs. actual

• Expected: both programs are rejected (they can panic) — i.e. Unsat/verification error.
• Actual: both are reported safe.

Root cause

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

https://github.com/coord-e/thrust/blob/5648fd2/std.rs#L308-L312

The sub operator on these types returns model::Int, and the analyzer lowers a MIR BinOp::Sub on an Int-typed operand to plain Term::sub (mathematical subtraction):

https://github.com/coord-e/thrust/blob/5648fd2/src/analyze/basic_block.rs#L510-L512

Nothing records that the operands are a fixed-width unsigned type, so the two facts that make the real program panic are both lost:

1. the result is unsigned (>= 0), so usize::MAX (not -1) is what is actually produced, and
2. subtraction wraps modulo 2^bits on underflow.

Relationship to #165 (why the proposed fix there is insufficient)

#165 suggests attaching a { v: int | v >= 0 } refinement to unsigned values. That addresses the rejected-safe-program direction, but it does not close this soundness hole. With the >= 0 bound assumed on the input, the panicking program is still verified safe:

#[thrust_macros::requires(a >= 0)]   // the bound #165 wants to add
fn f(a: usize) {
    if a == 0 {
        let c = a - 1;
        assert!(c < 100);
    }
}
fn main() {}

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

Worse, if a >= 0 refinement is imposed on the result of a - 1 (also typed usize), the model gains the contradiction c == a - 1 == -1 ∧ c >= 0, from which anything is provable — a different flavor of unsoundness. So the underflow issue needs its own handling: model unsigned subtraction with wraparound (or emit an underflow-safety obligation lhs >= rhs at each unsigned Sub, mirroring how slice indexing already emits a bounds obligation), rather than only assuming >= 0.

Suggested direction

Track fixed-width unsignedness through lowering (e.g. distinguish an unsigned model, or carry bit-width) and either:

• emit an underflow-safety proof obligation lhs >= rhs for unsigned Sub (and analogous obligations for other operations whose safety depends on width), or
• model the operation with true wraparound (mod 2^bits) semantics.

Assuming >= 0 for unsigned inputs (#165) is complementary but, on its own, leaves this soundness gap open.