Merge branch 'main' into core-transmutation-challenge-2024-06

Author: tautschnig

.github/workflows/kani.yml

@@ -26,6 +26,11 @@ jobs:
       matrix:
         # Kani does not support windows.
         os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
     steps:
       - name: Checkout Library
         uses: actions/checkout@v4
@@ -41,6 +46,11 @@ jobs:
           path: kani
           ref: features/verify-rust-std
 
+      - name: Setup Dependencies
+        working-directory: kani
+        run: |
+          ./scripts/setup/${{ matrix.base }}/install_deps.sh
+
       - name: Build `Kani`
         working-directory: kani
         run: |
@@ -52,5 +62,6 @@ jobs:
         env:
           RUST_BACKTRACE: 1
         run: |
-          kani verify-std -Z unstable-options ./library --target-dir "target"
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
           

.github/workflows/rustc.yml

@@ -61,6 +61,9 @@ jobs:
 
       - name: Run tests
         working-directory: upstream
+        env:
+          # Avoid error due to unexpected `cfg`.
+          RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
         run: |
           ./configure --set=llvm.download-ci-llvm=true
           ./x test --stage 0 library/std

.gitignore

@@ -26,6 +26,7 @@ Session.vim
 *.rlib
 *.rmeta
 *.mir
+Cargo.lock
 
 ## Temporary files
 *~

README.md

@@ -1,5 +1,9 @@
 # Rust std-lib verification
 
+[![Rust Tests](https://github.com/model-checking/verify-rust-std/actions/workflows/rustc.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/rustc.yml)
+[![Build Book](https://github.com/model-checking/verify-rust-std/actions/workflows/book.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/book.yml)
+
+
 This repository is a fork of the official Rust programming
 language repository, created solely to verify the Rust standard
 library. It should not be used as an alternative to the official

doc/book.toml

@@ -20,6 +20,5 @@ runnable = false
 
 [output.linkcheck]
 
-
 [rust]
 edition = "2021"

doc/src/SUMMARY.md

@@ -4,6 +4,7 @@
 
 - [General Rules](./general-rules.md)
   - [Challenge Template](./template.md)
+  - [Tool application](./todo.md)
 
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
@@ -12,5 +13,5 @@
 ---
 
 # Challenges
-- [Coming soon](./todo.md)
 - [Core Transmutation](./core-transmutation.md)
+- [Memory safety of core intrinsics](./intrinsics-memory.md)

doc/src/general-rules.md

@@ -10,7 +10,7 @@ NOTE: This work is not officially affiliated, or endorsed by the Rust project or
 tracking issue where contributors can add comments and ask clarification questions.
 You can find the list of [open challenges here](https://github.com/model-checking/verify-rust-std/labels/Challenge).
 
-**Solutions:** Solutions to a problem should be submitted as a single Pull Request (PR) to this repository. 
+**Solutions:** Solutions to a problem should be submitted as a single Pull Request (PR) to this repository.
 The solution should run as part of the CI.
 See more details about [minimum requirements for each solution](general-rules.md#solution-requirements).
 
@@ -33,7 +33,7 @@ well as to track the status of the challenge.
 
 A proposed solution to a verification problem will only **be reviewed** if all the minimum requirements below are met:
 
-* Each contribution or attempt should be submitted via a pull request to be analyzed by reviewers. 
+* Each contribution or attempt should be submitted via a pull request to be analyzed by reviewers.
 * By submitting the solution, participants confirm that they can use, modify, copy, and redistribute their contribution,
   under the terms of their choice.
 * The contribution must be automated and should be checked and pass as part of the PR checks.
@@ -56,7 +56,7 @@ The type of obstacles users face may depend on which part of the standard librar
 Everyone is welcome to submit new challenge proposals for review by our committee.
 Follow the following steps to create a new proposal:
 
-1. Create a tracking issue using the Issue template [Challenge Proposal](todo.md) for your challenge.
+1. Create a tracking issue using the Issue template [Challenge Proposal](template.md) for your challenge.
 2. In your fork of this repository do the following:
     1. Copy the template file (`book/src/challenge_template.md`) to `book/src/challenges/<ID_NUMBER>-<challenge-name>.md`.
     2. Fill in the details according to the template instructions.

doc/src/intrinsics-memory.md

@@ -0,0 +1,87 @@
+# Challenge 2: Verify the memory safery of core intrinsics using raw pointers
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/16)
+- **Start date:** *24/06/12*
+- **End date:** *24/12/10*
+
+-------------------
+
+
+## Goal
+
+Annotate Rust core::intrinsics functions that manipulate raw pointers with their safety contract. Verify their usage in the standard library is in fact safe.
+
+### Success Criteria
+
+1. All the following intrinsic functions must be annotated with safety contracts.
+2. Any fallback intrinsic implementation must be verified.
+3. For intrinsics modeled in the tool of choice, explain how their implementation matches the intrinsics definition. This can either be done in the PR description or as an entry to the contest book as part of the “Tools” chapter.
+4. For each function, contestants must state clearly the list of assumptions for each proof, how the proofs can be audited, and the list of (implicit and explicit) properties that are guaranteed.
+5. The verification of each intrinsic should ensure all the documented safety conditions are met, and that meeting them is enough to guarantee safe usage.
+
+
+Intrinsic functions to be annotated with safety contracts
+
+| Function | Location |
+|---------|---------|
+|typed_swap | core::intrisics |
+|vtable_size| core::intrisics |
+|vtable_align| core::intrisics |
+|copy_nonoverlapping| core::intrisics |
+|copy| core::intrisics |
+|write_bytes| core::intrisics |
+|size_of_val| core::intrisics |
+|arith_offset| core::intrisics |
+|volatile_copy_nonoverlapping_memory| core::intrisics |
+|volatile_copy_memory| core::intrisics |
+|volatile_set_memory| core::intrisics |
+|volatile_load| core::intrisics |
+|volatile_store| core::intrisics |
+|unaligned_volatile_load| core::intrisics |
+|unaligned_volatile_store| core::intrisics |
+|compare_bytes| core::intrisics |
+|min_align_of_val| core::intrisics |
+|ptr_offset_from| core::intrisics |
+|ptr_offset_from_unsigned| core::intrisics |
+|read_via_copy| core::intrisics |
+|write_via_move| core::intrisics |
+
+
+All the following usages of intrinsics were proven safe:
+
+| Function | Location |
+|---------|---------|
+|copy_from_slice	| core::slice |
+|parse_u64_into	| std::fmt |
+|swap | core::mem |
+|align_of_val | core::mem |
+|zeroed | core::mem::maybe_uninit |
+
+
+
+Annotate and verify all the functions that below that expose intrinsics with safety contracts
+
+| Function | Location |
+|---------|---------|
+|copy_from_slice	| std::ptr |
+|parse_u64_into	| std::ptr |
+|swap | std::ptr |
+|align_of_val | std::ptr |
+|zeroed | std::ptr |
+
+
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Invoking undefined behavior via compiler intrinsics.
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory except for padding or unions.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](general-rules.md)
+in addition to the ones listed above.

doc/src/template.md

@@ -1 +1,51 @@
-# Challenge Template
+# Challenge XXXX[^challenge_id]: Challenge Title
+
+- **Status:** *One of the following: [Open | Resolved | Expired]*
+- **Solution:** *Option field to point to the PR that solved this challenge.*
+- **Tracking Issue:** *Link to issue*
+- **Start date:** *YY/MM/DD*
+- **End date:** *YY/MM/DD*
+
+-------------------
+
+
+## Goal
+
+*Describe the goal of this challenge with 1-2 sentences.*
+
+## Motivation
+
+*Explain why this is a challenge that should be prioritized. Consider using a motivating example.*
+
+## Description
+
+*Describe the challenge in more details.*
+
+### Assumptions
+
+*Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".*
+
+### Success Criteria
+
+*Here are some examples of possible criteria:*
+
+All the following unsafe functions must be annotated with safety contracts and the contracts have been verified:
+
+| Function | Location |
+|---------|---------|
+|  abc   |  def    |
+
+At least N of the following usages were proven safe:
+
+| Function | Location |
+|---------|---------|
+|  xyz   |  123   |
+
+All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+*List of UBs*
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](general-rules.md)
+in addition to the ones listed above.
+
+[^challenge_id]: The number of the challenge sorted by publication date.

doc/src/tools.md

@@ -9,9 +9,9 @@ please see the [Tool Application](general-rules.md#tool-applications) section.
 
 ## Approved tools:
 
-| Tool      | CI Status |
-|-----------|-----------|
- | Kani     | TODO      |
+| Tool                | CI Status |
+|---------------------|-------|
+ | Kani Rust Verifier  | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml)      |
 
 
 

doc/src/tools/kani.md

@@ -1,7 +1,118 @@
 # 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/).
+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 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).
+
+## 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
+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::<i32>();
+    let b = kani::any::<i32>();
+    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
+
+```
+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 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 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 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`.
+
+``` 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() {
+        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 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.
+
+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:
+
+```
+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 information about how to install and how you can customize your use of Kani in the
+[Kani book](https://model-checking.github.io/kani/).