Add a few trait implementations to challenge

also fix warnings in the tool template section

Author: celinval

doc/src/challenges/0013-cstr.md

@@ -63,6 +63,15 @@ and that they maintain the overall safety invariant of `CStr` when called correc
 | `from_bytes_with_nul_uncheked` | `core::ffi::c_str`  |
 | `strlen`                       | `core::ffi::c_str`  |
 
+4. Verify that the following trait implementations for the `CStr` type are safe:
+
+
+| Trait                               | Implementation Location |
+|-------------------------------------|-------------------------|
+| `CloneToUninit` [^unsafe-fn]        | `core::clone`           |
+| `ops::Index<ops::RangeFrom<usize>>` | `core::ffi::c_str`      |
+
+[^unsafe-fn]: Unsafe functions will require safety contracts.
 
 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):
 
@@ -71,5 +80,5 @@ All proofs must automatically ensure the absence of the following undefined beha
 - Mutating immutable bytes.
 - Accessing uninitialized memory.
 
-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.
+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.

doc/src/tool_template.md

@@ -20,9 +20,9 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
 
 ## Steps to Use the Tool
 
-1. [First Step]
-2. [Second Step]
-3. [and so on...]
+1. \[First Step\]
+2. \[Second Step\]
+3. \[and so on...\]
 
 ## Artifacts
 _If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._