diff --git a/docs/design/doc-reality-audit.md b/docs/design/doc-reality-audit.md new file mode 100644 index 0000000..184404a --- /dev/null +++ b/docs/design/doc-reality-audit.md @@ -0,0 +1,194 @@ +# Documentation-Reality Audit + +Date: 2026-04-19 +Scope: README, docs/, CHANGELOG, AGENTS.md, CLAUDE.md, vscode-rivet/README.md, +schemas, CLI help strings. Evidence only; no fixes applied. + +## 1. TL;DR + +28 mismatches found. 4 HIGH, 14 MEDIUM, 10 LOW. Top offenders: (1) Kani +CI job and Verus/Rocq are soft-gated (`continue-on-error: true`) while the +v0.4.0 CHANGELOG bullet reads "wired into CI" without qualification on the +Kani line; (2) `docs/schemas.md` documents 5 schemas while `schemas/` ships +27; (3) `docs/audit-report.md` (dated 2026-03-09) still claims fuzz and +mutation testing are "NOT IMPLEMENTED" — both shipped months ago; (4) README +dogfood block hard-codes "447 artifacts across 19 types", while the regenerated +AGENTS.md managed section reports 518, and raw ID counts in `artifacts/` and +`safety/` are higher still. Systemic pattern: every hand-maintained count in +prose is out of date, because the project has no CI check that numbers in +prose match `rivet stats` / `rivet list` output. + +## 2. The Register + +| File:line | Claim (short) | Reality | Type | Severity | +|---|---|---|---|---| +| README.md:53 | "235+ Playwright E2E tests" | `tests/playwright/*.spec.ts` has 29 files, ~326 `test(` calls | Out-of-date | LOW | +| README.md:177 | "447 artifacts across 19 types" | AGENTS.md managed block says 518; rivet.yaml still pins project version 0.1.0 | Out-of-date | MEDIUM | +| README.md:188 | "uca 57" in dogfood block | AGENTS.md and `.rivet/agent-context.md` both say 59 | Out-of-date | LOW | +| README.md:172 | "Built-in domain schemas (8 schemas)" | `ls schemas/` → 27 files incl. do-178c, iec-61508, iec-62304, en-50128, iso-pas-8800, sotif, score, safety-case, eu-ai-act, and 9 bridge schemas | Out-of-date | MEDIUM | +| README.md:199 | "cargo test --all # 500+ tests" | Unverified from outside; count is not CI-published anywhere | Implementation-hidden | LOW | +| README.md:47 | "`rivet export --gherkin` generates .feature files" | CLI takes `--format gherkin`, not `--gherkin` (rivet-cli/src/main.rs:4230) | Out-of-date | LOW | +| README.md:51 | "`rivet init --agents` generates AGENTS.md (25+ tools)" | Accurate (36+ CLI subcommands in `enum Command` at rivet-cli/src/main.rs:162-715) | Accurate | — | +| CHANGELOG.md:7 | "Verus + Rocq jobs wired into CI via Bazel" on main feature bullet | `.github/workflows/ci.yml:392,404,423` all `continue-on-error: true`; Kani job also soft-gated | Silent-fail | HIGH | +| CHANGELOG.md:36-37 | CI section admits "marked `continue-on-error: true` pending toolchain stabilization" — but only for Verus/Rocq | Kani is *also* `continue-on-error: true` (ci.yml:392). CHANGELOG implies Kani is hard-gated ("enabled — previously commented out"). | Silent-fail | HIGH | +| CHANGELOG.md:29 | "27 Kani BMC harnesses" | `grep -c "#[kani::proof]" rivet-core/src/proofs.rs` → 27 exact | Accurate | — | +| CHANGELOG.md:82 | "235+ Playwright E2E tests across 22 spec files" | 29 files, ~326 tests today | Out-of-date | LOW | +| docs/schemas.md:11-17 | Schema table lists 5 schemas (common, dev, stpa, aspice, cybersecurity) | 27 schema files present incl. 10+ domain schemas and 9 bridge schemas not documented | Out-of-date | HIGH | +| docs/schemas.md | No section for `feature-model` YAML (user issue #3) | `rivet-core/src/feature_model.rs` loads kind:feature-model YAML; `examples/variant/feature-model.yaml` is the only example | Implementation-hidden | MEDIUM | +| docs/audit-report.md:130 | "Fuzz Testing — Status: NOT IMPLEMENTED" | `fuzz/fuzz_targets/` has 5 targets (yaml, reqif, schema merge, needs-json, document) | Out-of-date | HIGH | +| docs/audit-report.md:150 | "Mutation Testing — Status: NOT IMPLEMENTED" | `.github/workflows/ci.yml:288-333` runs cargo-mutants on both rivet-core and rivet-cli | Out-of-date | HIGH | +| docs/audit-report.md:220 | "MSRV 1.89" | Matches Cargo.toml:14 (`rust-version = "1.89"`) | Accurate | — | +| docs/verification.md:137 | "msrv 1.85" in CI gate table | Cargo.toml says 1.89; CI uses dtolnay/rust-toolchain@1.89.0 | Out-of-date | MEDIUM | +| docs/srs.md:85 | "[[REQ-011]] pins Rust edition 2024 with MSRV 1.85" | MSRV is 1.89 | Out-of-date | MEDIUM | +| docs/getting-started.md:465 | "Supported formats: `reqif`, `generic-yaml`" | `cmd_export` accepts reqif, generic-yaml, generic, html, gherkin, zola (rivet-cli/src/main.rs:4225-4232) | Out-of-date | MEDIUM | +| docs/getting-started.md:863 | "MCP Server — exposes 15 tools" | Count matches (mcp.rs `fn rivet_*` count: validate, list, stats, get, coverage, schema, embed, snapshot_capture, add, query, modify, link, unlink, remove, reload) | Accurate | — | +| docs/getting-started.md:839-840 | Only `rivet_artifact` and `rivet_stats` Zola shortcodes listed | Unverified; Zola shortcodes generated by `--shortcodes` flag — doc does not list the full set | Implementation-hidden | LOW | +| docs/architecture.md:85 | "`oslc` — OSLC client for discovery, query, CRUD, and sync (feature-gated)" | `rivet-core/src/oslc.rs` is 1911 lines and *not* feature-gated in rivet-core/Cargo.toml (builds unconditionally); there is no `rivet oslc` or `rivet sync --oslc` subcommand | Aspirational | MEDIUM | +| docs/architecture.md:269-275 | Schema table lists same 5 schemas as schemas.md | Same mismatch — 27 files exist | Out-of-date | MEDIUM | +| docs/stpa-sec.md:120 | "Current mitigations in place as of v0.2.0-dev" | Workspace is v0.4.0 | Version-stale | MEDIUM | +| docs/stpa-sec.md:127-129 | "SSC-1 Provenance check — Phase 3 / Planned" | Phase 3 features largely shipped in v0.4.0; status unverified but banner stale | Version-stale | LOW | +| docs/roadmap.md:104-116 | "Phase 3 — Sync & Extensibility (Planned)" | v0.4.0 shipped variant/PLE, MCP, Zola export, rowan/salsa, Kani, sphinx-needs import; roadmap document itself never updated past Phase 3 section | Out-of-date | MEDIUM | +| vscode-rivet/README.md:46 | "`cargo install rivet-cli`" | rivet-cli depends on rivet-core as a path dep; never published to crates.io; no publish CI for it | Aspirational | HIGH | +| vscode-rivet/package.json:6 | `"version": "0.3.0"` | Workspace is 0.4.0 | Version-stale | MEDIUM | +| CLAUDE.md:4 | "A Claude Code pre-commit hook runs `rivet validate` before each commit (configured in `.claude/settings.json`)" | Hook exists but `rivet init --hooks` installs one that requires `python3` to parse JSON (rivet-cli/src/main.rs:2480). Not documented as a dependency. | Implementation-hidden | MEDIUM | +| docs/getting-started.md:720-752 | S-expression predicates/quantifiers listed | Matches `rivet-core/src/sexpr_eval.rs`; `(reachable-from ...)`, `forall`, `exists` present | Accurate | — | +| docs/getting-started.md:722 | "s-expressions — one syntax for CLI, API, constraints, and queries" | Query engine in `rivet-core/src/query.rs` uses a *separate* `Query` struct (type/status/tags); only `--filter` on CLI takes s-expressions | Implementation-hidden | LOW | +| (various) | `{{query:...}}` and `{{group:...}}` embed tokens referenced in session prompt | No such tokens in code. `embed.rs` supports stats, coverage, diagnostics, matrix, artifact, links, table. No query/group. | N/A (never claimed in repo docs) | — | + +Tokens `{{query:...}}`, `{{group:...}}`, `rivet discover`, `rivet gaps`, +`rivet variant check-all` do **not** appear anywhere in the repo's doc files +(grep of `docs/`, `README.md`, `CHANGELOG.md`, `AGENTS.md` produced zero +matches for each). They were hypothesised in the audit prompt but the repo +is clean of those specific aspirational terms. + +## 3. Top 3 most-misleading + +### 3.1 Kani/Verus/Rocq "wired into CI" (CHANGELOG.md:7, 36) + +Claim (CHANGELOG.md:7): "Kani BMC expanded from 15 to 27 harnesses +covering the core public API, Verus/Rocq jobs wired into CI via Bazel". +Claim (CHANGELOG.md:36): "Kani job enabled — previously commented out". + +Reality (.github/workflows/ci.yml:392, 404, 423): all three jobs are +`continue-on-error: true`. Proof regressions cannot block merge. +CHANGELOG.md:37 discloses this for Verus/Rocq in a parenthetical but +omits Kani, and the headline bullet omits all three. + +Why misleading: a reader evaluating rivet for ISO 26262 / TCL 3 tool +qualification will conclude formal verification is hard-gated — the +headline v0.4.0 feature — when in practice regressions are silent. + +Remediation: either flip jobs to hard-gate or add "(soft-gated, pending +toolchain stabilization)" to every CHANGELOG mention including Kani. +Effort S. + +### 3.2 audit-report.md says fuzz + mutation "NOT IMPLEMENTED" (docs/audit-report.md:130, 150) + +Claim (130, 150): "**Status: NOT IMPLEMENTED**" for both fuzz and +mutation testing. + +Reality: `fuzz/fuzz_targets/` has 5 targets (yaml, reqif, schema-merge, +document, needs-json). `.github/workflows/ci.yml:288-333` runs +`cargo mutants` on both crates and uploads reports. + +Why misleading: this 2026-03-09 doc is the canonical "quality audit". +An auditor consulting it will misjudge test-effectiveness posture; the +"Overall 73%" score is calibrated against the missing-fuzz/mutation +lines. + +Remediation: delete or stamp "superseded by v0.4.0 verification +pyramid". Effort S. + +### 3.3 schemas.md documents 5 of 27 schemas (docs/schemas.md:11-17) + +Claim: table listing common, dev, stpa, aspice, cybersecurity. + +Reality: `ls schemas/` → 27 files. Missing from docs: do-178c, +en-50128, iec-61508, iec-62304, iso-pas-8800, sotif, stpa-sec, stpa-ai, +safety-case, score, aadl, eu-ai-act, research, supply-chain, and 9 +`.bridge.yaml` files. The feature-model YAML kind (issue #3) is also +undocumented apart from a code block in getting-started.md. + +Why misleading: a user adopting rivet for IEC 61508 or DO-178C will +see no mention in docs/schemas.md that these schemas exist, and will +likely write their own. The schemas ship but silently. + +Remediation: regenerate from `rivet schema list` + `rivet schema show +`; add feature-model section. Effort M. + +## 4. Systemic Patterns + +1. **Prose counts drift.** Every hand-coded number in `.md` files + (447 artifacts, 500+ tests, 235+ Playwright tests, MSRV 1.85) is + stale. Regenerated sections (AGENTS.md managed block, + `.rivet/agent-context.md`) are correct; free-form prose isn't. + No CI check compares prose to `rivet stats` output. + +2. **Soft-gate semantics hidden from CHANGELOG.** Three of four + verification pyramid jobs (kani, verus, rocq) use + `continue-on-error: true`; CHANGELOG qualifies only two, only + in a parenthetical, not in the headline bullet. + +3. **Stale snapshot docs never superseded.** audit-report.md, + roadmap.md, architecture.md §8, verification.md were written + for earlier releases and never refreshed. No "superseded" + marker, no `last-verified` frontmatter date, no CI that fails + when a doc references a deleted module/subcommand. + +4. **Cross-file divergence on identical facts.** README vs AGENTS.md + cite different UCA counts (57 vs 59) and artifact totals + (447 vs 518). No authoritative source. + +5. **Unverified "feature-gated" claims.** architecture.md marks + oslc and wasm_runtime as feature-gated; only `wasm` is actually + a Cargo feature; `oslc` builds unconditionally. + +## 5. Remediation Plan for v0.4.1 + +Ranked by impact/effort: + +| # | File | Change | Effort | +|---|---|---|---| +| 1 | CHANGELOG.md:7, 36 | Add "(soft-gated, pending toolchain stabilization)" to Kani and headline Verus/Rocq bullets, or hard-gate Kani | S | +| 2 | docs/audit-report.md | Either delete (stale point-in-time) or rewrite to reflect fuzz/mutants/Kani/Verus/Rocq that now ship | M | +| 3 | docs/schemas.md | Regenerate from `rivet schema list` for all 27 schemas; add feature-model section | M | +| 4 | docs/architecture.md:269-275, §8 | Update schema table; rewrite "Phase 3 Architecture Extensions" into a "what-shipped-in-v0.4.0" section | M | +| 5 | docs/roadmap.md | Reflect that Phase 3 and much of Phase 3 extensions shipped | S | +| 6 | docs/verification.md:137 | MSRV 1.85 → 1.89 | S | +| 7 | docs/srs.md:85 | MSRV 1.85 → 1.89 | S | +| 8 | README.md:177-193 | Replace hand-coded 447 / per-type counts with a note: "Run `rivet stats` for live counts." Remove 57 UCAs. | S | +| 9 | README.md:172 | "8 schemas" → "25+ domain schemas" or live count | S | +| 10 | README.md:47 | `rivet export --gherkin` → `rivet export --format gherkin` | S | +| 11 | README.md:53, 199, 203 | "235+ Playwright", "500+ tests" → strip numbers or link to CI badge | S | +| 12 | vscode-rivet/package.json:6 | Bump to 0.4.0 (align with workspace) | S | +| 13 | vscode-rivet/README.md:46 | Replace `cargo install rivet-cli` with `cargo install --path rivet-cli --git ...` or link to releases | S | +| 14 | docs/stpa-sec.md:120-129 | Remove "v0.2.0-dev" banner; refresh SSC implementation status table | S | +| 15 | docs/getting-started.md:465 | "Supported formats: reqif, generic-yaml" → add html, gherkin, zola | S | +| 16 | docs/architecture.md:85 | oslc: drop "(feature-gated)" wording or actually gate it | S | +| 17 | CLAUDE.md | Note `rivet init --hooks` requires python3 at runtime | S | +| 18 | (new) `docs/design/json-output-schema.md` | Publish the stable JSON envelope schema FEAT-025 claims | L | +| 19 | (new CI check) | Lint that fails when `.md` contains a count that differs from live `rivet stats` | L | + +## 6. What the Docs Should STOP Claiming + +Until genuinely shipped and hard-gated: + +- **"Verus + Rocq wired into CI"** / **"Kani job enabled"** without a + "(soft-gated)" qualifier on every mention. +- **"NOT IMPLEMENTED" banners on fuzz/mutation** in audit-report.md. +- **"OSLC feature-gated"** in architecture.md (gate in Cargo.toml or + drop the qualifier). +- **Hand-coded artifact counts** in README, CHANGELOG v0.2.0 subsection + claims (e.g. "31 adversarial threat artifacts"), docs/srs.md STPA ID + ranges. Replace with a single "live counts via `rivet stats`". +- **`cargo install rivet-cli`** in vscode-rivet/README.md — not possible + without crates.io publish. Use `--git` install form or publish. +- **Stable JSON output envelope** (FEAT-025) — claimed shipped but no + schema is published in docs/. + +--- + +Evidence: README.md, CHANGELOG.md, AGENTS.md, CLAUDE.md, docs/{schemas, +verification, srs, architecture, audit-report, getting-started, stpa-sec, +roadmap}.md, vscode-rivet/{README.md,package.json}, .github/workflows/ci.yml, +rivet-core/src/{proofs,embed}.rs, rivet-cli/src/main.rs, Cargo.toml.