docs: claim-verification pass — fix v0.1.0 status drift (#97) + gate it

.github/workflows/ci.yml

@@ -166,6 +166,24 @@ jobs:
       - name: rivet validate
         run: rivet validate
 
+  # A README is a claim about the system — the same species as a requirement,
+  # gated the same way. `claim-check` re-derives every load-bearing doc claim
+  # (version, admit-free proof count, published-crate count, WrapAdd.v, the
+  # scoped-soundness wording) from live source and fails the build on drift —
+  # so the status section can't silently rot ~40 versions again (issue #97).
+  claim-check:
+    name: Doc claims (claim-check)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - name: Install PyYAML
+        run: pip install pyyaml
+      - name: claim-check claims.yaml
+        run: python3 tools/claim-check.py claims.yaml
+
   spar-parse:
     name: AADL model (spar parse)
     runs-on: ubuntu-latest

README.md

@@ -60,24 +60,32 @@ deductive-proof and bounded-model-checking layers do not staff.
 
 ## status
 
-**v0.1.0 shipped 2026-05-27** —
-[release page](https://github.com/pulseengine/scry/releases/tag/v0.1.0)
-with cosign-signed `scry-0.1.0-wasm32-wasip2.wasm` + per-crate
-CycloneDX SBOMs + SHA256SUMS + SLSA v1 provenance. The full
-PulseEngine Wasm-component toolchain runs end-to-end on scry's own
-build (the dogfood gate for [[DD-008]]). v0.1.0 ships the
-**structural scaffold**: no real abstract-interpretation logic yet.
-
-The implementation work — interval-domain fixpoint on a parsed Wasm
-module, host wasmtime test harness, Verus + Rocq proof targets,
-region-memory domain — lands progressively from v0.2. Follow the
-[release plan](#release-plan) below; each numbered version closes a
-specific verified-evidence increment.
-
-`rivet validate` here is PASS with 0 warnings; 64 artifacts span 11
-types across `common + dev + research + research-ext + safety-case`.
-Everything in this README that isn't tagged "v0.1.0" is still a
-*requirements artifact* awaiting the labelled version.
+<!-- claim id=version: "scry-sai-core" crates.io max_version == workspace version -->
+<!-- claim id=crates: publish.rs lists 12 scry-sai-* crates -->
+<!-- claim id=admit-free: 0 Admitted/admit/Axiom across proofs/rocq/*.v -->
+**v3.2.4 shipped** — the full v0.1 → v3.2 arc is done; scry is a working **sound
+abstract interpreter**, not a scaffold. Shipped and on crates.io: **12 pure
+`scry-sai-*` crates** (10 abstract domains — interval, region-memory, call-graph
++ reachability, octagon, pentagon, known-bits/congruence, IEEE-754 float,
+Component-Model handle-state, linear-memory segmentation, convex polyhedra —
+plus the analyzer core and the viz) driving `analyze()` over parsed Wasm; a host
+wasmtime harness; runtime-trap classification (PROVEN-SAFE vs POTENTIAL-TRAP);
+ranked remediation guidance + a structured `guidance.json`; and a GitHub Pages
+[verification dashboard](https://pulseengine.github.io/scry).
+
+Soundness evidence is **scoped, not flattened** (mirrors the dashboard's Scope &
+limitations block):
+
+- **Mechanized (Rocq, admit-free):** 19 `.v` proofs, **0 `Admitted` / `admit` /
+  `Axiom`** — the domain lattices + core transfers, incl. `i32.add` vs the
+  OFFICIAL two's-complement wrapping semantics (`WrapAdd.v`).
+- **γ-sweep-validated (tested, NOT mechanized):** the harder transfer
+  algorithms — float round-to-nearest, known-bits at w=32/64 (issue #105), and
+  the polyhedra Fourier–Motzkin entailment.
+
+Releases are cosign-signed with CycloneDX SBOMs + SHA256SUMS + SLSA v1
+provenance; `rivet validate` is PASS. The roadmap below is **historical through
+v3.2** (shipped); only v3.3+ items are still plans.
 
 ## is this for you?
 

claims.yaml

@@ -0,0 +1,86 @@
+# claims.yaml — scry's load-bearing README/doc claims, gated against live evidence.
+#
+# A README is a claim about the system, the same species as a requirement pointing
+# the other way — and it rots for the same reason (no gate). This file makes each
+# load-bearing assertion a traced artifact: a verbatim doc string bound to a
+# predicate re-derived FROM SOURCE (never a number typed in prose). When the
+# evidence moves, the claim fails the build.
+#
+# Run:  python3 tools/claim-check.py claims.yaml     (CI: the `claim-check` job)
+#
+# The motivating drift: issue #97 — the README status section said "v0.1.0 …
+# no real abstract-interpretation logic yet" while the crate was v3.2.4 with 12
+# published domains and 19 admit-free proofs. Fixed 2026-07-16; now gated so it
+# can't silently drift ~40 versions again.
+
+claims:
+  # ── Version / status (issue #97) ──────────────────────────────────────────
+  # The status line names the current release. Bound to the workspace version:
+  # bump Cargo.toml and forget the README → the pattern matches 0 in Cargo.toml →
+  # "measures nothing" → red. (Bumping the version means updating README +
+  # Cargo.toml + this pattern together — exactly the point.)
+  - id: STATUS-VERSION
+    doc: README.md
+    text: "**v3.2.4 shipped**"
+    evidence:
+      - kind: count-min
+        pattern: 'version = "3\.2\.4"'
+        glob: ['Cargo.toml']
+        min: 1
+
+  # ── Admit-free proofs ─────────────────────────────────────────────────────
+  # The README claims 0 Admitted/admit/Axiom across the Rocq proofs. Re-counted
+  # from the actual .v source (not a typed figure); a single admit/axiom → red.
+  - id: ADMIT-FREE
+    doc: README.md
+    text: "0 `Admitted` / `admit` /"
+    evidence:
+      - kind: count-max
+        pattern: '\bAdmitted\b'
+        glob: ['proofs/rocq/**/*.v']
+        max: 0
+      - kind: count-max
+        pattern: '\bAxiom\s+\w'
+        glob: ['proofs/rocq/**/*.v']
+        max: 0
+      - kind: count-max
+        pattern: '\badmit\s*\.'
+        glob: ['proofs/rocq/**/*.v']
+        max: 0
+
+  # ── Published-crate count ─────────────────────────────────────────────────
+  # "12 pure scry-sai-* crates". Re-counted from the publish manifest; add a
+  # 13th crate and forget the README → 13 > 12 → red.
+  - id: CRATES-12
+    doc: README.md
+    text: "12 pure"
+    evidence:
+      - kind: count-max
+        pattern: '"scry-sai-[a-z]+"'
+        glob: ['scripts/publish.rs']
+        max: 12
+      - kind: count-min       # pin exact: a REMOVED crate also makes "12" stale
+        pattern: '"scry-sai-[a-z]+"'
+        glob: ['scripts/publish.rs']
+        min: 12
+
+  # ── i32.add vs OFFICIAL wrapping semantics (the differentiator) ────────────
+  # The README's scoped soundness claim rests on WrapAdd.v existing. If the proof
+  # is deleted/renamed, the claim fails rather than dangling.
+  - id: WRAPADD-EXISTS
+    doc: README.md
+    text: "`WrapAdd.v`"
+    evidence:
+      - kind: file-exists
+        path: proofs/rocq/WrapAdd.v
+
+  # ── Soundness stated as SCOPED, not flattened ─────────────────────────────
+  # A formal-methods reviewer distrusts a flat "verified" badge. The README must
+  # carry the mechanized-vs-γ-swept distinction verbatim (same wording as the
+  # deployed dashboard's Scope & limitations block).
+  - id: SOUNDNESS-SCOPED
+    doc: README.md
+    text: "γ-sweep-validated (tested, NOT mechanized)"
+    evidence:
+      - kind: file-exists
+        path: docs/qualification-dossier-v1.md

docs/architecture.md

@@ -184,11 +184,11 @@ graph TD
     S1[1 · AADL in spar<br/>spar/scry.aadl<br/>✅ parsed by spar] --> S2
     S2[2 · WIT from spar<br/>hand-derived per DD-010<br/>✅ round-trips wasm-tools] --> S3
     S3[3 · Typed rivet artifacts<br/>artifacts/*.yaml + schemas/research-ext.yaml<br/>✅ rivet validate PASS, 63 artifacts] --> S4
-    S4[4 · Code oracle-gated<br/>bazel build //:scry green<br/>scaffold ✅; real fixpoint ⏳ FEAT-001 AC#1] --> S5
-    S5[5 · witness MC/DC<br/>⏳ deferred: scaffold has too few branches] --> S6
-    S6[6 · sigil attestation<br/>⏳ deferred to v0.6 via FEAT-004 + release.yml cosign] --> S7
-    S7[7 · Clean-room verify<br/>⏳ deferred to v1.0 dossier] --> S8
-    S8[8 · Release via release-execution<br/>⏳ pending v0.1.0 tag]
+    S4[4 · Code oracle-gated<br/>bazel build //:scry green<br/>✅ full interval/region/octagon/…/polyhedra fixpoint] --> S5
+    S5[5 · witness MC/DC<br/>✅ live CI gate on scry_mcdc.wasm] --> S6
+    S6[6 · sigil attestation<br/>✅ cosign-signed releases + SLSA provenance] --> S7
+    S7[7 · Clean-room verify<br/>✅ per-release adversarial review] --> S8
+    S8[8 · Release via release-execution<br/>✅ shipped through v3.2.4]
 
     classDef done fill:#1a3a1a,stroke:#5fa05f,color:#fff
     classDef pending fill:#3a1a1a,stroke:#a05f5f,color:#fff
@@ -225,10 +225,16 @@ analyzer gets real branches to measure and real invariants to attest.
 
 ## 6. The cross-component runtime probe
 
-The v0.1 scaffold's `analyzer.analyze` implementation does one
-non-trivial thing: it calls the lattice's `constant_i32(42)` and
-embeds the result in a diagnostic. That call crosses the component
-boundary and exercises the entire WAC-composed runtime wiring:
+> **Historical (v0.1 milestone).** This section describes the very first
+> cross-component probe. As of v3.2.4 `analyze` runs the full
+> interval/region/octagon/pentagon/float/known-bits/handle/segmentation/polyhedra
+> fixpoint over a parsed Wasm module (see the roadmap and the 12 published
+> `scry-sai-*` crates); the runtime wiring below is unchanged.
+
+At the v0.1 milestone, `analyzer.analyze` did one non-trivial thing: it called
+the lattice's `constant_i32(42)` and embedded the result in a diagnostic. That
+call crosses the component boundary and exercises the entire WAC-composed
+runtime wiring:
 
 ```mermaid
 sequenceDiagram

tools/claim-check.py

@@ -0,0 +1,143 @@
+#!/usr/bin/env python3
+"""claim-check — gate a repo's documentation claims against live evidence.
+
+Reference implementation for the `claim-verification` skill. A repo drops a
+`claims.yaml` next to its docs; CI runs this; drift between a claim, its recorded
+ledger, 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
+
+A repo may reimplement this in Rust (cf. tools/fetch-reports); the shape is what
+matters. Evidence predicates re-derive from source — never a number typed in prose.
+
+claims.yaml shape:
+  claims:
+    - id: LOOM-BADGE
+      doc: README.md
+      text: "Translation-Validated"          # must appear VERBATIM in `doc`
+      evidence:
+        - kind: file-exists
+          path: proofs/Correctness.v
+        - kind: count-max                      # re-count from source; fail if over
+          pattern: '#\\[verifier::external_body\\]'
+          glob: ['src/**/*.rs']
+          max: 133
+        - kind: no-new                         # no new sorry/admit since recorded
+          pattern: '\\bAdmitted\\b'
+          glob: ['proofs/**/*.v']
+          recorded: 74
+"""
+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:
+        # Resolve globs relative to the claims file's directory, NOT the CWD —
+        # otherwise the predicate silently matches nothing and greens a claim it
+        # never checked (the "oracle that measures nothing" failure).
+        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":
+            # PRESENCE claim: the pattern must appear at least `min` times in the
+            # source. Unlike count-max, this catches DRIFT-TO-ABSENT — e.g. a
+            # version string the README asserts but Cargo.toml no longer carries.
+            # (count-max greens a 0-match because 0 <= max; count-min is the dual.)
+            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 but the source no longer shows 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()