Incompleteness: `#[requires(..)]` alone pins the postcondition to `true` instead of leaving it inferred (unlike `closure!(requires(..))` and `#[param(..)]`), so adding a precondition silently strips every caller of the call's result

[coord-e]

Summary

Writing only #[thrust_macros::requires(φ)] on a fn does not just add a precondition — it silently pins the function's postcondition to the constant true, replacing the inference template that the same function would otherwise get. Every caller therefore learns nothing about the call's result (and, for a &mut parameter, nothing about the referent after the call), so programs that verify without the annotation start failing with Unsat the moment a precondition is added, with no diagnostic pointing at the cause.

The two other front-ends for the very same concept do not behave this way:

• thrust_macros::closure!(requires(..), ..) leaves the postcondition inferred — that is its documented, tested behavior (thrust-macros/src/closure.rs:17, tests/ui/pass/closure_requires_only.rs: "its postcondition stays inferred as a predicate variable, so the caller still learns the body's exact result").
• #[thrust_macros::param(x: { v | φ })] also leaves the return refinement inferred.

Only the #[requires] attribute collapses it. This is an incompleteness (safe programs are rejected); soundness is preserved — see "Soundness is preserved" below.

Reproduction

repro.rs:

#[thrust_macros::requires(x > 0)]
fn f(x: i64) -> i64 { x + 1 }

fn main() {
 let r = f(3);
 assert!(r == 4);
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs && echo safe
error: verification error: Unsat

Deleting the one attribute line makes it verify:

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

f(3) is called with 3 > 0, so the precondition is satisfied — the annotation adds a fact and removes none, yet it turns a verifying program into a rejected one.

Observed vs. expected

program	Thrust	expected
#[requires(x>0)] fn f(x:i64)->i64 { x+1 }, assert!(f(3)==4)	Unsat	safe
same, attribute removed	safe ✓	safe
#[param(x:{v:i64|v>0})] fn f(x:i64)->i64 { x+1 }, assert!(f(3)==4)	safe ✓	safe
#[requires(x>0)] #[ensures(result==x+1)] fn f(..), assert!(f(3)==4)	safe ✓	safe
closure!(requires(x>0), |x:i64|->i64 { x+1 }) through a pre!/post! HOF, assert!(r==4)	safe ✓	safe

The precondition itself is installed correctly — only the postcondition is lost:

program	Thrust	why
#[requires(x>0)] fn f(x:i64)->i64 { assert!(x>0); x+1 }, called as f(3)	safe ✓	precondition is assumed in the body
#[requires(x>0)] fn f(x:i64)->i64 { assert!(x<0); x+1 }, called as f(3)	Unsat ✓	body is still checked

Why this bites real programs

The information lost is not limited to a returned integer. Any &mut parameter's referent is havoc'd at the call site, because the (now constant-true) postcondition says nothing about its prophecy:

#[thrust_macros::requires(x > 0)]
fn add(r: &mut i64, x: i64) { *r += x; }

fn main() {
 let mut a: i64 = 1;
 add(&mut a, 2);
 assert!(a == 3); // Unsat; safe (and verifies) without the `requires`
}

The same happens for the most natural use of a precondition — guarding an indexing helper — where the annotation is exactly the thing a user would reach for:

#[thrust_macros::requires(i < (*v).length)]
fn get(v: &Vec<i64>, i: usize) -> i64 { v[i] }

fn main() {
 let mut v: Vec<i64> = Vec::new();
 v.push(10);
 assert!(get(&v, 0) == 10); // Unsat; safe without the `requires`
}

program	Thrust	expected
#[requires(x>0)] fn add(r:&mut i64, x:i64), assert!(a==3)	Unsat	safe
same, attribute removed	safe ✓	safe
#[requires(i<(*v).length)] fn get(&Vec<i64>, usize), assert!(get(&v,0)==10)	Unsat	safe
same, attribute removed	safe ✓	safe

Because the failure surfaces as a plain Unsat at an unrelated assert! in the caller, the annotation is the last place a user looks. The only fix is to hand-write a complete #[ensures(..)] restating everything the body does — precisely the work Thrust's inference exists to avoid. (Switching the precondition to #[thrust_macros::param(x: { v: i64 | v > 0 })] is a workaround for a value-typed parameter: it is still enforced at call sites — check(y) { f(y) } with unconstrained y is correctly Unsat — still assumed in the body, and the return stays inferred.)

SMT evidence

Emitting the CHCs (THRUST_OUTPUT_DIR) for repro.rs and repro_no_annot.rs:

; ---- no annotation (safe) ----
(declare-fun p1 (Int Int) Bool) ; <-- return refinement template p1(result, x)
; c0 body: result = x+1, under the parameter predicate p4, establishes p1
(assert (forall ((v0 Int) (v1 Int) (v2 Int) (v3 Int) (v4 Int))
 (=> (and (= v0 (+ v1 1)) (= v2 v1) (p4 v2 v1) (= v3 v2) (= v4 v0) true) (p1 v4 v3))))
; c3 call site: p1(result, 3) is assumed, so the caller learns result = 4
(assert (forall ((v0 Int) (v1 Int)) (=> (and p5 (= v0 3) (p1 v1 v0) true) (p6 v1))))

; ---- #[requires(x > 0)] only (Unsat) ----
; (no return predicate is declared at all, and no clause types f's body against one)
; c0 the precondition is installed correctly
(assert (forall ((v0 Int) (v1 Int)) (=> (and (> v1 0)) (p2 v1 v1))))
; c1 call site discharges it: 3 > 0
(assert (forall ((v0 Int) (v1 Int)) (=> (and p3 (= v1 3) (not (> v1 0))) false)))
; c2 call site: the result v1 is completely unconstrained
(assert (forall ((v0 Int) (v1 Int)) (=> (and p3 (= v0 3) true) (p4 v1))))
; c4 ... so `assert!(r == 4)` is unprovable
(assert (forall ((v0 Int) (v1 Int)) (=> (and (p4 v0) p3 (= v1 v0) (not (= v1 4)) true) false)))

The return template p1 and the body clause c0 that constrains it both vanish; c2 hands the caller a fresh unconstrained v1.

Root cause

#[requires] and #[ensures] accumulate into a single internal #[_requires_ensures(req, ens)] attribute. When only one of them is written, the other slot is filled with the literal true:

// thrust-macros/src/spec.rs:214-249 (extract_requires_ensures)
 if let Some((req_expr, ens_expr)) = result {
 Ok((req_expr, ens_expr))
 } else {
 Ok((syn::parse_quote!(true), syn::parse_quote!(true))) // <-- both sides default to `true`
 }

ExpandedTokens::expand (thrust-macros/src/spec.rs:386-448) then unconditionally emits both companions and both markers, so a requires-only function is indistinguishable downstream from one that was written as #[requires(φ)] #[ensures(true)]:

 let requires_fn = self.requires_fn();
 let ensures_fn = self.ensures_fn(); // <-- always emitted, body `true`
 ...
 #[thrust::requires_path] #path_prefix #requires_name #turbofish;
 #[thrust::ensures_path] #path_prefix #ensures_name #turbofish; // <-- always emitted

The plugin side then takes the annotated path: expected_ty sees ensure_annot = Some(⊤) and calls

// src/analyze/local_def.rs:295-297
 if let Some(ensure) = ensure_annot {
 builder.ret_refinement(ensure.into());
 }

which sets ret_rty = Some(..) (src/refine/template.rs:546-553), so FunctionTemplateTypeBuilder::build never reaches the template branch:

// src/refine/template.rs:658-662
 let ret_rty = self.ret_rty.clone().unwrap_or_else(|| {
 self.inner.for_template(self.registry).with_scope(&builder).build_refined(self.ret_ty)
 }); // ^-- the inference template that is skipped

Contrast the closure front-end, which emits a marker only for the clause the user actually wrote:

// thrust-macros/src/closure.rs:143-176
 if let Some(body) = conjoin(requires) { prelude.push(quote! { .. #[thrust::requires_path] .. }); }
 if let Some(body) = conjoin(ensures) { prelude.push(quote! { .. #[thrust::ensures_path] .. }); }

with the module doc stating the intent explicitly (closure.rs:17): "Each clause is optional (an omitted one leaves that side inferred)".

Soundness is preserved

Pinning the postcondition to true only weakens what callers may assume, so it over-rejects and never accepts a bad program. The body is still analyzed and its panics are still caught (#[requires(x>0)] fn f(x:i64)->i64 { assert!(x<0); x+1 } called as f(3) is correctly Unsat), and the declared precondition is still enforced at call sites (check(y) { f(y) } with unconstrained y is correctly Unsat).

The dual manifestation, and a caveat on the fix

The same default makes #[ensures]-only pin the precondition to true:

#[thrust_macros::ensures(result == x + 1)]
fn f(x: i64) -> i64 { assert!(x > 0); x + 1 }

fn main() { let r = f(3); assert!(r == 4); } // Unsat; safe without the `ensures`

That direction is the same root cause, but it should not simply be flipped to an inference template: #179 shows that an inferred parameter precondition on an explicitly-declared function can be discharged vacuously (p0 := λx. false) when the function is never called, which is an accepts-bad direction. The postcondition side has no such hazard — a template in head position is constrained from above by the body clause, exactly as it is for a completely unannotated function — so it can be left inferred safely.

Expected behavior / suggested direction

#[requires(φ)] alone should behave like closure!(requires(φ), ..) and like #[param(x: {v | φ})]: install the precondition and leave the return refinement as an inference template, so repro.rs verifies. Concretely, distinguish "the user wrote ensures(true)" from "the user wrote no ensures" — e.g. carry Option<syn::Expr> through _requires_ensures and emit the #[thrust::ensures_path] marker (and the ensures_fn companion) only when an ensures clause was actually written, mirroring closure.rs.

A tests/ui/pass case for a requires-only fn whose caller relies on the inferred result (with a fail twin whose caller asserts the wrong value) would guard this, alongside the existing closure_requires_only.rs / closure_ensures_only.rs pair.

The README's "requires and ensures are independent: you can write either one on its own, and a missing one defaults to true" would need updating too: for closures the missing side is inferred, not true, and that is the behavior worth having for the postcondition side of fns as well.

Relation to existing issues

• Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected #191 (#[param] precondition dropped when #[ensures] is also present) is the mirror image in the other front-end: there an explicitly written precondition is lost; here an unwritten postcondition is over-specified as true. Different mechanism (refinement_at vs. the always-emitted ensures_path marker), different direction.
• Unsound: a function annotated only with sig/ret/param whose body violates the declared refinement verifies as safe when it is not called (unspecified param precondition becomes an inference template that is discharged vacuously) #179 (sig/ret/param-only functions checked against an inferrable — hence vacuous — parameter precondition) is about the precondition side defaulting to a template. This report is about the postcondition side defaulting to a constant; the two asks are compatible (see the caveat above), and fixing this one must not reintroduce Unsound: a function annotated only with sig/ret/param whose body violates the declared refinement verifies as safe when it is not called (unspecified param precondition becomes an inference template that is discharged vacuously) #179.
• Generic functions with requires/ensures are not verified against their bodies (treated as trusted summaries) #103 (closed: generic functions with requires/ensures treated as trusted summaries) concerned bodies not being checked; here the body is checked, and the loss is entirely on the caller side.
• Unrelated to the integer-modeling issues (Unsigned integer constants sign-extended incorrectly in const_value_ty, causing wrong CHC terms and potential panic #110/Unsound: unsigned integer constants with the high bit set (e.g. u8 = 200) are decoded as negative in const_value_ty, so always-panicking programs verify as safe #180/Unsound: negative SwitchInt match targets are sign-truncated to large positives, making match arms verify under a wrong path assumption #132/Unsoundness: unsigned subtraction underflow is not modeled, so panicking programs are verified as safe #172): every value here is small and in range.

Environment

• thrust @ cd6b330 ("Merge pull request Fold invariant_context into context #231 …unify-context-attribute")
• rustc nightly-2025-09-08 (1.91.0-nightly (12eb345e5 2025-09-07), per rust-toolchain.toml)
• Z3 5.0.0, default THRUST_SOLVER_ARGS
• All verdicts above were produced by running thrust-rustc, not by inspection.