RFC for List Subcommand

rfc/src/SUMMARY.md

@@ -17,3 +17,4 @@
 - [0009-function-contracts](rfcs/0009-function-contracts.md)
 - [0010-quantifiers](rfcs/0010-quantifiers.md)
 - [0011-source-coverage](rfcs/0011-source-coverage.md)
+- [0012-list](rfcs/0012-list.md)

rfc/src/rfcs/0012-list.md

@@ -0,0 +1,174 @@
+- **Feature Name:** List Subcommand
+- **Feature Request Issue:** [#2573](https://github.com/model-checking/kani/issues/2573), [#1612](https://github.com/model-checking/kani/issues/1612)
+- **RFC PR:** #3463
+- **Status:** Under Review
+- **Version:** 0
+
+-------------------
+
+## Summary
+
+Add a subcommand `list` that, for each crate under verification, lists the information relevant to its verification.
+
+## User Impact
+
+Currently, there is no automated way for a user to gather metadata about Kani's integration with their project. If, for example, a user wants a list of harnesses for their project, they must search for all the relevant contract attributes (currently `#[proof]` or `#[proof_for_contract]`) themselves. If done manually, this process is tedious, especially for large projects. Even with a shell script, it is error-prone--if, for example, we introduce a new type of proof harness, users would have to account for it when searching their project.
+
+Internally, this feature will be useful for tracking our customers' use of Kani and our progress with standard library verification. Externally, users can leverage this feature to get a high-level view of which areas of their projects have harnesses (and, by extension, which areas are still in need of verification).
+
+This feature will not cause any regressions for exisiting users.
+
+## User Experience
+
+Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[human|json]`, which changes the output format. The default is `human`, which prints to the terminal. The `json` option creates and writes to a JSON file instead.
+
+This subcommand will not fail. In the case that it does not find any harnesses or contracts, it will print a message informing the user of that fact.
+
+### Human Format
+
+The default format, `human`, will print the harnesses and contracts in a project, along with the total counts of each.
+
+For example:
+
+```
+Kani Version: 0.5.4
+
+Standard Harnesses:
+- example::verify::check_new
+- example::verify::check_modify
+
+Contract Harnesses:
+- example::verify::check_foo_u32
+- example::verify::check_foo_u64
+- example::verify::check_func
+- example::verify::check_bar
+
+Contracts:
+|--------------------------|-----------------------------------------------|
+| Function                 |  Contract Harnesses                           |
+|--------------------------|-----------------------------------------------|
+| example::impl::func      |  example::verify::check_func                  |
+|--------------------------|-----------------------------------------------|
+| example::impl::bar       |  example::verify::check_bar                   |
+|--------------------------|-----------------------------------------------|
+| example::impl::foo       |  example::verify::check_foo_u32,              |
+|                          |  example::verify::check_foo_u64               |
+|--------------------------|-----------------------------------------------|
+| example::prep::parse     |  NONE                                         |
+|--------------------------|-----------------------------------------------|
+
+Totals:
+- Standard Harnesses: 2
+- Contract Harnesses: 4
+- Functions with Contracts: 4
+- Contracts: 10
+```
+
+A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness.
+
+### JSON Format
+
+As the name implies, the goal of the `human` output is to be friendly for human readers. If the user wants an output format that's more easily parsed by a script, they can use the `json` option. 
+
+The JSON format will contain the same information as the human format, with the addition of file paths and JSON version. The JSON version number will start at zero and increment whenever we make an update to the format. This way, any users relying on this format for their scripts can realize that changes have occurred and update their logic accordingly.
+
+For example:
+
+```json
+{
+    kani-version: 0.5.4,
+    json-version: 0,
+    standard-harnesses: [
+        {
+            file: /Users/johnsmith/example/kani_standard_proofs.rs
+            harnesses: [
+                example::verify::check_modify,
+                example::verify::check_new
+            ]
+        },
+    ],
+    contract-harnesses: [
+        {
+            file: /Users/johnsmith/example/kani_contract_proofs.rs
+            harnesses: [
+                example::verify::check_bar,
+                example::verify::check_foo_u32,
+                example::verify::check_foo_u64, 
+                example::verify::check_func 
+            ]
+        },
+    ],
+    contracts: [
+        {
+            function: example::impl::func
+            file: /Users/johnsmith/example/impl.rs
+            harnesses: [example::verify::check_func]
+        },
+        {
+            function: example::impl::bar
+            file: /Users/johnsmith/example/impl.rs
+            harnesses: [example::verify::check_bar]
+        },
+        {
+            function: example::impl::foo
+            file: /Users/johnsmith/example/impl.rs
+            harnesses: [
+                example::verify::check_foo_u32,
+                example::verify::check_foo_u64
+            ]
+        },
+        {
+            function: example::prep::parse
+            file: /Users/johnsmith/example/prep.rs
+            harnesses: []
+        }
+    ],
+    totals: {
+        standard-harnesses: 2,
+        contract-harnesses: 4,
+        functions-with-contracts: 4,
+        contracts: 10,
+    }
+}
+```
+
+## Software Design
+
+We will add a new subcommand to `kani-driver`.
+
+*We will update this section once the UX is finalized*.
+
+## Rationale and alternatives
+
+Users of Kani may have many questions about their project--not only where their contracts and harnesses are, but also where their stubs are, what kinds of contracts they have, etc. Rather than try to answer every question a user might have, which would make the output quite verbose, we focus on these four:
+
+1. Where are the harnesses?
+2. Where are the contracts?
+3. Which contracts are verified, and by which harnesses?
+4. How many harnesses and contracts are there?
+
+We believe these questions are the most important for our use cases of tracking verification progress for customers and the standard library. The UX is designed to answer these questions clearly and concisely.
+
+We could have a more verbose or granular output, e.g., printing the metadata on a per-crate or per-module level, or including stubs or other attributes. Such a design would have the benefit of providing more information, with the disadvantage of being more complex to implement and more information for the user to process.
+
+If we do not implement this feature, users will have to obtain this metadata through manual searching, or by writing a script to do it themselves. This feature will improve our internal productivity by automating the process.
+
+## Open questions
+
+1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts, the number of `requires`, `ensures`, or `modifies` contracts, or the locations of the contracts.
+2. More generally, we could introduce additional options that collect information about other Kani attributes (e.g., stubs). The default would be to leave them out, but this way a user could get more verbose output if they so choose.
+
+## Out of scope / Future Improvements
+
+It would be nice to differentiate between regular Kani harnesses and Bolero harnesses. Bolero harnesses invoke Kani using conditional compilation, e.g.:
+
+```rust
+#[cfg_attr(kani, kani::proof)]
+fn check() {
+    bolero::check!()...
+}
+```
+
+See [this blog post](https://model-checking.github.io/kani-verifier-blog/2022/10/27/using-kani-with-the-bolero-property-testing-framework.html) for more information.
+
+There's no easy way for us to know whether a harness comes from Bolero, since Bolero takes care of rewriting the test to use Kani syntax and invoking the Kani engine. By the time the harness gets to Kani, there's no way for us to tell it apart from a regular harness. Fixing this would require some changes to our Bolero integration.