diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8841fe3..febc7c0 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/README.md b/README.md index 1532c26..96c2793 100644 --- a/README.md +++ b/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. + + + +**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? diff --git a/claims.yaml b/claims.yaml new file mode 100644 index 0000000..3f31280 --- /dev/null +++ b/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 diff --git a/docs/architecture.md b/docs/architecture.md index 0fc5766..8a2fb15 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -184,11 +184,11 @@ graph TD S1[1 · AADL in spar
spar/scry.aadl
✅ parsed by spar] --> S2 S2[2 · WIT from spar
hand-derived per DD-010
✅ round-trips wasm-tools] --> S3 S3[3 · Typed rivet artifacts
artifacts/*.yaml + schemas/research-ext.yaml
✅ rivet validate PASS, 63 artifacts] --> S4 - S4[4 · Code oracle-gated
bazel build //:scry green
scaffold ✅; real fixpoint ⏳ FEAT-001 AC#1] --> S5 - S5[5 · witness MC/DC
⏳ deferred: scaffold has too few branches] --> S6 - S6[6 · sigil attestation
⏳ deferred to v0.6 via FEAT-004 + release.yml cosign] --> S7 - S7[7 · Clean-room verify
⏳ deferred to v1.0 dossier] --> S8 - S8[8 · Release via release-execution
⏳ pending v0.1.0 tag] + S4[4 · Code oracle-gated
bazel build //:scry green
✅ full interval/region/octagon/…/polyhedra fixpoint] --> S5 + S5[5 · witness MC/DC
✅ live CI gate on scry_mcdc.wasm] --> S6 + S6[6 · sigil attestation
✅ cosign-signed releases + SLSA provenance] --> S7 + S7[7 · Clean-room verify
✅ per-release adversarial review] --> S8 + S8[8 · Release via release-execution
✅ 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 diff --git a/tools/claim-check.py b/tools/claim-check.py new file mode 100755 index 0000000..1802da7 --- /dev/null +++ b/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()