A locally-declared `struct`/`enum` never gets a `Model` instance, so `Vec<P>`/`Box<P>`/`&[P]`/`[P; N]`/`&mut P` abort in `TypeBuilder::build` — `Vec<P>` dies inside `alloc`'s private fields (`*const u8`), and a one-line `impl Model for P { type Ty = Self; }` makes every case verify

[coord-e]

Summary

Thrust decides a Rust type's logical model by normalizing <T as thrust_models::Model>::Ty (TypeBuilder::resolve_model_ty, src/refine/template.rs:154-169). std.rs gives Vec<T>, Box<T>, [T], [T; N] and &mut T conditional impls that require T: Model — but no Model instance is ever created for a user-defined struct/enum. For a local ADT P the projection therefore fails to normalize, resolve_model_ty silently returns the unresolved type, and TypeBuilder::build then either

• has no arm for it (&mut P, &[P], [P; N]) and hits unimplemented!, or
• — worse — takes the def.is_struct() structural arm for Vec<P> / Box<P> and starts expanding alloc's private representation, aborting with not implemented: ty: *const u8.

This is not "Vec is unsupported" or "&mut is unsupported": Vec<i64>, Box<i64>, &mut i64, &P, &self, by-value P, Option<P> and (P, i64) all verify today, and adding the semantically vacuous line impl thrust_models::Model for P { type Ty = Self; } makes every failing program below verify with the correct verdict in both directions. The analysis fully supports these types; what is missing is the Model instance that a local ADT should have by construction. A &mut P that is created and consumed inside one body already verifies without the impl (see the matrix) — only the positions that must go through the Model projection fail.

The failure surfaces as an ICE naming a std implementation detail (*const u8, *const P), which gives a user no way to work out that the fix is one line of undocumented boilerplate — thrust_models::Model appears nowhere in README.md, and inside a mod the workaround must additionally be spelled impl crate::thrust_models::Model for … (thrust_models is injected at the crate root; cf. #252/#256).

Minimal reproduction

repro.rs — no &mut, no annotations, a supported container holding a supported struct:

struct Point { x: i64, y: i64 }

fn main() {
    let mut points = Vec::new();
    points.push(Point { x: 1, y: 2 });
    assert!(points[0].x == 1);
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs
thread 'rustc' (5807) panicked at src/refine/template.rs:440:21:
not implemented: ty: *const u8
stack backtrace:
   2: thrust::refine::template::TemplateTypeBuilder<R,S>::build
             at ./src/refine/template.rs:440:21
   3: thrust::refine::template::TemplateTypeBuilder<R,S>::build::{{closure}}
             at ./src/refine/template.rs:432:56
  ...

*const u8 is alloc::raw_vec::RawVecInner's pointer field — Thrust walked into Vec's internals instead of using its Seq model. The program is ordinary safe Rust:

$ rustc -Adead_code --edition 2021 -o repro repro.rs && ./repro ; echo "exit=$?"
exit=0

Adding one line fixes it:

 struct Point { x: i64, y: i64 }
+impl thrust_models::Model for Point { type Ty = Self; }

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs && echo safe
safe
$ # and the negation is still correctly rejected:
$ #   assert!(points[0].x == 2)  ->  error: verification error: Unsat

The same one-liner is what makes &mut Point work:

struct P { x: i64 }
fn set(p: &mut P, n: i64) { p.x = n; }              // not implemented: ty: &'{erased} mut P
fn main() { let mut p = P { x: 1 }; set(&mut p, 5); assert!(p.x == 5); }

Evidence matrix

All rows -Adead_code -C debug-assertions=false --edition 2021, thrust @ 5c74a7f, Z3 5.0.0, default solver config. "no impl" = the program exactly as written; "with impl" = the same program plus impl thrust_models::Model for P { type Ty = Self; } (resp. for the enum).

#	program (struct P { x: i64 } / enum E { A(i64), B } unless noted)	no impl	with impl
1	fn get(p: P) -> i64 { p.x }, by value	safe	safe
2	fn get(p: &P) -> i64 { p.x }	safe	safe
3	impl P { fn get(&self) -> i64 { self.x } }	safe	safe
4	fn get(e: &E) -> i64 { match e { … } }	safe	safe
5	let o = Some(P{x:1}); match o { Some(p) => assert!(p.x == 1), … }	safe (neg: Unsat)	safe
6	let t = (P{x:1}, 2i64); assert!(t.0.x == 1 && t.1 == 2)	safe (neg: Unsat)	safe
7	let r = &mut p; r.x = 5; assert!(p.x == 5) — borrow created and consumed in one body	safe (neg: Unsat)	safe
8	fn set(p: &mut P, n: i64)	ICE ty: &'{erased} mut P	safe (neg: Unsat)
9	impl P { fn set(&mut self, n: i64) }	ICE ty: &'{erased} mut P	safe
10	fn id(p: &mut P) -> &mut P { p }	ICE ty: &'{erased} mut P	safe
11	fn bump(e: &mut E) (enum)	ICE ty: &'{erased} mut E	safe
12	impl Bump for P { fn bump(&mut self) } (trait method)	ICE ty: &'{erased} mut P	safe
13	fn f(o: Option<&mut P>)	ICE ty: &'{erased} mut P	safe
14	fn f(t: (&mut P, i64))	ICE ty: &'{erased} mut P	safe
15	let f = |q: &mut P| { q.x = 5; }; f(&mut p); (closure param)	ICE ty: &'{erased} mut P	safe
16	fn set<T>(r: &mut T, v: T) { *r = v; } called at T = P	ICE ty: &'{erased} mut P	safe
17	let mut v = Vec::new(); v.push(P{x:1}); assert!(v[0].x == 1)	ICE ty: *const u8	safe (neg: Unsat)
18	fn f(v: &Vec<P>) -> i64 { v[0].x } (shared ref)	ICE ty: *const u8	safe
19	fn f(v: &mut Vec<P>) { v[0].x = 5; }	ICE ty: &'{erased} mut Vec<P, Global>	safe
20	v.push(E::A(1)) (Vec of a local enum)	ICE ty: *const u8	safe
21	let b = Box::new(P{x:1}); assert!(b.x == 1)	ICE unrefined_ty: *const P	safe
22	fn f(s: &[P]) -> i64 { s[0].x }	ICE ty: [P]	safe
23	let a = [P{x:1}, P{x:2}]; assert!(a[0].x == 1)	ICE unrefined_ty: [P; 2_usize]	safe

Controls with a type that does have a Model impl in std.rs — all safe, no boilerplate needed:

program	verdict
let mut v = Vec::new(); v.push(1i64); assert!(v[0] == 1)	safe
let mut b = Box::new(1i64); *b += 1; assert!(*b == 2)	safe
fn set(r: &mut i64, v: i64) { *r = v; }	safe
fn set<T>(r: &mut T, v: T) { *r = v; } at T = i64	safe

Rows 1-7 are the decisive ones. They show that a local ADT is not unsupported anywhere build has a structural arm — including a mutable borrow of it, as long as that borrow never has to be turned into a type (row 7, which also rejects its negation, so the prophecy machinery is working on P already). Rows 8-23 are the same ADT in the positions that must go through the Model projection.

Note also the asymmetry between rows 2 and 18: a shared &P verifies, but &Vec<P> does not — so this is not a &mut-only story, and Vec is not "unsupported": the single variable is whether P: Model holds.

Root cause

resolve_model_ty (src/refine/template.rs:154-169) tries to normalize the Model::Ty projection and falls back to the original type when that fails, with no diagnostic:

pub fn resolve_model_ty(&self, orig_ty: mir_ty::Ty<'tcx>) -> mir_ty::Ty<'tcx> {
    let ty = self.replace_closure_model(orig_ty);
    let Some(model_ty_def_id) = self.def_ids.model_ty() else { return ty; };
    let args = self.tcx.mk_args(&[ty.into()]);
    let projection_ty = mir_ty::Ty::new_projection(self.tcx, model_ty_def_id, args);
    if let Ok(normalized_ty) = self.tcx.try_normalize_erasing_regions(self.typing_env, projection_ty) {
        return normalized_ty;
    }
    ty                                    // <- silent fallback
}

Every container model in std.rs is conditional on the element being a model:

impl<'a, T: ?Sized> Model for &'a mut T where T: Model { type Ty = model::Mut<T::Ty>; }  // std.rs:342
impl<T: ?Sized> Model for Box<T> where T: Model { … }                                    // std.rs:354
impl<T> Model for Vec<T> where T: Model { … }                                            // std.rs:366
impl<T> Model for [T] where T: Model { … }                                               // std.rs:370
impl<T: Model, const N: usize> Model for [T; N] { … }                                    // std.rs:375

and nothing ever supplies impl Model for P for a locally-declared P. So for a local ADT:

• &mut P. Both build impls (TypeBuilder::build, src/refine/template.rs:206-260; TemplateTypeBuilder::build, :392-440) have an arm for TyKind::Ref(_, elem, Mutability::Not) that builds PointerType::immut_to structurally, but no arm for Mutability::Mut — mutable references are handled only by resolve_model_ty rewriting them to model::Mut<..>, which model_adt's mut_model() branch then turns into PointerType::mut_to. When the rewrite does not fire, the type falls through to unimplemented!("ty: {:?}"). The shared-reference arm shows the structural fallback was intended here; it was just never written for Mut.
• Vec<P> / Box<P>. These are TyKind::Adt and def.is_struct(), so the unresolved type lands in the struct arm and is expanded field-by-field into alloc::raw_vec::RawVec → RawVecInner → Unique<u8> → NonNull<u8> → *const u8 (resp. Unique<P> → *const P). The abort message therefore names a std private field, not the user's type.
• &[P] / [P; N]. TyKind::Slice / TyKind::Array have no arm at all, so they reach unimplemented! directly.

Option<P> and (P, i64) escape all of this because build reaches them through its own is_enum() (nominal) and TyKind::Tuple arms, which never consult Model.

Because 62 of the 336 files under tests/ui/ already carry impl thrust_models::Model for … { type Ty = Self; } by hand, CI never exercises a local ADT without one.

Scope / when it bites

Every idiomatic Rust program hits this immediately: a &mut self method on a user type (rows 9, 12), a Vec of user structs (rows 17-19), Box (21) and slices (22-23) of them. It is the first thing encountered when pointing Thrust at real code, and the message gives no hint about the cause. Not a numeric-range/overflow/unsigned issue — every reproducer uses the literals 1, 2, 5.

Suggested direction

Give a locally-declared ADT a Model instance rather than requiring the user to write one:

• (a) In resolve_model_ty, when the <T as Model>::Ty projection does not normalize and T is a local ADT, treat T as its own model (type Ty = Self) and re-try the enclosing projection — i.e. make the container impls' T: Model bound discharge the way the 62 hand-written test impls make it discharge today. This fixes all of rows 8-23 at once, because it restores Vec<P> → Seq<P>, &mut P → Mut<P>, etc.
• (b) Or synthesize the impl Model for P { type Ty = Self; } item for every local ADT the way std.rs is injected, which is the same thing at the source level.

Independently worth doing, since both make the failure mode legible:

• add the missing TyKind::Ref(_, _, Mutability::Mut) arm to both build impls, mirroring the Mutability::Not arm (PointerType::mut_to(self.build(elem)));
• stop the def.is_struct() arm from expanding an ADT that carries a #[thrust::def::*] model (Vec, Box, …) — expanding alloc's private fields can only ever produce a confusing abort — and report a proper diagnostic naming the user's type instead.

If requiring the impl is deliberate, then at minimum it needs to be in README.md (it is currently undocumented), and the abort should name the user's type and the missing impl rather than *const u8.

Distinct from the known issues

• Stack overflow (non-termination) in TypeBuilder::build: a struct is always expanded structurally with no cycle cut, so any struct that reaches itself (struct Node { next: Option<Box<Node>> }, struct Tree { kids: Vec<Tree> }) aborts the compiler #249 (stack overflow in TypeBuilder::build for self-reaching structs) is the other build issue, but its trigger is a type-level cycle and every one of its reproducers already writes impl thrust_models::Model for S { type Ty = Self; }; here there is no recursion at all (struct Point { x: i64, y: i64 }) and the impl's absence is the trigger.
• Bug: Rvalue::Aggregate for a newtype struct ignores Model::Ty, causing call-site sort mismatch #73 (Rvalue::Aggregate for a newtype struct ignores Model::Ty) is about a call-site sort mismatch when a Model impl exists; this is about there being none.
• Panic / undeclared SMT sort: an enum reachable only through an ADT's field type is never registered in EnumDefs, so any struct with an enum-typed field (struct W { o: Option<i32> }) aborts verification #221 (an enum reachable only through an ADT field is never registered) is a registration gap for a type that build does handle.
• Annotation macros emit unqualified thrust_models::… paths, so no item inside a mod can be specified — requires/ensures/param/ret/sig/predicate/invariant!/ghost! all die with E0433 #252/Anchor macro-emitted model paths at the crate root #256 are about macro-emitted thrust_models::… paths inside a mod; they only make the workaround here harder to spell (impl crate::thrust_models::Model for …), they are not the cause.
• Incompleteness: a &mut into an enum/Option whose payload is a Vec (any Seq-modeled container) defeats the default solver configuration — a five-line Option<Vec<i64>> program times out, while the same code with the container in a struct field, or moved out by value, verifies in 0.5 s #263/Incompleteness: a &mut stored in a Vec (Seq/array-backed container) never has its prophecy resolved at drop, so safe programs are wrongly rejected as Unsat #202/Unsound: Vec equality (==) is modeled as structural equality of the whole (array, length) representation, so vectors equal in Rust but differing in stale slots past length (after pop/truncate) compare unequal — dead-branch panics verify as safe #203 concern Vec/Seq semantics once the Seq model is in use; here the Seq model is never selected at all.

Environment

• thrust @ 5c74a7f
• rustc nightly-2025-09-08 (per rust-toolchain.toml), --edition 2021
• Z3 5.0.0 (x64-glibc-2.39, the version .github/actions/setup-z3 pins), default THRUST_SOLVER_ARGS, default 30 s timeout — never reached in the ICE rows