Challenge 17: Verify the safety of `slice` functions

[thanhnguyen-aws]

Runbook Link

https://model-checking.github.io/verify-rust-std/challenges/0017-slice.html

[Lysxia]

For align_to and align_to_mut, can we assume that the target type U is a SIMD type and the source type T is a SimdElement, since the main use case seems to be as_simd and as_simd_mut?

[tautschnig]

For align_to and align_to_mut, can we assume that the target type U is a SIMD type and the source type T is a SimdElement, since the main use case seems to be as_simd and as_simd_mut?

We should not constrain proofs by current usage, but it may be a reasonable starting point to cover those cases and then try to find ways to prove the general case.