Unsound: a `#[param(name: { v | φ })]` precondition combined with `#[ensures(..)]` is dropped at call sites too, so a `#[thrust::trusted]` function with a violated precondition verifies panicking programs as `safe`

[coord-e]

Summary

This is the soundness consequence of the annotation-assembly defect reported in #191 (#[param(x: { v | φ })] + #[ensures(ψ)] silently drops the parameter precondition φ).

#191 concludes "Soundness is preserved", reasoning that dropping φ only makes the body check stricter, so no panicking program can slip through. That argument holds only for functions whose body Thrust actually checks. For a #[thrust::trusted] function the body is not analyzed, so the dropped precondition is never enforced anywhere — in particular it is not enforced at call sites. A caller may then violate φ while still assuming the postcondition ψ, and Thrust verifies a program that panics at runtime as safe.

The same reasoning applies to any function whose contract is assumed rather than checked (#[thrust::trusted], and by extension the extern_spec mechanism), which is exactly how external/unverifiable operations are modeled — so this is a real soundness hole, not a corner case.

Reproduction

repro.rs — a trusted function with a correct contract (x > 0 ⟹ result > 0, body returns x), called with a value that violates the precondition:

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

fn main() {
    let r = pos(-5);   // precondition `x > 0` is violated
    assert!(r > 0);    // Thrust assumes the postcondition `result > 0`
}

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

But the program panics at runtime — #[thrust::trusted] affects only Thrust's analysis, not codegen, so pos(-5) returns -5 and the assertion fails:

$ # equivalent program with the (analysis-only) annotations stripped
$ cat rt.rs
fn pos(x: i64) -> i64 { x }
fn main() { let r = pos(-5); assert!(r > 0); }
$ rustc rt.rs -o rt && ./rt
thread 'main' panicked at rt.rs:4:5:
assertion failed: r > 0

safe for a program that unconditionally panics ⇒ unsound.

The same happens with a non-constant argument (so it is not constant-folding): a #[thrust::callable] fn caller(a: i64) { let r = g(a); assert!(r > 0); } calling the trusted g above also verifies as safe, even though a is unconstrained.

The precondition form matters — matches #191's trigger

Swapping the refinement-style #[param] precondition for the equivalent formula-style #[requires] makes Thrust correctly reject the precondition-violating call:

#[thrust::trusted]
#[thrust_macros::requires(x > 0)]      // formula-style instead of #[param]
#[thrust_macros::ensures(result > 0)]
fn pos(x: i64) -> i64 { x }
fn main() { let r = pos(-5); assert!(r > 0); }

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

Soundness matrix for a #[thrust::trusted] function called as pos(-5); assert!(r > 0) (should always be Unsat, because the call violates the declared precondition):

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

(The #[param] + #[ret] and #[sig(..)] forms on a trusted function with a call currently panic at src/analyze/crate_.rs:115 — a separate lack-of-support issue — so they are omitted from the matrix.)

The param × ensures cell is exactly the combination #191 identifies as dropping the precondition. #191 observes it as over-rejection (the checked body loses the assumption); this report shows the very same dropped fact is also the call-site obligation, which is what turns it into unsoundness once the body is not checked.

Why #191's "Soundness is preserved" argument does not cover this

Per #191's SMT evidence, the entry clause that installs the parameter-context predicate is weakened from

(assert (forall ((v0 Int) (v1 Int)) (=> (and (> v1 0)) (p2 v1 v1))))   ; precondition kept (#[ret] form)

to

(assert (forall ((v0 Int) (v1 Int)) (=> (and  true)     (p2 v1 v1))))   ; precondition dropped (#[ensures] form)

So p2 (the parameter refinement predicate) holds for every v1, including v1 <= 0. #191 notes this makes the return/panic obligation c0 (from the body) harder to satisfy — the over-rejection. But p2 is also the predicate the caller must establish to satisfy the subtyping obligation arg_type <: param_type at the call site. With p2 provable for all values, that call-site obligation becomes vacuous: the caller is no longer required to establish φ.

• For a checked function, c0 from its body keeps the system unsat on a bad body ⇒ observable only as over-rejection (Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected #191).
• For a trusted function, there is no c0 from a body, so nothing rejects the vacuous call-site obligation, and the caller freely assumes ψ after violating φ ⇒ unsound.

Fixing the #191 root cause (keeping the #[param] precondition in the entry clause when an #[ensures] is also present) fixes both manifestations. I'm filing separately because the soundness classification changes the severity and directly contradicts the "Soundness is preserved" section of #191.

Environment

• thrust @ 6953863 (Merge pull request #185 …syn-3.0.2) — same commit referenced by Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected #191
• 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 safe (exit 0); the #[requires] variant is reported Unsat.