site: polish the explainer against the Impeccable design guidelines #106
Workflow file for this run
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
| # SPDX-License-Identifier: Apache-2.0 | |
| # | |
| # Merge-gate pipeline (specs.md §15). Every job below must pass for a PR to | |
| # merge. The pipeline is pinned to the project toolchain (the stable channel in | |
| # rust-toolchain.toml) for determinism; post-pivot there is no nightly-only | |
| # proving substrate. Golden-parity (export harness) gates are wired by their own | |
| # issues (backlog M2/M7). | |
| name: CI | |
| on: | |
| pull_request: | |
| push: | |
| branches: [main] | |
| permissions: | |
| contents: read | |
| # Cancel superseded runs on the same ref to keep the queue short. | |
| concurrency: | |
| group: ci-${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| env: | |
| CARGO_TERM_COLOR: always | |
| # Pinned project toolchain (must match rust-toolchain.toml). | |
| TOOLCHAIN: "stable" | |
| jobs: | |
| format: | |
| name: Format (cargo fmt --check) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable) | |
| with: | |
| toolchain: "stable" | |
| components: rustfmt | |
| - run: cargo fmt --all -- --check | |
| clippy: | |
| name: Lint (clippy -D warnings) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable) | |
| with: | |
| toolchain: "stable" | |
| components: clippy | |
| - uses: Swatinem/rust-cache@v2 | |
| - run: cargo clippy --all-targets --all-features --locked -- -D warnings | |
| test: | |
| name: Tests | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable) | |
| with: | |
| toolchain: "stable" | |
| - uses: Swatinem/rust-cache@v2 | |
| - run: cargo test --workspace --all-features --locked | |
| # Gate the headline claim: prove+verify the full 192-dim/6-block/16-head | |
| # predictor. It is #[ignore]d for the default (debug) run because it is heavy | |
| # in debug; in release it takes ~0.1 s. | |
| - name: Full-dims predictor (ignored, release) | |
| run: cargo test --workspace --all-features --release --locked -- --ignored | |
| msrv: | |
| name: MSRV (Rust 1.85) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| # The workspace pins rust-version = "1.85"; verify the first-party crates | |
| # actually build on that floor (a dependency or syntax bump that needs a | |
| # newer compiler must be a deliberate MSRV change, not a silent drift). | |
| - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable) | |
| with: | |
| toolchain: "1.85" | |
| - uses: Swatinem/rust-cache@v2 | |
| - run: cargo build --workspace --locked | |
| no-std: | |
| name: no_std verifier build | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable) | |
| with: | |
| toolchain: "stable" | |
| - uses: Swatinem/rust-cache@v2 | |
| # Canonical gate (specs.md §11.2): the verifier chain compiles with no | |
| # default features and no floating point. Post-pivot pwm-core and | |
| # pwm-verifier are #![no_std] with only blake2 (no_std) as a dependency, so | |
| # the no_std contract holds without any proving substrate. | |
| - run: cargo build -p pwm-verifier --no-default-features --locked | |
| - run: cargo build -p pwm-core --no-default-features --locked | |
| docs: | |
| name: Doc build + link check | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable) | |
| with: | |
| toolchain: "stable" | |
| - uses: Swatinem/rust-cache@v2 | |
| # rustdoc for the public API; -D warnings fails on broken intra-doc links. | |
| - run: cargo doc --workspace --no-deps --locked | |
| env: | |
| RUSTDOCFLAGS: "-D warnings" | |
| # Internal cross-reference check across the docs corpus (file + anchor). | |
| - name: Internal link check (docs/) | |
| run: python3 ci/check-links.py | |
| # Python<->Rust canonical-encoding parity (the export-side commitment bridge). | |
| - name: Export canonical parity (Python vs Rust) | |
| run: python3 crates/pwm-export/python/tests/test_canonical_parity.py | |
| # Export pipeline (E-201/202/203/208) on synthetic le-wm-shaped data (NumPy). | |
| - name: Export pipeline (ingest/quantize/fold/bundle) | |
| run: | | |
| python3 -m pip install --quiet numpy | |
| python3 crates/pwm-export/python/tests/test_export_pipeline.py | |
| # Python lint (config in crates/pwm-export/python/pyproject.toml). Pinned ruff. | |
| - name: Python lint (ruff) | |
| run: pipx run ruff==0.15.16 check crates/pwm-export/python | |
| license: | |
| name: License / SPDX | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: SPDX header check | |
| run: bash ci/check-spdx.sh | |
| # Full supply-chain gate: licenses + security advisories + yanked crates + | |
| # banned/duplicate deps + source allow-list (config in deny.toml). | |
| - name: cargo-deny (licenses + advisories + bans + sources) | |
| uses: EmbarkStudios/cargo-deny-action@v2 | |
| with: | |
| command: check | |
| mutation: | |
| name: Constraint mutation (scoped) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable) | |
| with: | |
| toolchain: "stable" | |
| - uses: Swatinem/rust-cache@v2 | |
| # Skeleton scope: the runner evaluates every registered campaign (only the | |
| # empty campaign exists yet) and exits non-zero on a survivor or a score | |
| # below target (INV-TEST-05). Components register real campaigns as they land. | |
| - run: cargo run -p pwm-testkit --bin mutation_runner --locked | |
| lean: | |
| name: Lean soundness proofs (D-805) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| # Builds the argmin uniqueness proof + the Freivalds probability bound. | |
| # Install elan/toolchain manually with retries: GitHub release downloads | |
| # intermittently 504, and `lean-action`'s installer has no retry, so a | |
| # transient blip fails the whole job. Mathlib oleans come from the (reliable) | |
| # `lake exe cache get` Azure cache — no Mathlib rebuild. | |
| - name: Install elan + Lean toolchain (retry transient GitHub 504s) | |
| working-directory: lean | |
| run: | | |
| set -euo pipefail | |
| url=https://github.com/leanprover/elan/releases/latest/download/elan-x86_64-unknown-linux-gnu.tar.gz | |
| for i in $(seq 1 8); do | |
| curl -fL --retry 5 --retry-all-errors --retry-delay 10 "$url" -o elan.tar.gz && break | |
| echo "elan download attempt $i failed (transient 504?); retrying in 20s"; sleep 20 | |
| done | |
| tar xzf elan.tar.gz | |
| ./elan-init -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| export PATH="$HOME/.elan/bin:$PATH" | |
| for i in $(seq 1 6); do | |
| elan toolchain install "$(cat lean-toolchain)" && break | |
| echo "toolchain install attempt $i failed; retrying in 20s"; sleep 20 | |
| done | |
| - name: Build Lean proofs (argmin + Freivalds bound) | |
| working-directory: lean | |
| run: | | |
| set -euo pipefail | |
| lake exe cache get | |
| lake build |