Re-execution: Challenge 17: Verify the safety of slice functions

[Stevengre]

This draft PR bootstraps an independent re-execution of Challenge 17: Verify the safety of slice functions from model-checking/verify-rust-std.

Tracking:

• Upstream challenge issue: #281
• Upstream issue state at bootstrap: OPEN
• Planner record: https://github.com/runtimeverification/mir-semantics/blob/verify-rust-std/reexec-0017-slice/docs/verify-rust-std/challenges/0017-slice/planner.md
• Generator record: https://github.com/runtimeverification/mir-semantics/blob/verify-rust-std/reexec-0017-slice/docs/verify-rust-std/challenges/0017-slice/generator.md
• Evaluator record: https://github.com/runtimeverification/mir-semantics/blob/verify-rust-std/reexec-0017-slice/docs/verify-rust-std/challenges/0017-slice/evaluator.md
• Branch-local rubric: https://github.com/runtimeverification/mir-semantics/blob/verify-rust-std/reexec-0017-slice/docs/verify-rust-std/challenges/0017-slice/rubric.md
• Challenge artifact directory: https://github.com/runtimeverification/mir-semantics/blob/verify-rust-std/reexec-0017-slice/kmir/src/tests/integration/data/verify-rust-std/0017-slice

Bootstrap status:

• dedicated branch and worktree created
• planner, generator, and evaluator records committed
• no challenge implementation, proof development, evaluation, or review has been performed by the orchestrator on this branch

[Stevengre]

Moving to fork Stevengre/mir-semantics for submission