Modify pr workflow

.github/pull_requests.toml

@@ -9,5 +9,6 @@ members = [
     "remi-delmas-3000",
     "qinheping",
     "tautschnig",
-    "jaisnan"
+    "jaisnan",
+    "Jaisu-1"
 ]

.github/workflows/kani.yml

@@ -9,6 +9,7 @@ on:
     paths:
       - 'library/**'
       - '.github/workflows/kani.yml'
+      - 'scripts/check_kani.sh'
 
 defaults:
   run:
@@ -30,32 +31,8 @@ jobs:
       - name: Checkout Library
         uses: actions/checkout@v4
         with:
-          path: verify-rust-std
+          path: head
           submodules: true
 
-      # We currently build Kani from a branch that tracks a rustc version compatible with this library version.
-      - name: Checkout `Kani`
-        uses: actions/checkout@v4
-        with:
-          repository: model-checking/kani
-          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: |
-          cargo build-dev --release
-          echo "$(pwd)/scripts" >> $GITHUB_PATH
-
-      - name: Run tests
-        working-directory: verify-rust-std
-        env:
-          RUST_BACKTRACE: 1
-        run: |
-          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+      - name: Run Kani Script
+        run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head

.github/workflows/pr_approval.yml

@@ -58,7 +58,7 @@ jobs:
               pull_number
             });
 
-            const relevantPaths = ['library/', 'doc/src/challenges/'];
+            const relevantPaths = ['library/', 'doc/src/challenges/', '.github/workflows'];
             const isRelevantPR = files.data.some(file =>
               relevantPaths.some(path => file.filename.startsWith(path))
             );
@@ -73,7 +73,6 @@ jobs:
               const tomlContent = fs.readFileSync('.github/pull_requests.toml', 'utf8');
               console.log('TOML content:', tomlContent);
               const tomlData = toml.parse(tomlContent);
-              console.log('Parsed TOML data:', JSON.stringify(tomlData, null, 2));
 
               if (!tomlData.committee || !Array.isArray(tomlData.committee.members)) {
                 throw new Error('committee.members is not an array in the TOML file');
@@ -99,7 +98,7 @@ jobs:
                 .map(review => review.user.login)
             );
 
-            const requiredApprovals = 2;
+            const requiredApprovals = 1;
             const currentCountfromCommittee = Array.from(approvers)
               .filter(approver => requiredApprovers.includes(approver))
               .length;
@@ -124,37 +123,23 @@ jobs:
               pull_number
             });
 
-            // Create or update check run
+            // Update check run
             const checkRuns = await github.rest.checks.listForRef({
               owner,
               repo,
               ref: pr.data.head.sha,
               check_name: checkName
             });
 
-            // Reuse the same workflow everytime there's a new review submitted
-            // instead of creating new workflows. Better efficiency and readability
-            // as the number of workflows is kept to a minimal number
-            if (checkRuns.data.total_count > 0) {
-              await github.rest.checks.update({
-                owner,
-                repo,
-                check_run_id: checkRuns.data.check_runs[0].id,
-                status: 'completed',
-                conclusion,
-                output
-              });
-            } else {
-              await github.rest.checks.create({
-                owner,
-                repo,
-                name: checkName,
-                head_sha: pr.data.head.sha,
-                status: 'completed',
-                conclusion,
-                output
-              });
-            }
+            await github.rest.checks.create({
+              owner,
+              repo,
+              name: checkName,
+              head_sha: pr.data.head.sha,
+              status: 'completed',
+              conclusion,
+              output
+            });
 
             if (conclusion === 'failure') {
               core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);

.github/workflows/rustc.yml

@@ -11,6 +11,7 @@ on:
       - 'library/**'
       - 'rust-toolchain.toml'
       - '.github/workflows/rustc.yml'
+      - 'scripts/check_rustc.sh'
 
 defaults:
   run:
@@ -29,35 +30,5 @@ jobs:
         with:
           path: head
 
-      - name: Checkout `upstream/master`
-        uses: actions/checkout@v4
-        with:
-          repository: rust-lang/rust
-          path: upstream
-          fetch-depth: 0
-          submodules: true
-
-      # Run rustc twice in case the toolchain needs to be installed.
-      # Retrieve the commit id from the `rustc --version`. Output looks like:
-      # `rustc 1.80.0-nightly (84b40fc90 2024-05-27)`
-      - name: Checkout matching commit
-        run: |
-          cd head
-          rustc --version
-          COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
-          cd ../upstream
-          git checkout ${COMMIT_ID}
-
-      - name: Copy Library
-        run: |
-          rm -rf upstream/library
-          cp -r head/library upstream
-
-      - 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
+      - name: Run rustc script
+        run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head

doc/src/SUMMARY.md

@@ -16,4 +16,7 @@
   - [Core Transmutation](./challenges/0001-core-transmutation.md)
   - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
   - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
+  - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
   - [Inductive data type](./challenges/0005-linked-list.md)
+  - [Contracts for SmallSort](./challenges/0008-smallsort.md)
+  - [Memory safety of String](./challenges/0010-string.md)

doc/src/challenges/0004-btree-node.md

@@ -0,0 +1,68 @@
+# Challenge 4: Memory safety of BTreeMap's `btree::node` module
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25)
+- **Start date:** *2024-07-01*
+- **End date:** *2024-12-10*
+
+-------------------
+
+
+## Goal
+
+Verify the memory safety of the [`alloc::collections::btree::node` module](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/btree/node.rs).
+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`
+1. `NodeRef::as_internal_mut`
+1. `NodeRef::len`
+1. `NodeRef::ascend`
+1. `NodeRef::first_edge`
+1. `NodeRef::last_edge`
+1. `NodeRef::first_kv`
+1. `NodeRef::last_kv`
+1. `NodeRef::into_leaf`
+1. `NodeRef::keys`
+1. `NodeRef::as_leaf_mut`
+1. `NodeRef::into_leaf_mut`
+1. `NodeRef::as_leaf_dying`
+1. `NodeRef::pop_internal_level`
+1. `NodeRef::push`
+1. `Handle::left_edge`
+1. `Handle::right_edge`
+1. `Handle::left_kv`
+1. `Handle::right_kv`
+1. `Handle::descend`
+1. `Handle::into_kv`
+1. `Handle::key_mut`
+1. `Handle::into_val_mut`
+1. `Handle::into_kv_mut`
+1. `Handle::into_kv_valmut`
+1. `Handle::kv_mut`
+
+Verification must be unbounded for functions that use recursion or contain loops, e.g.
+
+1. `NodeRef::new_internal`
+1. `Handle::insert_recursing`
+1. `BalancingContext::do_merge`
+1. `BalancingContext::merge_tracking_child_edge`
+1. `BalancingContext::steal_left`
+1. `BalancingContext::steal_right`
+1. `BalancingContext::bulk_steal_left`
+1. `BalancingContext::bulk_steal_right`
+
+### List of UBs
+
+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/challenges/0008-smallsort.md

@@ -0,0 +1,54 @@
+# Challenge 8: Contracts for SmallSort
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/56)
+- **Start date:** *2024-08-17*
+- **End date:** *2024-12-10*
+
+-------------------
+
+
+## Goal
+
+The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) 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](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/challenges/0010-string.md

@@ -0,0 +1,75 @@
+# Challenge X: Memory safety of String
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/61)
+- **Start date:** *2024-08-19*
+- **End date:** *2024-12-10*
+
+-------------------
+
+## 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:
+```rust
+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:
+```rust
+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)
+1. `from_utf16le_lossy`(unbounded)
+1. `from_utf16be` (unbounded)
+1. `from_utf16be_lossy` (unbounded)
+1. `pop`
+1. `remove`
+1. `remove_matches` (unbounded)
+1. `retain` (unbounded)
+1. `insert`
+1. `insert_str` (unbounded)
+1. `split_off` (unbounded)
+1. `drain`
+1. `replace_range` (unbounded)
+1. `into_boxed_str`
+1. `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](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.