Merge branch 'main' into Add-copyright-file

.github/workflows/book.yml

@@ -2,16 +2,12 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 # This workflow is responsible for building and releasing the book.
-# It should only run when there has been a change to the book files
-# or via manual trigger.
 
 name: Build Book
 on:
   workflow_dispatch:
   pull_request:
-    paths:
-      - 'doc/**'
-      - '.github/workflows/book.yml'
+    branches: [ main ]
   push:
     paths:
       - 'doc/**'

.github/workflows/kani.yml

@@ -7,9 +7,7 @@ name: Kani
 on:
   workflow_dispatch:
   pull_request:
-    paths:
-      - 'library/**'
-      - '.github/workflows/kani.yml'
+    branches: [ main ]
   push:
     paths:
       - 'library/**'
@@ -26,6 +24,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 +44,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 +60,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

@@ -8,10 +8,7 @@ name: Rust Tests
 on:
   workflow_dispatch:
   pull_request:
-    paths:
-      - 'library/**'
-      - 'rust-toolchain.toml'
-      - '.github/workflows/rustc.yml'
+    branches: [ main ]
   push:
     paths:
       - 'library/**'
@@ -61,6 +58,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
 *~

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,4 +13,5 @@
 ---
 
 # Challenges
-- [Coming soon](./todo.md)
+- [Core Transmutation](./core-transmutation.md)
+- [Memory safety of core intrinsics](./intrinsics-memory.md)

doc/src/core-transmutation.md

@@ -0,0 +1,146 @@
+# Challenge 1: Verify `core` transmuting methods
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19)
+- **Start date:** 2024-06-12
+- **End date:** 2024-12-10
+
+-------------------
+
+## Goal
+
+Confirm the soundness of value transmutations performed by libcore, including those transmutations exposed as public methods provided by libcore. A value-to-value transmutation is sound if:
+1. the source value is a bit-valid instance of the destination type;
+2. violations of library safety invariants (e.g., invariants on a field's value) of the destination type are not violated by subsequent use of the transmuted value.
+
+If the context of the transmute is safe, these conditions should be proven with local reasoning. If the context of the transmute is unsafe, they may be discharged with a safety obligation on the caller.
+
+To keep the goal somewhat manageable, it excludes some classes of code (e.g., UTF8-validation, async tasks, and others); see the assumptions listed below for the full list of excluded categories.
+
+## Details
+
+### Motivating Example
+
+There are several calls to unsafe methods using transmute within the code of safe methods exported by libcore itself, so having clear and verifiable safety contracts is critical for verifying the safety of the safe methods that invoke them.
+
+For example, `std::slice::align_to` (which unsafely converts any slice `&[T]` into a tuple `(&[T], &[U], &[T])` composed of a prefix, a maximal sequence of values of type `U`, and a suffix) just says for its safety that “all the usual caveats pertaining to `transmute::<T, U>` also apply here”, which might be an under specification. For more details, see the [documentation](https://doc.rust-lang.org/std/mem/fn.transmute.html) for `transmute`.
+
+
+### Breaking-down the verification
+
+We lay out the verification challenge from the bottom up. Starting with the core implementation of `transmute` moving up to all unsafe and safe APIs that rely on it.
+
+#### Part I - The Two Intrinsics
+
+The public unsafe intrinsic [`transmute<T, U>`](https://doc.rust-lang.org/std/mem/fn.transmute.html) takes a value of type `T` and reinterprets it to have type `U`, with the sole (statically-enforced) restriction being that the types `T` and `U` must have the same size. The unstable intrinsic [`transmute_unchecked<T, U>`](https://doc.rust-lang.org/core/intrinsics/fn.transmute_unchecked.html) is similar, except that it removes the static size restriction, treating violations of it as undefined behavior.
+
+_What is the right way to encode the preconditions of the two transmutation intrinsics?_
+
+If one is solely concerned about safety: The [Rustonomicon](https://doc.rust-lang.org/nomicon/transmutes.html) lists several ways that transmutation can yield undefined behavior. Encoding a safety contract for transmute that captures all the relevant criteria laid out in the documentation is crucial.
+
+If one is concerned about proving functional correctness, then reasoning about transmutation will require reasoning about the byte representation of values to justify that the reinterpretation of the value’s bytes for satisfying the pending proof obligation associated with the output value.
+
+
+#### Part II - `unsafe` APIs with Validity Constraints
+
+There are unsafe methods (which are defined by libcore and reexported by libstd) that have the effect of a transmutation between a (sequence of) `T` and a (sequence of) `U`. Come up with an appropriate safety contract for each of them.
+
+
+#### Part III - `unsafe` APIs with Richer Constraints
+
+Similar to part 2, there are also unsafe methods, but now the safety condition is more complicated, such as “is valid ascii character” or "is valid unicode scalar value."
+
+#### Part IV - `safe` APIs
+
+These are safe APIs that call into the unsafe API's from parts 1 through 3 above. Now our final goal is to prove that they actually are safe, despite calling transmute or transmute-related methods in their implementations.
+
+### Assumptions
+
+For this challenge, the following assumptions are acceptable:
+
+We are not attempting to validate all details of the memory model for this challenge; for example, you do not need to worry about whether we are using the Stacked Borrows or Tree Borrows aliasing models. Likewise, you do not need to validate the provenance-related API in `std::ptr`.
+
+You are allowed, but not required, to leverage the unstable `Transmutability` trait under development as part of your solution. This is a libstd-internal feature for auditing whether a given transmutation is safe. (It seems like something tools should try to leverage in some way; but it is also experimental.) Note that if you need to add new impls of `Transmutability`, then those new impl’s need to be accepted by (and landed in) the upstream Rust project before your solution can be considered completed. See also https://github.com/rust-lang/rust/issues/99571
+
+You do not need to verify the correctness of the transmute calls in the unit tests embedded in libcore, though it would be great to do so!
+
+To keep the goal somewhat manageable, we are omitting the following classes of code from the acceptance criteria for this challenge:
+ * utf8-validation (such as `str::from_utf8_unchecked`)
+ * the provenance-related API in `std::ptr` (such as `addr`, or `without_provenance`)
+ * the num methods (from modules like `core::num::f64`, `core::num::i32`, etc)
+ * pointer-metadata and vtable APIs (from modules like `core::ptr::metadata`)
+ * async rust runtime/task API (from `core::task`)
+ * core-internal specialization methods (such as traits like `RangeIteratorImpl` with methods prefixed with "spec_")
+ * core-internal `__iterator_get_unchecked` calls
+ * value output formatting machinery (from `std::fmt::rt`)
+ You do not need to verify those (potentially indirect) uses of transmute,  unless you need to establish the safety/correctness of some of those methods in order to verify some other type in this list. (That is, you cannot assume them to be safe nor correct in your verification of other methods listed here.) We expect to issue future challenges tailored to each of the categories of transmutation uses listed above.
+
+
+## Success Criteria
+
+A new entry to the specification book is created explaining the relevant patterns for verifying code that calls transmute.
+
+At least 35 of the following 47 intrinsics and functions (i.e. approximately 75%) have been annotated with contracts, and, for non-intrinsics, had their bodies verified.
+
+For the safe functions, you do not need to provide a full-functional correctness specification; it will suffice to add pre- and post-conditions (i.e. assumptions and assertions) around the relevant part of the code that calls the transmutation-related unsafe function or intrinsic.
+
+
+| Function              | Location          |
+|-----------------------|-------------------|
+| `transmute_unchecked` | `core::intrinsics` |
+| `transmute`           | `core::intrinsics` |
+| `MaybeUninit<T>::array_assume_init`    | `core::mem` |
+| `MaybeUninit<[T; N]>::transpose`       | `core::mem` |
+| `<[MaybeUninit<T>; N]>::transpose`     | `core::mem` |
+| `<[T; N] as IntoIterator>::into_iter`  | `core::array::iter` |
+| `BorrowedBuf::unfilled`    | `core::io::borrowed_buf` |
+| `BorrowedCursor::reborrow` | `core::io::borrowed_buf` |
+| `str::as_bytes`            | `core::str` |
+| `from_u32_unchecked`       | `core::char::convert` |
+| `char_try_from_u32`        | `core::char::convert` |
+| `Ipv6Addr::new`       | `core::net::ip_addr` |
+| `Ipv6Addr::segments`  | `core::net::ip_addr` |
+| `align_offset`        | `core::ptr`        |
+| `Alignment::new_unchecked` | `core::ptr::alignment` |
+| `MaybeUninit<T>::copy_from_slice` | `core::mem` |
+| `str::as_bytes_mut`        | `core::str` |
+| `<Filter<I,P> as Iterator>::next_chunk` | `core::iter::adapters` |
+| `<FilterMap<I,F> as Iterator>::next_chunk` | `core::iter::adapters` |
+| `try_from_fn` | `core::array` |
+| `iter_next_chunk` | `core::array` |
+| `from_u32_unchecked`            | `core::char`       |
+| `AsciiChar::from_u8_unchecked`  | `core::ascii_char` |
+| `memchr_aligned`  | `core::slice::memchr` |
+| `<[T]>::align_to_mut` | `core::slice`     |
+| `run_utf8_validation` | `core::str::validations` |
+| `<[T]>::align_to`     | `core::slice` |
+| `is_aligned_to`       | `core::const_ptr` |
+| `is_aligned_to`       | `core::mut_ptr`   |
+| `Alignment::new`      | `core::ptr::alignment` |
+| `Layout::from_size_align`           | `core::alloc::layout` |
+| `Layout::from_size_align_unchecked` | `core::alloc::layout` |
+| `make_ascii_lowercase` | `core::str` |
+| `make_ascii_uppercase` | `core::str` |
+| `<char as Step>::forward_checked` | `core::iter::range` |
+| `<Chars as Iterator>::next`                 | `core::str::iter` |
+| `<Chars as DoubleEndedIterator>::next_back` | `core::str::iter` |
+| `char::encode_utf16_raw` | `core::char` |
+| `<char as Step>::backward_unchecked` | `core::iter::range` |
+| `<char as Step>::forward_unchecked`  | `core::iter::range` |
+| `AsciiChar::from_u8` | `core::ascii_char` |
+| `char::as_ascii` | `core::char` |
+| `<[T]>::as_simd_mut` | `core::slice` |
+| `<[T]>::as_simd`     | `core::slice` |
+| `memrchr` | `core::slice::memchr` |
+| `do_count_chars` | `str::count` |
+
+
+* All solutions to verification challenges need to satisfy the criteria established in the [challenge book](https://model-checking.github.io/verify-rust-std/general-rules.html) in addition to the ones listed below
+
+## Appendix A: The list construction
+
+The list of methods and intrinsics was gathered by surveying the call-graph (solely within the libcore source) of function bodies that could eventually invoke `transmute` or `transmute_unchecked`. For each caller: if the caller was itself `unsafe`, then its callers were then surveyed; if the caller was not `unsafe`, then it was treated as an end point for the survey.
+
+As mentioned in the assumptions, some (large) classes of methods were omitted from the challenge, either because 1. they encompassed a large API surface (e.g. `core::num`) that deserved separate treatment, 2. they had an enormous number of callers that would deserve separate treatment (e.g. `core::str::from_utf8_unchecked`), or 3. they interact with aspects of the Rust memory model that still need to be better understood by reasoning tools (e.g. the provenance APIs).
+
+You can see the [call graph produced by the survey here](https://hackmd.io/PYQNIL_aTxK0N6-AltxfbQ).

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.