Let console-codegen take several spec files - #155
Draft
shellygr wants to merge 10 commits into
Draft
Conversation
`temp_certora_file` yields a path already relative to the project root, so it
carries the `certora/` segment (its docstring: "callers use it verbatim (no
`certora/` prefixing)"). `ConfigurationBuilder._build_to` prefixed it a second
time and yielded `<root>/certora/certora/run_<uid>.conf`, a path nothing ever
wrote to, so every natspec typecheck died with:
read_from_conf_file: /tmp/tmpXXXXXXXX/certora/certora/run_YYYY.conf: not found
`publish` is gated on a passing typecheck, so greenfield natspec runs could
never emit a spec: the authoring agents produced complete, judge-approved CVL,
burned their remaining turns retrying, and gave up. The pipeline still wrote
the interface and the stub, which made the failure look like missing specs
rather than a broken backend.
The sibling call in the same `with` block, `with_verify(spec_file=...)`, already
uses the yielded path verbatim.
Adds a regression test asserting `build_to` yields a path that exists and sits
under exactly one `certora` segment.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`with_verify` re-prefixed `certora/` onto a spec path that already carried it,
so the conf's `verify` attribute read
<Contract>:certora/certora/generated_<uid>.spec
The Certora CLI validates that path against the process CWD (which typecheck.py
sets to the project root), so it rejected every spec with
attribute/flag 'verify': file certora/certora/generated_<uid>.spec not found
This is the same mistake as the conf-location bug in the previous commit, one
layer up: fixing only that one moved the failure from "conf not found" to
"spec not found" without unblocking publish.
Widens the regression test to assert the invariant both bugs broke — every path
the conf hands to the CLI must resolve, from the project root, to a file on
disk. The test now fails on either bug alone.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Certora's scene assembly requires every entry in the conf's `files` to compile
to bytecode. An interface never does, so one interface entry fails the build
for every spec authored in that session:
Contract IFoo has no bytecode. It may be caused because the contract is
abstract, or is missing constructor code.
The pipeline registers only stubs, but the CVL-authoring agent registered the
interface too — reasonably, since its spec references it and
`register_verification_file` invited "any contract source the spec references".
There is no unregister tool, so a session poisoned itself irrecoverably: the
agent's own diagnosis after its sixth rejected publish was "blocking error is
scene assembly of the pre-registered interface-only file".
The registration also outlived the run that made it. FILES_NS is keyed by
document digest and not by cache namespace, so re-running the same document
under a fresh `--cache-ns` reused the poisoned entry. Hence two guards:
`register` refuses these paths, and `read_all` filters them so entries written
before this commit stay out of the conf.
The interfaces are in the scene regardless, via the stubs' imports. Verified by
running the real typecheck gate against a generated interface + stub with
`rule sanity { assert true; }`: with the interface excluded from `files`, the
gate passes.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`_compile_stub` gates every stub update and trusted solc's exit status. An
`abstract contract` satisfies that happily: solc returns 0 and emits no
bytecode. Certora's scene assembly then rejects the verification unit —
Contract StreamShareSplitter has no bytecode. It may be caused because the
contract is abstract, or is missing constructor code.
— failing every subsequent typecheck in the session. `publish` is gated on the
typecheck, so nothing the CVL author does afterwards can recover: the bad stub
is already in the VFS and the spec is not what is wrong.
This is not hypothetical. A registry agent asked for storage fields and got
back `abstract contract StreamShareSplitter is IStreamShareSplitter`, which the
validator accepted. All four components then produced judge-approved specs that
could never be published, while the artifact dumped at the end was the pristine
concrete stub from generation — so the failure was invisible in the output.
Ask solc for the bytecode via --combined-json and require it to be non-empty.
The rejection message names the two ways a contract ends up without bytecode so
the agent can act on it within its retry loop.
Note the neighbouring case is already safe: a contract that inherits a function
it does not implement is a hard solc error ("should be marked as abstract"), so
the exit-status path catches that one. Only explicit `abstract` slipped through.
Both are pinned by tests.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The workflow is already plumbed for N specs (`InputData.specs`), but the CLI mapped its triad to a one-element list, so there was no way to hand it more than one -- as `upload_input`'s comment noted, no producer needed it at the time. There is one now. Natspec emits one spec per component, four for a modest contract, and each carries its own copy of the shared ERC20 ghost model. Merging them by hand means reconciling duplicate ghosts, definitions and `methods` blocks; running codegen once per spec instead yields four unrelated implementations, each satisfying one component and ignoring the rest. `spec_file` becomes `nargs="+"`. The three-argument form parses exactly as before, so existing invocations are unaffected. `vfs_path` keys the specs downstream (audit's resume artifact indexes by it), so several specs are named after their files while a single spec keeps the conventional `rules.spec` -- recorded artifacts from single-spec runs stay valid. Two specs whose file names collide are refused by name rather than silently sharing a key, which would drop one of them. 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.
Stacked on #148 (
shelly/natspec-conf-path) — retarget tomasteronce that merges.Why
InputData.specsis already a list and the workflow is plumbed for N specs, but the CLI mapped its triad to a one-element list, so nothing could hand it more than one.upload_inputsaid as much: "The legacy CLI triad is single-spec; map it to a one-element specs list… The pipeline is plumbed for N specs."There is a producer now. Natspec emits one spec per component — four for a modest contract — and each carries its own copy of the shared ERC20 ghost model. The two workarounds are both bad:
balanceByToken,allowanceByToken,sumWithdrawn), 8 definitions/functions (N,MIN_RECIPIENTS,balanceOfCVL,transferCVL,transferFromCVL,approveCVL,allowanceCVL,recordOutbound) and four separatemethodsblocks.Change
spec_filebecomesnargs="+":The three-argument form parses exactly as before, so existing invocations and scripts are unaffected.
vfs_pathkeys the specs downstream (audit's resume artifact indexes by it), so the naming is deliberate:vfs_pathsrules.spec— unchanged, so artifacts recorded by single-spec runs stay validviews.spec,withdrawal.spec, …)The collision case matters because distinct directories can hold same-named specs (
core/vault.spec,periphery/vault.spec), and sharing a key would silently drop one. Refusing beats inventing a suffix the caller never asked for.Tests
tests/test_codegen_multi_spec_input.py— 5 cases covering the parser (one spec, several specs) and the mapping (conventional name, file names, collision refused).pyteston this file plus #148's three → 11 passed.