Refinements on `Box` (own-pointer) pointee in return position are not enforced — unsound

[coord-e]

Summary

A refinement on a Box (own pointer) pointee in return position — Box<{v | v > 0}> — is parsed and built into the function type correctly, but the corresponding subtyping/CHC obligation is generated incorrectly, so it is not enforced. This is a genuine verification-logic bug (unsound), not an annotation-semantics issue.

Enum / datatype nested type-argument refinements (Opt<{v | v > 0}>) are fine — see "Not a bug" below. (An earlier revision of this issue incorrectly flagged the enum case; that part was an annotation-semantics artifact, not unsoundness.)

Repro: genuine unsoundness (Box pointee)

//@compile-flags: -C debug-assertions=off

#[thrust_macros::param(n: { v: i32 | v > 0 })]   // satisfiable precondition
#[thrust_macros::ret(Box<{ v: i32 | v > 0 }>)]
fn mk(n: i32) -> Box<i32> { Box::new(-1) }        // ignores n, always returns -1

fn main() {
    let b = mk(7);        // precondition 7 > 0 holds, so mk is callable
    assert!(*b > 0);      // *b == -1, so this is FALSE
}

• Expected: verification failure (Unsat).
• Actual: verifies successfully (exit 0, no Unsat).

Because the precondition n > 0 is satisfiable and the body ignores n, no inferred precondition can "rescue" this — the body unconditionally returns -1, which violates Box<{v > 0}>. The obligation is simply not generated/enforced correctly.

The bug is specific to the Box pointee, not to zero-arg functions or nested positions in general:

function	body	called + asserted	result
fn h() -> i32 ret {r > 0} (top-level)	-1	yes	Unsat ✅
fn mk(n: i32) -> Opt<i32> ret Opt<{v > 0}> (enum arg)	Some(-1)	yes	Unsat ✅
fn mk(n: i32) -> Box<i32> ret Box<{v > 0}> (box pointee)	Box::new(-1)	yes	accepted ❌

The constraint also misfires in the opposite direction (incompleteness): fn mk(x: i32) -> Box<i32> { Box::new(x) } with param x > 0 / ret Box<{v > 0}> is wrongly rejected (Unsat) though it is valid. So the box-pointee obligation appears to relate the wrong term rather than merely being absent.

The function type itself is built correctly:

register_def ...::mk rty=({ () | p0 }) → own { int |  ν > 0 }

Likely area: subtyping / CHC generation for own pointer pointees in return-value relating (src/rty/subtyping.rs, src/analyze/basic_block.rs return-place handling), and/or how the Box::new extern-spec post-state (result == box(arg)) is related to a pointee refinement.

Not a bug: enum/datatype nested args (annotation-semantics note)

Opt<{v | v > 0}> is enforced soundly. A function annotated only on the return (#[thrust::ret(Opt<{v>0}>)]) with an unannotated parameter appears to "verify in isolation":

#[thrust::ret(Opt<{v: int | v > 0}>)]
fn g(x: i64) -> Opt<i64> { Opt::Some(x) }   // verifies on its own

…but this is because an unannotated parameter in a partially-annotated function receives a fresh predicate variable (inferred precondition), not true. The solver infers g's precondition to x > 0, so g is internally consistent, and any violating call is correctly rejected:

fn main() { let r = g(-5); match r { Opt::Some(i) => assert!(i > 0), Opt::None => {} } }
// => verification error: Unsat   (correctly rejected)

So the verifier is sound here. Possible improvement (separate from the bug above): give unannotated parameters of a partially-annotated function the true refinement instead of a fresh pvar, so such functions are checked against an unconstrained input rather than an inferred precondition.

Aside (separate, minor)

The legacy parse_rty parser panics on Box<{..}> syntax (#[thrust::ret(Box<{v: int | v > 0}>)]) at src/analyze/local_def.rs:97, so the box-pointee gap above is currently only reachable through the thrust_macros annotations (which build the equivalent type).

Environment

• Z3 4.13.0; nightly per rust-toolchain.toml. Reproduced on e25bfb0.

[coord-e]

Investigation findings

Reproduced on e25bfb0 (z3 4.16). The minimal repro is indeed unsound (exit 0 where Unsat is expected), but tracing the CHC generation shows the root cause is not the nested-argument subtyping layer.

Nested-arg subtyping/CHC generation is actually correct

The nested refinement survives into relate_sub_type (expected = Opt <{ int | ν > 0 }>) and the generated CHC contains the correct obligation. For the repro the dumped clause is:

; c1
(... (= v0 (Opt.Some v1)) (p3 v2 v1) ... (p4 v5 v1 v2) (not (> v5 0)) ) => false

The (not (> v5 0)) => false is exactly the nested v > 0 obligation, wired through p3/p4 back to p0 (the refinement of param x).

The unsoundness is an unpinned entry precondition, and it affects depth-0 too

p0 (x's precondition) is a free predicate with no head/lower-bound clause, so the solver picks p0 ≡ false and the whole obligation becomes vacuous. This happens because a function annotated with only #[thrust::ret(..)] (no requires, never called) gets an inferred template precondition that is never pinned to true.

This is not nested-specific. Matched pairs:

| Scenario | depth-0 ret({v|v>0}) | nested ret(Opt<{v|v>0}>) |
|---|---|---|
| uncalled, thrust::ret only | exit 0 (unsound) | exit 0 (unsound) |
| called from main | Unsat ✅ | Unsat ✅ |
| precondition pinned via requires_path | Unsat ✅ | Unsat ✅ |

e.g. fn g() -> i64 { -1 } with #[thrust::ret({v|v>0})] and fn main(){} also wrongly passes. Existing depth-0 tests don't expose this because they all fully annotate via requires/ensures/formula_fn (precondition becomes concrete true, generating the pinning clause true => p4) or call the function. So nested refinements are enforced once the function is exercised or its precondition is pinned.

The Box<{..}> parse panic is a real, separate bug

#[thrust::ret(Box<{v|v>0}>)] panics at src/analyze/local_def.rs:97. Root cause is src/annot.rs:1065: the Box arm parses its pointee with parse_ty(), which can't accept a {..} refinement, whereas the enum arm (line 1077) correctly uses parse_rty(). One-line fix: parse the Box pointee with parse_rty().

Suggested split

1. Unsoundness: decide whether unannotated parameters on an analyzed verification-root def should be checked against true (pinned), rather than an inferable free predicate that can collapse to false. This is a verification-semantics decision, not a fix in subtyping.rs.
2. Box parse panic: straightforward parse_ty → parse_rty change in src/annot.rs:1065.

---

Generated by Claude Code