Unsound: a crate with no `main` (any `--crate-type lib`/`rlib`/…) gets no entry-point anchor, so every inferred precondition is discharged as `false` and the whole crate — `pub` API functions that always panic included — verifies as `safe`

[coord-e]

Summary

crate_::Analyzer::assert_callable_entry anchors exactly one definition: tcx.entry_fn(()), i.e. the crate's main. It is the only place that ever emits a fact clause (true ⟹ p) for an inferred parameter precondition.

A library crate has no entry function. Nothing else in the generated CHC system constrains any inferred precondition predicate from below, so the solver takes every one of them to be false, every body obligation becomes vacuous, and the system is trivially SAT. Thrust exits 0 with no diagnostic for a library whose public API provably panics on every call.

The bodies are analyzed and the panic obligation is emitted — it is just discharged vacuously. Compiling the identical source as a binary with a main that calls the same function is correctly rejected.

Since a real-world Rust crate is a library (src/lib.rs) far more often than a binary, this means pointing thrust-rustc at real-world code silently certifies it. The vacuity also cascades: a private helper that is called from a pub function is equally unverified, because the caller's own precondition is unanchored.

Minimal reproduction

min.rs:

pub fn f() {
    let v: Vec<i64> = Vec::new();
    let _ = v[0]; // index out of bounds: this function panics on every call
}

$ cargo run -- -Adead_code -C debug-assertions=false --crate-type lib min.rs && echo safe
safe

The same body, in a crate that has a main calling it, is correctly rejected:

// min_bin.rs
pub fn f() {
    let v: Vec<i64> = Vec::new();
    let _ = v[0];
}
fn main() { f(); }

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

The vacuity cascades through the intra-crate call graph

A pub entry point calling a private helper is not saved by the call site — the caller is unanchored too, so the callee's precondition stays unconstrained:

// cascade.rs  --crate-type lib  ->  safe   (BUG)
pub fn get(v: &Vec<i64>, i: usize) -> i64 { v[i] }

pub fn run() -> i64 {
    let v: Vec<i64> = Vec::new();
    get(&v, 0) // `get`'s `requires(index < length)` is violated
}

// same functions + `fn main() { let _ = run(); }`  (bin)  ->  error: verification error: Unsat   (correct)

// private-helper form, --crate-type lib  ->  safe   (BUG)
fn helper() -> i64 { let v: Vec<i64> = Vec::new(); v[0] }
pub fn api() -> i64 { helper() }

Observed vs. expected

program	crate type	Thrust	expected
pub fn f() { Vec::<i64>::new()[0]; }	lib / rlib / staticlib / cdylib	safe	error
same + fn main() { f(); }	bin	error	error
fn main() { assert!(false); }	lib	safe	error
fn main() { assert!(false); }	bin	error	error
pub fn get(..) {..} + pub fn run() { get(&empty, 0) }	lib	safe	error
fn helper() {..panics..} + pub fn api() { helper() }	lib	safe	error
#[thrust::callable] pub fn f() { assert!(false); }	lib	error	error
#[requires(true)] #[ensures(result == n+1)] pub fn f(n: i64) -> i64 { n + 2 }	lib	error	error

The last two rows locate the defect precisely: a function that carries a concrete contract (requires/ensures/callable) is checked normally even in a library, because its precondition is the literal true rather than a predicate variable. Only functions whose precondition is inferred — i.e. every unannotated function, which is the common case — go vacuous.

Root cause

src/analyze/crate_.rs:242:

fn assert_callable_entry(&mut self) {
    if let Some((def_id, _)) = self.tcx.entry_fn(()) {
        // we want to assert entry function is safe to execute without any assumption
        ...
        for param_ty in entry_ty.params {
            let cs = builder.clone().with_value_var(&param_ty.ty).head(param_ty.refinement);
            self.ctx.extend_clauses(cs);   // <-- the only `true ⟹ p` fact in the system
        }
    }
}

tcx.entry_fn(()) is None for every non-bin crate type, so the whole function is a no-op and no fact clause is ever emitted.

An unannotated function is registered with a template precondition (RUST_LOG=info, pub fn f() in a lib crate):

refine_fn_def: register_def def_id=..::f rty=({ () |  p0 }) → { () |  p1 }
                                                        ^^ inferred, never anchored

The emitted CHC systems for cascade.rs show the difference directly (THRUST_OUTPUT_DIR). As a library, p2 — run's parameter precondition — occurs only in a hypothesis position:

; c8   (lib)
(assert (=> (and p2 true) p6))
;; ... and nowhere else. No `(assert (=> true p2))`.

so p2 := false propagates: p6 := false, which kills p0/p4, which makes the panic obligation

; c0  ... (=> (and ... (p4 ...) (not (< v6 (tuple_proj<...>.1 v4)))) false)

vacuous, and the system is SAT.

Compiled as a binary the very same run gains the anchor clause emitted by assert_callable_entry, and the chain becomes real (UNSAT):

; c12
(assert (=> (and p4 true) p11))
; c13
(assert (=> (and  true) p4))     ;; <-- anchor for `main`'s parameter precondition

So this is not "bodies are skipped" — the obligations are generated correctly; there is simply no root to make them non-vacuous.

Scope / when it bites

• Every crate type other than bin: lib, rlib, staticlib, cdylib (all confirmed safe on the minimal repro).
• Every function whose precondition is inferred, which is every function without requires/ensures/callable — including private helpers reachable from pub API, since the vacuity propagates backwards along the call graph.
• Failure is silent: exit status 0, no warning that nothing was anchored, so a user reasonably reads the result as "verified".
• This is the setting Support multi-crate projects (cargo) #255 (cargo/multi-crate) is heading towards: cargo builds src/lib.rs as a library, so a cargo integration built on the current behaviour would report safe for every library crate.

Workaround

Annotate the crate's API entry points with #[thrust::callable] (or requires/ensures), which replaces the inferred precondition with a concrete one and re-anchors everything reachable from it (rows 7–8 of the table).

Suggested direction

Anchor more than tcx.entry_fn(()). Some options, roughly in increasing order of aggressiveness:

1. Also anchor every function explicitly marked #[thrust::callable] — today callable gets its concrete true precondition from the annotation path, so it happens to work, but it is not routed through assert_callable_entry, and making that explicit would keep the "entry point" notion in one place.
2. When the crate has no entry function, anchor every externally reachable definition (tcx.effective_visibilities / exported items) — a library's pub API is precisely the set of functions callable "without any assumption" from outside, which is the same justification the existing main anchor uses.
3. At minimum, emit a diagnostic when the analysis anchors nothing, so safe is never printed for a crate where no obligation could have failed.

Distinct from existing issues

• Not 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. 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 is about the sig/ret/param front-end leaving an explicitly declared signature's unspecified parameters as templates, and it states that template inference "is the intended behavior for unannotated functions" and that the requires/ensures front-end "is checked correctly". Both hold here: the functions in this report carry no annotation at all, and 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's suggested fix (default the unspecified parameters of sig/ret/param-annotated functions to concrete true) would not change any row of the table above. The defect here is upstream of the annotation front-ends — which definitions get anchored as entry points at all (assert_callable_entry), not how one function's declared signature is built.
• Not Unsound: an uncalled generic function (a type param appears in its signature) has its body skipped entirely, so a #[thrust::callable] entry point whose body always panics — or whose body violates its own ensures — verifies as safe #200. There the body of an uncalled generic function is never analyzed (deferred def, concrete_def_ty is None). Here the bodies are analyzed and the clauses are emitted — including the panic obligation quoted above — they are merely satisfiable. Unsound: an uncalled generic function (a type param appears in its signature) has its body skipped entirely, so a #[thrust::callable] entry point whose body always panics — or whose body violates its own ensures — verifies as safe #200's table also asserts that "a plain uncalled non-generic helper ... Thrust does verify"; that row uses #[ensures(..)], and the unannotated non-generic case does not hold in a crate with no main.
• Not Support multi-crate projects (cargo) #255. Support multi-crate projects (cargo) #255 asks for cargo/multi-crate support; this is a soundness bug in single-crate analysis that a cargo front-end would inherit, and it reproduces with a plain thrust-rustc --crate-type lib invocation today.
• Not a numeric-range issue: the repro is an out-of-bounds index on an empty Vec (and assert!(false)), independent of any integer bound.

Environment

• thrust @ 2bf022d
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, repository-default THRUST_SOLVER_ARGS. Solver-independent: the library system is SAT because it lacks a fact clause, not because of solver strength.