Module site 

planarian-gym site: the guarantees site (SPEC §17c). Every page is computed from the repository at one commit: the invariant table (§7), docs/verification-ratio.toml, docs/assumptions.md, docs/bypasses.md, the gym catalog and a run’s results, docs/spec-history.md and the source tree. It writes an mdBook (book.toml, src/); mdbook build turns it into the site. The build is the check: any reference it cannot resolve fails it.

Structs

Assumption 🔒

Bypass 🔒

Entry 🔒

Invariant 🔒

Obligation 🔒

Opts

What a page needs to know about where it is published.

Row 🔒

Section 🔒

Site

Sources

Every file the site is built from, read once.

Constants

ASSUMPTIONS

BYPASSES

CATALOG

HISTORY

RATIO

SPEC

VERIFIED 🔒

The crates Verus checks: a function there is a verified fn.

Functions

about 🔒

The part of a changelog bullet about invariant n: its clauses that name it.

build

by_number 🔒

Invariant ids in numeric order (I6 before I12).

bypass_refs 🔒

Bypass ids a text names: B-8, X-12.

cells 🔒

A table row’s cells, the outer pipes dropped.

change_sections 🔒

The changes sections, each with the version it produced: “Changes from v4.4” produced the next one’s from-version, the last the current spec.

esc 🔒

expectation 🔒

A short, computed account of what an entry requires afterwards.

global_ids 🔒

The proof-validity ids every proof rests on: “proof-validity trust (V7–V11)”.

gym_ref 🔒

A gym reference in a tested list: “gym journal-record-edited”, “gym posture-*”; the entries it names, or None if it is not a gym reference.

invariant_refs

The invariant numbers a text names: I18, and ranges I1–I14.

kind_of 🔒

linkify 🔒

Markdown with §, invariant and bypass references as links, outside code spans. up leads from the page to the snapshot root.

locate 🔒

fn name in a crate’s sources: file, line, kind, doc comment, module.

main

planarian-gym site [--out DIR] [--results FILE] [--commit SHA] [--repo OWNER/NAME] [--snapshot NAME] [--others a,b]: exit 1 with every unresolved reference, 0 with the book written.

parse_assumptions 🔒

assumptions.md: each bold id with its text and the sites column.

parse_bypasses 🔒

rust_files 🔒

section_refs 🔒

The spec sections a text names: §12c → “12c”, §12 step 4 → “12”.

short_title 🔒

slug_of 🔒

A heading’s slug: “12c” for ### 12c. …, “22-27” for ## 22–27. …, else the title in lower case with dashes.

split_sections 🔒

## and ### sections, in order, with their text.

write

Write the book: book.toml and src/.