add experimental features section

docs/src/SUMMARY.md

@@ -12,12 +12,13 @@
   - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
   - [Loop unwinding](./tutorial-loop-unwinding.md)
   - [Nondeterministic variables](./tutorial-nondeterministic-variables.md)
-  - [Debugging verification failures](./debugging-verification-failures.md)
 
 - [Reference](./reference.md)
   - [Attributes](./reference/attributes.md)
-  - [Stubbing](./reference/stubbing.md)
-
+  - [Experimental features](./reference/experimental/experimental-features.md)
+    - [Coverage](./reference/experimental/coverage.md)
+    - [Stubbing](./reference/experimental/stubbing.md)
+    - [Debugging verification failures](./reference/experimental/debugging-verification-failures.md)
 - [Application](./application.md)
   - [Comparison with other tools](./tool-comparison.md)
   - [Where to start on real code](./tutorial-real-code.md)

docs/src/debugging-verification-failures.md → docs/src/reference/experimental/concrete-playback.md

@@ -1,4 +1,4 @@
-# Debugging verification failures
+# Concrete Playback
 
 When the result of a certain check comes back as a `FAILURE`,
 Kani offers different options to help debug:
@@ -7,14 +7,12 @@ proof harness using a concrete counterexample.
 * `--visualize`. This feature generates an HTML text-based trace that
 enumerates the execution steps leading to the check failure.
 
-## Concrete playback
-
 When concrete playback is enabled, Kani will generate unit tests for assertions that failed during verification,
 as well as cover statements that are reachable.
 
 These tests can then be executed using Kani's playback subcommand.
 
-### Usage
+## Usage
 
 In order to enable this feature, run Kani with the `-Z concrete-playback --concrete-playback=[print|inplace]` flag.
 After getting a verification failure, Kani will generate a Rust unit test case that plays back a failing
@@ -46,7 +44,7 @@ The output will have a line in the beginning like
 
 You can further debug the binary with tools like `rust-gdb` or `lldb`.
 
-### Example
+## Example
 
 Running `kani -Z concrete-playback --concrete-playback=print` on the following source file:
 ```rust
@@ -75,15 +73,15 @@ Here, `133` and `35207` are the concrete values that, when substituted for `a` a
 cause an assertion failure.
 `vec![135, 137]` is the byte array representation of `35207`.
 
-### Request for comments
+## Request for comments
 
 This feature is experimental and is therefore subject to change.
 If you have ideas for improving the user experience of this feature,
 please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/1536).
 We are tracking the existing feature requests in
 [this GitHub milestone](https://github.com/model-checking/kani/milestone/10).
 
-### Limitations 
+## Limitations 
 
 * This feature does not generate unit tests for failing non-panic checks (e.g., UB checks).
 This is because checks would not trigger runtime errors during concrete playback.

docs/src/reference/experimental/coverage.md

@@ -0,0 +1,32 @@
+## Coverage
+
+Recall our `estimate_size` example from [First steps](../tutorial-first-steps.md),
+where we wrote a proof harness constraining the range of inputs to integers less than 4096:
+
+```rust
+{{#include ../../tutorial/first-steps-v2/src/lib.rs:kani}}
+```
+
+We must wonder if we've 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.
+In the `first-steps-v2` directory, try running:
+
+```
+cargo kani --coverage -Z line-coverage --harness verify_success
+```
+
+which verifies the harness, then prints coverage information for each line.
+In this case, we see that each line of `estimate_size` is followed by `FULL`, indicating that our proof harness provides full coverage.
+
+Try changing the assumption in the proof harness to `x < 2048`.
+Now the harness won't be testing all possible cases.
+Rerun the command.
+You'll see this line:
+
+```
+src/lib.rs, 24, NONE
+```
+
+which indicates that the proof no longer covers line 24, which addresses the case where `x >= 2048`.

docs/src/reference/experimental/experimental-features.md

@@ -0,0 +1,5 @@
+# Experimental Features
+
+We elaborate on some of the more commonly used experimental features in Kani.
+This is not an exhaustive list; to see all of Kani's experimental features, run `cargo kani --help`.
+To use an experimental feature, invoke Kani with the `--unstable` or `-Z` flag followed by the name of the feature.

docs/src/tutorial-first-steps.md

@@ -193,30 +193,6 @@ Here's a revised example of the proof harness, one that now succeeds:
 {{#include tutorial/first-steps-v2/src/lib.rs:kani}}
 ```
 
-But now we must wonder if we've 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.
-Try running:
-
-```
-cargo kani --coverage -Z line-coverage --harness verify_success
-```
-
-which verifies the harness, then prints coverage information for each line.
-In this case, we see that each line of `estimate_size` is followed by `FULL`, indicating that our proof harness provides full coverage.
-
-Try changing the assumption in the proof harness to `x < 2048`.
-Now the harness won't be testing all possible cases.
-Rerun the command.
-You'll see this line:
-
-```
-src/lib.rs, 24, NONE
-```
-
-which indicates that the proof no longer covers line 24, which addresses the case where `x >= 2048`.
-
 ## Summary
 
 In this section:
@@ -226,4 +202,3 @@ In this section:
 3. We saw how to write a proof harness and use `kani::any()`.
 4. We saw how to get a failing **trace** using `kani --visualize`
 5. We saw how proof harnesses are used to set up preconditions with `kani::assume()`.
-6. We saw how to obtain **coverage** metrics and use them to ensure our proofs are covering as much as they should be.