Verify atomic types and intrinsic wrappers for Challenge 7

.github/workflows/verifast-atomics.yml

@@ -0,0 +1,58 @@
+name: VeriFast atomics
+
+on:
+  workflow_dispatch:
+  merge_group:
+  pull_request:
+    branches: [main]
+  push:
+    paths:
+      - 'library/core/src/sync/atomic.rs'
+      - 'library/core/src/intrinsics/mod.rs'
+      - 'rust-toolchain.toml'
+      - 'verifast-proofs/core/sync/atomic.rs/**'
+      - '.github/workflows/verifast-atomics.yml'
+
+permissions:
+  contents: read
+
+jobs:
+  atomics:
+    name: Atomic safety including 128-bit types
+    runs-on: macos-14
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+      - name: Install pinned Rust compiler components
+        run: rustup toolchain install nightly-2025-11-25 --profile minimal --component rustc-dev,llvm-tools-preview,rust-src
+      - name: Cache verified download inputs and Cargo dependencies
+        uses: actions/cache@v4
+        with:
+          path: |
+            ${{ runner.temp }}/atomic-downloads
+            ${{ runner.temp }}/atomic-cargo
+          key: atomic-build-macos-arm64-${{ hashFiles('verifast-proofs/core/sync/atomic.rs/toolchain/provenance.json') }}
+      - name: Build experimental VeriFast and check the complete atomic scope
+        run: >-
+          python3 verifast-proofs/core/sync/atomic.rs/toolchain/build.py
+          --workdir "$RUNNER_TEMP/atomic-build"
+          --downloads "$RUNNER_TEMP/atomic-downloads"
+          --cargo-home "$RUNNER_TEMP/atomic-cargo"
+          --check
+      - name: Upload proof coverage, generated sources, and build evidence
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: atomic-safety-evidence
+          path: |
+            ${{ runner.temp }}/atomic-build/build-manifest.json
+            ${{ runner.temp }}/atomic-build/*.log
+            verifast-proofs/core/sync/atomic.rs/proof/*.log
+            verifast-proofs/core/sync/atomic.rs/proof/coverage.json
+            verifast-proofs/core/sync/atomic.rs/proof/verified/*.rs
+            verifast-proofs/core/sync/atomic.rs/proof/normalized-original/*.rs
+            verifast-proofs/core/sync/atomic.rs/checks/**/*.log
+            verifast-proofs/core/sync/atomic.rs/checks/operations/results.json

verifast-proofs/core/sync/atomic.rs/.gitattributes

@@ -0,0 +1,2 @@
+# Preserve release-relative patch bytes, including CRLF and context whitespace.
+toolchain/verifast-26.01-atomic-source.patch -text -whitespace

verifast-proofs/core/sync/atomic.rs/.gitignore

@@ -0,0 +1,16 @@
+__pycache__/
+*.log
+*.rmeta
+*.rlib
+*.o
+/proof/original/
+/proof/normalized-original/
+/proof/verified/
+/proof/clients*.rs
+/proof/coverage.json
+/checks/operations/*.rs
+!/checks/operations/positive.rs
+!/checks/operations/unsized-domain-rejected.rs
+/checks/operations/results.json
+/checks/decoder/replay-runtime/
+/checks/decoder/replay-fixtures/

verifast-proofs/core/sync/atomic.rs/README.md

@@ -0,0 +1,116 @@
+# Challenge 7: atomic safety
+
+This is an independently authored proposed solution for
+[Challenge 7](https://github.com/model-checking/verify-rust-std/issues/83). It uses
+VeriFast with the explicit source update in `toolchain/`. VeriFast is an approved
+tool; this particular update is unreleased and requires review. Passing this
+directory's checks does not by itself establish committee acceptance.
+
+## Verified scope
+
+| Requirement | Proof and enforced coverage |
+| --- | --- |
+| `from_ptr` | Bool, generic Ptr, all signed/unsigned 8/16/32/64/128-bit types, and Isize/Usize: all 14 bodies must appear in verifier output. |
+| Pointer values and element sizes | The pointer proof is generic over sized `T`, with arbitrary stored addresses. Concrete intrinsic callers also cover element sizes 0, 1, 2, 3, and 4. |
+| Unsafe operation wrappers | All 15 current wrappers, including signed minimum and both compare-exchange variants. |
+| Intrinsics | All 91 legal ordering combinations of the 15 current const-generic intrinsics, matched to the challenge's order-suffixed names. |
+| Panic paths | Invalid load/store and compare-exchange failure orderings execute the real panic paths and preserve atomic permissions on unwind. |
+| Source connection | Pinned source digests, complete module refinement after documented metadata preparation, and explicit coverage checks. |
+
+The proof covers the challenge's required unsafe functions. It does not claim
+that every public safe method in the atomic module has been verified. Optional
+panic-avoidance contracts for those public methods are not part of this solution.
+No runtime implementation in `library/` is changed.
+
+## Ownership and validity
+
+`from_ptr` accepts either initialized ordinary ownership or an existing atomic
+share. A ghost boolean selects the permission path. Fresh conversion borrows
+the ordinary storage for the returned reference's lifetime and retains a unique
+recovery token. Reusing a share creates no recovery token. Both paths return
+sharing and reference-initialization permissions. Fourteen concrete callers
+each create and use two references to the same storage.
+
+The sharing interpretation contains a fractional lifetime borrow of typed
+atomic ownership. Integers and raw pointers accept all values of their type;
+the boolean interpretation accepts only bytes 0 and 1. Ordinary ownership
+establishes allocation validity and initialization. Atomic ownership additionally
+requires actual atomic alignment and excludes conflicting ordinary or mixed-size
+accesses through the verifier's existing atomic-mask model. Splitting the
+atomic resource permits concurrent atomic access; converting it back requires
+recovering its complete permission and ending the relevant borrow.
+
+Intrinsic contracts require the correct operand domain. `T: Copy` alone is
+insufficient. Integer updates use the same integer type; pointer updates use
+`usize`; signed and unsigned min/max have separate domains. Pointer-domain
+lemmas require a sized pointee. Stores, swaps, and compare-exchanges require a
+valid new value. Arithmetic and bitwise updates require a proved closure witness
+carrying the operand type identities, operation, invariant, and update value.
+Boolean AND/OR/XOR witnesses pass; invariant-breaking NAND/addition witnesses
+fail. Loads preserve validity and may use a resource derived from fractional
+ordinary ownership. Writes require a resource derived from full ordinary ownership.
+
+## Trusted boundary and source preparation
+
+The trusted boundary consists of Rust's primitive atomic semantics, VeriFast's
+existing RustBelt lifetime/atomic model, the primitive contracts added by the
+patch, and rustc's exported ABI layout. The model proves safety under its
+permissions and invariants; it does not establish general concurrent functional
+correctness or a hardware memory-model theorem.
+
+The patch adds concrete atomic-order translation, operand guards, compiler
+resolved `Self`, propagation of macro contracts to every expansion, and
+compiler-derived struct alignment. Generic `repr(align(N))` supplies a minimum
+alignment and divisibility fact, not an assertion of exact alignment. The
+primitive update model includes explicit u8 equations and restricted boolean-byte
+value tables. Those primitive facts remain reviewable trusted contracts.
+
+`source-lock.json` pins both the atomic implementation and intrinsic declarations.
+The generator copies the current complete atomic module and replaces its 18
+`rustc_diagnostic_item` attributes with documentation attributes in both proof
+inputs. This prevents duplicate diagnostic items when checking the module beside
+the compiler's `core` dependency. The refinement claim is between these prepared
+inputs. In the verified input, the existing reference expression is assigned to
+a local result variable to attach ghost steps; whole-module refinement checks
+that transformation. All other executable code is preserved.
+
+No reference-creation check, unwind path, or dead-code check is disabled. No false
+precondition skips required types or orderings. Negative controls reject invalid
+types/orderings, missing domain or closure witnesses, ordinary/fractional write
+permissions, invalid boolean values, uninitialized conversion, and duplicate
+ownership/recovery. Isolated mutated-MIR decoder tests are not counted as Rust
+proofs; their replay exporter is never used in the real proof runtime.
+
+## Reproduction
+
+Use native ARM64 macOS with Python 3.12 or newer and the pinned Rust toolchain:
+
+```sh
+rustup toolchain install nightly-2025-11-25 --profile minimal --component rustc-dev,llvm-tools-preview,rust-src
+python3 verifast-proofs/core/sync/atomic.rs/toolchain/build.py \
+  --workdir /tmp/atomic-build \
+  --downloads /tmp/atomic-downloads \
+  --cargo-home /tmp/atomic-cargo \
+  --check
+```
+
+The build directory must not exist. Archives and the patch are checked against
+pinned SHA-256 digests. The decoder revision and Cargo dependency locks are
+pinned. The script extracts fresh sources/dependencies, builds the verifier,
+refinement checker, and Rust MIR exporter, then runs all proof and rejection
+checks. It writes logs, a build manifest, and a relocation wrapper in that build
+directory. `--offline` is supported when all archive and Cargo inputs are cached.
+
+The dedicated GitHub workflow uses `macos-14` because the pinned x86_64 Linux
+target does not expose 128-bit atomics, including with `cmpxchg16b` enabled. The
+proof runner fails if either 128-bit instantiation is missing. GitHub documents
+`macos-14` as an ARM64 standard runner in its
+[runner reference](https://docs.github.com/en/actions/reference/runners/github-hosted-runners).
+
+The CI artifact includes the generated proof sources, per-function coverage,
+control results, and fresh-build manifest. To rerun checks using a built runtime:
+
+```sh
+/tmp/atomic-build/with-build-env python3 verifast-proofs/core/sync/atomic.rs/check.py \
+  /tmp/atomic-build/verifast-26.01/bin
+```

verifast-proofs/core/sync/atomic.rs/check.py

@@ -0,0 +1,32 @@
+#!/usr/bin/env python3
+"""Run every safety, source-connection, and negative-control gate for atomics."""
+from pathlib import Path
+import json
+import subprocess
+import sys
+
+if len(sys.argv) != 2:
+    raise SystemExit('usage: check.py /absolute/path/to/experimental-runtime/bin')
+base = Path(__file__).resolve().parent
+runtime = Path(sys.argv[1]).resolve()
+checks = [
+    ('source and fresh/shared callers', base / 'proof/check.py', runtime),
+    ('compiler/layout/ownership controls', base / 'checks/source/check.py', runtime / 'verifast'),
+    ('intrinsic types, orderings, and invariants', base / 'checks/operations/run.py', runtime / 'verifast'),
+    ('ordering refinement controls', base / 'checks/refinement/check.py', runtime / 'refinement-checker'),
+]
+for name, script, argument in checks:
+    print('Checking ' + name, flush=True)
+    subprocess.run([sys.executable, str(script), str(argument)], check=True)
+provenance = json.loads((base / 'toolchain/provenance.json').read_text())
+schema = runtime.parent.parent / provenance['source_archive_prefix'] / 'src/rust_frontend/vf_mir/vf_mir.capnp'
+print('Checking malformed MIR with an isolated replay exporter', flush=True)
+subprocess.run([sys.executable, str(base / 'checks/decoder/check.py'), str(runtime), str(schema)], check=True)
+coverage = json.loads((base / 'proof/coverage.json').read_text())
+operations = json.loads((base / 'checks/operations/results.json').read_text())
+assert len(coverage['from_ptr_functions_verified']) == 14
+assert len(coverage['generic_operation_wrappers_verified']) == 15
+assert len(coverage['fresh_and_shared_callers_verified']) == 14
+assert all(coverage['from_ptr_negative_controls'].values())
+assert len(operations) == 29 and all(result['passed'] for result in operations)
+print('PASS: complete required atomic proof scope and all configured rejection controls.', flush=True)

verifast-proofs/core/sync/atomic.rs/checks/decoder/check.py

@@ -0,0 +1,99 @@
+"""Adversarial MIR decoder tests, NOT Rust proofs or a proof exporter.
+
+Replay mutated copies of the real pinned exporter output through an isolated
+runtime. The actual proof runtime and exporter are never modified.
+"""
+from pathlib import Path
+import os
+import subprocess
+import sys
+
+repo = next(p for p in Path(__file__).resolve().parents if (p / 'library/core/src/sync/atomic.rs').is_file())
+base = Path(__file__).resolve().parent
+runtime = base / 'replay-runtime'
+fixtures = base / 'replay-fixtures'
+runtime.mkdir(exist_ok=True)
+fixtures.mkdir(exist_ok=True)
+if len(sys.argv) != 3:
+    raise SystemExit('usage: check.py /path/to/runtime/bin /path/to/vf_mir.capnp')
+proof_bin = Path(sys.argv[1]).resolve()
+for source in proof_bin.iterdir():
+    target = runtime / source.name
+    if source.name != 'vf-rust-mir-exporter' and not target.exists():
+        target.symlink_to(source)
+exporter = runtime / 'vf-rust-mir-exporter'
+exporter.write_text('#!/bin/sh\nset -eu\ncat "$TF_REPLAY_CAPNP"\n')
+exporter.chmod(0o755)
+
+original = (base / 'original-mir.txt').read_text().replace('__ATOMIC_DECODER_FIXTURE__', str(base / 'intrinsic-gate.rs'))
+leaf = '( leaf = (data = (h = 0, l = 0), size = 4) )'
+branch = 'branch = [\n                                              ' + leaf + ' ]'
+assert original.count(branch) == 1
+
+def replace_once(old, new):
+    assert original.count(old) == 1, (old, original.count(old))
+    return original.replace(old, new)
+
+def replace_value_with_param():
+    start = original.index('value = (\n                                          ty = (')
+    begin = original.index('(', start)
+    depth = 1
+    end = begin + 1
+    while depth:
+        depth += (original[end] == '(') - (original[end] == ')')
+        end += 1
+    return original[:start] + 'param = (index = 0, name = "ORD")' + original[end:]
+
+malformed = 'expected a concrete fieldless AtomicOrdering enum constant'
+cases = {
+    'valid-relaxed': (original, 'No matching heap chunks:'),
+    'valid-release': (replace_once(leaf, leaf.replace('l = 0', 'l = 1')), 'No matching heap chunks:'),
+    'valid-seqcst': (replace_once(leaf, leaf.replace('l = 0', 'l = 4')), 'No matching heap chunks:'),
+    'other-enum': (replace_once('std::intrinsics::AtomicOrdering', 'unrelated::AtomicOrdering'), malformed),
+    'data-type-u16': (replace_once('type = (\n                                      kind = (uInt = (u8 = void)) )', 'type = (kind = (uInt = (u16 = void)))'), malformed),
+    'data-type-tuple': (replace_once('type = (\n                                      kind = (uInt = (u8 = void)) )', 'type = (kind = (tuple = [(kind = (uInt = (u8 = void))), (kind = (uInt = (u8 = void)))]))'), malformed),
+    'data-type-param': (replace_once('type = (\n                                      kind = (uInt = (u8 = void)) )', 'type = (kind = (param = "T"))'), malformed),
+    'integer-instead-of-enum': (replace_once('ty = (\n                                            kind = (\n                                              adt = (\n                                                id = (\n                                                  name = \"std::intrinsics::AtomicOrdering\" ),\n                                                kind = (enumKind = void),\n                                                substs = [] ) ) )', 'ty = (kind = (uInt = (u32 = void)))'), malformed),
+    'struct-kind': (replace_once('enumKind = void', 'structKind = void'), malformed),
+    'union-kind': (replace_once('enumKind = void', 'unionKind = void'), malformed),
+    'enum-has-type-args': (replace_once('substs = []', 'substs = [(kind = (type = (kind = (uInt = (u8 = void))))) ]'), malformed),
+    'empty-branch': (replace_once(branch, 'branch = []'), malformed),
+    'payload-branch': (replace_once(branch, 'branch = [' + leaf + ', ' + leaf + ']'), malformed),
+    'bare-leaf': (replace_once(branch, 'leaf = (data = (h = 0, l = 0), size = 4)'), malformed),
+    'scalar-width-0': (replace_once(leaf, leaf.replace('size = 4', 'size = 0')), malformed),
+    'scalar-width-1': (replace_once(leaf, leaf.replace('size = 4', 'size = 1')), malformed),
+    'scalar-width-8': (replace_once(leaf, leaf.replace('size = 4', 'size = 8')), malformed),
+    'symbolic-param': (replace_value_with_param(), malformed),
+    'late-bound-param': (replace_once('lateBoundGenericParamCount = 0', 'lateBoundGenericParamCount = 1'), 'late-bound generic arguments are not permitted'),
+    'invalid-acquire': (replace_once(leaf, leaf.replace('l = 0', 'l = 2')), 'Acquire and AcqRel are not permitted for stores'),
+    'invalid-acqrel': (replace_once(leaf, leaf.replace('l = 0', 'l = 3')), 'Acquire and AcqRel are not permitted for stores'),
+    'index-5': (replace_once(leaf, leaf.replace('l = 0', 'l = 5')), 'invalid AtomicOrdering variant index'),
+    'index-over-u32': (replace_once(leaf, leaf.replace('l = 0', 'l = 4294967296')), 'invalid AtomicOrdering variant index'),
+    'index-high-u64': (replace_once(leaf, leaf.replace('h = 0', 'h = 1')), 'invalid AtomicOrdering variant index'),
+    'other-function': (replace_once('std::intrinsics::atomic_store', 'unrelated::atomic_store'), 'Unsupported constant value tree'),
+}
+# The fixture's surrounding pointer type still says u8, so changing only
+# the intrinsic type to u16 reaches argument type checking. It is not a proof.
+cases['data-type-u16'] = (cases['data-type-u16'][0], 'Type mismatch')
+cases['data-type-tuple'] = (cases['data-type-tuple'][0], 'operand must be an integer')
+cases['data-type-param'] = (cases['data-type-param'][0], 'No such type parameter')
+schema = Path(sys.argv[2]).resolve()
+include = Path(os.environ['CAPNP_INC_DIR'])
+summary = []
+for name, (fixture, expected) in cases.items():
+    text_file = fixtures / f'{name}.txt'
+    binary_file = fixtures / f'{name}.bin'
+    log_file = fixtures / f'{name}.log'
+    text_file.write_text(fixture)
+    binary = subprocess.run(['capnp', 'encode', '-I' + str(include), str(schema), 'VfMir'], input=fixture.encode(), stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=True).stdout
+    binary_file.write_bytes(binary)
+    env = dict(os.environ, TF_REPLAY_CAPNP=str(binary_file))
+    result = subprocess.run([str(runtime / 'verifast'), '-rustc_args', '--edition=2024 --crate-type=lib', str(base / 'intrinsic-gate.rs')], cwd=repo, env=env, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, text=True, timeout=30)
+    log_file.write_text('LOCALPATCH / MUTATED MIR REPLAY TEST ONLY\n' + result.stdout)
+    ok = result.returncode != 0 and expected in result.stdout
+    summary.append(f'{name}: {"PASS" if ok else "FAIL"} (exit {result.returncode}); expected {expected}')
+    if not ok:
+        print(result.stdout)
+        raise RuntimeError(name)
+(base / 'translator-mutations.log').write_text('LOCALPATCH / MUTATED MIR REPLAY TESTS ONLY\n' + '\n'.join(summary) + '\n')
+print('\n'.join(summary))

verifast-proofs/core/sync/atomic.rs/checks/decoder/intrinsic-gate.rs

@@ -0,0 +1,12 @@
+#![feature(core_intrinsics)]
+
+// Exact current-Rust intrinsic shape used by the atomic_store wrapper.
+unsafe fn store_relaxed(dst: *mut u8, val: u8)
+//@ req *dst |-> _;
+//@ ens *dst |-> val;
+//@ on_unwind_ens false;
+{
+    unsafe {
+        std::intrinsics::atomic_store::<u8, { std::intrinsics::AtomicOrdering::Relaxed }>(dst, val)
+    }
+}