Incompleteness: a `#[param(name: { v | φ })]` precondition is silently dropped when the function also has an `#[ensures(..)]`, so trivially-correct functions are rejected

[coord-e]

Summary

When a function is annotated with both a refinement-typed parameter #[thrust_macros::param(name: { v: T | φ })] and a formula postcondition #[thrust_macros::ensures(ψ)], the parameter's refinement φ (its precondition) is dropped — the body is checked as if the parameter were unrefined. As a result Thrust rejects (Unsat) functions that trivially satisfy their contract.

The defect is specific to the param × ensures combination. Each of the other three pre/post pairings keeps the precondition and verifies correctly:

precondition form	postcondition form	verdict	correct
#[param(x: { v: i64 | v > 0 })]	#[ret({ r: i64 | r > 0 })]	safe ✓	safe
#[requires(x > 0)]	#[ensures(result > 0)]	safe ✓	safe
#[requires(x > 0)]	#[ret({ r: i64 | r > 0 })]	safe ✓	safe
#[param(x: { v: i64 | v > 0 })]	#[ensures(result > 0)]	Unsat ✗	safe

#[sig(fn(x: { v: i64 | v > 0 }) -> { r: i64 | r > 0 })] (which desugars to param + ret, no ensures) also verifies. Only the mixed param + ensures form fails.

This is an incompleteness (a safe program is rejected), not a soundness hole — see "Soundness is preserved" below.

Reproduction

repro.rs — the most trivial refinement example: assume x > 0, return x, promise result > 0.

//@compile-flags: -C debug-assertions=off
#[thrust_macros::param(x: { v: i64 | v > 0 })]
#[thrust_macros::ensures(result > 0)]
fn f(x: i64) -> i64 { x }
fn main() {}

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

Replacing #[ensures(result > 0)] with #[ret({ r: i64 | r > 0 })] — an equivalent postcondition — makes it verify:

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

The dropped fact is exactly the parameter precondition

Keeping everything else fixed and varying only the ensures body pins the cause to the missing precondition:

ensures(..)	body	verdict	why
ensures(result > 0)	{ x }	Unsat ✗	needs x > 0, which is dropped
ensures(result > 0)	{ 5 }	safe ✓	5 > 0 holds without the precondition
ensures(result == x)	{ x }	safe ✓	structural, does not need the precondition
ensures(x > 0)	{ x }	Unsat ✗	the postcondition restates x > 0, which is unprovable because it is not assumed
ensures(1 > 0)	{ x }	safe ✓	trivially true

The ensures(x > 0) row is the clincher: Thrust cannot prove x > 0 in the postcondition even though #[param(x: { v | v > 0 })] declares exactly that — the parameter refinement is never assumed.

Adding a redundant #[requires(true)] does not help (still Unsat): the param precondition is dropped regardless.

SMT evidence

Emitting the CHCs (THRUST_OUTPUT_DIR) for the failing vs. the working #[ret] form, the only difference is clause c1, which installs the parameter-context predicate p2 from the declared precondition:

; FAILING  — #[param(x:{v|v>0})] + #[ensures(result>0)]
(assert (forall ((v0 Int) (v1 Int)) (=> (and  true)      (p2 v1 v1))))
;                                             ^^^^ precondition dropped

; WORKING  — #[param(x:{v|v>0})] + #[ret({r|r>0})]
(assert (forall ((v0 Int) (v1 Int)) (=> (and  (> v1 0))  (p2 v1 v1))))
;                                             ^^^^^^^ precondition kept

The panic/return obligation c0 is identical in both:

(assert (forall ((v0 Int) (v1 Int) (v2 Int) (v3 Int) (v4 Int))
  (=> (and (= v0 v1) (= v2 v1) (p2 v2 v1) (= v3 v2) (= v4 v0) (not (> v4 0))) false)))

With c1's antecedent weakened to true, p2 holds for every v1 (including v1 <= 0), so c0 has a model with result <= 0, contradicting (> v4 0) → the system is unsat. The #[requires(x>0)] + #[ensures(result>0)] form produces the same c1 as the working #[ret] form (antecedent (> v1 0)), confirming the loss is unique to param × ensures.

Soundness is preserved

The ensures postcondition is still enforced — only the param precondition is lost — so this only over-rejects, it does not accept unsafe programs:

• #[param(x:{v|v>0})] + #[ensures(result < 0)], body { x } → correctly Unsat (body does not satisfy the postcondition).
• #[param(x:{v|v>0})] + #[ensures(result > 0)], body { 5 } → safe (postcondition met).

Dropping the precondition makes the body check stricter, so no panicking program is verified as safe through this path.

Root cause (hypothesis)

The pre/post annotations are assembled in LocalDefAnalyzer::def_ty (src/analyze/local_def.rs:285-300): requires → builder.param_refinement(..), ensures → builder.ret_refinement(..), and param/ret/sig → builder.refinement_at(position, ..) (which populates param_rtys / ret_rty in src/refine/template.rs). FunctionTemplateTypeBuilder::build (src/refine/template.rs:603) does read param_rtys[idx] for annotated params, so the loss appears to happen in how the resulting parameter refinement is turned into the entry constraint c1 once an ensures-supplied ret_rty (via ret_refinement, template.rs:546) is also present — the refinement_at(Param(..)) refinement survives a refinement_at(Return, ..) (the ret case) but not a ret_refinement(..) (the ensures case). The two return-side entry points constructing ret_rty differently is the most likely place to look.

Expected behavior

#[param(x: { v | φ })] and #[ensures(ψ)] should compose: the body must be checked assuming φ on the parameter and obligated to establish ψ on the result. repro.rs above should verify as safe, matching the equivalent #[param] + #[ret] and #[requires] + #[ensures] forms. A tests/ui/pass case mixing param + ensures (and a fail twin whose body violates the postcondition) would guard the composition.

Relation to existing issues

• Incompleteness: refinement on a reference's pointee (&{ v | φ } / &mut { v | φ }) in parameter position is not assumed by the callee #166 is also an "annotated precondition not assumed" incompleteness, but for a reference's pointee refinement (&{v|φ} / &mut {v|φ}) in parameter position. This report is about a plain value refinement #[param(x: { v: i64 | v > 0 })] on a non-reference parameter, and it is triggered specifically by the presence of an #[ensures(..)]; the #[param] + #[ret] form of the same signature verifies, so it is a distinct annotation-composition defect.
• 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): the value > 0 here is small and in range, and the loss is purely in annotation assembly.

Environment

• thrust @ 6953863 (Merge pull request #185 …syn-3.0.2)
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default (spacer) configuration
• Confirmed by running thrust-rustc (not inspection-only): repro.rs is reported Unsat.