Skip to content

Commit 0182ea1

Browse files
celinvalcelinval
committed
Merge remote-tracking branch 'origin/main' into verify-intrinsics
# Conflicts: # library/core/src/intrinsics.rs
2 parents 79c6536 + 351e958 commit 0182ea1

File tree

747 files changed

+19987
-8337
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

747 files changed

+19987
-8337
lines changed

‎.github/TOOL_REQUEST_TEMPLATE.md

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
_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._
2+
3+
## Tool Name
4+
_Please enter your tool name here._
5+
6+
## Description
7+
_Please enter a description for your tool and any information you deem relevant._
8+
9+
## Tool Information
10+
11+
* [ ] Does the tool perform Rust verification?
12+
* [ ] Does the tool deal with *unsafe* Rust code?
13+
* [ ] Does the tool run independently in CI?
14+
* [ ] Is the tool open source?
15+
* [ ] Is the tool under development?
16+
* [ ] Will you or your team be able to provide support for the tool?
17+
18+
## Licenses
19+
_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)._
20+
21+
## Steps to Use the Tool
22+
23+
1. [First Step]
24+
2. [Second Step]
25+
3. [and so on...]
26+
27+
## Artifacts
28+
_If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._
29+
30+
## CI & Versioning
31+
_Please describe how you version the tool and how it will be supported in CI pipelines._

‎.github/pull_requests.toml

+4-1
Original file line numberDiff line numberDiff line change
@@ -9,5 +9,8 @@ members = [
99
"remi-delmas-3000",
1010
"qinheping",
1111
"tautschnig",
12-
"jaisnan"
12+
"jaisnan",
13+
"patricklam",
14+
"ranjitjhala",
15+
"carolynzech"
1316
]

‎.github/workflows/kani.yml

+4-27
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ on:
99
paths:
1010
- 'library/**'
1111
- '.github/workflows/kani.yml'
12+
- 'scripts/check_kani.sh'
1213

1314
defaults:
1415
run:
@@ -30,32 +31,8 @@ jobs:
3031
- name: Checkout Library
3132
uses: actions/checkout@v4
3233
with:
33-
path: verify-rust-std
34+
path: head
3435
submodules: true
3536

36-
# We currently build Kani from a branch that tracks a rustc version compatible with this library version.
37-
- name: Checkout `Kani`
38-
uses: actions/checkout@v4
39-
with:
40-
repository: model-checking/kani
41-
path: kani
42-
ref: features/verify-rust-std
43-
44-
- name: Setup Dependencies
45-
working-directory: kani
46-
run: |
47-
./scripts/setup/${{ matrix.base }}/install_deps.sh
48-
49-
- name: Build `Kani`
50-
working-directory: kani
51-
run: |
52-
cargo build-dev --release
53-
echo "$(pwd)/scripts" >> $GITHUB_PATH
54-
55-
- name: Run tests
56-
working-directory: verify-rust-std
57-
env:
58-
RUST_BACKTRACE: 1
59-
run: |
60-
kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
61-
-Z mem-predicates -Z ptr-to-ref-cast-checks
37+
- name: Run Kani Script
38+
run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head

‎.github/workflows/pr_approval.yml

-62
Original file line numberDiff line numberDiff line change
@@ -7,16 +7,9 @@ name: Check PR Approvals
77
on:
88
pull_request_review:
99
types: [submitted]
10-
workflow_dispatch:
11-
12-
# Without these permissions, we get a 403 error from github
13-
# for trying to modify the pull request for newer project.
14-
# Source: https://stackoverflow.com/a/76994510
15-
permissions: write-all
1610

1711
jobs:
1812
check-approvals:
19-
if: github.event.review.state == 'APPROVED' || github.event_name == 'workflow_dispatch'
2013
runs-on: ubuntu-latest
2114
steps:
2215
- name: Checkout repository
@@ -51,22 +44,6 @@ jobs:
5144
pull_number = context.issue.number;
5245
}
5346
54-
// Get PR files
55-
const files = await github.rest.pulls.listFiles({
56-
owner,
57-
repo,
58-
pull_number
59-
});
60-
61-
const relevantPaths = ['library/', 'doc/src/challenges/'];
62-
const isRelevantPR = files.data.some(file =>
63-
relevantPaths.some(path => file.filename.startsWith(path))
64-
);
65-
66-
if (!isRelevantPR) {
67-
console.log('PR does not touch relevant paths. Exiting workflow.');
68-
return;
69-
}
7047
7148
// Get parsed data
7249
try {
@@ -117,45 +94,6 @@ jobs:
11794
text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
11895
};
11996
120-
// Get PR details
121-
const pr = await github.rest.pulls.get({
122-
owner,
123-
repo,
124-
pull_number
125-
});
126-
127-
// Create or update check run
128-
const checkRuns = await github.rest.checks.listForRef({
129-
owner,
130-
repo,
131-
ref: pr.data.head.sha,
132-
check_name: checkName
133-
});
134-
135-
// Reuse the same workflow everytime there's a new review submitted
136-
// instead of creating new workflows. Better efficiency and readability
137-
// as the number of workflows is kept to a minimal number
138-
if (checkRuns.data.total_count > 0) {
139-
await github.rest.checks.update({
140-
owner,
141-
repo,
142-
check_run_id: checkRuns.data.check_runs[0].id,
143-
status: 'completed',
144-
conclusion,
145-
output
146-
});
147-
} else {
148-
await github.rest.checks.create({
149-
owner,
150-
repo,
151-
name: checkName,
152-
head_sha: pr.data.head.sha,
153-
status: 'completed',
154-
conclusion,
155-
output
156-
});
157-
}
158-
15997
if (conclusion === 'failure') {
16098
core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);
16199
}

‎.github/workflows/rustc.yml

+3-32
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ on:
1111
- 'library/**'
1212
- 'rust-toolchain.toml'
1313
- '.github/workflows/rustc.yml'
14+
- 'scripts/check_rustc.sh'
1415

1516
defaults:
1617
run:
@@ -29,35 +30,5 @@ jobs:
2930
with:
3031
path: head
3132

32-
- name: Checkout `upstream/master`
33-
uses: actions/checkout@v4
34-
with:
35-
repository: rust-lang/rust
36-
path: upstream
37-
fetch-depth: 0
38-
submodules: true
39-
40-
# Run rustc twice in case the toolchain needs to be installed.
41-
# Retrieve the commit id from the `rustc --version`. Output looks like:
42-
# `rustc 1.80.0-nightly (84b40fc90 2024-05-27)`
43-
- name: Checkout matching commit
44-
run: |
45-
cd head
46-
rustc --version
47-
COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
48-
cd ../upstream
49-
git checkout ${COMMIT_ID}
50-
51-
- name: Copy Library
52-
run: |
53-
rm -rf upstream/library
54-
cp -r head/library upstream
55-
56-
- name: Run tests
57-
working-directory: upstream
58-
env:
59-
# Avoid error due to unexpected `cfg`.
60-
RUSTFLAGS: "--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))"
61-
run: |
62-
./configure --set=llvm.download-ci-llvm=true
63-
./x test --stage 0 library/std
33+
- name: Run rustc script
34+
run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head

‎README.md

+6-3
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,8 @@
77
This repository is a fork of the official Rust programming
88
language repository, created solely to verify the Rust standard
99
library. It should not be used as an alternative to the official
10-
Rust releases.
10+
Rust releases. The repository is tool agnostic and welcomes the addition of
11+
new tools.
1112

1213
The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
1314
1. Contributing to the core mechanism of verifying the rust standard library
@@ -36,12 +37,14 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
3637
## License
3738

3839
### Kani
39-
4040
Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
4141
See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details.
4242

4343
## Rust
44-
4544
Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
4645

4746
See [the Rust repository](https://github.com/rust-lang/rust) for details.
47+
48+
## Introducing a New Tool
49+
50+
Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.

‎doc/book.toml

+1
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ build-dir = "../book"
1212
site-url = "/verify-rust-std/"
1313
git-repository-url = "https://github.com/model-checking/verify-rust-std"
1414
edit-url-template = "https://github.com/model-checking/verify-rust-std/edit/main/doc/{path}"
15+
no-section-label = true
1516

1617
[output.html.playground]
1718
runnable = false

‎doc/src/SUMMARY.md

+13-5
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,16 @@
1313
---
1414

1515
- [Challenges](./challenges.md)
16-
- [Core Transmutation](./challenges/0001-core-transmutation.md)
17-
- [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
18-
- [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
19-
- [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
20-
- [Inductive data type](./challenges/0005-linked-list.md)
16+
- [1: Verify core transmuting methods](./challenges/0001-core-transmutation.md)
17+
- [2: Verify the memory safery of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md)
18+
- [3: Verifying Raw Pointer Arithmetic Operations](./challenges/0003-pointer-arithmentic.md)
19+
- [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
20+
- [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md)
21+
- [6: Safety of `NonNull`](./challenges/0006-nonnull.md)
22+
- [8: Contracts for SmallSort](./challenges/0008-smallsort.md)
23+
- [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md)
24+
- [10: Memory safety of String](./challenges/0010-string.md)
25+
- [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
26+
- [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
27+
28+

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
# Challenge 1: Verify `core` transmuting methods
22

33
- **Status:** Open
4-
- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19)
4+
- **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
55
- **Start date:** 2024-06-12
66
- **End date:** 2024-12-10
77

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
# Challenge 2: Verify the memory safery of core intrinsics using raw pointers
22

33
- **Status:** Open
4-
- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/16)
4+
- **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
55
- **Start date:** *24/06/12*
66
- **End date:** *24/12/10*
77

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22

33
- **Status:** Open
44
- **Solution:**
5-
- **Tracking Issue:** <https://github.com/model-checking/verify-rust-std/issues/21>
5+
- **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
66
- **Start date:** 24/06/24
77
- **End date:** 24/12/10
88

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
# Challenge 4: Memory safety of BTreeMap's `btree::node` module
22

33
- **Status:** Open
4-
- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25)
4+
- **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
55
- **Start date:** *2024-07-01*
66
- **End date:** *2024-12-10*
77

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
# Challenge 5: Verify functions iterating over inductive data type: `linked_list`
22

33
- **Status:** Open
4-
- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29)
4+
- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
55
- **Start date:** *24/07/01*
66
- **End date:** *24/12/10*
77

0 commit comments

Comments
 (0)