Add a new challenge about pointer arithmetic ops

In this challenge, we want to look at the safe usage of pointer
arithmetic operations.

doc/src/challenges/0003-pointer-arithmentic.md

@@ -2,9 +2,9 @@
 
 - **Status:** Open
 - **Solution:**
-- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/21
-- **Start date:** *24/06/24*
-- **End date:** *24/12/10*
+- **Tracking Issue:** <https://github.com/model-checking/verify-rust-std/issues/21>
+- **Start date:** 24/06/24
+- **End date:** 24/12/10
 
 -------------------
 
@@ -16,7 +16,19 @@ raw pointer access.
 
 ## Motivation
 
-TBD
+Raw pointer arithmetic is a common operation employed in the implementation of highly optimized code,
+as well as containers with dynamic size.
+Examples of the former are `str::repeat`, `[u8]::is_asc_ii`,
+while for the latter we have `Vec`, `VecDeque`, `HashMap`.
+
+These unsafe operations are usually abstracted from the end user with the usage of
+[safe abstractions](https://doc.rust-lang.org/beta/book/ch19-01-unsafe-rust.html#creating-a-safe-abstraction-over-unsafe-code).
+However, bugs in these abstractions may compromise entire applications, potentially becoming a security concern.
+See [CVE-2018-1000810](https://www.cvedetails.com/cve/CVE-2018-1000810/) for an example of an issue with an
+optimization of `str::repeat`.
+
+These safe abstractions are great candidates for software verification.
+They are critical for Rust applications safety, and they are modular by design.
 
 ## Description
 
@@ -72,12 +84,15 @@ All the following unsafe functions must be annotated with safety contracts and t
 | *mut T::byte_offset      | core::ptr       |
 | *mut T::byte_offset_from | core::ptr       |
 
-At least 10 of the following usages were proven safe:
+At least 3 of the following usages were proven safe:
 
-| Function          | Location    |
-|-------------------|-------------|
-| \[u8\]::is_asc_ii | core::slice |
-| TBD               | ...         |
+| Function          | Location      |
+|-------------------|---------------|
+| \[u8\]::is_asc_ii | core::slice   |
+| String::remove    | alloc::string |
+ | Vec::swap_remove | alloc::vec |
+ | Option::as_slice | core::option |
+ | VecDeque::swap   | collections::vec_deque |
 
 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):