Slicing with a range (&v[1..], &v[..n], &v[a..b], &v[..]) ICEs: the refinement-spec table is keyed by DefId alone, so _extern_spec_slice_index's usize signature is applied to every I: SliceIndex instantiation of the one shared Index::index impl method #281

Summary

Analyzer::defs — the table that maps a function to its refinement type — is a HashMap<DefId, DefTy> (src/analyze.rs:234). #[thrust::extern_spec_fn] registers its spec under the target's DefId only: extern_spec_fn_target_def_id() computes Instance::try_resolve(..) and then returns instance.def_id(), discarding instance.args (src/analyze/local_def.rs:386-394).

For Index/IndexMut/get/get_mut on slices and Vec, std has a single generic impl method per operation:

impl<T, I> ops::Index<I> for [T] where I: SliceIndex<[T]> { fn index(&self, index: I) -> &I::Output }

so <[T] as Index<usize>>::index and <[T] as Index<Range<usize>>>::index are the same DefId. _extern_spec_slice_index (std.rs:1081), whose signature is fixed at I = usize

#[thrust_macros::requires(index < (*slice).len())]
#[thrust_macros::ensures(*result == (*slice)[index])]
fn _extern_spec_slice_index<T>(slice: &[T], index: usize) -> &T { <[T] as std::ops::Index<usize>>::index(slice, index) }

is therefore handed out for every I. def_ty_with_args only substitutes the spec's type params from generic_args.types() (src/analyze.rs:552-558); I is never looked at. The range struct is then related against the spec's index: usize, and rty::subtyping::relate_type hits its inconsistent types panic! (src/rty/subtyping.rs:155).

This is not an unimplemented!/unsupported marker — it is the wrong spec being selected, and it aborts the compiler. The same wrong spec also gets the return type wrong (see the trace below), which is the latent unsound half of the bug: it claims the call returns a single element &T satisfying *result == (*slice)[index] when it actually returns a sub-slice &[T]. Today the parameter mismatch always panics first, so nothing verifies incorrectly — but only because no SliceIndex type happens to model to Int.

Minimal reproduction

repro.rs:

fn main() {
    let arr = [1_i64, 2, 3];
    let v: &[i64] = &arr;
    let w = &v[1..];
    assert!(w.len() == 2);
}

$ cargo run -q -- -Adead_code -C debug-assertions=false repro.rs

thread 'rustc' panicked at src/rty/subtyping.rs:155:14:
inconsistent types: got=(own int,), expected=int
   2: thrust::rty::subtyping::relate_type
             at ./src/rty/subtyping.rs:155:14
   3: <C as thrust::rty::subtyping::Subtyping>::relate_sub_type
             at ./src/rty/subtyping.rs:63:9
   4: thrust::analyze::basic_block::Analyzer::relate_fn_param_sub_types_with_builder
             at ./src/analyze/basic_block.rs:349:36
   5: thrust::analyze::basic_block::Analyzer::relate_fn_sub_type
             at ./src/analyze/basic_block.rs:242:23
   6: thrust::analyze::basic_block::Analyzer::type_call
             at ./src/analyze/basic_block.rs:1055:32

Expected: safe (or, if range slicing is out of scope, a diagnostic).
Actual: the compiler aborts. got=(own int,) is RangeFrom<usize>'s struct model; expected=int is the usize from _extern_spec_slice_index.

Ground truth

rustc compiles and runs every program in this report to completion with exit status 0 — they cannot panic:

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

Direct evidence of the mis-selection

RUST_LOG=thrust=info on the reproduction above (ANSI stripped):

INFO … thrust::analyze::basic_block: resolved
  def_id=DefId(2:45105 ~ core::ops::index::Index::index)
  resolved_def_id=DefId(2:12912 ~ core::slice::index::{impl#0}::index)
  resolved_args=[i64, std::ops::RangeFrom<usize>]

INFO … thrust::analyze: formula_fn_with_args
  local_def_id=DefId(0:724 ~ repro::_thrust_requires__extern_spec_slice_index)
  formula_fn=|$0: <&[i64] as Model>::Ty, $1: <usize as Model>::Ty| true ∧ $1 < (seq.len *$0)
  generic_args=[i64, std::ops::RangeFrom<usize>]

INFO … thrust::analyze: deferred def
  def_id=DefId(2:12912 ~ core::slice::index::{impl#0}::index)
  rty=(&immut Seq<int>, { int | true ∧ ν < (seq.len *$0) }) → { &immut int | true ∧ *ν = (seq.nth *$0 $1) }
  generic_args=[i64, std::ops::RangeFrom<usize>]
  term=_4 = <[i64] as std::ops::Index<std::ops::RangeFrom<usize>>>::index(copy _2, move _5) -> [return: bb1, unwind continue]

The rty Thrust applies to a call that really has type (&[i64], RangeFrom<usize>) -> &[i64] is (&immut Seq<int>, int) -> &immut int — i.e. _extern_spec_slice_index's usize spec, requires/ensures included. generic_args carries RangeFrom<usize> right there in the record and is ignored. The identical rty is printed for Index<RangeFull>:

INFO … thrust::analyze: deferred def
  def_id=DefId(2:12912 ~ core::slice::index::{impl#0}::index)
  rty=(&immut Seq<int>, { int | true ∧ ν < (seq.len *$0) }) → { &immut int | true ∧ *ν = (seq.nth *$0 $1) }
  generic_args=[i64, std::ops::RangeFull]
  term=_4 = <[i64] as std::ops::Index<std::ops::RangeFull>>::index(copy _2, move _5) -> …

Isolation

All rows abort in relate_type at src/rty/subtyping.rs:155. got is exactly the index argument's model, which identifies which I leaked into the usize slot.

Affected methods, all one DefId per row regardless of I: <[T] as Index<I>>::index, <[T] as IndexMut<I>>::index_mut, <Vec<T> as Index<I>>::index, <Vec<T> as IndexMut<I>>::index_mut, <[T]>::get::<I>, <[T]>::get_mut::<I>.

Not solver- or optimization-dependent

The panic happens during analysis, before any solver runs — identical under the default z3 and under THRUST_SOLVER=tests/thrust-pcsat-wrapper.

Where it bites

Sub-slicing is how idiomatic Rust walks and passes buffers, so this blocks whole shapes of program rather than one expression:

// The textbook recursive formulation over a slice: ICE.
fn sum(v: &[i64]) -> i64 {
    if v.is_empty() { 0 } else { v[0] + sum(&v[1..]) }
}

Also &buf[..n] to hand a prefix to a helper, &v[..] to coerce a Vec to a slice, and the &mut variants — the operations a real caller reaches for first.

Workarounds

• split_first / split_last verify and are how tests/ui/pass/slice_split_first*.rs walk a slice — but they only peel one element at a time, so an arbitrary &v[a..b] cannot be expressed.
• v.as_slice() verifies, so &v[..] on a Vec has a direct replacement.
• v.split_at(n) does not help: unknown def (and not resolved): DefId(2:14095 ~ core::slice::…).
• A #[thrust::trusted] wrapper works, since a trusted body is not analyzed:

  #[thrust::trusted]
  #[thrust_macros::requires(n <= (*v).len())]
  #[thrust_macros::ensures((*result).len() == (*v).len() - n)]
  fn tail(v: &[i64], n: usize) -> &[i64] { &v[n..] }   // verifies

Suggested direction

Key the spec table on the instantiation, not just the DefId: have extern_spec_fn_target_def_id() return instance.args alongside the DefId and register/look up (DefId, GenericArgsRef) (or at least reject a lookup whose generic_args disagree with the spec's own target args, turning the ICE into a diagnostic). With that in place, _extern_spec_slice_index would only ever answer for I = usize, and range slicing could get its own specs — a natural one for Range/RangeFrom/RangeTo/RangeFull already exists in the Seq model as subsequence, which _extern_spec_vec_truncate and _extern_spec_vec_pop use.

Relation to existing issues

• Ordering comparisons (<, >) on tuple/aggregate values emit ill-typed SMT (< Tuple Tuple) via the generic PartialOrd::lt/gt extern specs, so safe programs comparing tuples are falsely rejected #195 (PartialOrd::lt/gt on tuples) and Incompleteness: a local impl PartialEq is checked against the blanket _extern_spec_partialeq_eq (structural model equality), so any non-structural eq — even one that is never used — makes the whole crate fail with Unsat #225 (local impl PartialEq vs the blanket _extern_spec_partialeq_eq) are the other face of "one spec covers instantiations it was not written for", but their specs are deliberately generic (<T>(x: &T, y: &T)) and the symptom is ill-typed SMT reaching the solver. Here the spec is fixed at I = usize and leaks to sibling instantiations of the same impl method, and the symptom is an analyzer panic! before any SMT is produced.
• Implicit derefs (rustc adjustments) are dropped in annotation translation, so any v.len()/v.length/s.0 on a &mut parameter builds an ill-sorted term and ICEs — only the explicit (*v) spelling works #239 is also an ill-sorted-term ICE, but its cause is dropped rustc adjustments in annotation translation, not spec selection at a call site.
• Not related to numeric ranges/overflow/unsigned modelling: every constant here is 1, 2 or 3, and v[0] — the same machinery at I = usize — verifies.

Environment

• thrust @ ff4f51a
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (default configuration) and PCSat 49ed9fe340; the panic precedes solver invocation either way