Skip to content

Commit 02c1126

Browse files
dkcummingdkcumming
committed
Merge remote-tracking branch 'upstream/main' into add-kmir-tool
2 parents 9e5dd9d + 2f8269d commit 02c1126

1,523 files changed

Lines changed: 841622 additions & 25576 deletions

File tree

Some content is hidden

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

‎.github/copilot-instructions.md‎

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
# Verify Rust Standard Library — Code Review Guidelines
2+
3+
## Purpose & Scope
4+
5+
This repository is a fork of the Rust standard library used exclusively for formal verification. Verification targets include memory safety, undefined behavior, and functional correctness, depending on the specific challenge. PRs fall into four categories: **solving challenges**, **proposing new challenges**, **proposing new tools**, and **maintenance**.
6+
7+
## Approved Verification Tools
8+
9+
Only these tools are accepted: **Kani**, **VeriFast**, **Flux**, and **ESBMC (GOTO-Transcoder)**. Flag any PR that uses a tool not on this list — it must go through a separate tool application process first.
10+
11+
---
12+
13+
## General Rules (All PRs)
14+
15+
- The contribution must be automated and pass as part of PR CI checks. Contributors should maintain the proofs and provide support thoughtout the lifetime of the contest (i.e. keeping it up-to-date with infrastructure changes in the contest).
16+
- Changes must not alter the runtime logic of the standard library unless the change is proposed and incorporated upstream into the official Rust standard library.
17+
- All contributors must be properly credited. By submitting, contributors confirm they can use, modify, copy, and redistribute their contribution.
18+
- PRs should reference the relevant tracking issue (e.g., `Resolves #ISSUE-NUMBER`).
19+
- Merging requires approval from at least two committee members listed in `.github/pull_requests.toml`.
20+
21+
---
22+
23+
## Challenge Solutions (Highest Priority)
24+
25+
These PRs solve open verification challenges. Apply the strictest review criteria:
26+
27+
### Success Criteria Compliance
28+
- Verify the PR meets **every** success criterion listed in the specific challenge description. Partial solutions should be flagged.
29+
- Check the challenge page at `doc/src/challenges/` or the [challenge book](https://model-checking.github.io/verify-rust-std/challenges/) for the exact requirements.
30+
31+
### Formal Verification Rigor
32+
- **No vacuous proofs.** Ensure harnesses and contracts actually exercise the property under verification. A proof that passes trivially (e.g., with an unsatisfiable precondition or an empty harness body) is unacceptable.
33+
- **No unjustified assumptions.** Every `#[kani::assume]`, `requires`, or equivalent precondition must be justified by the function's documented safety contract or API invariants. Flag assumptions that over-constrain inputs to make verification pass.
34+
- **Contracts must reflect documented safety conditions.** Cross-reference preconditions and postconditions against the function's `# Safety` doc comments and the [official std library documentation](https://doc.rust-lang.org/std/).
35+
- **Harnesses must cover meaningful input ranges**, not just trivial or degenerate cases.
36+
- **Verification must actually run in CI** using one of the approved tools. Check that the relevant workflow (kani.yml, verifast.yml, flux.yml, goto-transcoder.yml) executes the new proofs.
37+
38+
### Code Quality for the Rust Standard Library
39+
- Code should be **idiomatic Rust** and match the style of the surrounding standard library code.
40+
- Unsafe code blocks must have a `// SAFETY:` comment explaining why the usage is sound.
41+
- Use `#[inline]` only on public, small, non-generic functions. Do not add `#[inline]` to generic methods or trait methods without default implementations. Avoid `#[inline(always)]` unless justified by benchmarks.
42+
- Contracts and harness code should be **readable and well-documented** so that someone unfamiliar can understand what property is being verified and why.
43+
- Verification annotations (contracts, harnesses, proof attributes) should be clearly separated from the library's functional code using `cfg` attributes (e.g., `#[cfg(kani)]`) so they don't affect normal compilation.
44+
- Do not introduce new public API surface unless the challenge explicitly requires it.
45+
46+
---
47+
48+
## New Challenge Proposals
49+
50+
- Must follow the template at `doc/src/challenge_template.md`.
51+
- Must include a tracking issue created with the challenge issue template.
52+
- Must add an entry in `doc/src/SUMMARY.md`.
53+
- Success criteria must be specific, measurable, and achievable with the currently approved tools.
54+
- Flag vague or overly broad success criteria.
55+
56+
---
57+
58+
## New Tool Applications
59+
60+
- Must be submitted as a separate issue using the "Tool Application" template before any PR using the tool.
61+
- The PR must include a new CI workflow that runs the tool against the standard library.
62+
- The PR must add a new entry to the "Approved Tools" section of the book.
63+
64+
---
65+
66+
## Maintenance PRs
67+
68+
- Repository updates, CI fixes, documentation improvements, and dependency bumps.
69+
- Should not change verification semantics or weaken existing proofs.
70+
- Flag any maintenance PR that removes or weakens existing contracts, harnesses, or proof obligations.
71+
72+
---
73+
74+
## Common Red Flags to Watch For
75+
76+
- Harness with no assertions or only trivial assertions.
77+
- `kani::assume(false)` or preconditions that make the proof vacuously true.
78+
- Assumptions that are stricter than what the function's safety docs require.
79+
- Contracts that don't match the `# Safety` section of the function being verified.
80+
- Verification code that is not gated behind a tool-specific `cfg` (e.g., `#[cfg(kani)]`).
81+
- Changes to `library/` source files that alter runtime behavior without upstream justification.
82+
- Missing or incorrect tracking issue references.
83+
- Use of a verification tool not in the approved list.
84+
- Large, hard-to-review PRs that should be split into smaller logical units.

‎.github/workflows/flux.yml‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
name: Flux
2+
3+
on:
4+
workflow_dispatch:
5+
push:
6+
branches: [main]
7+
pull_request:
8+
branches: [main]
9+
10+
env:
11+
FLUX_VERSION: "6b080b32801f923bfb590ac48e729de38f829f21"
12+
FIXPOINT_VERSION: "nightly-10-15-2025"
13+
14+
jobs:
15+
check-flux-on-core:
16+
runs-on: ubuntu-latest
17+
steps:
18+
- uses: actions/checkout@v4
19+
with:
20+
submodules: true
21+
22+
- name: Local Binaries
23+
run: |
24+
mkdir -p ~/.local/bin
25+
echo ~/.cargo/bin >> $GITHUB_PATH
26+
echo ~/.local/bin >> $GITHUB_PATH
27+
28+
- name: Download and install fixpoint
29+
run: |
30+
set -e
31+
NAME="fixpoint-x86_64-linux-gnu.tar.gz"
32+
URL="https://github.com/ucsd-progsys/liquid-fixpoint/releases/download/${FIXPOINT_VERSION}/${NAME}"
33+
34+
echo "Downloading from $URL"
35+
curl -fsSL --retry 3 -o "$NAME" "$URL"
36+
37+
echo "Extracting archive"
38+
tar -xzf "$NAME"
39+
mkdir -p ~/.local/bin
40+
cp fixpoint ~/.local/bin/fixpoint
41+
42+
echo "Cleaning up"
43+
rm -f "$NAME"
44+
45+
- name: Install Z3
46+
uses: cda-tum/setup-z3@v1.6.1
47+
with:
48+
version: 4.12.1
49+
platform: linux
50+
env:
51+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
52+
53+
- name: Clone Flux
54+
run: |
55+
git clone https://github.com/flux-rs/flux.git
56+
cd flux
57+
git checkout $FLUX_VERSION
58+
59+
- name: Rust Cache
60+
uses: Swatinem/rust-cache@v2.7.8
61+
with:
62+
workspaces: flux
63+
64+
- name: Install Flux
65+
run: |
66+
cd flux
67+
cargo x install
68+
69+
- name: Verify Core
70+
run: |
71+
cd library
72+
FLUXFLAGS="-Ftimings" cargo flux -p core

‎.github/workflows/kani-metrics.yml‎

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,20 @@ defaults:
1111

1212
jobs:
1313
update-kani-metrics:
14+
permissions:
15+
contents: write
16+
pull-requests: write
17+
if: github.repository == 'model-checking/verify-rust-std'
1418
runs-on: ubuntu-latest
1519

1620
steps:
21+
- name: Remove unnecessary software to free up disk space
22+
run: |
23+
# inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
24+
df -h
25+
sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
26+
df -h
27+
1728
- name: Checkout Repository
1829
uses: actions/checkout@v4
1930
with:
@@ -26,7 +37,9 @@ jobs:
2637
python-version: '3.x'
2738

2839
- name: Compute Kani Metrics
29-
run: ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
40+
run: |
41+
./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
42+
rm kani-list.json
3043
3144
- name: Create Pull Request
3245
uses: peter-evans/create-pull-request@v7

0 commit comments

Comments
 (0)