Incompleteness: a refinement on a generic type argument in `#[param]` position is dropped for multi-variant enums, so the payload refinement is never assumed in the callee

[coord-e]

Summary

A refinement written on a generic type argument of an enum in #[thrust_macros::param(..)] position (e.g. o: Opt<{ v: i64 | v > 0 }>) is silently dropped when the enum has more than one variant. The refinement predicate for the payload is still generated and defined in the emitted CHC system, but it is never applied as a hypothesis to the destructured payload, so the callee cannot use the fact that the payload is refined. Safe programs are therefore rejected (verification error: Unsat).

The single-variant case works correctly (the payload predicate is applied), so the discrepancy is specifically about the variant count of the generic enum.

Reproduction (the bug)

//@compile-flags: -C debug-assertions=off
pub enum Opt<T> { Som(T), Non }
impl<T> thrust_models::Model for Opt<T> { type Ty = Self; }

// Precondition: if `o` is `Som(x)`, then `x > 0`.
#[thrust_macros::param(o: Opt<{ v: i64 | v > 0 }>)]
fn f(o: Opt<i64>) {
    match o {
        Opt::Som(x) => { assert!(x > 0); } // guaranteed by the precondition
        Opt::Non => {}
    }
}

fn main() {
    f(Opt::Som(5)); // 5 > 0 satisfies the precondition; never panics
}

• True runtime behavior: never panics. Opt::Som(5) satisfies the precondition Opt<{ v | v > 0 }>, and inside f the only reachable assert!(x > 0) holds because x == 5.
• Thrust verdict: error: verification error: Unsat (rejected). WRONG — this is an incompleteness.

Control that isolates it (single variant → correct)

Identical in every respect except the enum has one variant:

//@compile-flags: -C debug-assertions=off
pub enum One<T> { V(T) }
impl<T> thrust_models::Model for One<T> { type Ty = Self; }

#[thrust_macros::param(o: One<{ v: i64 | v > 0 }>)]
fn f(o: One<i64>) {
    match o { One::V(x) => { assert!(x > 0); } }
}

fn main() { f(One::V(5)); }

• Thrust verdict: safe. Correct. The only difference from the bug case is single- vs. multi-variant, so the payload refinement is being lost specifically for multi-variant generic enums.

Additional observations from narrowing:

• A two-variant enum where both variants carry T (enum Two<T> { A(T), B(T) }, asserting on the payload in each arm) is also rejected — so it is the variant count, not the nullary Non.
• The same multi-variant enum whose body does not rely on the payload refinement (e.g. Opt::Som(_x) => assert!(true)) verifies safe — so matching itself works; only the refinement is dropped.
• The built-in Option<{ v: i64 | v > 0 }> in the same position is dropped identically.
• Caller-side enforcement is still sound: passing a payload that violates the precondition is correctly rejected, so this is purely an incompleteness, not an unsoundness.

Root cause (SMT-level evidence)

Dumping the generated CHC (THRUST_OUTPUT_DIR=…) for the two programs above makes the difference precise.

Single variant — the precondition predicate p3 (defined as v1 > 0) is applied to the payload v1 in the hypothesis of the assert!-obligation clause, so the obligation is discharged:

; definition of the payload precondition
(assert (forall ((v0 A0_One<Int>) (v1 Int)) (=> (and (> v1 0)) (p3 v1))))
; assert!(x > 0) obligation — note (p3 v1) in the antecedent
(assert (forall (... (v1 Int) ...)
  (=> (and (p3 v1) (= (One.V<Int> v1) v4) (= v5 v1) (= v6 (> v5 0)) ... (= v6 false) ...)
      false)))

With (p3 v1) ⟹ v1 > 0, the antecedent v6 = (v1 > 0) ∧ v6 = false is contradictory, so the clause is vacuously valid → safe.

Multi variant — the analogous payload predicate p5 is defined but never used as a hypothesis anywhere. The Som-arm payload v1 is left completely unconstrained:

; p5 is defined ...
(assert (forall ((v0 A0_Opt<Int>) (v1 Int)) (=> (and (> v1 0)) (p5 v1))))
; ... but the assert!(x > 0) obligation clause never mentions p5:
(assert (forall (... (v1 Int) ...)
  (=> (and (= (Opt.Som<Int> v1) v7) (= v2 v1) (= v8 v2) (= v9 (> v8 0))
           (= v4 (datatype_discr<A0_Opt<Int>> v3)) ... (= v4 0) ...
           (= v9 false) ...)
      false)))

Because nothing constrains v1, v9 = (v1 > 0) may be false, the antecedent is satisfiable, and the false head is unprovable → Unsat. (p5, and the similarly-declared p6/p8, are emitted but orphaned.)

So the type-argument refinement does reach the type of the payload field — install_refinement_at installs it into EnumType.args (src/rty.rs:1656), and subst_ty_params/instantiate_ty_params correctly merge an arg's refinement into a Type::Param field (src/rty.rs:1800, the Type::Param branch does self.refinement.push_conj(refinement)). The refinement is nonetheless not wired as a hypothesis on the payload when a multi-variant enum parameter is bound and destructured. The relevant machinery is Env::bind_enum (src/refine/env.rs:741), which builds each variant's field binding with instantiate_ty_params(ty.args.clone()) guarded by discr == variant.discr (src/refine/env.rs:766-778) and then assembles the matcher_pred assumption (:781-819); for multi-variant enums the payload's precondition predicate is not connected to the destructured value in the emitted clauses, whereas for the single-variant representation it is.

Why this is not an already-filed / excluded issue

• Not a panic / unimplemented!: raw output is exactly error: verification error: Unsat; no panicked at / not implemented.
• Not numeric-range/overflow: the only values involved are 5 and > 0; no MAX/MIN/casts.
• Not a solver timeout/unknown: it is a deterministic Unsat (reproduced repeatedly), and the single-variant control is a deterministic safe.
• The function is called in main, so it is 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 (uncalled sig/ret/param body).
• It uses #[param] only, with no #[ensures], so it is not Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected #191 (param dropped when ensures is present) — and unlike Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected #191 the single-variant version verifies correctly.
• It concerns a user-defined multi-variant generic enum's type-argument refinement, distinct from Incompleteness: refinement on a reference's pointee (&{ v | φ } / &mut { v | φ }) in parameter position is not assumed by the callee #166 (reference-pointee refinements &{v|φ} / &mut{v|φ}), and unrelated to the enum-discriminant soundness items (Unsound: enum variants after an explicit discriminant get the wrong datatype_discr value, making match arms vacuously verify #126 explicit discriminants; Unsound: negative SwitchInt match targets are sign-truncated to large positives, making match arms verify under a wrong path assumption #132 negative SwitchInt).

Environment

• thrust @ 6953863
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (with the default fp.spacer.global=true fp.validate=true)