Current slice support is partial (slice_index_range is explicitly disabled with a TODO).
- push / pop — dynamic length mutation with capacity reasoning
- swap — in-place element exchange (already verified in Showcase but not stdlib)
- split_at / split_at_mut — slice partitioning; enables divide-and-conquer proofs
- contains — membership check (exists for Range, missing for slices)
- copy_from_slice — bulk copy with length-equality precondition
- reverse — in-place reversal (linked list reversal exists, not for slices)
- sort / sort_by — sorting with comparison specs (high-value proof target)
- fill — bulk initialization
Current slice support is partial (slice_index_range is explicitly disabled with a TODO).