diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 9dd37e37409ca..db5018121be02 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: 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) + + 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*