Documentation: Uniform style (model-checking#1016)

* Remove "The" in documentation title

* Use `**NOTE**:` for all notes

* Use "code available here" for links to example files.

* Use `<directory>` as labels for links to directories

* Use more contractions

docs/src/SUMMARY.md

@@ -1,4 +1,4 @@
-# The Kani Rust Verifier
+# Kani Rust Verifier
 
 - [Getting started](./getting-started.md)
   - [Installation](./install-guide.md)

docs/src/bookrunner.md

@@ -20,7 +20,7 @@ Because of that, we run up to three different types of jobs when generating the
 Note that these are incremental: A `verification` job depends on a previous `codegen` job.
 Similary, a `codegen` job depends on a `check` job.
 
-> **NOTE:** [Litani](https://github.com/awslabs/aws-build-accumulator) does not
+> **NOTE**: [Litani](https://github.com/awslabs/aws-build-accumulator) does not
 > support hierarchical views at the moment. For this reason, we are publishing a
 > [text version of the book runner report](./bookrunner/bookrunner.txt) which
 > displays the same results in a hierarchical way while we work on [improvements
@@ -34,7 +34,7 @@ Before running the above mentioned jobs, we pre-process the examples to:
 Finally, we run all jobs, collect their outputs and compare them against the expected outputs.
 The results are summarized as follows: If the obtained and expected outputs differ,
 the color of the stage bar will be red. Otherwise, it will be blue.
-If an example shows one red bar, it is considered a failed example that cannot be handled by Kani.
+If an example shows one red bar, it's considered a failed example that cannot be handled by Kani.
 
 The [book runner report](./bookrunner/index.html) and [its text version](./bookrunner/bookrunner.txt) are
 automatically updated whenever a PR gets merged into Kani.
@@ -49,8 +49,8 @@ To kick off the book runner process use:
 cargo run -p bookrunner
 ```
 
-The main function of the bookrunner is `generate_run()` in
-[`src/tools/bookrunner/src/books.rs`](https://github.com/model-checking/kani/blob/main/tools/bookrunner/src/books.rs),
+The main function of the bookrunner is `generate_run()` (code available
+[here](https://github.com/model-checking/kani/blob/main/tools/bookrunner/src/books.rs))
 which follows these steps:
  1. Sets up all the books, including data about their summaries.
  2. Then, for each book:

docs/src/dev-documentation.md

@@ -14,7 +14,7 @@ developers (including external contributors):
  3. [Development setup recommendations for working with `rustc`](./rustc-hacks.md).
  4. [Guide for testing in Kani](./testing.md).
 
-> **NOTE:** The developer documentation is intended for Kani developers and not
+> **NOTE**: The developer documentation is intended for Kani developers and not
 users. At present, the project is under heavy development and some items
 discussed in this documentation may stop working without notice (e.g., commands
 or configurations). Therefore, we recommend users to not rely on them.

docs/src/install-guide.md

@@ -4,8 +4,8 @@ Kani must currently be built from source.
 
 In general, the following dependencies are required.
 
-> **Note:** These dependencies may be installed by running the CI scripts shown
-> below and there is no need to install them separately, for their respective
+> **NOTE**: These dependencies may be installed by running the CI scripts shown
+> below and there's no need to install them separately, for their respective
 > OS.
 
 1. Cargo installed via [rustup](https://rustup.rs/)
@@ -62,7 +62,7 @@ Then, optionally, run the regression tests:
 ./scripts/kani-regression.sh
 ```
 
-This script has a lot of noisy output, but on a successful run you will see:
+This script has a lot of noisy output, but on a successful run you'll see:
 
 ```
 All Kani regression tests completed successfully.

docs/src/kani-tutorial.md

@@ -1,6 +1,6 @@
 # Tutorial
 
-> Note: This tutorial expects you to have followed the Kani [installation instructions](./install-guide.md) first.
+> **NOTE**: This tutorial expects you to have followed the Kani [installation instructions](./install-guide.md) first.
 
 This tutorial will step you through a progression from simple to moderately complex tasks with Kani.
 It's meant to ensure you can get started, and see at least some simple examples of how typical proofs are structured.

docs/src/regression-testing.md

@@ -16,7 +16,7 @@ The `kani-regression.sh` script executes different testing commands, which we cl
 See below for a description of each one.
 
 Note that regression testing is run whenever a Pull Request is opened, updated or merged
-into the main branch. Therefore, it is a good idea to run regression testing locally before
+into the main branch. Therefore, it's a good idea to run regression testing locally before
 submitting a Pull Request for Kani.
 
 ## Kani testing suites
@@ -33,7 +33,7 @@ Command-line options can be passed to the test by adding a special
 comment to the file. See [testing options](#testing-options) for more details.
 
 In particular, the Kani testing suites are composed of:
- * `kani`: The main testing suite for Kani. The test is a single Rust file that is
+ * `kani`: The main testing suite for Kani. The test is a single Rust file that's
           run through Kani. In general, the test passes if verification with Kani
           is successful, otherwise it fails.
  * `firecracker`: Works like `kani` but contains tests inspired by
@@ -57,7 +57,7 @@ In particular, the Kani testing suites are composed of:
                 Similar to the `expected` suite, we look for `*.expected` files
                 for each harness in the package.
 
-We have extended
+We've extended
 [`compiletest`](https://rustc-dev-guide.rust-lang.org/tests/intro.html) (the
 Rust compiler testing framework) to work with these suites. That way, we take
 advantage of all `compiletest` features (e.g., parallel execution).
@@ -77,7 +77,7 @@ 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 is expected to fail, there are two options to
+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
 
 ```rust,noplaypen
@@ -92,7 +92,7 @@ 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
+> **NOTE**: `kani::expect_fail` is only useful to indicate failure in the
 > `verify` stage, errors in other stages will be considered testing failures.
 
 ### Testing options

docs/src/rust-feature-support.md

@@ -148,9 +148,9 @@ features](#code-generation-for-unsupported-features).
 This results in verification failures if a call to one of these missing functions
 is reachable.
 
-We have done some experiments to embed the standard library into the generated
+We've done some experiments to embed the standard library into the generated
 code, but this causes verification times to increase significantly. As of now,
-we have not been able to find a simple solution for [this
+we've not been able to find a simple solution for [this
 issue](https://github.com/model-checking/kani/issues/581), but we have some
 ideas for future work in this direction. At present, Kani
 [overrides](./overrides.md) a few common functions (e.g., print macros) as
@@ -177,7 +177,7 @@ In particular, there are some outstanding issues to note here:
 We are particularly interested in bug reports concerning
 these features, so please [file a bug
 report](https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md)
-if you are aware of one.
+if you're aware of one.
 
 ### Panic strategies
 

docs/src/rustc-hacks.md

@@ -36,7 +36,7 @@ rustup toolchain install nightly --component rustc-dev
 ### CLion / IntelliJ
 This is not a great solution, but it works for now (see <https://github.com/intellij-rust/intellij-rust/issues/1618>
 for more details).
-Edit the `Cargo.toml` of the package that you are working on and add artificial dependencies on the `rustc` packages that you would like to explore.
+Edit the `Cargo.toml` of the package that you're working on and add artificial dependencies on the `rustc` packages that you would like to explore.
 
 ```toml
 # This configuration doesn't exist so it shouldn't affect your build.
@@ -59,7 +59,7 @@ There are a few reasons why you may want to use your own copy of `rustc`. E.g.:
 
 We will assume that you already have a Kani setup and that the variable `KANI_WORKSPACE` contains the path to your Kani workspace.
 
-**It is highly recommended that you start from the commit that corresponds to the current `rustc` version from your workspace.**
+**It's highly recommended that you start from the commit that corresponds to the current `rustc` version from your workspace.**
 To get that information, run the following command:
 ```bash
 cd ${KANI_WORKSPACE} # Go to your Kani workspace.
@@ -102,4 +102,4 @@ cargo build
 
 In order to enable logs, you can just define the `RUSTC_LOG` variable, as documented here: <https://rustc-dev-guide.rust-lang.org/tracing.html>.
 
-Note that depending on the level of logs you would like to enable, you will need to build your own version of `rustc` as described above.
+Note that depending on the level of logs you would like to enable, you'll need to build your own version of `rustc` as described above.

docs/src/testing.md

@@ -14,5 +14,5 @@ two very good reasons to do it:
     particularly valuable for project management purposes.
 
 We recommend reading our section on [Regression Testing](./regression-testing.md)
-if you are interested in Kani development. At present, we obtain metrics based
+if you're interested in Kani development. At present, we obtain metrics based
 on the [book runner](./bookrunner.md).

docs/src/tool-comparison.md

@@ -13,7 +13,7 @@ Tests in this style do actually state properties: *For all inputs (of some const
 
 Property testing is often quite effective, but the engine can't fully prove the property: It can only sample randomly a few of those values to test (though property testing libraries frequently give interesting "edge cases" a higher probability, making them more effective at bug-finding).
 
-**Model checking** is similar to these techniques in how you use them, but it is non-random and exhaustive (though often only up to some bound on input or problem size).
+**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!)

docs/src/tutorial-first-steps.md

@@ -4,7 +4,7 @@ Kani is unlike the testing tools you may already be familiar with.
 Much of testing is concerned with thinking of new corner cases that need to be covered.
 With Kani, all the corner cases are covered from the start, and the new concern is narrowing down the scope to something manageable for the checker.
 
-Consider this first program (which can be found under [`docs/src/tutorial/kani-first-steps`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/kani-first-steps/)):
+Consider this first program (which can be found under [`kani-first-steps`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/kani-first-steps/)):
 
 ```rust,noplaypen
 {{#include tutorial/kani-first-steps/src/lib.rs:code}}
@@ -99,7 +99,7 @@ warning: dereferencing a null pointer
    = note: `#[warn(deref_nullptr)]` on by default
 ```
 
-Still, it is just a warning, and we can run the code without test failures just as before.
+Still, it's just a warning, and we can run the code without test failures just as before.
 But Kani still catches the issue:
 
 ```
@@ -149,7 +149,7 @@ Let's encode this fact about our function by asserting some reasonable bound on
 {{#include tutorial/kani-first-steps/src/final_form.rs:code}}
 ```
 
-Now we have stated our previously implicit expectation: this function should never be called with inputs that are too big.
+Now we've stated our previously implicit expectation: this function should never be called with inputs that are too big.
 But if we attempt to verify this, we get a problem:
 
 ```

docs/src/tutorial-kinds-of-failure.md

@@ -8,7 +8,7 @@ In this section, we're going to expand on these additional checks, to give you a
 ## Bounds checking and pointers
 
 Rust is safe by default, and so includes dynamic (run-time) bounds checking where needed.
-Consider this Rust code (from [`src/bounds_check.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs)):
+Consider this Rust code (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs)):
 
 ```rust,noplaypen
 {{#include tutorial/kinds-of-failure/src/bounds_check.rs:code}}
@@ -148,7 +148,7 @@ Kani will spot this not as a bound error, but as a mathematical error: on an emp
 1. Exercise: Try to run Kani on the above, to see what this kind of failure looks like.
 
 Rust also performs runtime safety checks for integer overflows, much like it does for bounds checks.
-Consider this code (from [`src/overflow.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow.rs)):
+Consider this code (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow.rs)):
 
 ```rust,noplaypen
 {{#include tutorial/kinds-of-failure/src/overflow.rs:code}}
@@ -175,7 +175,7 @@ For instance, instead of `a + b` write `a.wrapping_add(b)`.
 ### Exercise: Classic overflow failure
 
 One of the classic subtle bugs that persisted in many implementations for a very long time is finding the midpoint in quick sort.
-This often naively looks like this (from [`src/overflow_quicksort.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow_quicksort.rs)):
+This often naively looks like this (code available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/kinds-of-failure/src/overflow_quicksort.rs)):
 
 ```rust,noplaypen
 {{#include tutorial/kinds-of-failure/src/overflow_quicksort.rs:code}}

docs/src/tutorial-loop-unwinding.md

@@ -1,6 +1,6 @@
 # Loops, unwinding, and bounds
 
-Consider code like this (from [`src/lib.rs`](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/loops-unwinding/src/lib.rs)):
+Consider code like this (available [here](https://github.com/model-checking/kani/blob/main/docs/src/tutorial/loops-unwinding/src/lib.rs)):
 
 ```rust,noplaypen
 {{#include tutorial/loops-unwinding/src/lib.rs:code}}
@@ -16,7 +16,7 @@ We can try to find this bug with a proof harness like this:
 When we run Kani on this, we run into an unfortunate result: non-termination.
 This non-termination is caused by CBMC trying to unwind the loop an unlimited number of times.
 
-> **NOTE:** Presently, [due to a bug](https://github.com/model-checking/kani/issues/493), this is especially bad: we don't see any output at all.
+> **NOTE**: Presently, [due to a bug](https://github.com/model-checking/kani/issues/493), this is especially bad: we don't see any output at all.
 > Kani is supposed to emit some log lines that might give some clue that an infinite loop is occurring.
 > If Kani doesn't terminate, it's almost always the problem that this section covers.
 

docs/src/tutorial-nondeterministic-variables.md

@@ -13,14 +13,14 @@ In this tutorial, we will show how to:
 
 ## Safe nondeterministic variables
 
-Let's say you are developing an inventory management tool, and you would like to verify that your API to manage items is correct.
+Let's say you're developing an inventory management tool, and you would like to verify that your API to manage items is correct.
 Here is a simple implementation of this API:
 
 ```rust,noplaypen
 {{#include tutorial/arbitrary-variables/src/inventory.rs:inventory_lib}}
 ```
 
-Now we would like to verify that, no matter which combination of `id` and `quantity`, a call to `Inventory::update()` followed by a call to `Inventory::get()` using the same `id` returns some value that is equal to the one we inserted:
+Now we would like to verify that, no matter which combination of `id` and `quantity`, a call to `Inventory::update()` followed by a call to `Inventory::get()` using the same `id` returns some value that's equal to the one we inserted:
 
 ```rust,noplaypen
 {{#include tutorial/arbitrary-variables/src/inventory.rs:safe_update}}
@@ -32,7 +32,7 @@ In this harness, we use `kani::any()` to generate the new `id` and `quantity`.
 If we run this example, Kani verification will succeed, including the assertion that shows that the underlying `u32` variable  used to represent `NonZeroU32` cannot be zero, per its type invariant:
 
 You can try it out by running the example under
-[arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
+[`arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
 
 ```
 cargo kani --harness safe_update
@@ -57,7 +57,7 @@ The verification will now fail showing that the `inventory.get(&id).unwrap()` me
 This is an interesting issue that emerges from how `rustc` optimizes the memory layout of `Option<NonZeroU32>`.
 The compiler is able to represent `Option<NonZeroU32>` using `32` bits by using the value `0` to represent `None`.
 
-You can try it out by running the example under [arbitrary-variables directory](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
+You can try it out by running the example under [`arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
 
 ```
 cargo kani --harness unsafe_update
@@ -88,7 +88,7 @@ Now you can use `kani::any()` to create valid nondeterministic variables of the
 ```
 
 You can try it out by running the example under
-[`docs/src/tutorial/arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
+[`arbitrary-variables`](https://github.com/model-checking/kani/tree/main/docs/src/tutorial/arbitrary-variables/):
 
 ```
 cargo kani --harness check_rating