Kani Book Documentation Improvements (#4296)

Best reviewed commit by commit.

Resolves #4026
Resolves #3999
Resolves #3568
Resolves #2539
Resolves #3041

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Michael Tautschnig <[email protected]>

Author: Carolyn Zech

docs/src/SUMMARY.md

@@ -16,8 +16,10 @@
   - [Nondeterministic variables](./tutorial-nondeterministic-variables.md)
 
 - [Reference](./reference.md)
+  - [Arbitrary Trait](./reference/arbitrary.md)
   - [Attributes](./reference/attributes.md)
   - [Bounded Non-deterministic variables](./reference/bounded_arbitrary.md)
+  - [List Kani Metadata](./reference/list.md)
   - [Experimental features](./reference/experimental/experimental-features.md)
     - [Automatic Harness Generation](./reference/experimental/autoharness.md)
     - [Coverage](./reference/experimental/coverage.md)
@@ -29,6 +31,7 @@
 - [Application](./application.md)
   - [Comparison with other tools](./tool-comparison.md)
   - [Where to start on real code](./tutorial-real-code.md)
+  - [Debugging slow proofs](./debugging-slow-proofs.md)
 
 - [Developer documentation](dev-documentation.md)
   - [Coding conventions](./conventions.md)

docs/src/debugging-slow-proofs.md

@@ -0,0 +1,107 @@
+# Debugging Slow Proofs
+
+Kani uses SAT/SMT solvers to verify code, which can sometimes result in slow or non-terminating proofs. This chapter outlines common causes of slowness and strategies to debug and improve proof performance.
+
+## Common Causes of Slow Proofs
+
+### Complex/Large Non-deterministic Types
+Some types are inherently more expensive to represent symbolically, e.g. strings, which have complex validation rules for UTF-8 encoding,
+or large bounded collections, like a vector with a large size.
+
+### Large Value Operations
+Mathematical operations on large values can be expensive, e.g., multiplication/division/modulo, especially with larger types (e.g., `u64`).
+
+### Unbounded Loops
+If Kani cannot determine a loop bound, it will unwind forever, c.f. [the loop unwinding tutorial](./tutorial-loop-unwinding.md).
+
+## Debugging Strategies
+
+These are some strategies to debug slow proofs, ordered roughly in terms of in the order you should try them:
+
+### Limit Loop Iterations
+
+First, identify whether (unbounded) loop unwinding may be the root cause. Try the `#[kani::unwind]` attribute or the `--unwind` option to limit [loop unwinding](./tutorial-loop-unwinding.md). If the proof fails because the unwind value is too low, but raising it causing the proof to be too slow, try specifying a [loop contract](./reference/experimental/loop-contracts.md) instead.
+
+### Use Different Solvers
+
+Kani supports multiple SAT/SMT solvers that may perform differently on your specific problem. Try out different solvers with the `#[kani::solver]` [attribute](./reference/attributes.md) or `--solver` option.
+
+### Remove Sources of Nondeterminism
+
+Start by replacing `kani::any()` calls with concrete values to isolate the problem:
+
+```rust
+#[kani::proof]
+fn slow_proof() {
+    // Instead of this:
+    // let x: u64 = kani::any();
+    // let y: u64 = kani::any();
+    
+    // Try this:
+    let x: u64 = 42;
+    let y: u64 = 100;
+    
+    let result = complex_function(x, y);
+    assert!(result > 0);
+}
+```
+
+If the proof becomes fast with concrete values, the issue is likely with the symbolic representation of your inputs. In that case, see you can [partition the proof](#partition-the-input-space) to cover different ranges of possible values, or restrict the proof to a smaller range of values if that is acceptable for your use case.
+
+### Reduce Collection Sizes
+
+Similarly, if smaller values are acceptable for your proof, use those instead:
+
+```rust
+#[kani::proof]
+fn test_with_small_collection() {
+    // Instead of a large Vec
+    // let vec: Vec<u8> = kani::bounded_any::<_, 100>();
+    
+    // Start with a small size
+    let vec: Vec<u8> = kani::bounded_any::<_, 2>();
+    
+    process_collection(&vec);
+}
+```
+
+### Partition the Input Space
+
+Break down complex proofs by partitioning the input space:
+
+```rust
+// Instead of one slow proof with large inputs
+#[kani::proof]
+fn test_multiplication_slow() {
+    let x: u64 = kani::any();
+    let y: u64 = kani::any();
+    
+    // This might be too slow for the solver
+    let result = x.saturating_mul(y);
+    assert!(result >= x || x == 0);
+}
+
+// Split into multiple proofs with bounded inputs
+#[kani::proof]
+fn test_multiplication_small_values() {
+    let x: u64 = kani::any_where(|x| *x <= 100);
+    let y: u64 = kani::any_where(|y| *y <= 100);
+    
+    let result = x.saturating_mul(y);
+    assert!(result >= x || x == 0);
+}
+
+// Insert harnesses for other ranges of `x` and `y`
+```
+
+See this [tracking issue](https://github.com/model-checking/kani/issues/3006) for adding support for such partitioning automatically.
+
+### Use Stubs
+
+If a function has a complex body, consider using a [stub](./reference/experimental/stubbing.md) or a [verified stub](./reference/experimental/contracts.md) to stub the body with a simpler abstraction.
+
+### Disable Unnecessary Checks
+
+If you're focusing on functional correctness rather than safety, you may disable memory safety checks (run `kani --help` for a list of options to do so). Note that disabling these checks may cause Kani to miss undefined behavior, so use it with caution.
+
+Alternatively, to assume that all assertions succeed and only focus on finding safety violations, use the `--prove-safety-only` option.

docs/src/kani-tutorial.md

@@ -6,5 +6,7 @@ This tutorial will step you through a progression from simple to moderately comp
 It's meant to ensure you can get started, and see at least some simple examples of how typical proofs are structured.
 It will also teach you the basics of "debugging" proof harnesses, which mainly consists of diagnosing and resolving non-termination issues with the solver.
 
+For a more in-depth overview of Kani's features, see the [Reference](./reference.md) section.
+
 You may also want to read the [Application](./application.md) section to better
 understand what Kani is and how it can be applied on real code.

docs/src/reference/arbitrary.md

@@ -0,0 +1,120 @@
+# Arbitrary Trait
+
+The `Arbitrary` trait is the foundation for generating non-deterministic values in Kani proof harnesses. It allows you to create symbolic values that represent all possible values of a given type.
+
+For a type to implement `Arbitrary`, Kani must be able to represent every possible value of it, so unbounded types cannot implement it. For nondeterministic representations of unbounded types, e.g., `Vec`, see the [`BoundedArbitrary` trait](./bounded_arbitrary.md).
+
+## Overview
+
+The `Arbitrary` trait defines methods for generating arbitrary (nondeterministic) values:
+
+```rust
+pub trait Arbitrary
+where
+    Self: Sized,
+{
+    fn any() -> Self;
+    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
+        [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
+    }
+}
+```
+
+## Basic Usage
+
+Use `kani::any()` to generate arbitrary values in proof harnesses:
+
+```rust
+#[kani::proof]
+fn verify_function() {
+    let x: u32 = kani::any();
+    let y: bool = kani::any();
+    let z: [char; 10] = kani::any();
+    
+    // x represents all possible u32 values
+    // y represents both true and false
+    // z represents an array of length 10 where each element can hold all possible char values
+    my_function(x, y, z);
+}
+```
+
+Kani implements `Arbitrary` for primitive types and some standard library types. See the [crate trait documentation](https://model-checking.github.io/kani/crates/doc/kani/trait.Arbitrary.html#foreign-impls) for a full list of implementations. 
+
+## Constrained Values
+
+Use `any_where` or `kani::assume()` to add constraints to arbitrary values:
+
+```rust
+#[kani::proof]
+fn verify_with_constraints() {
+    let x: u32 = kani::any_where(|t| *t < 1000); // Constrain x to be less than 1000
+    kani::assume(x % 2 == 0); // Constrain x to be even
+    
+    // Now x represents all even numbers from 0 to 998
+    my_function(x);
+}
+
+## Derive Implementations
+
+Kani can automatically derive `Arbitrary` implementations for structs and enums when all their fields/variants implement `Arbitrary`:
+
+### Structs
+
+```rust
+#[derive(kani::Arbitrary)]
+struct Point {
+    x: i32,
+    y: i32,
+}
+
+#[kani::proof]
+fn verify_point() {
+    let point: Point = kani::any();
+    // point.x and point.y can be any i32 values
+    process_point(point);
+}
+```
+
+### Enums
+
+```rust
+#[derive(kani::Arbitrary)]
+enum Status {
+    Ready,
+    Processing(u32),
+    Error { code: (char, i32) },
+}
+
+#[kani::proof]
+fn verify_status() {
+    let status: Status = kani::any();
+    // `status` can be any of the variants
+    match status {
+        Status::Ready => { /* ... */ }
+        Status::Processing(id) => { /* id can be any u32 */ }
+        Status::Error { code } => { /* code can be any (char, i32) tuple */ }
+    }
+}
+```
+
+## Manual Implementations
+
+Implement `Arbitrary` manually when you need constraints or custom logic. For example, Kani [manually implements `Arbitrary` for `NonZero` types](https://github.com/model-checking/kani/blob/100857e99d7506992c4589332a0d7d8dae1ee29a/library/kani_core/src/arbitrary.rs#L48-L60) to exclude zero values, e.g:
+
+```rust
+impl Arbitrary for NonZeroU8 {
+    fn any() -> Self {
+        let val = u8::any();
+        kani::assume(val != 0);
+        unsafe { NonZeroU8::new_unchecked(val) }
+    }
+}
+```
+
+An alternative means to add value constraints is provided by the [Invariant trait](https://model-checking.github.io/kani/crates/doc/kani/invariant/trait.Invariant.html).
+
+## See Also
+
+- [Nondeterministic Variables Tutorial](../tutorial-nondeterministic-variables.md)
+- [Bounded Non-deterministic Variables](./bounded_arbitrary.md)
+- [First Steps Tutorial](../tutorial-first-steps.md)

docs/src/reference/attributes.md

@@ -9,6 +9,7 @@ At present, the available Kani attributes are the following:
  - [`#[kani::unwind(<number>)]`](#kaniunwindnumber)
  - [`#[kani::solver(<solver>)]`](#kanisolversolver)
  - [`#[kani::stub(<original>, <replacement>)]`](#kanistuboriginal-replacement)
+ - [Contract-related attributes](#contract-attributes)
 
 ## `#[kani::proof]`
 
@@ -239,3 +240,14 @@ default one.
 **Replaces the function/method with name <original> with the function/method with name <replacement> during compilation**
 
 Check the [*Stubbing* section](../reference/stubbing.md) for more information about stubbing.
+
+## Contract Attributes
+
+There are numerous attributes for function and loop contracts. At present, these are:
+
+- Proof harness for contracts: `#[kani::proof_for_contract(name-of-function)]`
+- Verified stubbing: `#[kani::stub_verified]`
+- Function contract specification: `#[kani::requires]`, `#[kani::modifies]`, `#[kani::ensures]`, `#[kani::recursion]`
+- Loop contract specification: `#[kani::loop_invariant]`, `#[kani::loop_modifies]`.
+
+See the documentation on [function contracts](./experimental/contracts.md) and [loop contracts](./experimental/loop-contracts.md) for details.

docs/src/reference/experimental/autoharness.md

@@ -75,6 +75,10 @@ Note that because Kani prefixes function paths with the crate name, some pattern
 For example, given a function `foo_top_level` inside crate `my_crate`, the regex `.*::foo_.*` will match `foo_top_level`, since Kani interprets it as `my_crate::foo_top_level`.
 To match only `foo_` functions inside modules, use a more specific pattern, e.g. `.*::[^:]+::foo_.*`.
 
+Autoharness also accepts a `--list` argument, which runs the [list subcommand](../list.md) including automatic harnesses.
+
+For a full list of options, run `kani autoharness --help`.
+
 ## Example
 Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:
 ```rust

docs/src/reference/list.md

@@ -0,0 +1,52 @@
+# List Command
+
+The `list` subcommand provides an overview of harnesses and contracts in the provided project/file. This is useful for understanding which parts of your codebase have verification coverage and tracking verification progress.
+
+## Usage
+For basic usage, run `cargo kani list` or `kani list <FILE>`. The current options are:
+- `--format [pretty|markdown|json]`: Choose output format
+- `--std`: List harnesses and contracts in the standard library (standalone `kani` only)
+
+The default format is `pretty`, which prints a table to the terminal, e.g:
+
+```
+Kani Rust Verifier 0.65.0 (standalone)
+
+Contracts:
++-------+----------+-------------------------------+----------------------------------------------------------------+
+|       | Crate    | Function                      | Contract Harnesses (#[kani::proof_for_contract])               |
++=================================================================================================================+
+|       | my_crate | example::implementation::bar  | example::verify::check_bar                                     |
+|-------+----------+-------------------------------+----------------------------------------------------------------|
+|       | my_crate | example::implementation::foo  | example::verify::check_foo_u32, example::verify::check_foo_u64 |
+|-------+----------+-------------------------------+----------------------------------------------------------------|
+|       | my_crate | example::implementation::func | example::verify::check_func                                    |
+|-------+----------+-------------------------------+----------------------------------------------------------------|
+|       | my_crate | example::prep::parse          | NONE                                                           |
+|-------+----------+-------------------------------+----------------------------------------------------------------|
+| Total |          | 4                             | 4                                                              |
++-------+----------+-------------------------------+----------------------------------------------------------------+
+
+Standard Harnesses (#[kani::proof]):
++-------+----------+-------------------------------+
+|       | Crate    | Harness                       |
++==================================================+
+|       | my_crate | example::verify::check_modify |
+|-------+----------+-------------------------------|
+|       | my_crate | example::verify::check_new    |
+|-------+----------+-------------------------------|
+| Total |          | 2                             |
++-------+----------+-------------------------------+
+```
+
+The "Contracts" table shows functions that have contract attributes (`#[requires]`, `#[ensures]`, or `modifies`), and which harnesses exist for those functions.
+The "Standard Harnesses" table lists all of the `#[kani::proof]` harnesses found.
+
+The `markdown` and `json` options write the same information to Markdown or JSON files, respectively.
+
+For `--std`, ensure that the provided path points to a local copy of the standard library, e.g. `kani list --std rust/library`. (Compiling the standard library [works differently](https://doc.rust-lang.org/cargo/reference/unstable.html#build-std) than compiling a normal Rust project, hence the separate option).
+
+For a full list of options, run `kani list --help`. 
+
+## Autoharness
+Note that by default, this subcommand only detects manual harnesses. The [experimental autoharness feature](./experimental/autoharness.md) accepts a `--list` argument, which runs this subcommand for both manual harnesses and automatically generated harnesses.

docs/src/regression-testing.md

@@ -68,6 +68,8 @@ We've extended
 Rust compiler testing framework) to work with these suites. That way, we take
 advantage of all `compiletest` features (e.g., parallel execution).
 
+A good rule of thumb is to put a test in the `kani` or `cargo-kani` folders if all we care about is codegen and verification succeeding. This is usually the case if we're fixing a code pattern that previously crashed, so a successful verification result is a sufficient test. Otherwise, if the output refers to UI, e.g., a compiler error with a highlighted span, put it in the `ui` or `cargo-ui` suites. If the output is for a CBMC-based property that we expect Kani to check (e.g., ensuring that a particular assertion passes or fails), use the `expected` folder. 
+
 ### Testing stages
 
 The process of running single-file tests is split into three stages:
@@ -83,23 +85,15 @@ If a test fails, the error message will include the stage where it failed:
 error: test failed: expected check success, got failure
 ```
 
-When working on a test that's expected to fail, there are two options to
-indicate an expected failure. The first one is to add a comment
+Some tests have the following, historical syntax:
 
 ```rust
 // kani-<stage>-fail
 ```
 at the top of the test file, where `<stage>` is the stage where the test is
 expected to fail.
 
-The other option is to use the predicate `kani::expect_fail(cond, message)`
-included in the Kani library. The `cond` in `kani::expect_fail` is a condition
-that you expect not to hold during verification. The testing framework expects
-one `EXPECTED FAIL` message in the verification output for each use of the
-predicate.
-
-> **NOTE**: `kani::expect_fail` is only useful to indicate failure in the
-> `verify` stage, errors in other stages will be considered testing failures.
+We retain support for this test format, but prefer `expected` tests, since they more precisely indicate which failure we expect, rather than a general verification or codegen failure.
 
 ### Testing options
 

docs/src/rust-feature-support.md

@@ -176,11 +176,8 @@ stack unwinding support.
 
 Reading uninitialized memory is
 [considered undefined behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html#behavior-considered-undefined) in Rust.
-At the moment, Kani cannot detect if memory is uninitialized, but in practice
-this is mitigated by the fact that all memory is initialized with
-nondeterministic values.
-Therefore, any code that depends on uninitialized data will exhibit nondeterministic behavior.
-See [this issue](https://github.com/model-checking/kani/issues/920) for more details.
+Kani has partial, experimental support for detecting access to uninitialized memory with the `-Z uninit-checks` option.
+See [this issue](https://github.com/model-checking/kani/issues/3300) for more details.
 
 ### Destructors