diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b5687bb..c0b813a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -175,3 +175,20 @@ jobs: curl -Lo buildifier https://github.com/bazelbuild/buildtools/releases/download/v7.3.1/buildifier-linux-amd64 chmod +x buildifier ./buildifier --mode=check -r . || echo "Some files need formatting" + + # Doc-claim honesty gate (see claims.yaml / pulseengine claim-verification skill). + # A stale/overclaiming README fails this job the same way an un-kernel-checked + # proof fails a rocq_proof_test -- the claim IS the artifact being gated. + claim-check: + name: Claim Check + runs-on: [self-hosted, linux, x64, light] + + steps: + - name: Checkout repository + uses: actions/checkout@v4 + + - name: Install PyYAML + run: pip install --break-system-packages --quiet pyyaml + + - name: Check doc claims against evidence + run: python3 tools/claim_check.py claims.yaml diff --git a/README.md b/README.md index dc79eae..6c89a29 100644 --- a/README.md +++ b/README.md @@ -173,6 +173,11 @@ Test rule that verifies proofs compile successfully. | coqutil | Utility library | | Hammer | Automated proof tactics | | smpl | Simplification tactics | +| Flocq | Floating-point formalization library | +| Coq-Interval | Interval arithmetic / approximation-error bounds | +| Coquelicot | Real analysis library (Coq-Interval's dependency) | +| Gappa | Rounding-error prover binary, kernel-checked via `gappa_proof` (see `rocq:defs.bzl`) | +| gappalib-coq | Gappa's Rocq support library (built from source against Flocq) | | rocq-of-rust | Rust-to-Rocq translator (pinned version) | ## Supported Platforms @@ -208,6 +213,13 @@ bazel build //examples/rust_to_rocq:advanced_verified bazel test //examples/rust_to_rocq:point_proofs_test ``` +See `examples/gappa_proof/` for a machine-checked floating-point error-bound +proof (Gappa + Flocq), kernel-checked by Rocq: + +```bash +bazel test //examples/gappa_proof:rounding_bound_test +``` + ## License Apache-2.0 — see [LICENSE](LICENSE). @@ -216,6 +228,6 @@ Apache-2.0 — see [LICENSE](LICENSE).
-Part of PulseEngine — formally verified WebAssembly toolchain for safety-critical systems +Part of PulseEngine — Bazel rules powering the Rocq theorem-proving toolchain
diff --git a/claims.yaml b/claims.yaml new file mode 100644 index 0000000..ecf98f4 --- /dev/null +++ b/claims.yaml @@ -0,0 +1,69 @@ +# claims.yaml -- gates rules_rocq_rust's load-bearing README/doc claims against +# live evidence, per the PulseEngine claim-verification skill. Run: +# python3 tools/claim_check.py claims.yaml +# from the repo root. Drift between a claim and the actual source fails this check. + +claims: + # The badge fix (#36): replaces the flat "Formally Verified" overclaim with a + # technique-named "Rocq" badge. Gates that the old claim never reappears. + - id: README-BADGE + doc: README.md + text: "![Rocq](https://img.shields.io/badge/Rocq-9.0" + evidence: + - kind: verbatim + text: "![Rocq](https://img.shields.io/badge/Rocq-9.0" + - kind: count-max + pattern: 'Formally[_ ]Verified' + glob: ['README.md'] + max: 0 + + # The footer tagline was the same overclaim relocated (plus factually wrong -- + # this repo has nothing to do with WebAssembly). Gates the honest replacement + # and that the retired claim doesn't reappear. + - id: README-FOOTER + doc: README.md + text: "Bazel rules powering the Rocq theorem-proving toolchain" + evidence: + - kind: verbatim + text: "Bazel rules powering the Rocq theorem-proving toolchain" + - kind: count-max + pattern: 'formally verified WebAssembly' + glob: ['README.md'] + max: 0 + + # #37/FEAT-001: the gappa_proof macro's core safety property (rivet CC-002) + # -- Gappa's CLI output is never trusted directly, it's always kernel-checked + # by compiling the emitted proof term with rocq_library. Structural evidence: + # the macro body must actually call rocq_library (not just claim to in prose), + # and the from-source support library it kernel-checks against must exist. + - id: GAPPA-KERNEL-CHECK + doc: rocq/defs.bzl + text: "certificate is never trusted on its own" + evidence: + - kind: file-exists + path: rocq/private/gappalib_repository.bzl + - kind: count-min + pattern: 'rocq_library\(' + glob: ['rocq/defs.bzl'] + min: 1 + + # Toolchain Contents table must list what the toolchain actually wires in + # (rocq/extensions.bzl is the source of truth for what's fetched). + - id: TOOLCHAIN-CONTENTS-FLOCQ + doc: README.md + text: "| Flocq | Floating-point formalization library |" + evidence: + - kind: count-min + pattern: 'rocq_flocq' + glob: ['rocq/extensions.bzl'] + min: 1 + + # The Examples section's gappa_proof pointer must resolve to a real target. + - id: EXAMPLES-GAPPA-PROOF + doc: README.md + text: "bazel test //examples/gappa_proof:rounding_bound_test" + evidence: + - kind: file-exists + path: examples/gappa_proof/BUILD.bazel + - kind: file-exists + path: examples/gappa_proof/rounding_bound.gappa diff --git a/tools/claim_check.py b/tools/claim_check.py new file mode 100644 index 0000000..0d4ad5d --- /dev/null +++ b/tools/claim_check.py @@ -0,0 +1,116 @@ +#!/usr/bin/env python3 +"""claim-check — gate a repo's documentation claims against live evidence. + +Reference implementation for the `claim-verification` skill. This repo drops a +`claims.yaml` at the root; CI runs this; drift between a claim and the actual +source fails the build. Truth-over-time becomes a property of the gate, not +the author. + +Usage: claim_check.py [claims.yaml] (default: ./claims.yaml) +Exit: 0 = all claims hold · 1 = one or more drifted +""" +import sys +import re +import glob +import pathlib + +try: + import yaml +except ImportError: + sys.exit("claim-check: needs PyYAML (pip install pyyaml)") + + +def _count(pattern, globs, root): + rx = re.compile(pattern) + globs = [globs] if isinstance(globs, str) else globs + total = 0 + matched_any = False + for g in globs: + for f in glob.glob(str(root / g), recursive=True): + p = pathlib.Path(f) + if p.is_file(): + matched_any = True + total += len(rx.findall(p.read_text(errors="ignore"))) + return total, matched_any + + +def check_claim(c, root): + fails = [] + doc_path = root / c["doc"] + doc = doc_path.read_text(errors="ignore") if doc_path.exists() else "" + if not doc_path.exists(): + return [f'doc not found: {c["doc"]}'] + + text = c.get("text") + if text and text not in doc: + fails.append(f'claim text not found verbatim in {c["doc"]}: "{text}"') + + for ev in c.get("evidence", []): + kind = ev.get("kind") + if kind == "verbatim": + s = ev.get("text", text) + if s and s not in doc: + fails.append(f'verbatim string absent from {c["doc"]}: "{s}"') + elif kind == "file-exists": + if not (root / ev["path"]).exists(): + fails.append(f'evidence file missing: {ev["path"]}') + elif kind == "count-max": + n, matched = _count(ev["pattern"], ev["glob"], root) + if not matched: + fails.append(f'predicate matched NO files (measures nothing): glob {ev["glob"]}') + elif n > ev["max"]: + fails.append( + f'trusted base grew: {n} > recorded max {ev["max"]} ' + f'[/{ev["pattern"]}/] — update the claim, not the number' + ) + elif kind == "count-min": + n, matched = _count(ev["pattern"], ev["glob"], root) + if not matched: + fails.append(f'predicate matched NO files (measures nothing): glob {ev["glob"]}') + elif n < ev["min"]: + fails.append( + f'claim evidence absent: {n} < required min {ev["min"]} ' + f'[/{ev["pattern"]}/] — the doc asserts it; the source no longer carries it' + ) + elif kind == "no-new": + n, matched = _count(ev["pattern"], ev["glob"], root) + if not matched: + fails.append(f'predicate matched NO files (measures nothing): glob {ev["glob"]}') + elif n > ev.get("recorded", 0): + fails.append( + f'new unproven obligations: {n} > recorded {ev.get("recorded", 0)} ' + f'[/{ev["pattern"]}/]' + ) + else: + fails.append(f'unknown evidence kind: {kind!r}') + return fails + + +def main(): + path = pathlib.Path(sys.argv[1] if len(sys.argv) > 1 else "claims.yaml") + if not path.exists(): + sys.exit(f"claim-check: {path} not found") + root = path.parent + data = yaml.safe_load(path.read_text()) or {} + claims = data.get("claims", []) + if not claims: + print("claim-check: no claims declared — nothing to gate.") + return + + bad = 0 + for c in claims: + fails = check_claim(c, root) + if fails: + bad += 1 + print(f"✗ {c['id']}") + for f in fails: + print(f" {f}") + else: + print(f"✓ {c['id']}") + + print(f"\n{len(claims) - bad}/{len(claims)} claims hold.") + sys.exit(1 if bad else 0) + + +if __name__ == "__main__": + main()