Merge remote-tracking branch 'origin/main' into chores-tidy

.github/workflows/kani.yml

@@ -17,25 +17,39 @@ defaults:
 
 jobs:
   check-kani-on-std:
-    name: Verify std library
+    name: Verify std library (partition ${{ matrix.partition }})
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
         os: [ubuntu-latest, macos-latest]
+        partition: [1, 2, 3, 4]
         include:
           - os: ubuntu-latest
             base: ubuntu
           - os: macos-latest
             base: macos
+      fail-fast: false
+
+    env:
+      # Define the index of this particular worker [1-WORKER_TOTAL]
+      WORKER_INDEX: ${{ matrix.partition }}
+      # Total number of workers running this step
+      WORKER_TOTAL: 4
+
     steps:
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
         with:
           path: head
           submodules: true
-
-      # Step 2: Run Kani on the std library (default configuration)
+
+      # Step 2: Install jq
+      - name: Install jq
+        if: matrix.os == 'ubuntu-latest'
+        run: sudo apt-get install -y jq
+
+      # Step 3: Run Kani on the std library (default configuration)
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 

README.md

@@ -15,7 +15,8 @@ The goal is to have a verified [Rust standard library](https://doc.rust-lang.org
 2. Creating new techniques to perform scalable verification
 3. Apply techniques to verify previously unverified parts of the standard library.
 
-For that we are launching a contest that includes a series of challenges that focus on verifying
+For that we are launching a [contest supported by the Rust Foundation](https://foundation.rust-lang.org/news/rust-foundation-collaborates-with-aws-initiative-to-verify-rust-standard-libraries/)
+that includes a series of challenges that focus on verifying
 memory safety and a subset of undefined behaviors in the Rust standard library.
 Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its
 successful completion.

doc/src/SUMMARY.md

@@ -14,7 +14,7 @@
 
 - [Challenges](./challenges.md)
   - [1: Verify core transmuting methods](./challenges/0001-core-transmutation.md)
-  - [2: Verify the memory safery of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md)
+  - [2: Verify the memory safety of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md)
   - [3: Verifying Raw Pointer Arithmetic Operations](./challenges/0003-pointer-arithmentic.md)
   - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
   - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md)
@@ -26,4 +26,4 @@
   - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
   - [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
   - [13: Safety of `CStr`](./challenges/0013-cstr.md)
-
+  - [14: Safety of Primitive Conversions](./challenges/0014-convert-num.md)

doc/src/challenges/0014-convert-num.md

@@ -0,0 +1,150 @@
+# 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
+
+```rust
+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](https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked). 
+
+The intrinsic corresponds to the [fptoui](https://llvm.org/docs/LangRef.html#fptoui-to-instruction)/[fptosi](https://llvm.org/docs/LangRef.html#fptosi-to-instruction) 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](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* 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](../general-rules.md)
+in addition to the ones listed above.

doc/src/general-rules.md

@@ -6,8 +6,6 @@
 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](https://github.com/rust-lang/rust/).
 
-**NOTE:** This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation.
-
 **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](https://github.com/model-checking/verify-rust-std/labels/Challenge).
@@ -92,3 +90,21 @@ 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](https://doc.rust-lang.org/std/index.html))?
+   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)?

library/core/src/num/mod.rs

@@ -1759,6 +1759,7 @@ mod verify {
         ($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
             $(
                 #[kani::proof]
+                #[kani::solver(kissat)]
                 pub fn $harness_name() {
                     let lhs: $type = kani::any::<$type>();
                     let rhs: $type = kani::any::<$type>();

scripts/run-kani.sh

@@ -77,6 +77,22 @@ TOML_FILE=${KANI_TOML_FILE:-$DEFAULT_TOML_FILE}
 REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
+# Unstable arguments to pass to Kani
+unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts"
+
+# Variables used for parallel harness verification
+# When we say "parallel," we mean two dimensions of parallelization:
+#   1. Sharding verification across multiple workers. The Kani workflow that calls this script defines WORKER_INDEX and WORKER_TOTAL for this purpose: 
+#   we shard verification across WORKER_TOTAL workers, where each worker has a unique WORKER_INDEX that it uses to derive its share of ALL_HARNESSES to verify.
+#   2. Within a single worker, we parallelize verification between multiple cores by invoking kani with -j.
+
+# Array of all of the harnesses in the repository, set in get_harnesses()
+declare -a ALL_HARNESSES
+# Length of ALL_HARNESSES, set in get_harnesses()
+declare -i HARNESS_COUNT
+# `kani list` JSON FILE_VERSION that the parallel verification command expects
+EXPECTED_JSON_FILE_VERSION="0.1"
+
 # Function to read commit ID from TOML file
 read_commit_from_toml() {
     local file="$1"
@@ -153,10 +169,50 @@ get_kani_path() {
     echo "$(realpath "$build_dir/scripts/kani")"
 }
 
-run_kani_command() {
+# Run kani list with JSON format and process with jq to extract harness names and total number of harnesses.
+# Note: The code to extract ALL_HARNESSES is dependent on `kani list --format json` FILE_VERSION 0.1.
+# (The FILE_VERSION variable is defined in Kani in the list module's output code, current path kani-driver/src/list/output.rs)
+# If FILE_VERSION changes, first update the ALL_HARNESSES extraction logic to work with the new format, if necessary,
+# then update EXPECTED_JSON_FILE_VERSION.
+get_harnesses() {
     local kani_path="$1"
-    shift
-    "$kani_path" "$@"
+    "$kani_path" list -Z list $unstable_args ./library --std --format json
+    local json_file_version=$(jq -r '.["file-version"]' "$WORK_DIR/kani-list.json")
+    if [[ $json_file_version != $EXPECTED_JSON_FILE_VERSION ]]; then
+        echo "Error: The JSON file-version in kani-list.json does not equal $EXPECTED_JSON_FILE_VERSION"
+        exit 1
+    fi
+    # Extract the harnesses inside "standard-harnesses" and "contract-harnesses" 
+    # into an array called ALL_HARNESSES and the length of that array into HARNESS_COUNT
+    ALL_HARNESSES=($(jq -r '
+        ([.["standard-harnesses"] | to_entries | .[] | .value[]] + 
+            [.["contract-harnesses"] | to_entries | .[] | .value[]]) | 
+        .[]
+    ' $WORK_DIR/kani-list.json))
+    HARNESS_COUNT=${#ALL_HARNESSES[@]}
+}
+
+# Given an array of harness names, run verification for those harnesses
+run_verification_subset() {
+    local kani_path="$1"
+    local harnesses=("${@:2}")  # All arguments after kani_path are harness names
+
+    # Build the --harness arguments
+    local harness_args=""
+    for harness in "${harnesses[@]}"; do
+        harness_args="$harness_args --harness $harness"
+    done
+
+    echo "Running verification for harnesses:"
+    printf '%s\n' "${harnesses[@]}"
+    "$kani_path" verify-std -Z unstable-options ./library \
+        $unstable_args \
+        $harness_args --exact \
+        -j \
+        --output-format=terse \
+        $command_args \
+        --enable-unstable \
+        --cbmc-args --object-bits 12
 }
 
 # Check if binary exists and is up to date
@@ -178,7 +234,6 @@ check_binary_exists() {
     return 1
 }
 
-
 main() {
     local build_dir="$WORK_DIR/kani_build"
 
@@ -211,19 +266,38 @@ main() {
     "$kani_path" --version
 
     if [[ "$run_command" == "verify-std" ]]; then
-        echo "Running Kani verify-std command..."
-        "$kani_path" verify-std -Z unstable-options ./library \
-            -Z function-contracts \
-            -Z mem-predicates \
-            -Z loop-contracts \
-            -Z float-lib \
-            -Z c-ffi \
-            $command_args \
-            --enable-unstable \
-            --cbmc-args --object-bits 12
+        if [[ -n "$WORKER_INDEX" && -n "$WORKER_TOTAL" ]]; then
+            echo "Running as parallel worker $WORKER_INDEX of $WORKER_TOTAL"
+            get_harnesses "$kani_path"
+
+            echo "All harnesses:"
+            printf '%s\n' "${ALL_HARNESSES[@]}"
+            echo "Total number of harnesses: $HARNESS_COUNT"
+
+            # Calculate this worker's portion (add WORKER_TOTAL - 1 to force ceiling division)
+            chunk_size=$(( (HARNESS_COUNT + WORKER_TOTAL - 1) / WORKER_TOTAL ))
+            echo "Number of harnesses this worker will run: $chunk_size"
+
+            start_idx=$(( (WORKER_INDEX - 1) * chunk_size ))
+            echo "Start index into ALL_HARNESSES is $start_idx"
+
+            # Extract this worker's harnesses
+            worker_harnesses=("${ALL_HARNESSES[@]:$start_idx:$chunk_size}")
+
+            # Run verification for this subset
+            run_verification_subset "$kani_path" "${worker_harnesses[@]}"
+        else
+            # Run verification for all harnesses (not in parallel)
+            echo "Running Kani verify-std command..."
+            "$kani_path" verify-std -Z unstable-options ./library \
+                $unstable_args \
+                $command_args \
+                --enable-unstable \
+                --cbmc-args --object-bits 12
+        fi
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
-        "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi ./library --std --format markdown
+        "$kani_path" list -Z list $unstable_args ./library --std --format markdown
     fi
 }