The bounded `Vec` wrapper has no `View`, so spec positions needing a `Seq` fail

[maxinelevesque]

---

Two symptoms with one cause: the generated TVec* wrapper cannot produce a
Seq, and both the indexing emitter and the combinators want one.

Reproduction — indexing

fn f(xs: Vec<u64>) -> u64 req xs.len() > 0 ens result == xs[0] fx alloc { xs[0] }

error[E0599]: no method named `view` found for struct `TVecU64` in the current scope
  = note: the following traits define an item `view`, perhaps you need to implement one of them

The emitter writes xs@[i as int] — Verus's view operator — and the wrapper does
not implement View.

Reproduction — a combinator over the same value

fn g(xs: Vec<u32>, n: u32) -> bool
  req true
  ens result == forall_in(xs, |x| x != n)
  fx  alloc
{ true }

error[E0308]: mismatched types
   |                   --------- ^^ expected `Seq<u32>`, found `TVecU32`
   = note: expected struct `vstd::seq::Seq<u32>`

The combinator takes a Seq and receives the wrapper. Same missing bridge, a
different position.

The capability already exists

The wrapper emits spec_get (thermite-lower/src/lower.rs:5100):

"    pub open spec fn spec_get(&self, i: int) -> {ety} {{ self.data@[i] }}"

So the value is reachable in spec; only the Seq-shaped route to it is missing.

Suggested fix

Minimal: emit spec_get-based forms rather than @ for indexing.

General: implement View for the generated wrapper, which serves both symptoms
at once and lets the combinator library work over a Vec field unchanged.

Why it survives

No .th in conformance/ quantifies over a Vec or Map field. The corpus
reaches slices, which do have a working spec surface — binary_search.th indexes
and quantifies over &[u32] at L3. The asymmetry between slices and the bounded
wrappers is what suggests this is unfinished rather than intended.

One design note that belongs in any fix

A collection-quantifying invariant is folded into every obligation touching that
type, as a precondition and a postcondition at every use site, so an expensive
invariant multiplies solver load across a whole program. That is a question about
whether to encourage the pattern rather than whether it is sound — but a fix that
makes something possible and intractable is worse than one that arrives with
guidance about when to use it.

Environment

Thermite 84d276e76ed02509ea58812efc15861d58580a42, Verus
0.2026.05.24.ecee80a. Found while designing a verified kernel against the pin
(bulla-systems/bulla).