List RFC revisions

rfc/src/SUMMARY.md

@@ -17,4 +17,5 @@
 - [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)
+- [0012-loop-contracts](rfcs/0012-loop-contracts.md)
+- [0013-list](rfcs/0013-list.md)

rfc/src/rfcs/0012-list.md → rfc/src/rfcs/0013-list.md

@@ -2,7 +2,7 @@
 - **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
+- **Version:** 1
 
 -------------------
 
@@ -20,18 +20,18 @@ 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.
+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=[pretty|json]`, which changes the output format. The default is `pretty`, 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
+### Pretty Format
 
-The default format, `human`, will print the harnesses and contracts in a project, along with the total counts of each.
+The default format, `pretty`, will print the harnesses and contracts in a project, along with the total counts of each.
 
 For example:
 
 ```
-Kani Version: 0.5.4
+Kani Rust Verifier 0.54.0 (standalone)
 
 Standard Harnesses:
 - example::verify::check_new
@@ -66,18 +66,22 @@ Totals:
 
 A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness.
 
+All sections will be present in the output, regardless of the result. If a list is empty, Kani will output a `NONE` string.
+
 ### 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. 
+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 file version. The file version 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.
+The JSON format will contain the same information as the pretty format, with the addition of file paths and file version.
+The file version will use semantic versioning.
+This way, any users relying on this format for their scripts can detect when we've released a new major version and update their logic accordingly.
 
 For example:
 
 ```json
 {
-    kani-version: 0.5.4,
-    file-version: 0,
+    kani-version: 0.54,
+    file-version: 0.1,
     standard-harnesses: [
         {
             file: /Users/johnsmith/example/kani_standard_proofs.rs
@@ -132,6 +136,9 @@ For example:
 }
 ```
 
+All sections will be present in the output, regardless of the result.
+If there is no result for a given field (e.g., there are no contracts), Kani will output an empty list (or zero for totals).
+
 ## Software Design
 
 We will add a new subcommand to `kani-driver`.