Isolate Rust unsafety in audited boundaries (8.4) (#379)

.github/workflows/rust-boundaries.yml

@@ -0,0 +1,268 @@
+---
+name: Rust boundary verification
+
+on:
+  pull_request:
+    paths:
+      - 'rust/**'
+      - 'cuprum/_streams_rs.py'
+      - 'cuprum/_pipeline_stream*.py'
+      - 'pyproject.toml'
+      - 'scripts/*boundary*'
+      - 'scripts/tests/test_boundary*'
+      - 'tools/**'
+      - 'Makefile'
+      - '.github/workflows/rust-boundaries.yml'
+  schedule:
+    - cron: '23 4 * * 1'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: rust-boundaries-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+jobs:
+  native:
+    name: Native contracts (${{ matrix.os }})
+    runs-on: ${{ matrix.os }}
+    timeout-minutes: 20
+    strategy:
+      fail-fast: false
+      max-parallel: 2
+      matrix:
+        os: [ubuntu-latest, windows-2022, macos-latest]
+    defaults:
+      run:
+        shell: bash
+        working-directory: rust
+    env:
+      CARGO_BUILD_JOBS: '2'
+      RUSTFLAGS: '-D warnings'
+    steps:
+      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955  # v4
+        with:
+          # The job builds and runs repository code, so the checkout token
+          # must not stay in .git/config where that code could reach it.
+          persist-credentials: false
+      - name: Compute shared dependency cache keys
+        uses: ./.github/actions/cache-keys
+        with:
+          python-version: '3.13'
+      - name: Restore the shared Cargo registry
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+          key: ${{ env.CARGO_CACHE_KEY }}
+          restore-keys: ${{ env.CARGO_CACHE_PREFIX }}
+      - name: Install supported project toolchain
+        run: rustup toolchain install 1.85.0 --profile minimal --component clippy
+      - name: Restore the Linux boundary compiler cache
+        if: runner.os == 'Linux'
+        id: boundary-cache
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: ~/.cache/sccache
+          key: boundary-native-linux-${{ github.run_id }}
+          restore-keys: boundary-native-linux-
+      - name: Set up sccache
+        if: runner.os == 'Linux'
+        uses: ./.github/actions/setup-sccache
+        with:
+          cache-size: 1G
+      - name: Reset compiler-cache counters
+        if: runner.os == 'Linux'
+        run: sccache --zero-stats
+      - name: Check default feature configuration
+        run: cargo check -p cuprum-streams -p cuprum-native-io --all-targets --no-default-features
+      - name: Lint all feature and helper targets
+        run: cargo clippy -p cuprum-streams -p cuprum-native-io --all-targets --all-features -- -D warnings
+      - name: Exercise native effects and safe stream policy
+        run: |
+          set -o pipefail
+          mkdir -p target/boundary-verification
+          cargo test -p cuprum-streams -p cuprum-native-io --all-targets --all-features 2>&1 |
+            tee target/boundary-verification/native.log
+      - name: Record compiler-cache effectiveness
+        if: always() && runner.os == 'Linux'
+        run: sccache --show-stats --stats-format json
+      - name: Archive native evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02  # v4
+        with:
+          name: native-boundaries-${{ runner.os }}
+          path: rust/target/boundary-verification
+          retention-days: 14
+
+      - name: Save reviewed boundary cache generation
+        if: runner.os == 'Linux' && github.event_name == 'schedule' && github.ref == 'refs/heads/main'
+        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: ~/.cache/sccache
+          key: ${{ steps.boundary-cache.outputs.cache-primary-key }}
+
+  verus:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955  # v4
+        with:
+          # The job builds and runs repository code, so the checkout token
+          # must not stay in .git/config where that code could reach it.
+          persist-credentials: false
+      - name: Compute shared dependency cache keys
+        uses: ./.github/actions/cache-keys
+        with:
+          python-version: '3.13'
+      - name: Restore the shared Cargo registry
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+          key: ${{ env.CARGO_CACHE_KEY }}
+          restore-keys: ${{ env.CARGO_CACHE_PREFIX }}
+      - uses: astral-sh/setup-uv@f98e06938123ccabd21905ea5d0069192241f9f1  # v8.3.1
+        with:
+          python-version: '3.13'
+      - name: Restore pinned verifier, solver, and compiler objects
+        id: boundary-cache
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.local/share/cuprum-verus-0.2026.09.06.8dea4a2
+            ~/.rustup/toolchains/1.98.0-x86_64-unknown-linux-gnu
+            .cache/boundary-z3
+            ~/.cache/sccache
+          key: boundary-verus-${{ hashFiles('tools/verus/*', 'scripts/install_boundary_z3.py') }}-${{ github.run_id }}
+          restore-keys: boundary-verus-${{ hashFiles('tools/verus/*', 'scripts/install_boundary_z3.py') }}-
+      - name: Set up sccache
+        uses: ./.github/actions/setup-sccache
+        with:
+          cache-size: 1G
+      - name: Reset compiler-cache counters
+        run: sccache --zero-stats
+      - name: Install prebuilt verifier and solver
+        run: |
+          make install-verus
+          rustup toolchain install 1.98.0 --profile minimal
+      - name: Test proof correspondence and binary installation contracts
+        run: uv run pytest scripts/tests/test_boundary_*.py
+      - name: Verify production kernels and compiler prohibition
+        run: |
+          set -o pipefail
+          mkdir -p rust/target/boundary-verification
+          make boundary-verus boundary-contract 2>&1 | tee rust/target/boundary-verification/verus.log
+      - name: Record compiler-cache effectiveness
+        if: always()
+        run: sccache --show-stats --stats-format json
+      - name: Archive proof and negative compiler evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02  # v4
+        with:
+          name: verus-and-compiler-contracts
+          path: rust/target/boundary-verification
+          retention-days: 14
+
+      - name: Save reviewed boundary cache generation
+        if: github.event_name == 'schedule' && github.ref == 'refs/heads/main'
+        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.local/share/cuprum-verus-0.2026.09.06.8dea4a2
+            ~/.rustup/toolchains/1.98.0-x86_64-unknown-linux-gnu
+            .cache/boundary-z3
+            ~/.cache/sccache
+          key: ${{ steps.boundary-cache.outputs.cache-primary-key }}
+
+  extended:
+    if: github.event_name != 'pull_request'
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    strategy:
+      fail-fast: false
+      max-parallel: 1
+      matrix:
+        check: [kani, miri]
+    env:
+      CARGO_BUILD_JOBS: '2'
+    steps:
+      - uses: actions/checkout@08eba0b27e820071cde6df949e0beb9ba4906955  # v4
+        with:
+          # The job builds and runs repository code, so the checkout token
+          # must not stay in .git/config where that code could reach it.
+          persist-credentials: false
+      - name: Compute shared dependency cache keys
+        uses: ./.github/actions/cache-keys
+        with:
+          python-version: '3.13'
+      - name: Restore the shared Cargo registry
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+          key: ${{ env.CARGO_CACHE_KEY }}
+          restore-keys: ${{ env.CARGO_CACHE_PREFIX }}
+      - uses: astral-sh/setup-uv@f98e06938123ccabd21905ea5d0069192241f9f1  # v8.3.1
+        with:
+          python-version: '3.13'
+      - name: Restore proof tools and Miri sysroots
+        id: boundary-cache
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.kani
+            ~/.cache/miri
+            ~/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu
+            ~/.rustup/toolchains/nightly-2026-08-07-x86_64-unknown-linux-gnu
+            .cache/boundary-kani
+            .cache/boundary-z3
+            ~/.local/share/cuprum-verus-0.2026.09.06.8dea4a2
+            ~/.rustup/toolchains/1.98.0-x86_64-unknown-linux-gnu
+          key: boundary-${{ matrix.check }}-${{ hashFiles('tools/kani/*', 'Makefile') }}
+      - name: Install prebuilt Kani frontend and bundle
+        if: matrix.check == 'kani'
+        run: |
+          make install-boundary-kani
+          echo "${GITHUB_WORKSPACE}/.cache/boundary-kani/bin" >> "$GITHUB_PATH"
+      - name: Install pinned Miri binary toolchain
+        if: matrix.check == 'miri'
+        run: rustup toolchain install nightly-2026-08-07 --profile minimal --component miri
+      - name: Execute extended verification
+        run: |
+          set -o pipefail
+          mkdir -p rust/target/boundary-verification
+          make boundary-${{ matrix.check }} 2>&1 | tee rust/target/boundary-verification/${{ matrix.check }}.log
+      - name: Exercise deliberate production faults
+        if: matrix.check == 'kani'
+        run: |
+          make install-verus
+          rustup toolchain install 1.98.0 --profile minimal
+          make boundary-faults
+      - name: Archive proof summaries and failures
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02  # v4
+        with:
+          name: extended-${{ matrix.check }}
+          path: rust/target/boundary-verification
+          retention-days: 14
+
+      - name: Save reviewed boundary cache generation
+        if: github.event_name == 'schedule' && github.ref == 'refs/heads/main'
+        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.kani
+            ~/.cache/miri
+            ~/.rustup/toolchains/nightly-2025-11-21-x86_64-unknown-linux-gnu
+            ~/.rustup/toolchains/nightly-2026-08-07-x86_64-unknown-linux-gnu
+            .cache/boundary-kani
+            .cache/boundary-z3
+            ~/.local/share/cuprum-verus-0.2026.09.06.8dea4a2
+            ~/.rustup/toolchains/1.98.0-x86_64-unknown-linux-gnu
+          key: ${{ steps.boundary-cache.outputs.cache-primary-key }}

Makefile

@@ -60,6 +60,8 @@ TEST_CARGO_BUILD_JOBS ?= 1
 PYTEST_WORKERS ?= 0
 PYTEST_TARGETS ?= cuprum/unittests/test_*.py \
   tests/test_ci_*.py \
+  tests/test_native_sdist.py \
+  scripts/tests/test_boundary_*.py \
   tests/behaviour/test_[a-h]*.py \
   tests/behaviour/test_[i-r]*.py \
   tests/behaviour/test_[s-z]*.py
@@ -336,3 +338,46 @@ benchmark-e2e: build uv ## Run hyperfine end-to-end throughput benchmark
 help: ## Show available targets
 	@grep -E '^[a-zA-Z_-]+:.*?##' $(MAKEFILE_LIST) | \
 	awk 'BEGIN {FS=":"; printf "Available targets:\n"} {printf "  %-20s %s\n", $$1, $$2}'
+
+# Boundary verifiers use their own pinned binary toolchains; normal gates keep
+# rust/rust-toolchain.toml. Kani install is deliberately not source-built here.
+PROVER_TOOLS_SOURCE ?= git+https://github.com/leynos/rust-prover-tools@98929b558253659a0a8ae03be7c49dafeef5f673
+PROVER_TOOLS = $(UV_RUN_ENV) uv tool run --python 3.14 --from $(PROVER_TOOLS_SOURCE) prover-tools
+VERUS_INSTALL_DIR ?= $(HOME)/.local/share/cuprum-verus-0.2026.09.06.8dea4a2
+MIRI_TOOLCHAIN = nightly-2026-08-07
+KANI_VERSION = 0.67.0
+KANI_LIBRARY_PATH = $(HOME)/.kani/kani-$(KANI_VERSION)/toolchain/lib:$(HOME)/.kani/kani-$(KANI_VERSION)/lib
+
+.PHONY: install-verus boundary-verus boundary-kani boundary-miri boundary-test
+install-verus: ## Install the checksum-verified prebuilt Verus release
+	$(PROVER_TOOLS) verus install --install-dir $(VERUS_INSTALL_DIR)
+	$(UV_RUN_ENV) uv run python scripts/install_boundary_z3.py
+
+boundary-verus: ## Verify actual production length/accounting kernels
+	$(UV_RUN_ENV) uv run python scripts/render_boundary_proofs.py
+	VERUS_Z3_PATH=$(CURDIR)/.cache/boundary-z3/z3 RUSTUP_TOOLCHAIN=1.98.0 $(VERUS_INSTALL_DIR)/verus/verus rust/target/boundary-verification/progress.rs --crate-type=lib
+
+boundary-kani: ## Check bounded native ownership and existing policy proofs
+	$(PROVER_TOOLS) kani check-version
+	cd $(RUST_DIR) && LD_LIBRARY_PATH="$(KANI_LIBRARY_PATH)" $(CARGO) kani --package cuprum-native-io
+	cd $(RUST_DIR) && LD_LIBRARY_PATH="$(KANI_LIBRARY_PATH)" $(CARGO) kani --package cuprum-streams
+
+boundary-miri: ## Interpret isolated native resource and memory paths
+	cd $(RUST_DIR) && $(CARGO) +$(MIRI_TOOLCHAIN) miri test --package cuprum-native-io --lib
+
+boundary-test: ## Run isolated native integration and verification-tool contracts
+	cd $(RUST_DIR) && $(CARGO) test --package cuprum-native-io --lib
+	$(UV_RUN_ENV) uv run pytest scripts/tests/test_boundary_*.py
+
+.PHONY: install-boundary-kani
+install-boundary-kani: ## Install checksum-verified Kani binaries without a source build
+	$(UV_RUN_ENV) uv run python scripts/install_boundary_kani.py
+	PATH="$(CURDIR)/.cache/boundary-kani/bin:$(PATH)" $(CARGO) kani setup --use-local-bundle $(CURDIR)/.cache/boundary-kani/kani-$(KANI_VERSION)-x86_64-unknown-linux-gnu.tar.gz
+
+.PHONY: boundary-contract
+boundary-contract: ## Confirm actual safe targets reject all forms of unsafe Rust
+	$(UV_RUN_ENV) uv run python scripts/check_boundary_contract.py
+
+.PHONY: boundary-faults
+boundary-faults: ## Require proof and real-unwind regressions to detect deliberate faults
+	$(UV_RUN_ENV) uv run python -m scripts.check_boundary_faults

cuprum/_pipeline_stream_fds.py

@@ -87,17 +87,24 @@ class _ReaderPause:
     A transport with no ``pause_reading`` hook has no callbacks to race. One
     with a pause hook but no ``resume_reading`` hook is unsafe to hand off: it
     cannot be paused and later returned to asyncio, so it must fall back.
+
+    ``closing_transport`` marks the one decline its caller may overrule. A
+    closing transport must not have its descriptor duplicated, but a caller
+    that supplies its own descriptors is never exposed to that hazard.
     """
 
     may_hand_off: bool
     resume: cabc.Callable[[], None] | None
     decline_reason: RustPumpDeclineReason | None
+    closing_transport: bool
 
     def __init__(
         self,
         may_hand_off: object = None,
         resume: cabc.Callable[[], None] | None = None,
         decline_reason: RustPumpDeclineReason | None = None,
+        *,
+        closing_transport: bool = False,
     ) -> None:
         """Record a pause outcome, deriving its verdict from a decline reason."""
         object.__setattr__(
@@ -107,13 +114,33 @@ def __init__(
         )
         object.__setattr__(self, "resume", resume)
         object.__setattr__(self, "decline_reason", decline_reason)
+        object.__setattr__(self, "closing_transport", closing_transport)
 
 
 def _pause_reader_transport(
     reader: asyncio.StreamReader,
 ) -> _ReaderPause:
-    """Pause reader callbacks while a duplicate-backed native worker pumps."""
+    """Pause reader callbacks while a duplicate-backed native worker pumps.
+
+    A closing transport is reported as ``closing_transport`` rather than
+    declined outright: only a caller that derives the worker descriptor from
+    this transport is exposed to the hazard, and only that caller may overrule
+    the decline.
+
+    Returns
+    -------
+    _ReaderPause
+        The hand-off verdict, and the resume hook when a pause was applied.
+    """
     transport = _stream_transport(reader)
+    is_closing = getattr(transport, "is_closing", None)
+    if callable(is_closing) and is_closing():
+        # asyncio silently ignores pause on a closing transport. Its queued
+        # connection_lost callback can still close the FD during hand-off.
+        return _ReaderPause(
+            decline_reason=RustPumpDeclineReason.READER_PAUSE_FAILED,
+            closing_transport=True,
+        )
     pause_reading = getattr(transport, "pause_reading", None)
     resume_reading = getattr(transport, "resume_reading", None)
     if not callable(pause_reading):