Unsound: enum variants after an explicit discriminant get the wrong `datatype_discr` value, making match arms vacuously verify

[coord-e]

Summary

For enums that use explicit discriminants, Thrust assigns the wrong discriminant value to every variant that follows an explicit one. resolve_discr (src/analyze.rs:68) returns the relative offset stored in ty::VariantDiscr::Relative(i) verbatim, treating it as the absolute discriminant. In rustc, Relative(i) means "the nearest preceding explicit discriminant (or 0) plus i", so the absolute value is generally not i.

This wrong value is baked into the SMT datatype_discr function, while the SwitchInt lowering of a match compares that function against the actual discriminant values. The two disagree, the branch's path assumption becomes unsatisfiable (e.g. 1 = 2), and the match arm verifies vacuously — so Thrust accepts programs that panic at runtime.

Reproduction (minimal, no closures / refs)

//@compile-flags: -C debug-assertions=off
enum E {
    A = 1, // explicit discriminant 1
    B,     // runtime discriminant 2, but resolve_discr() reports 1
}

#[thrust::callable]
fn check(e: E) {
    match e {
        E::A => {}
        E::B => assert!(false), // E::B IS reachable at runtime → must be rejected
    }
}

fn main() {}

check(E::B) panics under plain rustc (assert!(false)), yet Thrust accepts this program. A three-variant version shows the value is shifted (not merely collided):

enum E { A = 1, B, C } // runtime discriminants 1,2,3; resolve_discr reports 1,1,2

For the all-default case enum E { A, B, C } (A=0,B=1,C=2) every variant is Relative(i) with no preceding explicit discriminant, so i happens to equal the absolute value and there is no bug. The bug is specific to enums with at least one explicit discriminant.

Root cause

src/analyze.rs:68

pub fn resolve_discr(tcx: TyCtxt<'_>, discr: mir_ty::VariantDiscr) -> u32 {
    match discr {
        mir_ty::VariantDiscr::Relative(i) => i, // <-- relative offset, not the absolute discriminant
        mir_ty::VariantDiscr::Explicit(did) => {
            let val = tcx.const_eval_poly(did).unwrap();
            val.try_to_scalar_int().unwrap().to_u32()
        }
    }
}

ty::VariantDiscr::Relative(i) is documented as the distance from the nearest preceding Explicit discriminant (or 0). So for enum E { A = 1, B }, variant B is Relative(1) and its absolute discriminant is 1 + 1 = 2, but resolve_discr returns 1.

This value reaches the SMT layer unchanged:

• src/analyze.rs:289 — let discr = resolve_discr(self.tcx, variant.discr); (with a // TODO: consider using TyCtxt::tag_for_variant right above it)
• src/analyze.rs:347 — discriminant: v.discr on chc::DatatypeCtor
• src/chc/unbox.rs:128 — unbox_datatype_ctor passes discriminant through untouched
• src/chc/smtlib2.rs:485-506 — DatatypeDiscrFun emits (ite ((_ is <ctor>) x) <discriminant> ...) using exactly that value

so the generated SMT is, for the reproduction:

(define-fun E_discr ((x E)) Int
  (ite ((_ is E.A) x) 1
  (ite ((_ is E.B) x) 1   ; WRONG: E::B's runtime discriminant is 2
  (- 1))))

Why it is unsound

The match lowers to a SwitchInt on Discriminant(e) (src/analyze/basic_block.rs:611-623 builds the datatype_discr term; type_switch_int at :789-831 compares it against chc::Term::int(n) where n is the MIR switch value). Crucially, the switch values are the actual discriminants — both the MIR itself and normalize_switch_int_discriminant_order (src/analyze/local_def.rs:764-767) use adt_def.discriminants(tcx) / discr.val, which are correct.

So for the arm that gets an exact SwitchInt target, Thrust assumes E_discr(e) == <actual discriminant>, while E_discr evaluates a real value of that variant to the wrong number. For enum E { A = 1, B } this happens regardless of how rustc orders the switch:

• {1 => A, otherwise => B}: the B arm assumes E_discr(e) != 1, but E_discr(E::B) = 1, so the assumption is 1 != 1 (unsat).
• {2 => B, otherwise => A}: the B arm assumes E_discr(e) == 2, but E_discr(E::B) = 1, so the assumption is 1 == 2 (unsat).

Either way the E::B arm runs under a contradictory premise, every verification condition in it (including assert!(false)) is vacuously valid, and the program is accepted.

When the mismatched variant instead lands in the otherwise branch, the same root cause produces the opposite symptom — a correct arm can be rejected (incompleteness) — but the false-accept above is the soundness hole.

Expected behavior

datatype_discr must agree with the discriminant values that SwitchInt compares against, i.e. the absolute discriminants. The fix is to stop using the raw Relative offset and instead read the absolute values rustc already computes — e.g. iterate tcx.adt_def(def_id).discriminants(tcx) (which yields (VariantIdx, Discr) with the absolute Discr.val) when building EnumVariantDef/DatatypeCtor, or use TyCtxt::tag_for_variant as the existing TODO suggests, rather than resolve_discr.

Notes

• Found by code inspection while reviewing the enum discriminant / SwitchInt path. I could not produce a console transcript because the pinned nightly-2025-09-08 toolchain (with rustc-dev) and Z3 are not available in my environment; the behavior above is fully determined by the cited code and rustc's VariantDiscr semantics.
• Independent of the open drop/move soundness issues (Unsoundness: partially-moved locals are still implicitly dropped, resolving prophecies of moved-out &mut borrows #121, Unsound: aggregate dropped wholesale after a partial field-move double-resolves the field's &mut prophecy #122, Panic: "deref unbound var" when reborrowing a &mut field out of an aggregate parameter #125): this is purely in enum datatype encoding, triggers without any &mut/move/drop, and affects both reads (Discriminant) and matches.

Environment

• thrust @ bcd2428
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 (any recent version)