§17c. Guarantees site

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

Planarian publishes a generated documentation site organized around its guarantees, as docs.rs is organized around a crate’s API: every page is computed from the repository at one commit, never written by hand, and every claim links down to the code, proofs, tests and limits that carry it. It exists so an auditor can start from “what does this system promise?” and reach the exact lines that keep the promise, at the exact commit under audit.

Sources. The site is built only from files the repository already maintains: the invariant table (§7), docs/verification-ratio.toml (obligations and assumptions per invariant), docs/assumptions.md, docs/bypasses.md, the gym catalog (each entry’s spec and invariants fields) and its latest run results, docs/spec-history.md, and the source tree (to locate each obligation by name). Nothing on the site is entered anywhere else.

Pages.

• One page per invariant: the statement verbatim from §7; proof phase, status and d:a against the baseline; each discharged obligation with its kind (verified fn, proof fn, Kani harness), what it guarantees, and a permalink to its line at the commit; the assumptions it rests on, each with its text, its kind (platform, proof-validity, internal unproven) and the other invariants that rest on it; the global proof-validity assumptions that apply to every proof; the gym entries that exercise it, with harness, expectation and the verdict from the run at that commit; the bypass rows that limit it; and its history across spec versions.
• Reverse indexes: per assumption (which invariants fall if it is false); per bypass (which guarantees it narrows); per source file (which invariants and obligations live there); per gym entry (what it exercises).
• The spec itself, one page per section, with cross-references as links.
• API docs: cargo doc output for the workspace, linked from invariant pages for the types they concern. Proof obligations link to source lines, not rustdoc, because rustdoc renders verus! blocks poorly.

Versions. A snapshot is built for every tagged release and for the head of main. Tagged snapshots are immutable and kept; main is rebuilt on every push. Every page names its commit and spec version in its first line and links to the same page in other snapshots.

The build is the check. The generator fails the build on any reference it cannot resolve: an obligation name with no matching function, an assumption or bypass id with no entry, an invariant with no page, a gym entry naming an invariant that does not exist, a bypass row with no invariants column. CI runs it on every push, so a docs failure is a build failure; a gate claim (§18 rule 19) may cite the site’s snapshot at the gate commit.

Where it lives. The generator is a subcommand of planarian-gym (planarian-gym site), beside verification, which already parses these files and checks the same names. The site is an mdBook published to GitHub Pages from CI. It is generated output and is never committed to the repository.