Incompleteness: calling the same un-annotated `&mut`-taking helper twice from a function that itself takes `&mut` makes the inferred-spec CHC system recursive over a `Mut<T>` datatype argument — trivially-safe programs die on `Timeout`

[coord-e]

Summary

A function whose own parameter is &mut T and which calls the same un-annotated &mut-taking helper twice in sequence cannot be verified: Thrust reports verification error: Timeout(30s) on a six-line, obviously-safe program.

The generated CHC system is satisfiable — z3 answers sat on the very file Thrust hands it, in milliseconds, once one preprocessing option is turned off. So this is not "the property is hard"; it is the shape of the system Thrust emits.

Two independent ingredients have to meet for the hang, and each one alone is harmless:

1. Recursion. One inference template per callee, reused at two sequential call sites, makes the callee's pre-template depend on its own post-template. Two distinct (identical-bodied) helpers, or one annotated helper, give an acyclic system that solves instantly.
2. A datatype-sorted predicate argument. A &mut T parameter is a live local of sort Mut<Int>, so every inferred predicate variable in that function carries an ADT argument. The same program written over a local i32 decomposes into scalar Int arguments only, and solves instantly even though it is just as recursive.

Recursion over Mut<T> is what defeats the solver.

Reproduction

two_calls.rs:

fn incr(x: &mut i32) { *x += 1; }

#[thrust::callable]
fn check(r: &mut i32) {
    let a = *r;
    incr(r);
    incr(r);
    assert!(*r == a + 2);
}

fn main() {}

$ cargo run --quiet -- -Adead_code -C debug-assertions=false two_calls.rs
error: verification error: Timeout(30s)

error: aborting due to 1 previous error

It is not a matter of budget — it still times out at THRUST_SOLVER_TIMEOUT_SECS=180.

v.push(x)-style code is unaffected because the Vec methods carry extern specs; the trigger is a helper the user wrote and did not annotate, which is the common case. The same shape with an extra argument fails identically:

fn add(x: &mut i32, d: i32) { *x += d; }

#[thrust::callable]
fn check(r: &mut i32, d: i32) {
    let a = *r;
    add(r, d);
    add(r, d);
    assert!(*r == a + d + d);   // Timeout(30s)
}

Evidence matrix

All at -Adead_code -C debug-assertions=false, z3 5.0.0, default solver config, wall-clock of the whole thrust-rustc run:

variant of the program above	result	time
one incr(r) call	safe	0.24 s
two incr(r) calls	Timeout(30s)	30.2 s
three incr(r) calls	Timeout(30s)	30.2 s
two calls, to two distinct helpers with identical bodies	safe	0.29 s
two calls, helper annotated #[requires(true)] #[ensures(!x == *x + 1)]	safe	0.27 s
two calls, but both wrapped in an intermediate fn twice(r: &mut i32)	safe	0.29 s
*r += 1; *r += 1; inline, no helper	safe	0.27 s
two calls, weaker assertion *r >= a	safe	0.28 s
let mut v = a; local instead of the &mut parameter, three calls	safe	0.28 s
two calls, wrong assertion *r == a + 3	Unsat (correct)	0.28 s

The wrong-assertion row matters: the failure is one-sided. Thrust still rejects the unsafe program promptly; it is only the provable one it cannot finish.

Root cause

The system is satisfiable; z3's default Horn preprocessing diverges on it

Dumping with THRUST_OUTPUT_DIR gives an 11-clause, 10-predicate system. Feeding exactly that file to z3:

$ z3 fp.spacer.global=true fp.validate=true thrust_output.smt2     # what Thrust passes today
(timeout — no answer in 180 s)
$ z3 thrust_output.smt2                                            # z3 defaults
(timeout)
$ z3 fp.xform.inline_eager=false thrust_output.smt2
sat

fp.xform.inline_eager (eager Horn-clause inlining, on by default) is the single option responsible; fp.spacer.global, fp.validate and fp.xform.slice make no difference either way.

Ingredient 1 — one template per callee, two call sites, hence recursion

incr gets a single inferred pre/post template pair (FunctionTemplateTypeBuilder::build, src/refine/template.rs:601-660). Each call site defines the pre-template, and the body defines the post-template under it, so with the second call site the two become mutually dependent. Predicate dependency edges (body → head) for the repro:

p5 → p0        (c2: first call site)
p0 → p4 → p1   (c1, c0: incr's parameter template, then its body)
p1 → p6        (c3)
p6 → p0        (c4: second call site — closes the loop)

i.e. p0 → p4 → p1 → p6 → p0. With two distinct helpers the graph is acyclic; with an annotated helper there is no template to solve for.

Ingredient 2 — a &mut parameter is an ADT-sorted predicate argument

Because check's parameter has type &mut i32, it is a live local of sort Mut<Int>, and the basic-block templates take it as an ADT argument:

; check(r: &mut i32)                          ; check(a: i32) with a local `let mut v = a`
(declare-fun p5 (A0_Mut<Int> A0_Mut<Int>) Bool)   (declare-fun p5 (Int Int) Bool)
(declare-fun p6 (Int Int Int A0_Mut<Int> Int Int Int) Bool)
                                                  (declare-fun p6 (Int Int Int Int Int Int Int Int Int) Bool)

The local-variable version has the same p0 → p4 → p1 → p6 → p0 cycle and solves in 0.28 s — the only difference is that its predicate arguments are all scalar Int, because a locally-created &mut keeps the referent as a scalar dependency and builds the Mut as a term at the borrow site. src/chc/unbox.rs:81-82 erases Sort::Box but deliberately keeps Sort::Mut, so nothing later flattens it.

Conversely, the two-distinct-helpers variant keeps the A0_Mut<Int> arguments and is fine, because it is acyclic.

So: ADT-sorted predicate arguments are affordable, and recursive templates are affordable, but not together.

Note on the obvious workaround — it is not a blanket fix

Adding fp.xform.inline_eager=false to the z3 defaults in src/chc/solver.rs:118-127 fixes every repro above (and still returns Unsat for the unsafe variants), but it regresses the existing suite:

$ THRUST_SOLVER_ARGS="fp.spacer.global=true fp.validate=true fp.xform.inline_eager=false" \
    cargo run -q -- -C debug-assertions=off tests/ui/fail/iterators/fixed_filter_loop_none.rs
error: verification error: Timeout(30s)      # Unsat with the current defaults

tests/ui/{pass,fail}/iterators/fixed_filter_loop_none.rs and fixed_filter_next_some.rs flip from correct to Timeout under that flag. It trades one class of programs for another, so it is a diagnostic here rather than a proposed patch.

Suggested direction

Attack ingredient 2 rather than the solver flags: represent a &mut T parameter by its two scalar components (current, final) in template dependency positions, the way a locally-created &mut already ends up, instead of one Mut<T> datatype argument. That is also what keeps RustHorn-style encodings inside plain LIA. It would make the &mut-parameter system structurally identical to the local-variable system that already solves in 0.28 s, and would not perturb the iterator tests, which do not depend on how Mut is passed.

If flattening is too invasive, an alternative is to avoid ingredient 1 for straight-line code — instantiate a fresh template per call site of an un-annotated callee (context-sensitivity), which removes the cycle; the two-distinct-helpers row shows the resulting system solves instantly.

Environment

• thrust @ cd6b330
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (x64-glibc-2.39, the version .github/actions/setup-z3 pins), default THRUST_SOLVER_ARGS, default 30 s timeout