Module verification 

planarian-gym verification: the verification ratio d:a (discharged to assumed obligations), the trust count |𝒯| and the internal-unproven count (SPEC §17a), from docs/verification-ratio.toml, checked against the source and docs/assumptions.md, and held to the recorded baseline; and the bypass register, docs/bypasses.md (§17b): its format, and its open rows by severity. --gate also fails on an open High row (every gate does).

The trust count is the number of platform and proof-validity ids in assumptions.md (P, G, V) plus every external_body and assume site in the verified crates. The internal-unproven count is the number of U ids: Planarian’s own unproven code that the proven gates take input from. A discharged obligation is a Verus lemma or verified function, or a Kani harness, named in the file and present in the source.

Structs

Report

Enums

Discharge

What discharges an obligation (§17a, R14): a Verus proof fn or a function verified against its ensures, inside verus!; or a Kani harness (#[kani::proof]). A name that is only present (a plain function, a test, a comment) discharges nothing.

Constants

ASSUMPTIONS 🔒

BYPASSES 🔒

CATALOG 🔒

RATIO 🔒

VERIFIED 🔒

Functions

bypasses 🔒

The bypass register’s open rows by severity, and its format errors.

discharge 🔒

discharge_in

parse_bypasses

run

rust_files 🔒

source 🔒

structure_errors

R14’s structural checks on the accounting, apart from the source: no invariant listed twice, no obligation listed twice under one invariant, and every invariant of the baseline still accounted.

trust_sites 🔒

external_body attributes and assume( calls in the verified crates (Kani’s input bounds, kani::assume, are not trust).