Lightly revise the rest of the documentation (rust-lang#1396)

docs/src/SUMMARY.md

@@ -3,9 +3,7 @@
 - [Getting started](./getting-started.md)
   - [Installation](./install-guide.md)
     - [Building from source](./build-from-source.md)
-  - [Usage](./usage.md)
-    - [On a single file](./kani-single-file.md)
-    - [On a package](./cargo-kani.md)
+  - [Using Kani](./usage.md)
   - [Verification results](./verification-results.md)
 
 - [Tutorial](./kani-tutorial.md)

docs/src/build-from-source.md

@@ -29,15 +29,15 @@ cd kani
 git submodule update --init
 ./scripts/setup/ubuntu/install_deps.sh
 ./scripts/setup/ubuntu/install_cbmc.sh
-./scripts/setup/install_viewer.sh 3.5
-./scripts/setup/install_rustup.sh
+./scripts/setup/install_viewer.sh
 # If you haven't already:
+./scripts/setup/install_rustup.sh
 source $HOME/.cargo/env
 ```
 
 ### Install dependencies on macOS
 
-Support is available for macOS 10.15. You need to have [Homebrew](https://brew.sh/) installed already.
+Support is available for macOS 10.15+. You need to have [Homebrew](https://brew.sh/) installed already.
 
 ```
 # git clone git@github.com:model-checking/kani.git
@@ -46,9 +46,9 @@ cd kani
 git submodule update --init
 ./scripts/setup/macos-10.15/install_deps.sh
 ./scripts/setup/macos-10.15/install_cbmc.sh
-./scripts/setup/install_viewer.sh 3.5
-./scripts/setup/install_rustup.sh
+./scripts/setup/install_viewer.sh
 # If you haven't already:
+./scripts/setup/install_rustup.sh
 source $HOME/.cargo/env
 ```
 
@@ -74,7 +74,7 @@ All Kani regression tests completed successfully.
 
 ## Adding Kani to your path
 
-To use Kani from anywhere, add the Kani scripts to your path:
+To use a locally-built Kani from anywhere, add the Kani scripts to your path:
 
 ```bash
 export PATH=$(pwd)/scripts:$PATH

docs/src/cargo-kani.md

@@ -1,32 +1,3 @@
 # Usage on a package
 
-Kani is also integrated with `cargo` and can be invoked from a crate directory as follows:
-
-```bash
-cargo kani [<kani-args>]*
-```
-
-`cargo kani` supports all `kani` arguments.
-
-`cargo kani` is the recommended approach for using Kani on a project, due to its
-ability to handle external dependencies and the option add configurations via the `Cargo.toml` file.
-
-If your proof harness is placed under `tests/`, you will need to run
-`cargo kani` with the `--tests` for Kani to be able to find your
-harness.
-
-## Configuration
-
-Users can add a default configuration to the `Cargo.toml` file for running harnesses in a package.
-Kani will extract any arguments from these sections:
- * `[kani]`
- * `[workspace.metadata.kani]`
- * `[package.metadata.kani]`
-
-For example, say you want to set a loop unwinding bound of `5` for all the harnesses in a package.
-You can achieve this by adding the following lines to the package's `Cargo.toml`:
-
-```toml
-[package.metadata.kani]
-flags = { default-unwind = "5" }
-```
+[See here](./usage.md#usage-on-a-package)

docs/src/getting-started.md

@@ -2,17 +2,20 @@
 
 Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs.
 Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked by the compiler.
-Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows).
+Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows).
 Kani can also prove custom properties provided in the form of user-specified assertions.
 
-Kani uses proof harnesses to analyze programs. Proof harnesses are similar to test harnesses, especially property-based test harnesses.
+Kani uses proof harnesses to analyze programs.
+Proof harnesses are similar to test harnesses, especially property-based test harnesses.
 
 ## Project Status
 
-Kani is currently under active development. Releases are published [here](https://github.com/model-checking/kani/releases).
+Kani is currently under active development.
+Releases are published [here](https://github.com/model-checking/kani/releases).
 There is support for a fair amount of Rust language features, but not all (e.g., concurrency).
 Please see [Limitations - Rust feature support](./rust-feature-support.md) for a detailed list of supported features.
 
-Kani usually synchronizes with the nightly release of Rust every two weeks, and so is generally up-to-date with the latest Rust language features.
+Kani releases every two weeks.
+As part of every release, Kani will synchronize with a recent nightly release of Rust, and so is generally up-to-date with the latest Rust language features.
 
 If you encounter issues when using Kani, we encourage you to [report them to us](https://github.com/model-checking/kani/issues/new/choose).

docs/src/kani-single-file.md

@@ -1,40 +1,3 @@
 # Usage on a single file
 
-For small examples or initial learning, it's very common to run Kani on just one source file.
-
-The command line format for invoking Kani directly is the following:
-
-```
-kani filename.rs [<kani-args>]*
-```
-
-For example,
-
-```
-kani example.rs
-```
-
-runs Kani on all the proof harnesses from file `example.rs`.
-A proof harness is simply a function with the `#[kani::proof]` annotation.
-
-## Common arguments
-
-The most common `kani` arguments are the following:
-
- * `--harness <name>`: By default, Kani checks all proof harnesses it finds. You
-   can switch to checking a single harness using this flag.
-
- * `--default-unwind <n>`: Set a global upper [loop
-   unwinding](./tutorial-loop-unwinding.md) bound on all loops. This can force
-   termination when CBMC tries to unwind loops indefinitely.
-
- * `--output-format <regular|terse|old>`: By default (`regular`), Kani
-   post-processes CBMC's output to produce more comprehensible results. In
-   contrast, `terse` outputs only a summary of these results, and `old` forces
-   Kani to emit the original output from CBMC.
-
- * `--visualize`: Generates an HTML report in the local directory accessible
-   through `report/html/index.html`. This report shows coverage information and
-   provides traces (i.e., counterexamples) for each failure found by Kani.
-
-Run `kani --help` to see a complete list of arguments.
+[See here](./usage.md#usage-on-a-single-crate)

docs/src/tool-comparison.md

@@ -16,7 +16,7 @@ Property testing is often quite effective, but the engine can't fully prove the
 **Model checking** is similar to these techniques in how you use them, but it's non-random and exhaustive (though often only up to some bound on input or problem size).
 Thus, properties checked with a model checker are effectively proofs.
 Instead of naively trying all possible _concrete_ inputs (which could be infeasible and blow up exponentially), model checkers like Kani will cleverly encode program traces as _symbolic_ "[SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem)/[SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)" problems, and hand them off to SAT/SMT solvers.
-Again, SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but most practical programs can be model- checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!)
+SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but many practical programs can be model-checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!)
 
 Model checking allows you to prove non-trivial properties about programs, and check those proofs in roughly the same amount of time as a traditional test suite would take to run.
 The downside is many types of properties can quickly become "too large" to practically model-check, and so writing "proof harnesses" (very similar to property tests and fuzzer harnesses) requires some skill to understand why the solver is not terminating and fix the structure of the problem you're giving it so that it does.

docs/src/tutorial-real-code.md

@@ -40,12 +40,12 @@ Sometimes the best place to start won't be your code, but the code that you depe
 If it's used by more projects that just yours, it will be valuable to more people, too!
 
 3. Find well-tested code.
-Code structure changes to make code more unit-testable will make it more provable, too.
+When you make changes to improve the unit-testability of code, that also makes it more amenable to proof, too.
 
 Here are some things to avoid, when starting out:
 
 1. Lots of loops, or at least nested loops.
-As we saw in the last section, right now we often need to put upper bounds on these to make more limited claims.
+As we saw in the [tutorial](./tutorial-loop-unwinding.md), right now we often need to put upper bounds on loops to make more limited claims.
 
 2. Inductive data structures.
 These are data structures with unbounded size (e.g., linked lists or trees.)
@@ -73,12 +73,21 @@ A first proof will likely start in the following form:
 
 Running Kani on this simple starting point will help figure out:
 
-1. What unexpected constraints might be needed on your inputs to avoid "expected" failures.
-2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because now you've over-constrained the inputs.
+1. What unexpected constraints might be needed on your inputs (using `kani::assume`) to avoid "expected" failures.
+2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs).
 3. Whether Kani will support all the Rust features involved.
 4. Whether you've started with a tractable problem.
-(If the problem is initially intractable, try `--default-unwind 1` and see if you can follow the techniques in the previous section to put a bound on the problem.)
+(Remember to try setting `#[kani::unwind(1)]` to force early termination and work up from there.)
 
-Once you've got something working, the next step is to prove more interesting properties than what Kani covers by default.
+Once you've got something working, the next step is to prove more interesting properties than just what Kani covers by default.
 You accomplish this by adding new assertions (not just in your harness, but also to the code being run).
 Even if a proof harness has no post-conditions being asserted directly, the assertions encountered along the way can be meaningful proof results by themselves.
+
+
+## Examples of the use of Kani
+
+On the [Kani blog](https://model-checking.github.io/kani-verifier-blog/), we've documented worked examples of applying Kani:
+
+1. [The `Rectangle` example of the Rust Book](https://model-checking.github.io/kani-verifier-blog/2022/05/04/announcing-the-kani-rust-verifier-project.html)
+2. [A Rust standard library CVE](https://model-checking.github.io/kani-verifier-blog/2022/06/01/using-the-kani-rust-verifier-on-a-rust-standard-library-cve.html)
+3. [Verifying a part of Firecracker](https://model-checking.github.io/kani-verifier-blog/2022/07/13/using-the-kani-rust-verifier-on-a-firecracker-example.html)

docs/src/undefined-behaviour.md

@@ -35,7 +35,7 @@ A non-exhaustive list of these, based on the non-exhaustive list from the [Rust
 * Calling a function with the wrong call ABI or unwinding from a function with the wrong unwind ABI.
     * Kani relies on `rustc` to check for this case.
 * Producing an invalid value, even in private fields and locals. 
-    * Kani provides a [mechanism](./tutorial-nondeterministic-variables.md#safe-nondeterministic-variables-for-custom-types) `is_valid()` which users can use to check validity of objects, but it does not currently apply to all types.
+    * Kani [won't create invalid values](./tutorial-nondeterministic-variables.md) with `kani::any()` but it also won't complain if you `transmute` an invalid value to a Rust type (for example, a `0` to `NonZeroU32`).
 * Incorrect use of inline assembly.
     * Kani does not support inline assembly.
 * Using uninitialized memory.
@@ -46,5 +46,3 @@ Kani makes a best-effort attempt to detect some cases of UB:
     * Kani can detect invalid dereferences, but may not detect them in [place expression context](https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions).
 * Invoking undefined behavior via compiler intrinsics.
     * See [current support for compiler intrinsics](./rust-feature-support/intrinsics.md).
-* Producing an invalid value, even in private fields and locals.
-    * Kani provides a [mechanism](./tutorial-nondeterministic-variables.md#safe-nondeterministic-variables-for-custom-types) `is_valid()` which users can use to check validity of objects, but it does not currently apply to all types.

docs/src/usage.md

@@ -1,12 +1,94 @@
-# Usage
+# Using Kani
 
 At present, Kani can used in two ways:
- * [On a single file](./kani-single-file.md) with the `kani` command.
- * [On a package](./cargo-kani.md) with the `cargo-kani` command.
 
-Running [Kani on a single file](./kani-single-file.md) is quite useful for small
-examples or projects that don't use `cargo`.
+ * [On a single crate](#usage-on-a-single-crate) with the `kani` command.
+ * [On a Cargo package](#usage-on-a-package) with the `cargo kani` command.
 
-However, if you plan to integrate Kani in your projects, the recommended
-approach is to use [Kani on a package](./cargo-kani.md) because of its ability
-to handle external dependencies.
+If you plan to integrate Kani in your projects, the recommended approach is to use `cargo kani`.
+If you're already using cargo, this will handle dependencies automatically, and it can be configured (if needed) in `Cargo.toml`.
+But `kani` is useful for small examples/tests.
+
+## Usage on a package
+
+Kani is integrated with `cargo` and can be invoked from a package as follows:
+
+```bash
+cargo kani [OPTIONS]
+```
+
+This works like `cargo test` except that it will analyze all proof harnesses instead of running all test harnesses.
+
+## Common command line flags
+
+Common to both `kani` and `cargo kani` are many command-line flags:
+
+ * `--visualize`: Generates an HTML report showing coverage information and providing traces (i.e., counterexamples) for each failure found by Kani.
+
+ * `--tests`: Build in "[test mode](https://doc.rust-lang.org/rustc/tests/index.html)", i.e. with `cfg(test)` set and `dev-dependencies` available (when using `cargo kani`).
+
+ * `--harness <name>`: By default, Kani checks all proof harnesses it finds.
+   You can switch to checking a single harness using this flag.
+
+ * `--default-unwind <n>`: Set a default global upper [loop unwinding](./tutorial-loop-unwinding.md) bound for proof harnesses.
+   This can force termination when CBMC tries to unwind loops indefinitely.
+
+Run `cargo kani --help` to see a complete list of arguments.
+
+## Usage on a single crate
+
+For small examples or initial learning, it's very common to run Kani on just one source file.
+The command line format for invoking Kani directly is the following:
+
+```
+kani filename.rs [OPTIONS]
+```
+
+This will build `filename.rs` and run all proof harnesses found within.
+
+## Configuration in `Cargo.toml`
+
+Users can add a default configuration to the `Cargo.toml` file for running harnesses in a package.
+Kani will extract any arguments from these sections:
+
+ * `[workspace.metadata.kani.flags]`
+ * `[package.metadata.kani.flags]`
+
+For example, if you want to set a default loop unwinding bound (when it's not otherwise specified), you can achieve this by adding the following lines to the package's `Cargo.toml`:
+
+```toml
+[package.metadata.kani.flags]
+default-unwind = 1
+```
+
+The options here are the same as on the command line (`cargo kani --help`), and flags (that is, command line arguments that don't take a value) are enabled by setting them to `true`.
+
+## The build process
+
+When Kani builds your code, it does two important things:
+
+1. It sets `cfg(kani)`.
+2. It injects the `kani` crate.
+
+A proof harness (which you can [learn more about in the tutorial](./kani-tutorial.md)), is a function annotated with `#[kani::proof]` much like a test is annotated with `#[test]`.
+But you may experience a similar problem using Kani as you would with `dev-dependencies`: if you try writing `#[kani::proof]` directly in your code, `cargo build` will fail because it doesn't know what the `kani` crate is.
+
+This is why we recommend the same conventions as are used when writing tests in Rust: wrap your proof harnesses in `cfg(kani)` conditional compilation:
+
+```rust
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    #[kani::proof]
+    pub fn check_something() {
+        // ....
+    }
+}
+```
+
+This will ensure that a normal build of your code will be completely unaffected by anything Kani-related.
+
+This conditional compilation with `cfg(kani)` (as seen above) is still required for Kani proofs placed under `tests/`.
+When this code is built by `cargo test`, the `kani` crate is not available, and so it would otherwise cause build failures.
+(Whereas the use of `dev-dependencies` under `tests/` does not need to be gated with `cfg(test)` since that code is already only built when testing.)