From 0680e5938218c6bac60592812b449e7a604caab7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Jul 2026 21:26:42 +0200 Subject: [PATCH 1/2] docs: gate README claims against live evidence (claim-verification) Audited this repo's load-bearing claims after the badge fix (#36/#38) and the Gappa/Flocq/Coq-Interval toolchain feature (#37/#41): - Found the footer tagline still carried the retired flat-verification overclaim ("formally verified WebAssembly toolchain for safety-critical systems") -- the same overclaim #36 fixed in the badge, just relocated, and factually wrong on top (this repo has nothing to do with WebAssembly). Replaced with an accurate description. - Toolchain Contents table and Examples section were stale after #41 -- didn't mention Flocq/Coq-Interval/Coquelicot/Gappa or examples/gappa_proof. Updated both. - Added claims.yaml + tools/claim_check.py (the claim-verification skill's reference implementation): each load-bearing README claim is bound to a predicate re-derived from the actual source (file-exists, count-min, count-max on the retired overclaims) rather than trusted as prose. - Wired `claim-check` into CI as its own job: a stale or overclaiming README now fails the build the same way an un-kernel-checked proof fails a rocq_proof_test. All 5 claims pass against current main: `python3 tools/claim_check.py claims.yaml` -> 5/5. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey --- .github/workflows/ci.yml | 17 ++++++ README.md | 14 ++++- claims.yaml | 69 +++++++++++++++++++++++ tools/claim_check.py | 116 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 215 insertions(+), 1 deletion(-) create mode 100644 claims.yaml create mode 100644 tools/claim_check.py diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b5687bb..2ef2d2c 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 --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() From 46ae3bac48392dca078156dbe3dfa448651bc1cc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 21 Jul 2026 21:28:14 +0200 Subject: [PATCH 2/2] fix(ci): use --break-system-packages for pip install in claim-check job The self-hosted smithy runners are Debian/python3.12 with PEP 668's externally-managed-environment guard, which refuses a bare pip install. Co-Authored-By: Claude Sonnet 5 Claude-Session: https://claude.ai/code/session_011MptgyfLZuHYCbfpq1zDey --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2ef2d2c..c0b813a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -188,7 +188,7 @@ jobs: uses: actions/checkout@v4 - name: Install PyYAML - run: pip install --quiet pyyaml + run: pip install --break-system-packages --quiet pyyaml - name: Check doc claims against evidence run: python3 tools/claim_check.py claims.yaml