Challenge 1 status update (#433)

Resolves #19 

## Status of verification of Challenge 1 functions

| Function | Location | Completion |
| :--- | :--- | :--- |
| `transmute_unchecked` | `core::intrinsics` | ✔* |
| `transmute` | `core::intrinsics` | ✔* |
| `MaybeUninit<T>::array_assume_init` | `core::mem` | X |
| `MaybeUninit<[T; N]>::transpose` | `core::mem` | ✔ |
| `<[MaybeUninit<T>; N]>::transpose` | `core::mem` | ✔ |
| `<[T; N] as IntoIterator>::into_iter` | `core::array::iter` | ✔ |
| `BorrowedBuf::unfilled` | `core::io::borrowed_buf` | ✔ |
| `BorrowedCursor::reborrow` | `core::io::borrowed_buf` | ✔ |
| `str::as_bytes` | `core::str` | ✔ |
| `from_u32_unchecked` | `core::char::convert` | ✔ |
| `char_try_from_u32` | `core::char::convert` | ✔ |
| `Ipv6Addr::new` | `core::net::ip_addr` | ✔ |
| `Ipv6Addr::segments` | `core::net::ip_addr` | ✔ |
| `align_offset` | `core::ptr` | ✔ |
| `Alignment::new_unchecked` | `core::ptr::alignment` | ✔ |
| `MaybeUninit<T>::copy_from_slice` | `core::mem` | ✔ |
| `str::as_bytes_mut` | `core::str` | ✔ |
| `<Filter<I,P> as Iterator>::next_chunk` | `core::iter::adapters` | X |
| `<FilterMap<I,F> as Iterator>::next_chunk` | `core::iter::adapters` |
X |
| `try_from_fn` | `core::array` | X |
| `iter_next_chunk` | `core::array` | X |
| `from_u32_unchecked` | `core::char` | ✔ |
| `AsciiChar::from_u8_unchecked` | `core::ascii_char` | ✔ |
| `memchr_aligned` | `core::slice::memchr` | ✔ |
| `<[T]>::align_to_mut` | `core::slice` | ✔ |
| `run_utf8_validation` | `core::str::validations` | ✔ |
| `<[T]>::align_to` | `core::slice` | ✔ |
| `is_aligned_to` | `core::const_ptr` | ✔ |
| `is_aligned_to` | `core::mut_ptr` | ✔ |
| `Alignment::new` | `core::ptr::alignment` | ✔ |
| `Layout::from_size_align` | `core::alloc::layout` | ✔ |
| `Layout::from_size_align_unchecked` | `core::alloc::layout` | ✔ |
| `make_ascii_lowercase` | `core::str` | ✔ |
| `make_ascii_uppercase` | `core::str` | ✔ |
| `<char as Step>::forward_checked` | `core::iter::range` | ✔ |
| `<Chars as Iterator>::next` | `core::str::iter` | ✔ |
| `<Chars as DoubleEndedIterator>::next_back` | `core::str::iter` | ✔ |
| `char::encode_utf16_raw` | `core::char` | N/A ** |
| `<char as Step>::backward_unchecked` | `core::iter::range` | ✔ |
| `<char as Step>::forward_unchecked` | `core::iter::range` | ✔ |
| `AsciiChar::from_u8` | `core::ascii_char` | ✔ |
| `<[T]>::as_simd_mut` | `core::slice` | ✔ |
| `<[T]>::as_simd` | `core::slice` | ✔ |
| `memrchr` | `core::slice::memchr` | ✔ |
| `do_count_chars` | `core::str::count` | ✔ |

\* Partial contract/harnesses (extent of what is currently expressible
by Kani)
** Does not transitively depend on transmute

## Some caveats

1. Not all functions with checkmarks have contracts & harnesses -- for
those that were trivially safe, nothing was done (a function is
"trivially safe" if there are no SAFETY comments, and upon visual
inspection, it is immediately clear that there is no way UB could be
triggered, such as for `as_bytes`).
2. As shown above, the transmute intrinsics don't have complete
contracts -- they've only been verified to what we understand to be the
extent of what is currently expressible by Kani (so we don't have a
precondition that checks, for instance, that it doesn't transmute an
immut ref into a mut ref)
3. As the challenge stipulates, the above functions were only checked
for safety, rather than functional correctness

## Question

Given that the completion condition for the challenge is 75% of
functions being verified, would it be considered as complete?

Please let us know if we're missing anything, or if any of the caveats
would need to be addressed for completion of the challenge.

Thanks!

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: thanhnguyen-aws <[email protected]>

Author: AlexLB99

doc/src/challenges/0001-core-transmutation.md

@@ -1,10 +1,11 @@
 # Challenge 1: Verify `core` transmuting methods
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
 - **Start date:** *2024/06/12*
 - **End date:** *2025/04/10*
 - **Reward:** *N/A*
+- **Contributors**: [Alex Le Blanc](https://github.com/AlexLB99), [Patrick Lam](https://github.com/patricklam)
 
 -------------------