• Feature Name: List Subcommand
  • Feature Request Issue: #2573, #1612
  • RFC PR: #3463
  • Status: Unstable
  • Version: 2

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 takes two options:

  • --message-format=[pretty|json]: choose the output format. The default is pretty, which prints to the terminal. The json option creates and writes to a JSON file instead.
  • --std: this option should be specified when listing the harnesses and contracts in the standard library. This option is only available for kani list (not cargo kani list), which mirrors the verification workflow for the standard library.

This subcommand does not fail. In the case that it does not find any harnesses or contracts, it prints a message informing the user of that fact.

Pretty Format

The default format, pretty, prints a "Contracts" table and a "Standard Harnesses" list. Each row of the "Contracts" table consists of a function under contract and its contract harnesses. The results are printed in lexicographic order.

For example:

Kani Rust Verifier 0.54.0 (standalone)

Contracts:
|-------|-------------------------|--------------------------------------------------|
|       | Function                | Contract Harnesses (#[kani::proof_for_contract]) |
|-------|-------------------------|--------------------------------------------------|
|       | example::impl::bar      | example::verify::check_bar                       |
|-------|-------------------------|--------------------------------------------------|
|       | example::impl::baz      | example::verify::check_baz                       |
|-------|-------------------------|--------------------------------------------------|
|       | example::impl::foo      | example::verify::check_foo_u32                   |
|       |                         | example::verify::check_foo_u64                   |
|-------|-------------------------|--------------------------------------------------|
|       | example::impl::func     | example::verify::check_func                      |
|-------|-------------------------|--------------------------------------------------|
|       | example::prep::parse    | NONE                                             |
|-------|-------------------------|--------------------------------------------------|
| Total | 5                       | 5                                                |
|-------|-------------------------|--------------------------------------------------|

Standard Harnesses (#[kani::proof]):
1. example::verify::check_modify
2. example::verify::check_new

All sections will be present in the output, regardless of the result. If there are no harnesses for a function under contract, Kani inserts NONE in the "Contract Harnesses" column. If the "Contracts" section is empty, Kani prints a message that "No contracts or contract harnesses were found." If the "Standard Harnesses" section is empty, Kani prints a message that "No standard harnesses were found."

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 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:

{
    kani-version: 0.54,
    file-version: 0.1,
    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_baz,
                example::verify::check_foo_u32,
                example::verify::check_foo_u64, 
                example::verify::check_func 
            ]
        },
    ],
    contracts: [
        {
            function: example::impl::bar
            file: /Users/johnsmith/example/impl.rs
            harnesses: [example::verify::check_bar]
        },
        {
            function: example::impl::baz
            file: /Users/johnsmith/example/impl.rs
            harnesses: [example::verify::check_baz]
        },
        {
            function: example::impl::foo
            file: /Users/johnsmith/example/impl.rs
            harnesses: [
                example::verify::check_foo_u32,
                example::verify::check_foo_u64
            ]
        },
        {
            function: example::impl::func
            file: /Users/johnsmith/example/impl.rs
            harnesses: [example::verify::check_func]
        },
        {
            function: example::prep::parse
            file: /Users/johnsmith/example/prep.rs
            harnesses: []
        }
    ],
    totals: {
        standard-harnesses: 2,
        contract-harnesses: 5,
        functions-with-contracts: 5,
    }
}

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

Driver/Metdata Changes

We add a new list subcommand to kani-driver, which invokes the compiler to collect metadata, then post-processes that metadata and outputs the result. We extend KaniMetadata to include a new field containing each function under contract and its contract harnesses.

Compiler Changes

In codegen_crate, we update the generation of KaniMetadata to include the new contracts information. We iterate through each local item in the crate. Each time we find a function under contract or a contract harness, we include it in the metadata.

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 functions under contract 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.

The Contracts table is close to Markdown, but not quite Markdown--it includes line separators between each row, when Markdown would only have a separator for the header. We include the separator because without it, it can be difficult to tell from reading the terminal output which entries are in the same row. The user can transform the table to Markdown by deleting these separators, and we can trivially add a Markdown option in the future if there is demand for it.

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 or the number of 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.
  3. Do we want to add a filtering option? For instance, --harnesses <pattern> and --contracts <pattern>, where pattern corresponds to a Rust-style path. For example, kani list --harnesses "my_crate::my_module::*" would include all harnesses with that path prefix, while kani list --contracts "my_crate::my_module::*" would include all functions under contract with that path prefix. (If we do this work, we could use it to improve our --harness pattern handling for verification).

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.:

#[cfg_attr(kani, kani::proof)]
fn check() {
    bolero::check!()...
}

See this blog post 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.