Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update tool application docs; add issue template #18

Merged
merged 1 commit into from
Dec 10, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions .github/ISSUE_TEMPLATE/tool_application.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
---
name: Tool Application
about: Submit a new tool application
title: "[Tool Application] "
labels: Tool Application
---

{% include_relative ../doc/src/tool_template.md %}
25 changes: 11 additions & 14 deletions doc/src/general-rules.md
Original file line number Diff line number Diff line change
Expand Up @@ -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).
This will not impact the approval status of the tool, however, new solutions that want to employ the tool may need to ensure the workflow is passing first.

## Committee Applications

Expand Down
15 changes: 11 additions & 4 deletions doc/src/tool_template.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)._

Expand All @@ -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?)._
Loading