Generalize findings: each backend says what its evidence is, the host writes it up

[ericeil]

What this is

The report's Findings section existed, but the only way to fill it was an evidence fetcher that
meant "run the Certora Prover write-up". Returning a fetcher opted you into a heavy-model pass
whose prompt asserts the Certora Prover found a concrete counterexample. Foundry and the Rust
host returned None to opt out of code that could never have served them.

This generalizes that seam so any backend — including a Rust-authored one — can answer what did
this run find in its own terms. The write-up loop stays in one place.

The seam

Formalizer.findings_policy(outcomes) -> FindingsPolicy | None. None means the backend produces
no findings and never starts the heavy model.

A FindingsPolicy is three fields, and only the first is a function:

Field	Role
fetch_evidence	Keyed by RuleRef — (file, name), how the report already identifies a row. A check name alone does not: one deliverable can hold several components' checks. The only hook, because it is the only one that does I/O.
domain	What this backend's evidence is. True of one backend and false of another. A Rust-authored backend ships this string as FindingsDeclaration.domain.
prompt	A TypedTemplate[FindingsPromptParams]. The Prover supplies its own; every Rust-authored backend shares one host template. The loop binds the same fields either way.

Everything else is shared in report/findings.py: walking the BAD rows, resolving properties and
audit groups, collapsing rows that share one finding, the proof of concept, composing the
Finding. A failure there costs the findings, never the report.

Evidence has one shape

Every backend hands back the same RuleEvidence. Backends differ in what they can fill, not in
the shape. Absence always means "this run recorded nothing of that kind".

Field
label	Which instance, where a rule can fail more than once
analysis	Why the check failed, when the backend produces a root-cause account
counterexample	What reproduces it
ran	The run's own outcome, before any expected-to-fail mark is folded in
accounting	What the run spent and covered
expected_failure_reason	Why the author marked this check expected to fail, when they did
finding_key	Opaque grouping key, when one conclusion covers several checks

One system prompt, one severity rule

A findings system prompt splits the same way for every backend: what this evidence is (and how
far it goes) is the backend's domain; how severity is reached and which sections come back is
the host's contract (autoprove_report_findings_system.j2).

The model rates impact and likelihood; severity_for maps the pair through a fixed matrix. No
backend picks a tier.

Report rows keep evidence, accounting, and expected-failure apart

The report Verdict / RuleVerdict carry three optional fields:

• message — the counterexample or error (detail on the rust wire)
• accounting — what the run spent (None for backends that do not report it)
• expected_failure — ReproducedExpectedFailure or UnreproducedExpectedFailure (reason +,
  when unreproduced, the outcome the run actually reached)

HTML shows them as separate blocks. The findings write-up reads the same split off
RuleEvidence, so a proof of concept is never padded with accounting or declaration prose.

Rust-authored backends

In this repo, a Rust-authored backend is a wheel: compiled Rust that the Python host drives
through an FFI. Three wire additions, all deny_unknown_fields + required::present:

• AppDescriptor.findings: Option<FindingsDeclaration> — opt-in. The domain string is what
  the evidence is. Default is None (no findings). The example app opts out.
• Verdict.accounting — what the run spent and covered, kept apart from detail.
• Verdict.finding_key: Option<FindingKey> — an opaque, run-global key for a conclusion the
  wheel could not attribute to one check. Rows stamped alike are written up once, against the
  union of their properties and groups. provenance.covers names every row the write-up answers
  for. Stamped and never inferred.

composer/rustapp/findings.py maps wire fields into RuleEvidence and leaves analysis unset.

Expected-to-fail checks still report as findings

A check marked expect_check_failure is a documented finding even if this run did not hit it.
The publish gate accepts such a check as clean without requiring a repro.

expected_failures rides RustFormalResult. reported_verdicts() folds the outcome to
BAD and leaves detail as the run reported it. expected_failure() builds the tagged union
for the report row. The console rollup reads the same outcome fold, so the terminal and
report.html cannot disagree about whether the run found something.

Docs

formalization-abstraction.md §4.6 covers the hook and the evidence table.
rust-applications.md §4.5 covers the wheel's side, and §5/§6 the expect_check_failure fold.

Validation

Cheap suite and pyright clean. The first commit stands alone (the suite passes there with no
rustapp participation).