chore: harden release quality

Author: AbdelStark

.github/workflows/ci.yml

@@ -3,8 +3,8 @@
 # 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).
+# proving substrate. `bash ci/check-local.sh full` mirrors the non-external
+# merge gates for local validation.
 name: CI
 
 on:
@@ -111,17 +111,26 @@ jobs:
       # Internal cross-reference check across the docs corpus (file + anchor).
       - name: Internal link check (docs/)
         run: python3 ci/check-links.py
+      # Public prose convention from AGENTS.md: no em dashes in README/docs/site.
+      - name: Prose style (no em dashes)
+        run: python3 ci/check-prose-style.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).
+      # Export pipeline 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
+        run: bash ci/check-python-style.sh
+      # Release helper self-checks, including SemVer ordering and changelog parsing.
+      - name: Release tooling
+        run: python3 ci/test-release-tools.py
+      # Shebang-bearing helper scripts must be directly executable.
+      - name: Script modes
+        run: bash ci/check-script-modes.sh
 
   license:
     name: License / SPDX
@@ -146,21 +155,20 @@ jobs:
         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.
+      # The runner evaluates every registered verifier mutation campaign and
+      # exits non-zero on a survivor or a score below target.
       - run: cargo run -p pwm-testkit --bin mutation_runner --locked
 
   lean:
-    name: Lean soundness proofs (D-805)
+    name: Lean soundness proofs
     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.
+      # 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: |

.github/workflows/release.yml

@@ -1,11 +1,11 @@
 # SPDX-License-Identifier: Apache-2.0
 #
-# Release automation (docs/spec/09-release-and-versioning.md, RFC-0016).
+# Release automation for the workspace policy in CHANGELOG.md and CONTRIBUTING.md.
 #
 # Triggered by pushing a semver tag `vX.Y.Z`. Validates the tag against the
-# semver policy and the changelog (INV-REL-10), runs the license/SPDX gate and
-# the quality bar, packages the publishable crates, and publishes a GitHub
-# Release with the changelog section as notes and the `.crate` files attached.
+# semver policy and the changelog, runs the license/SPDX gate and the quality
+# bar, packages the publishable crates, and publishes a GitHub Release with the
+# changelog section as notes and the `.crate` files attached.
 #
 # Publishing to a registry is intentionally out of scope (deferred); this
 # produces the packaged artifacts but does not run `cargo publish`. A manual
@@ -15,8 +15,9 @@ name: Release
 on:
   push:
     tags:
-      - "v[0-9]+.[0-9]+.[0-9]+"
-      - "v[0-9]+.[0-9]+.[0-9]+-*"
+      # GitHub tag filters are globs, not regex. Match broadly here and enforce
+      # strict SemVer before packaging or publishing.
+      - "v*.*.*"
   workflow_dispatch:
     inputs:
       version:
@@ -48,7 +49,7 @@ jobs:
       - name: Tag matches semver policy
         run: |
           VERSION="${{ steps.version.outputs.version }}"
-          if ! echo "$VERSION" | grep -Eq '^(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)(-[0-9A-Za-z.-]+)?(\+[0-9A-Za-z.-]+)?$'; then
+          if ! echo "$VERSION" | grep -Eq '^(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)\.(0|[1-9][0-9]*)(-((0|[1-9][0-9]*|[0-9]*[A-Za-z-][0-9A-Za-z-]*)(\.(0|[1-9][0-9]*|[0-9]*[A-Za-z-][0-9A-Za-z-]*))*))?(\+([0-9A-Za-z-]+(\.[0-9A-Za-z-]+)*))?$'; then
             echo "::error::tag version '$VERSION' is not semver-conformant"
             exit 1
           fi
@@ -62,30 +63,85 @@ jobs:
             exit 1
           fi
 
-      - name: Changelog completeness (INV-REL-10)
+      - name: Changelog completeness
         run: python3 ci/check-changelog.py "${{ steps.version.outputs.version }}"
+      - name: Release tooling self-check
+        run: python3 ci/test-release-tools.py
+      - name: Script modes
+        run: bash ci/check-script-modes.sh
 
       - uses: dtolnay/rust-toolchain@3c5f7ea28cd621ae0bf5283f0e981fb97b8a7af9 # pinned (no semver tags; SHA of master @ stable)
         with:
           toolchain: "stable"
           components: rustfmt, clippy
+      - name: Install MSRV toolchain
+        run: rustup toolchain install 1.85 --profile minimal
       - uses: Swatinem/rust-cache@v2
 
       # License gate runs in the release path (acceptance criterion).
       - name: License / SPDX gate
         run: bash ci/check-spdx.sh
-      - name: cargo-deny (licenses)
+      - name: cargo-deny (licenses + advisories + bans + sources)
         uses: EmbarkStudios/cargo-deny-action@v2
         with:
-          command: check licenses
+          command: check
 
-      # Quality bar — the release must pass the same gates as a merge.
+      # Quality bar: the release must pass the same core gates as a merge.
       - name: Format
         run: cargo fmt --all -- --check
+      - name: Prose style
+        run: python3 ci/check-prose-style.py
       - name: Lint
         run: cargo clippy --all-targets --all-features --locked -- -D warnings
       - name: Tests
         run: cargo test --workspace --all-features --locked
+      - name: MSRV (Rust 1.85)
+        run: cargo +1.85 build --workspace --locked
+      - name: Full-dims predictor (ignored, release)
+        run: cargo test --workspace --all-features --release --locked -- --ignored
+      - name: no_std verifier build
+        run: |
+          cargo build -p pwm-verifier --no-default-features --locked
+          cargo build -p pwm-core --no-default-features --locked
+      - name: Rustdoc
+        run: cargo doc --workspace --no-deps --locked
+        env:
+          RUSTDOCFLAGS: "-D warnings"
+      - name: Internal link check
+        run: python3 ci/check-links.py
+      - name: Export canonical parity
+        run: python3 crates/pwm-export/python/tests/test_canonical_parity.py
+      - name: Export pipeline
+        run: |
+          python3 -m pip install --quiet numpy
+          python3 crates/pwm-export/python/tests/test_export_pipeline.py
+      - name: Python style
+        run: bash ci/check-python-style.sh
+      - name: Constraint mutation
+        run: cargo run -p pwm-testkit --bin mutation_runner --locked
+      - 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: Lean soundness proofs
+        working-directory: lean
+        run: |
+          set -euo pipefail
+          lake exe cache get
+          lake build
 
       # Package the publishable crates (pwm-testkit is publish=false). The whole
       # workspace is packaged together so inter-crate deps resolve among the set.

AGENTS.md

@@ -71,6 +71,8 @@ Without Docker:
 cargo run -p pwm-testkit --bin pwm --release -- prove-predictor          # synthetic
 cargo run -p pwm-testkit --bin pwm --release -- prove-predictor <bundle> # real weights
 cargo test --workspace                                                   # accept + reject suites
+bash ci/check-local.sh quick                                             # fast local quality loop
+bash ci/check-local.sh full                                              # local merge-gate mirror
 ```
 
 The `pwm` CLI prints a five-stage pipeline (LOAD, INFER, COMMIT, VERIFY, TAMPER); it
@@ -84,8 +86,12 @@ honors `NO_COLOR` and `--json`.
   doc-comments may keep them per repo style.
 - Commits and PRs carry no tool attribution and no `Co-Authored-By` lines.
 - One logical change per branch and PR. Branch from `main`, open a PR, keep CI
-  green (fmt, clippy `-D warnings`, the full test suite, SPDX headers, link check,
-  the no-em-dash check). Confirm before any destructive git operation.
+  green (fmt, clippy `-D warnings`, the full test suite, release-mode ignored
+  predictor test, no_std builds, rustdoc, link check, Python parity/export/style,
+  script modes, mutation, Lean proofs, cargo-deny, SPDX headers, prose-style check). Confirm
+  before any destructive git operation.
+- Prefer `bash ci/check-local.sh full` before claiming a broad quality or release
+  pass. Use `quick` only for the inner loop.
 - Keep complexity and file size as low as the task allows. Small, focused files.
 
 ## Pointers

CHANGELOG.md

@@ -13,11 +13,13 @@ entry.
 
 ## [Unreleased]
 
+## [0.1.0] - 2026-06-11
+
 ### Security
 
 - **Per-buffer range enforcement on the exact-recompute path** (#180): the
-  verifier now rejects — with the typed `VerifyError::BufferRange` /
-  `VerifyError::InputRange` — any prover-supplied value outside the single-M31
+  verifier now rejects, with the typed `VerifyError::BufferRange` /
+  `VerifyError::InputRange`, any prover-supplied value outside the single-M31
   envelope `[-P_HALF, P_HALF]` before computing on it: every exactly-recomputed
   op's claimed output (flat trace and block paths), every seeded block input
   buffer, and every proof-carried quantization parameter (`zero_point`,
@@ -26,7 +28,7 @@ entry.
   in `i128` with explicit envelope bound checks (mirroring
   `fixed_point::finish`), and `ActivationTable::eval` computes its index in
   `i128`, so an adversarial buffer or table can no longer wrap `i64` arithmetic
-  into a fail-closed **panic** (under `overflow-checks`) — it is rejected
+  into a fail-closed **panic** (under `overflow-checks`); it is rejected
   cleanly. Narrows verifier acceptance; no honest proof regresses (full suite
   plus the real-dims predictor test stay green).
 
@@ -39,17 +41,27 @@ entry.
   `CommitmentMismatch(Model)` unless the proven weights reproduce the export's
   commitment bit-for-bit. The artifact alone now certifies which weight set was
   proven (bundle ⇄ export bound; checkpoint ⇄ export remains trusted
-  preprocessing — documented in README and specs §13). The Python↔Rust
+  preprocessing, documented in README and specs §13). The Python↔Rust
   canonical-encoding parity gate is now two-way: the multi-leaf `weights_root`
   vector and the full predictor weight scheme are pinned on both sides.
 
 ### Changed
 
-- Polished the explainer site against the Impeccable design guidelines: removed
-  the AI-default scaffolding (per-section uppercase eyebrow kickers, side-stripe
+- Added reproducible public-prose and Python-style gates: `ci/check-prose-style.py`
+  is now wired into CI and release validation, current first-party docs pass it,
+  and `ci/check-python-style.sh` runs the pinned ruff check through `uvx`, `uv`,
+  `pipx`, or a temporary venv so local contributors can reproduce CI without
+  relying on one preinstalled runner.
+- Hardened tagged releases to run the same core quality bar before packaging:
+  full cargo-deny, fmt, clippy, workspace tests, release-mode ignored predictor,
+  no_std builds, rustdoc, link/prose checks, export parity/pipeline, Python
+  style, the mutation campaign, and Lean soundness proofs.
+
+- Polished the explainer site against the project design guidelines: removed
+  the generic scaffolding (per-section uppercase eyebrow kickers, side-stripe
   accent borders, hero metric boxes, decorative card chips), swapped the body
   face from Inter to Archivo, and fixed real defects found while verifying in a
-  browser — grid blowouts that caused horizontal page scroll (`.start`, `.arch`),
+  browser: grid blowouts that caused horizontal page scroll (`.start`, `.arch`),
   a tamper switch that could not be toggled from the keyboard, the closed mobile
   menu remaining in the tab order, a focus ring that reshaped pill buttons, and
   missing arrow-key navigation on the tier tabs.
@@ -105,8 +117,8 @@ entry.
   small-dims predictor accept tests now pin the exact integer output vector
   (not just `is_ok` + float tolerance), locking the quantized semantics
   end-to-end; and the soundness mutation campaign gained a
-  `range_check.modp_predictor` mutant — the mod-`p` accumulator-aliasing
-  forgery on a `BatchedLinear` accumulator — so the predictor/block path's
+  `range_check.modp_predictor` mutant: the mod-`p` accumulator-aliasing
+  forgery on a `BatchedLinear` accumulator, so the predictor/block path's
   Freivalds range guard is merge-gated like the flat demo path's.
 - The soundness mutation campaign registered no mutant for the `tensor_memory`
   (op-to-op wiring) component, so its merge gate passed vacuously; it now exercises
@@ -172,4 +184,5 @@ entry.
   `overflow-checks` is enabled in the release profile so any integer wrap on the
   recompute path traps instead of silently producing a wrong-but-matching value.
 
-[Unreleased]: https://github.com/AbdelStark/ProvableWorldModel/commits/main
+[Unreleased]: https://github.com/AbdelStark/ProvableWorldModel/compare/v0.1.0...main
+[0.1.0]: https://github.com/AbdelStark/ProvableWorldModel/releases/tag/v0.1.0

CONTRIBUTING.md

@@ -16,6 +16,11 @@ under [docs/legacy-stark/](docs/legacy-stark/) and is no longer normative.
 3. Branch from `main`. Reference the issue in the pull request. Keep the diff
    focused on the issue's scope.
 
+Run `bash ci/check-local.sh quick` while iterating. Before opening or merging a
+pull request, run `bash ci/check-local.sh full`; it mirrors the non-external CI
+gates and fails on the first broken contract. Before tagging, run
+`bash ci/check-local.sh release <version>` after preparing the changelog.
+
 ## Changing the specification
 
 Load-bearing decisions are recorded in [specs.md](specs.md), not in code review. A
@@ -35,9 +40,11 @@ an approximation, a planner rule, or serialization mints a new `relation_id`; se
 - The verifier must not depend on the export pipeline or on PyTorch.
 - Public items carry doc comments stating preconditions, postconditions, and
   errors. Source files carry an `SPDX-License-Identifier: Apache-2.0` header.
-- Python (export pipeline): typed, formatted, and linted per the project
-  configuration; the fixed-point reference must match the Rust reference
-  bit-for-bit.
+- Public prose (README, specs, demo docs, changelog, website copy) uses no em
+  dashes; run `python3 ci/check-prose-style.py` before opening a pull request.
+- Python (export pipeline): keep code type-annotated and pass the pinned Ruff
+  gate with `bash ci/check-python-style.sh`.
+  The fixed-point reference must match the Rust reference bit-for-bit.
 
 ## Testing
 
@@ -49,10 +56,17 @@ primitives ship with committed golden vectors and stated domain bounds.
 ## Continuous integration gates
 
 A pull request must pass: formatting, `clippy -D warnings`, the unit and
-integration test suites, golden-vector parity (Python integer reference vs Rust
-integer reference), the `no_std` float-free verifier build, the documentation
-build, and the SPDX/license check. See [specs.md](specs.md#15-testing-strategy)
-and [backlog.md](backlog.md) (milestone M7).
+integration test suites, the MSRV build, golden-vector parity (Python integer
+reference vs Rust integer reference), the `no_std` float-free verifier build,
+the documentation build, the release-mode full-dims predictor test, the mutation
+gate, the Lean proofs, the Python style check, the prose-style check, the script
+mode check, and the SPDX/license/supply-chain check. See
+[specs.md](specs.md#15-testing-strategy) and the hardening ledger in
+[backlog.md](backlog.md).
+
+The local entry point is `bash ci/check-local.sh full`. The hosted Real E2E
+workflow remains separate because it downloads external Hugging Face assets and
+builds the PyTorch export image.
 
 ## Security
 

Cargo.toml

@@ -3,10 +3,10 @@
 # Workspace manifest for ProvableWorldModel.
 #
 # Pins the shared package metadata (MSRV, edition, license), the workspace-wide
-# lint configuration, and the build profiles. Post-pivot (CommitLLM commit-and-
-# audit backend) the system is five first-party crates under `crates/`:
-# pwm-core, pwm-export, pwm-prover, pwm-verifier, pwm-testkit. The STARK AIR /
-# circuits crates and the vendored Stwo prover were removed; see specs.md.
+# lint configuration, and the build profiles. Post-pivot, the CommitLLM
+# commit-and-audit backend is five first-party crates under `crates/`: pwm-core,
+# pwm-export, pwm-prover, pwm-verifier, pwm-testkit. The STARK AIR / circuits
+# crates and the vendored Stwo prover were removed; see specs.md.
 
 [workspace]
 resolver = "2"
@@ -21,6 +21,7 @@ edition = "2021"
 rust-version = "1.85"
 license = "Apache-2.0"
 repository = "https://github.com/AbdelStark/ProvableWorldModel"
+readme = "crates/README.md"
 authors = ["ProvableWorldModel contributors"]
 
 # Centralized dependency versions. First-party crates carry a `version` (not just
@@ -32,15 +33,15 @@ pwm-core = { path = "crates/pwm-core", version = "0.1.0" }
 pwm-export = { path = "crates/pwm-export", version = "0.1.0" }
 pwm-prover = { path = "crates/pwm-prover", version = "0.1.0" }
 pwm-verifier = { path = "crates/pwm-verifier", version = "0.1.0" }
-# Blake2s commitment / digest / transcript primitive (specs.md §4, §6). no_std;
-# the only crypto dependency in the pwm-core trust root (INV-ARCH-01).
+# Blake2s commitment / digest / transcript primitive. no_std; the only crypto
+# dependency in the pwm-core trust root.
 blake2 = { version = "0.10", default-features = false }
 # Test-only third-party dependencies (used by pwm-testkit and pwm-core dev-deps).
 serde = { version = "1", features = ["derive"] }
 serde_json = "1"
 
 # Shared lints applied to every first-party crate via `[lints] workspace = true`.
-# The CI clippy/fmt/header gates (#73) build on this baseline.
+# The CI clippy/fmt/header gates build on this baseline.
 [workspace.lints.rust]
 unsafe_code = "warn"
 unreachable_pub = "warn"
@@ -63,8 +64,8 @@ explicit_iter_loop = "warn"
 unreadable_literal = "warn"
 semicolon_if_nothing_returned = "warn"
 
-# Build profiles. The performance-budget profile is tuned under the perf gate
-# (#75); these are conservative defaults appropriate for a prover binary.
+# Build profiles. These are conservative defaults appropriate for a prover
+# binary.
 [profile.release]
 opt-level = 3
 lto = "thin"