From f11b9792a403b9a94c643b95e8ceafa7c29f58e7 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 20 Sep 2024 18:24:46 +0000 Subject: [PATCH 1/6] Improve documentation with links and additional steps --- doc/src/tools/kani.md | 57 +++++++++++++++++++++++++++++++++---------- 1 file changed, 44 insertions(+), 13 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 985d507c4be33..cd86cd82a7e9c 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -5,7 +5,7 @@ Kani is designed to prove safety properties in your code as well as the absence of some forms of undefined behavior. It uses model checking under the hood to ensure that Rust programs adhere to user specified properties. -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). +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). ## Usage @@ -27,7 +27,8 @@ fn harness() { let a = kani::any::(); let b = kani::any::(); let result = abs_diff(a, b); - kani::assert(result >= 0, "Result should always be more than 0");} + kani::assert(result >= 0, "Result should always be more than 0"); +} ``` Running the command `cargo kani` in your cargo crate will give the result @@ -46,29 +47,29 @@ Verification failed for - harness Complete - 0 successfully verified harnesses, 1 failures, 1 total. ``` +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). ## Using Kani to verify the Rust Standard Library To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started. +Here is a short tutorial to get started with using Kani to verify some proofs that you write for the standard library. ### Step 1 -Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify. +Create a local copy of the model-checking fork of the Rust Standard Library. The fork comes with Kani initiated, so all you'll need to do is to call Kani's +building-block APIs (such as +`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`) directly. -For example, insert this short blob into your copy of the library. This blob imports the building-block APIs such as -`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`. +For example, insert this module into an existing file like `library/core/src/lib.rs` in your copy of the library. ``` rust -#[cfg(kani)] -kani_core::kani_lib!(core); - #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] pub mod verify { use crate::kani; #[kani::proof] - pub fn harness() { + pub fn harness_introduction() { kani::assert(true, "yay"); } @@ -86,14 +87,16 @@ pub mod verify { ### Step 2 -Run the following command in your local terminal: +Run the following command in your local terminal (Replace "path/to/library" and "path/to/target" with your local paths): -`kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing`. +``` +kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z mem-predicates +``` 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. -- `"path/to/library"`: This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script. -- `--target-dir "path/to/target"`: This optional argument sets the target directory where Kani will store its output and intermediate files. +- `"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` +- `--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` Apart from these, you can use your regular `kani-args` such as `-Z function-contracts` and `-Z stubbing` depending on your verification needs. 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) @@ -112,6 +115,34 @@ Verification Time: 0.017101772s Complete - 2 successfully verified harnesses, 0 failures, 2 total. ``` +### Running on a specific harness + +You can specify a specific harness to be verified using the --harness flag. + +For example, in your local copy of the verify repo, run the following command. +``` +kani verify-std --harness harness_introduction -Z unstable-options "./library" --target-dir "/tmp" -Z function-contracts -Z mem-predicates +``` + +This gives you the verification result for just `harness_introduction` from the afore-mentioned blob. + +``` +RESULTS: +Check 1: verify::harness_introduction.assertion.1 + - Status: SUCCESS + - Description: "yay" + - Location: library/core/src/lib.rs:479:9 in function verify::harness_introduction + + +SUMMARY: + ** 0 of 1 failed + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.01885804s + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. +``` + ## More details You can find more information about how to install and how you can customize your use of Kani in the From 9bf408740850631a10f5a86c48679ea21a5d03e3 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 20 Sep 2024 18:27:50 +0000 Subject: [PATCH 2/6] Describe the steps --- doc/src/tools/kani.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index cd86cd82a7e9c..f0b2fd15ef63e 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -51,10 +51,9 @@ For a more detailed tutorial, you can refer to the [tutorial section of the Kani ## Using Kani to verify the Rust Standard Library -To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started. Here is a short tutorial to get started with using Kani to verify some proofs that you write for the standard library. -### Step 1 +### Step 1 - Add some proofs to your copy of the model-checking std Create a local copy of the model-checking fork of the Rust Standard Library. The fork comes with Kani initiated, so all you'll need to do is to call Kani's building-block APIs (such as @@ -85,8 +84,9 @@ pub mod verify { } ``` -### Step 2 +### Step 2 - Run the Kani verify-std subcommand +To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started. Run the following command in your local terminal (Replace "path/to/library" and "path/to/target" with your local paths): ``` @@ -101,7 +101,7 @@ The command `kani verify-std` is a sub-command of the `kani`. This specific sub- Apart from these, you can use your regular `kani-args` such as `-Z function-contracts` and `-Z stubbing` depending on your verification needs. 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) -### Step 3 +### Step 3 - Check verification result After running the command, you can expect an output that looks like this: From 9ba66e6fb7b2065a84ab13713a1efe40fd07d16a Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 20 Sep 2024 18:42:41 +0000 Subject: [PATCH 3/6] Fix type of function-contracts --- doc/src/tools/kani.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index f0b2fd15ef63e..de900216c088f 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -57,7 +57,7 @@ Here is a short tutorial to get started with using Kani to verify some proofs th Create a local copy of the model-checking fork of the Rust Standard Library. The fork comes with Kani initiated, so all you'll need to do is to call Kani's building-block APIs (such as -`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`) directly. +`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. For example, insert this module into an existing file like `library/core/src/lib.rs` in your copy of the library. @@ -117,7 +117,7 @@ Complete - 2 successfully verified harnesses, 0 failures, 2 total. ### Running on a specific harness -You can specify a specific harness to be verified using the --harness flag. +You can specify a specific harness to be verified using the `--harness` flag. For example, in your local copy of the verify repo, run the following command. ``` From c437471d29856d9c9e9597797c7243ad092662ff Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 20 Sep 2024 19:09:47 +0000 Subject: [PATCH 4/6] Fix wording --- doc/src/tools/kani.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index de900216c088f..4e03766c519d6 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -59,7 +59,7 @@ Create a local copy of the model-checking fork of the Rust Standard Library. The building-block APIs (such as `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. -For example, insert this module into an existing file like `library/core/src/lib.rs` in your copy of the library. +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. ``` rust #[cfg(kani)] @@ -87,10 +87,10 @@ pub mod verify { ### Step 2 - Run the Kani verify-std subcommand To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started. -Run the following command in your local terminal (Replace "path/to/library" and "path/to/target" with your local paths): +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: ``` -kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z mem-predicates +kani verify-std -Z unstable-options "/path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z mem-predicates ``` 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. From b9e7943131926fa7c89bc2e61fbcaff016a6409a Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Fri, 20 Sep 2024 20:06:17 +0000 Subject: [PATCH 5/6] Add link to https://github.com/model-checking/verify-rust-std --- doc/src/tools/kani.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 4e03766c519d6..85dc859698f93 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -55,8 +55,7 @@ Here is a short tutorial to get started with using Kani to verify some proofs th ### Step 1 - Add some proofs to your copy of the model-checking std -Create a local copy of the model-checking fork of the Rust Standard Library. The fork comes with Kani initiated, so all you'll need to do is to call Kani's -building-block APIs (such as +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 `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. 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. @@ -120,6 +119,7 @@ Complete - 2 successfully verified harnesses, 0 failures, 2 total. You can specify a specific harness to be verified using the `--harness` flag. For example, in your local copy of the verify repo, run the following command. + ``` kani verify-std --harness harness_introduction -Z unstable-options "./library" --target-dir "/tmp" -Z function-contracts -Z mem-predicates ``` From dc98adc111cba7fee0403d08305cb67077f637cf Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Fri, 20 Sep 2024 16:06:58 -0400 Subject: [PATCH 6/6] Apply suggestions from code review Co-authored-by: Carolyn Zech --- doc/src/tools/kani.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 85dc859698f93..390e3bb713832 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -51,7 +51,7 @@ For a more detailed tutorial, you can refer to the [tutorial section of the Kani ## Using Kani to verify the Rust Standard Library -Here is a short tutorial to get started with using Kani to verify some proofs that you write for the standard library. +Here is a short tutorial of how to use Kani to verify proofs for the standard library. ### Step 1 - Add some proofs to your copy of the model-checking std @@ -124,7 +124,7 @@ For example, in your local copy of the verify repo, run the following command. kani verify-std --harness harness_introduction -Z unstable-options "./library" --target-dir "/tmp" -Z function-contracts -Z mem-predicates ``` -This gives you the verification result for just `harness_introduction` from the afore-mentioned blob. +This gives you the verification result for just `harness_introduction` from the aforementioned blob. ``` RESULTS: