[codex] Support slices in Thrust

[coord-e]

Summary

• make Seq offset-aware and add prepend/subsequence operations
• model [T] as Seq<T::Ty> and specify slice length, emptiness, element access, and mutable access operations
• reconstruct first-class MIR slice indexing as Index/IndexMut calls, and route slice metadata length through the registered extern spec
• add paired passing/failing UI coverage for each step

Motivation

Slice representation belongs in std.rs; the basic-block analyzer should not know that slices are modeled by Seq. Reconstructing erased MIR operations as calls keeps slice semantics in the extern specs and lets the analyzer reuse normal function-type application.

Validation

• cargo check
• targeted PCSAT pass/fail tests for sequence views, slice methods, slice indexing, mutable slice indexing, and out-of-bounds rejection
• targeted Seq and Vec regression tests

[coord-e]

#152 #153