Ordering comparisons (<, >) on tuple/aggregate values emit ill-typed SMT (< Tuple Tuple) via the generic PartialOrd::lt/gt extern specs, so safe programs comparing tuples are falsely rejected #195

Summary

Tuples implement PartialOrd (lexicographically), so a < b / a > b on (i64, i64) is valid, safe Rust. Thrust accepts the program but, when lowering the comparison, translates the model-level </> with the numeric term builders, producing an SMT-LIB atom like (< v6 v7) where v6/v7 have sort A0_Tuple<Int-Int>. In SMT-LIB </> are declared only for Int, so the query is ill-typed and the solver rejects it. As a result, any function that compares two tuples (or any aggregate value) with </> fails verification — even when it is trivially safe.

Like #136, this is an incompleteness bug (not a soundness hole): the solver error is surfaced as a generic verification error, so safe programs are falsely rejected, never wrongly accepted.

This is distinct from #136, which is specifically the bool case flowing through the Rvalue::BinaryOp arms in src/analyze/basic_block.rs:509-520. Tuples are not a primitive MIR BinOp; a < b on a tuple lowers to a PartialOrd::lt call that Thrust maps to the generic extern spec _extern_spec_partialord_lt<T> in std.rs, whose ensures body is where the ill-typed < is produced. The two bugs share a class ("ordering operators applied to a non-Int sort") but have different code paths and different fix sites; #136's suggested fix (splitting the Int | Bool BinaryOp arms) does not touch this path.

Reproduction

Minimal — symbolic tuple parameters, a bare a < b:

#[thrust::callable]
fn check(a: (i64, i64), b: (i64, i64)) {
    let _ = a < b;
}
fn main() {}

$ cargo run -- -Adead_code -C debug-assertions=false min.rs
error: verification error: Error { stdout: "(error \"line 23 column 313: Sort mismatch at argument #1 for function (declare-fun < (Int Int) Bool) supplied sort is A0_Tuple<Int-Int>\")\nsat\n", stderr: "" }
error: aborting due to 1 previous error

Realistic — lexicographic max of two pairs (never panics, so it should verify):

fn max_pair(a: (i64, i64), b: (i64, i64)) -> (i64, i64) {
    if a > b { a } else { b }
}

#[thrust::callable]
fn check(a: (i64, i64), b: (i64, i64)) {
    let m = max_pair(a, b);
    let _ = m;
}
fn main() {}

fails the same way (... Sort mismatch ... for function (declare-fun > (Int Int) Bool) supplied sort is A0_Tuple<Int-Int>).

Control — the identical program with i64 scalars instead of tuples verifies (safe), isolating the defect to aggregate operands:

fn max_i(a: i64, b: i64) -> i64 { if a > b { a } else { b } }
#[thrust::callable]
fn check(a: i64, b: i64) { let m = max_i(a, b); let _ = m; }
fn main() {}

Generated SMT-LIB evidence

THRUST_OUTPUT_DIR=… on the minimal example emits (every vN here is A0_Tuple<Int-Int>):

(declare-datatypes ((A0_Tuple<Int-Int> 0)) (...))
...
(assert (forall ((v0 A0_Tuple<Int-Int>) ... (v6 A0_Tuple<Int-Int>) (v7 A0_Tuple<Int-Int>) (v8 Bool))
  (=> (and ... (= v8 (< v6 v7))) (p3 v8 v0 v1 v2 v3 v4 v5))))

(< v6 v7) applies the numeric < (declare-fun < (Int Int) Bool) to two A0_Tuple<Int-Int> arguments → ill-typed, which z3 (and any compliant solver) rejects.

Root cause

a < b / a > b on a tuple is a PartialOrd::lt / PartialOrd::gt call, which Thrust resolves to the generic extern specs in std.rs (T: PartialOrd, no restriction to integer types):

https://github.com/coord-e/thrust/blob/6953863/std.rs#L998-L1022

#[thrust_macros::ensures(result == (*x < *y))]
fn _extern_spec_partialord_lt<T>(x: &T, y: &T) -> bool
  where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd
{ PartialOrd::lt(x, y) }

#[thrust_macros::ensures(result == (*x > *y))]
fn _extern_spec_partialord_gt<T>(x: &T, y: &T) -> bool
  where T: thrust_models::Model + PartialOrd, T::Ty: PartialOrd
{ PartialOrd::gt(x, y) }

When T is instantiated at an aggregate type (here (i64, i64)), *x/*y have an aggregate model sort, and the formula-level </> in the ensures is translated with the numeric Term::lt/Term::gt builders (Function::LT/GT, src/chc.rs:806-816), which print as the Int-only </>. The comparison-operator lowering does not check the operand sort, so the aggregate sort flows straight into a numeric </> application — exactly the same class of defect as #136, but originating in the extern-spec/formula path rather than the BinaryOp path.

Note on <= / >=

<=/>= on tuples do not hit this path — there are no partialord_le/ge extern specs, so the call is unresolved and instead hits an unimplemented!/panic! ("unknown def") in src/analyze/basic_block.rs. So aggregate ordering is currently: </> → ill-typed SMT (this issue); <=/>= → clean "unsupported" panic. Ideally all four behave consistently.

Suggested direction

Two complementary options:

1. Encode lexicographic ordering for aggregate operands (recurse field-by-field), so </> on tuples/structs produce well-typed SMT that matches Rust's derived PartialOrd; add the missing <=/>= specs at the same time.
2. If aggregate ordering is out of scope for now, at least make </> on non-Int operands fail with the same explicit "unsupported" diagnostic as <=/>=, instead of silently emitting ill-typed SMT that surfaces as an opaque solver error.

Whichever direction, the comparison lowering should guard on the operand sort so a non-Int sort never reaches the numeric </>/<=/>= term builders (mirrors the guard recommended in #136 for the BinaryOp arms).

Environment

• thrust @ 6953863
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• z3 4.13.4

Related

• Boolean comparisons (<, <=, >, >=) emit ill-typed SMT (< Bool Bool), so any program comparing bools fails to verify #136 — same class (ordering operator applied to a non-Int sort) but the bool/BinaryOp path; this issue is the tuple/aggregate PartialOrd-extern-spec path.
• Quantifier (forall/exists) binder sorts are never declared in SMT-LIB, so any spec quantifying over a datatype/tuple-sorted variable emits an undefined sort #142 — quantifier binder sorts over datatypes (a different SMT-well-formedness issue).