name: Quality Gate
on:
push:
branches: [main, master]
pull_request:
branches: [main, master]
workflow_dispatch:
concurrency:
group: quality-gate-${{ github.event.pull_request.number || github.ref }}
cancel-in-progress: true
env:
RUST_MIN_STACK: "8388608"
CARGO_TERM_COLOR: always
jobs:
score:
name: pmat score
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
with:
fetch-depth: 0
- name: Checkout provable-contracts (path dep)
uses: actions/checkout@v7
with:
repository: paiml/provable-contracts
path: provable-contracts
- name: Symlink provable-contracts for Cargo path deps
run: ln -sf "$GITHUB_WORKSPACE/provable-contracts" "$GITHUB_WORKSPACE/../provable-contracts"
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
with:
cache-on-failure: true
- name: Install pmat
run: cargo install --path . --locked
- name: Run unified quality gate
run: pmat score --gate 60 --format json -o score.json
- name: Upload score artifact
uses: actions/upload-artifact@v7
with:
name: pmat-score
path: score.json
if: always()
- name: Post score summary
if: always()
run: |
# `composite` is null when a dimension could not be measured, and a
# sub-score is null when THAT dimension could not be measured — an
# unmeasured thing is no longer reported as 0.0, because "measured,
# terrible" and "never ran" are not the same claim (paiml/aprender
# #2463). This step still formatted both with `:.1f` and died with
# `TypeError: unsupported format string passed to NoneType.__format__`,
# so the producer changed and this consumer did not — the one-rule-two-
# implementations defect, in the reporting layer this time.
if [ -f score.json ]; then
python3 - <<'PY' >> "$GITHUB_STEP_SUMMARY"
import json
d = json.load(open("score.json"))
def num(v):
"""A number, or why there isn't one. Never a fabricated 0.0."""
if isinstance(v, (int, float)):
return f"{v:.1f}"
if isinstance(v, dict): # Result-shaped: {"Ok": x} / {"Err": "reason"}
if "Ok" in v:
return num(v["Ok"])
return f"not measured — {v.get('Err', 'reason unrecorded')}"
return "not measured"
gated = d.get("gated_by") or []
grade = d.get("grade", "?")
composite = d.get("composite")
headline = (
f"{composite:.1f}/100"
if isinstance(composite, (int, float))
else "not measured" # never "0.0/100", which reads as a verdict
)
print(f"### PMAT Score: {headline} ({grade})")
print()
if gated:
print(f"**Gated by:** {', '.join(gated)} — a measured zero gates the verdict "
f"rather than averaging into it, so one red dimension cannot masquerade "
f"as a uniformly bad project.")
print()
for nm in d.get("not_measured") or []:
name = nm.get("dimension", nm) if isinstance(nm, dict) else nm
why = nm.get("reason", "") if isinstance(nm, dict) else ""
print(f"- **not measured:** {name}{f' — {why}' if why else ''}")
if d.get("not_measured"):
print()
print("| Sub-Score | Value |")
print("|-----------|-------|")
for k, v in (d.get("sub_scores") or {}).items():
print(f"| {k} | {num(v)} |")
PY
fi
provable-ladder:
name: provable ladder
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v7
with:
fetch-depth: 0
- name: L5 — build Lean proofs (lake build)
uses: leanprover/lean-action@v1
with:
lake-package-directory: contracts/lean
build: true
use-mathlib-cache: false
- name: L5 — assert zero proof holes (no sorry / admit)
run: |
if grep -rInE '\bsorry\b|\badmit\b' contracts/lean/Theorems/; then
echo "::error::Lean proofs contain sorry/admit — L5 not proven"
exit 1
fi
echo "Lean proofs are hole-free (0 sorry, 0 admit)."
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
with:
cache-on-failure: true
- name: Checkout provable-contracts (path dep)
uses: actions/checkout@v7
with:
repository: paiml/provable-contracts
path: provable-contracts
- name: Symlink provable-contracts for Cargo path deps
run: ln -sf "$GITHUB_WORKSPACE/provable-contracts" "$GITHUB_WORKSPACE/../provable-contracts"
- name: Install pmat
run: cargo install --path . --locked
- name: L1 — binding registry AllImplemented (build.rs, already enforced by install)
run: echo "contracts/binding.yaml AllImplemented enforced at build time (build.rs)."
- name: Ladder gate — pmat comply
continue-on-error: true
run: pmat comply check --failures-only