Prepare AutoProver reports for Solana

[ericeil]

Third in a series splitting long-lived Solana/CVLR work into independently reviewable pieces (after #239 and #240). AutoProver cannot run the Solana Prover yet; this is shared report work that has to be in place before a Solana backend can produce a report anyone can trust.

Two different layers are involved, and they read more easily apart:

• Getting verdicts back from the Prover — how a finished job's per-rule results are fetched. An integration defect, and a bug regardless of what consumes the results.
• What the report document records — two places the report's own vocabulary was narrower than what the pipeline already knew.

composer/spec/source/report_prover.py is the adapter between those layers, which is the only reason one file appears in both halves below.

Getting verdicts back from the Prover

prover_output_utility extracts a job id from /output/<user>/<job>/… or /job/<job> and recognizes no other shape. The Solana Prover's report link — the one certoraSolanaProver prints and the CLI records — is /jobStatus/<userId>/<jobHash>?anonymousKey=…, so the extraction raises.

The report's verdict fetch is deliberately best-effort: any failure means "no verdicts for this run". Together those two facts make a completed Solana job come back empty. On the development branch, a run whose own output.json reported SUCCESS for all seven rules produced a report in which all seven were UNKNOWN, with no source lines and no durations — a false negative in the deliverable, arrived at silently, from a job that was green.

POU's entry points accept a bare job id as well as a URL, so job_input extracts the id and hands that over. Every shape POU already parses passes through untouched, which the tests pin — including the local emv- path its offline mode wants, because fixing the Solana link must not break the EVM one.

Two things to be clear about: the real fix belongs upstream in POU, and nothing on master reaches this path, since the shape is the Solana Prover's. It is here rather than in a PR of its own because it lives in the same adapter as the type change below.

What the report document records

A component that gave up now says why

When AutoProver stops on a component, it usually knows exactly what stopped it — often naming the prover error and the setting that would have unblocked it. The report recorded only that the component produced nothing: the reason existed on both paths (the author's own account, or an exception's text) and was discarded at the boundary, because the input type for "produced nothing" was None and a None has nowhere to put it.

Abandoned(reason) is that variant, and GaveUpComponent.reason is where it lands.

This is the one change here that affects AutoProver today, on EVM runs as much as any other, and the reason is often the most useful line in the document.

The verdict hook no longer names one backend

make_prover_fetcher reads nothing but a run link, but was typed VerdictFetcher[GeneratedCVL], so any other backend wanting the same roll-up had to reach past the factory for the module-private _fetch and re-implement the run_link is None check around it. It is VerdictFetcher[ReportableResult] now, and _fetch becomes public as fetch_verdicts. The test drives the returned fetcher over a non-CVL Formalized, on both the verdict path and the run_link is None one.

Review notes

• schema_version → 3.2, for GaveUpComponent.reason. Earlier revisions of this PR also carried a build_environment field recording whether a backend's builds ran sandboxed; it has been dropped, because nothing consumes it and no backend on master can set it.
• composer/pipeline/core.py is also touched by Let a component lose property extraction without losing the run #228; the report files by Generalize findings to support non-Prover backends #185 and Read verdicts from every run that accounts for the published spec #232. Whoever lands second pays a small merge.
• pytest -m "not expensive" → 1336 passed; pyright → 0 errors.

🤖 Generated with Claude Code