Compile-check generated harnesses before accepting them

[shellygr]

Problem

harness_generation_prompt.j2 tells the agent:

As part of delivering your result your generated harnesses will be checked for syntactic/type validity. Upon rejection, the Solidity compiler error messages will be returned to you; repair any issues and re-invoke the result tool.

That check never ran. It sat behind if False: # this doesn't work (with a second and False inside it) in generate_harnesses.result_validator, because the check it guarded was a bare solc <files> invocation, which cannot resolve a project's remappings, include paths, evm-version or via-ir settings.

So an uncompilable harness is delivered unchallenged, and is only discovered one phase later by AutoSetup, which reads it as a compilation problem to work around rather than a source error to repair. A dev run hit this: the harness for an abstract contract was missing implementations that live in a sibling mixin, AutoSetup spent four certoraRun passes on irrelevant workarounds plus an import patch, and the run then died — after the pipeline had gone on to spend roughly two thirds of its output tokens on analysis phases whose results were discarded with it.

Change

Check the candidates with the project's own build instead:

• materialize the VFS — the agent's own filesystem view, so a file it wrote but did not deliver (a shared base the harnesses import, say) is present for their imports to resolve
• run forge build --json there on the delivered harnesses, which reuses the copied build cache instead of recompiling the dependency graph
• do both off the event loop: the validator is an AsyncResultTool, the copy goes through asyncio.to_thread (as materializing_project does for the prover), and forge runs via create_subprocess_exec
• hand error-severity diagnostics back to the agent; the harnesses keep their certora/harnesses paths, so nothing needs rewriting

forge build --json exits 0 whether or not the sources compiled, so the report's severity field is the signal, not the exit code. A project with no foundry build, no forge, or a forge that never got as far as a report is accepted unchecked, as today.

Also drops HarnessAgentResult.solidity_compiler and the prompt paragraph requesting it: the removed solc invocation was its only consumer, and the version now comes from the project's own build config. No tape or fixture references the field.

Validation

• uv run --no-sync python -m pytest tests/ -m "not expensive" -q → 511 passed; pyright → 0 errors
• new unit tests over the report parsing, the forge invocation, and the result tool's schema/injection contract
• replayed the real failing harness set through a materialized copy of the actual project it came from: the broken set is rejected with the full should be marked as abstract diagnostic (including every Missing implementation note), the repaired set is accepted
• cost of the gate on that project (353MB, 12,286 files): ~4s to materialize, plus 1.8s to reject or 15.6s for a cold compile of all 16 harnesses — against a harness phase that runs ~15 minutes

Companions

Two independent PRs address the same failure from the other two directions: prompt guidance so the agent does not extend a non-deployable contract in the first place, and a terminal AutoSetup detection so the error is never mistaken for a workaround-able one.

Companion PRs: #130 #131. They are independent — any order, any subset.

[shellygr]

shouldn't you wrap this call with materialize?

[shellygr]

Claude answers: yes — done in e51d98f, and thank you, it was covering a real gap rather than just being tidier.

The gap: I was writing only the delivered harnesses. The VFS can also hold files the agent wrote but did not deliver — a shared base contract the harnesses import, for instance — and those were missing from the build, so a correct harness could be rejected for an import that does not resolve. Materializing gets the agent's actual filesystem view, which is what we want to compile.

It also lets a fair amount of machinery go: the harnesses keep their certora/harnesses paths, so the scratch directory, its same-depth requirement (so ../../src/... imports resolved) and its cleanup all disappear, and the diagnostics no longer need rewriting before they go back to the agent.

Measured on the project this came from (353MB, 12,286 files):

materialize	~6.5s
forge build after it	1.4s (rejecting) / 3.2s (accepting)

Notably forge reuses the copied cache/ and out/ — its cache keys are project-relative, so they survive the copy and no dependency graph is recompiled. Both cases re-verified end to end through a materialized copy: the original harness set is rejected with the full should be marked as abstract diagnostic, the repaired set is accepted.

One risk worth naming: the copy lands in the container's temp space, and it scales with the project. This one is 353MB; a project whose out/ carries build_info can be several GB, and the copy happens once per repair attempt. If that turns out to bite, the narrower fix is to materialize only what the VFS holds plus what the harnesses transitively import, rather than the whole tree.

[jtoman]

one major nit

[jtoman]

pydantic schema is cheap and easier to read imo

[shellygr]

Claude answers: agreed, done in 5ab7839 — the parsing is now a two-model schema and the digging is gone:

class ForgeDiagnostic(BaseModel):
    severity: str
    message: str = ""
    formatted_message: str = Field(default="", alias="formattedMessage")

    @property
    def rendered(self) -> str:
        return self.formatted_message or self.message


class ForgeReport(BaseModel):
    errors: list[ForgeDiagnostic] = Field(default_factory=list)

    @property
    def compile_errors(self) -> list[str]:
        return [d.rendered for d in self.errors if d.severity == "error"]

Call site is ForgeReport.model_validate_json(stdout) plus one except ValidationError. That also collapses three separate "not a report" returns (JSON decode error, non-dict, missing key) into the one place, and the two facts worth knowing about this format — that errors carries warnings too, and that the exit code says nothing because forge exits 0 either way — now sit on the models rather than in a comment above the .get chain.

[jtoman]

shouldn't this be async? you'll need to use an async result tool (there's one floating around you can use...) but that should be fine...

[shellygr]

Claude answers: it should, and it now is — 5ab7839. You were right that it mattered: both halves of this check block, the project copy as much as the compile, and it sat on the event loop for the whole of each attempt.

Found the one you meant — AsyncResultTool in composer/spec/natspec/async_result.py, as used by interface_gen/stub_gen. The validator is a coroutine now:

class HarnessResultTool(AsyncResultTool[HarnessAgentResult], WithInjectedState[GenerationState]):
    @override
    async def validate_result(self, res: HarnessAgentResult) -> str | None:
        ...
        async with _materialized(mat, self.state) as project_dir:
            compile_errors = await _compile_check(project_dir, harness_paths)

WithInjectedState on top of it because the validator needs the VFS — for the existence checks and for the materialization. That combination had no precedent in the tree, so I checked what the model actually sees rather than assuming: the tool's args are ['value'], state and tool_call_id are injected and hidden, a rejection returns the message without setting result, and an acceptance stores the validated model. There is a test pinning that now, since a silent change there would break the phase.

The copy goes through asyncio.to_thread around the accessor's context manager — the same shape materializing_project uses in composer/spec/source/prover.py for the prover's project copies — and forge runs via create_subprocess_exec with wait_for for the timeout.

Re-verified end to end against the source of the run this came from, through a materialized copy: the original harness set is rejected with the full diagnostic (materialize 4.3s, forge 1.8s), the repaired set is accepted (3.9s, 15.6s — a cold compile of all 16). Suite 511 passed, pyright clean.

[jtoman]

one nit about finding a new home for a class you're using, and a suggestion for a future API improvement, neither of which block the landing of this PR. ship it

[jtoman]

this is common enough now, and the materialize is slow enough, we should really add an accessor.amaterialize. This VFS API was designed before we went full async...

[shellygr]

I'll make an issue..

[jtoman]

worth moving out of this very specific package imo.