Skip to content

Pivot: Circle-STARK → CommitLLM commit-and-audit (LeWorldModel) #59

Pivot: Circle-STARK → CommitLLM commit-and-audit (LeWorldModel)

Pivot: Circle-STARK → CommitLLM commit-and-audit (LeWorldModel) #59

Workflow file for this run

# 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@master
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@master
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@master
with:
toolchain: "stable"
- uses: Swatinem/rust-cache@v2
- run: cargo test --workspace --all-features --locked
no-std:
name: no_std verifier build
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@master
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@master
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
license:
name: License / SPDX
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: SPDX header check
run: bash ci/check-spdx.sh
- name: cargo-deny (licenses)
uses: EmbarkStudios/cargo-deny-action@v2
with:
command: check licenses
mutation:
name: Constraint mutation (scoped)
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@master
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.
# lean-action installs elan from lean/lean-toolchain and fetches the prebuilt
# Mathlib cache (`lake exe cache get`) before `lake build` — no Mathlib rebuild.
- uses: leanprover/lean-action@v1
with:
lake-package-directory: "lean"