Any boolean-valued expression in a spec (`requires(b)`, `ensures(result)`, `!b`, `b && c`, `b ==> c`, `invariant!(|b: bool| b)`) aborts the compiler with `expected a formula`: `FormulaOrTerm::into_formula` has no `Term`→atom case, so only the `b == true` spelling is usable

[coord-e]

Summary

A bool-typed term — a bool parameter, result of a -> bool function, *r on a &bool, !r on a &mut bool, a bool struct field — can never be used where a formula is expected. Every such annotation aborts thrust-rustc with

thread 'rustc' panicked at src/analyze/annot_fn.rs:428:14:
expected a formula

This is not a missing feature: the Bool sort, the Model instance and the CHC encoding are all already correct, the same specs verify once the translator learns to lift a Bool-sorted term into an atom (one-line change, verified below, full suite still green), and the explicit-comparison spelling b == true of the very same spec verifies today. The hole is in the translation from the type-checked HIR of the formula_fn companion to chc::Formula.

The practical effect is that no predicate a real program carries as a bool can be named in a spec: no flag parameter, no -> bool postcondition, no is_*-style predicate result, no bool field of a struct, and no &&/||/!/==> over them. #[thrust_macros::requires], ensures, param, ret, sig, invariant! and closure! specs are all affected, as is the ==> implication syntax added in #106 and thrust_models::implies, whose operands are bool by construction. Because the failure is a compiler abort rather than a diagnostic, there is nothing pointing the user at the == true workaround.

Minimal reproduction

repro.rs:

#[thrust_macros::requires(b)]
#[thrust_macros::ensures(result == 1)]
fn f(b: bool) -> i64 { if b { 1 } else { 0 } }

#[thrust::callable]
fn check() { assert!(f(true) == 1); }

fn main() {}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' (21829) panicked at src/analyze/annot_fn.rs:428:14:
expected a formula
stack backtrace:
   ...
   4: thrust::analyze::annot_fn::AnnotFnTranslator::to_formula
             at ./src/analyze/annot_fn.rs:428:14
   5: thrust::analyze::annot_fn::AnnotFnTranslator::to_formula_fn
             at ./src/analyze/annot_fn.rs:404:28
   6: thrust::analyze::Analyzer::formula_fn_with_args

Expected: safe. Actual: the compiler aborts.

Ground truth

Every program in this report is valid, safe Rust that real rustc compiles and runs to completion; none of them can panic.

$ rustc -Adead_code --edition 2021 -o gt gt.rs && ./gt; echo "exit=$?"
exit=0

The same defect, thirteen spellings

All of these abort at annot_fn.rs:428 with expected a formula, and all thirteen verify safe with the fix below. Each is written so that it is provable but not vacuous: flipping the asserted value makes it Unsat under the fix.

#	spec	shape
1	#[requires(b)]	bare bool parameter
2	#[requires(!b)]	logical negation of a bool
3	#[requires(b && c)]	&& over bools
4	#[requires(b || c)]	|| over bools
5	#[requires(x > 0 && b)]	one comparison operand, one bool operand
6	#[requires(b ==> c)]	==> (#106) with bool operands
7	#[requires((x > 0) ==> b)]	==> with one bool operand
8	#[requires(thrust_models::implies(b, c))]	implies from std.rs
9	#[ensures(result)] on fn pos(x: i64) -> bool	bool return value
10	#[ensures(!r)] on fn set_true(r: &mut bool)	prophecy value of a &mut bool
11	#[requires(*r)] on r: &bool	deref of a &bool
12	#[requires(s.flag)]	bool field of a Model-ed struct
13	invariant!(|i: i64, b: bool| i >= 0 && b)	loop invariant

The refinement-type spelling fails the same way — #[param(b: { v: bool | v })] and #[sig(fn(b: { v: bool | v }) -> { r: i64 | r == 1 })] — as does a closure!(requires(b), ..) spec and a bool-binder quantifier body thrust_models::exists(|b: bool| b).

Three of them written out, because they are the shapes real code wants most:

// 9: a `-> bool` predicate cannot state what it returns
#[thrust_macros::requires(x > 0)]
#[thrust_macros::ensures(result)]
fn pos(x: i64) -> bool { x > 0 }

// 10: a `&mut bool` cannot state its prophecy value
#[thrust_macros::requires(true)]
#[thrust_macros::ensures(!r)]
fn set_true(r: &mut bool) { *r = true; }

// 12: a `bool` field cannot be named
struct S { flag: bool }
impl thrust_models::Model for S { type Ty = Self; }

#[thrust_macros::requires(s.flag)]
#[thrust_macros::ensures(result == 1)]
fn f(s: S) -> i64 { if s.flag { 1 } else { 0 } }

Controls — everything adjacent verifies

Program	Result	Why it is fine
#[requires(b == true)] + #[ensures(result == 1)] on row 1's body	safe	comparison → FormulaOrTerm::BinOp, which into_formula handles
#[requires(b == false)] + #[ensures(result == 0)]	safe	same
#[ensures(result == true)] on fn pos(x: i64) -> bool	safe	same, and it is row 9's workaround
#[requires(!(x > 0))]	safe	! applied to a comparison, i.e. Not(BinOp)
#[requires(x > 0 && y > 0)]	safe	And(BinOp, BinOp)
#[ensures(result == (x > 0))] on fn pos(x: i64) -> bool	safe	the mirror direction: a formula in term position is already converted by into_term
#[ensures(r == Mut::new(*r, !(*r)))] on fn flip(r: &mut bool)	safe	!(*r) sits in term position under Mut::new
assert!(b), assert!(!b), if b && c { .. } in ordinary code	safe	program code never goes through AnnotFnTranslator

So the trigger is exactly: a Bool-sorted term reaching formula position — directly, or as an operand of !, &&, ||, ==>/implies — in any annotation.

Root cause

FormulaOrTerm::into_formula (src/analyze/annot_fn.rs:137) has no case that turns a term into a formula:

fn into_formula(self) -> Option<chc::Formula<T>> {
    let fo = match self {
        FormulaOrTerm::Formula(fo) => fo,
        FormulaOrTerm::Term { .. } => return None,          // <-- here
        FormulaOrTerm::BinOp(lhs, binop, rhs) => { /* … builds an atom … */ }
        FormulaOrTerm::And(lhs, rhs) => lhs.into_formula()?.and(rhs.into_formula()?),
        FormulaOrTerm::Or(lhs, rhs) => lhs.into_formula()?.or(rhs.into_formula()?),
        FormulaOrTerm::Implies(lhs, rhs) => lhs.into_formula()?.implies(rhs.into_formula()?),
        FormulaOrTerm::Not(formula_or_term) => formula_or_term.into_formula()?.not(),
        FormulaOrTerm::Literal(b) => { /* … */ }
    };
    Some(fo)
}

A path expression of bool type is translated to FormulaOrTerm::Term, so into_formula returns None. And/Or/Implies/Not propagate that None through ?, which is why a single bool operand anywhere in the expression is enough — row 5 (x > 0 && b) fails although x > 0 && y > 0 verifies. Row 2 in particular reaches ExprKind::Unary(UnOp::Not, ..) at src/analyze/annot_fn.rs:698; the operand's ADT is not Mut, so it takes the _ arm and builds Not(Term(b)), which then cannot be converted. At the top, to_formula turns the None into an abort:

fn to_formula(&self, hir: &'tcx rustc_hir::Expr<'tcx>) -> chc::Formula<rty::FunctionParamIdx> {
    self.to_formula_or_term(hir)
        .into_formula()
        .expect("expected a formula")   // src/analyze/annot_fn.rs:428
}

The asymmetry is one-directional: into_term already converts each BinOp variant to a boolean term, which is why the mirror control row (ensures(result == (x > 0))) verifies.

Anything reaching into_formula is in formula position of a requires/ensures/refinement expression, which the companion formula_fn type-checks at type bool, so a Term arriving there is always Bool-sorted.

Suggested fix

Lift the term into the atom t = true:

-            FormulaOrTerm::Term { .. } => return None,
+            FormulaOrTerm::Term(t) => chc::Formula::Atom(chc::Atom::new(
+                chc::KnownPred::EQUAL.into(),
+                vec[t, chc::Term::bool(true)],
+            )),

With only that change, all thirteen rows plus the param/sig/closure!/quantifier spellings verify safe, each is correctly rejected with Unsat when the asserted value is flipped, and cargo test still reports 346 passed.

If a fix lands it would be worth adding a tests/ui/pass/annot_bool.rs / tests/ui/fail/annot_bool.rs pair over requires(b) / ensures(result) / !b / b && c / b ==> c, since the existing annotation tests (annot_implication.rs included) only ever put comparisons in formula position and so never exercise this path.

Scope / when it bites

Any spec that talks about a boolean: a flag parameter, a -> bool predicate's own postcondition, an is_empty/is_valid-style method, a bool field of a state struct, a loop invariant that carries a boolean flag. It needs no &mut reasoning, no containers, no generics and no recursion; it is independent of the enum-expansion depth limit; it reproduces at -C opt-level=0 (so it is unrelated to #244/#248); and it involves no numeric-range/overflow reasoning — every constant is 0 or 1. It is distinct from #136, which is about ordering comparisons (<, <=) on bool values in program code emitting (< Bool Bool) from analyze::basic_block; here the boolean never reaches the solver at all, and equality on bool in annotations works fine.

Environment

• thrust @ 5c74a7f
• rustc nightly-2025-09-08 (per rust-toolchain.toml), x86_64-unknown-linux-gnu
• Z3 5.0.0, default solver configuration
• Flags: -Adead_code -C debug-assertions=false