Add Challenges 20 21 22 for str Pattern and iter

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

@@ -7,9 +7,14 @@
 - **Reward:** *10000 USD*
 
 -------------------
+## Goal
+Verify the safety of char-related `Searcher` methods in `str::pattern`.
 
+## Motivation
 
-### Context
+String and str types are widely used in Rust programs. Verifying Rust String and str functions in Rust standard library is important in ensuring the safety of these programs.
+
+## Description
 
 The following str library functions are generic over the `Pattern` trait (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html): 
 - `contains`
@@ -37,7 +42,7 @@ The following str library functions are generic over the `Pattern` trait (https:
 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
+### Assumption
 
 **Important note:** for this challenge, you can assume: 
 1. The safety and functional correctness of all functions in `slice` module.

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

@@ -7,9 +7,14 @@
 - **Reward:** *10000 USD*
 
 -------------------
+## Goal
+Verify the safety of `StrSearcher` implementation in `str::pattern`.
 
+## Motivation
 
-### Context
+String and str types are widely used in Rust programs. Verifying Rust String and str functions in Rust standard library is important in ensuring the safety of these programs.
+
+## Description
 
 The following str library functions are generic over the `Pattern` trait (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html): 
 - `contains`
@@ -37,7 +42,7 @@ The following str library functions are generic over the `Pattern` trait (https:
 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
+### Assumption
 
 **Important note:** for this challenge, you can assume: 
 1. The safety and functional correctness of all functions in `slice` module. 
@@ -57,9 +62,6 @@ 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

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

@@ -13,6 +13,12 @@
 
 Verify the safety of [`std::str`] functions that are defined in (library/core/src/str/iter.rs):
 
+## Motivation
+
+String and str types are widely used in Rust programs. Verifying Rust String and str functions in Rust standard library is important in ensuring the safety of these programs.
+
+## Description
+
 **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).
@@ -43,7 +49,7 @@ Prove the safety of the following safe functions that contain unsafe code:
 |next_back| MatchesInternal|
 |remainder| SplitAsciiWhitespace|
 
-Write and prove the contract for this unsafe function: __iterator_get_unchecked
+Write and prove the safety contract for this unsafe function: __iterator_get_unchecked
 
 The verification must be unbounded---it must hold for str of arbitrary length.