summarization_detector: standalone summarization-target detector

.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

@@ -2,20 +2,26 @@ name: Integration Tests
 
 on:
   schedule:
-    - cron: '7 5 * * *'
-  workflow_dispatch: {}   # adds a "Run workflow" button in the Actions tab
+    - cron: "7 5 * * *"
+  workflow_dispatch: {} # adds a "Run workflow" button in the Actions tab
 
 # If a manual run and a scheduled run overlap, cancel the older one
 # so you don't pay for the expensive job twice.
 concurrency:
   group: scheduled-tests
   cancel-in-progress: true
 
+permissions:
+  id-token: write
+  contents: read
+
 jobs:
   test:
     runs-on: ubuntu-latest
     timeout-minutes: 20
-
+    environment: prod # Both dev/stg are available as well
+    env:
+      CERTORA_LAMBDA_URL: ${{ secrets.LAMBDA_FUNCTION_URL }}
     steps:
       - name: Check out code
         uses: actions/checkout@v4
@@ -31,18 +37,22 @@ jobs:
       - name: Set up JDK
         uses: actions/setup-java@v4
         with:
-          distribution: 'temurin'
-          java-version: '21'
+          distribution: "temurin"
+          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.
@@ -51,14 +61,28 @@ jobs:
           sudo chmod +x /usr/local/bin/solc8.29
           solc8.29 --version
 
+      - name: Configure AWS credentials
+        uses: aws-actions/configure-aws-credentials@e6de054238d6b7531b4efff3b6587d9aade6a06c # v6.2.3
+        with:
+          role-to-assume: ${{ secrets.AWS_OIDC_ROLE_ARN }}
+          aws-region: us-west-2
+
+      - name: Basic who-am-i check
+        run: |
+          # The stored URL ends in a slash and //who-am-i would not route.
+          curl -sS --fail-with-body "${CERTORA_LAMBDA_URL%/}/who-am-i" \
+            --user "$AWS_ACCESS_KEY_ID":"$AWS_SECRET_ACCESS_KEY" \
+            -H "x-amz-security-token: $AWS_SESSION_TOKEN" \
+            --aws-sigv4 "aws:amz:us-west-2:lambda"
+
       - 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

@@ -2,9 +2,9 @@ name: pyright-check
 
 on:
   push:
-    branches: [ main, master ]
+    branches: [ main, master, dev ]
   pull_request:
-    branches: [ main, master ]
+    branches: [ main, master, dev ]
 
 jobs:
   pyright:
@@ -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

@@ -2,9 +2,9 @@ name: pytest-check
 
 on:
   push:
-    branches: [ main, master ]
+    branches: [ main, master, dev ]
   pull_request:
-    branches: [ main, master ]
+    branches: [ main, master, dev ]
 
 jobs:
   pytest:
@@ -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.