List RFC revisions

rfc/src/rfcs/0012-list.md

@@ -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 Version: 0.54
 
 Standard Harnesses:
 - example::verify::check_new
@@ -66,17 +66,37 @@ Totals:
 
 A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness.
 
+#### Output Schema
+The formal output schema is:
+```
+Kani Version: float
+Standard Harnesses: List[function] | NONE
+    - function: string
+Contract Harnesses: List[function] | NONE
+    - function: string
+Contracts: Map[function -> contract_harnesses]
+    - function: string
+    - contract_harnesses: List[string] | NONE
+Totals: Map[string -> int]
+    - Standard Harnesses: int
+    - Contract Harnesses: int
+    - Functions with Contracts: int
+    - Contracts: int
+```
+
+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 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,
+    kani-version: 0.54,
     file-version: 0,
     standard-harnesses: [
         {
@@ -132,6 +152,30 @@ For example:
 }
 ```
 
+#### Output Schema
+The formal output schema is:
+```
+Kani Version: float
+File Version: int
+Standard Harnesses: List[Object]
+    - file: string
+    - harnesses: List[string]
+Contract Harnesses: List[Object]
+    - file: string
+    - harnesses: List[string]
+Contracts: List[Object]
+    - function: string
+    - file: string
+    - harnesses: List[string]
+Totals: Object
+    - standard-harnesses: int
+    - contract-harnesses: int
+    - functions-with-contracts: int
+    - contracts: int
+```
+
+All sections will be present in the output, regardless of the result.
+
 ## Software Design
 
 We will add a new subcommand to `kani-driver`.