Preserve exhausted slice iterator state in specs

[kimjune01]

Summary

• preserve slice::Iter position when next is called after exhaustion
• align the associated Iterator::step relation with the concrete method spec
• cover direct, repeated, and generic exhausted calls

Rust leaves an exhausted slice iterator at the same position, but the current extern spec advances idx unconditionally. This creates impossible states with idx > len and makes concrete and generic iterator reasoning disagree.

The regression fails on main and passes with these changes.

Context

• An earlier unmerged commit identified the conditional transition: 5b200c9
• The analogous exhausted-range fix is in Strengthen exhausted Range::next postcondition #1739.
• The broader discussion about checking iterator specs against core implementations: Remove "lib/{step.rs,iter.rs,iterator.rs}" #1170 (comment)

Test

PATH="$HOME/.cargo/bin:$PATH" cargo xtask test flux_core_slice00 --suite with-deps