Show judgment arguments in coverage proof trees

[System625]

What does this PR do?

Follow-up to #410, showing the judgment arguments in coverage proof trees. Each node gets a collapsed args sub-list: positive trees list the judgment's inputs and result, negative trees show the failing judgment's arguments. The JSONL format is additive, so old coverage files still read. To keep the book shippable, args are deduplicated against the parent node and only shown for the top levels of each tree (MAX_ATTR_DEPTH = 2); this and two other limits are one-line knobs.

How does it work, what questions do you have?

Attributes were already on ProofTree (the debug inputs/result), just never surfaced, same for failing judgments, whose args are buried in the tail of the Debug string. So this is purely coverage.rs mirror changes. New fields are #[serde(default)] so old coverage files still load fine.
Only real wrinkle is size, these Debug dumps get huge and repeat a lot across big trees. Clipping long values, dropping args that match the parent, and capping depth keeps it sane. Book's already about114MB from the hover tooltips, this only adds about 1MB on top. Still not sure MAX_ATTR_DEPTH = 2 is right though, now that the tooltips dominate the size anyway, maybe we can afford to go deeper.

Positive tree (expanded args)

Negative tree (failing judgment's args)

AI disclosure

• I used an AI to author the main logic of the code

[rustbot]

Thanks for contributing to formality! :)
A reviewer will take a look at your PR within a week or two. If not, come talk to us on https://rust-lang.zulipchat.com/#narrow/channel/402470-t-types.2Fformality

[nikomatsakis]

I'm thinking about the size. I'm not very worried about the size of the json per se, but i'd like to avoid large initial loads. Maybe what we should do is to create json files that can be loaded on demand via javascript?

Basically I'd rather have the data available but not fully displayed. My ideal would be that we load the json object lazilly when you are hovering or viewing it and we render it in a collapsible form. But when you are not looking at, those resources are freed.

[System625]

Thanks, this makes sense. I reworked it so the argument values are no longer in the initial page load.

Each detail page now writes a sidecar coverage-args/<slug>.args.json, and a small inline script fetches it lazily: opening a node's args disclosure loads and renders that node's values, and collapsing it frees them again. The page HTML carries only an empty placeholder per node, so the large Debug dumps (whole programs and so on) never ship in the initial load or the search index. mdbook copies non-markdown files under src/ to the output, which is how the JSON reaches the book; it is written deterministically so mdbook serve doesn't loop rebuilding.

Since size is no longer the constraint, I also dropped the MAX_ATTR_DEPTH gate and now show args at every depth.
The video I attached shows it in action: on check_adt__check-adt__pos.html I opened a proof tree with the Network tab open, and clicking args is what triggers the fetch of coverage-args/check_adt__check-adt__pos.args.json. Nothing loads until you ask for it.

One thing I will point out is showing the collapsed args affordance at every depth adds around 2000 placeholder elements on the largest pages, so those land around 1.6MB (compared to the 1.3MB estimate before). The values themselves are lazy, but the collapsed affordance is still static HTML.

check_adt / check adt (positive) - A MIR Formality - 8 July 2026 - Watch Video