Check that declared source paths exist during component analysis by shellygr · Pull Request #202 · Certora/AutoProver

shellygr · 2026-09-02T09:28:37Z

What

The path fields on SourceExplicitContract, SourceExternalActor and ExistingFromSource are
written by the component-analysis agent. Nothing checked them against the filesystem.
validate_solidity_connectivity covered names, duplicates and the interaction graph, and it was
typed over BaseApplication with no project root to check anything against.

So a declared path that resolves to nothing travels a long way before anyone notices. It goes
through run_setup_part1's name_to_path, into the transitive closure, into extra_files in
run_autosetup_phase, and finally into the AutoSetup subprocess argv, where parse_contract_files
raises File ... does not exist. By then an hour has passed and several analysis and bug-analysis
phases have run.

The shape that prompted this: a repository whose build project sits one or more directories below
the repository root. Paths are project-root-relative, so every declared path has to carry that
leading directory. A path assembled from an import statement or from a build tool's source
directory instead of from the agent's own file-tool output loses it, and every contract in the
submission loses it the same way.

How

The validator takes a third project_root: Path | None and checks the declared paths inside its
existing single pass over components. Path complaints join the same accumulated message as the
graph ones, so a submission that is wrong in both ways is corrected in one retry instead of two.
project_root threads through Ecosystem.validate_analysis, which follows the existing
locate_main precedent of handing ecosystem callables the run's facts. Solana and Soroban take an
ignored parameter; nothing in their models carries a source path.

Containment is lexical, meaning relative and never stepping up out of the root. Resolving instead
would follow symlinks, and the forbidden-read predicate deliberately keeps .sol readable under
lib/ and node_modules/, which are routinely symlinked. The agent is entitled to name a file
there and has no way to restate it as a non-symlinked path, so a resolving check would reject it
with no way to comply. There is a test pinning that.

The error says where to look instead. One walk of the tree collects readable files carrying the
declared name, narrowed to those whose path ends with the declared path, so the dropped-directory
case names exactly one real file rather than reporting "not found". One walk covers every bad path
in the submission, and wholly withheld directories are pruned during descent rather than filtered
out afterwards, because this runs while the agent waits on its retry.

Cache hits get the same check. root_cache_key is
sha256(project_root | doc_hash | relative_path | contract_name), which covers neither the source
tree nor the rules in force, and the cloud namespaces the cache per user and repository. Without
this, a model written before the check existed is replayed unvalidated on every rerun and the gate
never fires at all. An entry that fails validation is stale, so it is re-derived and the existing
cache_put replaces it.

The prompt and the path field descriptions now state the convention the validator enforces. They
reject nothing on their own; they say what the check requires.

Scope note for reviewers

SourceExternalActor.path is checked too, which is wider than the failure above. It is the same
class of unchecked agent-written string and it reaches the summarizer prompt. The error offers
"omit the path instead" as the remedy, and an actor with no path is passed over silently
downstream, so a repository that passes today can start reporting a validation error. That is
intended, not a regression.

Testing

tests/test_solidity_component_paths.py is new: 17 tests over acceptance, a path missing its
leading directory (asserting the hint names the one real file), several files sharing a name, no
file of that name anywhere, a directory, absolute and escaping paths, a path under a withheld
directory, a symlinked dependency being accepted, several bad paths arriving in one message, graph
errors and path errors arriving together, the external actor with and without a path,
project_root=None, greenfield, and FromSourceApplication where the existing contract is checked
and the fresh one is not. Two more cover the cache branch in both directions.

tests/test_analysis_input_phrase.py gained rendering assertions for the two path bullets and the
omit-the-path clause. tests/test_pipeline_overlap.py now asserts the driver forwards a real
project root.

Each new test was checked by breaking the code it covers and confirming it fails.

Targeted run: 91 passed. pyright composer/ analyzer sanity_analyzer certora_autosetup: 0 errors.

Review round

forbidden_read now comes off the pipeline input rather than the module-level fs_forbidden_read,
so the check asks the question the run's own file tools answer. It threads beside project_root
through Ecosystem.validate_analysis, and natspec carries it on its MentalModel. Normalizing the
two surface forms of a GlobalExcludeArg uses make_exclude_pred, exported from graphcore in
Certora/graphcore#37, now merged, and the pin sits on graphcore master.

The directory prune in the relocation walk stays on fs_withheld_subtree, which is a walk-cost
measure over prover and VCS scratch rather than a readability rule. A prune cannot be derived from
an arbitrary exclusion: lib/ is excluded whole while the .sol under it stays readable. Four new
tests pin the split, including the regex form of forbidden_read and a hint that must not name a
file the run withholds.

Advancing the graphcore pin also brings its token-usage accounting fix, so the fake message in
tests/test_token_usage.py carries usage_metadata, whose input total includes the cache buckets.

The path fields on the source-carrying model types are written by the component-analysis agent and were never checked against the filesystem. A path that resolves to nothing travelled through name_to_path, the transitive closure and extra_files before AutoSetup's parse_contract_files raised on it, an hour and several phases after it was written. validate_solidity_connectivity now takes the project root and checks each declared path in its existing pass over components, so a submission wrong in both its graph and its paths comes back as one message. Cache hits are held to the same check, since the analysis cache key covers neither the source tree nor the rules in force. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

jtoman · 2026-09-02T22:04:43Z

+    if fs_forbidden_read(PurePath(declared)):
+        return _PathFault.WITHHELD


I'm confused how this happened?

Claude answers: I don't have a case of the model actually doing it. The branch is there for consistency with the hints: the walk behind them prunes .certora_internal and the report directories, so a path into one is something the validator would never suggest, and accepting it would point AutoSetup at a prover's own copy of a contract that is readable at its canonical path anyway. Every prover run leaves such a copy behind, so the files really are there. tests/test_solidity_component_paths.py covers it.

jtoman · 2026-09-02T22:07:26Z

+    found: dict[str, list[str]] = {name: [] for name in names}
+    for dirpath, dirnames, filenames in os.walk(root):
+        rel_dir = Path(dirpath).relative_to(root)
+        dirnames[:] = [d for d in dirnames if not fs_withheld_subtree(rel_dir / d)]


I was today years old when I learned you could control the recursion behavior of os.walk by just mutating dirnames. This language is insane dude.

Claude answers: It is the only way to prune a directory without walking it first, which is what this loop is after.

jtoman · 2026-09-02T22:10:32Z

+    name = PurePosixPath(declared).name
+    candidates = same_named[name]
+    tail_matches = [c for c in candidates if c.endswith("/" + declared)]


Wait, I'm confused. This is basically finding candidates where the LLM clearly forgot a leading directory?

Claude answers: Yes. Candidates start as every readable file with that base name, and the tail match keeps the ones whose path ends with what was declared. That is the dropped-leading-directory case, and it usually leaves exactly one file for the agent to copy.

jtoman · 2026-09-02T22:13:59Z

+        return _PathFault.DIRECTORY
+    if not candidate.is_file():
+        return _PathFault.MISSING
+    if fs_forbidden_read(PurePath(declared)):


FWIW, we should be using the forbidden_read on SourceFields which makes up the input to the pipeline. fs_forbidden_read is just the default (that we happen to use always, so its worth considering whether we need to keep forbidden_read as a separate part of the input)

Claude answers: Done in 4f7c2f1. The validator takes the run's forbidden_read and normalizes it with make_exclude_pred, which I exported from graphcore in Certora/graphcore#37, so the regex and the callable form are read the way the tools read them. The pin here points at that branch commit until #37 merges. The directory prune in the walk stays on fs_withheld_subtree: a prune cannot come from an arbitrary exclusion, since lib/ is excluded whole while the .sol under it stays readable.

Claude answers: graphcore#37 is merged, so the pin here now points at graphcore master (2177f57) instead of the branch commit.

jtoman · 2026-09-02T22:16:09Z

 async def run_component_analysis[T: BaseApplication](
    ty: type[T],
    child_ctxt: WorkflowContext[T],
    input: SystemDoc | SourceCode | None,


FWIW, this is the input field which holds the source field to use.

jtoman · 2026-09-02T22:16:44Z

    extra_input: list[str | dict],
    expected_main_id: SourceIdentifier | None = None,
    *,
+    project_root: Path | None,


doesn't this duplicate the data available on SourceCode? When will this be non-none and input !is SourecCode?

Claude answers: They come apart in the natspec from-source workflow, which calls this with input a SystemDoc and a real root off mental_model.source_root (composer/spec/natspec/system_analysis.py). That workflow is generating contracts, so it has no contract_name or relative_path and cannot hand over a SourceCode. If you would rather it were one object, the shape is splitting (project_root, forbidden_read) out of SourceFields into a base both callers pass. Say so and I will do that instead.

oh. hmmm. Heck! okay then

jtoman · 2026-09-02T22:17:14Z

+
+    ``project_root`` is the tree the validator resolves any source paths the model declares
+    against; it is required (not defaulted) so a new call site has to say what the model's paths
+    mean, and is ``None`` only when the run has no source tree.


which is also the semantics (if you will) of input == SystemDoc or input == None. I think we're duplicating data.

Claude answers: Same as the parameter above: natspec from-source has a root and no SourceCode, so the two are not the same condition.

The path check called `fs_forbidden_read`, the Solidity default, instead of the predicate the run actually serves its source tree through. A run that narrows or widens that rule got a validator disagreeing with its own file tools about what counts as a source file. The `forbidden_read` now travels off the pipeline input beside the project root, normalized by graphcore's `make_exclude_pred` so both surface forms are read the way the tools read them. The prune in the relocation walk stays on `fs_withheld_subtree`. It keeps prover and VCS scratch off the walk for cost, and a prune cannot be derived from an arbitrary exclusion: `lib/` is excluded whole while the .sol under it stays readable. Advancing the graphcore pin to pick up `make_exclude_pred` also brings its token-usage accounting fix, so the fake message in test_token_usage carries `usage_metadata`, whose input total includes the cache buckets. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

master's own fix to the token-usage fake message wins; the copy of it on this branch, written while the graphcore pin was being advanced, is dropped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

jtoman · 2026-09-04T18:58:19Z

    extra_input: list[str | dict],
    expected_main_id: SourceIdentifier | None = None,
    *,
+    project_root: Path | None,


oh. hmmm. Heck! okay then

graphcore#37 is merged, so the submodule and the pin move off the branch commit they sat on and onto master. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

shellygr requested a review from jtoman September 2, 2026 20:25

jtoman requested changes Sep 2, 2026

View reviewed changes

shellygr and others added 2 commits September 4, 2026 21:48

Merge master into the declared-path validation branch

8863998

master's own fix to the token-usage fake message wins; the copy of it on this branch, written while the graphcore pin was being advanced, is dropped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

shellygr requested a review from jtoman September 4, 2026 18:55

jtoman approved these changes Sep 4, 2026

View reviewed changes

shellygr and others added 2 commits September 4, 2026 23:45

Point the graphcore pin at master

660889f

graphcore#37 is merged, so the submodule and the pin move off the branch commit they sat on and onto master. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Merge branch 'master' into shelly/validate-component-paths

8774b8d

shellygr merged commit b733ca0 into master Sep 4, 2026
4 checks passed

shellygr deleted the shelly/validate-component-paths branch September 4, 2026 20:50

		if fs_forbidden_read(PurePath(declared)):
		return _PathFault.WITHHELD

Uh oh!

Conversation

shellygr commented Sep 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What

How

Scope note for reviewers

Testing

Review round

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

shellygr commented Sep 2, 2026 •

edited

Loading