From 1891af786653753e9ad467a6dd6ca49234539f23 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Mon, 3 Jun 2024 21:31:19 +0000 Subject: [PATCH 1/5] Add disclaimer, and fix links --- README.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index b54f56aebf0e8..7ed92bef26c55 100644 --- a/README.md +++ b/README.md @@ -11,20 +11,22 @@ The goal is to have a contest to help verify the [Rust standard library](https:/ To help you get started in the contest, Amazon’s [Kani-rust-verifier team](https://github.com/model-checking/kani) has created mechanisms and tools to help participants verify the standard library. The Kani team has also created some initial contracts and proofs (To be filled and linked here later) to help you get started as a participant. + +NOTE: This work is not official, affiliated, or endorsed by the Rust project or Rust Foundation * * * ## Contest Details Here are some details for the contest -1. This repository will contain templates for [Issues](http://Insert link to Issues page), [pull requests](http://Link to PR page here) etc. that will be used to create new challenges for verifying the Rust standard library. +1. This repository will contain templates for [Issues](https://github.com/model-checking/verify-rust-std/issues), [pull requests](https://github.com/model-checking/verify-rust-std/pulls) etc. that will be used to create new challenges for verifying the Rust standard library. 2. This repository will contain the initial contracts and proofs that AWS creates using Kani as a tool to verify the standard library. 3. Verification of the functions will be enabled using CI pipelines and Kani tool initially. 4. Any new tool that participants want to enable will require an application using an Issue template. This tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS 1. A new tool application should clearly specify the differences to existing techniques and provide sufficient background of why this is needed. 2. Once the tool is approved, it needs to be enabled using CI pipelines. 5. Each contribution or attempt should be submitted via a pull request that will be analyzed by the committee. -6. Each contribution will be reviewed on a first come first serve basis. Acceptance will be based on a unanimous affirmative vote from the review committee. +6. Each contribution will be reviewed on a first come first serve basis. Acceptance will be based on a unanimous affirmative vote from the review committee. 7. The contribution must be automated and should work in CI. 8. Once approved by the review committee, the change will be merged into the repository. @@ -53,7 +55,7 @@ You can find out more about Kani from the [Kani book](https://model-checking.git ## Contact -For questions, suggestions or feedback, feel free to open an issue on the Kani page with the tag `stdlib-contest` or contact us directly at [kani-developers@amazon.com](mailto:kani-developers@amazon.com). +For questions, suggestions or feedback, feel free to open an [issue on the Kani page](https://github.com/model-checking/kani/issues) with the tag `stdlib-contest` or contact us directly at [kani-developers@amazon.com](mailto:kani-developers@amazon.com). ## Security @@ -65,7 +67,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0). -See [LICENSE-APACHE](link to LICENSE-APACHE) and [LICENSE-MIT](link to LICENSE-MIT) for details. +See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details. ## Rust @@ -73,5 +75,3 @@ See [LICENSE-APACHE](link to LICENSE-APACHE) and [LICENSE-MIT](link to LICENSE-M Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses. See [the Rust repository](https://github.com/rust-lang/rust) for details. - - From 5d3aa44e2bec73dc63d4c0c8653b0af0fab8c130 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Mon, 3 Jun 2024 21:32:29 +0000 Subject: [PATCH 2/5] Grammar --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7ed92bef26c55..8b7e4d4cac25c 100644 --- a/README.md +++ b/README.md @@ -12,7 +12,7 @@ The goal is to have a contest to help verify the [Rust standard library](https:/ To help you get started in the contest, Amazon’s [Kani-rust-verifier team](https://github.com/model-checking/kani) has created mechanisms and tools to help participants verify the standard library. The Kani team has also created some initial contracts and proofs (To be filled and linked here later) to help you get started as a participant. -NOTE: This work is not official, affiliated, or endorsed by the Rust project or Rust Foundation +NOTE: This work is not official, affiliated, or endorsed by the Rust project or Rust Foundation. * * * ## Contest Details From 4752023dce45ec6ea79832e90c5b9f1a0e525eaa Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Thu, 6 Jun 2024 20:43:23 +0000 Subject: [PATCH 3/5] Update issues page --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 8b7e4d4cac25c..f5d5126314d2e 100644 --- a/README.md +++ b/README.md @@ -55,7 +55,7 @@ You can find out more about Kani from the [Kani book](https://model-checking.git ## Contact -For questions, suggestions or feedback, feel free to open an [issue on the Kani page](https://github.com/model-checking/kani/issues) with the tag `stdlib-contest` or contact us directly at [kani-developers@amazon.com](mailto:kani-developers@amazon.com). +For questions, suggestions or feedback, feel free to open an [issue on the Kani page](https://github.com/model-checking/verify-rust-std/issues) with the tag `stdlib-contest` or contact us directly at [kani-developers@amazon.com](mailto:kani-developers@amazon.com). ## Security From 0e5e6d0b66e953bf791f772a866995395a25d1d4 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 6 Jun 2024 16:48:48 -0400 Subject: [PATCH 4/5] Update README.md Co-authored-by: Celina G. Val --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index f5d5126314d2e..d8e35287a25f8 100644 --- a/README.md +++ b/README.md @@ -19,7 +19,7 @@ NOTE: This work is not official, affiliated, or endorsed by the Rust project or Here are some details for the contest -1. This repository will contain templates for [Issues](https://github.com/model-checking/verify-rust-std/issues), [pull requests](https://github.com/model-checking/verify-rust-std/pulls) etc. that will be used to create new challenges for verifying the Rust standard library. +1. This repository will contain templates for [Issues](https://github.com/model-checking/verify-rust-std/issues), and [pull requests](https://github.com/model-checking/verify-rust-std/pulls), that will be used to create new challenges for verifying the Rust standard library. 2. This repository will contain the initial contracts and proofs that AWS creates using Kani as a tool to verify the standard library. 3. Verification of the functions will be enabled using CI pipelines and Kani tool initially. 4. Any new tool that participants want to enable will require an application using an Issue template. This tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS From 79c2454fe6d72fc8281c2840d99a56bd8f945d1a Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Thu, 6 Jun 2024 16:48:54 -0400 Subject: [PATCH 5/5] Update README.md Co-authored-by: Celina G. Val --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d8e35287a25f8..54d3758a44485 100644 --- a/README.md +++ b/README.md @@ -55,7 +55,7 @@ You can find out more about Kani from the [Kani book](https://model-checking.git ## Contact -For questions, suggestions or feedback, feel free to open an [issue on the Kani page](https://github.com/model-checking/verify-rust-std/issues) with the tag `stdlib-contest` or contact us directly at [kani-developers@amazon.com](mailto:kani-developers@amazon.com). +For questions, suggestions or feedback, feel free to open an [issue here](https://github.com/model-checking/verify-rust-std/issues). ## Security