You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: doc/src/tools/kani.md
+59-18Lines changed: 59 additions & 18 deletions
Original file line number
Diff line number
Diff line change
@@ -5,7 +5,7 @@ Kani is designed to prove safety properties in your code as well as
5
5
the absence of some forms of undefined behavior. It uses model checking under the hood to ensure that
6
6
Rust programs adhere to user specified properties.
7
7
8
-
You can find more information about how to install in [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
8
+
You can find more information about how to install in [the installation section of the Kani book](https://model-checking.github.io/kani/install-guide.html).
9
9
10
10
## Usage
11
11
@@ -27,7 +27,8 @@ fn harness() {
27
27
leta=kani::any::<i32>();
28
28
letb=kani::any::<i32>();
29
29
letresult=abs_diff(a, b);
30
-
kani::assert(result>=0, "Result should always be more than 0");}
30
+
kani::assert(result>=0, "Result should always be more than 0");
31
+
}
31
32
```
32
33
33
34
Running the command `cargo kani` in your cargo crate will give the result
@@ -46,29 +47,28 @@ Verification failed for - harness
For a more detailed tutorial, you can refer to the [tutorial section of the Kani book](https://model-checking.github.io/kani/kani-tutorial.html).
49
51
50
52
## Using Kani to verify the Rust Standard Library
51
53
52
-
To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started.
54
+
Here is a short tutorial of how to use Kani to verify proofs for the standard library.
53
55
54
-
### Step 1
56
+
### Step 1 - Add some proofs to your copy of the model-checking std
55
57
56
-
Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify.
58
+
Create a local copy of the [model-checking fork](https://github.com/model-checking/verify-rust-std) of the Rust Standard Library. The fork comes with Kani configured, so all you'll need to do is to call Kani's building-block APIs (such as
59
+
`assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `modifies`, `requires` and `ensures`) directly.
57
60
58
-
For example, insert this short blob into your copy of the library. This blob imports the building-block APIs such as
59
-
`assert`, `assume`, `proof` and [function-contracts](https://github.com/model-checking/kani/blob/main/rfc/src/rfcs/0009-function-contracts.md) such as `proof_for_contract` and `fake_function`.
60
61
61
-
```rust
62
-
#[cfg(kani)]
63
-
kani_core::kani_lib!(core);
62
+
For example, insert this module into an existing file in the core library, like `library/core/src/hint.rs` or `library/core/src/error.rs` in your copy of the library. This is just for the purpose of getting started, so you can insert in any existing file in the core library if you have other preferences.
64
63
64
+
```rust
65
65
#[cfg(kani)]
66
66
#[unstable(feature ="kani", issue ="none")]
67
67
pubmodverify {
68
68
usecrate::kani;
69
69
70
70
#[kani::proof]
71
-
pubfnharness() {
71
+
pubfnharness_introduction() {
72
72
kani::assert(true, "yay");
73
73
}
74
74
@@ -84,21 +84,24 @@ pub mod verify {
84
84
}
85
85
```
86
86
87
-
### Step 2
87
+
### Step 2 - Run the Kani verify-std subcommand
88
88
89
-
Run the following command in your local terminal:
89
+
To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started.
90
+
Run the following command in your local terminal (Replace "/path/to/library" and "/path/to/target" with your local paths) from the verify repository root:
The command `kani verify-std` is a sub-command of the `kani`. This specific sub-command is used to verify the Rust Standard Library with the following arguments.
94
97
95
-
-`"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script.
96
-
-`--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files.
98
+
-`"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script. For example, `./library` or `/home/ubuntu/verify-rust-std/library`
99
+
-`--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files. For example, `/tmp` or `/tmp/verify-std`
97
100
98
-
Apart from these, you can use your regular `kani-args` such as `-Z function-contracts`and `-Z stubbing` depending on your verification needs.
101
+
Apart from these, you can use your regular `kani-args` such as `-Z function-contracts`, `-Z stubbing`and `-Z mem-predicates` depending on your verification needs. If you run into a Kani error that says `Use of unstable feature`, add the corresponding feature with `-Z` to the command line.
99
102
For more details on Kani's features, refer to [the features section in the Kani Book](https://model-checking.github.io/kani/reference/attributes.html)
100
103
101
-
### Step 3
104
+
### Step 3 - Check verification result
102
105
103
106
After running the command, you can expect an output that looks like this:
0 commit comments