Challenge 17: safety of slice functions

Safety-precondition contracts and Kani harnesses for the Challenge 17 slice
functions (library/core/src/slice/mod.rs): 43 harnesses in slice::verify —
10 unsafe (contracts; proof_for_contract where the impl resolves) and 27 safe
(no-UB), should_panic pairs for the documented panics, and a kani::cover on
every assume-bearing harness. Loop-bearing functions are verified at bounded
lengths; genuine-unbounded and generic-T are disclosed in the PR description.

Author: kasimte