Add Challenges 20 21 22 for str Pattern and iter

doc/src/challenges/0020-str-pattern-pt1.md

@@ -4,30 +4,50 @@
 - **Tracking Issue:** [#277](https://github.com/model-checking/verify-rust-std/issues/277)
 - **Start date:** *2025-03-07*
 - **End date:** *2025-10-17*
-- **Reward:** *5000 USD*
+- **Reward:** *10000 USD*
 
 -------------------
 
 
 ### Context
 
 The following str library functions are generic over the `Pattern` trait (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html): 
-contains, starts_with, ends_with, find, rfind, split, split_inclusive, rsplit, split_terminator, rsplit_terminator, splitn, rsplitn, split_once, rsplit_once, rmatches, match_indices, rmatch_indices, trim_matches, trim_start_matches,
-strip_prefix, strip_suffix, trim_end_matches.
-The functions which take Pattern as input turn the input str into a kind of `Searcher` (https://doc.rust-lang.org/std/str/pattern/trait.Searcher.html)  which iterates over positions where the Pattern match, then perform their desired operations (split, find, ...).
+- `contains`
+- `starts_with`
+- `ends_with`
+- `find` 
+- `rfind`
+- `split`
+- `split_inclusive`
+- `rsplit`
+- `split_terminator`
+- `rsplit_terminator`
+- `splitn`
+- `rsplitn`
+- `split_once`
+- `rsplit_once`
+- `rmatches`
+- `match_indices`
+- `rmatch_indices`
+- `trim_matches`
+- `trim_start_matches`
+- `strip_prefix`
+- `strip_suffix`
+- `trim_end_matches`
+These functions accept a pattern as input, then call [into_searcher](https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html#tymethod.into_searcher) to create a [Searcher](https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html#associatedtype.Searcher) for the pattern. They use this `Searcher` to perform their desired operations (split, find, etc.).
 Those functions are implemented in (library/core/src/str/mod.rs), but the core of them is the searching algorithms which are implemented in (library/core/src/str/pattern.rs).
 
 # Details
 
 **Important note:** for this challenge, you can assume: 
 1. The safety and functional correctness of all functions in `slice` module.
-2. That all functions in (library/core/src/str/validations.rs) are functionally correct (consistent with the UTF8 encoding description in https://en.wikipedia.org/wiki/UTF-8). 
-3. That all the Searchers in (library/core/src/str/iter.rs) are created by the into_searcher(_, haystack) with haystack being a valid utf8 string (str). You can assume any utf8 string property of haystack.
+2. That all functions in (library/core/src/str/validations.rs) are functionally correct (consistent with the UTF-8 encoding description in https://en.wikipedia.org/wiki/UTF-8). 
+3. That all the Searchers in (library/core/src/str/iter.rs) are created by the into_searcher(_, haystack) with haystack being a valid UTF-8 string (str). You can assume any UTF-8 string property of haystack.
 
 Verify the safety of the functions in (library/core/src/str/pattern.rs) listed in the next section.
 
 The safety properties we are targeting are: 
-1. No undefined behavior occurs when calling the functions after the Searcher is created.
+1. No undefined behavior occurs after the Searcher is created.
 2. The impls of unsafe traits `Searcher` and `ReverseSearcher` satisfy the SAFETY condition stated in the file: 
 ```
 /// The trait is marked unsafe because the indices returned by the
@@ -40,13 +60,25 @@ This property should hold for next_back() of `ReverseSearcher` too.
 
 ### Success Criteria
 
-Verify the safety of the following functions in (library/core/src/str/pattern.rs) : next, next_match, next_back, next_match_back, next_reject, next_back_reject
-which are implemented for the following `Searcher`s:  CharSearcher, MultiCharEqSearcher, CharArraySearcher , CharArrayRefSearcher, CharSliceSearcher, CharPredicateSearcher.
-
-The verification is considered successful if for each `Searcher` above, you can specify a condition (a "type invariant") C and prove that:
-1. If the `Searcher` is created from any valid utf8 haystack, it satisfies C.
-2. If the `Searcher` satisfies C, it ensures the two safety properties mentioned in the previous section.
-3. If the `Searcher` satisfies C, after it calls any function above and gets modified, it still statisfies C.
+Verify the safety of the following functions in (library/core/src/str/pattern.rs) : 
+- `next`
+- `next_match`
+- `next_back`
+- `next_match_back`
+- `next_reject`
+- `next_back_reject`
+for the following `Searcher`s: 
+- `CharSearcher`
+- `MultiCharEqSearcher`
+- `CharArraySearcher`
+- `CharArrayRefSearcher`
+- `CharSliceSearcher`
+- `CharPredicateSearcher`
+
+The verification is considered successful if for each `Searcher` above, you can specify a condition (a "type invariant") `C` and prove that:
+1. If the `Searcher` is created from any valid UTF-8 haystack, it satisfies `C`.
+2. If the `Searcher` satisfies `C`, it ensures the two safety properties mentioned in the previous section.
+3. If the `Searcher` satisfies `C`, after it calls any function above and gets modified, it still satisfies `C`.
 
 Furthermore, you must prove the absence of undefined behaviors listed in the next section.
 

doc/src/challenges/0021-str-pattern-pt2.md

@@ -4,18 +4,38 @@
 - **Tracking Issue:** [#278](https://github.com/model-checking/verify-rust-std/issues/278)
 - **Start date:** *2025-03-07*
 - **End date:** *2025-10-17*
-- **Reward:** *5000 USD*
+- **Reward:** *10000 USD*
 
 -------------------
 
 
 ### Context
 
 The following str library functions are generic over the `Pattern` trait (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html): 
-contains, starts_with, ends_with, find, rfind, split, split_inclusive, rsplit, split_terminator, rsplit_terminator, splitn, rsplitn, split_once, rsplit_once, rmatches, match_indices, rmatch_indices, trim_matches, trim_start_matches,
-strip_prefix, strip_suffix, trim_end_matches.
-The functions which take Pattern as input turn the input str into a kind of `Searcher` (https://doc.rust-lang.org/std/str/pattern/trait.Searcher.html) which iterates over positions where the Pattern matches, then perform their desired operations (split, find, ...).
-Those functions is implemented in (library/core/src/str/mod.rs), but the core of them is the searching algorithms which are implemented in (library/core/src/str/pattern.rs).
+- `contains`
+- `starts_with`
+- `ends_with`
+- `find` 
+- `rfind`
+- `split`
+- `split_inclusive`
+- `rsplit`
+- `split_terminator`
+- `rsplit_terminator`
+- `splitn`
+- `rsplitn`
+- `split_once`
+- `rsplit_once`
+- `rmatches`
+- `match_indices`
+- `rmatch_indices`
+- `trim_matches`
+- `trim_start_matches`
+- `strip_prefix`
+- `strip_suffix`
+- `trim_end_matches`
+These functions accept a pattern as input, then call [into_searcher](https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html#tymethod.into_searcher) to create a [Searcher](https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html#associatedtype.Searcher) for the pattern. They use this `Searcher` to perform their desired operations (split, find, etc.).
+Those functions are implemented in (library/core/src/str/mod.rs), but the core of them is the searching algorithms which are implemented in (library/core/src/str/pattern.rs).
 
 # Details
 
@@ -37,16 +57,25 @@ The safety properties we are targeting are:
 ```
 This property should hold for next_back() of `ReverseSearcher` too.
 
+Although this challenge appears similar to Challenge 20 and only requires proving safety for the `StrSearcher` implementation, 
+it warrants being a separate challenge due to its complexity. 
+The `StrSearcher` implementation relies on sophisticated algorithms - TwoWay-Search and SIMD-search - making the safety proof significantly more complex.
 
-### Success Criteria
 
-Verify the safety of the following functions in (library/core/src/str/pattern.rs) : next, next_match, next_back, next_match_back, next_reject, next_back_reject
-which are implemented for `StrSearcher`.
+### Success Criteria
 
-The verification is consider successful if you can specify a condition (a "type invariant") C and prove that:
-1. If the `StrSearcher` is created from any valid utf8 haystack, it satisfies C.
-2. If the `StrSearcher` satisfies C, it ensures the two safety properties mentioned in the previous section.
-3. If the `StrSearcher` satisfies C, after it calls any function above and gets modified, it still statisfies C.
+Verify the safety of the following `StrSearcher` functions in (library/core/src/str/pattern.rs): 
+- `next`
+- `next_match`
+- `next_back`
+- `next_match_back`
+- `next_reject`
+- `next_back_reject`
+
+The verification is considered successful if you can specify a condition (a "type invariant") `C` and prove that:
+1. If the `StrSearcher` is created from any valid UTF-8 haystack, it satisfies `C`.
+2. If the `StrSearcher` satisfies `C`, it ensures the two safety properties mentioned in the previous section.
+3. If the `StrSearcher` satisfies `C`, after it calls any function above and gets modified, it still satisfies `C`.
 
 Furthermore, you must prove the absence of undefined behaviors listed in the next section.
 

doc/src/challenges/0022-str-iter.md

@@ -16,13 +16,13 @@ Verify the safety of [`std::str`] functions that are defined in (library/core/sr
 **Important note:** for this challenge, you can assume: 
 1. The safety and functional correctness of all functions in `slice` module. 
 2. The safety and functional correctness of all functions in (library/core/src/str/pattern.rs).
-3. That all functions in (library/core/src/str/validations.rs) are functionally correct (consistent with the UTF8 encoding description in https://en.wikipedia.org/wiki/UTF-8). 
-4. That all the Iterators in (library/core/src/str/iter.rs) are derived from a valid utf8 string (str) (You can assume any property of valid utf8 encoded string).
+3. That all functions in (library/core/src/str/validations.rs) are functionally correct (consistent with the UTF-8 encoding description in https://en.wikipedia.org/wiki/UTF-8). 
+4. That all the Iterators in (library/core/src/str/iter.rs) are derived from a valid UTF-8 string (str) (You can assume any property of valid UTF-8 encoded string).
 
 
 ### Success Criteria
 
-Write and prove the contract for the safety of the following functions:
+Prove the safety of the following safe functions that contain unsafe code:
 
 
 | Function | Impl for |
@@ -43,6 +43,8 @@ Write and prove the contract for the safety of the following functions:
 |next_back| MatchesInternal|
 |remainder| SplitAsciiWhitespace|
 
+Write and prove the contract for this unsafe function: __iterator_get_unchecked
+
 The verification must be unbounded---it must hold for str of arbitrary length.