From 392b20adfb85b37115933166b71f8911a69302ed Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sun, 9 Jun 2024 16:24:06 -0700 Subject: [PATCH 1/3] Add CI status badge and initial challenge template --- README.md | 4 +++ doc/src/template.md | 67 ++++++++++++++++++++++++++++++++++++++++++++- doc/src/tools.md | 6 ++-- 3 files changed, 73 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..2aba31054705d 100644 --- a/doc/src/template.md +++ b/doc/src/template.md @@ -1 +1,66 @@ -# 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* + +------------------- + + +Status: [Open | Resolved | Expired]: +Tracking issue: +Start date: +Due date: +Author(s): + + +## 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 Stack Borrow".* + +### Success Criteria* + +*Here are few 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 below + +[^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) | From 77a8df34bea42833d637596e3664e8c63a2245ef Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 10 Jun 2024 11:51:38 -0700 Subject: [PATCH 2/3] Apply suggestions from code review --- doc/src/template.md | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/doc/src/template.md b/doc/src/template.md index 2aba31054705d..539bdb410f090 100644 --- a/doc/src/template.md +++ b/doc/src/template.md @@ -1,7 +1,7 @@ # 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.* +- **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* @@ -9,13 +9,6 @@ ------------------- -Status: [Open | Resolved | Expired]: -Tracking issue: -Start date: -Due date: -Author(s): - - ## Goal *Describe the goal of this challenge with 1-2 sentences.* @@ -30,7 +23,7 @@ Author(s): ### Assumptions -*Mention any assumption that users may make. Example, "assuming the usage of Stack Borrow".* +*Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".* ### Success Criteria* @@ -61,6 +54,6 @@ All proofs must automatically ensure the absence of the following undefined beha *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 below +in addition to the ones listed above [^challenge_id]: The number of the challenge sorted by publication date. \ No newline at end of file From ae7bffe080da0fcb8997b92ffaa753af271f7632 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Jun 2024 10:28:26 -0700 Subject: [PATCH 3/3] Apply suggestions from code review --- doc/src/template.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/template.md b/doc/src/template.md index 539bdb410f090..b7ed239c6a50f 100644 --- a/doc/src/template.md +++ b/doc/src/template.md @@ -27,7 +27,7 @@ ### Success Criteria* -*Here are few possible 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: @@ -54,6 +54,6 @@ All proofs must automatically ensure the absence of the following undefined beha *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 +in addition to the ones listed above. [^challenge_id]: The number of the challenge sorted by publication date. \ No newline at end of file