Kani RFC Book

• Feature Name: List Subcommand
• Feature Request Issue: #2573, #1612
• RFC PR: #3463
• Status: Under Review
• Version: 1

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=[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.

Pretty Format

The default format, pretty, will print the harnesses and contracts in a project, along with the total counts of each.

For example:

Kani Rust Verifier 0.54.0 (standalone)

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.

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 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_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,
    }
}

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.

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

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.