Let console-codegen take several spec files - #155
Draft
shellygr wants to merge 1 commit into
Draft
Conversation
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.