remove output schemas; semantic versioning

rfc/src/rfcs/0012-list.md

@@ -31,7 +31,7 @@ The default format, `pretty`, will print the harnesses and contracts in a projec
 For example:
 
 ```
-Kani Version: 0.54
+Kani Rust Verifier 0.54.0 (standalone)
 
 Standard Harnesses:
 - example::verify::check_new
@@ -66,38 +66,22 @@ 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
 
 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 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.
+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.54,
-    file-version: 0,
+    file-version: 0.1,
     standard-harnesses: [
         {
             file: /Users/johnsmith/example/kani_standard_proofs.rs
@@ -152,29 +136,8 @@ 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.
+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