Fix text

.github/workflows/book.yml

@@ -1,8 +1,8 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
-# This workflow is responsible for building and releasing the contest book.
-# It should only run when there has been a change to the contest book files
+# This workflow is responsible for building and releasing the book.
+# It should only run when there has been a change to the book files
 # or via manual trigger.
 
 name: Build Book
@@ -57,5 +57,3 @@ jobs:
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v4
-
-

README.md

@@ -1,56 +1,24 @@
-# Rust std-lib verification contest
-
-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 Rust releases.
-
-The goal is to have a contest to help verify the [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe. The contest will contain several challenges that can be solved by participants. These challenges can take on one of many forms such as:
+# Rust std-lib verification
 
+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
+Rust releases.
 
+The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
 1. Contributing to the core mechanism of verifying the rust standard library
 2. Creating new techniques to perform scalable verification
 3. Apply techniques to verify previously unverified parts of the standard library.
 
-
-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](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
-    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.
-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.
-
-
-For more details, refer to the [contest book page](http://link to contest book page) here.
-* * *
-
-## Getting Started
-
-To be filled out later.
-* * *
-
 ## [Kani](https://github.com/model-checking/kani)
 
 The Kani Rust Verifier is a bit-precise model checker for Rust.
-
 Kani verifies:
-
 * Memory safety (e.g., null pointer dereferences)
 * User-specified assertions (i.e `assert!(...)`)
 * The absence of panics (eg., `unwrap()` on `None` values)
 * The absence of some types of unexpected behavior (e.g., arithmetic overflows).
 
-
 You can find out more about Kani from the [Kani book](https://model-checking.github.io/kani/) or the [Kani repository on Github](https://github.com/model-checking/kani).
 
 ## Contact
@@ -66,10 +34,8 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
 ### Kani
 
 Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
-
 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
 
 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.

doc/book.toml

@@ -1,8 +1,8 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 [book]
-title = "Verify Rust Std Lib Contest"
-description = "Contest Rules and Challenges"
+title = "Verify Rust Std Lib"
+description = "How & What?"
 authors = ["Kani Developers"]
 language = "en"
 multilingual = false

doc/src/general-rules.md

@@ -6,37 +6,39 @@
 and we kept a copy of the Rust standard library inside the `library/` folder that shall be used as the verification target for all our challenges.
 We will periodically update the `library/` folder to track newer versions of the [official Rust standard library](https://github.com/rust-lang/rust/).
 NOTE: This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation.
-**Challenges:** Each challenge will be documented in the contest book in the Challenges chapter, and they will have a
-tracking issue where participants can add comments and ask clarification questions.
+**Challenges:** Each individual verification effort will have a
+tracking issue where contributors can add comments and ask clarification questions.
 You can find the list of [open challenges here](https://github.com/model-checking/verify-rust-std/labels/Challenge).
 
-**Solutions:** Solutions to a challenge should be submitted as a single Pull Request (PR) to the contest repository.
+**Solutions:** Solutions to a problem should be submitted as a single Pull Request (PR) to this repository. 
 The solution should run as part of the CI.
 See more details about [minimum requirements for each solution](general-rules.md#solution-requirements).
 
 
 ## Basic Workflow
 
-1. A challenge will be published in the contest book with details of the challenge,
-   and a tracking issue labeled with “Challenge” will be opened, so it can be used for clarifications and questions,
-   as well as to track the status of the challenge.
-2. Participants should create a fork of the contest repository where they will implement their proposed solution.
-3. Once they are to submit their solution for analysis, participants should create a PR against the contest repository for analysis.
+1. A verification effort will be published in the repository with
+appropriate details, and a tracking issue labeled with “Challenge”
+will be opened, so it can be used for clarifications and questions, as
+well as to track the status of the challenge.
+
+2. Participants should create a fork of the repository where they will implement their proposed solution.
+3. Once they submit their solution for analysis, participants should create a PR against the repository for analysis.
    Please make sure your solution meets [the minimum requirements described here](general-rules.md#solution-requirements).
 4. Each contribution will be reviewed on a first come, first served basis.
-   Acceptance will be based on a unanimous affirmative vote from the review committee.
+   Acceptance will be based on a review by a committee.
 5. Once approved by the review committee, the change will be merged into the repository.
 
 ## Solution Requirements
 
-A proposed solution to a contest will only **be reviewed** if all the minimum requirements below are met:
+A proposed solution to a verification problem will only **be reviewed** if all the minimum requirements below are met:
 
-* Each contribution or attempt should be submitted via a pull request to be analyzed by the committee.
+* Each contribution or attempt should be submitted via a pull request to be analyzed by reviewers. 
 * By submitting the solution, participants confirm that they can use, modify, copy, and redistribute their contribution,
   under the terms of their choice.
 * The contribution must be automated and should be checked and pass as part of the PR checks.
 * All tools used by the solution must be in [the list of accepted tools](tools.md#approved-tools),
-  and previously integrated in the contest repository.
+  and previously integrated in the repository.
   If that is not the case, please submit a separate [tool application first](todo.md).
 * There is no restriction on the number of contributors for a solution.
   Make sure you have the rights to submit your solution and that all contributors are properly mentioned.
@@ -48,7 +50,7 @@ challenged being solved.
 
 ## Call for Challenges
 
-The goal of the contest is to enable the verification of the entire Rust standard library.
+The goal of the effort is to enable the verification of the entire Rust standard library.
 The type of obstacles users face may depend on which part of the standard library you would like to verify. Thus, our challenges are developed with the target of verifying a specific section of the standard library or strengthening existing verification.
 
 Everyone is welcome to submit new challenge proposals for review by our committee.
@@ -75,7 +77,7 @@ Solutions must be automated using one of the tools previously approved and liste
 * Once the tool is approved, the participant needs to create a PR that creates a new action that runs the
   std library verification using the new tool, as well as an entry to the “Approved Tools” section of this book.
 * Once the PR is merged, the tool is considered integrated.
-* The contest repository will be updated periodically, which can impact the tool capacity to analyze the new version of the repository.
+* The repository will be updated periodically, which can impact the tool capacity to analyze the new version of the repository.
   I.e., the action may no longer pass after an update.
   This will not impact the approval status of the tool, however,
   new solutions that want to employ the tool may need to ensure the action is passing first.

doc/src/intro.md

@@ -1,14 +1,17 @@
-# Verify Rust Standard Library Contest
+# Verify Rust Standard Library Effort
 
-The Verify Rust Standard Library contest is an ongoing contest that targets the verification of the [Rust standard library](https://doc.rust-lang.org/std/). The goal of this contest is to provide automated verification that can be used to verify that a given Rust standard library implementation is safe.
+The Verify Rust Standard Library effort is an ongoing investment that
+targets the verification of the [Rust standard
+library](https://doc.rust-lang.org/std/). The goal of this is
+to provide automated verification that can be used to verify that a
+given Rust standard library implementation is safe.
 
-The contest will contain several challenges that can be solved by participants. These challenges can take on one of many forms such as:
+Efforts are largely classified in the following areas:
 
 1. Contributing to the core mechanism of verifying the rust standard library
 2. Creating new techniques to perform scalable verification
 3. Apply techniques to verify previously unverified parts of the standard library.
 
 
-We encourage everyone to watch this repository to be notified of any changes.
-
-In this book you can find more details about the contest such as: General Rules, Challenges, Verification Tools.
+We encourage everyone to watch this repository to be notified of any
+changes.