docs: gate README claims against live evidence (claim-verification)

.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

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).
 
 <div align="center">
 
-<sub>Part of <a href="https://github.com/pulseengine">PulseEngine</a> &mdash; formally verified WebAssembly toolchain for safety-critical systems</sub>
+<sub>Part of <a href="https://github.com/pulseengine">PulseEngine</a> &mdash; Bazel rules powering the Rocq theorem-proving toolchain</sub>
 
 </div>

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

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()