Merge branch 'add-kani-user-guide' of https://github.com/jaisnan/rust…

…-dev into add-kani-user-guide

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)      |
 
 
 

doc/src/tools/kani.md

@@ -5,15 +5,14 @@ Kani is designed to prove safety properties in your code as well as
 the absence of some forms of undefined behavior. It uses model checking under the hood to ensure that
 Rust programs adhere to user specified properties.
 
-You can find more informations about how to install in [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
+You can find more information about how to install in [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
 
 ## Usage
 
-Consider a rust function that takes an integer and returns its absolute value and
-a kani proof that invokes the function that you want to verify
+Consider a Rust function that takes an integer and returns its absolute value and
+a Kani proof that invokes the function that you want to verify
 
 ``` rust
-// src/main.rs
 fn abs_diff(a: i32, b: i32) -> i32 {
     if a > b {
         a - b
@@ -34,8 +33,6 @@ fn harness() {
 Running the command `cargo kani` in your cargo crate will give the result
 
 ```
-...Metadata about the Kani run
-
 RESULTS:
 Check 1: abs_diff.assertion.1
          - Status: FAILURE
@@ -50,19 +47,18 @@ Complete - 0 successfully verified harnesses, 1 failures, 1 total.
 ```
 
 
-## Using Kani to verify the rust standard library
+## Using Kani to verify the Rust Standard Library
 
-To aid the std library verification effort, Kani provides a subcommand out of the box to help you get started.
+To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started.
 
 ### Step 1
 
-Modify your local copy of the rust std library by writing proofs for the functions/methods that you want to verify.
+Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify.
 
-For example, insert this short blob into your copy of the std library. This blob imports the building-block APIs such as
+For example, insert this short blob into your copy of the library. This blob imports the building-block APIs such as
 `assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `proof_for_contract` and `fake_function`.
 
 ``` rust
-// src/lib/.rs
 #[cfg(kani)]
 kani_core::kani_lib!(core);
 
@@ -94,9 +90,9 @@ Run the following command in your local terminal:
 
 `kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing`.
 
-The command `kani verify-std` is a subcommand of the `kani`. This specific subcommand is used to verify the Rust standard library with the following arguments.
+The command `kani verify-std` is a sub-command of the `kani`. This specific sub-command is used to verify the Rust Standard Library with the following arguments.
 
-- `"path/to/library"`: This argument specifies the path to the modified Rust standard library that was prepared earlier in the script.
+- `"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script.
 - `--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files.
 
 Apart from these, you can use your regular `kani-args` such as `-Z function-contracts` and `-Z stubbing` depending on your verification needs.
@@ -118,5 +114,5 @@ Complete - 2 successfully verified harnesses, 0 failures, 2 total.
 
 ## More details
 
-You can find more informations about how to install and how you can customize your use of Kani in the
+You can find more information about how to install and how you can customize your use of Kani in the
 [Kani book](https://model-checking.github.io/kani/).