Update Kani Book

docs/src/SUMMARY.md

@@ -7,6 +7,8 @@
   - [Using Kani](./usage.md)
   - [Verification results](./verification-results.md)
 
+- [Crates Documentation](./crates/index.md)
+
 - [Tutorial](./kani-tutorial.md)
   - [First steps](./tutorial-first-steps.md)
   - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
@@ -18,6 +20,7 @@
   - [Experimental features](./reference/experimental/experimental-features.md)
     - [Coverage](./reference/experimental/coverage.md)
     - [Stubbing](./reference/experimental/stubbing.md)
+    - [Contracts](./reference/experimental/contracts.md)
     - [Concrete Playback](./reference/experimental/concrete-playback.md)
 - [Application](./application.md)
   - [Comparison with other tools](./tool-comparison.md)
@@ -45,8 +48,6 @@
     - [Unstable features](./rust-feature-support/unstable.md)
   - [Overrides](./overrides.md)
 
-- [Crates Documentation](./crates/index.md)
-
 ---
 
 - [FAQ](./faq.md)

docs/src/getting-started.md

@@ -14,7 +14,7 @@ Proof harnesses are similar to test harnesses, especially property-based test ha
 
 Kani is currently under active development.
 Releases are published [here](https://github.com/model-checking/kani/releases).
-Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc).
+Major changes to Kani are documented in the [RFC Book](https://model-checking.github.io/kani/rfc). We also publish updates on Kani use cases and features on our [blog](https://model-checking.github.io/kani-verifier-blog/).
 
 There is support for a fair amount of Rust language features, but not all (e.g., concurrency).
 Please see [Limitations](./limitations.md) for a detailed list of supported features.

docs/src/reference/experimental/contracts.md

@@ -0,0 +1,58 @@
+# Contracts
+
+Consider the following example:
+
+```rust
+fn gcd(mut max: u64, mut min: u64) -> u64 {
+    if min > max {
+        std::mem::swap(&mut max, &mut min);
+    }
+
+    let rest = max % min;
+    if rest == 0 { min } else { gcd(min, rest) }
+}
+```
+In the [worst case](https://en.wikipedia.org/wiki/Euclidean_algorithm#Worst-case), the number of steps (recursions) in `gcd` approaches 1.5 times the number of bits needed to represent the input numbers. So, for two large 64-bit numbers, a single call to `gcd` can take almost 96 iterations. It would be very expensive for Kani to unroll each of these iterations and then perform symbolic execution.
+
+Instead, we can write *contracts* with guarantees about `gcd`'s behavior. For example, perhaps we want to ensure that the returned `result` does indeed divide both `max` and `min`. In that case, we could write contracts like these:
+
+```rust
+#[kani::requires(min != 0 && max != 0)]
+#[kani::ensures(|result| *result != 0 && max % *result == 0 && min % *result == 0)]
+#[kani::recursion]
+fn gcd(mut max: u64, mut min: u64) -> u64 { ... }
+```
+
+Since `gcd` performs `max % min` (and perhaps swaps those values), passing zero as an argument could cause a division by zero. The `requires` contract tells Kani to restrict the range of nondeterministic inputs to nonzero ones so that we don't run into this error. The `ensures` contract is what actually checks that the result is a correct divisor for the inputs. (The `recursion` attribute is required when using contracts on recursive functions).
+
+Then, we would write a harness to *verify* those contracts, like so:[^1]
+
+```rust
+#[kani::proof_for_contract(gcd)]
+fn check_gcd() {
+    let mut max: u64 = kani::any();
+    let mut min: u64 = kani::any();
+    gcd(max, min);
+}
+```
+
+and verify it by running `kani -Z function-contracts`.
+
+Once Kani verifies the contracts, we can use Kani's [stubbing feature](stubbing.md) to replace all invocations to `gcd` with its contracts, for instance:
+
+```rust
+// Assume foo() invokes gcd().
+// By using stub_verified, we tell Kani to replace 
+// invocations of gcd() with its verified contracts.
+#[kani::proof]
+#[kani::stub_verified(gcd)]
+fn check_foo() {
+    let x: usize = kani::any();
+    foo(x);
+}
+```
+By leveraging the stubbing feature, we can replace the (expensive) `gcd` call with a *verified abstraction* of its behavior, greatly reducing verification time for `foo`.
+
+There is far more information to learn about contracts. We highly recommend reading our [blog post about contracts](https://model-checking.github.io/kani-verifier-blog/2024/01/29/function-contracts.html) (from which this `gcd` example is taken). We also recommend looking at the `contracts` module in our [documentation](../../crates/index.md).
+
+[^1]: (If you are attempting to run this example locally, note you may run into performance issues with unconstrained `u64` inputs. If that is the case, try using `kani::assume` to restrict the inputs to a smaller range.)

docs/src/reference/experimental/coverage.md

@@ -1,4 +1,4 @@
-## Coverage
+# 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: