Merge branch 'main' into btree-node

.github/pull_requests.toml

@@ -0,0 +1,13 @@
+[committee]
+members = [
+ "celinval",
+ "rahulku",
+ "pnkfelix",
+ "adpaco-aws",
+ "feliperodri",
+ "zhassan-aws",
+ "remi-delmas-3000",
+ "qinheping",
+ "tautschnig",
+ "jaisnan"
+]

.github/workflows/pr_approval.yml

@@ -0,0 +1,161 @@
+name: Check PR Approvals
+
+# For now, the workflow gets triggered only when a review is submitted
+# This technically means, a PR with zero approvals can be merged by the rules of this workflow alone
+# To protect against that scenario, we can turn on number of approvals required to 2 in the github settings
+# of the repository
+on:
+ pull_request_review:
+ types: [submitted]
+ workflow_dispatch:
+
+# Without these permissions, we get a 403 error from github
+# for trying to modify the pull request for newer project.
+# Source: https://stackoverflow.com/a/76994510
+permissions: write-all
+
+jobs:
+ check-approvals:
+ if: github.event.review.state == 'APPROVED' || github.event_name == 'workflow_dispatch'
+ runs-on: ubuntu-latest
+ steps:
+ - name: Checkout repository
+ uses: actions/checkout@v2
+
+ - name: Install TOML parser
+ run: npm install @iarna/toml
+
+ - name: Check PR Relevance and Approvals
+ uses: actions/github-script@v6
+ with:
+ script: |
+ const fs = require('fs');
+ const toml = require('@iarna/toml');
+ const { owner, repo } = context.repo;
+ let pull_number;
+
+ if (github.event_name === 'workflow_dispatch') {
+ const branch = github.ref.replace('refs/heads/', '');
+ const prs = await github.rest.pulls.list({
+ owner,
+ repo,
+ head: `${owner}:${branch}`,
+ state: 'open'
+ });
+ if (prs.data.length === 0) {
+ console.log('No open PR found for this branch.');
+ return;
+ }
+ pull_number = prs.data[0].number;
+ } else {
+ pull_number = context.issue.number;
+ }
+
+ // Get PR files
+ const files = await github.rest.pulls.listFiles({
+ owner,
+ repo,
+ pull_number
+ });
+
+ const relevantPaths = ['library/', 'doc/src/challenges/'];
+ const isRelevantPR = files.data.some(file =>
+ relevantPaths.some(path => file.filename.startsWith(path))
+ );
+
+ if (!isRelevantPR) {
+ console.log('PR does not touch relevant paths. Exiting workflow.');
+ return;
+ }
+
+ // Get parsed data
+ try {
+ 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');
+ }
+ requiredApprovers = tomlData.committee.members;
+ } catch (error) {
+ console.error('Error reading or parsing TOML file:', error);
+ core.setFailed('Failed to read required approvers list');
+ return;
+ }
+
+ // Get all reviews
+ const reviews = await github.rest.pulls.listReviews({
+ owner,
+ repo,
+ pull_number
+ });
+
+ // Example: approvers = ["celina", "zyad"]
+ const approvers = new Set(
+ reviews.data
+ .filter(review => review.state === 'APPROVED')
+ .map(review => review.user.login)
+ );
+
+ const requiredApprovals = 2;
+ const currentCountfromCommittee = Array.from(approvers)
+ .filter(approver => requiredApprovers.includes(approver))
+ .length;
+
+ // TODO: Improve logging and messaging to the user
+ console.log('PR Approvers:', Array.from(approvers));
+ console.log('Required Approvers:', requiredApprovals);
+
+ // Core logic that checks if the approvers are in the committee
+ const checkName = 'PR Approval Status';
+ const conclusion = (approvers.size >= requiredApprovals && currentCountfromCommittee >= 2) ? 'success' : 'failure';
+ const output = {
+ title: checkName,
+ summary: `PR has ${approvers.size} total approvals and ${requiredApprovals} required approvals.`,
+ text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
+ };
+
+ // Get PR details
+ const pr = await github.rest.pulls.get({
+ owner,
+ repo,
+ pull_number
+ });
+
+ // Create or 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
+ });
+ }
+
+ if (conclusion === 'failure') {
+ core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);
+ }

doc/src/SUMMARY.md

@@ -15,4 +15,6 @@
 - [Challenges](./challenges.md)
  - [Core Transmutation](./challenges/0001-core-transmutation.md)
  - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
- - [Memory safety of the `alloc::collections::btree::node` module](./challenges/0004-btree-node.md)
+ - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
+ - [Inductive data type](./challenges/0005-linked-list.md)
+ - [Memory safety of the `btree::node` module](./challenges/0006-btree-node.md)

doc/src/challenges/0003-pointer-arithmentic.md

@@ -0,0 +1,107 @@
+# Challenge 3: Verifying Raw Pointer Arithmetic Operations
+
+- **Status:** Open
+- **Solution:**
+- **Tracking Issue:** <https://github.com/model-checking/verify-rust-std/issues/21>
+- **Start date:** 24/06/24
+- **End date:** 24/12/10
+
+-------------------
+
+
+## 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](https://doc.rust-lang.org/beta/book/ch19-01-unsafe-rust.html#creating-a-safe-abstraction-over-unsafe-code).
+However, bugs in these abstractions may compromise entire applications, potentially becoming a security concern.
+See [CVE-2018-1000810](https://www.cvedetails.com/cve/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`](https://doc.rust-lang.org/std/primitive.pointer.html#method.offset),
+[`ptr::add`](https://doc.rust-lang.org/std/primitive.pointer.html#method.add),
+and [`ptr::sub`](https://doc.rust-lang.org/std/primitive.pointer.html#method.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`](https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_offset),
+[`ptr::wrapping_add`](https://doc.rust-lang.org/std/primitive.pointer.html#method.wrapping_add),
+[`ptr::wrapping_sub`](https://doc.rust-lang.org/std/primitive.pointer.html#method.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:
+
+| Function | Location |
+|-----------------------------|----------|
+| *const T::add | core::ptr |
+| *const T::sub | core::ptr |
+| *const T::offset | core::ptr |
+| *const T::offset_from | core::ptr |
+| *const T::byte_add | core::ptr |
+| *const T::byte_sub | core::ptr |
+| *const T::byte_offset | core::ptr |
+| *const T::byte_offset_from | core::ptr |
+| *mut T::add | core::ptr |
+| *mut T::sub | core::ptr |
+| *mut T::offset | core::ptr |
+| *mut T::offset_from | core::ptr |
+| *mut T::byte_add | core::ptr |
+| *mut T::byte_sub | core::ptr |
+| *mut T::byte_offset | core::ptr |
+| *mut T::byte_offset_from | core::ptr |
+
+At least 3 of the following usages were proven safe:
+
+| Function | Location |
+|-------------------|---------------|
+| \[u8\]::is_asc_ii | core::slice |
+| String::remove | alloc::string |
+ | Vec::swap_remove | alloc::vec |
+ | Option::as_slice | core::option |
+ | VecDeque::swap | collections::vec_deque |
+
+All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+- 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](../general-rules.md)
+in addition to the ones listed above.
+

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

@@ -0,0 +1,50 @@
+# Challenge 5: Verify functions iterating over inductive data type: `linked_list`
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29)
+- **Start date:** *24/07/01*
+- **End date:** *24/12/10*
+
+-------------------
+
+
+## Goal
+
+Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate the 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:
+
+| Function | Location |
+|---------|---------|
+|clearn | alloc::collections::linked_list |
+|contains| alloc::collections::linked_list |
+|split_off| alloc::collections::linked_list |
+|remove| alloc::collections::linked_list |
+|retain| alloc::collections::linked_list |
+|retain_mut| alloc::collections::linked_list |
+|extract_if| alloc::collections::linked_list |
+
+
+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](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 except for padding or unions.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

doc/src/general-rules.md

@@ -81,3 +81,15 @@ Solutions must be automated using one of the tools previously approved and liste
  I.e., the action may no longer pass after an update.
  This will not impact the approval status of the tool, however,
  new solutions that want to employ the tool may need to ensure the action is passing first.
+
+## 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"
+]
+```