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)

[coord-e]

Summary

A function whose refinement signature is declared with #[thrust_macros::sig(..)], #[thrust_macros::ret(..)], or #[thrust_macros::param(..)] (i.e. via the refinement_path mechanism), but not with requires/ensures/callable, has an unspecified parameter precondition modeled as an inference template predicate rather than as the declared default true. When such a function is not called anywhere in the analyzed crate, nothing constrains that template from below, so the CHC solver discharges the body's proof obligations vacuously by choosing an unsatisfiable precondition. As a result Thrust reports the crate safe even though the function's body provably does not inhabit its declared refinement type, and even body-internal assert!s are skipped.

The equivalent spec written with #[ensures(..)] is checked correctly, so this is a discrepancy between the two annotation front-ends, and it defeats the entire purpose of writing a refinement signature to check a function.

This is a soundness bug in the refinement type checker's per-function (modular) guarantee: a #[sig]-annotated definition is accepted against a signature its body does not satisfy. (For a self-contained program whose only offender is dead code, the whole-program safe verdict is technically correct — but the checker's contract that "a #[sig]-annotated function that verifies inhabits the declared type" is broken, which is exactly the guarantee library-style verification and the sig/ret/param surface syntax exist to provide.)

Minimal reproduction

repro.rs:

#[thrust_macros::sig(fn(a: i32) -> { r: i32 | r > 0 })]
fn f(a: i32) -> i32 { a }   // returns its argument; f(-5) == -5, which is NOT > 0

fn main() {}

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

f is reported as satisfying fn(a: i32) -> { r: i32 | r > 0 }, but it does not: f(-5) == -5. The identical #[ret(..)] spelling behaves the same way, while the equivalent #[ensures(..)] is (correctly) rejected:

// (a) ret  -> verifies as `safe`  (BUG)
#[thrust_macros::ret({ r: i32 | r > 0 })]
fn f(a: i32) -> i32 { a }

// (b) ensures -> `error: verification error: Unsat`  (correct)
#[thrust_macros::ensures(result > 0)]
fn f(a: i32) -> i32 { a }

The body is not analyzed at all in the buggy case — even an unconditional in-body assertion is silently accepted:

// verifies as `safe`, despite `assert!(a > 0)` failing for a <= 0  (BUG)
#[thrust_macros::ret({ r: i32 | r > 0 })]
fn f(a: i32) -> i32 { assert!(a > 0); a }

fn main() {}

Observed vs. expected

program	Thrust	expected
#[sig(fn(a:i32)->{r:i32|r>0})] fn f(a:i32)->i32 { a }, uncalled	safe	error (a may be ≤ 0)
#[ret({r:i32|r>0})] fn f(a:i32)->i32 { a }, uncalled	safe	error
#[ret({r:i32|r>0})] fn f(a:i32)->i32 { assert!(a>0); a }, uncalled	safe	error
#[ensures(result>0)] fn f(a:i32)->i32 { a }, uncalled	error	error
#[param(a:{x:i32|true})] #[ret({r:i32|r>0})] fn f(a:i32)->i32 { a }, uncalled	error	error
#[sig(fn(a:i32)->{r:i32|r>0})] fn f(a:i32)->i32 { a } used in the crate	error	error

Root cause

The declared type Thrust builds for f in the buggy case has an uninterpreted predicate template on the parameter. With RUST_LOG=info, the two front-ends register visibly different types for the same intended spec:

# sig/ret only:
register_def def_id=..::f  rty=({ int |  p0 ν }) → { int |  ν > 0 }
#                                     ^^^^^ parameter precondition is a template predicate p0

# ensures (final registration, via the requires/ensures companion):
register_def def_id=..::f  rty=(int) → { int |  true∧  ν > 0 }
#                               ^^^ parameter precondition is the concrete `true`

For the sig/ret type, checking the body emits (roughly)

∀ a. p0(a) ∧ (ret = a)  ⟹  a > 0        i.e.   p0(a) ⟹ a > 0

with p0 a free predicate variable. Because f is never called, no clause ever requires p0 to be inhabited, so the solver simply takes p0 := λx. false (or λx. x > 0), the implication is vacuous, the system is SAT, and Thrust prints safe. With the ensures front-end the parameter is the concrete true, so the obligation is true ⟹ a > 0, which is UNSAT — correctly rejected.

The template is introduced in FunctionTemplateTypeBuilder::build (src/refine/template.rs:603-632): a parameter that has neither an explicit per-parameter refinement (param_rtys) nor a param_refinement falls into the for_template(..) branch and gets a fresh predicate variable:

// src/refine/template.rs (build loop)
let param_rty = self.param_rtys.get(&idx.into()).cloned().unwrap_or_else(|| {
    if idx == self.param_tys.len() - 1 {
        if let Some(param_refinement) = &self.param_refinement {
            /* concrete precondition (requires/ensures/callable path) */
        } else {
            self.inner.for_template(self.registry).with_scope(&builder)
                .build_refined(param_ty.ty)   // <-- fresh predicate p0 for the last param
        }
    } else if self.param_refinement.is_some() {
        rty::RefinedType::unrefined(/* concrete `true` */)
    } else {
        rty::RefinedType::unrefined(self.inner.for_template(..).build(param_ty.ty)) // <-- template
    }
});

expected_ty (src/analyze/local_def.rs:238-309) only sets builder.param_refinement(..) when a requires/ensures/callable annotation is present (lines 285-297); the sig/ret/param path installs refinements only at the explicitly declared positions via builder.refinement_at(..) (line 298-300) and leaves every other parameter to the for_template branch above. So a declared return refinement is checked against an inferred parameter precondition instead of the declared/default true, and that inferred precondition can be made vacuous.

Template-based inference for parameters is the intended behavior for unannotated functions. The defect is that it is also used for the unspecified parameters of a function whose signature the user has explicitly declared with sig/ret/param: the declared postcondition is then not actually enforced.

Scope / when it bites

• Reproduces whenever the offending function is not used anywhere in the analyzed crate. Any intra-crate use (direct call, fn pointer, or passing it to a higher-order function) adds a clause that constrains the template, which forces the body obligation to become real and the violation is then caught (see the last two table rows). So the whole-program safe verdict for a self-contained program is not itself wrong — the offender is dead code.
• It is a genuine problem for the use cases the sig/ret/param syntax targets: verifying a function against a declared contract as documentation/regression protection, and verifying library-style code whose annotated API functions are consumed by callers outside the analyzed set. In those settings Thrust silently certifies a signature the body does not satisfy.
• param-annotating every parameter (so no template remains) avoids it, as does using requires/ensures/callable.

Suggested direction

For a function that carries an explicit refinement-type annotation (sig/ret/param), unspecified parameter preconditions should default to the concrete true (unrefined) rather than to an inference template — mirroring how requires/ensures/callable produce a fully concrete signature — so that the declared return/postcondition is verified under the declared (default-true) precondition. Equivalently, presence of any refinement_path annotation could mark the function as "declared" so its body is checked against the declared type instead of an inferred one.

Notes

• Distinct from Incompleteness: function-type subtyping in relate_sub_type proves the return obligation without assuming the parameters' preconditions #128 (that is incompleteness in the nested Type::Function subtyping arm dropping parameter hypotheses); this is at the top-level function-declaration/template-construction level and is an accepts-bad (unsound-checker) direction.
• Not a numeric-range issue: the refinement r > 0 is violated at small values (e.g. -5), independent of i32 bounds.

Environment

• thrust @ af7cd99
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 4.13.0 (default THRUST_SOLVER_ARGS)