diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md new file mode 100644 index 0000000000000..21fb41dcb7129 --- /dev/null +++ b/doc/src/challenges/0016-iter.md @@ -0,0 +1,68 @@ +# Challenge 21: Verify the safety of `slice` iter functions - part 2 + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *?* + +------------------- + + +## Goal + +Verify the safety of iter functions that are defined in (library/core/src/iter/adapters): + + + +### Success Criteria + +Write and prove the contract for the safety of the following functions: + +| Function | Defined in | +|---------| ---------| +|next_back_remainder| array_chunks.rs| +|fold| array_chunks.rs| +|__iterator_get_unchecked| clone.rs| +|fold| clone.rs| +|next_unchecked| clone.rs| +|__iterator_get_unchecked| copied.rs| +|spec_next_chunk| copied.rs| +|__iterator_get_unchecked| enumerate.rs| +|next_chunk| filter.rs| +|next_chunk| filter_map.rs| +|__iterator_get_unchecked | fuse.rs| +|__iterator_get_unchecked | map.rs| +|next_unchecked | map.rs| +|as_array_ref | map_windows.rs| +|as_uninit_array_mut | map_windows.rs| +|push | map_windows.rs| +|drop | map_windows.rs| +|__iterator_get_unchecked | skip.rs| +|original_step | step_by.rs| +|spec_fold| take.rs| +|spec_for_each| take.rs| +|__iterator_get_unchecked | zip.rs| +|get_unchecked| zip.rs| +|fold| zip.rs| +|next| zip.rs| +|nth| zip.rs| +|next_back| zip.rs| +|spec_fold| zip.rs| + +The verification must be unbounded---it must hold for slices of arbitrary length. + +The verification must be hold for generic type `T` (no monomorphization). + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0016-slice.md b/doc/src/challenges/0016-slice.md deleted file mode 100644 index 02247ef04a68e..0000000000000 --- a/doc/src/challenges/0016-slice.md +++ /dev/null @@ -1,79 +0,0 @@ -# Challenge 20: Verify the memory safety of `slice` functions - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *?* - -------------------- - - -## Goal - -Verify the memory safety of [`std::slice` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/mod.rs). - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | -|---------| -|first_chunk| -|first_chunk_mut| -|split_first_chunk| -|split_first_chunk_mut| -|split_last_chunk| -|split_last_chunk_mut| -|last_chunk| -|last_chunk_mut| -|get_unchecked| -|get_unchecked_mut| -|as_ptr_range| -|as_mut_ptr_range| -|as_array| -|as_mut_array| -|swap| -|swap_unchecked| -|reverse| -|as_chunks_unchecked| -|as_chunks| -|as_rchunks| -|as_chunks_unchecked_mut| -|split_at_unchecked| -|split_at_mut_unchecked| -|split_at_checked| -|split_at_mut_checked| -|binary_search_by| -|partition_dedup_by| -|rotate_left| -|rotate_right| -|copy_from_slice| -|copy_within| -|swap_with_slice| -|align_to| -|align_to_mut| -|as_simd| -|as_simd_mut| -|get_many_unchecked_mut| -|get_many_mut| -|as_flattened| -|as_flattened_mut| - -The verification must be unbounded---it must hold for slices of arbitrary length. - -The verification must be hold for generic type `T` (no monomorphization). - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0017-integer-bit-correctness.md b/doc/src/challenges/0017-integer-bit-correctness.md deleted file mode 100644 index d981dac4ffec5..0000000000000 --- a/doc/src/challenges/0017-integer-bit-correctness.md +++ /dev/null @@ -1,64 +0,0 @@ -# Challenge 17: Correctness of primitive integer types' bit functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *N/A* - -------------------- - -## Goal - -Verify the correctness of primitive integer types' functions in `core::num::mod.rs`. - -For this challenge, you can assume that all the intrinsic functions are correct. - -### Success Criteria - -Prove the correctness the following functions and methods in `core::num::mod.rs` for all primitive integer types -`{isize, i8, i16, i32, i64, i128 , usize, u8, u16, u32, u64, u128}` - -| Function | -|--------- | -| `checked_shl` | -| `saturating_shl` | -| `unchecked_shl` | -| `overflowing_shl` | -| `wrapping_shl` | -| `unbounded_shr` | -| `checked_shr` | -| `saturating_shr` | -| `unchecked_shr` | -| `overflowing_shr` | -| `wrapping_shr` | -| `unbounded_shr` | -| `swap_bytes`| -| `reverse_bits`| -| `rotate_left`| -| `rotate_right`| -| `to_be` | -| `to_le` | -| `to_be_bytes` | -| `to_le_bytes` | -| `trailing_zeros` | -| `trailing_ones` | -| `leading_zeros` | -| `leading_ones` | -| `count_zeros` | -| `count_ones` | - - -### List of UBs - -In addition to any properties called out as `SAFETY` comments in the source -code, -all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory. -* Mutating immutable bytes. -* Producing an invalid value - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0018-nonzero-correctness.md b/doc/src/challenges/0018-nonzero-correctness.md deleted file mode 100644 index 63a0f0ace05a6..0000000000000 --- a/doc/src/challenges/0018-nonzero-correctness.md +++ /dev/null @@ -1,86 +0,0 @@ -# Challenge 19: Correctness of `NonZero` functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *N/A* - -------------------- - -## Goal - -Verify the correctness of `NonZero` functions in `core::num`. - -### Assumptions - -This challenge is the continuation of Challenge 12: Safety of `NonZero` and Challenge 14: Safety of Primitive Conversions. - -Now, you need to verify the "correctness" of the functions listed in Challenge 12. - -HOWEVER, You DON'T need to prove the "correctness" from the functions' descriptions, you JUST need to prove that those functions are consistent with those of -the primitive integer types (under safety preconditions of Challenge 12). - -For example, for the `max` function, you need to prove that -`∀ T in {isize, i8, i16, ... , usize, u8, ... }, ∀ x, y : NonZero, x.max(y).get() == x.get().max(y.get())` - -Proving the correctness of the functions of primitive integer types is proposed in Challenge 16 and 17. - -### Success Criteria - -Verify that the following functions and methods (all located within `core::num::nonzero`) are consistent with those of all of the primitive integer types: - -| Function | -|--------- | -| `max` | -| `min` | -| `clamp` | -| `bitor` (all 3 implementations) | -| `count_ones` | -| `rotate_left` | -| `rotate_right` | -| `swap_bytes` | -| `reverse_bits` | -| `from_be` | -| `from_le` | -| `to_be` | -| `to_le` | -| `checked_mul` | -| `saturating_mul` | -| `unchecked_mul` | -| `checked_pow` | -| `saturating_pow` | -| `neg` | -| `checked_add` | -| `saturating_add` | -| `unchecked_add` | -| `checked_next_power_of_two` | -| `midpoint` | -| `isqrt` | -| `abs` | -| `checked_abs` | -| `overflowing_abs` | -| `saturating_abs` | -| `wrapping_abs` | -| `unsigned_abs` | -| `checked_neg` | -| `overflowing_neg` | -| `wrapping_neg` | -| `from_mut` | -| `from_mut_unchecked` | - - -### List of UBs - -In addition to any properties called out as `SAFETY` comments in the source -code, -all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory. -* Mutating immutable bytes. -* Producing an invalid value - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. - diff --git a/doc/src/challenges/0019-silce.md b/doc/src/challenges/0019-silce.md deleted file mode 100644 index 02247ef04a68e..0000000000000 --- a/doc/src/challenges/0019-silce.md +++ /dev/null @@ -1,79 +0,0 @@ -# Challenge 20: Verify the memory safety of `slice` functions - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *?* - -------------------- - - -## Goal - -Verify the memory safety of [`std::slice` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/mod.rs). - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | -|---------| -|first_chunk| -|first_chunk_mut| -|split_first_chunk| -|split_first_chunk_mut| -|split_last_chunk| -|split_last_chunk_mut| -|last_chunk| -|last_chunk_mut| -|get_unchecked| -|get_unchecked_mut| -|as_ptr_range| -|as_mut_ptr_range| -|as_array| -|as_mut_array| -|swap| -|swap_unchecked| -|reverse| -|as_chunks_unchecked| -|as_chunks| -|as_rchunks| -|as_chunks_unchecked_mut| -|split_at_unchecked| -|split_at_mut_unchecked| -|split_at_checked| -|split_at_mut_checked| -|binary_search_by| -|partition_dedup_by| -|rotate_left| -|rotate_right| -|copy_from_slice| -|copy_within| -|swap_with_slice| -|align_to| -|align_to_mut| -|as_simd| -|as_simd_mut| -|get_many_unchecked_mut| -|get_many_mut| -|as_flattened| -|as_flattened_mut| - -The verification must be unbounded---it must hold for slices of arbitrary length. - -The verification must be hold for generic type `T` (no monomorphization). - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0020-slice-iter.md b/doc/src/challenges/0020-slice-iter.md deleted file mode 100644 index 228f6fc029492..0000000000000 --- a/doc/src/challenges/0020-slice-iter.md +++ /dev/null @@ -1,64 +0,0 @@ -# Challenge 21: Verify the memory safety of `slice` iter functions - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *?* - -------------------- - - -## Goal - -Verify the memory safety of functional correctness of [`std::slice` iter functions] (https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/iter/macros.rs). - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | -|---------| -|next_back_unchecked| -|make_slice| -|pre_dec_end| -|post_inc_start| -|len| -|is_empty| -|next| -|size_hint| -|count| -|nth| -|advance_by| -|last| -|fold| -|for_each| -|all| -|any| -|find| -|find_map| -|position| -|rposition| -|next_back| -|nth_back| -|advance_back_by| -|next_unchecked| - - -The verification must be unbounded---it must hold for slices of arbitrary length. - -The verification must be hold for generic type `T` (no monomorphization). - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0021-str-encode.md b/doc/src/challenges/0021-str-encode.md deleted file mode 100644 index 004a1958dc315..0000000000000 --- a/doc/src/challenges/0021-str-encode.md +++ /dev/null @@ -1,58 +0,0 @@ -# Challenge 5: Verify the correctness of UTF8 and UTF16 encoding functions -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the the correctness of functions related to UTF8 and UTF16 encoding - -### Details - -Rust str and String are either UTF8 or UTF16 encoded. Verifying the correctess of the related functions is important in ensuring the safety and correctness of Rust programs that involve Strings. - - -### Success Criteria - -Verify the the correctness of the following functions is functionally correct according to the UTF8 anf UTF16 descriptions in: -https://en.wikipedia.org/wiki/UTF-8 and https://en.wikipedia.org/wiki/UTF-16 - -| Function | Location | -|---------|---------| -|run_utf8_validation| core::src::str::validation | -|next_code_point| core::src::str::validation | -|next_code_point_reverse| core::src::str::validation | -|decode_utf16| core::src::char::decode | -|from_utf8| core::str::converts | -|from_utf8_unchecked| core::str::converts | -|from_utf8_mut| core::str::converts | -|from_utf8_unchecked_mut| core::str::converts | -|chars| core::str::mod | -|char_indices| core::str::mod | -|encode_utf16| core::str::mod| -|from_utf16| alloc::src::string | -|from_utf16_lossy| alloc::src::string | - - - -The verification must be unbounded---it must hold for inputs of arbitrary size. - - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0022-char-pattern.md b/doc/src/challenges/0022-char-pattern.md deleted file mode 100644 index e004796ca5880..0000000000000 --- a/doc/src/challenges/0022-char-pattern.md +++ /dev/null @@ -1,45 +0,0 @@ -# Challenge 23: Verify the correctness of char-related functions in str::pattern - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - - -### Details - -Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. -Those functions is implemented in core::str, but the core of them is implemented in core::str::pattern. -The main purposes of the functions in core::src::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), -then implementing the searching alorithm for those Searchers. - -IMPORTANT NOTE: You can assume the correctness of functions in Challenge 21. - -### Success Criteria - -Verify the memory safety and functional correctness of the following functions in -https://github.com/rust-lang/rust/blob/96cfc75584359ae7ad11cc45968059f29e7b44b7/library/core/src/str/pattern.rs - -1. `next`, `next_match`, `next_back`, `next_match_back`, -which are implemented for `CharSearcher`, `MultiCharEqSearcher`, `CharArraySearcher` , `CharArrayRefSearcher`, `CharSliceSearcher`, `CharPredicateSearcher` -2. `is_contained_in`, `is_prefix_of`, `strip_prefix_of` -which are implemented for `char`, `[char; N]`, `&[char; N]`, `&[char]`, `FnMut(char) -> bool` - -The verification must be unbounded---it must hold for inputs of arbitrary size. - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0023-two-way-search.md b/doc/src/challenges/0023-two-way-search.md deleted file mode 100644 index b7cec2881d6a1..0000000000000 --- a/doc/src/challenges/0023-two-way-search.md +++ /dev/null @@ -1,31 +0,0 @@ -# Challenge 23: Verify the correctness of the Two-Way search algorithm implementation in str::pattern - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - -### Details - -This algorithm is the main component of implementing searching functions for Patterns as substrings. - -### Success Criteria - -Verify the memory safety and functional correctness of the Two-Way search algorithm implementation in core::str::pattern. - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0024-substr-pattern.md b/doc/src/challenges/0024-substr-pattern.md deleted file mode 100644 index 7bf29efd51c04..0000000000000 --- a/doc/src/challenges/0024-substr-pattern.md +++ /dev/null @@ -1,45 +0,0 @@ -# Challenge 23: Verify the correctness of substring-related functions in str::pattern - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - - -### Details - -Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. -Those functions is implemented in core::str, but the core of them is implemented in core::src::str::pattern. -The main purposes of the functions in core::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), -then implementing the searching alorithm for those Searchers. - -IMPORTANT NOTE: You can assume the correctness of the Two-Way search algorithm (see Challenge 23), BUT have to verify the correctness of the simd_contains functions. - -### Success Criteria - -Verify the memory safety and functional correctness of the following functions in -https://github.com/rust-lang/rust/blob/96cfc75584359ae7ad11cc45968059f29e7b44b7/library/core/src/str/pattern.rs - -`next`, `next_match`, `next_back`, `next_match_back` -which are implemented for `StrSearcher` and `is_contained_in`, `is_prefix_of`, `strip_prefix_of`, `is_suffix_of`, `strip_suffix_of` for `&str`. - -The verification must be unbounded---it must hold for inputs of arbitrary size. - - - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0025-str-iter.md b/doc/src/challenges/0025-str-iter.md deleted file mode 100644 index 836503a681c7a..0000000000000 --- a/doc/src/challenges/0025-str-iter.md +++ /dev/null @@ -1,82 +0,0 @@ -# Challenge 25: Correctness of str functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *N/A* - -------------------- - -## Goal - -Verify the correctness of functions in `core::src::str::mod.rs`. - -IMPORTANT NOTE: You can assume the correctness of all the functions that are verified in Challenges 21 to 24, BUT you may have to verify the correctness of other dependent functions in core::str::iter - -### Success Criteria - -Prove the correctness the following functions and methods in `core::str::mod.rs` : -| Function | -|--------- | -| `is_char_boundary`| -| `floor_char_boundary`| -| `ceil_char_boundary`| -| `split_at` | -| `split_at_mut` | -| `split_at_checked` | -| `split_at_mut_checked` | -| `split_at_unchecked` | -| `split_at_mut_unchecked` | -| `split_whitespace` | -| `split_ascii_whitespace` | -| `lines` | -| `lines_any` | -| `starts_with` | -| `ends_with` | -| `find`| -| `rfind`| -| `rotate_left`| -| `rotate_right`| -| `split` | -| `split_inclusive` | -| `rsplit` | -| `split_terminator` | -| `rsplit_terminator` | -| `splitn` | -| `rsplitn` | -| `split_once` | -| `rsplit_once` | -| `matches` | -| `rmatches` | -| `match_indices` | -| `rmatch_indices` | -| `trim` | -| `trim_start` | -| `trim_end` | -| `trim_left` | -| `trim_right` | -| `trim_right` | -| `trim_start_matches` | -| `strip_prefix` | -| `strip_suffix` | -| `trim_end_matches` | -| `trim_left_matches` | -| `trim_right_matches` | - -The verification must be unbounded---it must hold for str of arbitrary size. - - -### List of UBs - -In addition to any properties called out as `SAFETY` comments in the source -code, -all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory. -* Mutating immutable bytes. -* Producing an invalid value - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above.