From c81bfeb4b3553e13b3eff1c242910a1a83636df9 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 11 Jun 2024 17:14:32 +0000 Subject: [PATCH 1/3] Add Kani usage and verify-std section --- doc/book.toml | 2 +- doc/src/tools/kani.md | 123 ++++++++++++++++++++++++++++++++++++++++-- 2 files changed, 121 insertions(+), 4 deletions(-) diff --git a/doc/book.toml b/doc/book.toml index 18759f5c0c20c..5e0ecd77ddb18 100644 --- a/doc/book.toml +++ b/doc/book.toml @@ -19,7 +19,7 @@ edit-url-template = "https://github.com/model-checking/verify-rust-std/edit/main runnable = false [output.linkcheck] - +optional = true [rust] edition = "2021" diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index 2b7b008f098fb..c5c70a1eb539f 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -1,7 +1,124 @@ # Kani Rust Verifier The Kani Rust Verifier is a bit-precise model checker for Rust. -This page will give more details on how to use Kani to verify the standard library. -You can find more informations about how to install and use Kani in the -[Kani book](https://model-checking.github.io/kani/). +Kani is designed to prove safety properties in your code as well as +the absence of undefined behavior. It uses formal methods under the hood to ensure that +Rust programs adhere to user specified properties. + +You can find more informations about how to install in [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html). + +## Usage + +Consider a rust function that takes an integer and returns its absolute value and +a kani proof that invokes the function that you want to verify + +``` rust +// src/main.rs +fn abs_diff(a: i32, b: i32) -> i32 { + if a > b { + a - b + } else { + b - a + } +} + +#[cfg(kani)] +#[kani::proof] +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");} +``` + +Running the command `cargo kani` in your cargo crate will give the result + +``` +...Metadata about the Kani run + +RESULTS: +Check 1: abs_diff.assertion.1 + - Status: FAILURE + - Description: "attempt to subtract with overflow" + - Location: src/main.rs:5:9 in function abs_diff + +... Other properties that might have failed or succeeded. + +Summary: +Verification failed for - harness +Complete - 0 successfully verified harnesses, 1 failures, 1 total. +``` + + +## Using Kani to verify the rust standard library + +To aid the std library verification effort, Kani provides a subcommand out of the box to help you get started. + +### Step 1 + +Modify your local copy of the rust std library by writing proofs for the functions/methods that you want to verify. + +For example, insert this short blob into your copy of the std library. This blob imports the building-block APIs such as +`assert`, `assume`, `proof` and function-contracts such as `proof_for_contract` and `fake_function`. + +``` rust +// src/lib/.rs +#[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() { + kani::assert(true, "yay"); + } + + #[kani::proof_for_contract(trivial_function)] + fn dummy_proof() { + trivial_function(true); + } + + #[kani::requires(x == true)] + fn trivial_function(x: bool) -> bool { + x + } +} +``` + +### Step 2 + +Run the following command in your local terminal: + +`kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing`. + +The command `kani verify-std` is a subcommand of the `kani`. This specific subcommand 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. + +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 + +After running the command, you can expect an output that looks like this: + +``` +... Details about properties that failed or suceeded verifiaction + +SUMMARY: + ** 0 of 1 failed + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.017101772s + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. +``` + +## More details + +You can find more informations about how to install and how you can customize your use of Kani in the +[Kani book](https://model-checking.github.io/kani/). From 82251b736f6f9e4103acf8e044983ad53eef05e3 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Tue, 11 Jun 2024 15:13:55 -0400 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Felipe R. Monteiro --- doc/src/tools/kani.md | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index c5c70a1eb539f..e86db26723084 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -5,15 +5,14 @@ Kani is designed to prove safety properties in your code as well as the absence of undefined behavior. It uses formal methods under the hood to ensure that Rust programs adhere to user specified properties. -You can find more informations 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 [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html). ## Usage -Consider a rust function that takes an integer and returns its absolute value and -a kani proof that invokes the function that you want to verify +Consider a Rust function that takes an integer and returns its absolute value and +a Kani proof that invokes the function that you want to verify ``` rust -// src/main.rs fn abs_diff(a: i32, b: i32) -> i32 { if a > b { a - b @@ -34,8 +33,6 @@ fn harness() { Running the command `cargo kani` in your cargo crate will give the result ``` -...Metadata about the Kani run - RESULTS: Check 1: abs_diff.assertion.1 - Status: FAILURE @@ -50,19 +47,18 @@ Complete - 0 successfully verified harnesses, 1 failures, 1 total. ``` -## Using Kani to verify the rust standard library +## Using Kani to verify the Rust Standard Library -To aid the std library verification effort, Kani provides a subcommand out of the box to help you get started. +To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started. ### Step 1 -Modify your local copy of the rust std library by writing proofs for the functions/methods that you want to verify. +Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify. -For example, insert this short blob into your copy of the std library. This blob imports the building-block APIs such as +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 such as `proof_for_contract` and `fake_function`. ``` rust -// src/lib/.rs #[cfg(kani)] kani_core::kani_lib!(core); @@ -94,9 +90,9 @@ Run the following command in your local terminal: `kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing`. -The command `kani verify-std` is a subcommand of the `kani`. This specific subcommand is used to verify the Rust standard library with the following arguments. +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. +- `"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. Apart from these, you can use your regular `kani-args` such as `-Z function-contracts` and `-Z stubbing` depending on your verification needs. @@ -120,5 +116,5 @@ Complete - 2 successfully verified harnesses, 0 failures, 2 total. ## More details -You can find more informations about how to install and how you can customize your use of Kani in the +You can find more information about how to install and how you can customize your use of Kani in the [Kani book](https://model-checking.github.io/kani/). From 8408d4008ca6e176f24da4c2818cf62272c340d8 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri Date: Tue, 11 Jun 2024 21:19:12 +0000 Subject: [PATCH 3/3] Add links and remove extra content --- doc/book.toml | 1 - doc/src/tools/kani.md | 8 +++----- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/doc/book.toml b/doc/book.toml index 5e0ecd77ddb18..ed71647dd8ad9 100644 --- a/doc/book.toml +++ b/doc/book.toml @@ -19,7 +19,6 @@ edit-url-template = "https://github.com/model-checking/verify-rust-std/edit/main runnable = false [output.linkcheck] -optional = true [rust] edition = "2021" diff --git a/doc/src/tools/kani.md b/doc/src/tools/kani.md index c5c70a1eb539f..9f72a08c9b7ff 100644 --- a/doc/src/tools/kani.md +++ b/doc/src/tools/kani.md @@ -1,8 +1,8 @@ # Kani Rust Verifier -The Kani Rust Verifier is a bit-precise model checker for Rust. +The [Kani Rust Verifier](https://github.com/model-checking/kani) is a bit-precise model checker for Rust. Kani is designed to prove safety properties in your code as well as -the absence of undefined behavior. It uses formal methods under the hood to ensure that +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 informations about how to install in [this section of the Kani book](https://model-checking.github.io/kani/install-guide.html). @@ -59,7 +59,7 @@ To aid the std library verification effort, Kani provides a subcommand out of th Modify your local copy of the rust std library by writing proofs for the functions/methods that you want to verify. For example, insert this short blob into your copy of the std library. This blob imports the building-block APIs such as -`assert`, `assume`, `proof` and function-contracts such as `proof_for_contract` and `fake_function`. +`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`. ``` rust // src/lib/.rs @@ -107,8 +107,6 @@ For more details on Kani's features, refer to [the features section in the Kani After running the command, you can expect an output that looks like this: ``` -... Details about properties that failed or suceeded verifiaction - SUMMARY: ** 0 of 1 failed