Incompleteness: the statically-known length `N` of `[T; N]` is dropped by the `Seq` model, so a fixed-size array that is not built by an array literal in the same body has an unconstrained `length` and cannot be indexed at all

[coord-e]

Summary

[T; N] is modeled as a Seq, i.e. the pair (array, length):

// std.rs:374-377
// NOTE: basic_block::Analyzer depends on the structure of array model
impl<T: Model, const N: usize> Model for [T; N] {
    type Ty = model::Seq<<T as Model>::Ty>;
}

The const generic N appears nowhere on the right-hand side, so [T; N] and [T] have exactly the same model and the length that Rust guarantees statically is lost. The only place a Seq's length is ever pinned for an array is the array-literal rvalue (src/analyze/basic_block.rs:546-570, chc::Term::int(size as i64) where size = fields.len()). Every other way a [T; N] value can enter a body — a function parameter, a struct field of a parameter, the return value of a #[thrust::trusted] function, the prophecy of a &mut [T; N] after a call — gives a Seq whose length component is a completely unconstrained Int.

Since _extern_spec_slice_index (std.rs:987-994) carries #[requires(index < (*slice).length)], the consequence is that indexing a fixed-size array parameter is never provable, even at a constant index that is in bounds for every value of the type:

#[thrust::callable]
fn first(a: &[i64; 3]) -> i64 {
    let s: &[i64] = a;
    s[0]            // in bounds for every `&[i64; 3]` — rejected as `Unsat`
}

This is an incompleteness (safe programs wrongly rejected), not a soundness hole: the length is left unconstrained rather than set to a wrong value (assert!(s.len() == 3) and assert!(s.len() != 3) are both rejected while the tautology assert!(s.len() == 3 || s.len() != 3) verifies).

Minimal reproduction

arr_param.rs:

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

#[thrust::callable]
fn first(a: &[i64; 3]) -> i64 {
    let s: &[i64] = a;
    s[0]
}

fn main() {}

$ cargo run -q -- -Adead_code -C debug-assertions=false arr_param.rs && echo safe
error: verification error: Unsat

error: aborting due to 1 previous error

Expected: safe. a: &[i64; 3] has three elements by its type, so s.len() == 3 and s[0] cannot panic for any input.
Actual: rejected as Unsat.

Ground truth (runnable)

The same function under plain rustc, exercised from main:

fn first(a: &[i64; 3]) -> i64 {
    let s: &[i64] = a;
    s[0]
}

fn main() {
    let arr = [7i64, 8, 9];
    assert!(first(&arr) == 7);
    println!("ok: first = {}", first(&arr));
}

$ rustc --edition 2021 -Adead_code -C debug-assertions=off -o plainrun plain.rs && ./plainrun
ok: first = 7

Isolation

All rows use -Adead_code -C debug-assertions=false on cd6b330.

#	Program	Verdict	Correct?
1	#[thrust::callable] fn first(a: &[i64; 3]) -> i64 { let s: &[i64] = a; s[0] }	Unsat	❌ bug
2	same body, assert!(s.len() == 3)	Unsat	❌ bug
3	same body, assert!(s.len() != 3)	Unsat	✅ (havoc)
4	same body, assert!(s.len() == 3 || s.len() != 3)	safe	✅ (confirms havoc, not miscomputation)
5	by-value param: #[thrust::callable] fn f(a: [i64; 3]) -> i64 { let s: &[i64] = &a; s[0] }	Unsat	❌ bug
6	array as a struct field of a parameter: struct Board { cells: [i64; 3] } … let s: &[i64] = &b.cells; s[0]	Unsat	❌ bug
7	&mut [i64; 3] after a call spec'd requires(true)/ensures(true), then s[2]	Unsat	❌ bug
8	#[thrust::trusted] fn make() -> [i64; 3] with ensures(true), then s[0]	Unsat	❌ bug
9	control — literal in the same body: let arr = [1i64,2,3]; let s: &[i64] = &arr; assert!(s.len() == 3); let _ = s[2];	safe	✅
10	control — no annotation, inference across the call: fn first(a: &[i64; 3]) -> i64 { … s[0] } called with a literal	safe	✅ (the caller pins the length)
11	workaround — #[requires((*a).length == 3)] fn f(a: &[i64; 3]) { let s: &[i64] = a; let _ = s[0]; }	safe	✅
12	control — genuine slice: #[thrust::callable] fn first(a: &[i64]) -> i64 { a[0] }	Unsat	✅ correct (a &[T] really has an unknown length)

Rows 1 and 12 are the crux: the identical rejection is correct for &[i64] and wrong for &[i64; 3], because only the latter carries the length in its type.

Row 7's diagnosis is confirmed by restating just the length relation, which makes it verify:

// safe: adding only the length fact repairs it
#[thrust_macros::requires(true)]
#[thrust_macros::ensures((!a).length == (*a).length)]
fn touch(a: &mut [i64; 3]) { let _ = a; }

fn main() {
    let mut arr = [1i64, 2, 3];
    touch(&mut arr);
    let s: &[i64] = &arr;
    let _ = s[2];
}

and row 8's by #[ensures(result.length == 3)] on make.

Root cause

resolve_model_ty (src/refine/template.rs:154-169) normalizes <[T; N] as Model>::Ty to model::Seq<T::Ty>, a plain struct, which TypeBuilder::build/TemplateTypeBuilder::build then turn into TupleType([Box<Array<Int, T>>, Box<Int>]). The const argument N is discarded by the Model projection at std.rs:375 and there is no compensating refinement anywhere: neither build_refined nor the function/basic-block template builders emit length == N for an Array-kinded mir_ty::Ty.

The generated SMT for the reproduction (THRUST_OUTPUT_DIR) shows the parameter v0 universally quantified with nothing said about its length projection, and the index obligation therefore unprovable:

; c0 — the `0 < length(a)` obligation for `s[0]`
(assert (forall ((v0 A1_Tuple<Array<Int-Int>-Int>) ... (v6 Int))
  (=> (and (= v1 v0) (= v2 0) (= v3 v0) (p2 v3 v0) (= v4 v1) (= v6 v2)
           (not (< v6 (tuple_proj<Array<Int-Int>-Int>.1 v4))))
      false)))

(tuple_proj<Array<Int-Int>-Int>.1 v4) is the length field of the incoming array; nothing in the clause body constrains it, so the premise is satisfiable (take length <= 0) and the clause is unprovable.

By contrast the array-literal path does pin it (src/analyze/basic_block.rs:564-568):

let size = fields.len();
let size_pty = PlaceType::with_ty_and_term(rty::Type::int(), chc::Term::int(size as i64));

which is exactly why rows 9 and 10 verify and everything else does not.

Expected behavior

A value of type [T; N] should carry length == N unconditionally, wherever it is built — not only at an array literal. Concretely, the refined type produced for a mir_ty::TyKind::Array(elem, n) (in build_refined/the template builders, so that it covers parameters, returns, struct fields and &mut prophecies alike) should conjoin the refinement v.length == N using the evaluated const n, rather than leaving the Seq's second component free. The same fact must also be attached to the prophecy component of a &mut [T; N], since Rust forbids a callee from changing the length of a fixed-size array.

Scope / when it bites

Fixed-size arrays crossing a function boundary are ordinary Rust (fn parse(buf: &[u8; 4]), struct Board { cells: [i64; 9] }, fn f(a: [i64; 3])), and this makes every one of them unindexable unless the caller happens to pin the length through inference (row 10). In particular any attempt to verify such a function in isolation — the #[thrust::callable] entry-point mode, and any function carrying its own requires/ensures — is currently impossible without hand-writing #[requires((*a).length == N)], a fact the type system already guarantees. It also silently degrades &mut [T; N]: any spec'd call through one loses the length for the rest of the caller (row 7).

There is a workaround (row 11) but it must be repeated on every function, and it turns a type-level guarantee into a proof obligation on callers.

Distinct from existing issues

• Not Incompleteness: v.len() on a &mut [T] leaves an unresolved reborrow that havocs the referent, so every safe &mut slice program that guards an index with len() is rejected at any -C opt-level >= 1 #240 (v.len() on &mut [T] leaving an unresolved reborrow at -C opt-level >= 1): this reproduces at the default -C opt-level=0, needs no &mut (rows 1, 5, 6, 8) and no len() call at all (rows 1, 5, 6, 7, 8 index directly); the defect is the missing length == N fact, not a havoc'd referent.
• Not 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 (implicit derefs dropped in annotation translation): rows 1-10 contain no annotations; and the explicit-deref spelling (*a).length that 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 says is the working one is precisely the workaround in row 11.
• Not 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 (Vec/slice equality over the whole array): no == on containers here, and the discrepancy is about the length component itself, not the slots past it.
• Not Incompleteness: unsigned integer types (usize/u32/u64) are modeled as unconstrained integers, so their >= 0 lower bound is not assumed and safe programs are wrongly rejected #165 (unsigned types modeled as unconstrained integers): the reproduction uses i64 elements, and adding a length >= 0 lower bound would not help — the needed fact is length == 3.
• Not a numeric-range/overflow issue (N is 3) and not a lack-of-support panic: [T; N] parameters are accepted and analyzed, they just carry no length.

Environment

• thrust @ cd6b330
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0, default solver configuration
• Reproduces identically with --edition 2021