Jaroslav/reset dev to master

.github/scripts/sandbox_vm_provision.sh

@@ -13,7 +13,8 @@
 # regardless (§11 item 2).
 #
 # Kept dependency-light on purpose: the escape suite imports only stdlib +
-# composer.sandbox.* (all stdlib) + pytest, so we install just pytest via uv and
+# composer.sandbox.*, whose sole third-party import is annotated_types (three
+# files, no dependencies of its own). So we install just pytest + that via uv and
 # put the repo on PYTHONPATH — no project build, no numpy/psycopg/langchain. We
 # pass --noconftest so tests/conftest.py (which imports those heavy deps) is not
 # collected; the suite's fixtures are all in-module.
@@ -75,8 +76,10 @@ section "Escape suite against kernel ${KREL}"
 export PYTHONPATH="${REPO}"
 # --no-project: don't build AutoProver; --with: ephemeral pytest env.
 # --noconftest: skip tests/conftest.py's heavy imports (fixtures here are in-module).
+# annotated-types is composer.sandbox.config's only non-stdlib import (it carries the
+# Ge(0) bound on the Rust-mirrored timeout_s), so importing the package needs it here.
 uv run --no-project --python 3.12 \
-  --with 'pytest>=9.0' --with 'pytest-asyncio>=1.3' \
+  --with 'pytest>=9.0' --with 'pytest-asyncio>=1.3' --with 'annotated-types>=0.7' \
   pytest --noconftest -v \
   --junitxml="${JUNIT}" \
   "${REPO}/tests/test_sandbox_escape.py"

.github/workflows/integration-tests.yml

@@ -41,14 +41,18 @@ jobs:
           java-version: "21"
 
       - name: sync-deps
+        # --no-dev skips the `dev` group (and the `apps` group it includes), so this
+        # job doesn't compile the Rust crates — nothing under `expensive` or `fuzz`
+        # touches them. Every `uv run` below needs the flag too: a bare `uv run`
+        # re-syncs with the default groups and would pull `apps` back in.
         run: |
-          uv sync --group test --extra prover
+          uv sync --group test --extra prover --no-dev
 
       - name: sync solc
         run: |
           uv pip install solc-select
-          uv run solc-select install 0.8.29
-          uv run solc-select use 0.8.29
+          uv run --no-dev solc-select install 0.8.29
+          uv run --no-dev solc-select use 0.8.29
           # certoraRun resolves Certora-convention names like `solc8.29` as
           # literal executables; solc-select only ships the `solc` shim, so
           # fetch the static binary under that exact name.
@@ -73,12 +77,12 @@ jobs:
 
       - name: run autoprover integration tests
         run: |
-          uv run pytest -n 3 -m 'expensive' tests
+          uv run --no-dev pytest -n 3 -m 'expensive' tests
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
       - name: run template fuzz tests
         run: |
-          uv run pytest -n 2 -m 'fuzz' tests
+          uv run --no-dev pytest -n 2 -m 'fuzz' tests
         env:
           HYPOTHESIS_PROFILE: extended
 

.github/workflows/pyright.yml

@@ -22,10 +22,13 @@ jobs:
           cache-suffix: pyright
 
       - name: sync-deps
+        # --no-dev skips the `dev` group (and the `apps` group it includes), so this
+        # job doesn't compile the Rust crates — pyright can't see into a compiled
+        # extension module anyway.
         run: |
-          uv sync --group ci
+          uv sync --group ci --no-dev
           uv pip install sentence_transformers --no-deps
 
       - name: Run pyright
         run: |
-          uv run pyright composer/ analyzer sanity_analyzer certora_autosetup
+          uv run --no-dev pyright composer/ analyzer sanity_analyzer certora_autosetup

.github/workflows/pytest.yml

@@ -20,7 +20,29 @@ jobs:
           enable-cache: true
           cache-dependency-glob: "uv.lock"
           cache-suffix: pytest
-
+
+      # `dev` is one of uv's default groups and includes `apps`, so the sync below
+      # builds the `rust/` wheels — tests/test_rustapp.py and the launcher suites
+      # skip themselves without them. uv builds those crates concurrently, and
+      # rustup's install path is not safe against concurrent invocations: whichever
+      # maturin -> cargo call wins clears $RUSTUP_HOME/downloads and the other one
+      # dies renaming its half-downloaded component. So install the toolchain
+      # serially, first. No argument — rustup takes the channel, profile and
+      # components from rust-toolchain.toml.
+      - name: Install the pinned Rust toolchain
+        run: rustup toolchain install --no-self-update
+
+      - name: Cache the Rust build
+        uses: actions/cache@v4
+        with:
+          path: |
+            ~/.cargo/registry/index
+            ~/.cargo/registry/cache
+            ~/.cargo/git/db
+            rust/target
+          key: cargo-pytest-${{ hashFiles('rust/Cargo.lock') }}
+          restore-keys: cargo-pytest-
+
       - name: sync-deps
         run: |
           uv sync --group test --extra prover

ARCHITECTURE.md

@@ -115,7 +115,7 @@ five steps and never inspects anything backend-specific:
 `run_pipeline` also takes an `ecosystem: Ecosystem[App, Main, Unit]`
 ([composer/pipeline/ecosystem.py](composer/pipeline/ecosystem.py)) — the *front-half* plug point,
 orthogonal to the backend. It pairs a **language** (how the target's source is read — fs-exclusion
-pattern, code-explorer prompt) with a **chain** and supplies the domain-specific pieces the shared
+pattern) with a **chain** (including the code-explorer prompt) and supplies the domain-specific pieces the shared
 steps need: the analyzed-model type (`App`), the analysis/property prompts, model validation, how
 to locate the target `Main`, and `units(main) -> list[Unit]` (the per-unit split the extraction and
 formalization phases iterate). `EVM` binds `(SourceApplication, ContractInstance,

CLAUDE.md

@@ -29,6 +29,12 @@ loose). Both flags matter:
   every non-default group the two commands above need, `ci` (pyright) included, or the sync
   that fixes one of them breaks the other:
   `uv sync --group test --group ci --group ragbuild --extra cpu --extra certora-cli`.
+- **The Rust toolchain.** That sync's default `dev` group builds the maturin crates under
+  `rust/`, so it needs cargo. If the toolchain `rust-toolchain.toml` pins is not installed
+  yet, install it first and on its own — `rustup toolchain install --no-self-update`, no
+  argument, so rustup reads the channel, profile and components from that file. uv builds
+  those crates concurrently and rustup's on-demand install is not concurrency-safe, so
+  letting the build trigger it races.
 
 ## Python
 

README.md

@@ -40,11 +40,28 @@ The rest of this document covers the **host `uv` flow** for development.
 You need everything from the [AIComposer infrastructure setup](AICOMPOSER_INFRA.md):
 
 - Python 3.12+, `uv`, Docker with compose
+- `rustup` — a default `uv sync` builds the `rust/` crates (see below)
 - `ANTHROPIC_API_KEY` in your environment
 - PostgreSQL databases running (see below)
 - RAG database populated
 - Solidity compiler(s) on `$PATH` (naming convention `solcX.Y`, e.g. `solc8.29`)
 
+### Rust toolchain
+
+A `uv sync`, or any `uv run`, which revalidates path dependencies, builds the maturin crates under `rust/`. Without a
+toolchain the sync fails outright rather than skipping. Install [rustup](https://rustup.rs) (a distro `cargo` package is
+not enough: `rust-toolchain.toml` pins the toolchain and rustup is what reads it), then once, from the repo root:
+
+```bash
+rustup toolchain install --no-self-update
+```
+
+Re-run that after any bump to `rust-toolchain.toml`'s `channel` — rustup would otherwise install the new toolchain from
+inside the build, where the concurrent cargo calls a sync makes race each other and one dies mid-download.
+
+Not working on the Rust side? `uv sync --no-dev` skips the crates entirely — the Rust tests then skip themselves instead
+of failing, and the CI pyright job runs this way.
+
 ### Certora Prover
 
 **Cloud mode (the default):** Two credentials are needed. `CERTORAKEY` (set in your environment) authenticates `certoraRun` when it submits prover jobs. The job *results* are fetched with the Certora cloud credentials produced by `certora-cloud login` — install the public CLI (`uv tool install certora-cloud`) and run it once (`certora-cloud login`); it writes `~/.certora/credentials.json`, which is read automatically. Exporting `CERTORA_USER`/`CERTORA_TOKEN`/`CERTORA_REFRESH_TOKEN` instead is an optional override.

certora_autosetup/autosetup/autosetup.py

@@ -418,7 +418,12 @@ def is_file_in_scope(self, file_path):
 
             # Get appropriate manager class and create instance
             ManagerClass = BuildSystemDetector.get_manager_class(detected)
-            manager: BuildSystemManager = ManagerClass(self.build_config_dir, scope)  # type: ignore
+            # The manager is anchored on the build config dir, but remapping contexts and the
+            # hoisted-package walk belong to the directory certoraRun runs from — the two differ
+            # exactly when the build config lives in a monorepo sub-project.
+            manager: BuildSystemManager = ManagerClass(  # type: ignore
+                self.build_config_dir, scope, run_root=run_root
+            )
 
             # Auto-detect and parse config (polymorphic - returns FoundryConfig or HardhatConfig)
             self.log(f"Auto-detecting {detected.value} configuration...")

certora_autosetup/autosetup/cli.py

@@ -28,7 +28,7 @@
     FILE_LLM_USAGE,
     FILE_PROVER_USAGE,
 )
-from certora_autosetup.utils.contract_utils import auto_detect_contracts, deduplicate_contract_handles, parse_contract_files, resolve_contract_handles, split_contract_spec
+from certora_autosetup.utils.contract_utils import auto_detect_contracts, deduplicate_contract_handles, parse_contract_files, resolve_contract_handles, split_contract_spec, with_contract_handle
 from certora_autosetup.utils.project_dir import find_build_config_dir
 from certora_autosetup.utils.enhanced_config_manager import ConfigManager
 from certora_autosetup.utils.llm_util import LlmUsageReport, ledger_reset
@@ -82,10 +82,31 @@ def main():
 
     contract_handles = deduplicate_contract_handles(contract_handles)
 
-    # Parse main contract
-    main_handles = parse_contract_files([args.main_contract])
+    # Parse main contract. It goes through the same artifact-backed name resolution as
+    # --contract-files-and-name, so a bare `path.sol` spec gets the contract the file really
+    # declares instead of the filename stem.
+    main_handles = resolve_contract_handles(
+        parse_contract_files([args.main_contract]), build_config_dir, profile=args.profile,
+        requested_build_system=args.build_system, handles_relative_to=cwd,
+    )
     main_contract_handle = main_handles[0]
 
+    # A contract the caller named is in scope by definition, but two upstream steps can drop
+    # it: auto-detection skips every file under a dependency directory (node_modules/, lib/,
+    # dependencies/, ...), which is where per-address verification bundles and vendored
+    # sub-projects keep real, deployed code, and deduplicate_contract_handles prefers the
+    # shortest path when two files declare the same contract name. Either way the run fails
+    # much later, from setup_prover, as "is not among the compiled contracts in the prover
+    # scene" — a compilation message for what is really a scoping decision.
+    if main_contract_handle not in contract_handles:
+        logger.log(
+            f"Main contract {main_contract_handle.contract_name}@"
+            f"{main_contract_handle.source_file} was not among the auto-detected contracts "
+            f"— adding it to the scene",
+            "INFO", "Autosetup",
+        )
+        contract_handles = with_contract_handle(contract_handles, main_contract_handle)
+
     # TODO: a bare `path.sol` spec drops only the contract whose name matches the file
     # stem. Expand to "drop every concrete contract in the file" for symmetry with
     # auto-detect's emit-all default. Mirror the same expansion for include specs

certora_autosetup/build_systems/foundry.py

@@ -124,15 +124,16 @@ class FoundryManager(BuildSystemManager):
     error handling, and integrated compilation management.
     """
 
-    def __init__(self, project_root: Path, scope):
+    def __init__(self, project_root: Path, scope, run_root: Optional[Path] = None):
         """
         Initialize foundry manager.
 
         Args:
-            project_root: Root directory of the project
+            project_root: Directory the foundry.toml is anchored on
             scope: Centralized scope for consistent filtering
+            run_root: Directory certoraRun is invoked from (defaults to project_root)
         """
-        super().__init__(project_root, scope, "FoundryManager")
+        super().__init__(project_root, scope, "FoundryManager", run_root=run_root)
 
     def get_config_filenames(self) -> List[str]:
         """Return list of config filenames to search for."""
@@ -182,7 +183,10 @@ def parse_config(self, config_file: Path, profile: str | None = None) -> Foundry
             # Build the packages list from forge remappings + foundry.toml + remappings.txt
             # + package.json for the resolved profile.
             packages = build_packages_from_remapping_sources(
-                base_dir=config_file.parent, log_fn=self.log, profile=profile
+                base_dir=config_file.parent,
+                log_fn=self.log,
+                profile=profile,
+                run_root=self.run_root,
             )
             if packages:
                 config.packages = packages
@@ -390,6 +394,15 @@ def get_build_command(self, profile: Optional[str] = None) -> str:
             return f"FOUNDRY_PROFILE={profile} forge build"
         return "forge build"
 
+    @staticmethod
+    def holds_artifacts(artifacts_dir: Path) -> bool:
+        """Foundry writes one `<source>.sol/` directory per compiled source file."""
+        if not artifacts_dir.is_dir():
+            return False
+        return any(
+            child.is_dir() and child.name.endswith(".sol") for child in artifacts_dir.iterdir()
+        )
+
     def filter_artifacts(self, artifacts_dir: Path) -> List[Path]:
         """
         Filter Foundry artifacts - all .json files except those in build-info/ directories.

certora_autosetup/build_systems/hardhat.py

@@ -76,15 +76,18 @@ class HardhatManager(BuildSystemManager):
     Parallel to FoundryManager but adapted for Hardhat's JavaScript/TypeScript ecosystem.
     """
 
-    def __init__(self, project_root: Path, scope):
+    def __init__(self, project_root: Path, scope, run_root: Optional[Path] = None):
         """
         Initialize Hardhat manager.
 
         Args:
-            project_root: Root directory of the project
+            project_root: Directory the hardhat config is anchored on
             scope: Centralized scope for consistent filtering
+            run_root: Directory certoraRun is invoked from (defaults to project_root).
+                Accepted for interface parity — autosetup constructs every manager class
+                through the same call.
         """
-        super().__init__(project_root, scope, "HardhatManager")
+        super().__init__(project_root, scope, "HardhatManager", run_root=run_root)
 
     def get_config_filenames(self) -> List[str]:
         """Return list of config filenames to search for."""
@@ -381,6 +384,16 @@ def get_build_command(self, profile: Optional[str] = None) -> str:
         """Return Hardhat build command."""
         return "npx hardhat compile"
 
+    @staticmethod
+    def holds_artifacts(artifacts_dir: Path) -> bool:
+        """Hardhat mirrors the sources tree under the artifacts dir and writes `build-info/`
+        beside it; the mirror is named after `paths.sources`, so `build-info/` is the part
+        that is there whatever the project calls its sources."""
+        if not artifacts_dir.is_dir():
+            return False
+        return (any((artifacts_dir / "contracts").rglob("*.json"))
+                or any((artifacts_dir / "build-info").glob("*.json")))
+
     def filter_artifacts(self, artifacts_dir: Path) -> List[Path]:
         """
         Filter Hardhat artifacts - only contracts/, exclude .dbg.json and build-info/.

certora_autosetup/build_systems/manager.py

@@ -11,7 +11,7 @@
 import sys
 from abc import ABC, abstractmethod
 from pathlib import Path
-from typing import Callable, List, Set
+from typing import Callable, List, Optional, Set
 
 from certora_autosetup.build_systems.base import BuildSystemConfig
 
@@ -25,16 +25,22 @@ class BuildSystemManager(ABC):
     build-system-specific parsing and command generation.
     """
 
-    def __init__(self, project_root: Path, scope, component_name: str):
+    def __init__(self, project_root: Path, scope, component_name: str, run_root: Optional[Path] = None):
         """
         Initialize build system manager.
 
         Args:
-            project_root: Root directory of the project
+            project_root: Directory the build config is anchored on — where config discovery
+                starts and artifacts are read from. In a monorepo this is the sub-project that
+                owns the main contract, not the run root.
             scope: Centralized scope for consistent filtering
             component_name: Name for logging (e.g. "FoundryManager", "HardhatManager")
+            run_root: Directory certoraRun is invoked from. Remapping contexts are expressed
+                against it and the hoisted-package walk is bounded by it. Defaults to
+                project_root, which is correct whenever the build config sits at the run root.
         """
         self.project_root = project_root
+        self.run_root = run_root or project_root
         self.scope = scope
         self.component = component_name
 
@@ -101,6 +107,27 @@ def get_build_command(self, profile: str | None = None) -> str:
         """
         pass
 
+    @staticmethod
+    @abstractmethod
+    def holds_artifacts(artifacts_dir: Path) -> bool:
+        """
+        Whether *artifacts_dir* holds output written by this build system.
+
+        Recognises the build system's own layout inside the directory, so a directory that
+        merely exists under the expected name does not pass for a built project. That
+        happens for real: a project whose configured output dir is nested (Foundry's
+        ``out = "out/foundry"``) has a bare ``out/`` holding only subdirectories, and a
+        project that shipped a second build config often has an empty artifact dir left by
+        the tool that no longer runs.
+
+        Args:
+            artifacts_dir: Directory to inspect; need not exist
+
+        Returns:
+            True if the directory holds this build system's artifacts
+        """
+        pass
+
     @abstractmethod
     def filter_artifacts(self, artifacts_dir: Path) -> List[Path]:
         """