From 5a369ecc0579d09b703b6b5f98fec5c2b219466d Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 11 Jun 2024 10:33:07 -0700
Subject: [PATCH] Add initial challenge template (#10)

Add an initial template for challenges, and also a CI status badge for
README and tools page.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 README.md           |  4 +++
 doc/src/template.md | 60 ++++++++++++++++++++++++++++++++++++++++++++-
 doc/src/tools.md    |  6 ++---
 3 files changed, 66 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index d4a7b44ad5dfb..b718f3fc6b1cd 100644
--- a/README.md
+++ b/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
diff --git a/doc/src/template.md b/doc/src/template.md
index d21ca3b687fab..b7ed239c6a50f 100644
--- a/doc/src/template.md
+++ b/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.
\ No newline at end of file
diff --git a/doc/src/tools.md b/doc/src/tools.md
index 6879e2aa6eae7..1e86d661ccb2e 100644
--- a/doc/src/tools.md
+++ b/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)      |