Update tool application section of book (#221)

This PR updates the tool application section of our book. The key
changes are:

- Specify how to submit tool applications (through an issue). Also
provide a "Tool Application" issue template.
- Move the details about specifying differences with other tools and
audit information to the application so they're harder to miss.

(These changes are inspired by our experience with the [Verifast
application](#213);
I realized there's a few things we can make clearer on our end).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Michael Tautschnig <[email protected]>

.github/ISSUE_TEMPLATE/tool_application.md

@@ -0,0 +1,10 @@
+---
+name: Tool Application
+about: Submit a new tool application
+title: "[Tool Application] "
+labels: Tool Application
+---
+
+<!--
+Please see https://model-checking.github.io/verify-rust-std/tool_template.html for the application template.
+-->

doc/src/general-rules.md

@@ -69,20 +69,17 @@ Follow the following steps to create a new proposal:
 
 ## Tool Applications
 
-Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools):
-
-* Any new tool that participants want to enable will require an application using the [tool application template](./tool_template.md).
-* The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS
-* A new tool application should clearly specify the differences to existing techniques and provide sufficient background
-  of why this is needed.
-* The tool application should also include mechanisms to audit its implementation and correctness.
-* 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 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.
+Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools).
+To use a new tool, participants must first submit an application for it.
+
+* To submit a tool application, open a new issue in this repository using the "Tool Application" issue template.
+* The committee will review the application. Once a committee member approves the application, the participant needs to create a PR with:
+  * A new workflow that runs the tool against the standard library.
+  * A new entry to the “Approved Tools” section of this book.
+* Once this PR is merged, the tool is considered integrated, and the tool application issue will be closed.
+
+The repository will be updated periodically, which can impact a tool's capacity to analyze the new version of the repository (i.e., the workflow may no longer pass after an update).
+If it is determined that the tool requires changes and such changes cannot be provided in a timely fashion the tool's approval may be revoked.
 
 ## Committee Applications
 

doc/src/tool_template.md

@@ -15,6 +15,9 @@ _Please enter a description for your tool and any information you deem relevant.
 * [ ] Is the tool under development? 
 * [ ] Will you or your team be able to provide support for the tool?
 
+## Comparison to Other Approved Tools
+_Describe how this tool compares to the other approved tools. For example, are there certain properties that this tool can prove that the other tools cannot? The comparison does not need to be exhaustive; the purpose of this section is for the committee to understand the salient differences, and how this tool would fit into the larger effort._
+
 ## Licenses
 _Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s)._
 
@@ -24,8 +27,12 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
 2. \[Second Step\]
 3. \[and so on...\]
 
-## Artifacts
-_If there are noteworthy examples of using the tool to perform verification, please include them in this section.Links, papers, etc._
+## Artifacts & Audit Mechanisms
+_If there are noteworthy examples of using the tool to perform verification, please include them in this section. Links, papers, etc._
+_Also include mechanisms for the committee to audit the implementation and correctness of this tool (e.g., regression tests)._
+
+## Versioning
+_Please describe how you version the tool._
 
-## CI & Versioning
-_Please describe how you version the tool and how it will be supported in CI pipelines._
+## CI
+_If your tool is approved, you will be responsible merging a workflow into this repository that runs your tool against the standard library. For an example, see the Kani workflow (.github/workflows/kani.yml). Describe, at a high level, how your workflow will operate. (E.g., how will you package the tool to run in CI, how will you identify which proofs to run?)._