Documentation: Uniform style

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/application.md

@@ -1,12 +1,12 @@
 # Application
 
-You may be interested in applying Kani if you're in this situation:
+You may be interested in applying Kani if you are in this situation:
 
-1. You're working on a moderately important project in Rust.
-2. You've already invested heavily in testing to ensure correctness.
+1. You are working on a moderately important project in Rust.
+2. You have already invested heavily in testing to ensure correctness.
 3. You want to invest further, to gain a much higher degree of assurance.
 
-> If you haven't already, we recommend techniques like property testing (e.g. with [`proptest`](https://github.com/AltSysrq/proptest)) before attempting model checking.
+> If you have not already, we recommend techniques like property testing (e.g. with [`proptest`](https://github.com/AltSysrq/proptest)) before attempting model checking.
 > These yield good results, are very cheap to apply, and are often easier to adopt and debug.
 > Kani is a next step: a tool that can be applied once cheaper tactics are no longer yielding results, or once the easier to detect issues have already been dealt with.
 

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
@@ -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:
@@ -67,7 +67,7 @@ which follows these steps:
 > In general, the path to a given example is
 > `src/test/bookrunner/books/<book>/<chapter>/<section>/<subsection>/<line>.rs`
 > where `<line>` is the line number where the example appears in the markdown
-> file where it's written. The `.props` files mentioned above follow the same
+> file where it is written. The `.props` files mentioned above follow the same
 > naming scheme in order to match them and detect conflicts.
 
  3. Runs all examples using

docs/src/cheat-sheets.md

@@ -96,15 +96,15 @@ As a result:
  1. The title of your pull request will become the main commit message.
  2. The messages from commits in your pull request will appear by default as a bulleted list in the main commit message body.
 
-But the main commit message body is editable at merge time, so you don't have to worry about "typo fix" messages because these can be removed before merging.
+But the main commit message body is editable at merge time, so you do not have to worry about "typo fix" messages because these can be removed before merging.
 
 ```bash
 # Set up your git fork
 git remote add fork git@github.com:${USER}/kani.git
 ```
 
 ```bash
-# Reset everything. Don't have any uncommitted changes!
+# Reset everything. Do not have any uncommitted changes!
 git clean -xffd
 git submodule foreach --recursive git clean -xffd
 git submodule update --init
@@ -124,7 +124,7 @@ cargo build
 git fetch origin
 git merge origin/main
 # Or rebase, but that requires a force push,
-# and because we squash and merge, an extra merge commit in a PR doesn't hurt.
+# and because we squash and merge, an extra merge commit in a PR does not hurt.
 ```
 
 ```bash

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/getting-started.md

@@ -7,7 +7,7 @@ tests).
 
 Kani is particularly useful for verifying unsafe code in Rust, where
 many of the language's usual guarantees can no longer be checked by the
-compiler. But it's also useful for finding panics and check user-defined
+compiler. But it is also useful for finding panics and check user-defined
 assertions in safe Rust.
 
 ## Project Status

docs/src/install-guide.md

@@ -4,7 +4,7 @@ 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
+> **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
 > OS.
 
@@ -17,7 +17,7 @@ Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##
 ## Install dependencies on Ubuntu
 
 Support is available for Ubuntu 18.04 and 20.04.
-The simplest way to install dependencies (especially if you're using a fresh VM)
+The simplest way to install dependencies (especially if you are using a fresh VM)
 is following our CI scripts:
 
 ```

docs/src/kani-single-file.md

@@ -1,6 +1,6 @@
 # Usage on a single file
 
-For small examples or initial learning, it's very common to run Kani on just one source file.
+For small examples or initial learning, it is very common to run Kani on just one source file.
 
 The command line format for invoking Kani directly is the following:
 

docs/src/kani-tutorial.md

@@ -1,9 +1,9 @@
 # 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.
+It is 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.
 
 You may also want to read the [Application](./application.md) section to better

docs/src/limitations.md

@@ -1,8 +1,8 @@
 # Limitations
 
 Like other tools, Kani comes with some limitations. In some cases, these
-limitations are inherent because of the techniques it's based on. In other
-cases, it's just a matter of time and effort to remove these limitations (e.g.,
+limitations are inherent because of the techniques it is based on. In other
+cases, it is just a matter of time and effort to remove these limitations (e.g.,
 specific unsupported Rust language features).
 
 In this chapter, we do the following to document these limitations:

docs/src/regression-testing.md

@@ -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/rustc-hacks.md

@@ -39,7 +39,7 @@ 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.
 
 ```toml
-# This configuration doesn't exist so it shouldn't affect your build.
+# This configuration does not exist so it should not affect your build.
 [target.'cfg(KANI_DEV)'.dependencies]
 # Adjust the path here to point to a local copy of the rust compiler.
 # The best way is to use the rustup path. Replace <toolchain> with the
@@ -48,7 +48,7 @@ rustc_driver = { path = "~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/
 rustc_interface = { path = "~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/rust/compiler/rustc_interface" }
 ```
 
-**Don't forget to rollback the changes before you create your PR.**
+**Do not forget to rollback the changes before you create your PR.**
 
 ## Custom `rustc`
 

docs/src/tool-comparison.md

@@ -1,7 +1,7 @@
 # Comparison with other tools
 
 **Fuzzing** (for example, with [`cargo-fuzz`](https://github.com/rust-fuzz/cargo-fuzz)) is a unguided approach to random testing.
-A fuzzer generally provides an input of random bytes, and then examines fairly generic properties (such as "doesn't crash" or "commit undefined behavior") about the resulting program.
+A fuzzer generally provides an input of random bytes, and then examines fairly generic properties (such as "does not crash" or "commit undefined behavior") about the resulting program.
 
 Fuzzers generally get their power through a kind of evolutionary algorithm that rewards new mutant inputs that "discover" new branches of the program under test.
 Fuzzers are excellent for testing security boundaries, precisely because they make no validity assumptions (hence, they are "unguided") when generating the input.
@@ -11,15 +11,15 @@ Fuzzers are excellent for testing security boundaries, precisely because they ma
 The purpose of this strategy is to either focus on interesting values, or avoid failing assertions that only hold for a constrained set of inputs.
 Tests in this style do actually state properties: *For all inputs (of some constrained kind), this condition should hold*.
 
-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).
+Property testing is often quite effective, but the engine cannot 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).
 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!)
 
 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.
+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 are giving it so that it does.
 This process basically boils down to "debugging" the proof.
 
 ## Looking for concurrency?

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}}
@@ -15,7 +15,7 @@ You would need figure out a whole set of arguments to call the function with tha
 You would also need to keep that test harness up-to-date with the code, in case some of the branches change.
 And if this function was more complicated—for example, if some of the branches depended on global state—the test harness would be even more onerous to write.
 
-We can try to property test a function like this, but if we're naive about it (and consider all possible `u32` inputs), then it's unlikely we'll ever find the bug.
+We can try to property test a function like this, but if we are naive about it (and consider all possible `u32` inputs), then it is unlikely we will ever find the bug.
 
 ```rust,noplaypen
 {{#include tutorial/kani-first-steps/src/lib.rs:proptest}}
@@ -27,7 +27,7 @@ We can try to property test a function like this, but if we're naive about it (a
 test tests::doesnt_crash ... ok
 ```
 
-There's only 1 in 4 billion inputs that fail, so it's vanishingly unlikely the property test will find it, even with a million samples.
+There is only 1 in 4 billion inputs that fail, so it is vanishingly unlikely the property test will find it, even with a million samples.
 
 With Kani, however, we can use `kani::any()` to represent all possible `u32` values:
 
@@ -49,13 +49,13 @@ VERIFICATION:- FAILED
 ```
 
 Kani has immediately found a failure.
-Notably, we haven't had to write explicit assertions in our proof harness: by default, Kani will find a host of erroneous conditions which include a reachable call to `panic` or a failing `assert`.
+Notably, we have not had to write explicit assertions in our proof harness: by default, Kani will find a host of erroneous conditions which include a reachable call to `panic` or a failing `assert`.
 
 ### Getting a trace
 
 By default, Kani only reports failures, not how the failure happened.
 This is because, in its full generality, understanding how a failure happened requires exploring a full (potentially large) execution trace.
-Here, we've just got some nondeterministic inputs up front, but that's something of a special case that has a "simpler" explanation (just the choice of nondeterministic input).
+Here, we have just got some nondeterministic inputs up front, but that is something of a special case that has a "simpler" explanation (just the choice of nondeterministic input).
 
 To see traces, run:
 
@@ -72,13 +72,13 @@ let x: u32 = kani::any();
 x = 1023u
 ```
 
-Here we're seeing the line of code and the value assigned in this particular trace.
+Here we are seeing the line of code and the value assigned in this particular trace.
 Like property testing, this is just one example of a failure.
-To find more, we'd presumably fix this issue and then re-run Kani.
+To find more, we would presumably fix this issue and then re-run Kani.
 
 ### Exercise: Try other failures
 
-We put an explicit panic in this function, but it's not the only kind of failure Kani will find.
+We put an explicit panic in this function, but it is not the only kind of failure Kani will find.
 Try a few other types of errors.
 
 For example, instead of panicking we could try explicitly dereferencing a null pointer:
@@ -143,7 +143,7 @@ VERIFICATION:- FAILED
 ## Assertions, Assumptions, and Harnesses
 
 It seems a bit odd that we can take billions of inputs when our function only handles up to a few thousand.
-Let's encode this fact about our function by asserting some reasonable bound on our input, after we've fixed our bug:
+Let us encode this fact about our function by asserting some reasonable bound on our input, after we have fixed our bug:
 
 ```rust,noplaypen
 {{#include tutorial/kani-first-steps/src/final_form.rs:code}}
@@ -169,13 +169,13 @@ But we know that, that was our intention.
 
 This is the purpose of _proof harnesses_.
 Much like property testing (which would also fail in this assertion), we need to set up our preconditions, call the function in question, then assert our postconditions.
-Here's a revised example of the proof harness, one that now succeeds:
+Here is a revised example of the proof harness, one that now succeeds:
 
 ```rust,noplaypen
 {{#include tutorial/kani-first-steps/src/final_form.rs:kani}}
 ```
 
-But now we must wonder if we've really fully tested our function.
+But now we must wonder if we have really fully tested our function.
 What if we revise the function, but forget to update the assumption in our proof harness to cover the new range of inputs?
 
 Fortunately, Kani is able to report a coverage metric for each proof harness.
@@ -190,6 +190,6 @@ The beginning of the report includes coverage information.
 Clicking through to the file will show fully-covered lines in green.
 Lines not covered by our proof harness will show in red.
 
-1. Try changing the assumption in the proof harness to `x < 2048`. Now the harness won't be testing all possible cases.
+1. Try changing the assumption in the proof harness to `x < 2048`. Now the harness will not be testing all possible cases.
 2. Rerun `kani --visualize` on the file
-3. Look at the report: you'll see we no longer have 100% coverage of the function.
+3. Look at the report: you will see we no longer have 100% coverage of the function.