Boolean comparisons (<, <=, >, >=) emit ill-typed SMT (< Bool Bool), so any program comparing bools fails to verify #136

Summary

bool implements Ord, so a < b, a <= b, a > b, a >= b are valid safe Rust. Thrust accepts these in MIR but translates each operand directly with the numeric comparison term builders, producing SMT-LIB terms like (< b1 b2) / (<= b1 b2) where b1/b2 have sort Bool. In SMT-LIB, <, <=, >, >= are defined only for Int/Real, so the resulting query is ill-typed and the solver rejects it. As a result, any function that compares two booleans with an ordering operator fails verification — even when it is trivially safe.

This is an incompleteness bug (not a soundness hole): the solver error is surfaced as a generic verification error at src/analyze.rs:645-646, so safe programs are falsely rejected rather than wrongly accepted.

Reproduction

boolcmp.rs (a tautology — <= is a total order, so this never panics):

#[thrust::callable]
fn check(a: bool, b: bool) {
    assert!((a <= b) || (b <= a));
}
fn main() {}

$ THRUST_OUTPUT_DIR=/tmp/out cargo run -- -Adead_code -C debug-assertions=false boolcmp.rs
error: verification error: ...

The generated /tmp/out/thrust_output.smt2 contains (every vN is declared Bool):

(assert (forall ((v0 Bool) (v1 Bool) ... )
  (=> (and (= v2 (<= v1 v0)) (= v7 (<= v5 v6)) ...) (p2 ...))))

(<= v1 v0) applies <= to two Bool arguments → ill-typed SMT, which z3 (and any compliant solver) rejects.

For contrast, the identical program with i32 instead of bool produces Int-sorted operands ((v0 Int), (v1 Int) ...), so (<= v1 v0) is well-typed. The defect is specific to the Bool case.

Root cause

src/analyze/basic_block.rs:509-520, in rvalue_type for Rvalue::BinaryOp, groups Bool together with Int for the ordering operators and calls the numeric term builders:

(rty::Type::Int | rty::Type::Bool, mir::BinOp::Ge) => {
    builder.build(rty::Type::Bool, lhs_term.ge(rhs_term))
}
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Gt) => {
    builder.build(rty::Type::Bool, lhs_term.gt(rhs_term))
}
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Le) => {
    builder.build(rty::Type::Bool, lhs_term.le(rhs_term))
}
(rty::Type::Int | rty::Type::Bool, mir::BinOp::Lt) => {
    builder.build(rty::Type::Bool, lhs_term.lt(rhs_term))
}

Term::ge/gt/le/lt (src/chc.rs:715-729) emit Function::GE/GT/LE/LT, which print as the numeric >=/>/<=/< (Bool is emitted as the SMT Bool sort, src/chc/format_context.rs:80). Applying them to Bool-sorted operands is invalid.

(Eq/Ne for Bool are fine: =/distinct are defined for any sort, so only the four ordering operators are affected.)

Suggested fix

Handle the Bool cases of Ge/Gt/Le/Lt separately using the boolean order false < true, e.g.:

• a <= b ≡ a ⇒ b ≡ (or (not a) b)
• a < b ≡ (and (not a) b)
• a >= b ≡ b ⇒ a
• a > b ≡ (and a (not b))

(or, alternatively, model bool operands as Int 0/1 for these operators). The existing Int | Bool arms should be split so that Bool does not reach the numeric ge/gt/le/lt builders.

Notes

• No existing tests/ui example compares booleans with an ordering operator, so this is currently untested.
• Discovered by reading the Rvalue::BinaryOp lowering and confirmed by dumping the generated SMT-LIB via THRUST_OUTPUT_DIR (no solver required to observe the ill-typed term).