From 6b0fcb151c00e4cde50583ebae15beb953bd9319 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 17 Feb 2025 13:03:09 -0800 Subject: [PATCH 01/18] add empty files --- doc/src/challenges/0016-iteration-correctness.md | 0 doc/src/challenges/0017-str.md | 0 doc/src/challenges/0018-intrinsic-math-error.md | 0 doc/src/challenges/0019-silce.md | 0 doc/src/challenges/0020-math-function.md | 0 doc/src/challenges/0021-hashmap.md | 0 doc/src/challenges/0022-vector.md | 0 7 files changed, 0 insertions(+), 0 deletions(-) create mode 100644 doc/src/challenges/0016-iteration-correctness.md create mode 100644 doc/src/challenges/0017-str.md create mode 100644 doc/src/challenges/0018-intrinsic-math-error.md create mode 100644 doc/src/challenges/0019-silce.md create mode 100644 doc/src/challenges/0020-math-function.md create mode 100644 doc/src/challenges/0021-hashmap.md create mode 100644 doc/src/challenges/0022-vector.md diff --git a/doc/src/challenges/0016-iteration-correctness.md b/doc/src/challenges/0016-iteration-correctness.md new file mode 100644 index 0000000000000..e69de29bb2d1d diff --git a/doc/src/challenges/0017-str.md b/doc/src/challenges/0017-str.md new file mode 100644 index 0000000000000..e69de29bb2d1d diff --git a/doc/src/challenges/0018-intrinsic-math-error.md b/doc/src/challenges/0018-intrinsic-math-error.md new file mode 100644 index 0000000000000..e69de29bb2d1d diff --git a/doc/src/challenges/0019-silce.md b/doc/src/challenges/0019-silce.md new file mode 100644 index 0000000000000..e69de29bb2d1d diff --git a/doc/src/challenges/0020-math-function.md b/doc/src/challenges/0020-math-function.md new file mode 100644 index 0000000000000..e69de29bb2d1d diff --git a/doc/src/challenges/0021-hashmap.md b/doc/src/challenges/0021-hashmap.md new file mode 100644 index 0000000000000..e69de29bb2d1d diff --git a/doc/src/challenges/0022-vector.md b/doc/src/challenges/0022-vector.md new file mode 100644 index 0000000000000..e69de29bb2d1d From d42bdf65c1ba65f4453816935e496c7132d618db Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Feb 2025 12:43:20 -0800 Subject: [PATCH 02/18] add 2 more challenges --- .../challenges/0023-nonzero-correctness.md | 74 +++++++++++++++++++ .../0024-integer-function-correctness.md | 0 2 files changed, 74 insertions(+) create mode 100644 doc/src/challenges/0023-nonzero-correctness.md create mode 100644 doc/src/challenges/0024-integer-function-correctness.md diff --git a/doc/src/challenges/0023-nonzero-correctness.md b/doc/src/challenges/0023-nonzero-correctness.md new file mode 100644 index 0000000000000..eb71661b46289 --- /dev/null +++ b/doc/src/challenges/0023-nonzero-correctness.md @@ -0,0 +1,74 @@ +# Challenge 23: Correctness of `NonZero` functions + +- **Status:** Open +- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) +- **Start date:** *2025/02/24* +- **End date:** *2025/08/24* +- **Reward:** *N/A* + +------------------- + +## Goal + +Verify the correctness of `NonZero` functions in `core::num`. + +### Assumptions + +This challenge is the continuation of Challenge 12: Safety of `NonZero` and Challenge 14: Safety of Primitive Conversions. + +Now, you need to verify the "correctness" of the functions listed in Challenge 12. + +HOWEVER, You DON'T need to prove the "correctness" from the functions' descriptions, you JUST need to prove that those functions are consistent with those of +the primitive integer types (under safety preconditions of Challenge 12). + +For example, for the `max` function, you need to prove that +`∀ T in {isize, i8, i16, ... , usize, u8, ... }, ∀ x, y : NonZero, x.max(y).get() == x.get().max(y.get())` + +Proving the correctness of the functions of primitive integer types is proposed in Challenge 24. + +### Success Criteria + +Verify that the following functions and methods (all located within `core::num::nonzero`) are consistent with those of all of the primitive integer types: + +| Function | +|--------- | +| `max` | +| `min` | +| `clamp` | +| `bitor` (all 3 implementations) | +| `count_ones` | +| `rotate_left` | +| `rotate_right` | +| `swap_bytes` | +| `reverse_bits` | +| `from_be` | +| `from_le` | +| `to_be` | +| `to_le` | +| `checked_mul` | +| `saturating_mul` | +| `unchecked_mul` | +| `checked_pow` | +| `saturating_pow` | +| `neg` | +| `checked_add` | +| `saturating_add` | +| `unchecked_add` | +| `checked_next_power_of_two` | +| `midpoint` | +| `isqrt` | +| `abs` | +| `checked_abs` | +| `overflowing_abs` | +| `saturating_abs` | +| `wrapping_abs` | +| `unsigned_abs` | +| `checked_neg` | +| `overflowing_neg` | +| `wrapping_neg` | +| `from_mut` | +| `from_mut_unchecked` | + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0024-integer-function-correctness.md b/doc/src/challenges/0024-integer-function-correctness.md new file mode 100644 index 0000000000000..e69de29bb2d1d From 40b20f43899696392f3e9d281e2b451328afa80f Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 19 Feb 2025 14:34:50 -0800 Subject: [PATCH 03/18] editing --- .../challenges/0018-intrinsic-math-error.md | 41 +++++++++++++++ .../challenges/0023-nonzero-correctness.md | 2 +- .../0024-integer-arith-correctness.md | 43 +++++++++++++++ .../0024-integer-function-correctness.md | 0 .../0025-integer-bit-correctness.md | 52 +++++++++++++++++++ 5 files changed, 137 insertions(+), 1 deletion(-) create mode 100644 doc/src/challenges/0024-integer-arith-correctness.md delete mode 100644 doc/src/challenges/0024-integer-function-correctness.md create mode 100644 doc/src/challenges/0025-integer-bit-correctness.md diff --git a/doc/src/challenges/0018-intrinsic-math-error.md b/doc/src/challenges/0018-intrinsic-math-error.md index e69de29bb2d1d..426a3fe46ca76 100644 --- a/doc/src/challenges/0018-intrinsic-math-error.md +++ b/doc/src/challenges/0018-intrinsic-math-error.md @@ -0,0 +1,41 @@ +# Challenge 18: Correctness of instrinsic floating-point mathematic functions + +- **Status:** Open +- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) +- **Start date:** *2025/02/24* +- **End date:** *2025/08/24* +- **Reward:** *N/A* + +------------------- + +## Goal + +Floating-point computation is subjected to rounding errors. Knowing the accuracy of basic library functions is crucial when using them in precision-critical computations. + +Ideally, we expect the elementary functions `cosf16` to be correctly-rounded (the unrounded value of the real mathematic functions should be rounded to the returned value of the floating-point functions +under all rounding-modes). However, it is not always the case. + +In this challenge, for each function listed in the next section, you are required to either: +- If the function is correctly-rounded, prove that. +OR +- If not, provide an input to to confirm that, then provide a "tight" rigorous bound for the relative error of that function. +A bound is considered "tight" if you can provide an input such that the error is at least 90% the magnitude of the bound. + + +### Success Criteria + +Prove thet the following functions are correctly-rounded or provide "tight" error-bounds for them. + +| Functions | +|--------- | +| `cosf16` | +| `cosf32` | +| `cosf64` | +| `cosf128` | + + +And similar versions for `exp2`, `log2`, `log10`, `powf`, `sinf`, `sqrtf`, + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0023-nonzero-correctness.md b/doc/src/challenges/0023-nonzero-correctness.md index eb71661b46289..2a8a24474b247 100644 --- a/doc/src/challenges/0023-nonzero-correctness.md +++ b/doc/src/challenges/0023-nonzero-correctness.md @@ -24,7 +24,7 @@ the primitive integer types (under safety preconditions of Challenge 12). For example, for the `max` function, you need to prove that `∀ T in {isize, i8, i16, ... , usize, u8, ... }, ∀ x, y : NonZero, x.max(y).get() == x.get().max(y.get())` -Proving the correctness of the functions of primitive integer types is proposed in Challenge 24. +Proving the correctness of the functions of primitive integer types is proposed in Challenge 24 and 25. ### Success Criteria diff --git a/doc/src/challenges/0024-integer-arith-correctness.md b/doc/src/challenges/0024-integer-arith-correctness.md new file mode 100644 index 0000000000000..6ccce591ba50f --- /dev/null +++ b/doc/src/challenges/0024-integer-arith-correctness.md @@ -0,0 +1,43 @@ +# Challenge 24: Correctness of primitive integer types' arithmetic functions + +- **Status:** Open +- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) +- **Start date:** *2025/02/24* +- **End date:** *2025/08/24* +- **Reward:** *N/A* + +------------------- + +## Goal + +Verify the correctness of primitive integer types' arithmetic functions in `core::num::mod.rs`. + + +### Success Criteria + +Prove the correctness the following functions and methods in `core::num::mod.rs` for all primitive integer types +`{isize, i8, i16, i32, i64, i128 , usize, u8, u16, u32, u64, u128}` + +| Functions | +|--------- | +| `checked_add` | +| `saturating_add` | +| `unchecked_add` | +| `overflowing_add` | +| `wrapping_add` | + +And similar versions for `sub`, `mul`, `abs`, `neg`, `pow`, `rem`, `div` (if available). + +| More functions | +|--------- | +| `pow` | +| `rem_euclid` | +| `div_euclid` | +| `div_ceil` | +| `div_floor` | +| `ilog2` | +| `ilog10` | + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0024-integer-function-correctness.md b/doc/src/challenges/0024-integer-function-correctness.md deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/doc/src/challenges/0025-integer-bit-correctness.md b/doc/src/challenges/0025-integer-bit-correctness.md new file mode 100644 index 0000000000000..5a08e7b65ea09 --- /dev/null +++ b/doc/src/challenges/0025-integer-bit-correctness.md @@ -0,0 +1,52 @@ +# Challenge 24: Correctness of primitive integer types' bit functions + +- **Status:** Open +- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) +- **Start date:** *2025/02/24* +- **End date:** *2025/08/24* +- **Reward:** *N/A* + +------------------- + +## Goal + +Verify the correctness of primitive integer types' functions in `core::num::mod.rs`. + + +### Success Criteria + +Prove the correctness the following functions and methods in `core::num::mod.rs` for all primitive integer types +`{isize, i8, i16, i32, i64, i128 , usize, u8, u16, u32, u64, u128}` + +| Function | +|--------- | +| `checked_shl` | +| `saturating_shl` | +| `unchecked_shl` | +| `overflowing_shl` | +| `wrapping_shl` | +| `unbounded_shr` | +| `checked_shr` | +| `saturating_shr` | +| `unchecked_shr` | +| `overflowing_shr` | +| `wrapping_shr` | +| `unbounded_shr` | +| `swap_bytes`| +| `reverse_bits`| +| `rotate_left`| +| `rotate_right`| +| `to_be` | +| `to_le` | +| `to_be_bytes` | +| `to_le_bytes` | +| `trailing_zeros` | +| `trailing_ones` | +| `leading_zeros` | +| `leading_ones` | +| `count_zeros` | +| `count_ones` | + + +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 924d7521cfefab7e9f67df50c12b2e1eb142e376 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 20 Feb 2025 09:36:15 -0800 Subject: [PATCH 04/18] editing --- ...s.md => 0016-integer-arith-correctness.md} | 4 +- .../challenges/0016-iteration-correctness.md | 0 ...ess.md => 0017-integer-bit-correctness.md} | 3 +- doc/src/challenges/0017-str.md | 0 ...ectness.md => 0019-nonzero-correctness.md} | 4 +- doc/src/challenges/0019-silce.md | 0 doc/src/challenges/0020-math-function.md | 0 doc/src/challenges/0020-silce.md | 51 +++++++++++++++++++ doc/src/challenges/0021-hashmap.md | 0 doc/src/challenges/0021-iter.md | 51 +++++++++++++++++++ doc/src/challenges/0022-validation.md | 51 +++++++++++++++++++ doc/src/challenges/0022-vector.md | 0 doc/src/challenges/0023-pattern.md | 51 +++++++++++++++++++ doc/src/challenges/0024-str.md | 51 +++++++++++++++++++ doc/src/challenges/0025-string.md | 51 +++++++++++++++++++ 15 files changed, 313 insertions(+), 4 deletions(-) rename doc/src/challenges/{0024-integer-arith-correctness.md => 0016-integer-arith-correctness.md} (88%) delete mode 100644 doc/src/challenges/0016-iteration-correctness.md rename doc/src/challenges/{0025-integer-bit-correctness.md => 0017-integer-bit-correctness.md} (89%) delete mode 100644 doc/src/challenges/0017-str.md rename doc/src/challenges/{0023-nonzero-correctness.md => 0019-nonzero-correctness.md} (95%) delete mode 100644 doc/src/challenges/0019-silce.md delete mode 100644 doc/src/challenges/0020-math-function.md create mode 100644 doc/src/challenges/0020-silce.md delete mode 100644 doc/src/challenges/0021-hashmap.md create mode 100644 doc/src/challenges/0021-iter.md create mode 100644 doc/src/challenges/0022-validation.md delete mode 100644 doc/src/challenges/0022-vector.md create mode 100644 doc/src/challenges/0023-pattern.md create mode 100644 doc/src/challenges/0024-str.md create mode 100644 doc/src/challenges/0025-string.md diff --git a/doc/src/challenges/0024-integer-arith-correctness.md b/doc/src/challenges/0016-integer-arith-correctness.md similarity index 88% rename from doc/src/challenges/0024-integer-arith-correctness.md rename to doc/src/challenges/0016-integer-arith-correctness.md index 6ccce591ba50f..5ee8ccfe8519b 100644 --- a/doc/src/challenges/0024-integer-arith-correctness.md +++ b/doc/src/challenges/0016-integer-arith-correctness.md @@ -1,4 +1,4 @@ -# Challenge 24: Correctness of primitive integer types' arithmetic functions +# Challenge 16: Correctness of primitive integer types' arithmetic functions - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) @@ -12,6 +12,8 @@ Verify the correctness of primitive integer types' arithmetic functions in `core::num::mod.rs`. +For this challenge, you can assume that all the intrinsic functions are correct. + ### Success Criteria diff --git a/doc/src/challenges/0016-iteration-correctness.md b/doc/src/challenges/0016-iteration-correctness.md deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/doc/src/challenges/0025-integer-bit-correctness.md b/doc/src/challenges/0017-integer-bit-correctness.md similarity index 89% rename from doc/src/challenges/0025-integer-bit-correctness.md rename to doc/src/challenges/0017-integer-bit-correctness.md index 5a08e7b65ea09..a8ba4f02fec4d 100644 --- a/doc/src/challenges/0025-integer-bit-correctness.md +++ b/doc/src/challenges/0017-integer-bit-correctness.md @@ -1,4 +1,4 @@ -# Challenge 24: Correctness of primitive integer types' bit functions +# Challenge 17: Correctness of primitive integer types' bit functions - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) @@ -12,6 +12,7 @@ Verify the correctness of primitive integer types' functions in `core::num::mod.rs`. +For this challenge, you can assume that all the intrinsic functions are correct. ### Success Criteria diff --git a/doc/src/challenges/0017-str.md b/doc/src/challenges/0017-str.md deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/doc/src/challenges/0023-nonzero-correctness.md b/doc/src/challenges/0019-nonzero-correctness.md similarity index 95% rename from doc/src/challenges/0023-nonzero-correctness.md rename to doc/src/challenges/0019-nonzero-correctness.md index 2a8a24474b247..4453ac27a925f 100644 --- a/doc/src/challenges/0023-nonzero-correctness.md +++ b/doc/src/challenges/0019-nonzero-correctness.md @@ -1,4 +1,4 @@ -# Challenge 23: Correctness of `NonZero` functions +# Challenge 19: Correctness of `NonZero` functions - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) @@ -24,7 +24,7 @@ the primitive integer types (under safety preconditions of Challenge 12). For example, for the `max` function, you need to prove that `∀ T in {isize, i8, i16, ... , usize, u8, ... }, ∀ x, y : NonZero, x.max(y).get() == x.get().max(y.get())` -Proving the correctness of the functions of primitive integer types is proposed in Challenge 24 and 25. +Proving the correctness of the functions of primitive integer types is proposed in Challenge 16 and 17. ### Success Criteria diff --git a/doc/src/challenges/0019-silce.md b/doc/src/challenges/0019-silce.md deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/doc/src/challenges/0020-math-function.md b/doc/src/challenges/0020-math-function.md deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/doc/src/challenges/0020-silce.md b/doc/src/challenges/0020-silce.md new file mode 100644 index 0000000000000..3bfcb87cc73a3 --- /dev/null +++ b/doc/src/challenges/0020-silce.md @@ -0,0 +1,51 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clear| alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### 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-hashmap.md b/doc/src/challenges/0021-hashmap.md deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/doc/src/challenges/0021-iter.md b/doc/src/challenges/0021-iter.md new file mode 100644 index 0000000000000..3bfcb87cc73a3 --- /dev/null +++ b/doc/src/challenges/0021-iter.md @@ -0,0 +1,51 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clear| alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### 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-validation.md b/doc/src/challenges/0022-validation.md new file mode 100644 index 0000000000000..3bfcb87cc73a3 --- /dev/null +++ b/doc/src/challenges/0022-validation.md @@ -0,0 +1,51 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clear| alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### 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-vector.md b/doc/src/challenges/0022-vector.md deleted file mode 100644 index e69de29bb2d1d..0000000000000 diff --git a/doc/src/challenges/0023-pattern.md b/doc/src/challenges/0023-pattern.md new file mode 100644 index 0000000000000..3bfcb87cc73a3 --- /dev/null +++ b/doc/src/challenges/0023-pattern.md @@ -0,0 +1,51 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clear| alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0024-str.md b/doc/src/challenges/0024-str.md new file mode 100644 index 0000000000000..3bfcb87cc73a3 --- /dev/null +++ b/doc/src/challenges/0024-str.md @@ -0,0 +1,51 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clear| alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0025-string.md b/doc/src/challenges/0025-string.md new file mode 100644 index 0000000000000..3bfcb87cc73a3 --- /dev/null +++ b/doc/src/challenges/0025-string.md @@ -0,0 +1,51 @@ +# Challenge 5: Verify functions iterating over inductive data type: `linked_list` + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. + +### Details + +The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | Location | +|---------|---------| +|clear| alloc::collections::linked_list | +|contains| alloc::collections::linked_list | +|split_off| alloc::collections::linked_list | +|remove| alloc::collections::linked_list | +|retain| alloc::collections::linked_list | +|retain_mut| alloc::collections::linked_list | +|extract_if| alloc::collections::linked_list | + + +The verification must be unbounded---it must hold for linked lists of arbitrary shape. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### 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 fabd40f15e8435ecc80bad678089aff02695607d Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 20 Feb 2025 13:03:55 -0800 Subject: [PATCH 05/18] editing --- doc/src/challenges/0018-intrinsic-math-error.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0018-intrinsic-math-error.md b/doc/src/challenges/0018-intrinsic-math-error.md index 426a3fe46ca76..8ad59cb1dcd93 100644 --- a/doc/src/challenges/0018-intrinsic-math-error.md +++ b/doc/src/challenges/0018-intrinsic-math-error.md @@ -16,9 +16,9 @@ Ideally, we expect the elementary functions `cosf16` to be correctly-rounded (th under all rounding-modes). However, it is not always the case. In this challenge, for each function listed in the next section, you are required to either: -- If the function is correctly-rounded, prove that. +- Prove that the function is correctly-rounded. OR -- If not, provide an input to to confirm that, then provide a "tight" rigorous bound for the relative error of that function. +- Provide an input to show that the function is not correctly-rounded, then provide a "tight" rigorous bound for the relative error of that function. A bound is considered "tight" if you can provide an input such that the error is at least 90% the magnitude of the bound. From 4a3a0e6b4e2b641f6ad627da79253f6bac4497d3 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 28 Feb 2025 08:07:24 -0800 Subject: [PATCH 06/18] add 10 challenges --- .../0016-integer-arith-correctness.md | 14 +++- .../0017-integer-bit-correctness.md | 15 +++- .../challenges/0018-intrinsic-math-error.md | 41 ---------- ...ectness.md => 0018-nonzero-correctness.md} | 16 +++- doc/src/challenges/0019-silce.md | 79 ++++++++++++++++++ doc/src/challenges/0020-silce.md | 51 ------------ doc/src/challenges/0020-slice-iter.md | 64 +++++++++++++++ doc/src/challenges/0021-iter.md | 51 ------------ doc/src/challenges/0021-str-encode.md | 58 +++++++++++++ doc/src/challenges/0022-char-pattern.md | 45 ++++++++++ doc/src/challenges/0022-validation.md | 51 ------------ doc/src/challenges/0023-pattern.md | 51 ------------ doc/src/challenges/0023-two-way-search.md | 31 +++++++ doc/src/challenges/0024-str.md | 51 ------------ doc/src/challenges/0024-substr-pattern.md | 45 ++++++++++ doc/src/challenges/0025-str-iter.md | 82 +++++++++++++++++++ doc/src/challenges/0025-string.md | 51 ------------ 17 files changed, 443 insertions(+), 353 deletions(-) delete mode 100644 doc/src/challenges/0018-intrinsic-math-error.md rename doc/src/challenges/{0019-nonzero-correctness.md => 0018-nonzero-correctness.md} (79%) create mode 100644 doc/src/challenges/0019-silce.md delete mode 100644 doc/src/challenges/0020-silce.md create mode 100644 doc/src/challenges/0020-slice-iter.md delete mode 100644 doc/src/challenges/0021-iter.md create mode 100644 doc/src/challenges/0021-str-encode.md create mode 100644 doc/src/challenges/0022-char-pattern.md delete mode 100644 doc/src/challenges/0022-validation.md delete mode 100644 doc/src/challenges/0023-pattern.md create mode 100644 doc/src/challenges/0023-two-way-search.md delete mode 100644 doc/src/challenges/0024-str.md create mode 100644 doc/src/challenges/0024-substr-pattern.md create mode 100644 doc/src/challenges/0025-str-iter.md delete mode 100644 doc/src/challenges/0025-string.md diff --git a/doc/src/challenges/0016-integer-arith-correctness.md b/doc/src/challenges/0016-integer-arith-correctness.md index 5ee8ccfe8519b..737448e1988be 100644 --- a/doc/src/challenges/0016-integer-arith-correctness.md +++ b/doc/src/challenges/0016-integer-arith-correctness.md @@ -2,8 +2,8 @@ - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/02/24* -- **End date:** *2025/08/24* +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* - **Reward:** *N/A* ------------------- @@ -40,6 +40,16 @@ And similar versions for `sub`, `mul`, `abs`, `neg`, `pow`, `rem`, `div` (if ava | `ilog2` | | `ilog10` | +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) in addition to the ones listed above. diff --git a/doc/src/challenges/0017-integer-bit-correctness.md b/doc/src/challenges/0017-integer-bit-correctness.md index a8ba4f02fec4d..d981dac4ffec5 100644 --- a/doc/src/challenges/0017-integer-bit-correctness.md +++ b/doc/src/challenges/0017-integer-bit-correctness.md @@ -2,8 +2,8 @@ - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/02/24* -- **End date:** *2025/08/24* +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* - **Reward:** *N/A* ------------------- @@ -49,5 +49,16 @@ Prove the correctness the following functions and methods in `core::num::mod.rs` | `count_ones` | +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) in addition to the ones listed above. diff --git a/doc/src/challenges/0018-intrinsic-math-error.md b/doc/src/challenges/0018-intrinsic-math-error.md deleted file mode 100644 index 8ad59cb1dcd93..0000000000000 --- a/doc/src/challenges/0018-intrinsic-math-error.md +++ /dev/null @@ -1,41 +0,0 @@ -# Challenge 18: Correctness of instrinsic floating-point mathematic functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/02/24* -- **End date:** *2025/08/24* -- **Reward:** *N/A* - -------------------- - -## Goal - -Floating-point computation is subjected to rounding errors. Knowing the accuracy of basic library functions is crucial when using them in precision-critical computations. - -Ideally, we expect the elementary functions `cosf16` to be correctly-rounded (the unrounded value of the real mathematic functions should be rounded to the returned value of the floating-point functions -under all rounding-modes). However, it is not always the case. - -In this challenge, for each function listed in the next section, you are required to either: -- Prove that the function is correctly-rounded. -OR -- Provide an input to show that the function is not correctly-rounded, then provide a "tight" rigorous bound for the relative error of that function. -A bound is considered "tight" if you can provide an input such that the error is at least 90% the magnitude of the bound. - - -### Success Criteria - -Prove thet the following functions are correctly-rounded or provide "tight" error-bounds for them. - -| Functions | -|--------- | -| `cosf16` | -| `cosf32` | -| `cosf64` | -| `cosf128` | - - -And similar versions for `exp2`, `log2`, `log10`, `powf`, `sinf`, `sqrtf`, - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0019-nonzero-correctness.md b/doc/src/challenges/0018-nonzero-correctness.md similarity index 79% rename from doc/src/challenges/0019-nonzero-correctness.md rename to doc/src/challenges/0018-nonzero-correctness.md index 4453ac27a925f..63a0f0ace05a6 100644 --- a/doc/src/challenges/0019-nonzero-correctness.md +++ b/doc/src/challenges/0018-nonzero-correctness.md @@ -2,8 +2,8 @@ - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/02/24* -- **End date:** *2025/08/24* +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* - **Reward:** *N/A* ------------------- @@ -70,5 +70,17 @@ Verify that the following functions and methods (all located within `core::num:: | `from_mut_unchecked` | +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) in addition to the ones listed above. + diff --git a/doc/src/challenges/0019-silce.md b/doc/src/challenges/0019-silce.md new file mode 100644 index 0000000000000..7820ba3220c1b --- /dev/null +++ b/doc/src/challenges/0019-silce.md @@ -0,0 +1,79 @@ +# Challenge 20: Verify the memory safety of `slice` functions + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *?* + +------------------- + + +## Goal + +Verify the memory safety of [`std::slice` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/mod.rs). + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | +|---------| +|first_chunk| +|first_chunk_mut| +|split_first_chunk| +|split_first_chunk_mut| +|split_last_chunk| +|split_last_chunk_mut| +|last_chunk| +|last_chunk_mut| +|get_unchecked| +|get_unchecked_mut| +|as_ptr_range| +|as_mut_ptr_range| +|as_array| +|as_mut_array| +|swap| +|swap_unchecked| +|reverse| +|as_chunks_unchecked| +|as_chunks| +|as_rchunks| +|as_chunks_unchecked_mut| +|split_at_unchecked| +|split_at_mut_unchecked| +|split_at_checked| +|split_at_mut_checked| +|binary_search_by| +|partition_dedup_by| +|rotate_left| +|rotate_right| +|copy_from_slice| +|copy_within| +|swap_with_slice| +|align_to| +|align_to_mut| +|as_simd| +|as_simd_mut| +|get_many_unchecked_mut| +|get_many_mut| +|as_flattened| +|as_flattened_mut| + +The verification must be unbounded---it must hold for slices of arbitrary length. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0020-silce.md b/doc/src/challenges/0020-silce.md deleted file mode 100644 index 3bfcb87cc73a3..0000000000000 --- a/doc/src/challenges/0020-silce.md +++ /dev/null @@ -1,51 +0,0 @@ -# Challenge 5: Verify functions iterating over inductive data type: `linked_list` - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2024/07/01* -- **End date:** *2025/04/10* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. - -### Details - -The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | Location | -|---------|---------| -|clear| alloc::collections::linked_list | -|contains| alloc::collections::linked_list | -|split_off| alloc::collections::linked_list | -|remove| alloc::collections::linked_list | -|retain| alloc::collections::linked_list | -|retain_mut| alloc::collections::linked_list | -|extract_if| alloc::collections::linked_list | - - -The verification must be unbounded---it must hold for linked lists of arbitrary shape. - -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0020-slice-iter.md b/doc/src/challenges/0020-slice-iter.md new file mode 100644 index 0000000000000..069a8e643218e --- /dev/null +++ b/doc/src/challenges/0020-slice-iter.md @@ -0,0 +1,64 @@ +# Challenge 21: Verify the memory safety and functional correctness of `slice` iter functions + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *?* + +------------------- + + +## Goal + +Verify the memory safety of functional correctness of [`std::slice` iter functions] (https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/iter/macros.rs). + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | +|---------| +|next_back_unchecked| +|make_slice| +|pre_dec_end| +|post_inc_start| +|len| +|is_empty| +|next| +|size_hint| +|count| +|nth| +|advance_by| +|last| +|fold| +|for_each| +|all| +|any| +|find| +|find_map| +|position| +|rposition| +|next_back| +|nth_back| +|advance_back_by| +|next_unchecked| + + +The verification must be unbounded---it must hold for slices of arbitrary length. + +It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. + +### 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-iter.md b/doc/src/challenges/0021-iter.md deleted file mode 100644 index 3bfcb87cc73a3..0000000000000 --- a/doc/src/challenges/0021-iter.md +++ /dev/null @@ -1,51 +0,0 @@ -# Challenge 5: Verify functions iterating over inductive data type: `linked_list` - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2024/07/01* -- **End date:** *2025/04/10* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. - -### Details - -The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | Location | -|---------|---------| -|clear| alloc::collections::linked_list | -|contains| alloc::collections::linked_list | -|split_off| alloc::collections::linked_list | -|remove| alloc::collections::linked_list | -|retain| alloc::collections::linked_list | -|retain_mut| alloc::collections::linked_list | -|extract_if| alloc::collections::linked_list | - - -The verification must be unbounded---it must hold for linked lists of arbitrary shape. - -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0021-str-encode.md b/doc/src/challenges/0021-str-encode.md new file mode 100644 index 0000000000000..6c36ae3183cd3 --- /dev/null +++ b/doc/src/challenges/0021-str-encode.md @@ -0,0 +1,58 @@ +# Challenge 5: Verify the correctness of UTF8 and UTF16 encoding functions +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *5,000 USD* + +------------------- + + +## Goal + +Verify the the correctness of functions related to UTF8 and UTF16 encoding + +### Details + +Rust str and String are either UTF8 and UTF16 encoded. Verifying the correctess of the related functions is important in ensuring the safety and correctness of Rust programs that involve Strings. + + +### Success Criteria + +Verify the the correctness of the following functions is functionally correct according to the UTF8 anf UTF16 descriptions in: +https://en.wikipedia.org/wiki/UTF-8 and https://en.wikipedia.org/wiki/UTF-16 + +| Function | Location | +|---------|---------| +|run_utf8_validation| core::src::str::validation | +|next_code_point| core::src::str::validation | +|next_code_point_reverse| core::src::str::validation | +|decode_utf16| core::src::char::decode | +|from_utf8| core::str::converts | +|from_utf8_unchecked| core::str::converts | +|from_utf8_mut| core::str::converts | +|from_utf8_unchecked_mut| core::str::converts | +|chars| core::str::mod | +|char_indices| core::str::mod | +|encode_utf16| core::str::mod| +|from_utf16| alloc::src::string | +|from_utf16_lossy| alloc::src::string | + + + +The verification must be unbounded---it must hold for inputs of arbitrary size. + + + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0022-char-pattern.md b/doc/src/challenges/0022-char-pattern.md new file mode 100644 index 0000000000000..60c65ba073e40 --- /dev/null +++ b/doc/src/challenges/0022-char-pattern.md @@ -0,0 +1,45 @@ +# Challenge 23: Verify the correctness of char-related functions in str::pattern + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *5,000 USD* + +------------------- + + +### Details + +Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. +Those functions is implemented in core::src::str, but the core of them is implemented in core::src::str::pattern. +The main purposes of the functions in core::src::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), +then implementing the searching alorithm for those Searchers. + +IMPORTANT NOTE: You can assume the correctness of functions in Challenge 21. + +### Success Criteria + +Verify the memory safety and functional correctness of the following functions in +https://github.com/rust-lang/rust/blob/96cfc75584359ae7ad11cc45968059f29e7b44b7/library/core/src/str/pattern.rs + +1. `next`, `next_match`, `next_back`, `next_match_back`, +which are implemented for `CharSearcher`, `MultiCharEqSearcher`, `CharArraySearcher` , `CharArrayRefSearcher`, `CharSliceSearcher`, `CharPredicateSearcher` +2. `is_contained_in`, `is_prefix_of`, `strip_prefix_of` +which are implemented for `char`, `[char; N]`, `&[char; N]`, `&[char]`, `FnMut(char) -> bool` + +The verification must be unbounded---it must hold for inputs of arbitrary size. + + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0022-validation.md b/doc/src/challenges/0022-validation.md deleted file mode 100644 index 3bfcb87cc73a3..0000000000000 --- a/doc/src/challenges/0022-validation.md +++ /dev/null @@ -1,51 +0,0 @@ -# Challenge 5: Verify functions iterating over inductive data type: `linked_list` - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2024/07/01* -- **End date:** *2025/04/10* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. - -### Details - -The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | Location | -|---------|---------| -|clear| alloc::collections::linked_list | -|contains| alloc::collections::linked_list | -|split_off| alloc::collections::linked_list | -|remove| alloc::collections::linked_list | -|retain| alloc::collections::linked_list | -|retain_mut| alloc::collections::linked_list | -|extract_if| alloc::collections::linked_list | - - -The verification must be unbounded---it must hold for linked lists of arbitrary shape. - -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0023-pattern.md b/doc/src/challenges/0023-pattern.md deleted file mode 100644 index 3bfcb87cc73a3..0000000000000 --- a/doc/src/challenges/0023-pattern.md +++ /dev/null @@ -1,51 +0,0 @@ -# Challenge 5: Verify functions iterating over inductive data type: `linked_list` - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2024/07/01* -- **End date:** *2025/04/10* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. - -### Details - -The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | Location | -|---------|---------| -|clear| alloc::collections::linked_list | -|contains| alloc::collections::linked_list | -|split_off| alloc::collections::linked_list | -|remove| alloc::collections::linked_list | -|retain| alloc::collections::linked_list | -|retain_mut| alloc::collections::linked_list | -|extract_if| alloc::collections::linked_list | - - -The verification must be unbounded---it must hold for linked lists of arbitrary shape. - -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0023-two-way-search.md b/doc/src/challenges/0023-two-way-search.md new file mode 100644 index 0000000000000..88d58dd4e860d --- /dev/null +++ b/doc/src/challenges/0023-two-way-search.md @@ -0,0 +1,31 @@ +# Challenge 23: Verify the correctness of the Two-Way search algorithm implementation in str::pattern + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *5,000 USD* + +------------------- + +### Details + +This algorithm is the main component of implementing searching functions for Patterns as substrings. + +### Success Criteria + +Verify the memory safety and functional correctness of the Two-Way search algorithm implementation in str::pattern. + + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0024-str.md b/doc/src/challenges/0024-str.md deleted file mode 100644 index 3bfcb87cc73a3..0000000000000 --- a/doc/src/challenges/0024-str.md +++ /dev/null @@ -1,51 +0,0 @@ -# Challenge 5: Verify functions iterating over inductive data type: `linked_list` - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2024/07/01* -- **End date:** *2025/04/10* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. - -### Details - -The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | Location | -|---------|---------| -|clear| alloc::collections::linked_list | -|contains| alloc::collections::linked_list | -|split_off| alloc::collections::linked_list | -|remove| alloc::collections::linked_list | -|retain| alloc::collections::linked_list | -|retain_mut| alloc::collections::linked_list | -|extract_if| alloc::collections::linked_list | - - -The verification must be unbounded---it must hold for linked lists of arbitrary shape. - -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0024-substr-pattern.md b/doc/src/challenges/0024-substr-pattern.md new file mode 100644 index 0000000000000..795d2dd6e8164 --- /dev/null +++ b/doc/src/challenges/0024-substr-pattern.md @@ -0,0 +1,45 @@ +# Challenge 23: Verify the correctness of substring-related functions in str::pattern + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *5,000 USD* + +------------------- + + +### Details + +Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. +Those functions is implemented in core::src::str, but the core of them is implemented in core::src::str::pattern. +The main purposes of the functions in core::src::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), +then implementing the searching alorithm for those Searchers. + +IMPORTANT NOTE: You can assume the correctness of the Two-Way search algorithm (see Challenge 23), BUT have to verify the correctness of the simd_contains functions. + +### Success Criteria + +Verify the memory safety and functional correctness of the following functions in +https://github.com/rust-lang/rust/blob/96cfc75584359ae7ad11cc45968059f29e7b44b7/library/core/src/str/pattern.rs + +`next`, `next_match`, `next_back`, `next_match_back` +which are implemented for `StrSearcher` and `is_contained_in`, `is_prefix_of`, `strip_prefix_of`, `is_suffix_of`, `strip_suffix_of` for `&str`. + +The verification must be unbounded---it must hold for inputs of arbitrary size. + + + + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0025-str-iter.md b/doc/src/challenges/0025-str-iter.md new file mode 100644 index 0000000000000..836503a681c7a --- /dev/null +++ b/doc/src/challenges/0025-str-iter.md @@ -0,0 +1,82 @@ +# Challenge 25: Correctness of str functions + +- **Status:** Open +- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *N/A* + +------------------- + +## Goal + +Verify the correctness of functions in `core::src::str::mod.rs`. + +IMPORTANT NOTE: You can assume the correctness of all the functions that are verified in Challenges 21 to 24, BUT you may have to verify the correctness of other dependent functions in core::str::iter + +### Success Criteria + +Prove the correctness the following functions and methods in `core::str::mod.rs` : +| Function | +|--------- | +| `is_char_boundary`| +| `floor_char_boundary`| +| `ceil_char_boundary`| +| `split_at` | +| `split_at_mut` | +| `split_at_checked` | +| `split_at_mut_checked` | +| `split_at_unchecked` | +| `split_at_mut_unchecked` | +| `split_whitespace` | +| `split_ascii_whitespace` | +| `lines` | +| `lines_any` | +| `starts_with` | +| `ends_with` | +| `find`| +| `rfind`| +| `rotate_left`| +| `rotate_right`| +| `split` | +| `split_inclusive` | +| `rsplit` | +| `split_terminator` | +| `rsplit_terminator` | +| `splitn` | +| `rsplitn` | +| `split_once` | +| `rsplit_once` | +| `matches` | +| `rmatches` | +| `match_indices` | +| `rmatch_indices` | +| `trim` | +| `trim_start` | +| `trim_end` | +| `trim_left` | +| `trim_right` | +| `trim_right` | +| `trim_start_matches` | +| `strip_prefix` | +| `strip_suffix` | +| `trim_end_matches` | +| `trim_left_matches` | +| `trim_right_matches` | + +The verification must be unbounded---it must hold for str of arbitrary size. + + +### List of UBs + +In addition to any properties called out as `SAFETY` comments in the source +code, +all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory. +* Mutating immutable bytes. +* Producing an invalid value + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0025-string.md b/doc/src/challenges/0025-string.md deleted file mode 100644 index 3bfcb87cc73a3..0000000000000 --- a/doc/src/challenges/0025-string.md +++ /dev/null @@ -1,51 +0,0 @@ -# Challenge 5: Verify functions iterating over inductive data type: `linked_list` - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2024/07/01* -- **End date:** *2025/04/10* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type. - -### Details - -The internal representations of `linked_list` are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions. - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | Location | -|---------|---------| -|clear| alloc::collections::linked_list | -|contains| alloc::collections::linked_list | -|split_off| alloc::collections::linked_list | -|remove| alloc::collections::linked_list | -|retain| alloc::collections::linked_list | -|retain_mut| alloc::collections::linked_list | -|extract_if| alloc::collections::linked_list | - - -The verification must be unbounded---it must hold for linked lists of arbitrary shape. - -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. - -### 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 67b6403db1175f6d4c572495112f7fa4ac01f776 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 28 Feb 2025 08:13:27 -0800 Subject: [PATCH 07/18] fix typos --- doc/src/challenges/0021-str-encode.md | 2 +- doc/src/challenges/0022-char-pattern.md | 2 +- doc/src/challenges/0023-two-way-search.md | 2 +- doc/src/challenges/0024-substr-pattern.md | 4 ++-- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/src/challenges/0021-str-encode.md b/doc/src/challenges/0021-str-encode.md index 6c36ae3183cd3..004a1958dc315 100644 --- a/doc/src/challenges/0021-str-encode.md +++ b/doc/src/challenges/0021-str-encode.md @@ -14,7 +14,7 @@ Verify the the correctness of functions related to UTF8 and UTF16 encoding ### Details -Rust str and String are either UTF8 and UTF16 encoded. Verifying the correctess of the related functions is important in ensuring the safety and correctness of Rust programs that involve Strings. +Rust str and String are either UTF8 or UTF16 encoded. Verifying the correctess of the related functions is important in ensuring the safety and correctness of Rust programs that involve Strings. ### Success Criteria diff --git a/doc/src/challenges/0022-char-pattern.md b/doc/src/challenges/0022-char-pattern.md index 60c65ba073e40..e004796ca5880 100644 --- a/doc/src/challenges/0022-char-pattern.md +++ b/doc/src/challenges/0022-char-pattern.md @@ -12,7 +12,7 @@ ### Details Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. -Those functions is implemented in core::src::str, but the core of them is implemented in core::src::str::pattern. +Those functions is implemented in core::str, but the core of them is implemented in core::str::pattern. The main purposes of the functions in core::src::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), then implementing the searching alorithm for those Searchers. diff --git a/doc/src/challenges/0023-two-way-search.md b/doc/src/challenges/0023-two-way-search.md index 88d58dd4e860d..b7cec2881d6a1 100644 --- a/doc/src/challenges/0023-two-way-search.md +++ b/doc/src/challenges/0023-two-way-search.md @@ -14,7 +14,7 @@ This algorithm is the main component of implementing searching functions for Pat ### Success Criteria -Verify the memory safety and functional correctness of the Two-Way search algorithm implementation in str::pattern. +Verify the memory safety and functional correctness of the Two-Way search algorithm implementation in core::str::pattern. ### List of UBs diff --git a/doc/src/challenges/0024-substr-pattern.md b/doc/src/challenges/0024-substr-pattern.md index 795d2dd6e8164..7bf29efd51c04 100644 --- a/doc/src/challenges/0024-substr-pattern.md +++ b/doc/src/challenges/0024-substr-pattern.md @@ -12,8 +12,8 @@ ### Details Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. -Those functions is implemented in core::src::str, but the core of them is implemented in core::src::str::pattern. -The main purposes of the functions in core::src::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), +Those functions is implemented in core::str, but the core of them is implemented in core::src::str::pattern. +The main purposes of the functions in core::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), then implementing the searching alorithm for those Searchers. IMPORTANT NOTE: You can assume the correctness of the Two-Way search algorithm (see Challenge 23), BUT have to verify the correctness of the simd_contains functions. From 140f95ed1936fafdbd4b488902059a1365ea971e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 13:44:59 -0800 Subject: [PATCH 08/18] fix typo --- doc/src/challenges/0019-silce.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0019-silce.md b/doc/src/challenges/0019-silce.md index 7820ba3220c1b..02247ef04a68e 100644 --- a/doc/src/challenges/0019-silce.md +++ b/doc/src/challenges/0019-silce.md @@ -63,7 +63,7 @@ The memory safety of the following public functions that iterating over the inte The verification must be unbounded---it must hold for slices of arbitrary length. -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. +The verification must be hold for generic type `T` (no monomorphization). ### List of UBs From b4b7cadca888515a5584a585186b7e83fdbf0668 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 4 Mar 2025 13:45:17 -0800 Subject: [PATCH 09/18] fix type T --- doc/src/challenges/0020-slice-iter.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0020-slice-iter.md b/doc/src/challenges/0020-slice-iter.md index 069a8e643218e..228f6fc029492 100644 --- a/doc/src/challenges/0020-slice-iter.md +++ b/doc/src/challenges/0020-slice-iter.md @@ -1,4 +1,4 @@ -# Challenge 21: Verify the memory safety and functional correctness of `slice` iter functions +# Challenge 21: Verify the memory safety of `slice` iter functions - **Status:** Open - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) @@ -48,7 +48,7 @@ The memory safety of the following public functions that iterating over the inte The verification must be unbounded---it must hold for slices of arbitrary length. -It is OK to assume that the generic type `T` of the proofs is primitive types, e.g., `i32`, `u32`, `bool`, etc. +The verification must be hold for generic type `T` (no monomorphization). ### List of UBs From b9d0e74e2d0e9315fabf72058786137edf873e77 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 5 Mar 2025 15:06:31 -0800 Subject: [PATCH 10/18] fixed challenge 16 --- .../0016-integer-arith-correctness.md | 55 ------------- doc/src/challenges/0016-slice.md | 79 +++++++++++++++++++ 2 files changed, 79 insertions(+), 55 deletions(-) delete mode 100644 doc/src/challenges/0016-integer-arith-correctness.md create mode 100644 doc/src/challenges/0016-slice.md diff --git a/doc/src/challenges/0016-integer-arith-correctness.md b/doc/src/challenges/0016-integer-arith-correctness.md deleted file mode 100644 index 737448e1988be..0000000000000 --- a/doc/src/challenges/0016-integer-arith-correctness.md +++ /dev/null @@ -1,55 +0,0 @@ -# Challenge 16: Correctness of primitive integer types' arithmetic functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *N/A* - -------------------- - -## Goal - -Verify the correctness of primitive integer types' arithmetic functions in `core::num::mod.rs`. - -For this challenge, you can assume that all the intrinsic functions are correct. - - -### Success Criteria - -Prove the correctness the following functions and methods in `core::num::mod.rs` for all primitive integer types -`{isize, i8, i16, i32, i64, i128 , usize, u8, u16, u32, u64, u128}` - -| Functions | -|--------- | -| `checked_add` | -| `saturating_add` | -| `unchecked_add` | -| `overflowing_add` | -| `wrapping_add` | - -And similar versions for `sub`, `mul`, `abs`, `neg`, `pow`, `rem`, `div` (if available). - -| More functions | -|--------- | -| `pow` | -| `rem_euclid` | -| `div_euclid` | -| `div_ceil` | -| `div_floor` | -| `ilog2` | -| `ilog10` | - -### List of UBs - -In addition to any properties called out as `SAFETY` comments in the source -code, -all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory. -* Mutating immutable bytes. -* Producing an invalid value - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0016-slice.md b/doc/src/challenges/0016-slice.md new file mode 100644 index 0000000000000..02247ef04a68e --- /dev/null +++ b/doc/src/challenges/0016-slice.md @@ -0,0 +1,79 @@ +# Challenge 20: Verify the memory safety of `slice` functions + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *?* + +------------------- + + +## Goal + +Verify the memory safety of [`std::slice` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/mod.rs). + + +### Success Criteria + +The memory safety of the following public functions that iterating over the internal inductive data type must be verified: + +| Function | +|---------| +|first_chunk| +|first_chunk_mut| +|split_first_chunk| +|split_first_chunk_mut| +|split_last_chunk| +|split_last_chunk_mut| +|last_chunk| +|last_chunk_mut| +|get_unchecked| +|get_unchecked_mut| +|as_ptr_range| +|as_mut_ptr_range| +|as_array| +|as_mut_array| +|swap| +|swap_unchecked| +|reverse| +|as_chunks_unchecked| +|as_chunks| +|as_rchunks| +|as_chunks_unchecked_mut| +|split_at_unchecked| +|split_at_mut_unchecked| +|split_at_checked| +|split_at_mut_checked| +|binary_search_by| +|partition_dedup_by| +|rotate_left| +|rotate_right| +|copy_from_slice| +|copy_within| +|swap_with_slice| +|align_to| +|align_to_mut| +|as_simd| +|as_simd_mut| +|get_many_unchecked_mut| +|get_many_mut| +|as_flattened| +|as_flattened_mut| + +The verification must be unbounded---it must hold for slices of arbitrary length. + +The verification must be hold for generic type `T` (no monomorphization). + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. From 93207e4a7f728b5feddfe379bfcfe53380f01509 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 6 Mar 2025 09:36:21 -0800 Subject: [PATCH 11/18] keep only iter challenge --- doc/src/challenges/0016-iter.md | 68 +++++++++++++++ doc/src/challenges/0016-slice.md | 79 ----------------- .../0017-integer-bit-correctness.md | 64 -------------- .../challenges/0018-nonzero-correctness.md | 86 ------------------- doc/src/challenges/0019-silce.md | 79 ----------------- doc/src/challenges/0020-slice-iter.md | 64 -------------- doc/src/challenges/0021-str-encode.md | 58 ------------- doc/src/challenges/0022-char-pattern.md | 45 ---------- doc/src/challenges/0023-two-way-search.md | 31 ------- doc/src/challenges/0024-substr-pattern.md | 45 ---------- doc/src/challenges/0025-str-iter.md | 82 ------------------ 11 files changed, 68 insertions(+), 633 deletions(-) create mode 100644 doc/src/challenges/0016-iter.md delete mode 100644 doc/src/challenges/0016-slice.md delete mode 100644 doc/src/challenges/0017-integer-bit-correctness.md delete mode 100644 doc/src/challenges/0018-nonzero-correctness.md delete mode 100644 doc/src/challenges/0019-silce.md delete mode 100644 doc/src/challenges/0020-slice-iter.md delete mode 100644 doc/src/challenges/0021-str-encode.md delete mode 100644 doc/src/challenges/0022-char-pattern.md delete mode 100644 doc/src/challenges/0023-two-way-search.md delete mode 100644 doc/src/challenges/0024-substr-pattern.md delete mode 100644 doc/src/challenges/0025-str-iter.md diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md new file mode 100644 index 0000000000000..21fb41dcb7129 --- /dev/null +++ b/doc/src/challenges/0016-iter.md @@ -0,0 +1,68 @@ +# Challenge 21: Verify the safety of `slice` iter functions - part 2 + +- **Status:** Open +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Start date:** *2025/03/07* +- **End date:** *2025/10/17* +- **Reward:** *?* + +------------------- + + +## Goal + +Verify the safety of iter functions that are defined in (library/core/src/iter/adapters): + + + +### Success Criteria + +Write and prove the contract for the safety of the following functions: + +| Function | Defined in | +|---------| ---------| +|next_back_remainder| array_chunks.rs| +|fold| array_chunks.rs| +|__iterator_get_unchecked| clone.rs| +|fold| clone.rs| +|next_unchecked| clone.rs| +|__iterator_get_unchecked| copied.rs| +|spec_next_chunk| copied.rs| +|__iterator_get_unchecked| enumerate.rs| +|next_chunk| filter.rs| +|next_chunk| filter_map.rs| +|__iterator_get_unchecked | fuse.rs| +|__iterator_get_unchecked | map.rs| +|next_unchecked | map.rs| +|as_array_ref | map_windows.rs| +|as_uninit_array_mut | map_windows.rs| +|push | map_windows.rs| +|drop | map_windows.rs| +|__iterator_get_unchecked | skip.rs| +|original_step | step_by.rs| +|spec_fold| take.rs| +|spec_for_each| take.rs| +|__iterator_get_unchecked | zip.rs| +|get_unchecked| zip.rs| +|fold| zip.rs| +|next| zip.rs| +|nth| zip.rs| +|next_back| zip.rs| +|spec_fold| zip.rs| + +The verification must be unbounded---it must hold for slices of arbitrary length. + +The verification must be hold for generic type `T` (no monomorphization). + +### List of UBs + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +* Reading from uninitialized memory except for padding or unions. +* Mutating immutable bytes. +* Producing an invalid value + + +Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) +in addition to the ones listed above. diff --git a/doc/src/challenges/0016-slice.md b/doc/src/challenges/0016-slice.md deleted file mode 100644 index 02247ef04a68e..0000000000000 --- a/doc/src/challenges/0016-slice.md +++ /dev/null @@ -1,79 +0,0 @@ -# Challenge 20: Verify the memory safety of `slice` functions - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *?* - -------------------- - - -## Goal - -Verify the memory safety of [`std::slice` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/mod.rs). - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | -|---------| -|first_chunk| -|first_chunk_mut| -|split_first_chunk| -|split_first_chunk_mut| -|split_last_chunk| -|split_last_chunk_mut| -|last_chunk| -|last_chunk_mut| -|get_unchecked| -|get_unchecked_mut| -|as_ptr_range| -|as_mut_ptr_range| -|as_array| -|as_mut_array| -|swap| -|swap_unchecked| -|reverse| -|as_chunks_unchecked| -|as_chunks| -|as_rchunks| -|as_chunks_unchecked_mut| -|split_at_unchecked| -|split_at_mut_unchecked| -|split_at_checked| -|split_at_mut_checked| -|binary_search_by| -|partition_dedup_by| -|rotate_left| -|rotate_right| -|copy_from_slice| -|copy_within| -|swap_with_slice| -|align_to| -|align_to_mut| -|as_simd| -|as_simd_mut| -|get_many_unchecked_mut| -|get_many_mut| -|as_flattened| -|as_flattened_mut| - -The verification must be unbounded---it must hold for slices of arbitrary length. - -The verification must be hold for generic type `T` (no monomorphization). - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0017-integer-bit-correctness.md b/doc/src/challenges/0017-integer-bit-correctness.md deleted file mode 100644 index d981dac4ffec5..0000000000000 --- a/doc/src/challenges/0017-integer-bit-correctness.md +++ /dev/null @@ -1,64 +0,0 @@ -# Challenge 17: Correctness of primitive integer types' bit functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *N/A* - -------------------- - -## Goal - -Verify the correctness of primitive integer types' functions in `core::num::mod.rs`. - -For this challenge, you can assume that all the intrinsic functions are correct. - -### Success Criteria - -Prove the correctness the following functions and methods in `core::num::mod.rs` for all primitive integer types -`{isize, i8, i16, i32, i64, i128 , usize, u8, u16, u32, u64, u128}` - -| Function | -|--------- | -| `checked_shl` | -| `saturating_shl` | -| `unchecked_shl` | -| `overflowing_shl` | -| `wrapping_shl` | -| `unbounded_shr` | -| `checked_shr` | -| `saturating_shr` | -| `unchecked_shr` | -| `overflowing_shr` | -| `wrapping_shr` | -| `unbounded_shr` | -| `swap_bytes`| -| `reverse_bits`| -| `rotate_left`| -| `rotate_right`| -| `to_be` | -| `to_le` | -| `to_be_bytes` | -| `to_le_bytes` | -| `trailing_zeros` | -| `trailing_ones` | -| `leading_zeros` | -| `leading_ones` | -| `count_zeros` | -| `count_ones` | - - -### List of UBs - -In addition to any properties called out as `SAFETY` comments in the source -code, -all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory. -* Mutating immutable bytes. -* Producing an invalid value - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0018-nonzero-correctness.md b/doc/src/challenges/0018-nonzero-correctness.md deleted file mode 100644 index 63a0f0ace05a6..0000000000000 --- a/doc/src/challenges/0018-nonzero-correctness.md +++ /dev/null @@ -1,86 +0,0 @@ -# Challenge 19: Correctness of `NonZero` functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *N/A* - -------------------- - -## Goal - -Verify the correctness of `NonZero` functions in `core::num`. - -### Assumptions - -This challenge is the continuation of Challenge 12: Safety of `NonZero` and Challenge 14: Safety of Primitive Conversions. - -Now, you need to verify the "correctness" of the functions listed in Challenge 12. - -HOWEVER, You DON'T need to prove the "correctness" from the functions' descriptions, you JUST need to prove that those functions are consistent with those of -the primitive integer types (under safety preconditions of Challenge 12). - -For example, for the `max` function, you need to prove that -`∀ T in {isize, i8, i16, ... , usize, u8, ... }, ∀ x, y : NonZero, x.max(y).get() == x.get().max(y.get())` - -Proving the correctness of the functions of primitive integer types is proposed in Challenge 16 and 17. - -### Success Criteria - -Verify that the following functions and methods (all located within `core::num::nonzero`) are consistent with those of all of the primitive integer types: - -| Function | -|--------- | -| `max` | -| `min` | -| `clamp` | -| `bitor` (all 3 implementations) | -| `count_ones` | -| `rotate_left` | -| `rotate_right` | -| `swap_bytes` | -| `reverse_bits` | -| `from_be` | -| `from_le` | -| `to_be` | -| `to_le` | -| `checked_mul` | -| `saturating_mul` | -| `unchecked_mul` | -| `checked_pow` | -| `saturating_pow` | -| `neg` | -| `checked_add` | -| `saturating_add` | -| `unchecked_add` | -| `checked_next_power_of_two` | -| `midpoint` | -| `isqrt` | -| `abs` | -| `checked_abs` | -| `overflowing_abs` | -| `saturating_abs` | -| `wrapping_abs` | -| `unsigned_abs` | -| `checked_neg` | -| `overflowing_neg` | -| `wrapping_neg` | -| `from_mut` | -| `from_mut_unchecked` | - - -### List of UBs - -In addition to any properties called out as `SAFETY` comments in the source -code, -all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory. -* Mutating immutable bytes. -* Producing an invalid value - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. - diff --git a/doc/src/challenges/0019-silce.md b/doc/src/challenges/0019-silce.md deleted file mode 100644 index 02247ef04a68e..0000000000000 --- a/doc/src/challenges/0019-silce.md +++ /dev/null @@ -1,79 +0,0 @@ -# Challenge 20: Verify the memory safety of `slice` functions - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *?* - -------------------- - - -## Goal - -Verify the memory safety of [`std::slice` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/mod.rs). - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | -|---------| -|first_chunk| -|first_chunk_mut| -|split_first_chunk| -|split_first_chunk_mut| -|split_last_chunk| -|split_last_chunk_mut| -|last_chunk| -|last_chunk_mut| -|get_unchecked| -|get_unchecked_mut| -|as_ptr_range| -|as_mut_ptr_range| -|as_array| -|as_mut_array| -|swap| -|swap_unchecked| -|reverse| -|as_chunks_unchecked| -|as_chunks| -|as_rchunks| -|as_chunks_unchecked_mut| -|split_at_unchecked| -|split_at_mut_unchecked| -|split_at_checked| -|split_at_mut_checked| -|binary_search_by| -|partition_dedup_by| -|rotate_left| -|rotate_right| -|copy_from_slice| -|copy_within| -|swap_with_slice| -|align_to| -|align_to_mut| -|as_simd| -|as_simd_mut| -|get_many_unchecked_mut| -|get_many_mut| -|as_flattened| -|as_flattened_mut| - -The verification must be unbounded---it must hold for slices of arbitrary length. - -The verification must be hold for generic type `T` (no monomorphization). - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0020-slice-iter.md b/doc/src/challenges/0020-slice-iter.md deleted file mode 100644 index 228f6fc029492..0000000000000 --- a/doc/src/challenges/0020-slice-iter.md +++ /dev/null @@ -1,64 +0,0 @@ -# Challenge 21: Verify the memory safety of `slice` iter functions - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *?* - -------------------- - - -## Goal - -Verify the memory safety of functional correctness of [`std::slice` iter functions] (https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/core/src/slice/iter/macros.rs). - - -### Success Criteria - -The memory safety of the following public functions that iterating over the internal inductive data type must be verified: - -| Function | -|---------| -|next_back_unchecked| -|make_slice| -|pre_dec_end| -|post_inc_start| -|len| -|is_empty| -|next| -|size_hint| -|count| -|nth| -|advance_by| -|last| -|fold| -|for_each| -|all| -|any| -|find| -|find_map| -|position| -|rposition| -|next_back| -|nth_back| -|advance_back_by| -|next_unchecked| - - -The verification must be unbounded---it must hold for slices of arbitrary length. - -The verification must be hold for generic type `T` (no monomorphization). - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0021-str-encode.md b/doc/src/challenges/0021-str-encode.md deleted file mode 100644 index 004a1958dc315..0000000000000 --- a/doc/src/challenges/0021-str-encode.md +++ /dev/null @@ -1,58 +0,0 @@ -# Challenge 5: Verify the correctness of UTF8 and UTF16 encoding functions -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - - -## Goal - -Verify the the correctness of functions related to UTF8 and UTF16 encoding - -### Details - -Rust str and String are either UTF8 or UTF16 encoded. Verifying the correctess of the related functions is important in ensuring the safety and correctness of Rust programs that involve Strings. - - -### Success Criteria - -Verify the the correctness of the following functions is functionally correct according to the UTF8 anf UTF16 descriptions in: -https://en.wikipedia.org/wiki/UTF-8 and https://en.wikipedia.org/wiki/UTF-16 - -| Function | Location | -|---------|---------| -|run_utf8_validation| core::src::str::validation | -|next_code_point| core::src::str::validation | -|next_code_point_reverse| core::src::str::validation | -|decode_utf16| core::src::char::decode | -|from_utf8| core::str::converts | -|from_utf8_unchecked| core::str::converts | -|from_utf8_mut| core::str::converts | -|from_utf8_unchecked_mut| core::str::converts | -|chars| core::str::mod | -|char_indices| core::str::mod | -|encode_utf16| core::str::mod| -|from_utf16| alloc::src::string | -|from_utf16_lossy| alloc::src::string | - - - -The verification must be unbounded---it must hold for inputs of arbitrary size. - - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0022-char-pattern.md b/doc/src/challenges/0022-char-pattern.md deleted file mode 100644 index e004796ca5880..0000000000000 --- a/doc/src/challenges/0022-char-pattern.md +++ /dev/null @@ -1,45 +0,0 @@ -# Challenge 23: Verify the correctness of char-related functions in str::pattern - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - - -### Details - -Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. -Those functions is implemented in core::str, but the core of them is implemented in core::str::pattern. -The main purposes of the functions in core::src::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), -then implementing the searching alorithm for those Searchers. - -IMPORTANT NOTE: You can assume the correctness of functions in Challenge 21. - -### Success Criteria - -Verify the memory safety and functional correctness of the following functions in -https://github.com/rust-lang/rust/blob/96cfc75584359ae7ad11cc45968059f29e7b44b7/library/core/src/str/pattern.rs - -1. `next`, `next_match`, `next_back`, `next_match_back`, -which are implemented for `CharSearcher`, `MultiCharEqSearcher`, `CharArraySearcher` , `CharArrayRefSearcher`, `CharSliceSearcher`, `CharPredicateSearcher` -2. `is_contained_in`, `is_prefix_of`, `strip_prefix_of` -which are implemented for `char`, `[char; N]`, `&[char; N]`, `&[char]`, `FnMut(char) -> bool` - -The verification must be unbounded---it must hold for inputs of arbitrary size. - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0023-two-way-search.md b/doc/src/challenges/0023-two-way-search.md deleted file mode 100644 index b7cec2881d6a1..0000000000000 --- a/doc/src/challenges/0023-two-way-search.md +++ /dev/null @@ -1,31 +0,0 @@ -# Challenge 23: Verify the correctness of the Two-Way search algorithm implementation in str::pattern - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - -### Details - -This algorithm is the main component of implementing searching functions for Patterns as substrings. - -### Success Criteria - -Verify the memory safety and functional correctness of the Two-Way search algorithm implementation in core::str::pattern. - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0024-substr-pattern.md b/doc/src/challenges/0024-substr-pattern.md deleted file mode 100644 index 7bf29efd51c04..0000000000000 --- a/doc/src/challenges/0024-substr-pattern.md +++ /dev/null @@ -1,45 +0,0 @@ -# Challenge 23: Verify the correctness of substring-related functions in str::pattern - -- **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *5,000 USD* - -------------------- - - -### Details - -Most functions in str library is defined on the concept of Pattern, which can be a char, a set of chars, a char filter, or a substring. -Those functions is implemented in core::str, but the core of them is implemented in core::src::str::pattern. -The main purposes of the functions in core::str::pattern is converting a str (a slice of bytes) into some kinds of Searchers (iterators), -then implementing the searching alorithm for those Searchers. - -IMPORTANT NOTE: You can assume the correctness of the Two-Way search algorithm (see Challenge 23), BUT have to verify the correctness of the simd_contains functions. - -### Success Criteria - -Verify the memory safety and functional correctness of the following functions in -https://github.com/rust-lang/rust/blob/96cfc75584359ae7ad11cc45968059f29e7b44b7/library/core/src/str/pattern.rs - -`next`, `next_match`, `next_back`, `next_match_back` -which are implemented for `StrSearcher` and `is_contained_in`, `is_prefix_of`, `strip_prefix_of`, `is_suffix_of`, `strip_suffix_of` for `&str`. - -The verification must be unbounded---it must hold for inputs of arbitrary size. - - - - -### List of UBs - -All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory except for padding or unions. -* Mutating immutable bytes. -* Producing an invalid value - - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. diff --git a/doc/src/challenges/0025-str-iter.md b/doc/src/challenges/0025-str-iter.md deleted file mode 100644 index 836503a681c7a..0000000000000 --- a/doc/src/challenges/0025-str-iter.md +++ /dev/null @@ -1,82 +0,0 @@ -# Challenge 25: Correctness of str functions - -- **Status:** Open -- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2025/03/07* -- **End date:** *2025/10/17* -- **Reward:** *N/A* - -------------------- - -## Goal - -Verify the correctness of functions in `core::src::str::mod.rs`. - -IMPORTANT NOTE: You can assume the correctness of all the functions that are verified in Challenges 21 to 24, BUT you may have to verify the correctness of other dependent functions in core::str::iter - -### Success Criteria - -Prove the correctness the following functions and methods in `core::str::mod.rs` : -| Function | -|--------- | -| `is_char_boundary`| -| `floor_char_boundary`| -| `ceil_char_boundary`| -| `split_at` | -| `split_at_mut` | -| `split_at_checked` | -| `split_at_mut_checked` | -| `split_at_unchecked` | -| `split_at_mut_unchecked` | -| `split_whitespace` | -| `split_ascii_whitespace` | -| `lines` | -| `lines_any` | -| `starts_with` | -| `ends_with` | -| `find`| -| `rfind`| -| `rotate_left`| -| `rotate_right`| -| `split` | -| `split_inclusive` | -| `rsplit` | -| `split_terminator` | -| `rsplit_terminator` | -| `splitn` | -| `rsplitn` | -| `split_once` | -| `rsplit_once` | -| `matches` | -| `rmatches` | -| `match_indices` | -| `rmatch_indices` | -| `trim` | -| `trim_start` | -| `trim_end` | -| `trim_left` | -| `trim_right` | -| `trim_right` | -| `trim_start_matches` | -| `strip_prefix` | -| `strip_suffix` | -| `trim_end_matches` | -| `trim_left_matches` | -| `trim_right_matches` | - -The verification must be unbounded---it must hold for str of arbitrary size. - - -### List of UBs - -In addition to any properties called out as `SAFETY` comments in the source -code, -all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): - -* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. -* Reading from uninitialized memory. -* Mutating immutable bytes. -* Producing an invalid value - -Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) -in addition to the ones listed above. From fd6642e0c340db1f8d19eb88a9389d959208e9f8 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 6 Mar 2025 09:40:07 -0800 Subject: [PATCH 12/18] fix typos --- doc/src/challenges/0016-iter.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md index 21fb41dcb7129..2689229534cd1 100644 --- a/doc/src/challenges/0016-iter.md +++ b/doc/src/challenges/0016-iter.md @@ -1,4 +1,4 @@ -# Challenge 21: Verify the safety of `slice` iter functions - part 2 +# Challenge 16: Verify the safety of Iterator functions - **Status:** Open - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) From 2fbbbb0a183cd3d83e0e432efdefc79d3432ec51 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Mar 2025 08:28:24 -0700 Subject: [PATCH 13/18] fix date format --- doc/src/challenges/0016-iter.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md index 2689229534cd1..06643ef776334 100644 --- a/doc/src/challenges/0016-iter.md +++ b/doc/src/challenges/0016-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 2676728585f4b5074283d6c6495c9891f58d9b25 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Mar 2025 08:32:31 -0700 Subject: [PATCH 14/18] fix typos --- doc/src/challenges/0016-iter.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md index 06643ef776334..a91c0dd5fa426 100644 --- a/doc/src/challenges/0016-iter.md +++ b/doc/src/challenges/0016-iter.md @@ -52,7 +52,7 @@ Write and prove the contract for the safety of the following functions: The verification must be unbounded---it must hold for slices of arbitrary length. -The verification must be hold for generic type `T` (no monomorphization). +The verification must hold for generic type `T` (no monomorphization). ### List of UBs From 36badcbfe152e28f1f7ca3f5f810a8309dfed77c Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 09:09:42 -0700 Subject: [PATCH 15/18] fix issue link, reward --- doc/src/challenges/0016-iter.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md index a91c0dd5fa426..1112a55ca2dfb 100644 --- a/doc/src/challenges/0016-iter.md +++ b/doc/src/challenges/0016-iter.md @@ -1,10 +1,10 @@ # Challenge 16: Verify the safety of Iterator functions - **Status:** Open -- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#280](https://github.com/model-checking/verify-rust-std/issues/280) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *?* +- **Reward:** *5000 USD* ------------------- From 15f3c83e466d7fa0dfbba52058aa633a507c2509 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 18 Mar 2025 16:45:20 -0700 Subject: [PATCH 16/18] update SUMMARY.md, separate safe/unsafe functions --- doc/src/SUMMARY.md | 1 + doc/src/challenges/0016-iter.md | 26 ++++++++++++++++---------- 2 files changed, 17 insertions(+), 10 deletions(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index f1de498184d14..86385d62ba13f 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -29,3 +29,4 @@ - [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) + - [16: Verify the safety of Iterator functions](./challenges/0016-iter.md) diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md index 1112a55ca2dfb..78f0381f52cee 100644 --- a/doc/src/challenges/0016-iter.md +++ b/doc/src/challenges/0016-iter.md @@ -17,39 +17,45 @@ Verify the safety of iter functions that are defined in (library/core/src/iter/a ### Success Criteria -Write and prove the contract for the safety of the following functions: +Write and prove the contract for the safety of the following unsafe functions: | Function | Defined in | |---------| ---------| -|next_back_remainder| array_chunks.rs| -|fold| array_chunks.rs| |__iterator_get_unchecked| clone.rs| -|fold| clone.rs| |next_unchecked| clone.rs| |__iterator_get_unchecked| copied.rs| -|spec_next_chunk| copied.rs| |__iterator_get_unchecked| enumerate.rs| -|next_chunk| filter.rs| -|next_chunk| filter_map.rs| |__iterator_get_unchecked | fuse.rs| |__iterator_get_unchecked | map.rs| |next_unchecked | map.rs| +|__iterator_get_unchecked | skip.rs| +|__iterator_get_unchecked | zip.rs| +|get_unchecked| zip.rs| + +Prove the absence of UB for following safe functions: + +| Function | Defined in | +|---------| ---------| +|next_back_remainder| array_chunks.rs| +|fold| array_chunks.rs| +|spec_next_chunk| copied.rs| +|next_chunk_dropless| filter.rs| +|next_chunk| filter_map.rs| |as_array_ref | map_windows.rs| |as_uninit_array_mut | map_windows.rs| |push | map_windows.rs| |drop | map_windows.rs| -|__iterator_get_unchecked | skip.rs| |original_step | step_by.rs| |spec_fold| take.rs| |spec_for_each| take.rs| -|__iterator_get_unchecked | zip.rs| -|get_unchecked| zip.rs| |fold| zip.rs| |next| zip.rs| |nth| zip.rs| |next_back| zip.rs| |spec_fold| zip.rs| + + The verification must be unbounded---it must hold for slices of arbitrary length. The verification must hold for generic type `T` (no monomorphization). From e9caacfaef304ccfcdea49d693b02e3615ec740c Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sat, 22 Mar 2025 11:01:50 -0400 Subject: [PATCH 17/18] safea abstractions --- doc/src/challenges/0016-iter.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md index 78f0381f52cee..5b60a5f151017 100644 --- a/doc/src/challenges/0016-iter.md +++ b/doc/src/challenges/0016-iter.md @@ -32,7 +32,7 @@ Write and prove the contract for the safety of the following unsafe functions: |__iterator_get_unchecked | zip.rs| |get_unchecked| zip.rs| -Prove the absence of UB for following safe functions: +Prove the absence of undefined behavior for following safe abstractions: | Function | Defined in | |---------| ---------| From 63540f7ebe8636bb19eee0fbb33904289659e83e Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 2 Apr 2025 12:49:12 -0700 Subject: [PATCH 18/18] Modify reward --- doc/src/challenges/0016-iter.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md index 5b60a5f151017..b85b9badc70a4 100644 --- a/doc/src/challenges/0016-iter.md +++ b/doc/src/challenges/0016-iter.md @@ -4,7 +4,7 @@ - **Tracking Issue:** [#280](https://github.com/model-checking/verify-rust-std/issues/280) - **Start date:** *2025-03-07* - **End date:** *2025-10-17* -- **Reward:** *5000 USD* +- **Reward:** *10,000 USD* -------------------