Add offset slice views and split_first_mut

[coord-e]

Summary

• extend Seq with an offset field
• add offset-aware subsequence support without prepend
• update Vec and slice specs and their tests for the three-field Seq representation
• add a split_first_mut extern spec using Mut::new and subsequence
• add paired pass/fail tests

Design

The offset lets multiple slice views share one underlying array while changing their logical start and length. subsequence(start, end) preserves the array, advances the offset by start, and sets the view length to end - start.

Known limitation

The current handling of mutable references returned inside tuples can make mutation propagation through split_first_mut unsound. This is accepted for this PR and documented in the related discussion on #124: #124 (comment)

Validation

• cargo check
• compiler-backed slice-index reconstruction unit tests
• all slice and split_first_mut pass/fail pairs with the default Spacer solver
• subsequence and loop-invariant pass/fail pairs with PCSAT