diff --git a/composer/cli/natspec_startup.py b/composer/cli/natspec_startup.py index d2db6169..361d1b41 100644 --- a/composer/cli/natspec_startup.py +++ b/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. diff --git a/composer/cli/tui_pipeline.py b/composer/cli/tui_pipeline.py index eec4e9e6..1a5dc1f0 100644 --- a/composer/cli/tui_pipeline.py +++ b/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]}" diff --git a/composer/foundry/entry.py b/composer/foundry/entry.py index 5e9e6288..dafa19cb 100644 --- a/composer/foundry/entry.py +++ b/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, diff --git a/composer/foundry/env.py b/composer/foundry/env.py index 5f85191b..5dc9acf6 100644 --- a/composer/foundry/env.py +++ b/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, ...], diff --git a/composer/pipeline/cli.py b/composer/pipeline/cli.py index 7f496806..38e29f86 100644 --- a/composer/pipeline/cli.py +++ b/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) ) diff --git a/composer/spec/context.py b/composer/spec/context.py index 623c3f9c..0fdb0e57 100644 --- a/composer/spec/context.py +++ b/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): diff --git a/composer/spec/source/autoprove_common.py b/composer/spec/source/autoprove_common.py index 24eb0a7e..df60655d 100644 --- a/composer/spec/source/autoprove_common.py +++ b/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, diff --git a/composer/spec/source/source_env.py b/composer/spec/source/source_env.py index 1836a18e..a524dfd8 100644 --- a/composer/spec/source/source_env.py +++ b/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, ...] diff --git a/composer/spec/util.py b/composer/spec/util.py index 5ebc5f46..fd1860b0 100644 --- a/composer/spec/util.py +++ b/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/.*(?--``. 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] diff --git a/graphcore b/graphcore index 932cf73f..c8b3ae56 160000 --- a/graphcore +++ b/graphcore @@ -1 +1 @@ -Subproject commit 932cf73faad68266f5dd8b4d6943e82d2b3130ae +Subproject commit c8b3ae5615c648d47978006ae9d70ac4e6a2add4 diff --git a/pyproject.toml b/pyproject.toml index 4659d9a5..6fdc8c83 100644 --- a/pyproject.toml +++ b/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", diff --git a/tests/test_design_doc_finder.py b/tests/test_design_doc_finder.py index f22878f3..722471ea 100644 --- a/tests/test_design_doc_finder.py +++ b/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] = [ diff --git a/tests/test_fs_forbidden_read.py b/tests/test_fs_forbidden_read.py new file mode 100644 index 00000000..fa9b4018 --- /dev/null +++ b/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")