Draft: production coding runs and benchmark-driven hardening #275
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Foundation verification | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| workflow_dispatch: | |
| inputs: | |
| proof_impact_base: | |
| description: Immutable base commit for proof-impact comparison | |
| required: true | |
| type: string | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: foundation-${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| CARGO_BUILD_JOBS: "1" | |
| RUST_VERSION: 1.97.1 | |
| VERUS_VERSION: 0.2026.08.09.92f466f | |
| VERUS_LINUX_SHA256: 2f5a41c553f424aacdd732339e9d125563716a0b003c27730f75d6f81a282cef | |
| PERITUS_PROOF_IMPACT_BASE: ${{ github.event.pull_request.base.sha || github.event.before || inputs.proof_impact_base }} | |
| jobs: | |
| bootstrap: | |
| name: Verify pre-Cargo policy | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 5 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Verify reviewed pre-Cargo policy | |
| shell: bash | |
| run: git diff --no-ext-diff --no-textconv --exit-code 6ca5f56d2ab12e93f155d684b33f4a86c2f877b8 -- .cargo/config.toml .gitattributes | |
| rust: | |
| name: Rust (${{ matrix.os }}) | |
| needs: bootstrap | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-24.04, macos-15, windows-2025] | |
| runs-on: ${{ matrix.os }} | |
| timeout-minutes: 45 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| components: clippy,rustfmt | |
| - name: Check formatting | |
| run: cargo run --locked --package xtask -- format-check | |
| - name: Build every target | |
| run: cargo build --workspace --all-targets --all-features --locked | |
| - name: Run tests | |
| run: cargo test --workspace --all-targets --all-features --locked -- --test-threads=1 | |
| - name: Run documentation tests | |
| run: cargo test --doc --workspace --all-features --locked | |
| - name: Deny Clippy warnings | |
| run: cargo clippy --workspace --all-targets --all-features --locked -- -D warnings | |
| - name: Deny rustdoc warnings | |
| run: cargo doc --workspace --all-features --no-deps --locked | |
| env: | |
| RUSTDOCFLAGS: -D warnings | |
| - name: Enforce workspace policy | |
| run: cargo run --locked --package xtask -- all | |
| supply-chain: | |
| name: Licenses and dependency policy | |
| needs: bootstrap | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| - name: Install pinned cargo-deny | |
| run: cargo install cargo-deny --version 0.20.2 --locked | |
| - name: Check advisories, licenses, bans, and sources | |
| run: cargo deny --locked check | |
| verus: | |
| name: Locked Verus workspace | |
| needs: bootstrap | |
| runs-on: ubuntu-24.04 | |
| timeout-minutes: 40 | |
| steps: | |
| - name: Check out repository | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Install pinned Rust | |
| uses: dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772 # v1 | |
| with: | |
| toolchain: ${{ env.RUST_VERSION }} | |
| - name: Install digest-checked Verus archive | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| archive="$RUNNER_TEMP/verus.zip" | |
| install_root="$RUNNER_TEMP/peritus-verus" | |
| curl --fail --location --retry 3 \ | |
| --output "$archive" \ | |
| "https://github.com/verus-lang/verus/releases/download/release/$VERUS_VERSION/verus-$VERUS_VERSION-x86-linux.zip" | |
| printf '%s %s\n' "$VERUS_LINUX_SHA256" "$archive" | sha256sum --check --strict | |
| mkdir -p "$install_root" | |
| unzip -q "$archive" -d "$install_root" | |
| printf '%s\n' "$install_root/verus-x86-linux" >> "$GITHUB_PATH" | |
| - name: Probe every pinned tool component | |
| run: cargo run --locked --package xtask -- toolchain-check | |
| - name: Enforce ordinary-Rust formal API contracts | |
| run: cargo run --locked --package xtask -- ordinary-api-check | |
| - name: Verify the full applicable workspace | |
| run: cargo verus verify --workspace --all-features --locked --check-toolchain --fwd-verus-args-to roots -- --rlimit 20 | |
| - name: Reject proof cheats in every V and H root | |
| run: cargo verus verify --package peritus-agent --package peritus-app-protocol --package peritus-approval --package peritus-artifact-store --package peritus-budget --package peritus-codec --package peritus-collaboration --package peritus-context --package peritus-daemon --package peritus-debugger --package peritus-eval --package peritus-evidence --package peritus-evolution --package peritus-gates --package peritus-git --package peritus-harness --package peritus-journal --package peritus-kernel --package peritus-leases --package peritus-mcp --package peritus-memory --package peritus-migrations --package peritus-model-protocol --package peritus-network --package peritus-orchestrator --package peritus-patch --package peritus-plugin-host --package peritus-plugin-sdk --package peritus-policy --package peritus-process --package peritus-product-runner --package peritus-product-state --package peritus-projection --package peritus-protocol --package peritus-provider-anthropic --package peritus-provider-compatible --package peritus-provider-core --package peritus-provider-google --package peritus-provider-openai --package peritus-quality-policy --package peritus-release-policy --package peritus-review --package peritus-role --package peritus-sandbox --package peritus-sandbox-linux --package peritus-sandbox-macos --package peritus-sandbox-windows --package peritus-scheduler --package peritus-secrets --package peritus-security-policy --package peritus-spec --package peritus-telemetry --package peritus-tool-protocol --package peritus-tool-router --package peritus-tools-fs --package peritus-tools-git --package peritus-tools-quality --package peritus-tools-shell --package peritus-trace --package peritus-types --package peritus-workspace --all-features --locked --check-toolchain --fwd-verus-args-to roots -- --no-cheating --rlimit 20 | |
| - name: Produce the full verified release build | |
| run: cargo verus build --workspace --all-features --release --locked --check-toolchain --fwd-verus-args-to roots -- --rlimit 20 | |
| - name: Build every V and H root without proof cheats | |
| run: cargo verus build --package peritus-agent --package peritus-app-protocol --package peritus-approval --package peritus-artifact-store --package peritus-budget --package peritus-codec --package peritus-collaboration --package peritus-context --package peritus-daemon --package peritus-debugger --package peritus-eval --package peritus-evidence --package peritus-evolution --package peritus-gates --package peritus-git --package peritus-harness --package peritus-journal --package peritus-kernel --package peritus-leases --package peritus-mcp --package peritus-memory --package peritus-migrations --package peritus-model-protocol --package peritus-network --package peritus-orchestrator --package peritus-patch --package peritus-plugin-host --package peritus-plugin-sdk --package peritus-policy --package peritus-process --package peritus-product-runner --package peritus-product-state --package peritus-projection --package peritus-protocol --package peritus-provider-anthropic --package peritus-provider-compatible --package peritus-provider-core --package peritus-provider-google --package peritus-provider-openai --package peritus-quality-policy --package peritus-release-policy --package peritus-review --package peritus-role --package peritus-sandbox --package peritus-sandbox-linux --package peritus-sandbox-macos --package peritus-sandbox-windows --package peritus-scheduler --package peritus-secrets --package peritus-security-policy --package peritus-spec --package peritus-telemetry --package peritus-tool-protocol --package peritus-tool-router --package peritus-tools-fs --package peritus-tools-git --package peritus-tools-quality --package peritus-tools-shell --package peritus-trace --package peritus-types --package peritus-workspace --all-features --release --locked --check-toolchain --fwd-verus-args-to roots -- --no-cheating --rlimit 20 |