Challenge 1 status update

[AlexLB99]

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.

[tautschnig]

Could you please also add a Contributors line to the resolved challenge, cf. challenges 0011 or 0014, among others.