Add findings to the report#80
Conversation
| class EvidenceFetcher(Protocol): | ||
| """Backend hook: given a violated rule's run link + name, return its `RuleEvidence` (or ``None`` | ||
| when the backend has none). Prover reads the run-scoped CEX-analysis capture; foundry has none.""" | ||
| async def __call__(self, link: str | None, rule_name: str, /) -> "RuleEvidence | None": |
There was a problem hiding this comment.
absolutely no reason to quote this type annotation. a little curious you have the "positional only" marker here but I'm not mad about it.
| For each violated rule (a `RuleVerdict` with ``outcome == Outcome.BAD``) this reshapes the | ||
| counterexample analysis the run already produced — looked up via the backend `EvidenceFetcher` — into | ||
| a `Finding`. One structured LLM call per violation, fed the *distilled* analysis rather than the raw | ||
| counterexample, so the expensive counterexample reasoning is not repeated. Best-effort per finding: |
There was a problem hiding this comment.
what expensive reasoning? the cex analysis in cex_analysis_raw or whatever it is is single shot llm call?
| counterexample, so the expensive counterexample reasoning is not repeated. Best-effort per finding: | ||
| any failure drops that one finding, never the report. | ||
|
|
||
| v1 scope: prover-only (a foundry BAD is an author-declared demonstration, not a discovered bug). |
There was a problem hiding this comment.
I... don't think this is true? if you write an invariant test or a fuzz test, it's worth an explanation of why that invariant failure happened or why the fuzz test parameters chosen were problematic right? But for v1 this is fine, but I just want to make sure we don't buy this reasoning and avoid revisiting this for foundry in the future.
| system template. ``IssueIn.locations`` is not produced here — a run knows only local paths and CVL-spec | ||
| lines, so the submission layer reconstructs source locations from the engagement scope + counterexample | ||
| (the accurate report-time locator is on ``FindingProvenance``: rule name, spec file, prover-run link). |
There was a problem hiding this comment.
I'm sure I'll understand this more as I read the rest of the file, but having read it without further context, this last sentence is unintelligible.
| max_length=4000, | ||
| description="1-3 sentences: the Impact tier, the Likelihood tier, and the matrix cell they select.", | ||
| ) | ||
| summary: str = Field(max_length=2000, description="1-3 sentence tl;dr.") |
| prover_runs: list[RunView] | ||
| rule_counts: list[ChipView] | ||
| group_counts: list[ChipView] | ||
| findings: list[FindingView] |
| # and the ``content`` prose. One finding is emitted per violated rule (a `RuleVerdict` with | ||
| # ``outcome == Outcome.BAD``); its prose is synthesized from the rule's counterexample analysis and | ||
| # the property/group it breaks (see ``report/findings.py``). Sherlock length caps are mirrored but | ||
| # not enforced (report.json is lenient — the submission endpoint is the validating gate). |
There was a problem hiding this comment.
oh THIS is where the length caps come from? But ... wait what API are we targeting here?
| summary: str = Field(max_length=2000, description="Short tl;dr of the finding, in one to three sentences.") | ||
| description: str = Field(max_length=50000, description="Full technical description of the vulnerability and how it manifests.") | ||
| impact: str = Field(max_length=20000, description="Concrete consequence if exploited (funds at risk, DoS, data exposure, ...).") | ||
| attack_path: str | None = Field(default=None, max_length=20000, description="Step-by-step exploit path, if applicable.") | ||
| assumptions_and_uncertainties: str | None = Field(default=None, max_length=10000, description="Assumptions relied on and anything the submitter is unsure about.") | ||
| proof_of_concept: str | None = Field(default=None, max_length=65536, description="Executable PoC, or the prover counterexample demonstrating the issue.") |
There was a problem hiding this comment.
this looks super similar to the fields found in the findings.py FindingDraft schema, common basemodel class?
| In-memory is sufficient: the report phase runs in the same process as formalization within | ||
| ``composer.pipeline.core.run_pipeline``. A ``BaseStore``-backed variant (cf. | ||
| ``composer.prover.report_store``) would be the resume-safe upgrade. |
There was a problem hiding this comment.
I strongly suspect we'll someday want to use the agentic handler for the cex in autoprover, so make sure we're not baking in an assumption about always using the TrivialFanoutCexHandler here.
That said, why not use the BaseStore version? seems like we'd want to save this sort of thing?
| Use `informational` ONLY for a property break with no real-world exploit path — a code-quality or | ||
| specification observation, not a vulnerability. A prover counterexample proves the property CAN be | ||
| broken, so never downgrade a genuine break to `informational` just because it looks hard to reach; | ||
| instead lower the Likelihood tier and let the matrix decide. |
There was a problem hiding this comment.
if we expect informational to never be the correct output, why even include it in the output schema?
This also suggests we shouldn't let the agent choose this, but pick the two axes on this matrix?
2 participants
No description provided.