Express the source-tool read filter as a predicate

composer/cli/natspec_startup.py

@@ -3,7 +3,7 @@
 
 from langchain_core.tools import BaseTool
 
-from graphcore.tools.vfs import DirBackend, FSBackend, Materializer, fs_tools_layered
+from graphcore.tools.vfs import GlobalExcludeArg, DirBackend, FSBackend, Materializer, fs_tools_layered
 
 from composer.spec.gen_types import PartialTemplate
 from composer.spec.system_model import Application, FromSourceApplication
@@ -74,7 +74,7 @@ def build_mental_model(
 
 def make_source_factory(
     source_root: pathlib.Path | None,
-    forbidden_read: str | None,
+    forbidden_read: GlobalExcludeArg,
 ):
     """Build the ``source_factory`` closure the pipeline calls at each phase.
 

composer/cli/tui_pipeline.py

@@ -4,6 +4,7 @@
 ``existing`` (verify-as-is from source) lives in ``console_autoprove``.
 """
 
+from graphcore.tools.vfs import GlobalExcludeArg
 import composer.bind as _
 
 import argparse
@@ -32,7 +33,7 @@
 from composer.llm.registry import get_provider_for
 from composer.spec.natspec.pipeline import run_natspec_pipeline
 from composer.spec.natspec.run_tags import NatspecRunTags
-from composer.spec.util import FS_FORBIDDEN_READ
+from composer.spec.util import fs_forbidden_read
 from composer.spec.cvl_research import DEFAULT_CVL_AGENT_INDEX_NS
 from composer.ui.tool_display import async_tool_context
 
@@ -52,7 +53,7 @@ class PipelineArgs(ModelOptions, RAGDBOptions, Protocol):
     cache_ns: str | None
     memory_ns: str | None
     source_root: str | None
-    forbidden_read: str | None
+    forbidden_read: GlobalExcludeArg
     prover_conf: str | None
     output_root: str | None
     interactive: bool
@@ -92,7 +93,7 @@ async def _main() -> int:
     )
     parser.add_argument(
         "--forbidden-read", default=None,
-        help="Regex of paths source tools may not read. Defaults to FS_FORBIDDEN_READ "
+        help="Regex of paths source tools may not read. Overrides the default predicate "
              "when source-root is set.",
     )
     parser.add_argument(
@@ -150,7 +151,7 @@ async def _main() -> int:
 
         sort = "update" if source_root_path is not None else "greenfield"
         forbidden_read = (
-            args.forbidden_read or (FS_FORBIDDEN_READ if source_root_path else None)
+            args.forbidden_read or (fs_forbidden_read if source_root_path else None)
         )
 
         thread_id = f"pipeline_{uuid.uuid4().hex[:12]}"

composer/foundry/entry.py

@@ -29,7 +29,7 @@
 from composer.io.thread_logging import RunDataLogger
 from composer.rag.db import FOUNDRY_DEFAULT_CONNECTION, PostgreSQLRAGDatabase
 from composer.spec.context import SourceFields
-from composer.spec.util import FS_FORBIDDEN_READ
+from composer.spec.util import fs_forbidden_read
 
 from composer.foundry.artifacts import FoundryArtifactStore
 from composer.foundry.env import build_foundry_env
@@ -160,7 +160,7 @@ async def runner(fact: HandlerFactory[FoundryPhase, None]) -> FoundryPipelineRes
             env = build_foundry_env(
                 model_provider=staged.llm_models,
                 project_root=staged.source.project_root,
-                forbidden_read=FS_FORBIDDEN_READ,
+                forbidden_read=fs_forbidden_read,
                 rag_db=foundry_rag_db,
                 store=staged.conns.indexed_store,
                 source_question_ns=source_question_ns,

composer/foundry/env.py

@@ -19,6 +19,7 @@
 """
 
 
+from graphcore.tools.vfs import GlobalExcludeArg
 from langgraph.store.base import BaseStore
 from langgraph.types import Checkpointer
 
@@ -36,7 +37,7 @@ def build_foundry_env(
     *,
     model_provider: ModelProvider,
     project_root: str,
-    forbidden_read: str,
+    forbidden_read: GlobalExcludeArg,
     rag_db: ComposerRAGDB,
     store: BaseStore,
     source_question_ns: tuple[str, ...],

composer/pipeline/cli.py

@@ -39,7 +39,7 @@
 if TYPE_CHECKING:
     from sentence_transformers import SentenceTransformer
 
-from composer.spec.util import FS_FORBIDDEN_READ
+from composer.spec.util import fs_forbidden_read
 import hashlib
 
 
@@ -169,7 +169,7 @@ async def cli_pipeline[P: enum.Enum, H](
     init_source = SourceFields(
         relative_path=relative_path,
         contract_name=SolidityIdentifier(contract_name),
-        forbidden_read=FS_FORBIDDEN_READ,
+        forbidden_read=fs_forbidden_read,
         project_root=str(project_root)
     )
 

composer/spec/context.py

@@ -7,6 +7,7 @@
 be passed explicitly to agents that need it.
 """
 
+from graphcore.tools.vfs import GlobalExcludeArg
 from dataclasses import dataclass
 from typing import Annotated, Callable, overload, Awaitable
 
@@ -44,7 +45,7 @@ class SourceFields:
     project_root: str
     contract_name: SolidityIdentifier
     relative_path: str
-    forbidden_read: str
+    forbidden_read: GlobalExcludeArg
 
 @dataclass
 class SourceCode(SystemDoc, SourceFields):

composer/spec/source/autoprove_common.py

@@ -29,7 +29,7 @@
 from composer.ui.autoprove_app import AutoProvePhase
 from composer.io.thread_logging import RunDataLogger
 
-from composer.spec.util import FS_FORBIDDEN_READ
+from composer.spec.util import fs_forbidden_read
 from composer.io.multi_job import HandlerFactory
 
 _logger = logging.getLogger(__name__)
@@ -134,7 +134,7 @@ async def callback(
             source_env = build_source_env(
                 models=staged.llm_models,
                 db=rag_db,
-                forbidden_read=FS_FORBIDDEN_READ,
+                forbidden_read=fs_forbidden_read,
                 kb_ns=DEFAULT_KB_NS,
                 root=staged.source.project_root,
                 store=staged.conns.indexed_store,

composer/spec/source/source_env.py

@@ -6,7 +6,7 @@
 from langchain_core.language_models.chat_models import BaseChatModel
 
 from graphcore.graph import Builder
-from graphcore.tools.vfs import fs_tools
+from graphcore.tools.vfs import GlobalExcludeArg, fs_tools
 
 from composer.spec.tool_env import BaseSourceTools
 from composer.spec.services import build_rag_tool_env, RAGInputs
@@ -22,7 +22,7 @@ class _BaseSourceTools():
 
 def build_basic_source_tools(
     root: str,
-    forbidden_read: str,
+    forbidden_read: GlobalExcludeArg,
 ) -> BaseSourceTools:
     return _BaseSourceTools(
         tuple(fs_tools(fs_layer=root, forbidden_read=forbidden_read, cache_listing=False))
@@ -74,7 +74,7 @@ class _ExplorerEnv:
 
 class SourceParams(RAGInputs):
     root: str
-    forbidden_read: str
+    forbidden_read: GlobalExcludeArg
     source_question_ns: tuple[str, ...]
 
 

composer/spec/util.py

@@ -3,7 +3,7 @@
 import os
 import re
 import uuid
-from pathlib import Path
+from pathlib import Path, PurePath
 from typing import Iterator
 
 from composer.spec.gen_types import CERTORA_DIR
@@ -61,7 +61,63 @@ def temp_certora_file(
     finally:
         os.unlink(tgt)
 
-FS_FORBIDDEN_READ = r"(^lib/.*)|(^\.certora_internal.*)|(^\.git.*)|(^test/.*)|(^emv-.*)|(.*\.json$)|(^node_modules/.*(?<!\.sol)$)"
+# Prover working directories and VCS internals. Withheld whole, Solidity included:
+# their .sol is a verbatim copy of a contract already readable at its canonical path,
+# since each certoraRun invocation materializes its own ``inputs/.certora_sources/**``.
+# Analysis that wants a specific report's copy reaches it through a VFS scoped to that
+# report, not through the project source surface.
+_WITHHELD_WHOLE_DIRS = frozenset({".git", ".certora_internal"})
+
+# Prover report directories, named ``emv-<n>-<verdict>-<contract>``. Root-only: these
+# are created where certoraRun was invoked, which for this pipeline is the project root.
+_REPORT_DIR_PREFIX = "emv-"
+
+# Directories that carry source alongside content of no use to a reader — vendored
+# dependencies, scaffolding, build output. Matched at any depth, since a package's own
+# dependency tree nests as readily as the project's own sits at the root.
+_NON_SOLIDITY_DIRS = frozenset({"node_modules", "lib", "test", "dist"})
+
+# Machine-generated files. Beyond being unreadable, a minified bundle or a packed data
+# blob holds its content on very few very long lines — a single line can span megabytes
+# — and a content grep reports whole matching lines.
+_GENERATED_SUFFIXES = frozenset({".json", ".map", ".dat"})
+
+# Every separator/marker pairing a bundle name is written with in practice, so that
+# ``str.endswith`` can take the whole tuple in one call: ``.min`` / ``-min`` / ``_min``
+# and the same three for ``bundle``.
+_BUNDLE_STEM_SUFFIXES = tuple(
+    sep + marker for sep in (".", "-", "_") for marker in ("min", "bundle")
+)
+
+
+def _is_generated_bundle(path: PurePath) -> bool:
+    """``vendor.min.js`` / ``app-bundle.js`` / ``app_bundle.js``, but not a hand-written
+    ``bundle.js``: the marker has to be a suffix of the name, not the whole of it."""
+    return path.suffix == ".js" and path.stem.endswith(_BUNDLE_STEM_SUFFIXES)
+
+
+def fs_forbidden_read(path: PurePath) -> bool:
+    """True to withhold *path* from the agent's source tools (``list_files`` /
+    ``get_file`` / ``grep_files``). Paths are project-root-relative.
+
+    Solidity is never withheld from the project source surface: any .sol can turn out
+    to be part of the verification target, since the conf's ``packages`` remappings
+    resolve into vendored dependency trees and a stock Foundry layout keeps real
+    contracts in ``lib/`` and ``test/``. The one exception is the whole-withheld
+    directories, which is why they are tested before the carve-out.
+    """
+    parts = path.parts
+    if _WITHHELD_WHOLE_DIRS.intersection(parts):
+        return True
+    if parts and parts[0].startswith(_REPORT_DIR_PREFIX):
+        return True
+    if path.suffix == ".sol":
+        return False
+    return (
+        bool(_NON_SOLIDITY_DIRS.intersection(parts))
+        or path.suffix in _GENERATED_SUFFIXES
+        or _is_generated_bundle(path)
+    )
 
 def uniq_thread_id(prefix: str) -> str:
     suff = uuid.uuid4().hex[:16]

pyproject.toml

@@ -15,7 +15,7 @@ authors = [
 ]
 
 dependencies = [
-    "graphcore @ git+ssh://git@github.com/Certora/graphcore.git@932cf73faad68266f5dd8b4d6943e82d2b3130ae",
+    "graphcore @ git+ssh://git@github.com/Certora/graphcore.git@c8b3ae5615c648d47978006ae9d70ac4e6a2add4",
     "aiohttp>=3.13",
     "attrs>=26.1",
     "Jinja2>=3.1",

tests/test_design_doc_finder.py

@@ -39,7 +39,7 @@
 from composer.input.files import InMemoryTextFile
 from composer.spec.context import WorkflowContext, SourceFields
 from composer.spec.service_host import ModelProvider
-from composer.spec.util import FS_FORBIDDEN_READ
+from composer.spec.util import fs_forbidden_read
 from composer.templates.loader import load_jinja_template
 from composer.ui.autoprove_app import AutoProvePhase
 from composer.ui.autoprove_console import AutoProveConsoleHandler
@@ -110,7 +110,7 @@ def _source(
         project_root=project_root,
         contract_name=cast(Any, contract_name),
         relative_path=relative_path,
-        forbidden_read=FS_FORBIDDEN_READ,
+        forbidden_read=fs_forbidden_read,
     )
 
 
@@ -198,7 +198,7 @@ async def test_finder_graph_selects_the_design_doc(tmp_path):
     (tmp_path / "design.md").write_text("# Design\nThe counter must never decrease.\n")
     (tmp_path / "README.md").write_text("# Build\nRun `forge build`.\n")
 
-    tools = build_basic_source_tools(str(tmp_path), FS_FORBIDDEN_READ).base_source_tools
+    tools = build_basic_source_tools(str(tmp_path), fs_forbidden_read).base_source_tools
 
     # Script: inventory -> read the design doc -> submit the result.
     responses: list[BaseMessage] = [
@@ -232,7 +232,7 @@ async def test_finder_graph_can_read_a_pdf_via_read_document(tmp_path):
     user message) and the graph completes with that file selected."""
     (tmp_path / "spec.pdf").write_bytes(b"%PDF-1.4 the protocol specification")
 
-    tools = list(build_basic_source_tools(str(tmp_path), FS_FORBIDDEN_READ).base_source_tools)
+    tools = list(build_basic_source_tools(str(tmp_path), fs_forbidden_read).base_source_tools)
     tools.append(read_document_tool(cast(Any, _StubUploader()), str(tmp_path)))
 
     responses: list[BaseMessage] = [
@@ -266,7 +266,7 @@ async def test_read_document_keeps_tool_results_adjacent_under_parallel_calls(tm
     (tmp_path / "spec.pdf").write_bytes(b"%PDF-1.4 the spec")
     (tmp_path / "README.md").write_text("# Build\nrun make\n")
 
-    tools = list(build_basic_source_tools(str(tmp_path), FS_FORBIDDEN_READ).base_source_tools)
+    tools = list(build_basic_source_tools(str(tmp_path), fs_forbidden_read).base_source_tools)
     tools.append(read_document_tool(cast(Any, _StubUploader()), str(tmp_path)))
 
     responses: list[BaseMessage] = [

tests/test_fs_forbidden_read.py

@@ -0,0 +1,83 @@
+"""Tests for ``fs_forbidden_read``, the predicate gating what the agent's source tools
+(``list_files`` / ``get_file`` / ``grep_files``) are allowed to read.
+
+Two properties matter, and they pull in opposite directions. Solidity always stays
+readable, wherever it sits: the conf's ``packages`` remappings resolve into vendored
+dependency trees, and a stock Foundry layout keeps real contracts in ``lib/`` and
+``test/``. Machine-generated output stays unreadable, because a minified bundle carries
+megabytes on a single line and a content grep reports whole matching lines — one call can
+then exceed the model's context window.
+
+graphcore hands the predicate a ``PurePosixPath`` of a project-root-relative path, so
+that is how it is exercised here.
+"""
+
+from pathlib import PurePosixPath
+
+from composer.spec.util import fs_forbidden_read
+
+
+def can_read(path: str) -> bool:
+    """Mirror graphcore's check: readable when the predicate does not exclude."""
+    return not fs_forbidden_read(PurePosixPath(path))
+
+
+def test_contract_under_analysis_is_readable() -> None:
+    assert can_read("pkg/sub/src/Widget.sol")
+
+
+def test_solidity_is_readable_wherever_it_sits() -> None:
+    # A `packages` remapping resolves into a vendored tree, at whatever depth.
+    assert can_read("pkg/sub/node_modules/@vendor/artifacts/contracts/src/IThing.sol")
+    assert can_read("node_modules/@vendor/contracts/IThing.sol")
+    # A stock Foundry layout keeps dependencies in lib/ and contracts in test/.
+    assert can_read("lib/openzeppelin-contracts/contracts/token/ERC20.sol")
+    assert can_read("test/Widget.t.sol")
+    assert can_read("pkg/sub/lib/forge-std/src/Test.sol")
+    assert can_read("pkg/sub/test/Harness.sol")
+    # Even a name that collides with a generated-output rule stays readable.
+    assert can_read("apps/dist/Widget.sol")
+
+
+def test_non_solidity_in_a_dependency_tree_is_not_readable_at_any_depth() -> None:
+    assert not can_read("node_modules/pkg/index.js")
+    # Nested dependency trees are the common case in a monorepo, and the reason this rule
+    # cannot be bound to the project root.
+    assert not can_read("pkg/sub/node_modules/pkg/index.js")
+    assert not can_read("pkg/sub/node_modules/pkg/README.md")
+    assert not can_read("pkg/sub/lib/forge-std/README.md")
+    assert not can_read("test/fixtures/expected.txt")
+
+
+def test_generated_bundles_and_data_blobs_are_not_readable() -> None:
+    # Built web output: the payload that made a single grep exceed the context window.
+    assert not can_read("apps/dist/index.html")
+    assert not can_read("apps/dist/assets/params.dat")
+    # Bundles are named with any of the three separators in practice.
+    assert not can_read("shared/app_bundle.js")
+    assert not can_read("shared/app-bundle.js")
+    assert not can_read("shared/app.bundle.js")
+    assert not can_read("shared/vendor.min.js")
+    assert not can_read("shared/app.js.map")
+    assert not can_read("package.json")
+
+
+def test_prover_working_directories_are_withheld_whole_including_solidity() -> None:
+    # Their .sol is a verbatim copy of a contract already readable at its canonical
+    # path — each certoraRun invocation leaves another one — so the Solidity carve-out
+    # deliberately does not reach here.
+    assert not can_read("emv-1-verified-Widget/inputs/.certora_sources/src/Widget.sol")
+    assert not can_read(".certora_internal/abc123/.certora_sources/src/Widget.sol")
+    assert not can_read("pkg/sub/.certora_internal/abc123/.certora_sources/src/Widget.sol")
+    assert not can_read(".certora_internal/autoProve/run.log")
+    assert not can_read(".git/config")
+    assert not can_read("pkg/sub/.git/config")
+
+
+def test_ordinary_sources_are_not_caught_by_the_generated_output_rules() -> None:
+    # The bundle/minified rules key on a separator before the marker, so hand-written
+    # files whose names merely end in those words stay readable.
+    assert can_read("apps/src/bundle.js")
+    assert can_read("apps/src/min.js")
+    assert can_read("services/daemon.mjs")
+    assert can_read("README.md")