Verify Rust Standard Library Effort

The Verify Rust Standard Library effort is an ongoing investment that targets the verification of the Rust standard library. The goal of this is to provide automated verification that can be used to verify that a given Rust standard library implementation is safe.

Verifying the Rust libraries is difficult because:

1. Lack of a specification,
2. Lack of an existing verification mechanism in the Rust ecosystem,
3. The large size of the verification problem,
4. The unknowns of scalable verification.

Given the magnitude and scope of the effort, we believe this should be a community owned effort. For that, we are launching a contest that includes a series of challenges that focus on verifying memory safety and a subset of undefined behaviors in the Rust standard library.

Efforts are largely classified in the following areas:

1. Contributing to the core mechanism of verifying the rust standard library
2. Creating new techniques to perform scalable verification
3. Apply techniques to verify previously unverified parts of the standard library.

There is a financial award tied to each challenge per its specification, which is awarded upon its successful completion.

We encourage everyone to watch this repository to be notified of any changes.

General Rules

Terms / Concepts

Verification Target: Our repository is a fork of the original Rust repository, and we kept a copy of the Rust standard library inside the library/ folder that shall be used as the verification target for all our challenges. We will periodically update the library/ folder to track newer versions of the official Rust standard library.

Challenges: Each individual verification effort will have a tracking issue where contributors can add comments and ask clarification questions. You can find the list of open challenges here.

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.

Basic Workflow

1. A verification effort will be published in the repository with appropriate details, and a tracking issue labeled with “Challenge” will be opened, so it can be used for clarifications and questions, as well as to track the status of the challenge.

2. Participants should create a fork of the repository where they will implement their proposed solution.

3. Once they submit their solution for analysis, participants should create a PR against the repository for analysis. Please make sure your solution meets the minimum requirements described here.

4. Each contribution will be reviewed on a first come, first served basis. Acceptance will be based on a review by a committee.

5. Once approved by the review committee, the change will be merged into the repository.

Solution Requirements

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.
• 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.
• All tools used by the solution must be in the list of accepted tools, and previously integrated in the repository. If that is not the case, please submit a separate tool application first.
• There is no restriction on the number of contributors for a solution. Make sure you have the rights to submit your solution and that all contributors are properly mentioned.
• The solution cannot impact the runtime logic of the standard library unless the change is proposed and incorporated into the Rust standard library.

Any exception to these requirements will only be considered if it is specified as part of the acceptance criteria of the challenged being solved.

Call for Challenges

The goal of the effort is to enable the verification of the entire Rust standard library. The type of obstacles users face may depend on which part of the standard library you would like to verify. Thus, our challenges are developed with the target of verifying a specific section of the standard library or strengthening existing verification.

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 challenge template 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.
   3. Add a link to the new challenge inside book/src/SUMMARY.md
   4. Submit a pull request.
3. Address any feedback in the pull request.
4. If approved, we will publish your challenge and add the “Challenge” label to the tracking issue.

Tool Applications

Solutions must be automated using one of the tools previously approved and listed here. To use a new tool, participants must first submit an application for it.

• To submit a tool application, open a new issue in this repository using the "Tool Application" issue template.
• The committee will review the application. Once a committee member approves the application, the participant needs to create a PR with:
  • A new workflow that runs the tool against the standard library.
  • A new entry to the “Approved Tools” section of this book.
• Once this PR is merged, the tool is considered integrated, and the tool application issue will be closed.

The repository will be updated periodically, which can impact a tool's capacity to analyze the new version of the repository (i.e., the workflow may no longer pass after an update). If it is determined that the tool requires changes and such changes cannot be provided in a timely fashion the tool's approval may be revoked.

Committee Applications

You can apply to be part of the committee by submitting a pull request that adds your GitHub login name to the pull_request.toml file.

For example, if your user login is @rahulku, add the login without @ to the committee member's list,

[committee]
members = [
+   "rahulku"
]

Committee members are expected to contribute by reviewing pull requests (all pull requests review approvals from at least two committee members before they can be merged). Reviews of solutions towards challenges should consider at least the following aspects:

1. Does the pull request implement a solution that respects/meets the success criteria of the challenge?
2. Do the contracts and harnesses incorporate the safety conditions stated in the documentation (from comments in the code and the standard library documentation)? Note that we currently focus on safety verification. Pre- and post-conditions towards functional correctness are acceptable as long as they do not negatively impact verification of safety, such as over-constraining input values or causing excessive verification run time.
3. Is the contributed code of adequate quality, idiomatic, and stands a chance to be accepted into the standard library (to the best of the committee member's knowledge)?

Challenge XXXX1: 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: YYYY/MM/DD
• End date: YYYY/MM/DD
• Reward: TBD²

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:

At least N of the following usages were proven safe:

All proofs must automatically ensure the absence of the following undefined behaviors ref:

List of UBs

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

The following form is designed to provide information for your tool that should be included in the effort to verify the Rust standard library. Please note that the tool will need to be supported if it is to be included.

Tool Name

Please enter your tool name here.

Description

Please enter a description for your tool and any information you deem relevant.

Tool Information

• Does the tool perform Rust verification?
• Does the tool deal with unsafe Rust code?
• Does the tool run independently in CI?
• Is the tool open source?
• Is the tool under development?
• Will you or your team be able to provide support for the tool?

Comparison to Other Approved Tools

Describe how this tool compares to the other approved tools. For example, are there certain properties that this tool can prove that the other tools cannot? The comparison does not need to be exhaustive; the purpose of this section is for the committee to understand the salient differences, and how this tool would fit into the larger effort.

Licenses

Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s).

Steps to Use the Tool

1. [First Step]
2. [Second Step]
3. [and so on...]

Artifacts & Audit Mechanisms

If there are noteworthy examples of using the tool to perform verification, please include them in this section. Links, papers, etc. Also include mechanisms for the committee to audit the implementation and correctness of this tool (e.g., regression tests).

Versioning

Please describe how you version the tool.

CI

If your tool is approved, you will be responsible merging a workflow into this repository that runs your tool against the standard library. For an example, see the Kani workflow (.github/workflows/kani.yml). Describe, at a high level, how your workflow will operate. (E.g., how will you package the tool to run in CI, how will you identify which proofs to run?).

Verification Tools

The verification tool ecosystem for Rust is rapidly growing, and we welcome the usage of different tools to solve our challenges. In this chapter, you can find a list of tools that have already been approved for new solutions, what is their CI current status, as well as more details on how to use them.

If you would like to add a new tool to the list of tool applications, please see the Tool Application section.

Approved tools:

Tool	CI Status
Kani Rust Verifier

Kani Rust Verifier

The Kani Rust Verifier 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 the installation section of the Kani book.

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

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.

For a more detailed tutorial, you can refer to the tutorial section of the Kani book.

Using Kani to verify the Rust 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

Create a local copy of the model-checking fork 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 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 it in a different (existing) file in the core library instead.

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
pub mod verify {
    use crate::kani;

    #[kani::proof]
    pub fn harness_introduction() {
        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 Kani script on the std library

To aid the Rust Standard Library verification effort, Kani provides a script out of the box to help you get started. Run the following command in your local terminal from the verify repository root:

./scripts/run-kani.sh --path .

To pass kani arguments such as --harness, you can run the script with --kani-args and continue passing in all the necessary arguments:

./scripts/run-kani.sh --path . --kani-args --harness alloc::layout::verify::check_array_i32 --output-format=terse

The script run-kani installs the right version of Kani for you, builds it and then finally runs the verify-std sub-command of the kani with some default flags.

NOTE: This script may crash due to linking issues. If the script fails with an error message related to linking, link the new CBMC version, delete the ./kani_build directory and re-run.

Step 3 - Check verification result

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.

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.

./scripts/run-kani.sh --kani-args --harness harness_introduction

This gives you the verification result for just harness_introduction from the aforementioned 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.

Now you can write proof harnesses to verify specific functions in the library. The current convention is to keep proofs in the same module file of the verification target.

To run Kani for an individual proof, use --harness [harness_function_name]. Note that Kani will batch run all proofs in the library folder if you do not supply the --harness flag.

If Kani returns the error no harnesses matched the harness filter, you can give the full name of the harness. For example, to run the proof harness named check_new in library/core/src/ptr/unique.rs, use --harness ptr::unique::verify::check_new. To run all proofs in unique.rs, use --harness ptr::unique::verify.

To find the full name of a harness, check the Kani output and find the line starting with Checking harness [harness full name].

More details

You can find more information about how to install and how you can customize your use of Kani in the Kani book.

This chapter contains all existing challenges, including the ones that have already been solved or expired.

For the most up-to-date information on a challenge status, please check their tracking issue linked in the challenge description.

If you would like to submit a new challenge, please see "Call for Challenges" section.

Challenge 1: Verify core transmuting methods

• Status: Open
• Tracking Issue: #19
• Start date: 2024/06/12
• End date: 2025/04/10
• Reward: N/A

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 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> 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> 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 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.

• All solutions to verification challenges need to satisfy the criteria established in the challenge book 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.

Challenge 2: Verify the memory safety of core intrinsics using raw pointers

• Status: Open
• Tracking Issue: #16
• Start date: 2024/06/12
• End date: 2025/04/10
• Reward: N/A

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

All the following usages of intrinsics were proven safe:

Annotate and verify all the functions below that expose intrinsics with safety contracts

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors ref:

• 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 in addition to the ones listed above.

Challenge 3: Verifying Raw Pointer Arithmetic Operations

• Status: Resolved
• Tracking Issue: #76
• Start date: 2024/06/24
• End date: 2024/12/11
• Reward: N/A
• Contributors: Surya Togaru, Yifei Wang, Szu-Yu Lee, Mayuresh Joshi

Goal

The goal of this challenge is to verify safety of code that relies on raw pointer arithmetic, and eventual raw pointer access.

Motivation

Raw pointer arithmetic is a common operation employed in the implementation of highly optimized code, as well as containers with dynamic size. Examples of the former are str::repeat, [u8]::is_ascii, while for the latter we have Vec, VecDeque, HashMap.

These unsafe operations are usually abstracted from the end user with the usage of safe abstractions. However, bugs in these abstractions may compromise entire applications, potentially becoming a security concern. See CVE-2018-1000810 for an example of an issue with an optimization of str::repeat.

These safe abstractions are great candidates for software verification. They are critical for Rust applications safety, and they are modular by design.

Description

Rust provides different options for pointer arithmetic, which have different semantics when it comes to safety. For example, methods such as ptr::offset, ptr::add, and ptr::sub are unsafe, and one of their safety conditions is that:

• Both the starting and resulting pointer must be either in bounds or one byte past the end of the same allocated object.

I.e., violating this safety condition triggers immediate UB.

On the other hand, wrapping operations such as ptr::wrapping_offset, ptr::wrapping_add, ptr::wrapping_sub, are safe, however, the resulting pointer must not be used to read or write other allocated objects.

Thus, we would like to be able to verify usage of these different methods within the standard library to ensure they are safely employed, as well as provide function contracts that can be used by other Rust crates to verify their own usage of these methods.

Assumptions

For this challenge, we do not require a full proof that is independent of the pointee type T. Instead, we require that the verification is done for the following pointee types:

1. All integer types.
2. At least one dyn Trait.
3. At least one slice.
4. For unit type.
5. At least one composite type with multiple non-ZST fields.

Success Criteria

All the following unsafe functions must be annotated with safety contracts and the contracts have been verified:

At least 3 of the following usages were proven safe:

All proofs must automatically ensure the absence of the following undefined behaviors ref:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Performing a place projection that violates the requirements of in-bounds pointer arithmetic. A place projection is a field expression, a tuple index expression, or an array/slice index expression.
• Invoking undefined behavior via compiler intrinsics.
• Producing an invalid value, even in private fields and locals.

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 4: Memory safety of BTreeMap's btree::node module

• Status: Open
• Tracking Issue: #77
• Start date: 2024/07/01
• End date: 2025/04/10
• Reward: 10,000 USD

Goal

Verify the memory safety of the alloc::collections::btree::node module. This is one of the main modules used for implementing the BTreeMap collection, and it includes a lot of unsafe code.

Success Criteria

The memory safety of all public functions (especially safe ones) containing unsafe code must be verified, e.g.:

1. LeafNode::new
2. NodeRef::as_internal_mut
3. NodeRef::len
4. NodeRef::ascend
5. NodeRef::first_edge
6. NodeRef::last_edge
7. NodeRef::first_kv
8. NodeRef::last_kv
9. NodeRef::into_leaf
10. NodeRef::keys
11. NodeRef::as_leaf_mut
12. NodeRef::into_leaf_mut
13. NodeRef::as_leaf_dying
14. NodeRef::pop_internal_level
15. NodeRef::push
16. Handle::left_edge
17. Handle::right_edge
18. Handle::left_kv
19. Handle::right_kv
20. Handle::descend
21. Handle::into_kv
22. Handle::key_mut
23. Handle::into_val_mut
24. Handle::into_kv_mut
25. Handle::into_kv_valmut
26. Handle::kv_mut

Verification must be unbounded for functions that use recursion or contain loops, e.g.

1. NodeRef::new_internal
2. Handle::insert_recursing
3. BalancingContext::do_merge
4. BalancingContext::merge_tracking_child_edge
5. BalancingContext::steal_left
6. BalancingContext::steal_right
7. BalancingContext::bulk_steal_left
8. BalancingContext::bulk_steal_right

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 5: Verify functions iterating over inductive data type: linked_list

• Status: Open
• Tracking Issue: #29
• Start date: 2024/07/01
• End date: 2025/04/10
• Reward: 5,000 USD

Goal

Verify the memory safety of alloc::collections::linked_list functions that iterate over its internal inductive-defined data type.

Details

The internal representations of linked_list are bi-direction linked list nodes. To unboundedly prove the memory safety of functions that iterating over such inductive-defined data type, we need to illustrate the memory safety for linked lists of arbitrary shape. On the other hand, if we can only prove the memory safety for certain shapes of linked lists, how should we specify the precondition---the assumptions on the shape of the inductive-defined data type---of such functions.

Success Criteria

The memory safety of the following public functions that iterating over the internal inductive data type must be verified:

The verification must be unbounded---it must hold for linked lists of arbitrary shape.

It is OK to assume that the generic type T of the proofs is primitive types, e.g., i32, u32, bool, etc.

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors ref:

• 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 in addition to the ones listed above.

Challenge 6: Safety of NonNull

• Status: Open
• Tracking Issue: #53
• Start date: 2024/08/16
• End date: 2025/04/10
• Reward: N/A

Goal

Verify absence of undefined behavior of the ptr::NonNull module. Most of its functions are marked unsafe, yet they are used in 62 other modules of the standard library.

Success Criteria

Prove absence of undefined behavior of the following 48 public functions. You may wish to do so by attaching pre- and postconditions to these, and then (if needed by the tooling that you choose to use) adding verification harnesses.

1. NonNull<T>::add
2. NonNull<T>::addr
3. NonNull<T>::align_offset
4. NonNull<T>::as_mut<'a>
5. NonNull<T>::as_mut_ptr
6. NonNull<T>::as_non_null_ptr
7. NonNull<T>::as_ptr
8. NonNull<T>::as_ref<'a>
9. NonNull<T>::as_uninit_mut<'a>
10. NonNull<T>::as_uninit_ref<'a>
11. NonNull<T>::as_uninit_slice<'a>
12. NonNull<T>::as_uninit_slice_mut<'a>
13. NonNull<T>::byte_add
14. NonNull<T>::byte_offset_from<U: ?Sized>
15. NonNull<T>::byte_offset
16. NonNull<T>::byte_sub
17. NonNull<T>::cast<U>
18. NonNull<T>::copy_from_nonoverlapping
19. NonNull<T>::copy_from
20. NonNull<T>::copy_to_nonoverlapping
21. NonNull<T>::copy_to
22. NonNull<T>::dangling
23. NonNull<T>::drop_in_place
24. NonNull<T>::from_raw_parts
25. NonNull<T>::get_unchecked_mut<I>
26. NonNull<T>::is_aligned_to
27. NonNull<T>::is_aligned
28. NonNull<T>::is_empty
29. NonNull<T>::len
30. NonNull<T>::map_addr
31. NonNull<T>::new_unchecked
32. NonNull<T>::new
33. NonNull<T>::offset_from
34. NonNull<T>::offset
35. NonNull<T>::read_unaligned
36. NonNull<T>::read_volatile
37. NonNull<T>::read
38. NonNull<T>::replace
39. NonNull<T>::slice_from_raw_parts
40. NonNull<T>::sub_ptr
41. NonNull<T>::sub
42. NonNull<T>::swap
43. NonNull<T>::to_raw_parts
44. NonNull<T>::with_addr
45. NonNull<T>::write_bytes
46. NonNull<T>::write_unaligned
47. NonNull<T>::write_volatile
48. NonNull<T>::write

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 7: Safety of Methods for Atomic Types & Atomic Intrinsics

• Status: Open
• Tracking Issue: #83
• Start date: 2024/10/30
• End date: 2025/04/10
• Reward: 10,000 USD

Goal

core::sync::atomic provides methods that operate on atomic types. For example, AtomicBool::store(&self, val: bool, order: Ordering) stores val in the atomic boolean referenced by self according to the specified atomic memory ordering.

The goal of this challenge is to verify that these methods are safe.¹

Success Criteria

Part 1: Unsafe Methods

First, verify that the unsafe from_ptr methods are safe, given that their safety preconditions are met.

Write safety contracts for each of the from_ptr methods:

• AtomicBool::from_ptr
• AtomicPtr::from_ptr
• AtomicI8::from_ptr
• AtomicU8::from_ptr
• AtomicI16::from_ptr
• AtomicU16::from_ptr
• AtomicI32::from_ptr
• AtomicU32::from_ptr
• AtomicI64::from_ptr
• AtomicU64::from_ptr
• AtomicI128::from_ptr
• AtomicU128::from_ptr

Specifically, encode the conditions about ptr's alignment and validity (marked #Safety in the methods' documentation) as preconditions. Then, verify that the methods are safe for all possible values for the type that ptr points to, given that ptr satisfies those preconditions.

For example, AtomicI8::from_ptr is defined as:

/// `ptr` must be [valid] ... (comment continues; omitted for brevity)
pub const unsafe fn from_ptr<'a>(ptr: *mut i8) -> &'a AtomicI8 {
    // SAFETY: guaranteed by the caller
    unsafe { &*ptr.cast() }
}

To verify this method, first encode the safety comments (e.g., about pointer validity) as preconditions, then verify the absence of undefined behavior for all possible i8 values.

For the AtomicPtr case only, we do not require that you verify safety for all possible types. Concretely, below is the type signature for AtomicPtr::from_ptr:

pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr<T>

The type pointed to is a *mut T. Verify that for any arbitrary value for this *mut T (i.e., any arbitrary memory address), the method is safe. However, you need not verify the method for all possible instantiations of T. It suffices to verify this method for T of byte sizes 0, 1, 2, 4, and at least one non-power of two.

Part 2: Safe Abstractions

The atomic types expose safe abstractions for atomic operations. In this part, you will work toward verifying that these abstractions are indeed safe by writing and verifying safety contracts for the unsafe code in their bodies.

For example, AtomicBool::store is the (public) safe method that atomically updates the boolean's value. This method invokes the unsafe function atomic_store, which in turn calls intrinsics::atomic_store_relaxed, intrinsics::atomic_store_release, or intrinsics::atomic_store_seqcst, depending on the provided ordering.

Write and verify safety contracts for the unsafe functions:

• atomic_store
• atomic_load
• atomic_swap
• atomic_add
• atomic_sub
• atomic_compare_exchange
• atomic_compare_exchange_weak
• atomic_and
• atomic_nand
• atomic_or
• atomic_xor
• atomic_max
• atomic_umax
• atomic_umin

Then, for each of the safe abstractions that invoke the unsafe functions listed above, write contracts that ensure that they are not invoked with orders that would cause panics.

For example, atomic_store panics if invoked with Acquire or AcqRel ordering. In this case, you would write contracts on the safe store methods that enforce that they are not called with either of those orders.

Part 3: Atomic Intrinsics

Write and verify safety contracts for the intrinsics invoked by the unsafe functions from Part 2 (in core::intrinsics):

List of UBs

In addition to any safety properties mentioned in the API documentation, all proofs must automatically ensure the absence of the following undefined behaviors:

• Data races.
• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Invoking undefined behavior via compiler intrinsics.
• Producing an invalid value.

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 8: Contracts for SmallSort

• Status: Open
• Tracking Issue: #56
• Start date: 2024/08/17
• End date: 2025/04/10
• Reward: 10,000 USD

Goal

The implementations of the traits StableSmallSortTypeImpl, UnstableSmallSortTypeImpl, and UnstableSmallSortFreezeTypeImpl in the smallsort module of the Rust standard library are the sorting algorithms optimized for slices with small lengths. In this challenge, the goal is to, first prove the memory safety of the public functions in the smallsort module, and, second, write contracts for them to show that the sorting algorithms actually sort the slices.

Success Criteria

Prove absence of undefined behavior of the following public functions.

1. <T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort
2. <T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort
3. <T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort
4. slice::sort::shared::smallsort::swap_if_less
5. slice::sort::shared::smallsort::insertion_sort_shift_left
6. slice::sort::shared::smallsort::sort4_stable
7. slice::sort::shared::smallsort::has_efficient_in_place_swap

Write contracts for the following public functions that show that they actually sort the slices.

1. <T as slice::sort::shared::smallsort::StableSmallSortTypeImpl>::small_sort
2. <T as slice::sort::shared::smallsort::UnstableSmallSortTypeImpl>::small_sort
3. <T as slice::sort::shared::smallsort::UnstableSmallSortFreezeTypeImpl>::small_sort

The memory safety and the contracts of the above listed functions must be verified for all possible slices with arbitrary valid length.

Note that most of the functions listed above call functions that contain loops. Function contracts and loop contracts of those callee functions may be required.

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 9: Safe abstractions for core::time::Duration

• Status: Resolved
• Tracking Issue: #72
• Start date: 2024/08/20
• End date: 2024/12/10
• Reward: N/A
• Contributors: Samuel Thomas and Cole Vick

Goal

Write function contracts for core::time::Duration that can be used as safe abstractions. Even though the majority of Duration methods are safe, many of them are safe abstractions over unsafe code.

For instance, the new method is implemented as follows in v1.3.0:

pub const fn new(secs: u64, nanos: u32) -> Duration {
    if nanos < NANOS_PER_SEC {
        // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
        Duration { secs, nanos: unsafe { Nanoseconds(nanos) } }
    } else {
        let secs = match secs.checked_add((nanos / NANOS_PER_SEC) as u64) {
            Some(secs) => secs,
            None => panic!("overflow in Duration::new"),
        };
        let nanos = nanos % NANOS_PER_SEC;
        // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
        Duration { secs, nanos: unsafe { Nanoseconds(nanos) } }
    }
}

Success Criteria

Write a type invariant for the struct Duration. Write function contracts for the following public functions.

1. Duration::new(secs: u64, nanos: u32) -> Duration

2. Duration::from_secs(secs: u64) -> Duration

3. Duration::from_millis(millis: u64) -> Duration

4. Duration::from_micros(micros: u64) -> Duration

5. Duration::from_nanos(nanos: u64) -> Duration

6. Duration::as_secs(&self) -> u64

7. Duration::as_millis(&self) -> u128

8. Duration::as_micros(&self) -> u128

9. Duration::as_nanos(&self) -> u128

10. Duration::subsec_millis(&self) -> u32

11. Duration::subsec_micros(&self) -> u32

12. Duration::subsec_nanos(&self) -> u32

13. Duration::checked_add(&self, rhs: Duration) -> Option<Duration>

14. Duration::checked_sub(&self, rhs: Duration) -> Option<Duration>

15. Duration::checked_mul(&self, rhs: u32) -> Option<Duration>

16. Duration::checked_div(&self, rhs: u32) -> Option<Duration>

The memory safety and the contracts of the above listed functions must be verified for all possible input values.

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 10: Memory safety of String

• Status: Open
• Tracking Issue: #61
• Start date: 2024/08/19
• End date: 2025/04/10
• Reward: N/A

Goal

In this challenge, the goal is to verify the memory safety of std::string::String. Even though the majority of String methods are safe, many of them are safe abstractions over unsafe code.

For instance, the insert method is implemented as follows in v1.80.1:

pub fn insert(&mut self, idx: usize, ch: char) {
    assert!(self.is_char_boundary(idx));
    let mut bits = [0; 4];
    let bits = ch.encode_utf8(&mut bits).as_bytes();

    unsafe {
        self.insert_bytes(idx, bits);
    }
}

where insert_bytes has the following implementation:

unsafe fn insert_bytes(&mut self, idx: usize, bytes: &[u8]) {
    let len = self.len();
    let amt = bytes.len();
    self.vec.reserve(amt);

    unsafe {
        ptr::copy(self.vec.as_ptr().add(idx), self.vec.as_mut_ptr().add(idx + amt), len - idx);
        ptr::copy_nonoverlapping(bytes.as_ptr(), self.vec.as_mut_ptr().add(idx), amt);
        self.vec.set_len(len + amt);
    }
}

The call to the unsafe insert_bytes method (which itself contains unsafe code) makes insert susceptible to undefined behavior.

Success Criteria

Verify the memory safety of all public functions that are safe abstractions over unsafe code:

1. from_utf16le (unbounded)
2. from_utf16le_lossy(unbounded)
3. from_utf16be (unbounded)
4. from_utf16be_lossy (unbounded)
5. pop
6. remove
7. remove_matches (unbounded)
8. retain (unbounded)
9. insert
10. insert_str (unbounded)
11. split_off (unbounded)
12. drain
13. replace_range (unbounded)
14. into_boxed_str
15. leak

Ones marked as unbounded must be verified for any string/slice length.

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 11: Safety of Methods for Numeric Primitive Types

• Status: Resolved
• Tracking Issue: #59
• Start date: 2024/08/20
• End date: 2024/12/04
• Reward: N/A
• Contributors: Rajath M Kotyal, Yen-Yun Wu, Lanfei Ma, Junfeng Jin

Goal

Verify the safety of public unsafe methods for floats and integers in core::num.

To find the documentation for these methods, navigate first to the core::num documentation, then click on the appropriate primitive type in the left-side menu bar. For example, for i8::unchecked_add, click on i8.

Success Criteria

Part 1: Unsafe Integer Methods

Prove the absence of arithmetic overflow/underflow and undefined behavior in the following methods for each of the listed integer types, given that their safety preconditions are satisfied:

Part 2: Safe API Verification

Now, verify some of the safe APIs that leverage the unsafe integer methods from Part 1. Verify the absence of arithmetic overflow/underflow and undefined behavior of the following methods for each of the listed integer types:

Part 3: Float to Integer Conversion

Verify the absence of arithmetic overflow/underflow and undefined behavior in to_int_unchecked for f16, f32, f64, and f128.

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors:

• Invoking undefined behavior via compiler intrinsics.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value.

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 12: Safety of NonZero

• Status: Open
• Tracking Issue: #71
• Start date: 2024/08/23
• End date: 2025/04/10
• Reward: N/A

Goal

Verify the safety of NonZero in core::num.

Assumptions

new and get leverage transmute_unchecked, so verifying the safety of these methods would require verifying that transmutations are safe. This task is out of scope for this challenge (instead, it's work for Challenge 1). For this challenge, for a transmutation from type T to type U, it suffices to write and verify a contract that T and U have the same size.

You may assume that each NonZeroInner type upholds the safety conditions of the ZeroablePrimitive trait. Specifically, you need not verify that the integer primitives which implement ZeroablePrimitive are valid when 0, or that transmutations to the Option type are sound.

Success Criteria

Part 1: new and new_unchecked

Verify the safety and correctness of NonZero::new and NonZero::new_unchecked.

Specifically, write and verify contracts specifying the following:

1. The preconditions specified by the SAFETY comments are upheld.
2. For an input n:
   a. A NonZero object is created if and only if the input was nonzero.
   b. The value of the NonZeroInner object equals n.

Part 2: Other Uses of unsafe

Verify the safety of the following functions and methods (all located within core::num::nonzero):

You are not required to write correctness contracts for these methods (e.g., for max, ensuring that the result is indeed the maximum of the inputs), but it would be great to do so!

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors ref:

• Invoking undefined behavior via compiler intrinsics.
• Reading from uninitialized memory.
• Producing an invalid value.

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 13: Safety of CStr

• Status: Open
• Solution:
• Tracking Issue: #150
• Start date: 2024/11/04
• End date: 2025/04/10
• Reward: N/A

Goal

Verify that CStr safely represents a borrowed reference to a null-terminated array of bytes sequences similar to the C string representation.

Motivation

The CStr structure is meant to be used to build safe wrappers of FFI functions that may leverage CStr::as_ptr and the unsafe CStr::from_ptr constructor to provide a safe interface to other consumers. It provides safe methods to convert CStr to a Rust &str by performing UTF-8 validation, or into an owned CString.

Any issue with this structure or misusage of its unsafe methods could trigger an invalid memory access, which poses a security risk for their users.

Description

The goal of this challenge is to ensure the safety of the CStr struct implementation. First, we need to specify a safety invariant that captures the essential safety properties that must be maintained.

Next, we should verify that all the safe, public methods respect this invariant. For example, we can check that creating a CStr from a byte slice with method from_bytes_with_nul will only yield safe values of CStr.

Finally, for unsafe methods like from_ptr() and from_bytes_with_nul_unchecked, we need to specify appropriate safety contracts. These contracts should ensure no undefined behavior occurs within the unsafe methods themselves, and that they maintain the overall safety invariant of CStr when called correctly.

Assumptions

• Harnesses may be bounded.

Success Criteria

1. Implement the Invariant trait for CStr.

2. Verify that the CStr safety invariant holds after calling any of the following public safe methods.

3. Annotate and verify the safety contracts for the following unsafe functions:

4. Verify that the following trait implementations for the CStr type are safe:

All proofs must automatically ensure the absence of the following undefined behaviors ref:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Performing a place projection that violates the requirements of in-bounds pointer arithmetic.
• Mutating immutable bytes.
• Accessing uninitialized memory.

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

Challenge 14: Safety of Primitive Conversions

• Status: Open
• Tracking Issue: https://github.com/model-checking/verify-rust-std/issues/220
• Start date: 2024/12/15
• End date: 2025/2/28
• Prize: TBD

Goal

Verify the safety of number conversions in core::convert::num.

There are two conversions that use unsafe code: conversion from NonZero integer to NonZero integer and conversion from floating point number to integer. All conversions use macros to implement traits for primitive types in bulk. You will need to add contracts into the macros so that contracts are generated for each implementation. As the conversions are all macro generated, it is probably a good idea to write your own macro for generating the harnesses.

Success Criteria

NonZero Conversions

Write a type invariant for core::num::NonZero, then write harnesses for all nonzero conversions.

Write proof contracts for each NonZero primitive conversion, listed in full below. These conversions are implemented through two macros: impl_nonzero_int_from_nonzero_int! and impl_nonzero_int_try_from_nonzero_int!.

For each invocation of impl_nonzero_int_from_nonzero_int!, prove that the conversion it implements does not cause undefined behavior nor panic. For example, for impl_nonzero_int_from_nonzero_int!(u8 => u16);, prove that calling NonZero<u16>::from(small: NonZero<u8>) does not cause undefined behavior nor panic for an arbitrary small that satisfies the NonZero type invariant.

For each invocation of impl_nonzero_int_try_from_nonzero_int!, prove that the conversion it implements does not cause undefined behavior. For example, for impl_nonzero_int_try_from_nonzero_int!(u16 => u8);, prove that calling NonZero<u8>::try_from(value: NonZero<u16>) does not cause undefined behavior for an arbitrary value that satisfies the NonZero type invariant. Additionally, prove that if the value does not fit into the target type (e.g., value is too large to fit into a NonZero<u8>) that the function panics.

non-zero unsigned integer -> non-zero unsigned integer

• impl_nonzero_int_from_nonzero_int!(u8 => u16);
• impl_nonzero_int_from_nonzero_int!(u8 => u32);
• impl_nonzero_int_from_nonzero_int!(u8 => u64);
• impl_nonzero_int_from_nonzero_int!(u8 => u128);
• impl_nonzero_int_from_nonzero_int!(u8 => usize);
• impl_nonzero_int_from_nonzero_int!(u16 => u32);
• impl_nonzero_int_from_nonzero_int!(u16 => u64);
• impl_nonzero_int_from_nonzero_int!(u16 => u128);
• impl_nonzero_int_from_nonzero_int!(u16 => usize);
• impl_nonzero_int_from_nonzero_int!(u32 => u64);
• impl_nonzero_int_from_nonzero_int!(u32 => u128);
• impl_nonzero_int_from_nonzero_int!(u64 => u128);

non-zero signed integer -> non-zero signed integer

• impl_nonzero_int_from_nonzero_int!(i8 => i16);
• impl_nonzero_int_from_nonzero_int!(i8 => i32);
• impl_nonzero_int_from_nonzero_int!(i8 => i64);
• impl_nonzero_int_from_nonzero_int!(i8 => i128);
• impl_nonzero_int_from_nonzero_int!(i8 => isize);
• impl_nonzero_int_from_nonzero_int!(i16 => i32);
• impl_nonzero_int_from_nonzero_int!(i16 => i64);
• impl_nonzero_int_from_nonzero_int!(i16 => i128);
• impl_nonzero_int_from_nonzero_int!(i16 => isize);
• impl_nonzero_int_from_nonzero_int!(i32 => i64);
• impl_nonzero_int_from_nonzero_int!(i32 => i128);
• impl_nonzero_int_from_nonzero_int!(i64 => i128);

non-zero unsigned -> non-zero signed integer

• impl_nonzero_int_from_nonzero_int!(u8 => i16);
• impl_nonzero_int_from_nonzero_int!(u8 => i32);
• impl_nonzero_int_from_nonzero_int!(u8 => i64);
• impl_nonzero_int_from_nonzero_int!(u8 => i128);
• impl_nonzero_int_from_nonzero_int!(u8 => isize);
• impl_nonzero_int_from_nonzero_int!(u16 => i32);
• impl_nonzero_int_from_nonzero_int!(u16 => i64);
• impl_nonzero_int_from_nonzero_int!(u16 => i128);
• impl_nonzero_int_from_nonzero_int!(u32 => i64);
• impl_nonzero_int_from_nonzero_int!(u32 => i128);
• impl_nonzero_int_from_nonzero_int!(u64 => i128);

There are also the fallible versions. Remember to cover both the panicking and non-panicking cases.

unsigned non-zero integer -> unsigned non-zero integer

• impl_nonzero_int_try_from_nonzero_int!(u16 => u8);
• impl_nonzero_int_try_from_nonzero_int!(u32 => u8, u16, usize);
• impl_nonzero_int_try_from_nonzero_int!(u64 => u8, u16, u32, usize);
• impl_nonzero_int_try_from_nonzero_int!(u128 => u8, u16, u32, u64, usize);
• impl_nonzero_int_try_from_nonzero_int!(usize => u8, u16, u32, u64, u128);

signed non-zero integer -> signed non-zero integer

• impl_nonzero_int_try_from_nonzero_int!(i16 => i8);
• impl_nonzero_int_try_from_nonzero_int!(i32 => i8, i16, isize);
• impl_nonzero_int_try_from_nonzero_int!(i64 => i8, i16, i32, isize);
• impl_nonzero_int_try_from_nonzero_int!(i128 => i8, i16, i32, i64, isize);
• impl_nonzero_int_try_from_nonzero_int!(isize => i8, i16, i32, i64, i128);

unsigned non-zero integer -> signed non-zero integer

• impl_nonzero_int_try_from_nonzero_int!(u8 => i8);
• impl_nonzero_int_try_from_nonzero_int!(u16 => i8, i16, isize);
• impl_nonzero_int_try_from_nonzero_int!(u32 => i8, i16, i32, isize);
• impl_nonzero_int_try_from_nonzero_int!(u64 => i8, i16, i32, i64, isize);
• impl_nonzero_int_try_from_nonzero_int!(u128 => i8, i16, i32, i64, i128, isize);
• impl_nonzero_int_try_from_nonzero_int!(usize => i8, i16, i32, i64, i128, isize);

signed non-zero integer -> unsigned non-zero integer

• impl_nonzero_int_try_from_nonzero_int!(i8 => u8, u16, u32, u64, u128, usize);
• impl_nonzero_int_try_from_nonzero_int!(i16 => u8, u16, u32, u64, u128, usize);
• impl_nonzero_int_try_from_nonzero_int!(i32 => u8, u16, u32, u64, u128, usize);
• impl_nonzero_int_try_from_nonzero_int!(i64 => u8, u16, u32, u64, u128, usize);
• impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize);
• impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);

Safety for Float to Int

macro_rules! impl_float_to_int {
    ($Float:ty => $($Int:ty),+) => {
        #[unstable(feature = "convert_float_to_int", issue = "67057")]
        impl private::Sealed for $Float {}
        $(
            #[unstable(feature = "convert_float_to_int", issue = "67057")]
            impl FloatToInt<$Int> for $Float {
                #[inline]
                unsafe fn to_int_unchecked(self) -> $Int {
                    // SAFETY: the safety contract must be upheld by the caller.
                    unsafe { crate::intrinsics::float_to_int_unchecked(self) }
                }
            }
        )+
    }
}

The safety constraints referenced in the comments are that the input value must:

• Not be NaN
• Not be infinite
• Be representable in the return type Int, after truncating off its fractional part

These constraints are given in the documentation.

The intrinsic corresponds to the fptoui/fptosi LLVM instructions, which may be useful for reference. Prove safety for each of the following conversions:

• impl_float_to_int!(f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)
• impl_float_to_int!(f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)
• impl_float_to_int!(f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)
• impl_float_to_int!(f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize)

List of UBs

In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following undefined behaviors:

• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.