From a03f09dde14ffd54f0bb29a6ebe770fea44f050d Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 6 Sep 2024 16:49:36 -0400 Subject: [PATCH 1/2] Fix challenges numbering Signed-off-by: Felipe R. Monteiro --- doc/src/SUMMARY.md | 24 ++++++++++--------- doc/src/challenges/0001-core-transmutation.md | 2 +- doc/src/challenges/0002-intrinsics-memory.md | 2 +- .../challenges/0003-pointer-arithmentic.md | 2 +- doc/src/challenges/0004-btree-node.md | 2 +- doc/src/challenges/0005-linked-list.md | 2 +- doc/src/challenges/0006-nonnull.md | 2 +- doc/src/challenges/0008-smallsort.md | 2 +- doc/src/challenges/0010-string.md | 2 +- doc/src/challenges/0011-floats-ints.md | 2 +- doc/src/challenges/0012-nonzero.md | 2 +- 11 files changed, 23 insertions(+), 21 deletions(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 9dd37e37409ca..abb657984199e 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -13,14 +13,16 @@ --- - [Challenges](./challenges.md) - - [Core Transmutation](./challenges/0001-core-transmutation.md) - - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) - - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) - - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - - [Inductive data type](./challenges/0005-linked-list.md) - - [Safety of NonNull](./challenges/0006-nonnull.md) - - [Contracts for SmallSort](./challenges/0008-smallsort.md) - - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) - - [Memory safety of String](./challenges/0010-string.md) - - [Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) - - [Safety of NonZero](./challenges/0012-nonzero.md) + 1. [Core Transmutation](./challenges/0001-core-transmutation.md) + 2. [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) + 3. [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) + 4. [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) + 5. [Inductive data type](./challenges/0005-linked-list.md) + 6. [Safety of NonNull](./challenges/0006-nonnull.md) + 7. [--](./challenges/0007-.md) + 8. [Contracts for SmallSort](./challenges/0008-smallsort.md) + 9. [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) + 10. [Memory safety of String](./challenges/0010-string.md) + 11. [Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) + 12. [Safety of NonZero](./challenges/0012-nonzero.md) + diff --git a/doc/src/challenges/0001-core-transmutation.md b/doc/src/challenges/0001-core-transmutation.md index 3a71c0c12ff29..2b53256b3c34e 100644 --- a/doc/src/challenges/0001-core-transmutation.md +++ b/doc/src/challenges/0001-core-transmutation.md @@ -1,7 +1,7 @@ # Challenge 1: Verify `core` transmuting methods - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19) +- **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19) - **Start date:** 2024-06-12 - **End date:** 2024-12-10 diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index 3eac59fb02681..185e04e5a3e2a 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -1,7 +1,7 @@ # Challenge 2: Verify the memory safery of core intrinsics using raw pointers - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/16) +- **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16) - **Start date:** *24/06/12* - **End date:** *24/12/10* diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index 0e73c3c7f014a..5362983ffe0f3 100644 --- a/doc/src/challenges/0003-pointer-arithmentic.md +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -2,7 +2,7 @@ - **Status:** Open - **Solution:** -- **Tracking Issue:** +- **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76) - **Start date:** 24/06/24 - **End date:** 24/12/10 diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md index 6f29ce23eba73..835d71365292f 100644 --- a/doc/src/challenges/0004-btree-node.md +++ b/doc/src/challenges/0004-btree-node.md @@ -1,7 +1,7 @@ # Challenge 4: Memory safety of BTreeMap's `btree::node` module - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25) +- **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77) - **Start date:** *2024-07-01* - **End date:** *2024-12-10* diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index 5701acb7b82d2..a5c931712025a 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -1,7 +1,7 @@ # Challenge 5: Verify functions iterating over inductive data type: `linked_list` - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29) +- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) - **Start date:** *24/07/01* - **End date:** *24/12/10* diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index 1e5d8c7bb32c4..923e00427ad62 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -1,7 +1,7 @@ # Challenge 6: Safety of NonNull - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/53) +- **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53) - **Start date:** *2024-08-16* - **End date:** *2024-12-10* diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md index b0a4a8f743275..c6632af9af837 100644 --- a/doc/src/challenges/0008-smallsort.md +++ b/doc/src/challenges/0008-smallsort.md @@ -1,7 +1,7 @@ # Challenge 8: Contracts for SmallSort - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/56) +- **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56) - **Start date:** *2024-08-17* - **End date:** *2024-12-10* diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md index cb12bfe9fdfbd..4783841bee429 100644 --- a/doc/src/challenges/0010-string.md +++ b/doc/src/challenges/0010-string.md @@ -1,7 +1,7 @@ # Challenge 10: Memory safety of String - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61) +- **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61) - **Start date:** *2024-08-19* - **End date:** *2024-12-10* diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md index 881a15a09caff..9dde411c527ca 100644 --- a/doc/src/challenges/0011-floats-ints.md +++ b/doc/src/challenges/0011-floats-ints.md @@ -2,7 +2,7 @@ - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/59) +- **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59) - **Start date:** *2024-08-20* - **End date:** *2024-12-10* diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index f5d2dadf84437..15d2abbb8eb3c 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -1,7 +1,7 @@ # Challenge 12: Safety of `NonZero` - **Status:** Open -- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/71) +- **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) - **Start date:** *2024-08-23* - **End date:** *2024-12-10* From b1bae95586e42079c9f73e047b38abc4aec77da4 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 6 Sep 2024 17:31:07 -0400 Subject: [PATCH 2/2] Add numbering manually Signed-off-by: Felipe R. Monteiro --- doc/src/SUMMARY.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index abb657984199e..db5018121be02 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -13,16 +13,16 @@ --- - [Challenges](./challenges.md) - 1. [Core Transmutation](./challenges/0001-core-transmutation.md) - 2. [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md) - 3. [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md) - 4. [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) - 5. [Inductive data type](./challenges/0005-linked-list.md) - 6. [Safety of NonNull](./challenges/0006-nonnull.md) - 7. [--](./challenges/0007-.md) - 8. [Contracts for SmallSort](./challenges/0008-smallsort.md) - 9. [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) - 10. [Memory safety of String](./challenges/0010-string.md) - 11. [Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) - 12. [Safety of NonZero](./challenges/0012-nonzero.md) + - [1: Verify core transmuting methods](./challenges/0001-core-transmutation.md) + - [2: Verify the memory safery of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md) + - [3: Verifying Raw Pointer Arithmetic Operations](./challenges/0003-pointer-arithmentic.md) + - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md) + - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md) + - [6: Safety of `NonNull`](./challenges/0006-nonnull.md) + - [8: Contracts for SmallSort](./challenges/0008-smallsort.md) + - [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md) + - [10: Memory safety of String](./challenges/0010-string.md) + - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) + - [12: Safety of `NonZero`](./challenges/0012-nonzero.md) +