Merge remote-tracking branch 'origin/main' into rawvec-tour

Author: btj

.github/workflows/flux.yml

@@ -9,7 +9,7 @@ on:
 
 env:
   FIXPOINT_VERSION: "556104ba5508891c357b0bdf819ce706e93d9349"
-  FLUX_VERSION: "a17246965a8752e3d3d4e3559865311048bb61f7"
+  FLUX_VERSION: "f5e57bec353e2eb3550d2b7ba086462264dfa290"
 
 jobs:
   check-flux-on-core:

.github/workflows/kani.yml

@@ -198,6 +198,7 @@ jobs:
             --include-pattern time::Duration::from_micros \
             --include-pattern time::Duration::from_millis \
             --include-pattern time::Duration::from_nanos \
+            --exclude-pattern time::Duration::from_nanos_u128 \
             --include-pattern time::Duration::from_secs \
             --exclude-pattern time::Duration::from_secs_f \
             --include-pattern unicode::unicode_data::conversions::to_ \

.github/workflows/testable-simd-models.yml

@@ -0,0 +1,31 @@
+# This workflow runs the tests for testable simd models.
+
+name: Testable simd models
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [ main ]
+  push:
+    paths:
+      - '.github/workflows/testable-simd-models.yml'
+      - 'testable-simd-models/**'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  testable-simd-models:
+    name: Test testable simd models
+    runs-on: ubuntu-latest
+    
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+      
+      - name: Run tests
+        working-directory: testable-simd-models
+        run: cargo test -- --test-threads=1 --nocapture
+        

.gitignore

@@ -56,3 +56,4 @@ goto-transcoder
 # already existing elements were commented out
 
 #/target
+testable-simd-models/target

README.md

@@ -1,4 +1,4 @@
-# Rust std-lib verification
+# Rust standard library verification
 
 [![Rust Tests](https://github.com/model-checking/verify-rust-std/actions/workflows/rustc.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/rustc.yml)
 [![Build Book](https://github.com/model-checking/verify-rust-std/actions/workflows/book.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/book.yml)
@@ -8,7 +8,7 @@ This repository is a fork of the official Rust programming
 language repository, created solely to verify the Rust standard
 library. It should not be used as an alternative to the official
 Rust releases. The repository is tool agnostic and welcomes the addition of
-new tools.
+new tools. The currently accepted tools are [Flux](https://model-checking.github.io/verify-rust-std/tools/flux.html), [GOTO Transcoder (ESBMC)](https://model-checking.github.io/verify-rust-std/tools/goto-transcoder.html), [Kani](https://model-checking.github.io/verify-rust-std/tools/kani.html), and [VeriFast](https://model-checking.github.io/verify-rust-std/tools/verifast.html).
 
 The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
 1. Contributing to the core mechanism of verifying the rust standard library
@@ -21,8 +21,39 @@ 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.
 
-See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules
-and the list of existing challenges.
+These are the challenges:
+
+| Challenge | Reward | Status | Proof |
+| --------- | ------ | ------ | ----- |
+| [1: Verify core transmuting methods](https://model-checking.github.io/verify-rust-std/challenges/0001-core-transmutation.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/issues/19) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/intrinsics/mod.rs) |
+| [2: Verify the memory safety of core intrinsics using raw pointers](https://model-checking.github.io/verify-rust-std/challenges/0002-intrinsics-memory.html) | N/A | Open | |
+| [3: Verifying Raw Pointer Arithmetic Operations](https://model-checking.github.io/verify-rust-std/challenges/0003-pointer-arithmentic.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/212) | [Kani](https://github.com/model-checking/verify-rust-std/pull/212/files) |
+| [4: Memory safety of BTreeMap's `btree::node` module](https://model-checking.github.io/verify-rust-std/challenges/0004-btree-node.html) | 10,000 USD | Open | |
+| [5: Verify functions iterating over inductive data type: `linked_list`](https://model-checking.github.io/verify-rust-std/challenges/0005-linked-list.html) | 5,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/238) | [VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/collections/linked_list.rs) |
+| [6: Safety of `NonNull`](https://model-checking.github.io/verify-rust-std/challenges/0006-nonnull.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/247) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/ptr/non_null.rs) |
+| [7: Safety of Methods for Atomic Types & Atomic Intrinsics](https://model-checking.github.io/verify-rust-std/challenges/0007-atomic-types.html) | 10,000 USD | Open | |
+| [8: Contracts for SmallSort](https://model-checking.github.io/verify-rust-std/challenges/0008-smallsort.html) | 10,000 USD | Open | |
+| [9: Safe abstractions for `core::time::Duration`](https://model-checking.github.io/verify-rust-std/challenges/0009-duration.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/136) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/time.rs) |
+| [10: Memory safety of String](https://model-checking.github.io/verify-rust-std/challenges/0010-string.html) | N/A | Open | |
+| [11: Safety of Methods for Numeric Primitive Types](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/issues/59) | [Kani](https://github.com/model-checking/verify-rust-std/tree/main/library/core/src/num) |
+| [12: Safety of `NonZero`](https://model-checking.github.io/verify-rust-std/challenges/0012-nonzero.html) | N/A | Open | |
+| [13: Safety of `CStr`](https://model-checking.github.io/verify-rust-std/challenges/0013-cstr.html) | N/A | Open | |
+| [14: Safety of Primitive Conversions](https://model-checking.github.io/verify-rust-std/challenges/0014-convert-num.html) | TBD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/247) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/convert/num.rs) |
+| [15: Contracts and Tests for SIMD Intrinsics](https://model-checking.github.io/verify-rust-std/challenges/0015-intrinsics-simd.html) | | Open | |
+| [16: Verify the safety of Iterator functions](https://model-checking.github.io/verify-rust-std/challenges/0016-iter.html) | 10,000 USD | Open | |
+| [17: Verify the safety of slice functions](https://model-checking.github.io/verify-rust-std/challenges/0017-slice.html) | 10,000 USD | Open | |
+| [18: Verify the safety of slice iter functions](https://model-checking.github.io/verify-rust-std/challenges/0018-slice-iter.html) | 10,000 USD | Open | |
+| [19: Safety of `RawVec`](https://model-checking.github.io/verify-rust-std/challenges/0019-rawvec.html) | 10,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/422) | [VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/raw_vec/mod.rs) |
+| [20: Verify the safety of char-related functions in str::pattern](https://model-checking.github.io/verify-rust-std/challenges/0020-str-pattern-pt1.html) | 25,000 USD | Open | |
+| [21: Verify the safety of substring-related functions in str::pattern](https://model-checking.github.io/verify-rust-std/challenges/0021-str-pattern-pt2.html) | 25,000 USD | Open | |
+| [22: Verify the safety of str iter functions](https://model-checking.github.io/verify-rust-std/challenges/0022-str-iter.html) | 10,000 USD | Open | |
+| [23: Verify the safety of Vec functions part 1](https://model-checking.github.io/verify-rust-std/challenges/0023-vec-pt1.html) | 15,000 USD | Open | |
+| [24: Verify the safety of Vec functions part 2](https://model-checking.github.io/verify-rust-std/challenges/0024-vec-pt2.html) | 15,000 USD | Open | |
+| [25: Verify the safety of `VecDeque` functions](https://model-checking.github.io/verify-rust-std/challenges/0025-vecdeque.html) | 10,000 USD | Open | |
+| [26: Verify reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0026-rc.html) | 10,000 USD | Open | |
+| [27: Verify atomically reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0027-arc.html) | 10,000 USD | Open | |
+
+See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules.
 
 We welcome everyone to participate!
 

doc/src/challenges/0001-core-transmutation.md

@@ -1,10 +1,11 @@
 # Challenge 1: Verify `core` transmuting methods
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
 - **Start date:** *2024/06/12*
 - **End date:** *2025/04/10*
-- **Reward:** *N/A*
+- **Reward:** *10000 USD*
+- **Contributors**: [Alex Le Blanc](https://github.com/AlexLB99), [Patrick Lam](https://github.com/patricklam)
 
 -------------------
 

doc/src/challenges/0002-intrinsics-memory.md

@@ -4,7 +4,7 @@
 - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
 - **Start date:** *2024/06/12*
 - **End date:** *2025/04/10*
-- **Reward:** *N/A*
+- **Reward:** *10000 USD*
 
 -------------------
 

doc/src/challenges/0005-linked-list.md

@@ -4,7 +4,7 @@
 - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
 - **Start date:** *2024/07/01*
 - **End date:** *2025/08/12*
-- **Reward:** *5,000 USD*
+- **Reward:** *20000 USD*
 - **Contributors:** [Bart Jacobs](https://github.com/btj)
 
 -------------------

doc/src/challenges/0010-string.md

@@ -4,7 +4,7 @@
 - **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61)
 - **Start date:** *2024/08/19*
 - **End date:** *2025/04/10*
-- **Reward:** *N/A*
+- **Reward:** *10000 USD*
 
 -------------------
 

doc/src/challenges/0012-nonzero.md

@@ -4,7 +4,7 @@
 - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
 - **Start date:** *2024/08/23*
 - **End date:** *2025/04/10*
-- **Reward:** *N/A*
+- **Reward:** *10000 USD*
 
 -------------------