Add the challenge to page

doc/src/SUMMARY.md

@@ -13,3 +13,4 @@
 
 # Challenges
 - [Coming soon](./todo.md)
+- [Memory safety of core intrinsics](./intrinsics-memory.md)

doc/src/intrinsics-memory.md

@@ -0,0 +1,106 @@
+# Challenge 2: Verify the memory safery of core intrinsics using raw pointers
+
+- **Status:** *One of the following: [Open | Resolved | Expired]* Open
+- **Tracking Issue:** *Link to issue*
+- **Start date:** *YY/MM/DD*
+- **End date:** *YY/MM/DD*
+
+-------------------
+
+
+## Goal
+
+Annotate Rust core::intrinsics functions that manipulate raw pointers with their safety contract and verify their usage in the standard library are in fact safe.
+
+## Motivation
+
+*Explain why this is a challenge that should be prioritized. Consider using a motivating example.*
+
+## Description
+
+*Describe the challenge in more details.*
+
+### Assumptions
+
+*Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".*
+
+### Success Criteria*
+
+1. All the following intrinsic functions must be annotated with safety contracts.
+2. Any fallback intrinsic implementation must be verified.
+3. For intrinsics modeled in the tool of choice, explain how its implementation matches the intrinsics definition. This can either be done in the PR description or as an entry to the contest book as part of the “Tools” chapter.
+4. For each function, contestants must state clearly the list of assumptions for each proof, how the proofs can be audit, and the list of (implicit and explicit) properties that are guarantee.
+5. The verification of each intrinsics should ensure all the documented safety conditions are met, and that meeting them is enough to guarantee safe usages.
+
+
+#### Functions for verification
+
+|Function	|Location	|
+|---	|---	|
+|typed_swap | core::intrisics |
+vtable_size| core::intrisics |
+vtable_align| core::intrisics |
+copy_nonoverlapping| core::intrisics |
+copy| core::intrisics |
+write_bytes| core::intrisics |
+size_of_val| core::intrisics |
+arith_offset| core::intrisics |
+volatile_copy_nonoverlapping_memory| core::intrisics |
+volatile_copy_memory| core::intrisics |
+volatile_set_memory| core::intrisics |
+volatile_load| core::intrisics |
+volatile_store| core::intrisics |
+unaligned_volatile_load| core::intrisics |
+unaligned_volatile_store| core::intrisics |
+compare_bytes| core::intrisics |
+min_align_of_val| core::intrisics |
+ptr_offset_from| core::intrisics |
+ptr_offset_from_unsigned| core::intrisics |
+read_via_copy| core::intrisics |
+write_via_move| core::intrisics |
+|	|	|
+
+
+
+**At least 10 of the following usages of intrinsics were proven safe:**
+
+|Function	|Location	|
+|---	|---	|
+|copy_from_slice	| core::slice |
+parse_u64_into	| std::fmt |
+swap | core::mem |
+align_of_val | core::mem |
+zeroed | core::mem::maybe_uninit |
+|	|	|
+
+
+
+**At least 5 unsafe functions that expose those intrinsics are also annotated with safety contracts, and those contracts are verified:**
+
+|Function	|Location	|
+|---	|---	|
+|copy_from_slice	| std::ptr |
+parse_u64_into	| std::ptr |
+swap | std::ptr |
+align_of_val | std::ptr |
+zeroed | std::ptr |
+|	|	|
+
+
+
+
+### 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):
+
+* Invoking undefined behavior via compiler intrinsics.
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* 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.
+
+[^challenge_id]: The number of the challenge sorted by publication date.