[DEV] Compile-check generated harnesses before accepting them - #142
Merged
Conversation
The harness generation prompt promises the agent that its harnesses are type-checked on delivery and that compiler errors come back for repair, but the check behind that promise never ran: it was gated on `if False`, because invoking bare `solc` on the harness files cannot resolve a project's remappings, include paths or compiler settings. A harness that does not compile is therefore only discovered by AutoSetup, one phase later, where it is misread as a compilation problem to work around rather than a source error to repair -- and the run dies with everything downstream of it discarded. Check them with the project's own build instead: write the candidates to a scratch directory at the same depth as `certora/harnesses` (so their relative imports resolve identically) and run `forge build --json` on them, which reports diagnostics with a severity field and reuses the artifacts the build phase already produced. Error-severity diagnostics are handed back to the agent against the paths it knows; the scratch directory does not outlive the check. Projects with no foundry build, or a forge that never gets as far as a report, are accepted unchecked as before. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Building the delivered files in a scratch directory inside the live project checks something subtly different from what the agent produced: the VFS may hold files it wrote but did not deliver -- a shared base contract the harnesses import, say -- and those would be missing from the build, failing harnesses that are in fact correct. It also puts a directory into the project tree for the duration of the check. Materialize the VFS instead and build there. The harnesses keep their `certora/harnesses` paths, so the diagnostics need no rewriting and the scratch directory, its depth-matching requirement and its cleanup all go away. Cost on a 353MB / 12k-file project: ~6.5s to materialize, and forge reuses the copied build cache rather than recompiling the dependency graph. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Mirror of #129 onto the
devbleeding-edge branch.Source branch:
shelly/harness-compile-gate. This branch is that head merged forward withdev; #129 itself is untouched and still targetsmaster.Per the
devbranch policy this merges without review oncepyrightandpytestare green.