From 14fc35a16a48334969f7d152b3c3f404de3b994e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 6 Mar 2025 15:46:00 -0800 Subject: [PATCH 01/40] add str-iter challenges --- doc/src/challenges/0020-str-pattern-pt1.md | 63 ++++++++++++++++++++++ doc/src/challenges/0021-str-pattern-pt2.md | 63 ++++++++++++++++++++++ doc/src/challenges/0022-str-iter.md | 60 +++++++++++++++++++++ 3 files changed, 186 insertions(+) create mode 100644 doc/src/challenges/0020-str-pattern-pt1.md create mode 100644 doc/src/challenges/0021-str-pattern-pt2.md create mode 100644 doc/src/challenges/0022-str-iter.md diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md new file mode 100644 index 0000000000000..140a43bf553f3 --- /dev/null +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -0,0 +1,63 @@ +# Challenge 20: Verify the safety 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* + +------------------- + + +### Context + +A majority portion in str library functions take a Pattern (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. +The functions which take Pattern as input turn the input str into a kind of Searcher which iterates over positions where the Pattern match, 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). + +# 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 is a valid utf8 string (str). You can assume any utf8 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. There is no UB happens when calling the functions after the Searcher is created. +2. The impls of unsafe traits `Searcher` and `ReverseSearcher` satisfies the SAFETY condition stated in the file: +``` +/// The trait is marked unsafe because the indices returned by the +/// [`next()`][Searcher::next] methods are required to lie on valid utf8 +/// boundaries in the haystack. This enables consumers of this trait to +/// slice the haystack without additional runtime checks. +``` +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 consider 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. + + +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/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md new file mode 100644 index 0000000000000..7899e264dd5c6 --- /dev/null +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -0,0 +1,63 @@ +# Challenge 20: 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* + +------------------- + + +### Context + +A majority portion in str library functions take a Pattern (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. +The functions which take Pattern as input turn the input str into a kind of `Searcher` 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). + +# 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 is a valid utf8 string (str). You can assume any utf8 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. There is no UB happens when calling the functions after the Searcher is created. +2. The impls of unsafe traits `Searcher` and `ReverseSearcher` satisfies the SAFETY condition stated in the file: +``` +/// The trait is marked unsafe because the indices returned by the +/// [`next()`][Searcher::next] methods are required to lie on valid utf8 +/// boundaries in the haystack. This enables consumers of this trait to +/// slice the haystack without additional runtime checks. +``` +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 `StrSearcher`. + +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. + + +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-str-iter.md b/doc/src/challenges/0022-str-iter.md new file mode 100644 index 0000000000000..f9092054d9d9c --- /dev/null +++ b/doc/src/challenges/0022-str-iter.md @@ -0,0 +1,60 @@ +# Challenge 22: Verify the safety of `str` 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 [`std::str`] functions that are defined in (library/core/src/str/iter.rs): + +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) + + +### Success Criteria + +Write and prove the contract for the safety of the following functions: + + +| Function | Impl for | +|---------| ---------| +|next| Chars| +|advance_by| Chars| +|next_back| Chars| +|as_str| Chars| +|get_end| SplitInternal| +|next| SplitInternal| +|next_inclusive| SplitInternal| +|next_match_back| SplitInternal| +|next_back_inclusive| SplitInternal| +|remainder| SplitInternal| +|next| MatchIndicesInternal| +|next_back| MatchIndicesInternal| +|next| MatchesInternal| +|next_back| MatchesInternal| +|remainder| SplitAsciiWhitespace| + +The verification must be unbounded---it must hold for str of arbitrary length. + + +### 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. From 44b9e12b170da24f5462b7d58351c8da20e10259 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Mar 2025 08:24:30 -0700 Subject: [PATCH 02/40] fix date format --- doc/src/challenges/0020-str-pattern-pt1.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 140a43bf553f3..8b3368a3bb075 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -2,9 +2,9 @@ - **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* +- **Start date:** *2025-03-07* +- **End date:** *2025-10-17* +- **Reward:** *? USD* ------------------- From 766009a473fb7e0cc52ec9b12171537a298a71df Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Mar 2025 08:25:17 -0700 Subject: [PATCH 03/40] fix date format --- doc/src/challenges/0021-str-pattern-pt2.md | 8 ++++---- doc/src/challenges/0022-str-iter.md | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index 7899e264dd5c6..f5688dee891ad 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -1,10 +1,10 @@ -# Challenge 20: Verify the correctness of char-related functions in str::pattern +# Challenge 21: 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* +- **Start date:** *2025-03-07* +- **End date:** *2025-10-17* +- **Reward:** *? USD* ------------------- diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index f9092054d9d9c..3e997bbc9c73d 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -2,8 +2,8 @@ - **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* +- **Start date:** *2025-03-07* +- **End date:** *2025-10-17* - **Reward:** *?* ------------------- From 83f112d6ff56861d09bb4df9d7f7c9bda44b6bd6 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 08:34:43 -0700 Subject: [PATCH 04/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Michael Tautschnig --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 8b3368a3bb075..556fb5b0ec5bb 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -19,7 +19,7 @@ Those functions is implemented in (library/core/src/str/mod.rs), but the core of 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) . +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 is a valid utf8 string (str). You can assume any utf8 string property of haystack. Verify the safety of the functions in (library/core/src/str/pattern.rs) listed in the next section. From 495e44fbe649ada9d82645c668c5a8df845eb34b Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 08:35:33 -0700 Subject: [PATCH 05/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Michael Tautschnig --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 556fb5b0ec5bb..4a9aae701c236 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -13,7 +13,7 @@ A majority portion in str library functions take a Pattern (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. The functions which take Pattern as input turn the input str into a kind of Searcher which iterates over positions where the Pattern match, 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). +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 From 34a29edf552b6b659bbd980d2ed6f46b0b8cc113 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 08:35:49 -0700 Subject: [PATCH 06/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Michael Tautschnig --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 4a9aae701c236..3c5459f7096b6 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -26,7 +26,7 @@ Verify the safety of the functions in (library/core/src/str/pattern.rs) listed i The safety properties we are targeting are: 1. There is no UB happens when calling the functions after the Searcher is created. -2. The impls of unsafe traits `Searcher` and `ReverseSearcher` satisfies the SAFETY condition stated in the file: +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 /// [`next()`][Searcher::next] methods are required to lie on valid utf8 From 51f3854c012bec3df00959d498bfeb91cd82dd69 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 08:37:23 -0700 Subject: [PATCH 07/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Michael Tautschnig --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 3c5459f7096b6..083c6d3890ecd 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -20,7 +20,7 @@ Those functions are implemented in (library/core/src/str/mod.rs), but the core o 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 is a valid utf8 string (str). You can assume any utf8 string property of haystack. +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. Verify the safety of the functions in (library/core/src/str/pattern.rs) listed in the next section. From 00ed97ee99a7659587f2eebb50feed32b726d7ca Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 08:38:03 -0700 Subject: [PATCH 08/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Michael Tautschnig --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 083c6d3890ecd..5f8683fa9ca78 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -25,7 +25,7 @@ IMPORTANT NOTE: for this challenge, you can assume: 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. There is no UB happens when calling the functions after the Searcher is created. +1. No UB occurs when calling the functions 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 From 5aa096c021aadfc44ddb15ef2875821b65f995ca Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 09:02:09 -0700 Subject: [PATCH 09/40] fix issue link, reward and some typos --- doc/src/challenges/0020-str-pattern-pt1.md | 14 +++++++------- doc/src/challenges/0021-str-pattern-pt2.md | 12 ++++++------ doc/src/challenges/0022-str-iter.md | 8 ++++---- 3 files changed, 17 insertions(+), 17 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 5f8683fa9ca78..002471eba2f4a 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -1,23 +1,23 @@ # Challenge 20: Verify the safety of char-related functions in str::pattern - **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#277](https://github.com/model-checking/verify-rust-std/issues/277) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *? USD* +- **Reward:** *5000 USD* ------------------- ### Context -A majority portion in str library functions take a Pattern (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. -The functions which take Pattern as input turn the input str into a kind of Searcher which iterates over positions where the Pattern match, then perform their desired operations (split, find, ...). +A majority portion in str library functions take a `Pattern` (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. +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, ...). 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: +**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. @@ -38,8 +38,8 @@ 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`. +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 consider 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. diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index f5688dee891ad..a44e1b6ab9c5a 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -1,10 +1,10 @@ -# Challenge 21: Verify the correctness of char-related functions in str::pattern +# Challenge 21: Verify the safety of char-related functions in str::pattern - **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#278](https://github.com/model-checking/verify-rust-std/issues/278) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *? USD* +- **Reward:** *5000 USD* ------------------- @@ -12,12 +12,12 @@ ### Context A majority portion in str library functions take a Pattern (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. -The functions which take Pattern as input turn the input str into a kind of `Searcher` which iterates over positions where the Pattern matches, then perform their desired operations (split, find, ...). +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). # Details -IMPORTANT NOTE: for this challenge, you can assume: +**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 is a valid utf8 string (str). You can assume any utf8 string property of haystack. @@ -38,7 +38,7 @@ 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` +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`. The verification is consider successful if you can specify a condition (a "type invariant") C and prove that: diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index 3e997bbc9c73d..25b6f12b9366f 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -1,10 +1,10 @@ -# Challenge 22: Verify the safety of `str` iter functions - part 2 +# Challenge 22: Verify the safety of `str` iter functions - **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#279](https://github.com/model-checking/verify-rust-std/issues/279) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *?* +- **Reward:** *5000* ------------------- @@ -13,7 +13,7 @@ Verify the safety of [`std::str`] functions that are defined in (library/core/src/str/iter.rs): -IMPORTANT NOTE: for this challenge, you can assume: +**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). From e2aec463010ce0a646de70363b0a05b1d9a0758d Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 09:04:02 -0700 Subject: [PATCH 10/40] some typos --- doc/src/challenges/0021-str-pattern-pt2.md | 4 ++-- doc/src/challenges/0022-str-iter.md | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index a44e1b6ab9c5a..c07a805b0a862 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -18,8 +18,8 @@ Those functions is implemented in (library/core/src/str/mod.rs), but the core of # 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) . +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 is a valid utf8 string (str). You can assume any utf8 string property of haystack. Verify the safety of the functions in (library/core/src/str/pattern.rs) listed in the next section. diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index 25b6f12b9366f..fd8ffe95b65bb 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -14,10 +14,10 @@ Verify the safety of [`std::str`] functions that are defined in (library/core/src/str/iter.rs): **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) +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) +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). ### Success Criteria From 09c2f99ff4ce2794438492c940a8d2603fe9659b Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 10:29:18 -0700 Subject: [PATCH 11/40] fix a typo --- doc/src/challenges/0021-str-pattern-pt2.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index c07a805b0a862..ecaf64ea826e9 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -1,4 +1,4 @@ -# Challenge 21: Verify the safety of char-related functions in str::pattern +# Challenge 21: Verify the safety of substring-related functions in str::pattern - **Status:** Open - **Tracking Issue:** [#278](https://github.com/model-checking/verify-rust-std/issues/278) From 470897cc0c2b9eb28b35ad2e9169e663b14b120a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Mar 2025 08:48:31 -0700 Subject: [PATCH 12/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 002471eba2f4a..00aec7e59b5b6 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -25,7 +25,7 @@ Those functions are implemented in (library/core/src/str/mod.rs), but the core o 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 UB occurs when calling the functions after the Searcher is created. +1. No undefined behavior occurs when calling the functions 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 From 3cceb5c694c49d7c96811db1e2a6ed7d2043a74f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Mar 2025 08:48:44 -0700 Subject: [PATCH 13/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 00aec7e59b5b6..f66387ebab1e2 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -41,7 +41,7 @@ This property should hold for next_back() of `ReverseSearcher` too. 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 consider successful if for each `Searcher` above, you can specify a condition (a "type invariant") C and prove that: +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. From 7c2b29eed0a2ce057e810bbcea60437440516015 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Mar 2025 09:30:48 -0700 Subject: [PATCH 14/40] update summary.md --- doc/src/SUMMARY.md | 3 +++ doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index f1de498184d14..188f6d0e949dc 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -29,3 +29,6 @@ - [13: Safety of `CStr`](./challenges/0013-cstr.md) - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md) - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md) + - [20: Verify the safety of char-related functions in str::pattern](./challenges/0020-str-pattern-pt1.md) + - [21: Verify the safety of substring-related functions in str::pattern](./challenges/0021-str-pattern-pt2.md) + - [22: Verify the safety of str iter functions](./challenges/0022-str-iter.md) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 002471eba2f4a..20c7b6e18b1db 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -11,7 +11,7 @@ ### Context -A majority portion in str library functions take a `Pattern` (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. +A majority portion in str library functions are generic over the `Pattern` trait (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html). 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, ...). 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). From 0c02e9394681bd5ed103dbe6d95c99910dcf8a0a Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 20 Mar 2025 10:03:29 -0700 Subject: [PATCH 15/40] add UB check requirement --- doc/src/challenges/0020-str-pattern-pt1.md | 5 ++++- doc/src/challenges/0021-str-pattern-pt2.md | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 4920f1956cdc4..9d422cb0ae926 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -11,7 +11,9 @@ ### Context -A majority portion in str library functions are generic over the `Pattern` trait (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html). +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, ...). 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). @@ -46,6 +48,7 @@ The verification is considered successful if for each `Searcher` above, you can 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. +Furthermore, you must prove the absence of undefined behaviors listed in the next section. The verification must be unbounded---it must hold for inputs of arbitrary size. diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index ecaf64ea826e9..6a6633c77005e 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -11,7 +11,9 @@ ### Context -A majority portion in str library functions take a Pattern (https://doc.rust-lang.org/std/str/pattern/trait.Pattern.html) as input. +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). @@ -46,6 +48,7 @@ The verification is consider successful if you can specify a condition (a "type 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. +Furthermore, you must prove the absence of undefined behaviors listed in the next section. The verification must be unbounded---it must hold for inputs of arbitrary size. From b490be88825c7f0fcdcb0b201218d7d6811a4eb5 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:30:54 -0700 Subject: [PATCH 16/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 9d422cb0ae926..581e3bafaa8cb 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -14,7 +14,7 @@ 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, ...). +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 From f2a6d63fd383ce617bb8e3648f3968a7ab027d73 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:31:10 -0700 Subject: [PATCH 17/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 24 ++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 581e3bafaa8cb..6a92a0eebee82 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -12,8 +12,28 @@ ### 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. +- `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). From 6f2f7199deb3c9521ae15cac38f5502a7e3f9931 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:31:22 -0700 Subject: [PATCH 18/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 6a92a0eebee82..f1f88cadf1bed 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -41,8 +41,8 @@ Those functions are implemented in (library/core/src/str/mod.rs), but the core o **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. From 13eae8c5fe175e6f41bd7e7cec0503f187ebbf55 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:31:31 -0700 Subject: [PATCH 19/40] Update doc/src/challenges/0021-str-pattern-pt2.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0021-str-pattern-pt2.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index 6a6633c77005e..e06a588610edb 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -40,8 +40,13 @@ 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 `StrSearcher`. +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 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. From fe78182d1b5b2b623270f593b28c1b4f8d1585a2 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:31:53 -0700 Subject: [PATCH 20/40] Update doc/src/challenges/0021-str-pattern-pt2.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0021-str-pattern-pt2.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index e06a588610edb..3074e37aefab8 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -48,10 +48,10 @@ Verify the safety of the following `StrSearcher` functions in (library/core/src/ - `next_reject` - `next_back_reject` -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. +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. From 58c29afd8360bf025f8abf02dda569414867d5c5 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:32:02 -0700 Subject: [PATCH 21/40] Update doc/src/challenges/0022-str-iter.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0022-str-iter.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index fd8ffe95b65bb..b90c06ca3d689 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -16,8 +16,8 @@ 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 From 8c07a6113feca9ab6598089f2f8f8f07ef93cb7e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:32:18 -0700 Subject: [PATCH 22/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index f1f88cadf1bed..76856325a3c55 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -47,7 +47,7 @@ Those functions are implemented in (library/core/src/str/mod.rs), but the core o 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 From fc305628525b918f20ed08b9aafacd5b3bbbee23 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:32:33 -0700 Subject: [PATCH 23/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 76856325a3c55..af31323ff338f 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -60,8 +60,20 @@ 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. +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 utf8 haystack, it satisfies C. From 4ae8c79786d47bd412b9634577e077f184948b00 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:34:49 -0700 Subject: [PATCH 24/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index af31323ff338f..0681263fd06ac 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -75,10 +75,10 @@ for the following `Searcher`s: - `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. +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. From 542ddc7ee6ac8ecc740e80e97ccdfcbeb2136571 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 11:42:00 -0700 Subject: [PATCH 25/40] change reward for ch 20 21 --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- doc/src/challenges/0021-str-pattern-pt2.md | 30 ++++++++++++++++++---- 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 0681263fd06ac..a2b0a31a44de0 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -4,7 +4,7 @@ - **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* ------------------- diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index 3074e37aefab8..1c82d59dd5a51 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -4,7 +4,7 @@ - **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* ------------------- @@ -12,10 +12,30 @@ ### 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 From fd6dbfe1a072cf269674ba969d9cf03324644ac8 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 12:05:32 -0700 Subject: [PATCH 26/40] complexity of challenge 21 --- doc/src/challenges/0021-str-pattern-pt2.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index 1c82d59dd5a51..15b0e70462020 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -57,6 +57,10 @@ 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 From d34f1cbefb236225b920095bc406ffbb3b2b99b2 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 24 Mar 2025 13:15:41 -0700 Subject: [PATCH 27/40] separate safe/unsafe functions in challenge 22 --- doc/src/challenges/0022-str-iter.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index b90c06ca3d689..e73c8129704f4 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -22,7 +22,7 @@ Verify the safety of [`std::str`] functions that are defined in (library/core/sr ### 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. From 27119608d18e189dfcdbdd3d32fa5bc9004ee185 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 28 Mar 2025 15:37:52 -0700 Subject: [PATCH 28/40] Update doc/src/challenges/0021-str-pattern-pt2.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0021-str-pattern-pt2.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index 15b0e70462020..f2b379a85d952 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -57,9 +57,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 From 279efe698fcec70f1c392d57d3ae3c163cf06c9e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 28 Mar 2025 15:38:27 -0700 Subject: [PATCH 29/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index a2b0a31a44de0..a1766c026eaed 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -7,6 +7,8 @@ - **Reward:** *10000 USD* ------------------- +## Goal +Verify the safety of `Searcher` methods in `str::pattern`. ### Context From 947538ebebe715e6747b48f3dde16779e4a4952f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 28 Mar 2025 15:39:12 -0700 Subject: [PATCH 30/40] Update doc/src/challenges/0022-str-iter.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0022-str-iter.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index e73c8129704f4..3dfcb48b4d6f1 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -43,7 +43,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. From f0fbb0c2e2f817cd84abb725136fc0247de53a91 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 31 Mar 2025 10:44:43 -0700 Subject: [PATCH 31/40] fixing the template --- doc/src/challenges/0020-str-pattern-pt1.md | 9 ++++++--- doc/src/challenges/0021-str-pattern-pt2.md | 9 +++++++-- doc/src/challenges/0022-str-iter.md | 6 ++++++ 3 files changed, 19 insertions(+), 5 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index a1766c026eaed..7ad61db3e0118 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -8,10 +8,13 @@ ------------------- ## Goal -Verify the safety of `Searcher` methods in `str::pattern`. +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` @@ -39,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. diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index f2b379a85d952..f88bc57dc889b 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/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. diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index 3dfcb48b4d6f1..d0c6c930ce001 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/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). From 74e044e969c5dc44fdb439d57a6b9e88aaefa452 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 07:53:29 -0700 Subject: [PATCH 32/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 7ad61db3e0118..0d282d86345b9 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -12,7 +12,7 @@ Verify the safety of char-related `Searcher` methods in `str::pattern`. ## 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. +String and `str` types are widely used in Rust programs, so it is important that their associated functions do not cause undefined behavior. ## Description From 00d288c21a77dcf5853e21275389079af3d70c14 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 07:53:40 -0700 Subject: [PATCH 33/40] Update doc/src/challenges/0021-str-pattern-pt2.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0021-str-pattern-pt2.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index f88bc57dc889b..59984120cfb80 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -12,7 +12,7 @@ Verify the safety of `StrSearcher` implementation in `str::pattern`. ## 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. +String and `str` types are widely used in Rust programs, so it is important that their associated functions do not cause undefined behavior. ## Description From a24cc0f543c6da31eaa93d017413c8aa7480a490 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 07:53:50 -0700 Subject: [PATCH 34/40] Update doc/src/challenges/0020-str-pattern-pt1.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index 0d282d86345b9..e93de5e5991d7 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -42,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). -### Assumption +### Assumptions **Important note:** for this challenge, you can assume: 1. The safety and functional correctness of all functions in `slice` module. From 8d98b12ea7f8e81bccf94fc74f7a18c6d063efd3 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 07:53:56 -0700 Subject: [PATCH 35/40] Update doc/src/challenges/0022-str-iter.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0022-str-iter.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index d0c6c930ce001..e084acdab0732 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -15,8 +15,7 @@ Verify the safety of [`std::str`] functions that are defined in (library/core/sr ## 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. - +String and `str` types are widely used in Rust programs, so it is important that their associated functions do not cause undefined behavior. ## Description **Important note:** for this challenge, you can assume: From f30067b7a33f64dedf370e160e95d83f5cba1430 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 07:54:05 -0700 Subject: [PATCH 36/40] Update doc/src/challenges/0022-str-iter.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0022-str-iter.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index e084acdab0732..67ada27183841 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -48,7 +48,7 @@ Prove the safety of the following safe functions that contain unsafe code: |next_back| MatchesInternal| |remainder| SplitAsciiWhitespace| -Write and prove the safety 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. From 0b13289d898b9eb58b204df7de4ecd1a4e02dc71 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 07:54:23 -0700 Subject: [PATCH 37/40] Update doc/src/challenges/0021-str-pattern-pt2.md Co-authored-by: Carolyn Zech --- doc/src/challenges/0021-str-pattern-pt2.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index 59984120cfb80..47b6fe0a49448 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -42,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). -### Assumption +### Assumptions **Important note:** for this challenge, you can assume: 1. The safety and functional correctness of all functions in `slice` module. From ffbfee312b6e7796877be9527c266b3f97a4f6d0 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 3 Apr 2025 08:01:11 -0700 Subject: [PATCH 38/40] update reward --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- doc/src/challenges/0021-str-pattern-pt2.md | 2 +- doc/src/challenges/0022-str-iter.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index e93de5e5991d7..b54202cbbd890 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -4,7 +4,7 @@ - **Tracking Issue:** [#277](https://github.com/model-checking/verify-rust-std/issues/277) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *10000 USD* +- **Reward:** *25000 USD* ------------------- ## Goal diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index 47b6fe0a49448..cd43d0b5e0c7e 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -4,7 +4,7 @@ - **Tracking Issue:** [#278](https://github.com/model-checking/verify-rust-std/issues/278) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *10000 USD* +- **Reward:** *25000 USD* ------------------- ## Goal diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md index 67ada27183841..8dee36bc2a0cc 100644 --- a/doc/src/challenges/0022-str-iter.md +++ b/doc/src/challenges/0022-str-iter.md @@ -4,7 +4,7 @@ - **Tracking Issue:** [#279](https://github.com/model-checking/verify-rust-std/issues/279) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *5000* +- **Reward:** *10000* ------------------- From 07c0ff44977740ef9ddfd58bb3b16c77ef63b367 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Apr 2025 12:34:16 +0200 Subject: [PATCH 39/40] Update doc/src/challenges/0020-str-pattern-pt1.md --- doc/src/challenges/0020-str-pattern-pt1.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md index b54202cbbd890..03810be562050 100644 --- a/doc/src/challenges/0020-str-pattern-pt1.md +++ b/doc/src/challenges/0020-str-pattern-pt1.md @@ -40,7 +40,7 @@ The following str library functions are generic over the `Pattern` trait (https: - `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). +Those functions are implemented in (library/core/src/str/mod.rs), but the core of them are the searching algorithms which are implemented in (library/core/src/str/pattern.rs). ### Assumptions From 3fd252782e00dc27896b846a34c432ae1a3d0ad3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Apr 2025 12:34:23 +0200 Subject: [PATCH 40/40] Update doc/src/challenges/0021-str-pattern-pt2.md --- doc/src/challenges/0021-str-pattern-pt2.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md index cd43d0b5e0c7e..e8a6bb6ed7bf0 100644 --- a/doc/src/challenges/0021-str-pattern-pt2.md +++ b/doc/src/challenges/0021-str-pattern-pt2.md @@ -40,7 +40,7 @@ The following str library functions are generic over the `Pattern` trait (https: - `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). +Those functions are implemented in (library/core/src/str/mod.rs), but the core of them are the searching algorithms which are implemented in (library/core/src/str/pattern.rs). ### Assumptions