Merge branch 'main' into verify-0000-mem

README.md

@@ -1,5 +1,9 @@
 # Rust std-lib verification
 
+[![Rust Tests](https://github.com/model-checking/verify-rust-std/actions/workflows/rustc.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/rustc.yml)
+[![Build Book](https://github.com/model-checking/verify-rust-std/actions/workflows/book.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/book.yml)
+
+
 This repository is a fork of the official Rust programming
 language repository, created solely to verify the Rust standard
 library. It should not be used as an alternative to the official

doc/src/template.md

@@ -1 +1,59 @@
-# Challenge Template
+# Challenge XXXX[^challenge_id]: Challenge Title
+
+- **Status:** *One of the following: [Open | Resolved | Expired]*
+- **Solution:** *Option field to point to the PR that solved this challenge.*
+- **Tracking Issue:** *Link to issue*
+- **Start date:** *YY/MM/DD*
+- **End date:** *YY/MM/DD*
+
+-------------------
+
+
+## Goal
+
+*Describe the goal of this challenge with 1-2 sentences.*
+
+## 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*
+
+*Here are some examples of possible criteria:*
+
+All the following unsafe functions must be annotated with safety contracts and the contracts have been verified:
+
+|Function	|Location	|
+|---	|---	|
+|	|	|
+|	|	|
+|	|	|
+|	|	|
+|	|	|
+
+At least N of the following usages were proven safe:
+
+|Function	|Location	|
+|---	|---	|
+|	|	|
+|	|	|
+|	|	|
+|	|	|
+|	|	|
+
+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):
+
+*List of UBs*
+
+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.

doc/src/tools.md

@@ -9,9 +9,9 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
 
 ## Approved tools:
 
-| Tool      | CI Status |
-|-----------|-----------|
- | Kani     | TODO      |
+| Tool                | CI Status |
+|---------------------|-------|
+ | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |