Documentation: Structural changes

docs/src/SUMMARY.md

@@ -1,25 +1,29 @@
 # The Kani Rust Verifier
 
-- [Getting started with Kani](./getting-started.md)
+- [Getting started](./getting-started.md)
   - [Installation](./install-guide.md)
-  - [Comparison with other tools](./tool-comparison.md)
-  - [Kani on a single file](./kani-single-file.md)
-  - [Kani on a package](./cargo-kani.md)
-  - [Kani result types](./kani-result-types.md)
-  - [Debugging failures]()
-  - [Debugging non-termination]()
-  - [Debugging coverage]()
+  - [Usage](./usage.md)
+    - [On a single file](./kani-single-file.md)
+    - [On a package](./cargo-kani.md)
+  - [Verification results](./verification-results.md)
 
-- [Kani tutorial](./kani-tutorial.md)
-  - [First steps with Kani](./tutorial-first-steps.md)
+- [Tutorial](./kani-tutorial.md)
+  - [First steps](./tutorial-first-steps.md)
   - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
-  - [Loops, unwinding, and bounds](./tutorial-loops-unwinding.md)
-  - [Creating non-deterministic variables](./tutorial-nondeterministic-variables.md)
+  - [Loop unwinding](./tutorial-loop-unwinding.md)
+  - [Nondeterministic variables](./tutorial-nondeterministic-variables.md)
   - [Where to start on real code](./tutorial-real-code.md)
 
-- [Kani developer documentation](./dev-documentation.md)
-  - [Working with `RUSTC`](./rustc-hacks.md)
-  - [Testing](./kani-testing.md)
-  - [Book runner](./bookrunner.md)
+- [Developer documentation](dev-documentation.md)
+  - [Command cheat sheets](./cheat-sheets.md)
+  - [Working with `rustc`](./rustc-hacks.md)
+  - [Testing](./testing.md)
+    - [Regression testing](./kani-testing.md)
+    - [Book runner](./bookrunner.md)
 
-- [Limitations](./limitations.md)
+- [Rust feature support](./rust-feature-support.md)
+  - [Overrides](./overrides.md)
+
+---
+
+[Comparison with other tools](./tool-comparison.md)

docs/src/cheat-sheets.md

@@ -0,0 +1,125 @@
+# Kani developer documentation
+
+## Build command cheat sheet
+
+```bash
+# Build all packages in the repository
+cargo build
+```
+
+```bash
+# Full regression suite (does not run bookrunner)
+./scripts/kani-regression.sh
+```
+```bash
+# Delete regression test caches
+# Use build/x86_64-apple-darwin/tests for MacOs
+rm -r build/x86_64-unknown-linux-gnu/tests/
+```
+```bash
+# Test suite run (we can only run one at a time)
+# cargo run -p compiletest -- --suite ${suite} --mode ${mode}
+cargo run -p compiletest -- --suite kani --mode kani
+```
+```bash
+# Book runner run
+./scripts/setup/install_bookrunner_deps.sh
+cargo run -p bookrunner
+```
+```bash
+# Documentation build
+cd docs
+./build-docs.sh
+```
+
+### Resolving development issues
+
+```bash
+# Error "'rustc' panicked at 'failed to lookup `SourceFile` in new context'"
+# or similar error? Clean kani-compiler build:
+cargo clean -p kani-compiler
+cargo build -p kani-compiler
+```
+
+## Git command cheat sheet
+
+Kani follows the "squash and merge pull request" pattern.
+As a result, the "main commit message" will be the title of your pull request.
+The individual commit message bodies you commit during development will by default be a bulleted list in the squashed commit message body, but these are editable at merge time.
+So you don't have to worry about a series of "oops typo fix" messages while fixing up your pull request, these can be edited out of the final message when you click merge.
+
+```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!
+git clean -xffd
+git submodule foreach --recursive git clean -xffd
+git submodule update --init
+```
+```bash
+# Done with that PR, time for a new one?
+git switch main
+git pull origin
+git submodule update --init
+cd src/kani-compiler
+cargo build
+```
+```bash
+# Need to update local branch (e.g. for an open pull request?)
+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.
+```
+```bash
+# Checkout a pull request locally without the github cli
+git fetch origin pull/$ID/head:pr/$ID
+git switch pr/$ID
+```
+```bash
+# Search only git-tracked files
+git grep codegen_panic
+```
+```bash
+# See all commits that are part of Kani, not part of Rust
+git log --graph --oneline origin/upstream-rustc..origin/main
+```
+```bash
+# See all files modified by Kani (compared to upstream Rust)
+git diff --stat origin/upstream-rustc..origin/main
+```
+
+## Kani command cheat sheet
+
+These can help understand what Kani is generating or encountering on an example or test file:
+
+```bash
+# Enable `debug!` macro logging output when running Kani:
+kani --debug file.rs
+```
+```bash
+# Keep CBMC Symbol Table and Goto-C output (.json and .goto)
+kani --keep-temps file.rs
+```
+```bash
+# Generate "C code" from CBMC IR (.c)
+kani --gen-c file.rs
+```
+
+## CBMC command cheat sheet
+
+```bash
+# See CBMC IR from a C file:
+goto-cc file.c -o file.out
+goto-instrument --print-internal-representation file.out
+# or (for json symbol table)
+cbmc --show-symbol-table --json-ui file.out
+# or (an alternative concise format)
+cbmc --show-goto-functions file.out
+```
+```bash
+# Recover C from goto-c binary
+goto-instrument --dump-c file.out > file.gen.c
+```

docs/src/dev-documentation.md

@@ -1,125 +1,8 @@
-# Kani developer documentation
+# Developer documentation
 
-## Build command cheat sheet
+Kani is an open source project open to external contributions.
 
-```bash
-# Build all packages in the repository
-cargo build
-```
-
-```bash
-# Full regression suite (does not run bookrunner)
-./scripts/kani-regression.sh
-```
-```bash
-# Delete regression test caches
-# Use build/x86_64-apple-darwin/tests for MacOs
-rm -r build/x86_64-unknown-linux-gnu/tests/
-```
-```bash
-# Test suite run (we can only run one at a time)
-# cargo run -p compiletest -- --suite ${suite} --mode ${mode}
-cargo run -p compiletest -- --suite kani --mode kani
-```
-```bash
-# Book runner run
-./scripts/setup/install_bookrunner_deps.sh
-cargo run -p bookrunner
-```
-```bash
-# Documentation build
-cd docs
-./build-docs.sh
-```
-
-### Resolving development issues
-
-```bash
-# Error "'rustc' panicked at 'failed to lookup `SourceFile` in new context'"
-# or similar error? Clean kani-compiler build:
-cargo clean -p kani-compiler
-cargo build -p kani-compiler
-```
-
-## Git command cheat sheet
-
-Kani follows the "squash and merge pull request" pattern.
-As a result, the "main commit message" will be the title of your pull request.
-The individual commit message bodies you commit during development will by default be a bulleted list in the squashed commit message body, but these are editable at merge time.
-So you don't have to worry about a series of "oops typo fix" messages while fixing up your pull request, these can be edited out of the final message when you click merge.
-
-```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!
-git clean -xffd
-git submodule foreach --recursive git clean -xffd
-git submodule update --init
-```
-```bash
-# Done with that PR, time for a new one?
-git switch main
-git pull origin
-git submodule update --init
-cd src/kani-compiler
-cargo build
-```
-```bash
-# Need to update local branch (e.g. for an open pull request?)
-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.
-```
-```bash
-# Checkout a pull request locally without the github cli
-git fetch origin pull/$ID/head:pr/$ID
-git switch pr/$ID
-```
-```bash
-# Search only git-tracked files
-git grep codegen_panic
-```
-```bash
-# See all commits that are part of Kani, not part of Rust
-git log --graph --oneline origin/upstream-rustc..origin/main
-```
-```bash
-# See all files modified by Kani (compared to upstream Rust)
-git diff --stat origin/upstream-rustc..origin/main
-```
-
-## Kani command cheat sheet
-
-These can help understand what Kani is generating or encountering on an example or test file:
-
-```bash
-# Enable `debug!` macro logging output when running Kani:
-kani --debug file.rs
-```
-```bash
-# Keep CBMC Symbol Table and Goto-C output (.json and .goto)
-kani --keep-temps file.rs
-```
-```bash
-# Generate "C code" from CBMC IR (.c)
-kani --gen-c file.rs
-```
-
-## CBMC command cheat sheet
-
-```bash
-# See CBMC IR from a C file:
-goto-cc file.c -o file.out
-goto-instrument --print-internal-representation file.out
-# or (for json symbol table)
-cbmc --show-symbol-table --json-ui file.out
-# or (an alternative concise format)
-cbmc --show-goto-functions file.out
-```
-```bash
-# Recover C from goto-c binary
-goto-instrument --dump-c file.out > file.gen.c
-```
+The easiest way to contribute is to [report any
+issue](https://github.com/model-checking/kani/issues/new/choose) you encounter
+while using the tool. If you want to contribute to its development,
+we recommend looking into [these issues](https://github.com/model-checking/kani/contribute).

docs/src/kani-testing.md

@@ -1,22 +1,3 @@
-# Testing
-
-Testing in Kani is carried out in multiple ways. There are at least
-two very good reasons to do it:
- 1. **Software regression**: A regression is a type of bug
-    that appears after a change is introduced where a feature that
-    was previously working has unexpectedly stopped working.
-
-    Regression testing allows one to prevent a software regression
-    from happening by running a comprehensive set of working tests
-    before any change is committed to the project.
- 2. **Software metrics**: A metric is a measure of software
-    characteristics which are quantitative and countable. Metrics are
-    particularly valuable for project management purposes.
-
-We recommend reading our section on [Regression Testing](#regression-testing)
-if you are interested in Kani development. At present, we obtain metrics based
-on the [book runner](./bookrunner.md).
-
 # Regression testing
 
 Kani relies on a quite extensive range of tests to perform regression testing.

docs/src/overrides.md

@@ -0,0 +1,17 @@
+## Overrides
+
+As explained in [Comparison with other
+tools](./tool-comparison.md#comparison-with-other-tools), Kani is based on a
+technique called model checking, which verifies a program without actually
+executing it. It does so through encoding the program and analyzing the encoded
+version. The encoding process often requires "modeling" some of the library
+functions to make them suitable for analysis. Typical examples of functionality
+that requires modeling are system calls and I/O operations. In some cases, Kani
+performs such encoding through overriding some of the definitions in the Rust
+standard library. The following table lists some of the symbols that Kani
+overrides and a description of their behavior compared to the `std` versions:
+
+Name | Description |
+---  | --- |
+`print`, `eprint`, `println`, and `eprintln` macros | Kani's version of these macros skips functionality that is not relevant for verification, e.g., string formatting and I/O operations |
+`assert`, `assert_eq`, and `assert_ne` macros | Kani overrides these macros in order to skip string formatting code, control the message that is displayed in the verification report for those asserts, and perform some instrumentation. |

docs/src/limitations.md → docs/src/rust-feature-support.md

@@ -1,4 +1,3 @@
-# Limitations
 ## Rust feature support
 
 The table below tries to summarize the current support in Kani for
@@ -429,21 +428,3 @@ code to be sequential.
 While Kani is capable of generating code for SIMD instructions, unfortunately, it
 does not provide support for the verification of some operations like vector
 comparison (e.g., `simd_eq`).
-
-## Overrides
-
-As explained in [Comparison with other
-tools](./tool-comparison.md#comparison-with-other-tools), Kani is based on a
-technique called model checking, which verifies a program without actually
-executing it. It does so through encoding the program and analyzing the encoded
-version. The encoding process often requires "modeling" some of the library
-functions to make them suitable for analysis. Typical examples of functionality
-that requires modeling are system calls and I/O operations. In some cases, Kani
-performs such encoding through overriding some of the definitions in the Rust
-standard library. The following table lists some of the symbols that Kani
-overrides and a description of their behavior compared to the `std` versions:
-
-Name | Description |
----  | --- |
-`print`, `eprint`, `println`, and `eprintln` macros | Kani's version of these macros skips functionality that is not relevant for verification, e.g., string formatting and I/O operations |
-`assert`, `assert_eq`, and `assert_ne` macros | Kani overrides these macros in order to skip string formatting code, control the message that is displayed in the verification report for those asserts, and perform some instrumentation. |

docs/src/testing.md

@@ -0,0 +1,18 @@
+# Testing
+
+Testing in Kani is carried out in multiple ways. There are at least
+two very good reasons to do it:
+ 1. **Software regression**: A regression is a type of bug
+    that appears after a change is introduced where a feature that
+    was previously working has unexpectedly stopped working.
+
+    Regression testing allows one to prevent a software regression
+    from happening by running a comprehensive set of working tests
+    before any change is committed to the project.
+ 2. **Software metrics**: A metric is a measure of software
+    characteristics which are quantitative and countable. Metrics are
+    particularly valuable for project management purposes.
+
+We recommend reading our section on [Regression Testing](#regression-testing)
+if you are interested in Kani development. At present, we obtain metrics based
+on the [book runner](./bookrunner.md).