diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md new file mode 100644 index 00000000..dcf96eb4 --- /dev/null +++ b/ARCHITECTURE.md @@ -0,0 +1,320 @@ +# AutoProver — Architecture & High-Level Design + +> A companion to the [README](README.md). The README tells you how to *run* AutoProver; +> this document explains how it is *built* — the major subsystems, the abstractions that +> hold them together, and the data flow through a run. + +## 1. What it is + +AutoProver (internally "AI Composer") is a **multi-agent pipeline that turns a smart-contract +codebase + a design document into verified formal specifications.** Given a project root, a +main contract/program, and a system description, it drives a fleet of LLM agents to analyze the +system, formulate properties, author CVL (Certora Verification Language) specs, and run the +Certora Prover in a feedback loop until the specs verify (or the agent gives up with a +reason). + +The default target is Solidity + the Certora Prover, but the front half is parameterized by an +**ecosystem** (an analyzed *language* × *chain* pairing — see §4), so the same driver also +analyzes Rust/Solana programs; the domain is not hardcoded into the shared steps. + +The same generic pipeline also powers two sibling workflows — **Foundry test generation** +and **NatSpec greenfield code generation** — which reuse the shared analysis/extraction/ +reporting machinery behind a backend protocol. + +## 2. Design philosophy + +A handful of decisions shape the whole codebase: + +- **Generic driver, two axes of pluggability.** One backend-agnostic driver + ([composer/pipeline/core.py](composer/pipeline/core.py)) owns the steps that are the same + for everyone (system analysis, property extraction, caching, report assembly). Two things + plug into it independently: a **backend** contributes how a spec is authored and verified + (the *back* half), and an **ecosystem** supplies the domain-specific *front* half — the + analyzed-model type, prompts, source-reading conventions, and how the target is split into + units. Adding the Foundry backend required *no* changes to the shared steps; adding the + Solana ecosystem required *no* backend changes. +- **Phase-chain immutability.** Each phase produces an immutable object that is the + constructor input to the next: `Backend → PreparedSystem → Formalizer`. The *existence* of + a `Formalizer` proves that system analysis and preparation already succeeded — ordering is + a type-level dependency, not a call-order convention, so there is no half-initialized state. + A backend whose units all build on one shared artifact adds a link instead of an exception: + `prepare_formalization` returns a `StagedFormalizer`, whose `begin` takes every unit's + properties and returns the `Formalizer` built around the artifact authored from them. +- **Agents are graphs; everything is checkpointed.** Every agent is a LangGraph state graph + built from a reusable framework ([graphcore/](graphcore/)). State, conversations, and + intermediate results are persisted to Postgres so any run can be resumed, time-traveled, + inspected, or replayed. +- **Tight LLM↔tool loops with hard validation gates.** Agents don't emit free text that is + hoped to be correct — every CVL write passes the Certora type-checker, every spec is run + through the actual prover, and a separate "judge" agent adjudicates whether a property was + legitimately handled. Invalid output is rejected at the tool boundary with actionable + feedback. +- **Deterministic, LLM-free replay for tests.** A "tape" system records real LLM responses + per task and replays them, letting the entire pipeline run end-to-end in CI with no API + calls. + +## 3. The big picture + +``` + ┌──────────────────────────────────────────────┐ + CLI / TUI │ GENERIC PIPELINE DRIVER │ + (console_autoprove, │ composer/pipeline/core.py │ + tui_autoprove) │ │ + │ │ 1. System Analysis ───────► SourceApplication│ + │ builds context │ 2. backend.prepare_system ─► PreparedSystem │ + ▼ │ 3. prepare_formalization ∥ property extraction│ + AIComposerContext │ 4. per-unit formalize (parallel) │ + (LLM, RAG, prover opts, │ 5. backend-agnostic Report │ + VFS, handler factory) └───────────────┬────────────────────────────────┘ + │ │ PipelineBackend protocol + │ ┌─────────────────┼─────────────────┐ + ▼ ▼ ▼ ▼ + ┌─────────┐ Prover backend Foundry backend NatSpec workflow + │ graphcore│ (CVL specs + (.t.sol tests + (greenfield stubs + │ agent fw │ Certora Prover) forge test) + CVL) + └────┬─────┘ + │ each agent = LangGraph state graph + tools + ▼ + ┌──────────────────────────────────────────────────────────────────┐ + │ Tools: filesystem/VFS · CVL author+typecheck · prover · RAG │ + │ search · knowledge base · human-in-loop · memory │ + └──────────────────────────────────────────────────────────────────┘ + │ + ▼ + ┌──────────────────────────────────────────────────────────────────┐ + │ Persistence (Postgres): rag_db · langgraph_store_db · │ + │ langgraph_checkpoint_db · memory_tool_db · audit_db │ + └──────────────────────────────────────────────────────────────────┘ +``` + +## 4. The generic pipeline driver + +[composer/pipeline/core.py](composer/pipeline/core.py) is the spine. `run_pipeline()` executes +five steps and never inspects anything backend-specific: + +1. **System analysis** (shared). Runs `run_component_analysis` to produce the ecosystem's + analyzed model (`App`) — for EVM, a `SourceApplication` of contracts, components, external + actors, and their interactions. Determined by the ecosystem, not the backend: every backend + on a given ecosystem sees the same analyzed type. +2. **`backend.prepare_system(analyzed)`** — the backend's transform. The prover backend lifts + the source app into a *harnessed* application (generating harness contracts for external + dependencies); the Foundry backend is an identity transform. +3. **`prepared.prepare_formalization()` runs concurrently with property extraction.** Neither + depends on the other, so the prover's expensive AutoSetup/summary/invariant work overlaps + with per-unit property inference. Property extraction fans out one agent per *unit* — + `ecosystem.units(main)` — one per **component** of the main contract/program in both + ecosystems — bounded by a semaphore (`--max-concurrent`). +4. **Per-unit formalization** (parallel). For each unit's properties, the backend's + `Formalizer.formalize()` is invoked. Results are cached by the backend's result type. +5. **Report assembly** (shared, best-effort). The driver collects per-unit verdicts via a + backend-supplied `fetch_verdicts` callback, an LLM groups properties into semantic clusters, + and a coverage check validates the result. A failure here never fails the run. + +### The ecosystem seam + +`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 +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, +ContractComponentInstance)`; `SOLANA` binds `(SolanaApplication, SolanaProgramInstance, +SolanaComponentInstance)`. A unit is any +`FeatureUnit` ([spec/system_model.py](composer/spec/system_model.py)) — the ecosystem-agnostic +interface the driver uses for per-unit cache keys, task ids, and labels. The default is `EVM`, so +Solidity backends pass nothing. + +### The backend contract + +A backend implements `PipelineBackend[P, FormT, H, A, U, Main]` plus three phase objects. `U` +(the `FeatureUnit` type) and `Main` are the ecosystem-tying parameters — `run_pipeline` binds a +`PipelineBackend[..., U, Main]` to an `Ecosystem[App, Main, U]` so the analyzed model, main-unit, +and per-unit values flow through without casts: + +| Object | Responsibility | Prover impl | Foundry impl | +|---|---|---|---| +| `PipelineBackend` | Phase-enum map, analysis prompt, artifact store, `prepare_system` | [spec/source/pipeline.py](composer/spec/source/pipeline.py) | [foundry/pipeline.py](composer/foundry/pipeline.py) | +| `PreparedSystem` | Holds the located `Main`; builds the `Formalizer` | harness-lifted app + AutoSetup/invariants | identity | +| `Formalizer` | `formalize()` one unit; `fetch_verdicts`; `finalize` | `batch_cvl_generation` + prover | `batch_foundry_test_generation` + `forge test` | + +The phase enum (`CorePhases`) lets each backend label its own phases while the driver tags the +three universal ones (analysis / extraction / formalization) for the UI and the replay tapes. + +## 5. The agent framework (graphcore + workflow) + +Every LLM agent in the system is a LangGraph state graph, constructed through a reusable, +type-safe framework. + +- **[graphcore/](graphcore/)** is a standalone library (its own package, used by other Certora + products too). It provides a fluent `Builder[State, Context, Input]` that binds a model, + state type, tools, system/initial prompt templates, and an optional summarization config, + then compiles a checkpointed `StateGraph`. The agent loop is the standard + *LLM → tool calls → tool results → LLM …* cycle, terminating when the model produces a + final structured output instead of more tool calls. +- **Tools** are Pydantic models with `run()` implementations and mixins for injecting graph + state / tool-call id. Tools return either a string, a `Command` that merges into state, or an + `interrupt()` that pauses the graph for human input. +- **[composer/workflow/](composer/workflow/)** wires graphcore to this application: model + capability parsing ([llm.py](composer/workflow/llm.py) — thinking budgets, interleaved + thinking, memory-tool beta, cache control), Postgres checkpointer + store services + ([services.py](composer/workflow/services.py)), and summarization tuned for long spec runs + ([summarization.py](composer/workflow/summarization.py)). +- **[composer/io/](composer/io/)** is the execution and observability layer. `run_task` + ([multi_job.py](composer/io/multi_job.py)) wraps each schedulable unit with a handler factory, + an optional concurrency semaphore, and lifecycle hooks. Graph execution emits an immutable + event stream (Start / StateUpdate / Checkpoint / CustomUpdate / End) onto a lock-free queue; + a background drainer dispatches events to the active IO handler (console or TUI). Nested + sub-agent graphs are tracked transparently so handlers can reconstruct the full call path. + +### State, context, and editing + +- `AIComposerState` ([core/state.py](composer/core/state.py)) extends LangGraph's message state + with a virtual filesystem (VFS), validation results, and the working spec being edited. +- `AIComposerContext` ([core/context.py](composer/core/context.py)) is the run-scoped dependency + container: the bound LLM, RAG connection, prover options, and VFS materializer. +- Spec edits go through `replace_unique` ([core/edit.py](composer/core/edit.py)) — a surgical, + match-exactly-once text replacement that fails with actionable guidance on ambiguity, keeping + the model honest about what it's changing and saving tokens. + +## 6. The prover (default) backend — phase by phase + +Implemented under [composer/spec/source/](composer/spec/source/). The phases map onto the +README's Phase 0–5: + +- **System analysis** ([spec/system_analysis.py](composer/spec/system_analysis.py), + [system_model.py](composer/spec/system_model.py)) — an agent reads the design doc and source + to produce a `SourceApplication` of contracts → components, each with entry points, state + variables, interactions, and requirements. +- **Harness setup** ([spec/source/harness.py](composer/spec/source/harness.py)) — a classifier + agent categorizes external contracts (singleton / multiple / dynamic, ERC20s, interfaces) and + generates harness contracts, lifting the system to a `HarnessedApplication`. +- **AutoSetup** ([spec/source/autosetup.py](composer/spec/source/autosetup.py)) — shells out to + the [certora_autosetup/](certora_autosetup/) package to compile the project and produce a + prover `compilation_config.conf` plus summaries for known externals. +- **Custom summaries** ([spec/source/summarizer.py](composer/spec/source/summarizer.py)) — + generates CVL summaries for ERC20s and external interfaces. +- **Structural invariants** ([spec/source/struct_invariant.py](composer/spec/source/struct_invariant.py)) + — a two-agent loop: one proposes invariants, a judge accepts/rejects each (not structural / + not inductive / unlikely to hold / …). Survivors become `certora/specs/invariants.spec`, + importable by later phases. +- **Per-component property extraction** ([spec/prop_inference.py](composer/spec/prop_inference.py)) + — multi-round agent producing `PropertyFormulation`s (attack vectors, safety properties, + invariants), optionally refined interactively or against a threat model. +- **CVL generation** ([spec/cvl_generation.py](composer/spec/cvl_generation.py), + [spec/source/author.py](composer/spec/source/author.py)) — the core feedback loop. The agent + authors CVL with `put_cvl`/`edit_cvl` (type-checked on every write), runs the prover via a + `verify_spec` tool, analyzes any counterexamples, and revises. A property-feedback judge + validates coverage and adjudicates the agent's objections (e.g. "this property is vacuous + because…"). Output is a `GeneratedCVL` carrying the spec, skipped properties with reasons, + the property→rule mapping, and the final prover run link. + +### Outputs and artifacts + +`ArtifactStore` ([spec/artifacts.py](composer/spec/artifacts.py), prover subclass in +[spec/source/](composer/spec/source/)) owns the on-disk layout under the project's `certora/`: +specs in `certora/specs/`, configs in `certora/confs/`, per-spec metadata (properties, +property→rules, commentary) in `certora/properties/`, and a final `certora/ap_report/report.json`. + +## 7. Caching & resumption + +Two complementary mechanisms: + +- **Phase cache** (`--cache-ns`). `WorkflowContext` / `CacheKey` + ([spec/context.py](composer/spec/context.py)) form a hierarchical, type-parameterized cache + in the LangGraph store: `None → SourceApplication → Properties → ComponentGroup → CVLGeneration`. + Each key incorporates a hash of its inputs, so changing the project, doc, or contract + invalidates exactly the affected subtree. Repeated runs skip completed phases. +- **Checkpointing** (`--thread-id` / `--checkpoint-id`). LangGraph persists graph state after + every node to `langgraph_checkpoint_db`, enabling crash recovery and "time travel" — resuming + from any prior checkpoint, even a non-latest one. + +## 8. Prover integration + +[composer/prover/](composer/prover/) abstracts running the Certora Prover. `run_prover` +([core.py](composer/prover/core.py)) spawns `certoraRun`, streams stdout, and resolves results +through either a **local** results path or a **cloud** path ([cloud.py](composer/prover/cloud.py), +polled via job URL) depending on `ProverOptions.cloud`. Violated rules are fed to a +counterexample analyzer ([analysis.py](composer/prover/analysis.py)) whose findings go back to +the authoring agent. A callback protocol streams per-rule outcomes to the UI and the audit DB. + +## 9. Knowledge: RAG + curated KB + +- **RAG** ([composer/rag/](composer/rag/)) — the CVL manual, chunked and embedded + (`nomic-embed-text-v1.5`) into `rag_db` (pgvector, with a ChromaDB fallback). Agents query it + for CVL syntax/semantics during authoring. Read-only at runtime; rebuilt offline from the docs. +- **Curated KB** ([composer/kb/](composer/kb/)) — ~30 hand-written articles on CVL pitfalls + (vacuity traps, ghost semantics, summary misapplication…) stored in the LangGraph store and + searched semantically by symptom. Agents can also contribute new articles (`KBPut`). + +## 10. Alternate backends & workflows + +- **Foundry backend** ([composer/foundry/](composer/foundry/)) — same driver, but formalizes + properties as Solidity `.t.sol` tests verified by `forge test` instead of CVL + prover. + Verdicts come from test pass/expected-failure status. Entry points: + [cli/console_foundry.py](composer/cli/console_foundry.py), `tui_foundry.py`. +- **Solana ecosystem** ([composer/spec/solana/](composer/spec/solana/)) — the *front half* for + Rust/Solana targets: a `SolanaApplication` analysis model, Solana-specific analysis/property + prompts ([templates/solana/](composer/templates/solana/)), and per-component `units()` — one + unit per `ProgramComponent`, the Solana analog of EVM's `ContractComponent` + ([docs/ecosystem-abstraction.md](docs/ecosystem-abstraction.md) §4). It plugs into the same + driver via the `SOLANA` ecosystem; the matching verification backend (Crucible) lands separately. +- **NatSpec** ([composer/spec/natspec/](composer/spec/natspec/)) — a *greenfield* workflow + (its own asyncio orchestrator, not the generic driver) that goes from a design doc to Solidity + interfaces, stub implementations, and CVL. A semaphore-serialized "semantic registry" + ([natspec/registry.py](composer/spec/natspec/registry.py)) lets parallel agents share and + reuse generated state fields without conflicting. + +## 11. CLI, TUI & observability + +- **Entry points** ([composer/cli/](composer/cli/)) — `console-autoprove` (headless, prints to + stdout; best for `print`/log debugging) and `tui-autoprove` (Textual UI with per-phase panels + and live prover-output logs). Both build the context and call the same pipeline; CLI args are + parsed by introspecting `Annotated` protocol definitions in [composer/input/](composer/input/). +- **TUI** ([composer/ui/](composer/ui/)) — observes the pipeline purely through the IO event + stream, rendering per-task lanes, tool calls, and streamed prover output. +- **Diagnostics** ([composer/diagnostics/](composer/diagnostics/) + [scripts/](scripts/)) — + per-phase timing/token aggregation; `snapshot_viewer.py` replays a single agent's conversation + by mnemonic; `traceDump.py` renders a full run to HTML; `autoprove_cache_explorer.py` inspects + (and edits) cached phase results and agent memories. + +## 12. Testing — deterministic replay tapes + +[composer/testing/](composer/testing/) solves end-to-end testing without an LLM. A +`TapeRecorder` captures real `AIMessage` responses **per task, in call order** (including +out-of-graph calls like CEX analysis and interleaved sub-agents). `HarnessFakeLLM` replays +them by routing on the active task id (a `ContextVar` set by `run_task`). Tapes are +human-editable Python modules with embedded JSON; smoke scenarios live in +[test_scenarios/](test_scenarios/). Recording is curated into a clean tape before use (see the +`generate-tape` and `inspect-run` skills). + +## 13. Persistence map + +All state lives in Postgres (a single `pgvector/pgvector:pg16` container provisions all five): + +| Database | Holds | +|---|---| +| `rag_db` | CVL-manual embeddings for RAG search | +| `langgraph_store_db` | LangGraph document/index store — phase cache, KB articles | +| `langgraph_checkpoint_db` | Per-node workflow checkpoints (resume / time-travel) | +| `memory_tool_db` | Hierarchical LLM context memory (per agent) | +| `audit_db` | Run history, VFS snapshots, prover results, summaries (resumption + `traceDump`) | + +## 14. Top-level packages at a glance + +| Package | Role | +|---|---| +| [composer/](composer/) | The application — pipeline, agents, backends, tools, UI | +| [graphcore/](graphcore/) | Reusable LangGraph agent-building framework (separate package) | +| [certora_autosetup/](certora_autosetup/) | Solidity project analysis, compilation, harness/conf generation (Phase 1) | +| [analyzer/](analyzer/) | Standalone counterexample analyzer (also used inline by the prover backend) | +| [sanity_analyzer/](sanity_analyzer/) | Diagnoses unsatisfiable / sanity-failed prover runs | +| [scripts/](scripts/) | Docker entry, DB/RAG setup, trace & snapshot debugging tools | +| [tests/](tests/), [test_scenarios/](test_scenarios/) | Unit tests and tape-based smoke scenarios | + +--- + +*This document is a high-level map. For runtime/setup details see [README.md](README.md) and +[AICOMPOSER_INFRA.md](AICOMPOSER_INFRA.md); for the canonical contract between the driver and a +backend, read the module docstring and protocols in +[composer/pipeline/core.py](composer/pipeline/core.py).* diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 00000000..78798b81 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,54 @@ +# Repository conventions for coding agents + +Guidance for AI coding agents (and humans) working in this repo. Keep changes consistent +with these unless a maintainer says otherwise. + +## Pre-validating a commit + +The routine pass, both parts, ~20s total: + +```bash +uv run --no-sync pytest tests/ -m "not expensive" -q # ~10s +uv run --no-sync pyright # ~7s, must report 0 errors +``` + +Expect `N passed, M deselected`. `pyright` needs no arguments — `pyrightconfig.json` already +names the packages it checks (`tests/` is deliberately not among them, so test stubs may be +loose). Both flags matter: + +- **`-m "not expensive"` — do not omit this.** The `expensive` marker is *registered* in + `pyproject.toml` but **not** deselected by `addopts`, so a bare `pytest tests/` runs the + expensive tests, and those submit real jobs to the **live Certora cloud prover**. That costs + real money and ~6 minutes per test. Never run the suite without this filter unless a + maintainer asked for an expensive run specifically. +- **`--no-sync`.** A bare `uv run` re-syncs first, and a default sync *prunes* this venv: + `pytest`/`testcontainers` (group `test`), `pyright` (group `ci`), `sentence-transformers` + (group `ragbuild`) and `certora_cli`/`torch` (extras) all live outside uv's default groups, so + syncing uninstalls them and the next run dies at collection with `ModuleNotFoundError: No + module named 'certora_cli'`. To (re)build the env deliberately, sync everything at once: + `uv sync --group test --group ragbuild --extra cpu --extra certora-cli`. + +## Python + +### Do NOT use `from __future__ import annotations` + +Never add `from __future__ import annotations` to a module. If you touch a file that has it +and it's reasonable to do so, remove it. + +Why: +- It's a dead-end feature. PEP 563 (the string-annotations behaviour this import enables) was + never made the default and has effectively been superseded by PEP 649 / PEP 749 (lazy + evaluation) from Python 3.14 on. Relying on the `__future__` behaviour is betting on a path + the language is moving away from — it will change/break under you in future versions. +- It doesn't actually solve the problem it's reached for. Stringizing *all* annotations breaks + anything that introspects them at runtime — pydantic, dataclasses, `typing.get_type_hints`, + and our own annotation-driven graph wiring (see `composer/rustapp/_llm_agent.py`, which had + to stay eager precisely because stringized `NotRequired[T]` broke pydantic unwrapping). It + trades one set of problems for a subtler set. + +What to do instead (we target Python 3.12+): +- Modern syntax works at runtime without the future import: `X | None`, `list[str]`, + `dict[str, int]`, `tuple[int, ...]`, PEP 695 generics (`class Foo[T]:` / `def f[T]()`). +- For a genuine forward reference (a name not yet defined where the annotation is evaluated — + e.g. a dataclass field typed as a class defined later in the file), quote just that one + annotation: `backend: "RustBackend"`. Quote the specific ref; don't stringize the whole module. diff --git a/composer/cli/tui_pipeline.py b/composer/cli/tui_pipeline.py index cd7fafd1..73ba2486 100644 --- a/composer/cli/tui_pipeline.py +++ b/composer/cli/tui_pipeline.py @@ -31,6 +31,7 @@ WorkflowContext, SystemDoc, ) from composer.llm.registry import get_provider_for +from composer.pipeline.ecosystem import EVM 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 @@ -228,6 +229,8 @@ async def work(): handler_factory=app.make_handler, mental_model=mental_model, source_factory=source_factory, + # The only ecosystem natspec can run under; it authors Solidity and CVL. + ecosystem=EVM, max_concurrent=args.max_concurrent, interactive=args.interactive, max_bug_rounds=args.max_bug_rounds, diff --git a/composer/foundry/entry.py b/composer/foundry/entry.py index 5e9e6288..dda31f83 100644 --- a/composer/foundry/entry.py +++ b/composer/foundry/entry.py @@ -37,6 +37,7 @@ FoundryPhase, FoundryPipelineResult, backend ) from composer.pipeline.cli import cli_pipeline, user_ns, AtExit +from composer.pipeline.ecosystem import EVM _log = logging.getLogger(__name__) @@ -172,6 +173,6 @@ async def runner(fact: HandlerFactory[FoundryPhase, None]) -> FoundryPipelineRes source_input=staged.source, forge_concurrency=args.max_forge_runners ) - return await cont(env, f_backend) + return await cont(env, f_backend, EVM) yield runner \ No newline at end of file diff --git a/composer/foundry/pipeline.py b/composer/foundry/pipeline.py index ef7c323e..7c5ba396 100644 --- a/composer/foundry/pipeline.py +++ b/composer/foundry/pipeline.py @@ -32,9 +32,10 @@ from composer.pipeline.core import ( Formalizer, PreparedSystem, PipelineRun, GaveUp, SystemAnalysisSpec, - CorePhases, main_instance, CorePipelineResult, + CorePhases, CorePipelineResult, COMMON_SYSTEM_CACHE_KEY ) +from composer.pipeline.ecosystem import main_instance from composer.foundry.artifacts import FoundryTestArtifact from composer.spec.source.report.collect import ReportComponentInput, Verdict from composer.spec.context import ( @@ -78,7 +79,7 @@ system (a uint256 being non-negative, etc.) are also uninteresting. """ from composer.spec.system_model import ( - ContractComponentInstance, SourceApplication, + ContractComponentInstance, ContractInstance, SourceApplication, ) from composer.io.multi_job import HandlerFactory @@ -106,7 +107,7 @@ class FoundryPhase(enum.Enum): TEST_GENERATION = "test_generation" REPORT = "report" -class FoundryFormalizer(Formalizer[GeneratedFoundryTest]): +class FoundryFormalizer(Formalizer[GeneratedFoundryTest, ContractComponentInstance]): def __init__(self, conf: _ForgeRunConfig): super().__init__(GeneratedFoundryTest, "foundry") self.conf = conf @@ -138,11 +139,11 @@ async def fetch_verdicts(self, inp: ReportComponentInput[GeneratedFoundryTest]) return await _foundry_verdicts(inp) @dataclass -class FoundrySystem(PreparedSystem[GeneratedFoundryTest]): +class FoundrySystem(PreparedSystem[GeneratedFoundryTest, ContractComponentInstance, ContractInstance]): form: FoundryFormalizer @override - async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedFoundryTest]: + async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedFoundryTest, ContractComponentInstance]: return self.form @dataclass @@ -166,7 +167,7 @@ async def prepare_system( self, analyzed: SourceApplication, run: PipelineRun[FoundryPhase, None] - ) -> PreparedSystem[GeneratedFoundryTest]: + ) -> PreparedSystem[GeneratedFoundryTest, ContractComponentInstance, ContractInstance]: return FoundrySystem( main_instance( analyzed, run.source diff --git a/composer/pipeline/cli.py b/composer/pipeline/cli.py index ccdd16c5..83325243 100644 --- a/composer/pipeline/cli.py +++ b/composer/pipeline/cli.py @@ -20,8 +20,10 @@ CorePipelineResult ) from composer.spec.artifacts import ArtifactIdentifier +from composer.spec.system_model import FeatureUnit, BaseApplication from composer.spec.service_host import ModelProvider -from composer.spec.system_analysis import SolidityIdentifier +from composer.spec.types import SourceIdentifier +from composer.pipeline.ecosystem import Ecosystem from .core import PipelineBackend, run_pipeline from composer.io.multi_job import HandlerFactory, run_task, TaskInfo from composer.diagnostics.timing import RunSummary, install_run_summary @@ -113,10 +115,11 @@ class StagedPipeline: root_key: str class Continuation[P: enum.Enum, H](Protocol): - async def __call__[FormT: BackendResult, A: ArtifactIdentifier]( + async def __call__[FormT: BackendResult, A: ArtifactIdentifier, U: FeatureUnit, Main, App: BaseApplication]( self, env: ServiceHost, - backend: PipelineBackend[P, FormT, H, A] + backend: PipelineBackend[P, FormT, H, A, U, Main, App], + ecosystem: Ecosystem[App, Main, U] ) -> CorePipelineResult[FormT]: ... @@ -166,7 +169,7 @@ async def cli_pipeline[P: enum.Enum, H]( init_source = SourceFields( relative_path=relative_path, - contract_name=SolidityIdentifier(contract_name), + contract_name=SourceIdentifier(contract_name), forbidden_read=FS_FORBIDDEN_READ, project_root=str(project_root) ) @@ -249,9 +252,10 @@ async def cli_pipeline[P: enum.Enum, H]( relative_path=init_source.relative_path ) - async def cont[FormT: BackendResult, A: ArtifactIdentifier]( + async def cont[FormT: BackendResult, A: ArtifactIdentifier, U: FeatureUnit, Main, App: BaseApplication]( env: ServiceHost, - backend: PipelineBackend[P, FormT, H, A] + backend: PipelineBackend[P, FormT, H, A, U, Main, App], + ecosystem: Ecosystem[App, Main, U] ) -> CorePipelineResult[FormT]: full_ctx = WorkflowContext.create( services=conns.memory, @@ -273,9 +277,9 @@ async def cont[FormT: BackendResult, A: ArtifactIdentifier]( run=run, interactive=args.interactive, max_bug_rounds=args.max_bug_rounds, - threat_model=threat_model + threat_model=threat_model, + ecosystem=ecosystem, ) - ... yield (StagedPipeline( conns=conns, llm_models=models, logger=data_logger, diff --git a/composer/pipeline/core.py b/composer/pipeline/core.py index 3c92a585..2160bf80 100644 --- a/composer/pipeline/core.py +++ b/composer/pipeline/core.py @@ -6,6 +6,10 @@ Backend ──prepare_system──▶ PreparedSystem ──prepare_formalization──▶ Formalizer (config, source) (.main: structure) (formalize / persist / report) +A backend whose units all build on one *shared* artifact inserts a link: ``prepare_formalization`` returns +a :class:`StagedFormalizer`, and its ``begin`` — handed every unit's properties — is what produces the +:class:`Formalizer`. + The driver owns the genuinely-shared steps: system analysis, per-component property extraction, the result-type-keyed cache, and (since the report is backend-agnostic) building + persisting the property-keyed report. Everything backend-specific — the harnessed lift, autosetup/summaries/ @@ -17,10 +21,10 @@ import enum import logging from dataclasses import dataclass -from typing import Protocol +from typing import Protocol, Any, cast +from collections.abc import Sequence from abc import ABC, abstractmethod -from pydantic import BaseModel from composer.io.multi_job import TaskInfo from composer.spec.artifacts import ArtifactStore @@ -28,7 +32,7 @@ WorkflowContext, CacheKey, Properties, ComponentGroup, SourceCode ) from composer.spec.system_model import ( - SourceApplication, ContractInstance, ContractComponentInstance, AnyApplication + BaseApplication, FeatureUnit ) from composer.spec.types import PropertyFormulation, ArtifactIdentifier from composer.spec.system_analysis import run_component_analysis @@ -40,8 +44,10 @@ from composer.spec.source.report.schema import RuleName, ReportBackend from composer.spec.source.report import build as report_build from composer.spec.source.task_ids import SYSTEM_ANALYSIS_TASK_ID, REPORT_TASK_ID +from composer.pipeline.ecosystem import Ecosystem from .ptypes import ( - BackendJob, BackendResult, ComponentOutcome, CorePhases, CorePipelineResult, Delivered, GaveUp, PipelineRun, SystemAnalysisSpec + BackendJob, BackendResult, ComponentOutcome, CorePhases, CorePipelineResult, Delivered, GaveUp, + PipelineRun, SystemAnalysisSpec ) COMMON_SYSTEM_CACHE_KEY = "system-analysis" @@ -49,18 +55,23 @@ _log = logging.getLogger(__name__) @dataclass -class Formalizer[FormT: BackendResult](ABC): - """Immutable, fully constructed by prepare_formalization. Carries the prover's +class Formalizer[FormT: BackendResult, U: FeatureUnit](ABC): + """Immutable, fully constructed by whatever produced it — ``prepare_formalization``, or + :meth:`StagedFormalizer.begin` for a backend with a shared artifact. Carries the prover's config/resources/prover_tool/invariant-results (or nothing, for foundry) as constructor - state — never set post-hoc. `FormT: ReportableResult` is what makes the report a core step.""" + state — never set post-hoc. `FormT: ReportableResult` is what makes the report a core step. + + Generic over ``U``, the *formalized unit* type it consumes (EVM's ``ContractComponentInstance``, + a Rust backend's ``FeatureUnit``): the backend works with its concrete unit — reading its + members without casts — while the driver stays unit-agnostic.""" formalized_type: type[FormT] backend_tag: ReportBackend - + @abstractmethod async def formalize( self, label: str, - feat: ContractComponentInstance, + feat: U, props: list[PropertyFormulation], ctx: WorkflowContext[FormT], run: PipelineRun @@ -77,20 +88,63 @@ async def fetch_verdicts(self, inp: ReportComponentInput[FormT]) -> dict[RuleNam off-thread. Foundry: read straight off inp.formalized.result.""" ... - async def finalize(self, outcomes: list[ComponentOutcome[FormT]], run: PipelineRun) -> None: + async def finalize(self, outcomes: list[ComponentOutcome[FormT, U]], run: PipelineRun) -> None: """Emit any backend-specific run-level artifacts from the full outcome set (prover: components_to_prover_runs.json). Default: none.""" return None + +class StagedFormalizer[FormT: BackendResult, U: FeatureUnit](ABC): + """A formalizer that cannot exist yet: returned from ``prepare_formalization`` in place of a + :class:`Formalizer` by backends whose units all build on one *shared* artifact — Crucible's + fixture, whatever setup module a CVLR backend needs. + + Such an artifact must be authored from the union of every unit's properties (that union is what + makes them checkable), which pins it to exactly one point in the run. Not + ``prepare_formalization``: that overlaps extraction, so no properties exist there yet. Not lazily + on first ``formalize``: whichever unit won the race would decide the artifact all the others are + then told to work within — harmless at one unit, silently wrong at several. ``begin`` sits + between the two, where extraction is done and no unit has been formalized. + + A separate type rather than a hook on ``Formalizer`` so the types carry the ordering instead of + the driver's call sequence: ``begin`` *returns* the formalizer, so the shared artifact arrives as + a constructor argument and there is no window in which a formalizer exists without it — the same + property the rest of the phase chain has. + + Most backends need none of this and return a ``Formalizer`` directly; the prover's shared peer + (``invariants.spec``) is staged in ``prepare_formalization``.""" + + @abstractmethod + async def begin( + self, jobs: Sequence[BackendJob[U]], run: PipelineRun + ) -> Formalizer[FormT, U]: + """Author the shared artifact from **every** unit's properties, and return the formalizer + built around it. Called once, after extraction, before the per-unit fan-out.""" + ... + + @dataclass -class PreparedSystem[FormT: BackendResult](ABC): - main: ContractInstance +class PreparedSystem[FormT: BackendResult, U: FeatureUnit, Main](ABC): + #: The located "main" of the analyzed program — the ecosystem's ``Main`` type (EVM's + #: :class:`~composer.spec.system_model.ContractInstance`, Solana's + #: :class:`~composer.spec.solana.model.SolanaProgramInstance`). This is a *different* axis + #: from :class:`FeatureUnit` (the per-unit items ``units()`` iterates): EVM's main is not a + #: unit. The driver treats it opaquely — it only hands it to ``ecosystem.units(main)`` — + #: so each backend binds ``Main`` to its ecosystem's type. + main: Main @abstractmethod - async def prepare_formalization(self, run: PipelineRun) -> Formalizer[FormT]: ... + async def prepare_formalization( + self, run: PipelineRun + ) -> Formalizer[FormT, U] | StagedFormalizer[FormT, U]: + """The formalizer — or, for a backend whose units share an artifact, the + :class:`StagedFormalizer` that becomes one once every unit's properties are known. Which of + the two a backend returns is its own declared signature, so a backend with no shared artifact + never mentions staging at all.""" + ... -class PipelineBackend[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentifier](Protocol): +class PipelineBackend[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentifier, U: FeatureUnit, Main, App: BaseApplication](Protocol): @property def backend_guidance(self) -> str: ... @@ -104,11 +158,11 @@ def core_phases(self) -> CorePhases[P]: ... def artifact_store(self) -> ArtifactStore[A, FormT]: ... async def prepare_system( - self, analyzed: SourceApplication, + self, analyzed: App, run: PipelineRun[P, H] - ) -> PreparedSystem[FormT]: ... + ) -> PreparedSystem[FormT, U, Main]: ... - def to_artifact_id(self, c: ContractComponentInstance) -> A: ... + def to_artifact_id(self, c: U) -> A: ... # ---- shared helpers (the de-duplicated cache keys + batch) ------------------- @@ -116,26 +170,19 @@ def PROPERTIES_KEY(nm: str): return CacheKey[None, Properties](nm) -def main_instance(app: AnyApplication, source: SourceCode) -> ContractInstance: - """Locate the application's main contract — the one whose solidity identifier matches - ``source.contract_name`` — and return a ``ContractInstance`` pointing at it. Backends call this - from ``prepare_system`` to seed the per-component loop; component analysis should already have - guaranteed the contract is present (via ``expected_main_id``).""" - for i, c in enumerate(app.contract_components): - if c.solidity_identifier == source.contract_name: - return ContractInstance(i, app) - raise ValueError(f"main contract {source.contract_name!r} not found in analyzed application") - - @dataclass -class _Batch(BackendJob): +class _Batch[U: FeatureUnit](BackendJob[U]): feat_ctx: WorkflowContext[ComponentGroup] -def _component_cache_key(c: ContractComponentInstance) -> CacheKey[Properties, ComponentGroup]: - return CacheKey(string_hash("|".join([c.app.model_dump_json(), str(c.ind), str(c._contract.ind)]))) +def _component_cache_key(c: FeatureUnit) -> CacheKey[Properties, ComponentGroup]: + # ``cache_material`` is the ecosystem-agnostic view of what identifies a unit; EVM's + # implementation reproduces the previous inline key (app JSON | ind | contract ind) exactly. + return CacheKey(string_hash(c.cache_material())) -def _batch_cache_key[FormT: BaseModel](props: list[PropertyFormulation]) -> CacheKey[ComponentGroup, FormT]: +def _batch_cache_key[FormT: BackendResult]( + props: list[PropertyFormulation], +) -> CacheKey[ComponentGroup, FormT]: # pyright: ignore[reportInvalidTypeVarUse] return CacheKey(string_hash("|".join(p.model_dump_json() for p in props))) @@ -147,28 +194,34 @@ def formalize_task_id(idx: int) -> str: return f"formalize-{idx}" # ---- the driver -------------------------------------------------------------- -async def run_pipeline[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentifier]( - backend: PipelineBackend[P, FormT, H, A], +async def run_pipeline[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentifier, U: FeatureUnit, Main, App: BaseApplication]( + backend: PipelineBackend[P, FormT, H, A, U, Main, App], run: PipelineRun[P, H], *, interactive: bool = False, threat_model: Document | None = None, max_bug_rounds: int = 3, + ecosystem: Ecosystem[App, Main, U], ) -> CorePipelineResult[FormT]: spec, phases = backend.analysis_spec, backend.core_phases source = run.source - # 1. System analysis (shared primitive, backend-parameterized; always yields SourceApplication). + assert ecosystem.supports_greenfield or run.env.sort != "greenfield", ( + f"ecosystem {ecosystem.name!r} has no greenfield prompts; got sort='greenfield'" + ) + + # 1. System analysis (shared primitive; the ecosystem supplies the analyzed model type, + # prompts, validation, and front-matter — EVM reproduces prior behavior exactly). analyzed = await run.runner( TaskInfo(SYSTEM_ANALYSIS_TASK_ID, "System Analysis", phases["analysis"]), lambda: run_component_analysis( - ty=SourceApplication, child_ctxt=run.ctx.child(CacheKey(spec.analysis_key)), - input=source, env=run.env, extra_input=[ - f"The main entry point of this application has been explicitly identified as {source.contract_name} at relative path {source.relative_path}. " - "Your output MUST contain an explicit contract instance with this solidity identifier.", - *spec.extra_input - ], + ty=ecosystem.system_model, child_ctxt=run.ctx.child(CacheKey(spec.analysis_key)), + input=source, env=run.env, + extra_input=[*ecosystem.analysis_extra_input(source), *spec.extra_input], expected_main_id=source.contract_name, + system_template=ecosystem.analysis_prompts.system, + initial_template=ecosystem.analysis_prompts.initial, + validate=ecosystem.validate_analysis, ), ) if analyzed is None: @@ -179,32 +232,39 @@ async def run_pipeline[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentif # 3. Pre-formalization setup runs CONCURRENTLY with extraction (neither needs the other) — # this preserves the prover's autosetup ∥ bug-analysis overlap, generically. - formalizer_task = asyncio.create_task(prepared.prepare_formalization(run)) + staged_task = asyncio.create_task(prepared.prepare_formalization(run)) - batches = await _extract_all( - backend.analysis_spec.properties_key, + batches: list[_Batch[U]] = await _extract_all( + backend.analysis_spec.properties_key, prepared.main, backend.backend_guidance, run, - phases["extraction"], interactive, threat_model, max_bug_rounds - ) - formalizer = await formalizer_task + phases["extraction"], interactive, threat_model, max_bug_rounds, ecosystem) + staged = await staged_task if not batches: raise ValueError("No properties extracted from any component.") - # 4. Per-component formalization. Caching is core-owned, keyed by the backend's result type. - async def _run(batch: _Batch) -> ComponentOutcome[FormT]: + # 4. A backend whose units share an artifact handed back a ``StagedFormalizer`` instead of a + # formalizer: the artifact is authored HERE — once, from every unit's properties — and the + # formalizer it yields is the only one that exists (see :class:`StagedFormalizer`). + formalizer = ( + await staged.begin(batches, run) if isinstance(staged, StagedFormalizer) else staged + ) + + # 5. Per-component formalization. Caching is core-owned, keyed by the backend's result type. + async def _run(batch: _Batch[U]) -> ComponentOutcome[FormT, U]: result_key = backend.to_artifact_id(batch.feat) backend.artifact_store.write_properties(result_key, batch.props) child : WorkflowContext[FormT] = await batch.feat_ctx.child( - _batch_cache_key(batch.props), {"properties": [p.model_dump() for p in batch.props]}, + _batch_cache_key(batch.props), + {"properties": [p.model_dump() for p in batch.props]}, ) cached_result: FormT | None = await child.cache_get(formalizer.formalized_type) result : FormT | GaveUp if cached_result is None: - label = f"{batch.feat.component.name} ({len(batch.props)} properties)" + label = f"{batch.feat.display_name} ({len(batch.props)} properties)" result : FormT | GaveUp = await run.runner( TaskInfo( - formalize_task_id(batch.feat.ind), - f"{batch.feat.component.name} ({len(batch.props)} properties)", + formalize_task_id(batch.feat.unit_index), + label, phases["formalization"] ), lambda: formalizer.formalize(label, batch.feat, batch.props, child, run), @@ -227,12 +287,12 @@ async def _run(batch: _Batch) -> ComponentOutcome[FormT]: await formalizer.finalize(outcomes, run) - # 5. Report (shared, backend-agnostic). The driver assembles the per-component inputs; backends + # 6. Report (shared, backend-agnostic). The driver assembles the per-component inputs; backends # contribute only synthetic extras (prover: structural invariants). Best-effort: a failure here # never fails the run. inputs = [ ReportComponentInput( - name=o.feat.component.name, + name=o.feat.display_name, props=o.props, formalized=o.result if isinstance(o.result, Delivered) else None, ) @@ -254,34 +314,43 @@ async def _run(batch: _Batch) -> ComponentOutcome[FormT]: return _tally(outcomes) -async def _extract_all[P: enum.Enum, H]( +async def _extract_all[P: enum.Enum, H, Main, U: FeatureUnit]( prop_key: str, - main: ContractInstance, backend_guidance: str, run: PipelineRun[P, H], + main: Main, backend_guidance: str, run: PipelineRun[P, H], phase: P, interactive: bool, threat_model: Document | None, max_rounds: int, -) -> list[_Batch]: + # ``App`` stays ``Any`` here: this helper never touches the analyzed-model axis, only + # ``Main``/``U`` (matching the caller's), so there's nothing to tie it to. + ecosystem: Ecosystem[Any, Main, U], +) -> list[_Batch[U]]: prop_ctx = run.ctx.child(PROPERTIES_KEY(prop_key)) - async def _one(idx: int) -> _Batch | None: - feat = ContractComponentInstance(_contract=main, ind=idx) - feat_ctx = await prop_ctx.child(_component_cache_key(feat), - {"component": feat.component.model_dump()}) + async def _one(feat: U) -> _Batch[U] | None: + feat_ctx = await prop_ctx.child(_component_cache_key(feat), feat.context_tag()) props = await run.runner( - TaskInfo(extract_task_id(idx), feat.component.name, phase), + TaskInfo(extract_task_id(feat.unit_index), feat.display_name, phase), lambda conv: run_property_inference( feat_ctx, run.env, feat, refinement=conv if interactive else None, - threat_model=threat_model, max_rounds=max_rounds, backend_guidance=backend_guidance), + threat_model=threat_model, max_rounds=max_rounds, backend_guidance=backend_guidance, + system_template=ecosystem.property_prompts.system, + initial_template=ecosystem.property_prompts.initial), ) return _Batch(feat, props, feat_ctx) if props else None - got = await asyncio.gather(*[_one(i) for i in range(len(main.contract.components))]) + got = await asyncio.gather(*[_one(u) for u in ecosystem.units(main)]) return [b for b in got if b is not None] -def _tally[FormT: BackendResult](outcomes: list[ComponentOutcome[FormT]]) -> CorePipelineResult[FormT]: +def _tally[FormT: BackendResult, U: FeatureUnit]( + outcomes: list[ComponentOutcome[FormT, U]] +) -> CorePipelineResult[FormT]: failures: list[str] = [] for o in outcomes: if isinstance(o.result, BaseException): - failures.append(f"{o.feat.component.name}: {o.result}") + failures.append(f"{o.feat.display_name}: {o.result}") elif isinstance(o.result, GaveUp): - failures.append(f"{o.feat.component.name}: GAVE_UP: {o.result.reason}") - return CorePipelineResult(len(outcomes), sum(len(o.props) for o in outcomes), outcomes, failures) + failures.append(f"{o.feat.display_name}: GAVE_UP: {o.result.reason}") + # The rollup is unit-agnostic; widen the concrete-unit outcomes to the protocol for storage. + return CorePipelineResult( + len(outcomes), sum(len(o.props) for o in outcomes), + cast(list[ComponentOutcome[FormT, FeatureUnit]], outcomes), failures, + ) diff --git a/composer/pipeline/ecosystem.py b/composer/pipeline/ecosystem.py new file mode 100644 index 00000000..4b85b288 --- /dev/null +++ b/composer/pipeline/ecosystem.py @@ -0,0 +1,429 @@ +"""The ecosystem seam — the *front half* of the pipeline made parametric over the +blockchain/source domain (see ``docs/ecosystem-abstraction.md``). + +An **ecosystem** bundles everything the shared analysis + property-extraction steps need +that is domain-specific: the system-model type they produce, the analysis/property prompt +templates, connectivity validation, the main-unit locator, and the per-unit enumeration. +It factors into a **language** facet (the conventions for reading the *analyzed* program's +source — Solidity, Rust — shared across chains that use the same language) and the **chain** +facet (the platform model + prompts). The language here is that of the *code under analysis*, +not the language the AutoProver backend is implemented in (see :class:`Language`). + +``EVM = SOLIDITY ⊕ evm`` binds the EVM types, prompt templates, ``validate_solidity_connectivity``, +``main_instance``, and unit enumeration into the seam; ``SOLANA = RUST ⊕ solana`` binds the +Solana model + prompts and reuses the shared ``RUST`` language facet. See ``docs/ecosystem-abstraction.md``. +""" + +from dataclasses import dataclass +from typing import Any, Callable, Literal, Mapping, TypedDict + +from composer.spec.context import SourceCode +from composer.spec.code_explorer import CODE_EXPLORER_SYS_PROMPT +from composer.spec.gen_types import TypedTemplate +from composer.spec.prop_inference import ( + PropertyInitialPromptParams, + PropertySystemPromptParams, + PROPERTY_INITIAL_TEMPLATE, + PROPERTY_SYSTEM_TEMPLATE, +) +from composer.spec.system_analysis import ( + AnalysisPromptParams, + ANALYSIS_INITIAL_TEMPLATE, + ANALYSIS_SYSTEM_TEMPLATE, + validate_solidity_connectivity, +) +from composer.spec.system_model import ( + AnyApplication, + BaseApplication, + ContractComponentInstance, + ContractInstance, + FeatureUnit, + SourceApplication, +) +from composer.spec.types import SourceIdentifier +from composer.spec.solana.model import ( + AuthorityInteraction, + SolanaApplication, + SolanaAuthority, + SolanaComponentInstance, + SolanaProgram, + SolanaProgramInstance, +) +from composer.spec.util import FS_FORBIDDEN_READ, slugify_filename + +LanguageTag = Literal["solidity", "rust"] +ChainTag = Literal["evm", "solana", "soroban"] + + +@dataclass(frozen=True) +class PromptPair[SysParams: Mapping[str, Any], InitParams: Mapping[str, Any]]: + """A (system prompt, initial prompt) typed-template pair for one agent — see + :class:`~composer.spec.gen_types.TypedTemplate`. Two type parameters because a pair's system + and initial templates don't always share a kwargs shape (the property-inference system + prompt takes just ``sort``; its initial prompt also takes ``context``/``prior_properties``).""" + + system: TypedTemplate[SysParams] + initial: TypedTemplate[InitParams] + + +@dataclass(frozen=True) +class Language: + """The language of the **code being analyzed** — a facet of the ecosystem, shared by every + chain whose programs are written in it (e.g. the ``rust`` facet is shared by Solana and + Soroban). It drives how the shared front half *reads* the target's source (fs-exclusion + pattern, code-explorer prompt, failure modes).""" + + name: LanguageTag + default_forbidden_read: str + code_explorer_prompt: str + # The j2 partial with this language's vulnerability patterns (overflow, panics, …). Reserved + # for the prompt-fragment split; unused while prompts are still monolithic. + vulnerability_patterns_partial: str | None = None + + +@dataclass(frozen=True) +class Ecosystem[App: BaseApplication, Main, Unit: FeatureUnit]: + """A resolved ecosystem = a chain that carries its language. The driver consumes it to + drive the shared front half without hardcoding any one domain. + + Generic over ``App`` (the analyzed system-model type), ``Main`` (the located main-unit + wrapper), and ``Unit`` (the per-unit item the extraction phase iterates). A backend is + paired with an ecosystem by these types: ``run_pipeline`` ties + ``PipelineBackend[..., App, Main, Unit]`` to ``Ecosystem[App, Main, Unit]``, so the analyzed + model, the main-unit, and the per-unit values flow through without casts. EVM binds + ``(SourceApplication, ContractInstance, ContractComponentInstance)``; Solana binds its own.""" + + name: ChainTag + language: Language + #: The pydantic model the analysis phase produces. + system_model: type[App] + #: Prompts for the system-analysis agent. + analysis_prompts: PromptPair[AnalysisPromptParams, AnalysisPromptParams] + #: Prompts for the per-component property-inference agent. + property_prompts: PromptPair[PropertySystemPromptParams, PropertyInitialPromptParams] + #: Connectivity/shape validation of the analyzed model (retry feedback on failure). + validate_analysis: Callable[[App, SourceIdentifier | None], str | None] + #: Locate the target unit (the "main contract"/program) in the analyzed model. + locate_main: Callable[[App, SourceCode], Main] + #: Enumerate the units the extraction phase infers properties for — one batch per unit. Both + #: ecosystems return one per **component** of the main contract/program: a named cluster of its + #: behavior produced by system analysis (docs/ecosystem-abstraction.md §4). Note this is on the + #: *ecosystem* axis, so every backend paired with a chain inherits the same split — pick it on + #: backend-neutral grounds, and let a backend that wants coarser work aggregate in its + #: ``Formalizer`` instead. + units: Callable[[Main], list[Unit]] + #: Domain-specific front-matter appended to the analysis input (was hardcoded in the driver). + analysis_extra_input: Callable[[SourceCode], list[str | dict]] + #: Whether ``analysis_prompts``/``property_prompts`` have a ``sort == "greenfield"`` branch. + #: Only EVM does (the natspec design-doc-to-Solidity path) — Solana's templates have no + #: greenfield content, so ``run_pipeline`` asserts against this rather than silently rendering + #: a template that never mentions the mode it was asked for. + supports_greenfield: bool + + +#: Names for the two concrete instantiations, so a consumer that is pinned to one chain can say so +#: without respelling the triple (or erasing it to ``Any``). :class:`Ecosystems` declares the same +#: pairing; these are what its fields are typed with. +type EvmEcosystem = Ecosystem[SourceApplication, ContractInstance, ContractComponentInstance] +type SolanaEcosystem = Ecosystem[SolanaApplication, SolanaProgramInstance, SolanaComponentInstance] + + +# --------------------------------------------------------------------------- +# main-unit location +# --------------------------------------------------------------------------- + + +def main_instance(app: AnyApplication, source: SourceCode) -> ContractInstance: + """Locate the application's main contract — the one whose solidity identifier matches + ``source.contract_name`` — and return a ``ContractInstance`` pointing at it. Backends call + this from ``prepare_system`` to seed the per-component loop; component analysis should + already have guaranteed the contract is present (via ``expected_main_id``).""" + for i, c in enumerate(app.contract_components): + if c.solidity_identifier == source.contract_name: + return ContractInstance(i, app) + raise ValueError(f"main contract {source.contract_name!r} not found in analyzed application") + + +# --------------------------------------------------------------------------- +# The EVM ecosystem +# --------------------------------------------------------------------------- + + +def _evm_units(main: ContractInstance) -> list[ContractComponentInstance]: + return [ + ContractComponentInstance(_contract=main, ind=i) + for i in range(len(main.contract.components)) + ] + + +def _evm_analysis_extra_input(source: SourceCode) -> list[str | dict]: + return [ + f"The main entry point of this application has been explicitly identified as " + f"{source.contract_name} at relative path {source.relative_path}. " + "Your output MUST contain an explicit contract instance with this solidity identifier." + ] + + +# Adding Vyper support (a second EVM source language) would, at a very high level: +# 1. Extend ``LanguageTag`` with ``"vyper"`` and add a ``VYPER`` ``Language`` facet here (its +# own ``forbidden_read``, code-explorer prompt, and — eventually — failure-modes partial). +# 2. Bind it to a Vyper-flavored EVM ``Ecosystem`` (its own analysis/property prompts) and +# route to it by detecting the target's source language at the entry point. +# 3. Loosen the analysis model's Solidity assumptions: contracts are keyed by +# ``SolidityIdentifier`` / ``solidity_identifier`` throughout (see ``system_model`` and +# ``main_instance``), which would need to widen to the language-neutral +# ``SourceIdentifier`` the ecosystem seam already speaks. +# The CVL backend needs the least work — the Certora Prover already accepts Vyper (it verifies +# compiled bytecode) — while the Foundry backend is Solidity-only by construction (it authors +# and runs ``.t.sol`` tests), so it would need a separate Vyper story or be left EVM/Solidity-only. +SOLIDITY = Language( + name="solidity", + default_forbidden_read=FS_FORBIDDEN_READ, + code_explorer_prompt=CODE_EXPLORER_SYS_PROMPT, +) + +EVM: EvmEcosystem = Ecosystem( + name="evm", + language=SOLIDITY, + system_model=SourceApplication, + analysis_prompts=PromptPair(ANALYSIS_SYSTEM_TEMPLATE, ANALYSIS_INITIAL_TEMPLATE), + property_prompts=PromptPair(PROPERTY_SYSTEM_TEMPLATE, PROPERTY_INITIAL_TEMPLATE), + validate_analysis=validate_solidity_connectivity, + locate_main=main_instance, + supports_greenfield=True, + units=_evm_units, + analysis_extra_input=_evm_analysis_extra_input, +) + + +# --------------------------------------------------------------------------- +# The RUST language facet (shared by Solana, Soroban) +# --------------------------------------------------------------------------- + +#: Cargo/Anchor project layout: hide build output, VCS, lockfiles, and the JS side; keep the +#: crate sources and `tests/`. (Contrast the Foundry-shaped ``FS_FORBIDDEN_READ``.) +RUST_FORBIDDEN_READ = r"(^target/.*)|(^\.git.*)|(^node_modules/.*)|(.*\.lock$)" +# NOTE: the confined-build scratch dirs (``.sandbox_cargo`` / ``.sandbox_rustup`` / +# ``.sandbox_tmp`` and nested ``target/``) are also excluded, but that extension lives with the +# rust-framework layer that introduces confined Rust builds — no build runs in this front-half, so +# those dirs never exist here. + +RUST_CODE_EXPLORER_PROMPT = """\ +You are a code-exploration assistant analyzing Rust source for on-chain programs (e.g. Solana +/ Anchor). You have file tools (list_files, get_file, grep_files) to explore the project. +Answer the question concretely, citing the relevant items: instruction handlers, account +validation structs (e.g. Anchor `#[derive(Accounts)]`), account/state types, PDA seed +derivations, signer/owner checks, and cross-program invocations. Quote the exact Rust snippets +that establish or omit a check; do not speculate about code you have not read. +""" + +RUST = Language( + name="rust", + default_forbidden_read=RUST_FORBIDDEN_READ, + code_explorer_prompt=RUST_CODE_EXPLORER_PROMPT, + vulnerability_patterns_partial="rust/_vulnerability_patterns.j2", +) + + +# --------------------------------------------------------------------------- +# The Solana chain (RUST ⊕ solana) +# --------------------------------------------------------------------------- + + +def _validate_program_components(prog: SolanaProgram) -> list[str]: + """One program's :class:`ProgramComponent` checks — the peer of the component half of EVM's + ``validate_solidity_connectivity`` (``docs/ecosystem-abstraction.md`` §4, "Validation"). + + Name and slug uniqueness mirror EVM directly. The component↔instruction mapping check has no + EVM peer and is the one deliberate divergence: EVM's ``external_entry_points`` are prose the + prompt renders, while a Solana component's ``instructions`` are *references* that resolve into + the program (the unit wrapper turns them back into ``SolanaInstruction`` objects). A dangling + name would silently drop an instruction's account/constraint detail from the extraction + prompt, and an *unreferenced* instruction is an entry point no property will ever cover — so + the mapping is required to be both valid and total. It costs two set operations.""" + errors: list[str] = [] + seen: set[str] = set() + slug_origin: dict[str, str] = {} + for comp in prog.components: + if comp.name in seen: + errors.append(f"Duplicate component names in {prog.name}: {comp.name}") + seen.add(comp.name) + slug = slugify_filename(comp.name) + if slug in slug_origin: + errors.append( + f"Components {slug_origin[slug]!r} and {comp.name!r} in {prog.name} both reduce " + f"to the filename slug {slug!r} (punctuation and symbols are normalized to " + f"underscores); give them names that differ in more than that." + ) + else: + slug_origin[slug] = comp.name + for ins_name in comp.instructions: + if ins_name not in prog.instructions_by_name: + errors.append( + f"Component {comp.name!r} of {prog.name} lists an instruction {ins_name!r} " + f"that {prog.name} does not declare." + ) + referenced = {n for comp in prog.components for n in comp.instructions} + unassigned = [i.name for i in prog.instructions if i.name not in referenced] + if unassigned: + errors.append( + f"Instruction(s) {', '.join(repr(n) for n in unassigned)} of {prog.name} belong to no " + f"component; every instruction must appear in at least one component's `instructions` " + f"(an instruction may appear in more than one)." + ) + return errors + + +def _solana_validate(app: SolanaApplication, expected_main: SourceIdentifier | None) -> str | None: + """Connectivity/shape validation for a ``SolanaApplication`` (retry feedback on failure). + + Typed over ``SolanaApplication``, not ``BaseApplication``: ``Ecosystem.validate_analysis`` is + ``Callable[[App, ...]]``, so the seam already guarantees the model came from *this* ecosystem's + ``system_model``. An earlier version narrowed at runtime and returned ``None`` for a foreign + application; that silently passed a model this function cannot check, and the parameter type is + what makes the case unreachable instead. + Mirrors the EVM ``validate_solidity_connectivity`` structure: unique program identifiers and names, + unique instruction slugs within a program, unique component names/slugs within a program, the + component↔instruction mapping valid and total, component interactions resolving, and the + expected main program present.""" + errors: list[str] = [] + known_identifiers: set[str] = set() + # Program NAME -> its component names. Keyed by name (not identifier) because that is what an + # interaction names, exactly as EVM keys by contract name. + known_components: dict[str, set[str]] = {} + programs = [c for c in app.components if isinstance(c, SolanaProgram)] + known_authorities = {c.name for c in app.components if isinstance(c, SolanaAuthority)} + for prog in programs: + if prog.program_identifier in known_identifiers: + errors.append(f"Duplicate program identifier: {prog.program_identifier}") + known_identifiers.add(prog.program_identifier) + if prog.name in known_components: + errors.append(f"Duplicate program names: {prog.name}") + known_components.setdefault(prog.name, set()).update(c.name for c in prog.components) + slug_origin: dict[str, str] = {} + for ins in prog.instructions: + slug = slugify_filename(ins.name) + if slug in slug_origin: + errors.append( + f"Instructions {slug_origin[slug]!r} and {ins.name!r} in {prog.name} " + f"reduce to the same filename slug {slug!r}; give them more-distinct names." + ) + slug_origin[slug] = ins.name + # An instruction may call into another program (Solana's version of one + # contract calling another). That target is often a standard program every + # app uses (e.g. the token or system program) that the model author never + # bothered to declare, so we don't flag undeclared call targets here. A + # future policy could require them to match known_programs | known_authorities + # | an allowlist. + errors.extend(_validate_program_components(prog)) + + # Interactions, in a second pass so a component may name one declared later (EVM does the same). + # Unlike the CPI-target leniency above, these ARE required to resolve: the analysis prompt tells + # the model to declare every external actor it interacts with, including SPL Token / System. + for prog in programs: + for comp in prog.components: + where = f"Component {comp.name} of {prog.name} interacts with" + for inter in comp.interactions: + if isinstance(inter, AuthorityInteraction): + if inter.authority not in known_authorities: + errors.append(f"{where} unknown external authority: {inter.authority}") + elif inter.program not in known_components: + errors.append(f"{where} an unknown program: {inter.program}") + elif inter.component and inter.component not in known_components[inter.program]: + errors.append( + f"{where} unknown component {inter.component} of program {inter.program}" + ) + + if expected_main is not None and expected_main not in known_identifiers: + errors.append( + f"Expected a program with identifier {expected_main!r}; declared programs: " + f"{sorted(known_identifiers) or '(none)'}." + ) + if not errors: + return None + + # The declared-names reference block (EVM peer): every error above is a name that failed to + # resolve, so the retry is far more likely to land if it can see the vocabulary it submitted. + def _fmt(items: set[str]) -> str: + return ", ".join(sorted(items)) if items else "(none)" + + reference_lines = [ + f"- Declared programs: {_fmt(set(known_components))}", + f"- Declared external authorities: {_fmt(known_authorities)}", + ] + for prog_name, comps in sorted(known_components.items()): + reference_lines.append(f"- Components of {prog_name}: {_fmt(comps)}") + reference = ( + "\n\nFor reference, the names you declared in your submission:\n" + "\n".join(reference_lines) + ) + + if len(errors) == 1: + return errors[0] + reference + return ( + "Multiple validation errors; fix all before resubmitting:\n" + + "\n".join(f"- {e}" for e in errors) + + reference + ) + + +def _solana_locate_main(app: SolanaApplication, source: SourceCode) -> SolanaProgramInstance: + for i, prog in enumerate(app.programs): + if prog.program_identifier == source.contract_name: + return SolanaProgramInstance(i, app) + raise ValueError(f"main program {source.contract_name!r} not found in analyzed application") + + +def _solana_units(main: SolanaProgramInstance) -> list[SolanaComponentInstance]: + # One unit per component of the MAIN program — the exact shape of ``_evm_units`` (which + # enumerates the main *contract's* components; siblings are context, not units). Replaces the + # whole-program singleton this returned before: one extraction agent for a 62-instruction + # program is a hard cap on depth, and the unit was a Crucible cost decision sitting on a + # backend-neutral seam. See docs/ecosystem-abstraction.md §1 (the two axes) and §4. + return [ + SolanaComponentInstance(ind=i, _program=main) + for i in range(len(main.program.components)) + ] + + +def _solana_analysis_extra_input(source: SourceCode) -> list[str | dict]: + return [ + f"The main program of this application has been explicitly identified as " + f"{source.contract_name} at relative path {source.relative_path}. " + "Your output MUST contain a program whose program_identifier is this exact identifier." + ] + + +# Per-component units, mirroring EVM: ``Main`` is the located program, ``Unit`` is one of its +# ``ProgramComponent``s. Every Solana backend inherits this split — Crucible today, a CVLR backend +# later — which is why it is chosen on backend-neutral grounds (docs/ecosystem-abstraction.md §4). +SOLANA: SolanaEcosystem = Ecosystem( + name="solana", + language=RUST, + system_model=SolanaApplication, + analysis_prompts=PromptPair( + TypedTemplate[AnalysisPromptParams]("solana/analysis_system.j2"), + TypedTemplate[AnalysisPromptParams]("solana/analysis_prompt.j2"), + ), + property_prompts=PromptPair( + TypedTemplate[PropertySystemPromptParams]("solana/property_system.j2"), + TypedTemplate[PropertyInitialPromptParams]("solana/property_prompt.j2"), + ), + validate_analysis=_solana_validate, + locate_main=_solana_locate_main, + supports_greenfield=False, + units=_solana_units, + analysis_extra_input=_solana_analysis_extra_input, +) + + +class Ecosystems(TypedDict): + """Registry of available ecosystems, keyed by chain tag. The set is closed (a new chain + means a new field here, not a new dict entry), so a ``TypedDict`` gives each entry its own + concrete ``Ecosystem[App, Main, Unit]`` instead of erasing all of them to + ``Ecosystem[Any, Any, Any]``.""" + + evm: EvmEcosystem + solana: SolanaEcosystem + + +ECOSYSTEMS: Ecosystems = {"evm": EVM, "solana": SOLANA} diff --git a/composer/pipeline/ptypes.py b/composer/pipeline/ptypes.py index e665c790..fbf1a18a 100644 --- a/composer/pipeline/ptypes.py +++ b/composer/pipeline/ptypes.py @@ -13,7 +13,7 @@ ) from composer.spec.service_host import ServiceHost from composer.spec.system_model import ( - ContractComponentInstance + FeatureUnit, ) from composer.spec.types import PropertyFormulation, FormalResult from composer.spec.source.report.collect import ReportableResult @@ -63,16 +63,21 @@ class CorePhases[P: enum.Enum](TypedDict): @dataclass(frozen=True) class SystemAnalysisSpec: - """The backend's contribution to the shared analysis call. The analyzed type is always - SourceApplication (the prover's harnessed lift is its prepare_system, not analysis).""" + """The backend's contribution to the shared analysis call. The analyzed type is the + ecosystem's ``App`` (SourceApplication for EVM; the prover's harnessed lift is its + prepare_system, not analysis).""" analysis_key: str properties_key: str extra_input: list[str | dict] = field(default_factory=list) @dataclass -class BackendJob: - feat: ContractComponentInstance +class BackendJob[U: FeatureUnit]: + # ``U`` is the *formalized unit* type the paired backend consumes (EVM's + # ``ContractComponentInstance``, Solana's invariant unit, …) — see ``FeatureUnit``. The shared + # driver is generic over it; a backend narrows it to its concrete unit and reads its members + # without casts. + feat: U props: list[PropertyFormulation] @dataclass(frozen=True) @@ -94,14 +99,16 @@ def run_link(self) -> str | None: return self.result.output_link @dataclass -class ComponentOutcome[FormT: BackendResult](BackendJob): +class ComponentOutcome[FormT: BackendResult, U: FeatureUnit](BackendJob[U]): result: Delivered[FormT] | GaveUp | BaseException @dataclass class CorePipelineResult[FormT: BackendResult]: + # The result rollup is unit-agnostic — it only reads ``feat.display_name`` (a ``FeatureUnit`` + # member) — so it stays mono in the unit type and widens the outcomes to the protocol. n_components: int n_properties: int - outcomes: list[ComponentOutcome[FormT]] + outcomes: list[ComponentOutcome[FormT, FeatureUnit]] failures: list[str] @property diff --git a/composer/spec/context.py b/composer/spec/context.py index 623c3f9c..3ebbb36c 100644 --- a/composer/spec/context.py +++ b/composer/spec/context.py @@ -20,7 +20,7 @@ from composer.input.files import Document from composer.io.mnemonic_store import assign_mnemonic from composer.core.user import user_data_ns -from composer.spec.system_model import SolidityIdentifier +from composer.spec.types import SourceIdentifier # --------------------------------------------------------------------------- @@ -37,12 +37,12 @@ class SystemDoc: class SourceFields: """Input when source code is also available (source_spec). - ``contract_name`` is the Solidity identifier of the main contract being + ``contract_name`` is the source identifier of the main contract/program being verified — the ```` half of the ``--main-contract path:Name`` CLI - argument. + argument (a Solidity identifier on EVM, a program identifier on Solana). """ project_root: str - contract_name: SolidityIdentifier + contract_name: SourceIdentifier relative_path: str forbidden_read: str diff --git a/composer/spec/natspec/pipeline.py b/composer/spec/natspec/pipeline.py index b69e9329..31d61487 100644 --- a/composer/spec/natspec/pipeline.py +++ b/composer/spec/natspec/pipeline.py @@ -32,6 +32,7 @@ from composer.io.multi_job import ( TaskInfo, HandlerFactory, run_task, ) +from composer.pipeline.ecosystem import EvmEcosystem from composer.spec.context import ( WorkflowContext, @@ -39,7 +40,7 @@ Contract ) from composer.spec.util import string_hash -from composer.spec.prop_inference import run_property_inference +from composer.spec.prop_inference import CERTORA_BACKEND_GUIDANCE, run_property_inference from composer.spec.types import PropertyFormulation from composer.spec.natspec.interface_gen import generate_interface, DESCRIPTION as INTERFACE_GEN_DESC from composer.spec.natspec.stub_gen import generate_stub @@ -166,6 +167,9 @@ class PipelineServices: env: ServiceHost mental_model: MentalModel file_registry: FileRegistry + # Consumed for its prompt pairs only; pinned to EVM because everything else in this pipeline + # is Solidity-only (solc, CVL, stub/interface generation). + ecosystem: EvmEcosystem # When True, the bug-analysis step opens a per-component conversation # channel via the TUI's switcher so the user can refine the extracted # property list interactively. Parallel components each get their own @@ -239,6 +243,9 @@ async def _analyze_component(component_idx: int) -> _ComponentBatch | None: system_doc.content.to_dict(), ], max_rounds=services.max_bug_rounds, + backend_guidance=CERTORA_BACKEND_GUIDANCE, + system_template=services.ecosystem.property_prompts.system, + initial_template=services.ecosystem.property_prompts.initial, ), semaphore, ) @@ -401,6 +408,7 @@ async def run_natspec_pipeline[A: NatspecApplication, I: InterfaceDeclModel, S: mental_model: MentalModel[A, I, S], source_factory: ToolGenerator, *, + ecosystem: EvmEcosystem, max_concurrent: int = 4, interactive: bool = False, max_bug_rounds: int = 3, @@ -430,6 +438,7 @@ async def run_natspec_pipeline[A: NatspecApplication, I: InterfaceDeclModel, S: store: BaseStore for shared artifacts and caching. handler_factory: Creates per-task ``(IOHandler, EventHandler)`` pairs. Called once per top-level agent invocation. + ecosystem: Supplies the analysis and property prompt pairs. max_concurrent: Maximum concurrent LLM agents. """ semaphore = asyncio.Semaphore(max_concurrent) @@ -446,7 +455,7 @@ async def run_natspec_pipeline[A: NatspecApplication, I: InterfaceDeclModel, S: summary = await run_task( handler_factory, TaskInfo("component-analysis", SYSTEM_DESC, Phase.COMPONENT_ANALYSIS), - lambda: run_component_analysis(ctx, system_doc, curr_env, mental_model), + lambda: run_component_analysis(ctx, system_doc, curr_env, mental_model, ecosystem), ) if summary is None: raise ValueError("Component analysis produced no result — is the system doc empty?") @@ -552,6 +561,7 @@ async def gen_one_stub( factory=handler_factory, mental_model=mental_model, file_registry=file_registry, + ecosystem=ecosystem, interactive=interactive, max_bug_rounds=max_bug_rounds, ) diff --git a/composer/spec/natspec/system_analysis.py b/composer/spec/natspec/system_analysis.py index 83a99624..935cc139 100644 --- a/composer/spec/natspec/system_analysis.py +++ b/composer/spec/natspec/system_analysis.py @@ -1,12 +1,16 @@ from typing import Any +from composer.pipeline.ecosystem import EvmEcosystem from composer.spec.context import ( WorkflowContext, CacheKey, SystemDoc ) from composer.spec.natspec.task_description import MentalModel from composer.spec.system_model import NatspecApplication -from composer.spec.system_analysis import run_component_analysis as wrapped_analysis +from composer.spec.system_analysis import ( + run_component_analysis as wrapped_analysis, + validate_solidity_connectivity, +) from composer.spec.service_host import ServiceHost @@ -22,6 +26,7 @@ async def run_component_analysis[A: NatspecApplication]( input: SystemDoc, tools: ServiceHost, mental_model: MentalModel[A, Any, Any], + ecosystem: EvmEcosystem, ) -> A | None: """Analyze application components from a system doc and optionally source code. @@ -34,5 +39,8 @@ async def run_component_analysis[A: NatspecApplication]( child_ctxt=context.child(source_analysis_key(mental_model)), env=tools, extra_input=[], - input=input + input=input, + system_template=ecosystem.analysis_prompts.system, + initial_template=ecosystem.analysis_prompts.initial, + validate=validate_solidity_connectivity, ) diff --git a/composer/spec/prop_inference.py b/composer/spec/prop_inference.py index 3edc92c0..e5dfdd0b 100644 --- a/composer/spec/prop_inference.py +++ b/composer/spec/prop_inference.py @@ -4,7 +4,7 @@ Parameterized by source availability via AnalysisInput tuple. """ -from typing import Any, Callable, NotRequired, override, Literal, Sequence +from typing import Any, Callable, NotRequired, TypedDict, override, Literal, Sequence import re from difflib import SequenceMatcher from pydantic import BaseModel, Field @@ -19,9 +19,10 @@ from composer.input.files import Document from composer.spec.context import WorkflowContext, CacheKey, ComponentGroup +from composer.spec.gen_types import TypedTemplate from composer.spec.graph_builder import bind_standard, run_to_completion from composer.spec.types import PropertyFormulation -from composer.spec.system_model import ContractComponentInstance +from composer.spec.system_model import FeatureUnit from composer.tools.thinking import RoughDraftState, get_rough_draft_tools from composer.spec.service_host import Sort, ServiceHost from composer.io.conversation import ConversationContextProvider @@ -50,6 +51,24 @@ class _AgentRoundResult(_BugAnalysisCache): "understand your reasoning. Be specific." ) +class PropertySystemPromptParams(TypedDict): + """Kwargs for the property-extraction agent's system prompt template.""" + sort: Sort + + +class PropertyInitialPromptParams(TypedDict): + """Kwargs for the property-extraction agent's initial prompt template.""" + context: FeatureUnit + backend_guidance: str + sort: Sort + prior_properties: list[_AgentRoundResult] + + +#: The EVM/Solidity property prompts. +PROPERTY_SYSTEM_TEMPLATE = TypedTemplate[PropertySystemPromptParams]("property_analysis_system_prompt.j2") +PROPERTY_INITIAL_TEMPLATE = TypedTemplate[PropertyInitialPromptParams]("property_analysis_prompt.j2") + + class _AgentRoundWithHistory(_AgentRoundResult): agent_conversation: list[AnyMessage] @@ -101,18 +120,18 @@ class RefinementState(MessagesState): def _get_initial_prompt( - context: ContractComponentInstance, + context: FeatureUnit, sort: Sort, prev_results: list[_AgentRoundResult], backend_guidance: str, + template: TypedTemplate[PropertyInitialPromptParams], ) -> str: - return load_jinja_template( - "property_analysis_prompt.j2", - context=context, - backend_guidance=backend_guidance, - sort=sort, - prior_properties=prev_results - ) + return template.bind({ + "context": context, + "backend_guidance": backend_guidance, + "sort": sort, + "prior_properties": prev_results, + }).render_to(load_jinja_template) @tool_display("Ending conversation...", None) class Exit(WithImplementation[str]): @@ -279,12 +298,14 @@ def validate(_state: Any, result: _AgentRoundResult) -> str | None: async def _run_bug_round( env: ServiceHost, - component: ContractComponentInstance, + component: FeatureUnit, front_matter_items: Sequence[str | dict], ctx: WorkflowContext[_AgentResult], round: int, prev: list[_AgentRoundResult], backend_guidance: str, + system_template: TypedTemplate[PropertySystemPromptParams], + initial_template: TypedTemplate[PropertyInitialPromptParams], ) -> _AgentRoundWithHistory: round_ctx = ctx.child(agent_round_key(round)) if (cached := await round_ctx.cache_get(_AgentRoundWithHistory)) is not None: @@ -305,13 +326,13 @@ class ST(MessagesState, RoughDraftState): ).with_input( BugAnalysisInput ).with_initial_prompt( - _get_initial_prompt(component, env.sort, prev, backend_guidance) + _get_initial_prompt(component, env.sort, prev, backend_guidance, initial_template) ).with_tools( get_rough_draft_tools(ST) ).with_tools( env.analysis_tools - ).with_sys_prompt_template( - "property_analysis_system_prompt.j2", sort=env.sort + ).inject( + lambda g: system_template.bind({"sort": env.sort}).render_to(g.with_sys_prompt_template) ).compile_async() flow_input: BugAnalysisInput = BugAnalysisInput( @@ -341,11 +362,13 @@ class ST(MessagesState, RoughDraftState): async def _run_bug_analysis_inner( agent_component_analysis: WorkflowContext[_AgentResult], env: ServiceHost, - component: ContractComponentInstance, + component: FeatureUnit, extra_input: Sequence[str | dict], threat_model: Document | None, max_rounds: int, backend_guidance: str, + system_template: TypedTemplate[PropertySystemPromptParams], + initial_template: TypedTemplate[PropertyInitialPromptParams], ) -> _AgentResult: if (cached := await agent_component_analysis.cache_get(_AgentResult)) is not None: return cached @@ -367,7 +390,7 @@ async def _run_bug_analysis_inner( for i in range(0, max_rounds): next_result = await _run_bug_round( env, component, front_matter_items, agent_component_analysis, i, prev_rounds, - backend_guidance, + backend_guidance, system_template, initial_template, ) if len(next_result.items) == 0: assert last_round_convo is not None @@ -389,22 +412,22 @@ async def _run_bug_analysis_inner( async def run_property_inference( ctx: WorkflowContext[ComponentGroup], env: ServiceHost, - component: ContractComponentInstance, + component: FeatureUnit, extra_input : Sequence[str | dict] = tuple(), threat_model: Document | None = None, refinement: ConversationContextProvider | None = None, max_rounds: int = 3, - backend_guidance: str = CERTORA_BACKEND_GUIDANCE, + *, + backend_guidance: str, + system_template: TypedTemplate[PropertySystemPromptParams], + initial_template: TypedTemplate[PropertyInitialPromptParams], ) -> list[PropertyFormulation]: """ Extract security properties for a component. - ``backend_guidance`` is inlined verbatim into the property-analysis - prompt as the "what's expressible in your downstream verification - tool" filter. Defaults to ``CERTORA_BACKEND_GUIDANCE`` so existing - callers (the autoprove pipeline) get the same prompt they always had; - other backends (e.g. foundry tests) pass their own string describing - what's a fit / not a fit for *their* verification surface. + ``backend_guidance`` is inlined verbatim into the property-analysis prompt as the "what's + expressible in your downstream verification tool" filter — the Certora Prover, foundry + tests, each describing what is and isn't a fit for *their* verification surface. """ component_analysis = ctx.child(bug_analysis_key(threat_model, refinement is not None)) @@ -419,6 +442,8 @@ async def run_property_inference( threat_model, max_rounds=max_rounds, backend_guidance=backend_guidance, + system_template=system_template, + initial_template=initial_template, ) if refinement is None: to_ret = agent_attempt.items diff --git a/composer/spec/solana/__init__.py b/composer/spec/solana/__init__.py new file mode 100644 index 00000000..8cc5e84a --- /dev/null +++ b/composer/spec/solana/__init__.py @@ -0,0 +1,10 @@ +"""Solana ecosystem: system model + (in the ecosystem module) prompts and wiring. + +The Solana chain of the ecosystem abstraction (see docs/ecosystem-abstraction.md). This +package holds the Solana-native system model the shared analysis phase produces +(``SolanaApplication`` — programs, their instructions, and the ``ProgramComponent`` +capabilities grouping them) and the index-wrapper instances the driver iterates +(``SolanaProgramInstance`` / ``SolanaComponentInstance``, the latter satisfying the +``FeatureUnit`` protocol). The ecosystem object that binds these + the Rust language facet + +the Solana prompts lives in ``composer/pipeline/ecosystem.py``. +""" diff --git a/composer/spec/solana/model.py b/composer/spec/solana/model.py new file mode 100644 index 00000000..e9c460ae --- /dev/null +++ b/composer/spec/solana/model.py @@ -0,0 +1,316 @@ +"""The Solana system model — the standalone analog of the EVM ``SourceApplication``. + +Where the EVM model is contracts → components with storage variables and external functions, +Solana is **programs → instructions** that operate on **accounts passed in by the caller** +(there is no per-contract owned storage; state lives in accounts the instruction validates +and mutates). The model captures that shape natively — accounts + their signer/owner/PDA +constraints, cross-program invocations (CPIs), and the authorities involved — rather than +reusing the EVM field names. + +Programs additionally carry :class:`ProgramComponent`\\ s — the Solana analog of EVM's +``ContractComponent``: named *capabilities*, each a semantic cluster of instructions plus the +account state they maintain. A component **references** its instructions by name; the program's +flat ``instructions`` list stays authoritative. See ``docs/ecosystem-abstraction.md`` §4. + +``SolanaApplication`` is what the shared analysis phase produces (it is a ``BaseApplication`` +so ``run_component_analysis`` accepts it). ``SolanaProgramInstance`` / ``SolanaComponentInstance`` +are the driver's ``Main`` / ``Unit`` — thin index wrappers over the model, mirroring EVM's +``ContractInstance`` / ``ContractComponentInstance``, with the component instance satisfying the +ecosystem-agnostic ``FeatureUnit`` protocol so the shared driver's cache keys / task ids / labels +work unchanged. +""" + +from dataclasses import dataclass +from functools import cached_property +from typing import Literal + +from pydantic import BaseModel, Field + +from composer.spec.system_model import BaseApplication +from composer.spec.types import ComponentName, ProgramName, RustIdentifier +from composer.spec.util import slugify_filename + +#: How an account is expected to be supplied to an instruction. Drives the "missing signer / +#: owner check" and "account substitution" reasoning in the property prompt. +AccountRole = Literal["signer", "writable", "readonly", "pda", "program", "sysvar"] + + +class AccountConstraint(BaseModel): + """One account an instruction expects in its accounts context, plus the constraints the + program is responsible for enforcing on it.""" + + name: str = Field(description="The account's name in the instruction's accounts struct/context.") + account_type: str = Field( + description="The account's declared type (e.g. 'Signer', 'Account', 'Program', " + "'SystemAccount', 'UncheckedAccount', a PDA of some seeds)." + ) + roles: list[AccountRole] = Field( + default_factory=list, + description="Roles this account plays: signer / writable / readonly / pda / program / sysvar.", + ) + constraints: list[str] = Field( + default_factory=list, + description="Validations the program must enforce on this account — e.g. Anchor " + "constraints (has_one, seeds+bump, address, owner), an explicit owner/signer check, or " + "a documented invariant. Empty means the program performs no checks (often a finding).", + ) + + +class CpiCall(BaseModel): + """A cross-program invocation the instruction makes.""" + + target_program: str = Field(description="The program invoked (name or program id).") + description: str = Field(description="What the CPI does and any authority/PDA-signer it uses.") + + +class SolanaInstruction(BaseModel): + """A single instruction (entry point) of a program.""" + + name: str = Field(description="The instruction's snake_case name (its handler function).") + description: str = Field(description="What the instruction does, at the behavioral level (not how).") + accounts: list[AccountConstraint] = Field( + default_factory=list, description="The accounts the instruction takes and their constraints." + ) + signers: list[str] = Field( + default_factory=list, + description="Which accounts must sign (authorities/owners the instruction authenticates).", + ) + cpis: list[CpiCall] = Field( + default_factory=list, description="Cross-program invocations this instruction performs." + ) + args: list[str] = Field( + default_factory=list, description="The instruction's non-account arguments (name & type)." + ) + requirements: list[str] = Field( + description="Natural-language behavioral requirements — the instruction's specification." + ) + + +class InterComponentInteraction(BaseModel): + """An interaction with another component of a program this application implements. + + The Solana peer of :class:`composer.spec.system_model.ComponentInteraction`; keyed by + ``ProgramName`` rather than ``ContractName``""" + + program: ProgramName = Field( + description="The conceptual name of the program interacted with (matching the `name` field " + "of a program in this application)." + ) + component: ComponentName | None = Field( + description="The specific component within that program interacted with, if identifiable." + ) + description: str = Field(description="A description of the interaction with that component.") + + +class AuthorityInteraction(BaseModel): + """An interaction with an external authority/actor — an admin keypair, an off-chain signer, or + a program the application does not itself implement (SPL Token, the System program, an oracle). + + The Solana peer of :class:`composer.spec.system_model.ExternalDependency`.""" + + authority: str = Field( + description="The name of the external authority/actor interacted with (matching the `name` " + "field of an external authority in this application)." + ) + description: str = Field(description="A description of the interaction with that actor.") + + +type ComponentInteraction = InterComponentInteraction | AuthorityInteraction + + +class ProgramComponent(BaseModel): + """A single major "component" of a program — a named *capability*: a semantic cluster of the + program's instructions together with the account state they maintain. + + The Solana analog of :class:`composer.spec.system_model.ContractComponent`, field for field + (``external_entry_points`` → ``instructions``, ``state_variables`` → ``account_types``). Like + its EVM peer it **references, it does not own**: ``instructions`` and ``account_types`` are + lists of *names* resolving into the owning :class:`SolanaProgram`, which stays the single + source of truth for the rich per-instruction data. An instruction may appear in more than one + component when it genuinely serves two capabilities. See ``docs/ecosystem-abstraction.md`` + §4.""" + + name: ComponentName = Field(description="A short, concise name of the component") + description: str = Field( + description="A longer description describing *what* this component does, not *how* it does it." + ) + instructions: list[str] = Field( + description="The names of this program's instructions that make up this component. Each " + "must match the `name` of an instruction declared on the program." + ) + account_types: list[str] = Field( + description="The account/state types this component maintains. Each must match one of the " + "program's declared `account_types`." + ) + interactions: list[ComponentInteraction] = Field( + description="Interactions with other components described in this system, or with external " + "authorities/actors." + ) + requirements: list[str] = Field( + description="Natural-language requirements for this component — its behavioral specification." + ) + + +class SolanaProgram(BaseModel): + """A concrete on-chain program in the system.""" + + name: ProgramName = Field( + description="A short conceptual name for the program, used to refer to it across the system." + ) + program_identifier: RustIdentifier = Field( + pattern=r"^[a-zA-Z_][a-zA-Z0-9_]*$", + description="The program's Rust crate/module identifier as it appears in source. A valid " + "Rust identifier (snake_case).", + ) + program_id: str | None = Field( + default=None, description="The on-chain program id (base58), if declared (e.g. declare_id!)." + ) + description: str = Field(description="The program's role in the system.") + instructions: list[SolanaInstruction] = Field(description="The program's instructions.") + account_types: list[str] = Field( + default_factory=list, + description="The account/state types this program owns and derives (PDAs), name & purpose.", + ) + components: list[ProgramComponent] = Field( + description="The capabilities making up this program — semantic clusters of its " + "instructions. Every instruction must belong to at least one component." + ) + + @cached_property + def instructions_by_name(self) -> dict[str, SolanaInstruction]: + """The program's instructions keyed by name — how a :class:`ProgramComponent`'s + ``instructions`` name list resolves to the real objects. Shared by the analysis validator + and the unit wrapper so neither re-derives the lookup.""" + return {i.name: i for i in self.instructions} + + +class SolanaAuthority(BaseModel): + """An external actor: a signer/authority, an off-chain keypair, or another program the + system interacts with but does not itself implement.""" + + name: str = Field(description="A short unique identifier for this authority/actor.") + description: str = Field(description="A short technical description.") + assumptions: list[str] = Field( + default_factory=list, description="Assumptions about this actor's behavior/trust." + ) + + +type SolanaComponent = SolanaProgram | SolanaAuthority + + +class SolanaApplication(BaseApplication[SolanaComponent]): + """A Solana application: a set of programs (+ external authorities).""" + + @cached_property + def programs(self) -> list[SolanaProgram]: + return [c for c in self.components if isinstance(c, SolanaProgram)] + + @cached_property + def authorities(self) -> list[SolanaAuthority]: + return [c for c in self.components if isinstance(c, SolanaAuthority)] + + +# --------------------------------------------------------------------------- +# Index wrappers — the driver's Main (program) and Unit (instruction). +# --------------------------------------------------------------------------- + + +@dataclass +class SolanaProgramInstance: + """The located target program — the ecosystem's ``Main``, and the peer of EVM's + :class:`composer.spec.system_model.ContractInstance`. + + Deliberately **not** a ``FeatureUnit``: ``Main`` and ``Unit`` are different axes, and EVM's main + is not a unit either. It briefly doubled as the whole-program extraction unit; that is what + :class:`SolanaComponentInstance` replaced (docs/ecosystem-abstraction.md §4).""" + + ind: int + app: SolanaApplication + + @property + def program(self) -> SolanaProgram: + return self.app.programs[self.ind] + + +@dataclass +class SolanaComponentInstance: + """One :class:`ProgramComponent` of the target program — the ecosystem's ``Unit``. + + The Solana peer of :class:`composer.spec.system_model.ContractComponentInstance`, and like it an + index pair (program, component) over the analyzed model rather than a copy of it. The component + is an authoring and attribution scope, not an execution scope: Crucible still fuzzes the whole + program in one action sequence, exactly as Foundry's stateful fuzzer calls every function of a + contract while its authoring stays per component (docs/ecosystem-abstraction.md §4).""" + + ind: int + _program: SolanaProgramInstance + + @property + def app(self) -> SolanaApplication: + return self._program.app + + @property + def program(self) -> SolanaProgram: + return self._program.program + + @property + def component(self) -> ProgramComponent: + return self.program.components[self.ind] + + @property + def instructions(self) -> list[SolanaInstruction]: + """This component's instructions, resolved to the real objects. The component holds only + names; the program stays authoritative for the account/constraint/CPI detail, and this is + the single place the two are joined (a name that doesn't resolve is rejected upstream by + ``_solana_validate``, so the lookup cannot fail here).""" + by_name = self.program.instructions_by_name + return [by_name[n] for n in self.component.instructions if n in by_name] + + @property + def sibling_components(self) -> list[ProgramComponent]: + """The program's other components — context, not units, mirroring EVM's ``ommer_contracts``.""" + return [c for i, c in enumerate(self.program.components) if i != self.ind] + + @property + def sibling_programs(self) -> list[SolanaProgram]: + """The application's other programs — context for cross-program (CPI) reasoning. Indexed off + the located program rather than compared by ``program_identifier``, exactly as + :attr:`sibling_components` is.""" + return [p for i, p in enumerate(self.app.programs) if i != self._program.ind] + + # -- FeatureUnit protocol ----------------------------------------------------------- + @property + def display_name(self) -> str: + return self.component.name + + @property + def slug(self) -> str: + """Slug uniqueness within a program is guaranteed upstream (``_solana_validate`` rejects + sibling components that slugify alike), so no disambiguation is needed here.""" + return slugify_filename(self.component.name) + + @property + def unit_index(self) -> int: + return self.ind + + def cache_material(self) -> str: + return "|".join([self.app.model_dump_json(), str(self.ind), str(self._program.ind)]) + + def context_tag(self) -> dict[str, object]: + return {"component": self.component.model_dump()} + + def feature_json(self) -> dict[str, object]: + """The component, and only the component — EVM's ``feature_json`` is + ``self.component.model_dump(mode="json")`` and this mirrors it (§14 Q3). Two mechanical + additions: ``instructions`` is resolved from names to the full objects (EVM's + ``external_entry_points`` are self-contained strings and have nothing to resolve), and + ``slug`` rides along because a backend names artifacts after it and must not re-derive it. + + The *whole-program* surface deliberately does NOT travel here. A backend that needs it has + its own route: Crucible's authored fixture — injected into every ``AuthorInput.context`` and + rendered in the prompt — already exposes every ``action_*`` the fuzzer can drive.""" + return { + **self.component.model_dump(mode="json"), + "slug": self.slug, + "instructions": [i.model_dump(mode="json") for i in self.instructions], + } diff --git a/composer/spec/solana/null_backend.py b/composer/spec/solana/null_backend.py new file mode 100644 index 00000000..c76d8a0a --- /dev/null +++ b/composer/spec/solana/null_backend.py @@ -0,0 +1,176 @@ +"""A null Solana backend — records extracted properties without verifying them. + +It satisfies the full ``PipelineBackend`` contract over the Solana ecosystem's +``(SolanaApplication, SolanaProgramInstance, SolanaComponentInstance)`` triple, but its +``formalize`` just echoes the extracted properties into a trivial result and its +``fetch_verdicts`` returns nothing. + +**Role:** a **test double** for the Solana front half (analysis + property extraction) +without a real verifier — see ``tests/test_solana_gate.py``. Production Solana +verification is the Crucible fuzzer backend. +""" + +import enum +import json +from dataclasses import dataclass +from pathlib import Path +from typing import override + +from pydantic import BaseModel, Field + +from composer.pipeline.core import ( + CorePhases, + Formalizer, + GaveUp, + PipelineRun, + PreparedSystem, + SystemAnalysisSpec, +) +from composer.spec.artifacts import ArtifactStore +from composer.spec.context import WorkflowContext +from composer.spec.cvl_generation import SkippedProperty +from composer.spec.solana.model import ( + SolanaApplication, + SolanaComponentInstance, + SolanaProgramInstance, +) +from composer.spec.source.report.collect import ReportComponentInput, Verdict +from composer.spec.source.report.schema import RuleName +from composer.spec.types import PropertyFormulation +from composer.spec.util import ensure_dir + +SOLANA_NULL_GUIDANCE: str = """\ +These properties are recorded by a null backend (no verification is performed). Extract +properties a Solana verification tool could plausibly check: account/state invariants, access +control (signer/owner/authority), PDA-derivation correctness, and arithmetic safety. Freely +state universally-quantified properties. +""" + + +class SolanaPhase(enum.Enum): + ANALYSIS = "analysis" + EXTRACTION = "extraction" + FORMALIZATION = "formalization" + REPORT = "report" + + +class NullResult(BaseModel): + """A trivial formalization result: it just carries the properties back out.""" + + commentary: str = "" + property_rules: list[tuple[str, list[str]]] = Field(default_factory=list) + skipped: list[SkippedProperty] = Field(default_factory=list) + + def property_units(self) -> list[tuple[str, list[str]]]: + return [(t, list(u)) for t, u in self.property_rules] + + @property + def artifact_text(self) -> str: + return json.dumps( + {"commentary": self.commentary, "properties": self.property_units()}, indent=2 + ) + + @property + def output_link(self) -> str | None: + return None + + +@dataclass(frozen=True) +class NullArtifact: + slug: str + + @property + def stem(self) -> str: + return f"null_{self.slug}" + + @property + def artifact_file(self) -> str: + return f"{self.stem}.json" + + +class NullSolanaArtifactStore(ArtifactStore[NullArtifact, NullResult]): + def __init__(self, project_root: str): + super().__init__( + project_root, + "property_units", + deliverable_dir="certora/solana_null", + internal_dir=".certora_internal/solana_null", + report_dir="certora/solana_null/reports", + ) + + @override + def _artifact_dir(self) -> Path: + return ensure_dir(Path(self._project_root) / "certora/solana_null/artifacts") + + +class NullSolanaFormalizer(Formalizer[NullResult, SolanaComponentInstance]): + def __init__(self) -> None: + # The tag is provenance only — it picks the report's outcome labels, and this backend's + # results are all-UNKNOWN either way. So borrow ``"prover"``, an existing member of + # ``ReportBackend``: the real Solana verifier's own tag is added to that literal by the + # backend that introduces it, and until then a value outside the literal is not merely + # untyped but unusable — ``AutoProverReport`` is a pydantic model, so it would fail + # validation in ``build_report`` and lose the report phase to a swallowed exception. + super().__init__(NullResult, "prover") + + @override + async def formalize( + self, + label: str, + feat: SolanaComponentInstance, + props: list[PropertyFormulation], + ctx: WorkflowContext[NullResult], + run: PipelineRun, + ) -> NullResult | GaveUp: + return NullResult( + commentary=f"Null formalization of instruction {feat.display_name} " + f"({len(props)} properties recorded, unverified).", + property_rules=[(p.title, [p.title]) for p in props], + ) + + @override + async def fetch_verdicts( + self, inp: ReportComponentInput[NullResult] + ) -> dict[RuleName, Verdict]: + return {} + + +@dataclass +class NullSolanaPrepared(PreparedSystem[NullResult, SolanaComponentInstance, SolanaProgramInstance]): + form: NullSolanaFormalizer + + @override + async def prepare_formalization( + self, run: PipelineRun + ) -> Formalizer[NullResult, SolanaComponentInstance]: + return self.form + + +@dataclass +class NullSolanaBackend: + """``PipelineBackend[SolanaPhase, NullResult, None, NullArtifact, SolanaComponentInstance, + SolanaProgramInstance, SolanaApplication]`` (P, FormT, H, A, Unit, Main, App) — structural.""" + + artifact_store: NullSolanaArtifactStore + backend_guidance = SOLANA_NULL_GUIDANCE + analysis_spec = SystemAnalysisSpec("solana-analysis", "solana-properties") + core_phases = CorePhases( + { + "analysis": SolanaPhase.ANALYSIS, + "extraction": SolanaPhase.EXTRACTION, + "formalization": SolanaPhase.FORMALIZATION, + "report": SolanaPhase.REPORT, + } + ) + + async def prepare_system( + self, analyzed: SolanaApplication, run: PipelineRun[SolanaPhase, None] + ) -> PreparedSystem[NullResult, SolanaComponentInstance, SolanaProgramInstance]: + # Use the Solana ecosystem's locate_main so the backend and ecosystem agree on the + # target program (imported lazily to avoid an import cycle with pipeline.ecosystem). + from composer.pipeline.ecosystem import SOLANA + + return NullSolanaPrepared(SOLANA.locate_main(analyzed, run.source), NullSolanaFormalizer()) + + def to_artifact_id(self, c: SolanaComponentInstance) -> NullArtifact: + return NullArtifact(c.slug) diff --git a/composer/spec/source/autoprove_common.py b/composer/spec/source/autoprove_common.py index 24eb0a7e..4441c97f 100644 --- a/composer/spec/source/autoprove_common.py +++ b/composer/spec/source/autoprove_common.py @@ -19,6 +19,7 @@ SourceFields ) from composer.pipeline.cli import cli_pipeline, user_ns +from composer.pipeline.ecosystem import EVM from composer.spec.source.pipeline import ProverBackend, GeneratedCVL from composer.prover.core import make_prover_options from composer.spec.source.source_env import build_source_env @@ -146,5 +147,5 @@ async def callback( ProverArtifactStore(staged.source.project_root, staged.source.contract_name), make_prover_options(cloud=args.cloud) ) - return await cont(source_env, backend) + return await cont(source_env, backend, EVM) yield callback diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index c6ac5120..dbbaea0e 100644 --- a/composer/spec/source/pipeline.py +++ b/composer/spec/source/pipeline.py @@ -30,7 +30,7 @@ from composer.spec.types import PropertyFormulation from composer.spec.gen_types import CVLResource, SPECS_DIR, certora_relative_to_project from composer.spec.system_model import ( - ContractComponentInstance, SourceApplication, HarnessedApplication, + ContractComponentInstance, ContractInstance, SourceApplication, HarnessedApplication, SourceExplicitContract, HarnessedExplicitContract, SourceExternalActor, HarnessDefinition, SolidityIdentifier, ) @@ -56,9 +56,10 @@ from composer.ui.autoprove_app import AutoProvePhase from composer.pipeline.core import ( Formalizer, PreparedSystem, PipelineRun, Delivered, GaveUp, - CorePhases, SystemAnalysisSpec, ComponentOutcome, main_instance, + CorePhases, SystemAnalysisSpec, ComponentOutcome, COMMON_SYSTEM_CACHE_KEY ) +from composer.pipeline.ecosystem import main_instance INV_CVL_KEY = CacheKey[None, GeneratedCVL]("invariant-cvl") @@ -98,7 +99,7 @@ def _lift_harnessed( @dataclass -class ProverRunner(Formalizer[GeneratedCVL]): +class ProverRunner(Formalizer[GeneratedCVL, ContractComponentInstance]): """Immutable formalizer: per-batch CVL generation against a fixed prover config + resource set (already including ``invariants.spec`` when there are structural invariants), plus the in-memory invariant result for the report.""" @@ -149,7 +150,7 @@ async def fetch_verdicts( return await self._fetch(inp) @override - async def finalize(self, outcomes: list[ComponentOutcome[GeneratedCVL]], run: PipelineRun) -> None: + async def finalize(self, outcomes: list[ComponentOutcome[GeneratedCVL, ContractComponentInstance]], run: PipelineRun) -> None: # components_to_prover_runs.json: {run_key (slug): prover /output/ link}. runs: dict[str, str] = { ComponentSpec(o.feat.slugified_name).run_key: o.result.run_link @@ -164,7 +165,7 @@ async def finalize(self, outcomes: list[ComponentOutcome[GeneratedCVL]], run: Pi @dataclass -class ProverPrepared(PreparedSystem[GeneratedCVL]): +class ProverPrepared(PreparedSystem[GeneratedCVL, ContractComponentInstance, ContractInstance]): """Post-harness system: holds the harnessed app + prover tool, and runs the prover-only pre-formalization fan-out in ``prepare_formalization``.""" _store: ProverArtifactStore @@ -175,7 +176,7 @@ class ProverPrepared(PreparedSystem[GeneratedCVL]): _analyzed: SourceApplication @override - async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedCVL]: + async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedCVL, ContractComponentInstance]: # AutoSetup (+ custom summaries) ∥ structural-invariant formulation; both # depend only on the harnessed app, so they run concurrently. (setup_config, resources), invariants = await asyncio.gather( @@ -272,7 +273,9 @@ async def _invariants(self, run: PipelineRun): @dataclass class ProverBackend: - """PipelineBackend[AutoProvePhase, GeneratedCVL, None, ComponentSpec].""" + """PipelineBackend[AutoProvePhase, GeneratedCVL, None, ComponentSpec, + ContractComponentInstance, ContractInstance, SourceApplication] + (P, FormT, H, A, Unit, Main, App).""" backend_guidance = CERTORA_BACKEND_GUIDANCE core_phases = CorePhases({ "analysis": AutoProvePhase.COMPONENT_ANALYSIS, @@ -287,7 +290,7 @@ class ProverBackend: async def prepare_system( self, analyzed: SourceApplication, run: PipelineRun[AutoProvePhase, None], - ) -> PreparedSystem[GeneratedCVL]: + ) -> PreparedSystem[GeneratedCVL, ContractComponentInstance, ContractInstance]: sys_desc = await run.runner( TaskInfo(HARNESS_TASK_ID, "Harness Creation", AutoProvePhase.HARNESS), lambda: run_harness_creation(run.ctx, run.source, run.env, analyzed), diff --git a/composer/spec/system_analysis.py b/composer/spec/system_analysis.py index 57953825..603c66c6 100644 --- a/composer/spec/system_analysis.py +++ b/composer/spec/system_analysis.py @@ -1,4 +1,4 @@ -from typing import NotRequired, Any +from typing import NotRequired, Any, Callable, TypedDict from graphcore.graph import MessagesState, FlowInput @@ -6,17 +6,35 @@ from composer.spec.context import ( WorkflowContext, SystemDoc ) +from composer.spec.gen_types import TypedTemplate from composer.spec.graph_builder import bind_standard, run_to_completion -from composer.spec.system_model import BaseApplication, ExplicitContract, ExternalActor, ExternalDependency, SolidityIdentifier -from composer.spec.service_host import ServiceHost +from composer.spec.system_model import BaseApplication, ExplicitContract, ExternalActor, ExternalDependency +from composer.spec.types import SourceIdentifier +from composer.spec.service_host import ServiceHost, Sort from composer.spec.util import slugify_filename from composer.tools.thinking import RoughDraftState, get_rough_draft_tools DESCRIPTION = "Component analysis" -def _validate_connectivity( - app: BaseApplication, expected_main_id: SolidityIdentifier | None + +class AnalysisPromptParams(TypedDict): + """Kwargs shared by the analysis agent's system and initial prompt templates.""" + sort: Sort + has_doc: bool + + +#: The EVM/Solidity analysis prompts. +ANALYSIS_SYSTEM_TEMPLATE = TypedTemplate[AnalysisPromptParams]("application_analysis_system.j2") +ANALYSIS_INITIAL_TEMPLATE = TypedTemplate[AnalysisPromptParams]("application_analysis_prompt.j2") + +def validate_solidity_connectivity( + app: BaseApplication, expected_main_id: SourceIdentifier | None ) -> str | None: + """Connectivity/shape validation for the Solidity model *family*: typed over + ``BaseApplication`` because it checks only the contract/actor/interaction graph that + ``Application``, ``SourceApplication``, ``HarnessedApplication``, and + ``FromSourceApplication`` all share. Both callers name it directly; neither can use the + other's ``Ecosystem.validate_analysis``, which is narrowed to one ``system_model``.""" errors: list[str] = [] known_components: dict[str, set[str]] = {} known_external: set[str] = set() @@ -94,7 +112,11 @@ async def run_component_analysis[T: BaseApplication]( input: SystemDoc | None, env: ServiceHost, extra_input: list[str | dict], - expected_main_id: SolidityIdentifier | None = None, + expected_main_id: SourceIdentifier | None = None, + *, + system_template: TypedTemplate[AnalysisPromptParams], + initial_template: TypedTemplate[AnalysisPromptParams], + validate: Callable[[T, SourceIdentifier | None], str | None], ) -> T | None: """Analyze application components from a system doc and optionally source code.""" if (cached := await child_ctxt.cache_get(ty)) is not None: @@ -112,26 +134,23 @@ class AnalysisInput(RoughDraftState, FlowInput): }) def _validation_wrapper( - _: Any, app: BaseApplication + _: Any, app: T ) -> str | None: - return _validate_connectivity(app, expected_main_id) + return validate(app, expected_main_id) + prompt_params: AnalysisPromptParams = {"sort": env.sort, "has_doc": input is not None} b = bind_standard( builder=env.builder_lite(), state_type=AnalysisState, validator=_validation_wrapper ).with_input( AnalysisInput - ).with_sys_prompt_template( - "application_analysis_system.j2", - sort=env.sort, - has_doc=input is not None + ).inject( + lambda g: system_template.bind(prompt_params).render_to(g.with_sys_prompt_template) ).with_tools( [memory, *get_rough_draft_tools(AnalysisState), *env.analysis_tools] - ).with_initial_prompt_template( - "application_analysis_prompt.j2", - sort=env.sort, - has_doc=input is not None + ).inject( + lambda g: initial_template.bind(prompt_params).render_to(g.with_initial_prompt_template) ) graph = b.compile_async() diff --git a/composer/spec/system_model.py b/composer/spec/system_model.py index 7bdb4059..abbea617 100644 --- a/composer/spec/system_model.py +++ b/composer/spec/system_model.py @@ -1,10 +1,48 @@ from dataclasses import dataclass -from typing import Literal +from typing import Literal, Protocol from pydantic import BaseModel, Field from functools import cached_property from composer.spec.util import slugify_filename from .types import ComponentName, SolidityIdentifier, ContractName + +class FeatureUnit(Protocol): + """The per-unit interface the shared pipeline driver needs, independent of ecosystem. + + Each ecosystem's unit wrapper (EVM's :class:`ContractComponentInstance`, Solana's + instruction instance, …) satisfies it; ecosystem-specific code — prompts, backends, + formalizers — works with the concrete unit type. This keeps the driver's per-unit cache + keys, task ids, labels, and context tags ecosystem-agnostic.""" + + @property + def display_name(self) -> str: + """Human label for tasks / report rows.""" + ... + + @property + def slug(self) -> str: + """Filesystem-safe slug used as an artifact-id base.""" + ... + + @property + def unit_index(self) -> int: + """Stable per-run index used in task ids.""" + ... + + def cache_material(self) -> str: + """Stable string identifying this unit, hashed into its per-unit cache key.""" + ... + + def context_tag(self) -> dict[str, object]: + """The tag persisted alongside this unit's workflow context.""" + ... + + def feature_json(self) -> dict[str, object]: + """The unit's semantic content as a JSON-able dict, for a backend that + marshals it across a boundary (e.g. a Rust wheel's ``FormalizeInput.component``). + The shape is ecosystem-specific; the paired backend knows how to read it.""" + ... + type ContractSort = Literal["dynamic", "singleton", "multiple"] @@ -92,7 +130,10 @@ class SourceExternalActor(ExternalActor): type SystemComponent = ExternalActor | ExplicitContract -class BaseApplication[T : SystemComponent](BaseModel): +# Bound is ``BaseModel`` (not ``SystemComponent``) so non-EVM ecosystems can parameterize it +# with their own component unions (e.g. Solana's programs/authorities); the EVM subclasses below +# still pin the concrete ``SystemComponent`` union. +class BaseApplication[T : BaseModel](BaseModel): application_type: str = Field(description="A concise, description of the type of application (AMM/Liquidity Provider/etc.)") description: str = Field(description="A description of the application's main functionality (2 - 3 sentences max)") components : list[T] = Field(description="The system components (explicit contract & external actors) that comprise this application") @@ -231,9 +272,31 @@ def slugified_name(self) -> str: """Filesystem-safe slug for this component, used as an output filename base. Slug uniqueness within a contract is guaranteed upstream: component analysis rejects any application whose sibling components slugify to the same id (see - ``_validate_connectivity``), so no disambiguation is needed here.""" + ``validate_solidity_connectivity``), so no disambiguation is needed here.""" return slugify_filename(self.component.name) + # -- FeatureUnit protocol (the ecosystem-agnostic view the driver consumes) --------- + @property + def display_name(self) -> str: + return self.component.name + + @property + def slug(self) -> str: + return self.slugified_name + + @property + def unit_index(self) -> int: + return self.ind + + def cache_material(self) -> str: + return "|".join([self.app.model_dump_json(), str(self.ind), str(self._contract.ind)]) + + def context_tag(self) -> dict[str, object]: + return {"component": self.component.model_dump()} + + def feature_json(self) -> dict[str, object]: + return self.component.model_dump(mode="json") + @staticmethod def from_app( app: AnyApplication, diff --git a/composer/spec/types.py b/composer/spec/types.py index 368bc6b0..da360081 100644 --- a/composer/spec/types.py +++ b/composer/spec/types.py @@ -1,25 +1,36 @@ from typing import TYPE_CHECKING, Protocol, Literal -# Nominal ``str`` subtypes for the two distinct contract-identity fields. -# Both phantom-typed (TYPE_CHECKING-only subclass; ``str`` at runtime) so they -# remain distinct at static-check time but pydantic ``Field`` validates them -# as plain strings. +# Nominal ``str`` subtypes for the distinct identity fields of an analyzed +# system. All phantom-typed (TYPE_CHECKING-only subclasses; ``str`` at runtime) +# so they remain distinct at static-check time but pydantic ``Field`` validates +# them as plain strings. # -# ``SolidityIdentifier``: a Solidity contract identifier (regex-validated where -# stored on a pydantic field). -# ``ContractName``: the conceptual / design-doc-readable name of a contract. -# May be a Solidity identifier when the design doc names contracts that way, -# but allowed to be anything human-readable. +# ``SourceIdentifier``: the identifier an entity is defined under in source — +# EVM's contract identifier, Solana's program identifier. What the +# ecosystem-agnostic seam speaks. +# ``SolidityIdentifier`` / ``RustIdentifier``: a ``SourceIdentifier`` in a +# specific source language (regex-validated where stored on a pydantic field). +# ``ContractName`` / ``ProgramName``: the conceptual / design-doc-readable name +# of an EVM contract or a Solana program. May coincide with the source +# identifier when the design doc names the entity that way, but allowed to be +# anything human-readable. # -# The two are **siblings under str**, not in a subtype relation with each -# other — passing a ``SolidityIdentifier`` where ``ContractName`` is expected -# (or vice-versa) is a type error, even though both are ``str`` at runtime. +# ``SolidityIdentifier`` and ``RustIdentifier`` are **siblings** under +# ``SourceIdentifier``; the conceptual names are siblings of each other and of +# ``SourceIdentifier``. Passing one where a sibling is expected is a type error, +# even though all are ``str`` at runtime. if TYPE_CHECKING: - class SolidityIdentifier(str): ... + class SourceIdentifier(str): ... + class SolidityIdentifier(SourceIdentifier): ... + class RustIdentifier(SourceIdentifier): ... class ContractName(str): ... + class ProgramName(str): ... else: + SourceIdentifier = str SolidityIdentifier = str + RustIdentifier = str ContractName = str + ProgramName = str type UnitName = str diff --git a/composer/templates/application_analysis_macros.j2 b/composer/templates/application_analysis_macros.j2 deleted file mode 100644 index 39bf30b4..00000000 --- a/composer/templates/application_analysis_macros.j2 +++ /dev/null @@ -1,5 +0,0 @@ -{% macro input_phrase(and_or=false) %} -{%- if has_doc %}system/design document{% endif %} -{%- if has_doc and sort != "greenfield" %} and{% if and_or%}/or{%endif%} {%endif%} -{%- if sort != "greenfield" %}the implementation{%endif%} -{% endmacro %} diff --git a/composer/templates/application_analysis_prompt.j2 b/composer/templates/application_analysis_prompt.j2 index 7a303af6..19288162 100644 --- a/composer/templates/application_analysis_prompt.j2 +++ b/composer/templates/application_analysis_prompt.j2 @@ -1,4 +1,4 @@ -{% from "application_analysis_macros.j2" import input_phrase %} +{% from "shared/analysis_macros.j2" import input_phrase with context %} # Background @@ -158,9 +158,4 @@ whether this other contract should be an external actor or not: actor, but include S1, S2, ... etc as explicit contract components whose role is to implement interface I. {% endif %} -# Memory - -You have access to a memory tool which may include your prior progress on this task. -You should assume that the documentation or source code you are analyzing has NOT changed -since the memories were written. You do *NOT* need to reverify or validate any claims or information -in your memory. You may immediately proceed with that information as if you derived it yourself. +{% include "shared/analysis_memory.j2" %} diff --git a/composer/templates/application_analysis_system.j2 b/composer/templates/application_analysis_system.j2 index 16ba89e1..43e6368a 100644 --- a/composer/templates/application_analysis_system.j2 +++ b/composer/templates/application_analysis_system.j2 @@ -1,21 +1,9 @@ -{% from "application_analysis_macros.j2" import input_phrase %} +{% from "shared/analysis_macros.j2" import input_phrase with context %} You are an experienced system architect who is also well-versed in Web3 (blockchain) applications. In this role, you are analyzing the {{ input_phrase() }} to extract a structured model of its behavior. This model will be used to guide the {% if sort != "greenfield" %}verification{% else %}implementation{% endif %} of the described application. -## Behavior - -- After any collection of data, use your adaptive thinking capabilities to consider all of your information - before proceeding -- Ground any results you produce in verifiable information as much as possible. -- When resolving any ambiguity during your work, favor self-consistency. - -## Tools - -- You have access to a "memory" tool, presented using a filesystem-like abstraction. Whenever you synthesize - new knowledge or reach some conclusion, use the memory tool to record this information and any reasoning you used. -- When presented with a multi-step task, use the memory tool to track your progress through that task. Concretely, - use `/memories/progress.md` to track both the current step of the task, along with any "data" that is part of the task. +{% include "shared/architect_behavior_tools.j2" %} {% with draft_subject = "your response" %} {% include "rough_draft_protocol.j2" %} {% endwith %} diff --git a/composer/templates/property_analysis_prompt.j2 b/composer/templates/property_analysis_prompt.j2 index 88f264b7..4488a2d2 100644 --- a/composer/templates/property_analysis_prompt.j2 +++ b/composer/templates/property_analysis_prompt.j2 @@ -7,36 +7,7 @@ audit effort. {% include "application_context_new.j2" %} -{% if prior_properties %} - -You are running iteratively. {{ prior_properties | length }} prior round(s) have already -analyzed this component. Their findings and reasoning are below. The properties listed -here MUST NOT be re-proposed by you — including reframings of the same underlying claim -as a different property sort (e.g. an attack-vector restated as an invariant, or vice -versa). Your task this round is to surface security properties that prior rounds *missed*. - -{% for round_result in prior_properties %} -### Round {{ loop.index }} extracted properties: -{% for p in round_result.items %} -- [{{ p.sort }}] `{{ p.title }}`: {{ p.description }} -{% endfor %} - -### Round {{ loop.index }} reasoning: -{{ round_result.reasoning }} - -{% endfor %} - -When deciding what to look at this round, treat the prior rounds' reasoning as the -authoritative record of what has been considered — not your own assumptions about what -"a prior agent probably looked at". If a prior round's reasoning is silent on an angle, -that angle is fair game for you. - -The standing rule from your system prompt — return an empty `items` list rather than -pad with low-value properties — applies in full force here. If the prior rounds have -already covered the meaningful property surface, returning nothing new is the right -answer. - -{% endif %} +{% with unit_noun = "component" %}{% include "shared/prior_properties.j2" %}{% endwith %} {% if sort != "greenfield" %} diff --git a/composer/templates/property_analysis_system_prompt.j2 b/composer/templates/property_analysis_system_prompt.j2 index f0e5dcc2..638e8a9c 100644 --- a/composer/templates/property_analysis_system_prompt.j2 +++ b/composer/templates/property_analysis_system_prompt.j2 @@ -11,35 +11,7 @@ later rounds and a human reviewer will read. # Behavior -## Quality over quantity — and "nothing new" is the right answer when it's true - -The whole point of running multiple rounds is to *eventually exhaust* the meaningful -property surface for this component. The convergence signal — an empty `items` list -with a `reasoning` field that explains what you looked at and why nothing new -emerged — is the desired outcome of a good round, not a failure. - -DO NOT propose properties just to feel productive. DO NOT pad the list. DO NOT -reach for marginal, low-value, or barely-defensible properties to avoid returning -empty. The following are concrete failure modes you must NOT fall into: - -- Restating a prior property in slightly different words and pretending it's new. -- Proposing trivial corollaries of existing properties ("X holds" plus "X holds - at block N", "X holds for user U"). -- Inventing edge cases the design document does not actually motivate, just to - have *something* to return. -- Proposing properties about behavior that is not security-relevant or formally - verifiable, in order to fill space. -- Proposing properties whose violation has no meaningful consequence. - -For every property you DO include, your `reasoning` field must defend why the -property matters AND, when prior rounds exist, why a prior round legitimately -could have missed it. If you can't articulate that defense, drop the property. - -If you find yourself thinking "this is a stretch, but I should include something" — -return an empty list. That is the right call. The pipeline is built to handle empty -returns gracefully; it is NOT built to filter low-quality properties out of a padded -list, and downstream agents will waste expensive prover cycles on whatever junk you -ship. +{% with unit_noun = "component" %}{% include "shared/property_quality_over_quantity.j2" %}{% endwith %} ## Reasoning is load-bearing @@ -50,12 +22,7 @@ shape. Be specific about what you looked at — name functions, name parameters, name attack patterns. "I considered X but ruled it out because Y" is exactly the right granularity. "I thought about it carefully and decided Y" is useless. -## Adaptive thinking and self-consistency - -After collecting information from the source / design doc, use your adaptive -thinking capabilities to integrate what you've found before drafting properties. -Don't propose properties from a single read; reason over the full picture. When -resolving ambiguity in the inputs, favor self-consistency. +{% include "shared/property_adaptive_thinking.j2" %} # Tools diff --git a/composer/templates/rust/_vulnerability_patterns.j2 b/composer/templates/rust/_vulnerability_patterns.j2 new file mode 100644 index 00000000..6a52ea05 --- /dev/null +++ b/composer/templates/rust/_vulnerability_patterns.j2 @@ -0,0 +1,15 @@ +Rust language-level vulnerability patterns (shared by every Rust on-chain ecosystem — Solana, Soroban, …): + +- **Integer overflow / underflow.** On-chain Rust builds usually enable `overflow-checks`, so an + overflow *panics* (aborting the transaction) rather than wrapping — a denial-of-service / + griefing vector, not silent corruption. But code that uses `wrapping_*`, `unchecked_*`, `as` + casts (truncation), or arithmetic in a non-checked build can silently produce wrong values. + Look for arithmetic on balances, amounts, indices, and lengths. +- **Panics as aborts.** `unwrap()`, `expect()`, `panic!`, array indexing out of bounds, and + `unreachable!` all abort the transaction. An attacker-controllable input that forces one is a + DoS / stuck-funds vector (e.g. an operation that can be made to always panic). +- **Lossy conversions / precision.** `as` casts between integer widths truncate; integer + division rounds toward zero. Rounding direction that favors the caller over the protocol + (or vice versa) across two code paths is an arbitrage / value-leak vector. +- **Unchecked results.** An ignored `Result`/error (`let _ = ...`, `.ok()`, `?` swallowed) that + should have aborted lets execution continue in an inconsistent state. diff --git a/composer/templates/shared/analysis_macros.j2 b/composer/templates/shared/analysis_macros.j2 new file mode 100644 index 00000000..8e19374e --- /dev/null +++ b/composer/templates/shared/analysis_macros.j2 @@ -0,0 +1,22 @@ +{#- The analysis agent's *input phrase*: names what it was actually handed — the design document, + the implementation, or both. The design document is optional (``run_component_analysis`` + takes ``input: SystemDoc | None`` and passes ``has_doc`` accordingly), so every sentence that + refers to the inputs has to stay true when there is no document; this macro is the single + place that decides how to say it. + + Callers supply the leading article ("the {{ input_phrase() }}"), so the branches are + article-free. ``impl_noun`` names the implementation in the ecosystem's own terms — + "implementation" for Solidity, "Rust implementation" for Solana. + + IMPORT WITH CONTEXT: {% raw %}{% from "shared/analysis_macros.j2" import input_phrase with context %}{% endraw %} + The branches read ``has_doc``/``sort`` off the render params, and a plain import gives the + macro only the environment globals — leaving both Undefined, which silently renders the + no-document phrasing for every caller. -#} +{% macro input_phrase(and_or=false, impl_noun="implementation") -%} +{%- if has_doc -%} +system/design document +{%- if sort != "greenfield" %} and{% if and_or %}/or{% endif %} the {{ impl_noun }}{% endif -%} +{%- else -%} +{{ impl_noun }} +{%- endif -%} +{%- endmacro %} diff --git a/composer/templates/shared/analysis_memory.j2 b/composer/templates/shared/analysis_memory.j2 new file mode 100644 index 00000000..fc3e4ef0 --- /dev/null +++ b/composer/templates/shared/analysis_memory.j2 @@ -0,0 +1,6 @@ +# Memory + +You have access to a memory tool which may include your prior progress on this task. +You should assume that the documentation or source code you are analyzing has NOT changed +since the memories were written. You do *NOT* need to reverify or validate any claims or information +in your memory. You may immediately proceed with that information as if you derived it yourself. diff --git a/composer/templates/shared/architect_behavior_tools.j2 b/composer/templates/shared/architect_behavior_tools.j2 new file mode 100644 index 00000000..72139f9e --- /dev/null +++ b/composer/templates/shared/architect_behavior_tools.j2 @@ -0,0 +1,13 @@ +## Behavior + +- After any collection of data, use your adaptive thinking capabilities to consider all of your information + before proceeding +- Ground any results you produce in verifiable information as much as possible. +- When resolving any ambiguity during your work, favor self-consistency. + +## Tools + +- You have access to a "memory" tool, presented using a filesystem-like abstraction. Whenever you synthesize + new knowledge or reach some conclusion, use the memory tool to record this information and any reasoning you used. +- When presented with a multi-step task, use the memory tool to track your progress through that task. Concretely, + use `/memories/progress.md` to track both the current step of the task, along with any "data" that is part of the task. diff --git a/composer/templates/shared/prior_properties.j2 b/composer/templates/shared/prior_properties.j2 new file mode 100644 index 00000000..c3cf74f9 --- /dev/null +++ b/composer/templates/shared/prior_properties.j2 @@ -0,0 +1,30 @@ +{% if prior_properties %} + +You are running iteratively. {{ prior_properties | length }} prior round(s) have already +analyzed this {{ unit_noun }}. Their findings and reasoning are below. The properties listed +here MUST NOT be re-proposed by you — including reframings of the same underlying claim +as a different property sort (e.g. an attack-vector restated as an invariant, or vice +versa). Your task this round is to surface security properties that prior rounds *missed*. + +{% for round_result in prior_properties %} +### Round {{ loop.index }} extracted properties: +{% for p in round_result.items %} +- [{{ p.sort }}] `{{ p.title }}`: {{ p.description }} +{% endfor %} + +### Round {{ loop.index }} reasoning: +{{ round_result.reasoning }} + +{% endfor %} + +When deciding what to look at this round, treat the prior rounds' reasoning as the +authoritative record of what has been considered — not your own assumptions about what +"a prior agent probably looked at". If a prior round's reasoning is silent on an angle, +that angle is fair game for you. + +The standing rule from your system prompt — return an empty `items` list rather than +pad with low-value properties — applies in full force here. If the prior rounds have +already covered the meaningful property surface, returning nothing new is the right +answer. + +{% endif %} diff --git a/composer/templates/shared/property_adaptive_thinking.j2 b/composer/templates/shared/property_adaptive_thinking.j2 new file mode 100644 index 00000000..1ed4c809 --- /dev/null +++ b/composer/templates/shared/property_adaptive_thinking.j2 @@ -0,0 +1,6 @@ +## Adaptive thinking and self-consistency + +After collecting information from the source / design doc, use your adaptive +thinking capabilities to integrate what you've found before drafting properties. +Don't propose properties from a single read; reason over the full picture. When +resolving ambiguity in the inputs, favor self-consistency. diff --git a/composer/templates/shared/property_quality_over_quantity.j2 b/composer/templates/shared/property_quality_over_quantity.j2 new file mode 100644 index 00000000..0b1e88ef --- /dev/null +++ b/composer/templates/shared/property_quality_over_quantity.j2 @@ -0,0 +1,29 @@ +## Quality over quantity — and "nothing new" is the right answer when it's true + +The whole point of running multiple rounds is to *eventually exhaust* the meaningful +property surface for this {{ unit_noun }}. The convergence signal — an empty `items` list +with a `reasoning` field that explains what you looked at and why nothing new +emerged — is the desired outcome of a good round, not a failure. + +DO NOT propose properties just to feel productive. DO NOT pad the list. DO NOT +reach for marginal, low-value, or barely-defensible properties to avoid returning +empty. The following are concrete failure modes you must NOT fall into: + +- Restating a prior property in slightly different words and pretending it's new. +- Proposing trivial corollaries of existing properties ("X holds" plus "X holds + at block N", "X holds for user U"). +- Inventing edge cases the design document does not actually motivate, just to + have *something* to return. +- Proposing properties about behavior that is not security-relevant or formally + verifiable, in order to fill space. +- Proposing properties whose violation has no meaningful consequence. + +For every property you DO include, your `reasoning` field must defend why the +property matters AND, when prior rounds exist, why a prior round legitimately +could have missed it. If you can't articulate that defense, drop the property. + +If you find yourself thinking "this is a stretch, but I should include something" — +return an empty list. That is the right call. The pipeline is built to handle empty +returns gracefully; it is NOT built to filter low-quality properties out of a padded +list, and downstream agents will waste expensive prover cycles on whatever junk you +ship. diff --git a/composer/templates/solana/_vulnerability_patterns.j2 b/composer/templates/solana/_vulnerability_patterns.j2 new file mode 100644 index 00000000..176f0def --- /dev/null +++ b/composer/templates/solana/_vulnerability_patterns.j2 @@ -0,0 +1,30 @@ +Solana platform vulnerability patterns (the account/PDA/CPI model — reason about these specifically): + +- **Missing signer check.** An instruction that mutates state or moves value on behalf of an + authority but never checks that authority `is_signer` (or omits the Anchor `Signer<'info>` / + `has_one` / `#[account(signer)]` constraint) lets anyone act as that authority. +- **Missing owner check.** An account deserialized as a program type without verifying its + `owner` is the expected program lets an attacker substitute a look-alike account they created + under a program they control (`UncheckedAccount` / `AccountInfo` without checks is the smell; + Anchor `Account<'info, T>` checks owner, raw does not). +- **Account substitution / confused deputy.** Two accounts that must be related (e.g. a vault and + its authority, a token account and its mint/owner) but whose relationship is not constrained + (`has_one`, `constraint = a.key() == b.x`, `address = ...`) let an attacker pass a mismatched + pair — draining a different user's vault, minting to the wrong mint, etc. +- **Unvalidated PDA seeds / bump.** A PDA account not re-derived and checked against its expected + `seeds` + canonical `bump` lets an attacker pass an arbitrary account in its place; a mutable + bump or non-canonical bump enables collisions/hijacking. +- **Arbitrary CPI / program substitution.** Invoking a program taken from an unchecked account + (not pinned to a known program id) lets an attacker redirect the CPI to malicious code; missing + checks on the callee for token/system operations. +- **Signer-seed / authority misuse in CPI.** A PDA that signs a CPI (`invoke_signed`) with seeds + an attacker can influence, or over-broad authority, lets value move without proper authorization. +- **Lamport / rent draining & account close bugs.** Manual lamport transfers that don't preserve + rent exemption, or `close` handling that doesn't zero data / send to the right account, enable + reinitialization attacks or fund theft. +- **Duplicate mutable accounts.** Passing the same account twice where the program assumes two + distinct accounts (e.g. `from`/`to`) can double-count or bypass a balance check. +- **Missing reinitialization / init guards.** An `init`-like path callable twice, or state that + can be re-initialized after close, resets ownership/config. +- **Sysvar / clock spoofing.** Reading a sysvar (clock, rent) from a passed account rather than the + canonical sysvar lets an attacker forge time/rent values. diff --git a/composer/templates/solana/analysis_prompt.j2 b/composer/templates/solana/analysis_prompt.j2 new file mode 100644 index 00000000..9bfa1415 --- /dev/null +++ b/composer/templates/solana/analysis_prompt.j2 @@ -0,0 +1,100 @@ +{% from "shared/analysis_macros.j2" import input_phrase with context %} +{%- set impl = "Rust implementation" %} +# Background + +{% if has_doc %} +You have been provided a system/design document describing a Solana application, plus access to +the Rust source (native and/or Anchor) that implements it. +{% else %} +You have been provided the Rust source (native and/or Anchor) of a Solana application. No design +document accompanies it; ground all of your conclusions in the source itself. +{% endif %} + +# Task + +Analyze the {{ input_phrase(impl_noun=impl) }} and extract a holistic, structured model of the +application. Your model describes the **programs** present in the implementation, the +**instructions** each program exposes, the **accounts** each instruction operates on (with the +checks the program must enforce), and any **external authorities/actors** involved. Produce +natural-language descriptions — do *NOT* write Rust or pseudo-code. + +## Application Description + +Provide an "Application Type" — a broad category (e.g. "AMM", "Staking", "NFT marketplace", +"Escrow") — and a short (2–3 sentence) description that refines it. Then a list of "System +Components": each is either a **Program** or an **External Authority**. + +### External Authorities + +Any actor not part of the core application the programs interact with: an admin/authority +keypair, an off-chain signer, or a third-party program (e.g. an oracle) the system does not +itself implement. The **SPL Token program, the System program, and other standard Solana +programs are external authorities** unless the application implements them. Give each a short +name, a description of its role, and the assumptions/trust placed in it. + +### Programs + +Each program the application implements. For each program provide: + +- `name`: a short conceptual label (e.g. "Vault", "Staking Pool"). +- `program_identifier`: the program's Rust crate/module identifier as it appears (or will + appear) in source — a valid Rust identifier (snake_case, matching `[a-zA-Z_][a-zA-Z0-9_]*`). +- `program_id`: the on-chain base58 program id if declared (e.g. via `declare_id!`), else null. +- `description`: the program's role in the application. +- `account_types`: the account/state types this program owns and derives (PDAs) — name & purpose. +- `instructions`: the program's instructions (entry points), described below. +- `components`: the program's capabilities, described below. + +#### Instructions + +Each instruction (the program's entry points / handlers). For each: + +- `name`: the instruction's snake_case name. +- `description`: what it does behaviorally (not how). +- `args`: its non-account arguments (name & type). +- `accounts`: every account it takes in its accounts context. For each account give its `name`, + its `account_type` (e.g. `Signer`, `Account`, `Program`, `SystemAccount`, + `UncheckedAccount`, a PDA of specific seeds), its `roles` (signer / writable / readonly / pda / + program / sysvar), and the `constraints` the program is responsible for enforcing on it + (signer/owner checks, `has_one`, `seeds`+`bump`, `address`, or documented invariants). If an + account has no enforced constraints, record an empty list — that is itself important signal. +- `signers`: which accounts must sign (the authorities the instruction authenticates). +- `cpis`: cross-program invocations it performs (target program + what it does / signer used). +- `requirements`: the instruction's behavioral specification, stated as requirements ("The + instruction must ..."). + +#### Components + +Each program is additionally comprised of "components" which serve to organize related +functionality. A component is a *capability* of the program — not a single instruction, and not +the whole program. Each component should be given a short, descriptive `name` and a longer +`description` of the component. This description should focus on *what* the component does, not +*how* it does it. + +Group instructions by **capability and the account state they share**, not by call order or by +which file they live in: instructions that read and write the same PDA or state account almost +always belong to the same component. Administrative/configuration instructions usually form a +component of their own. (For example, a vault program might have "Deposits & share accounting", +"Withdrawals", and "Admin & configuration".) + +For each component provide: + +- `instructions`: the names of the instructions that make up this component. Every instruction + you declared for the program **must appear in at least one component**. An instruction may + appear in more than one component when it genuinely serves two capabilities. +- `account_types`: which of the program's declared account/state types this component maintains. +- `requirements`: any requirements or assumptions on the component's behavior, stated as + implementation requirements ("The implementation must ..."). +- `interactions`: a description of this component's interactions, either with components of this + or another program in the application, or with an external authority/actor. Each interaction + should identify the program+component or the external authority *by name*, and describe the + interaction. + +## On Interactions + +Enumerate programs and authorities as comprehensively as the inputs allow. Halt transitive +exploration at external-authority boundaries — do not speculate about what those actors do +internally. When an instruction CPIs into another program the application implements, that +callee is a Program (a component), not an external authority. + +{% include "shared/analysis_memory.j2" %} diff --git a/composer/templates/solana/analysis_system.j2 b/composer/templates/solana/analysis_system.j2 new file mode 100644 index 00000000..4b202349 --- /dev/null +++ b/composer/templates/solana/analysis_system.j2 @@ -0,0 +1,17 @@ +{% from "shared/analysis_macros.j2" import input_phrase with context %} +You are an experienced system architect well-versed in Solana on-chain programs (native and +Anchor). You are analyzing the {{ input_phrase(impl_noun="Rust implementation") }} of a Solana +application to extract a structured model of its behavior. This model guides the verification of +the application. + +{% include "shared/architect_behavior_tools.j2" %} +{% with draft_subject = "your response" %} +{% include "rough_draft_protocol.j2" %} +{% endwith %} +{% with source_tools_has_explorer = sort == "existing" %} +{% include "source_tools_system_prompt.j2" %} +{% endwith %} +When reading Rust/Anchor source, pay attention to the instruction handlers, their +`#[derive(Accounts)]` account-validation structs (and the constraints on each account: +`signer`, `mut`, `has_one`, `seeds`/`bump`, `owner`, `address`), the account/state types the +program declares, and any cross-program invocations. diff --git a/composer/templates/solana/component_context.j2 b/composer/templates/solana/component_context.j2 new file mode 100644 index 00000000..d2410039 --- /dev/null +++ b/composer/templates/solana/component_context.j2 @@ -0,0 +1,89 @@ +This task is targeting the security properties of the component {{ context.component.name }} within +the program {{ context.program.name }} (`{{ context.program.program_identifier }}`). + +This component is described as: + +{{ context.component.description }} + +{% if context.component.requirements %} +The following are the requirements for this component: +{% for req in context.component.requirements %} +* {{ req }} +{% endfor %} +{% endif %} +{% if context.component.account_types %} + +The account/state types this component maintains: {{ context.component.account_types | join(", ") }}. +{% endif %} + +The {{ context.program.name }} program itself is part of the implementation of a broader application +described as {{ context.app.application_type }}. + +## This component's instructions + +These are the entry points that make up the component, and the checks the program is responsible for +enforcing on each account they take. +{% for ins in context.instructions %} + +### `{{ ins.name }}` + +{{ ins.description }} +{% if ins.requirements %} +Requirements: +{% for req in ins.requirements %} +* {{ req }} +{% endfor %} +{% endif %} +{% if ins.args %} +Non-account arguments: {% for a in ins.args %}`{{ a }}`{% if not loop.last %}, {% endif %}{% endfor %}. +{% endif %} +Accounts: +{% for acc in ins.accounts %} +* `{{ acc.name }}` — {{ acc.account_type }}{% if acc.roles %} [{{ acc.roles | join(", ") }}]{% endif %}. + {% if acc.constraints %}Program-enforced constraints: {{ acc.constraints | join("; ") }}.{% else %}No constraints were recorded for this account — consider whether a signer/owner/relationship check is required here.{% endif %} +{% endfor %} +{% if ins.signers %} +Accounts that must sign: {{ ins.signers | join(", ") }}. +{% endif %} +{% if ins.cpis %} +Cross-program invocations: +{% for cpi in ins.cpis %} +* → `{{ cpi.target_program }}`: {{ cpi.description }} +{% endfor %} +{% endif %} +{% endfor %} + +{% if context.sibling_components %} +## The rest of the program + +The other components of {{ context.program.name }} are below. They are context, not your subject — +do not write properties about them. They matter because their instructions act on the same program +state, and may run before, after, or interleaved with this component's. +{% for other in context.sibling_components %} +* **{{ other.name }}**: {{ other.description }} +{% endfor %} +{% endif %} + +{% if context.sibling_programs %} +Other programs in the application: +{% for p in context.sibling_programs %} +* `{{ p.name }}` (`{{ p.program_identifier }}`): {{ p.description }} +{% endfor %} +{% endif %} +{% if context.app.authorities %} +External authorities / actors the system interacts with: +{% for a in context.app.authorities %} +* {{ a.name }}: {{ a.description }} +{% endfor %} +{% endif %} + +{% if context.component.interactions %} +This component interacts with other parts of the application/external actors: +{% for other in context.component.interactions %} +{% if other.authority is defined %} +- The external authority "{{ other.authority }}". This interaction is described as {{ other.description }} +{% else %} +- The {{ other.component or "" }} component of {% if other.program == context.program.name %}this program{% else %}the {{ other.program }} program{% endif %}. This interaction is described as {{ other.description }} +{% endif %} +{% endfor %} +{% endif %} diff --git a/composer/templates/solana/property_prompt.j2 b/composer/templates/solana/property_prompt.j2 new file mode 100644 index 00000000..e433eaac --- /dev/null +++ b/composer/templates/solana/property_prompt.j2 @@ -0,0 +1,84 @@ + +You are performing a security review of a Solana program in the context of a larger audit effort. + + + +{% include "solana/component_context.j2" %} + + +{% with unit_noun = "component" %}{% include "shared/prior_properties.j2" %}{% endwith %} + + +Input: the Rust/Anchor implementation of a Solana program, and a description of one of its components. +Output: a list of "security properties" for that component. + +Follow these steps exactly: + +## Step 1 + +Analyze the provided implementation and formulate a set of security +properties that are PLAUSIBLE for this program. Each description must be precise and concise, and +phrased as something checkable against the program's on-chain state. + +Security properties fall into three categories: + +1. **Invariants** — representational invariants that should always hold for the program's accounts/state, + across every reachable state. + Good: "The vault's token balance always equals the sum of all depositors' recorded shares." + Good: "A config PDA's `admin` field is only ever the key that signed the last `set_admin`." + Bad: "The accounts should be correct" (overly broad). + +2. **Safety properties** — concrete statements about what should not be possible in a correct program. + These SHOULD include intended-normal-behavior properties, not only immediately-security-critical ones. + Good: "Only the account stored in `vault.authority` (and it must sign) can ever reduce the vault balance." + Good: "`initialize` can succeed at most once for a given config PDA, no matter the call order." + Good: "No sequence of actions lets a user withdraw more than they have deposited." + Bad: "A user should not be able to hack the program" (overly broad). + +3. **Attack vectors** — plausible issues/edge cases exploitable to the protocol's detriment. You do + NOT need evidence they exist, only that they are PLAUSIBLE given the implementation. + Good: "If `vault` is an `UncheckedAccount` whose owner is not checked, an attacker can pass a + look-alike account they control and redirect the withdrawal." + Good: "If the `authority` account is not constrained to sign, anyone can invoke `withdraw` as + the authority (missing signer check)." + Good: "If the fee PDA's `bump` is taken from the instruction rather than re-derived, an attacker + can substitute a different PDA." + Bad: "The program could be exploited somehow" (overly broad). + +When reasoning about attack vectors and the checks each account requires, consider these vulnerability patterns: + +{% include "rust/_vulnerability_patterns.j2" %} + +{% include "solana/_vulnerability_patterns.j2" %} + +{{ backend_guidance }} + +NB: you do **NOT** need to formalize the properties yourself; limit your analysis to properties that +can reasonably be formalized by the downstream verification tool. + +## Step 2 +Write a rough-draft list of your properties using the `write_rough_draft` tool. + +## Step 3 +Review your rough draft. For each property, confirm it meets the Step-1 guidelines — a clear +violation consequence, non-trivial, plausibly verifiable by the downstream tool. Drop anything you +cannot defend. + +## Step 4 +Output the results using the result tool. + + + + + Derive invariants and safety properties from first principles — what the program SHOULD + guarantee — relying as little as possible on what the code CURRENTLY does. + + + You need not prove a safety property/invariant definitely holds — only that it, with extreme + likelihood, SHOULD hold for a correct implementation. + + + For attack vectors you need not find evidence the issue exists — only that it is plausible + given the program and its implementation. + + diff --git a/composer/templates/solana/property_system.j2 b/composer/templates/solana/property_system.j2 new file mode 100644 index 00000000..550db3b5 --- /dev/null +++ b/composer/templates/solana/property_system.j2 @@ -0,0 +1,46 @@ +You are an expert security auditor of Solana on-chain programs (native and Anchor). You know the +failure modes that recur on Solana — missing signer/owner checks, account substitution / confused +deputy, unvalidated PDAs, arbitrary CPIs, lamport/rent and account-close bugs, duplicate mutable +accounts, reinitialization — plus the Rust-level ones (overflow-panic DoS, truncating casts). You +recognize them in design documents and in Rust/Anchor code. + +Your job is to extract a list of *security properties* — statements about the program's on-chain +state and behavior that a downstream verification tool will check. (Which tool, and what it can do +with them, is described in the task's backend guidance; write the properties the program should +satisfy, not properties shaped around one tool.) The work happens in a multi-round loop: each round +produces only the NEW properties not surfaced by prior rounds, plus a written reasoning record that +later rounds and a human reviewer will read. + +# Behavior + +{% with unit_noun = "component" %}{% include "shared/property_quality_over_quantity.j2" %}{% endwith %} + +## Reasoning is load-bearing + +Your `reasoning` field is read by future-round agents and by a human reviewer. Be specific: name +the instruction, the accounts, the seeds, the CPI target, the attack pattern. "I considered the +missing owner check on `vault` but ruled it out because the Anchor `Account` type already +enforces owner = this program" is the right granularity; "I thought about it and decided Y" is not. + +{% include "shared/property_adaptive_thinking.j2" %} + +# Tools + +## Rough draft + +{% with draft_subject = "your property list" %} +{% include "rough_draft_protocol.j2" %} +{% endwith %} +When reviewing your draft, verify each property against the task criteria — verifiability, +non-triviality, a clear violation consequence, and defensibility in your `reasoning`. + +## Source exploration + +{% with source_tools_has_explorer = sort == "existing" %} +{% include "source_tools_system_prompt.j2" %} +{% endwith %} + +Use the tools to ground reasoning in the actual Rust/Anchor implementation when the design is +ambiguous or an attack hinges on a code-level detail — which account checks are (or are not) +present in the `#[derive(Accounts)]` struct, how a PDA is derived, where a CPI's target program +comes from. Don't speculate when you can read the code. diff --git a/composer/testing/ui_harness_autoprove_Counter.py b/composer/testing/ui_harness_autoprove_Counter.py index 4531c2a6..fdc3eb40 100644 --- a/composer/testing/ui_harness_autoprove_Counter.py +++ b/composer/testing/ui_harness_autoprove_Counter.py @@ -220,7 +220,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # # Shape must satisfy pydantic validation of # ``composer.spec.system_model.SourceApplication`` AND the -# ``_validate_connectivity`` validator: unique names + all referenced +# ``validate_solidity_connectivity`` validator: unique names + all referenced # components / external actors exist. One SourceExplicitContract ("Counter") # with one ContractComponent ("Increment"), no interactions, no external # actors — minimal valid shape. @@ -399,7 +399,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # Tools available: memory, write_rough_draft, read_rough_draft, # source_tools = list_files, get_file, grep_files, code_explorer, # code_document_ref. - # Validator: _validate_connectivity (graph wellformedness only; no + # Validator: validate_solidity_connectivity (graph wellformedness only; no # did_read requirement — we can hit `result` at any time once the # application shape is correct). @@ -482,7 +482,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: _tc("read_rough_draft"), ), - # P1.5 — emit the SourceApplication. Satisfies _validate_connectivity + # P1.5 — emit the SourceApplication. Satisfies validate_solidity_connectivity # (unique names, no dangling interaction references since there are no # interactions). _ai( diff --git a/composer/testing/ui_harness_natspec.py b/composer/testing/ui_harness_natspec.py index d0811717..66bc414f 100644 --- a/composer/testing/ui_harness_natspec.py +++ b/composer/testing/ui_harness_natspec.py @@ -259,7 +259,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # Tools available in greenfield: memory, write_rough_draft, # read_rough_draft, result. ``env.analysis_tools`` is empty in # greenfield, so no source/rag tools here. - # Validator: ``_validate_connectivity`` — checks unique names and + # Validator: ``validate_solidity_connectivity`` — checks unique names and # resolved component references. No did_read gate. # P1.1 — exercise the `memory` tool once. The memory backend constrains @@ -272,7 +272,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # P1.2 — emit the Application via the result tool. One ExplicitContract # (Counter) with one ContractComponent (Increment). No external actors, - # no interactions — this keeps ``_validate_connectivity`` happy and the + # no interactions — this keeps ``validate_solidity_connectivity`` happy and the # per-component phases will each run exactly once. # # NOTE: ExplicitContract requires both ``name`` (ContractName) and diff --git a/docs/ecosystem-abstraction.md b/docs/ecosystem-abstraction.md new file mode 100644 index 00000000..95244028 --- /dev/null +++ b/docs/ecosystem-abstraction.md @@ -0,0 +1,261 @@ +# The Ecosystem Abstraction + +AutoProver's shared pipeline is parametric over an **ecosystem** — the blockchain/source +domain being analyzed. The ecosystem supplies the domain-specific *front half* of a run: the +system-model type the analysis phase produces, the analysis and property-extraction prompts, +the source-reading conventions, connectivity validation, how the target's "main" is located, +and how it is split into units. Everything downstream of properties (how a property becomes a +verified artifact) belongs to the **backend**, a separate axis. + +Today two ecosystems are implemented: `EVM` (Solidity, fully wired to the CVL/prover and +Foundry backends) and `SOLANA` (Rust, front half only — analysis + property extraction, gated +by a null backend). + +--- + +## 1. Two orthogonal axes + +The pipeline has a front half and a back half, joined by *properties*: + +``` + ┌─────────── ECOSYSTEM owns ───────────┐ ┌──────── BACKEND owns ────────┐ +source ─analyze─▶ SystemModel ─extract─▶ properties ─formalize─▶ artifact ─verdicts─▶ + (how we MODEL and REASON about (how a property becomes a + the domain: contracts vs programs, checkable, verified artifact: + storage vs accounts, reentrancy CVL + prover / foundry test / …) + vs missing-signer) + └──────── SHARED: report ────────┘ +``` + +- **Ecosystem** = the *front half*: the system-model type, the analysis + property-extraction + prompts, source conventions, connectivity validation, main-unit location, and unit split. +- **Backend** = the *back half*: `prepare_system` → `Formalizer` (`formalize` / `fetch_verdicts`). +- **Report** is shared and domain-neutral. + +The axes meet at the analyzed model: the backend's `prepare_system(analyzed: App)` consumes the +ecosystem's `App` type, so a **backend is written against an ecosystem's model** — the CVL prover +backend needs `SourceApplication`; a Solana backend needs `SolanaApplication`. `run_pipeline` +ties a `PipelineBackend[..., U, Main]` to an `Ecosystem[App, Main, U]`, so the analyzed model, +main-unit, and per-unit values flow through without casts. + +--- + +## 2. The seam + +The seam lives in [composer/pipeline/ecosystem.py](../composer/pipeline/ecosystem.py) as two +frozen dataclasses. An ecosystem factors into a **language** facet (conventions for reading the +analyzed program's *source* — shared by every chain written in that language) and the **chain** +itself (the platform model + prompts). The language here is that of the *code under analysis*, +not the language a backend is implemented in. + +```python +LanguageTag = Literal["solidity", "rust"] +ChainTag = Literal["evm", "solana", "soroban"] # "soroban" is reserved; not yet wired + +@dataclass(frozen=True) +class Language: + name: LanguageTag + default_forbidden_read: str # fs-exclusion regex (Cargo layout vs Foundry layout) + code_explorer_prompt: str # source-navigation framing ("Rust source" vs "Solidity") + vulnerability_patterns_partial: str | None = None # j2 partial of language-level vulnerability patterns + +@dataclass(frozen=True) +class Ecosystem[App: BaseApplication, Main, Unit: FeatureUnit]: + name: ChainTag + language: Language + system_model: type[App] # the pydantic type analysis produces + analysis_prompts: PromptPair # (system, initial) template names + property_prompts: PromptPair + validate_analysis: Callable[[BaseApplication, SourceIdentifier | None], str | None] + locate_main: Callable[[App, SourceCode], Main] # find the "main" contract/program + units: Callable[[Main], list[Unit]] # split into per-unit extraction items + analysis_extra_input: Callable[[SourceCode], list[str | dict]] +``` + +`Main` and `Unit` generalize what were EVM's `ContractInstance` / `ContractComponentInstance` — +thin index wrappers over `App` that the driver hands to the backend and to property inference. +`Unit` is any [`FeatureUnit`](../composer/spec/system_model.py) — the ecosystem-agnostic +interface (`display_name` / `slug` / `unit_index` / `cache_material` / `context_tag` / +`feature_json`) the driver uses for per-unit cache keys, task ids, and labels. + +A registry exposes the ecosystems by chain tag; it is heterogeneous in `App`/`Main`/`Unit` +(each chain has its own model), hence `Ecosystem[Any, Any, Any]`: + +```python +ECOSYSTEMS: dict[ChainTag, Ecosystem[Any, Any, Any]] = {"evm": EVM, "solana": SOLANA} +``` + +--- + +## 3. The EVM ecosystem (`SOLIDITY ⊕ evm`) + +`EVM` is the `SOLIDITY` language facet composed with the `evm` chain. Its members are the +pre-existing EVM types, prompts, and functions bound into the seam — the CVL prover and Foundry +backends run against it unchanged. + +```python +SOLIDITY = Language( + name="solidity", + default_forbidden_read=FS_FORBIDDEN_READ, # Foundry layout: lib/, test/, .sol carve-out + code_explorer_prompt=CODE_EXPLORER_SYS_PROMPT, +) + +EVM: Ecosystem[SourceApplication, ContractInstance, ContractComponentInstance] = Ecosystem( + name="evm", + language=SOLIDITY, + system_model=SourceApplication, + analysis_prompts=PromptPair("application_analysis_system.j2", "application_analysis_prompt.j2"), + property_prompts=PromptPair("property_analysis_system_prompt.j2", "property_analysis_prompt.j2"), + validate_analysis=validate_solidity_connectivity, + locate_main=main_instance, # match by solidity_identifier + units=_evm_units, # one unit per contract component + analysis_extra_input=_evm_analysis_extra_input, +) +``` + +EVM's unit split is one `ContractComponentInstance` per component of the located contract, so +property extraction fans out one agent per component — the historical per-component behavior. + +--- + +## 4. The Solana ecosystem (`RUST ⊕ solana`) + +`SOLANA` is the `RUST` language facet composed with the `solana` chain. The front half is +implemented and exercised by a null (report-only) backend; the verification backend is a +separate effort and not part of this seam. + +```python +RUST = Language( + name="rust", + # Cargo/Anchor layout: hide build output, VCS, lockfiles, and the JS side; keep crate sources + tests/. + default_forbidden_read=r"(^target/.*)|(^\.git.*)|(^node_modules/.*)|(.*\.lock$)", + code_explorer_prompt=RUST_CODE_EXPLORER_PROMPT, # "Rust source … instruction handlers, Accounts, PDAs" + vulnerability_patterns_partial="rust/_vulnerability_patterns.j2", # overflow/underflow, panic!/unwrap/expect, ownership +) + +SOLANA: Ecosystem[SolanaApplication, SolanaProgramInstance, SolanaComponentInstance] = Ecosystem( + name="solana", + language=RUST, + system_model=SolanaApplication, + analysis_prompts=PromptPair("solana/analysis_system.j2", "solana/analysis_prompt.j2"), + property_prompts=PromptPair("solana/property_system.j2", "solana/property_prompt.j2"), + validate_analysis=_solana_validate, + locate_main=_solana_locate_main, # match by program_identifier + units=_solana_units, # one per ProgramComponent of the main program + analysis_extra_input=_solana_analysis_extra_input, +) +``` + +- **System model** ([composer/spec/solana/model.py](../composer/spec/solana/model.py)) — + `SolanaApplication` is the standalone analog of `SourceApplication`: `SolanaProgram`s with + their instructions and account constraints (Solana accounts are **passed in**, not owned + storage), CPI targets, and signers in place of EOA actors. `SolanaProgramInstance` / + `SolanaComponentInstance` are the index-wrapper instances (the latter satisfies + `FeatureUnit`), mirroring EVM's `ContractInstance` / `ContractComponentInstance`. +- **Per-component units.** `units` returns one `SolanaComponentInstance` per `ProgramComponent` + of the main program — the same shape as `_evm_units`. A component is a *capability* (a named + cluster of instructions plus the account state they maintain), produced by system analysis. It + is an authoring and attribution scope, not an execution scope: Crucible still fuzzes the whole + program in one action sequence, and a symbolic backend would not execute sequences at all. + Note `units` is on the **ecosystem** axis, so *every* Solana backend inherits this split — + Crucible today, a Certora Solana Prover (CVLR) backend later — which is why it is chosen on + backend-neutral grounds rather than to suit a fuzzer's cost model. The full design note — + the per-backend analysis and the measurements behind this choice — is **not yet in the tree**; + it lands with the verification backend later in this stack. +- **Validation** — `_solana_validate` mirrors `validate_solidity_connectivity`'s structure over + `SolanaApplication`: unique program identifiers and names, unique instruction slugs within a + program, unique component names/slugs, component interactions resolving to a declared + program+component or authority, and the expected main program present. It adds one rule EVM + has no peer for: the component→instruction mapping must be **valid and total**. EVM's + `external_entry_points` are prose the prompt renders, but a `ProgramComponent`'s `instructions` + are *references* the unit wrapper resolves, so a name that doesn't resolve silently drops an + instruction's account detail from the extraction prompt — and an instruction no component + claims is an entry point no property will ever cover. + +### Prompt composition — the shared Rust fragment + +The `RUST` language facet is chain-independent, so its source conventions and vulnerability-pattern +fragment are authored once and pulled into the chain's prompts by Jinja `{% include %}`. The +Solana property template composes the shared Rust fragment with its own platform fragment: + +```jinja +{# composer/templates/solana/property_prompt.j2 #} +{% include "rust/_vulnerability_patterns.j2" %} {# shared: overflow, panics, unwrap, lossy casts #} +{% include "solana/_vulnerability_patterns.j2" %} {# chain-specific: signer/owner/PDA/CPI checks #} +``` + +`rust/_vulnerability_patterns.j2` (the language facet) states language-level vulnerability +patterns — integer overflow/underflow, `panic!`/`unwrap`/`expect` aborts, lossy conversions, +unchecked results — independent of any chain; `solana/_vulnerability_patterns.j2` adds the +Solana-native ones. Because the Rust facet is factored out this way, it is reusable by any future +Rust chain without copying. + +--- + +## 5. Driver integration + +`run_pipeline` ([composer/pipeline/core.py](../composer/pipeline/core.py)) takes an +`ecosystem` and never hardcodes a domain. It is a required keyword argument — every caller names +its ecosystem (`ecosystem=EVM`, `ecosystem=SOLANA`) rather than inheriting one by omission. + +```python +async def run_pipeline[..., U, Main, App]( + backend: PipelineBackend[P, FormT, H, A, U, Main, App], + run: PipelineRun[P, H], + *, ..., + ecosystem: Ecosystem[App, Main, U], +): + analyzed = await run_component_analysis( + ty=ecosystem.system_model, + system_template=ecosystem.analysis_prompts.system, + initial_template=ecosystem.analysis_prompts.initial, + validate=ecosystem.validate_analysis, + extra_input=[*ecosystem.analysis_extra_input(source), *spec.extra_input], ...) + prepared = await backend.prepare_system(analyzed, run) + ... + batches = await _extract_all(..., ecosystem=ecosystem) # iterates ecosystem.units(prepared.main) +``` + +- **`run_component_analysis`** ([system_analysis.py](../composer/spec/system_analysis.py)) is + generic over the analyzed type and takes the prompt pair + validation function, all three + required. Each is domain-specific, so none carries a default. +- **`run_property_inference`** ([prop_inference.py](../composer/spec/prop_inference.py)) takes the + ecosystem's property prompt pair and a generic `FeatureUnit`. The "expressible downstream" axis + stays backend-owned (`backend_guidance`, from `PipelineBackend`); the "failure modes in this + domain" axis is the ecosystem's prompt. Both axes are required keyword arguments. +- **The natspec pipeline** ([natspec/pipeline.py](../composer/spec/natspec/pipeline.py)) is the + other consumer of both primitives. It takes an `EvmEcosystem` for the prompt pairs and is + Solidity-only otherwise (solc, CVL, interface/stub generation). Its analyzed model comes from + its `MentalModel` — `Application` / `FromSourceApplication`, siblings of `EVM.system_model` + under `BaseApplication` rather than subtypes — so `ecosystem.validate_analysis` does not + typecheck there and it names `validate_solidity_connectivity` directly. +- **`_extract_all`** iterates `ecosystem.units(main)`, running one property-inference agent per + unit — one per component for EVM, one for the whole program for Solana. + +--- + +## 6. What is shared and domain-neutral + +- Source tools (`fs_tools`, `code_explorer`, `code_document_ref`) — language-neutral; they read + Rust as well as Solidity. The only ecosystem inputs are the `forbidden_read` default and the + explorer prompt string. +- The report (`collect` / `Verdict` / schema) and `ReportBackend`. +- Caching, the multi-round property loop, interactive refinement, and the agent plumbing. +- The backend seam itself — a verification backend is "just another backend," paired to an + ecosystem by its `App` model. + +--- + +## 7. Key files + +| Concern | File | +|---|---| +| The ecosystem seam | [composer/pipeline/ecosystem.py](../composer/pipeline/ecosystem.py) | +| Driver integration | [composer/pipeline/core.py](../composer/pipeline/core.py) | +| System analysis (ecosystem-driven) | [composer/spec/system_analysis.py](../composer/spec/system_analysis.py) | +| Property inference (ecosystem-driven) | [composer/spec/prop_inference.py](../composer/spec/prop_inference.py) | +| `FeatureUnit` protocol | [composer/spec/system_model.py](../composer/spec/system_model.py) | +| EVM system model + prompts | [composer/spec/system_model.py](../composer/spec/system_model.py) · `composer/templates/application_analysis_*.j2` · `property_analysis_*.j2` | +| Solana system model | [composer/spec/solana/model.py](../composer/spec/solana/model.py) | +| Solana prompts + shared Rust fragment | `composer/templates/solana/*.j2` · `composer/templates/rust/_vulnerability_patterns.j2` | +| fs-exclusion default (EVM) | [composer/spec/util.py](../composer/spec/util.py) | diff --git a/scripts/autoprove_cache_explorer.py b/scripts/autoprove_cache_explorer.py index f10093c3..733c1f5c 100644 --- a/scripts/autoprove_cache_explorer.py +++ b/scripts/autoprove_cache_explorer.py @@ -215,7 +215,7 @@ async def build_tree_inner( harnessed_app = _build_harnessed_app(sa_leaf.value, config_val) # Find the main contract. The pipeline matches the entry point by - # solidity_identifier (pipeline.core.main_instance), so the explorer does too. + # solidity_identifier (pipeline.ecosystem.main_instance), so the explorer does too. contract_ind = -1 for i, c in enumerate(harnessed_app.contract_components): if c.solidity_identifier == contract_name: diff --git a/tests/test_analysis_input_phrase.py b/tests/test_analysis_input_phrase.py new file mode 100644 index 00000000..42684df0 --- /dev/null +++ b/tests/test_analysis_input_phrase.py @@ -0,0 +1,53 @@ +"""Unit tests for the analysis prompts' optional-design-document handling. + +``run_component_analysis`` takes ``input: SystemDoc | None`` and renders the analysis prompts with +``has_doc``; the ``input_phrase`` macro (``composer/templates/shared/analysis_macros.j2``) is the +one place that decides how each ecosystem's prompts refer to their inputs in both cases. + +These are rendering tests, not golden snapshots: they assert the *branch* each combination takes +(and that no branch promises a document that was never supplied), so the prose stays free to +change. The regression they exist for is silent: the macro used to be imported without +``with context``, which left ``has_doc``/``sort`` Undefined inside it and rendered the no-document +phrasing for every caller — including greenfield, where the document is the only input. +""" + +import pytest + +from composer.templates.loader import load_jinja_template + +EVM_TEMPLATES = ["application_analysis_system.j2", "application_analysis_prompt.j2"] +SOLANA_TEMPLATES = ["solana/analysis_system.j2", "solana/analysis_prompt.j2"] +ALL_TEMPLATES = EVM_TEMPLATES + SOLANA_TEMPLATES + + +@pytest.mark.parametrize("template", ALL_TEMPLATES) +def test_with_a_document_the_prompt_names_both_inputs(template: str) -> None: + rendered = load_jinja_template(template, sort="existing", has_doc=True) + assert "system/design document and the" in rendered + + +@pytest.mark.parametrize("template", ALL_TEMPLATES) +def test_without_a_document_the_prompt_never_mentions_one(template: str) -> None: + rendered = load_jinja_template(template, sort="existing", has_doc=False) + # "No design document accompanies it" is the background's way of saying it is absent; the + # claim under test is that nothing tells the agent it *was* given one. + assert "provided a system/design document" not in rendered + assert "analyzing the system/design document" not in rendered + + +@pytest.mark.parametrize("template", EVM_TEMPLATES) +def test_greenfield_names_only_the_document(template: str) -> None: + # Greenfield is EVM-only (``Ecosystem.supports_greenfield``) and document-only: there is no + # implementation yet, so the input phrase must not offer to read one. + rendered = load_jinja_template(template, sort="greenfield", has_doc=True) + assert "system/design document" in rendered + assert "the system/design document and the implementation" not in rendered + + +@pytest.mark.parametrize("template", ALL_TEMPLATES) +@pytest.mark.parametrize("has_doc", [True, False]) +def test_the_input_phrase_carries_no_article_of_its_own(template: str, has_doc: bool) -> None: + # Call sites write "the {{ input_phrase() }}", so a branch that also leads with "the" doubles + # it — which is exactly what the broken no-document branch used to produce. + rendered = load_jinja_template(template, sort="existing", has_doc=has_doc) + assert "the the" not in rendered diff --git a/tests/test_null_solana_backend.py b/tests/test_null_solana_backend.py new file mode 100644 index 00000000..986bff15 --- /dev/null +++ b/tests/test_null_solana_backend.py @@ -0,0 +1,157 @@ +"""Unit tests for the null Solana backend (``composer/spec/solana/null_backend.py``). + +The null backend is a pure test double for the Solana front half — it records extracted +properties without verifying them. These tests exercise it in isolation: no LLM, no Postgres, +no prover. (The end-to-end live gate that drives real models through it is +``tests/test_solana_gate.py``, marked ``expensive``.) +""" + +import json +from types import SimpleNamespace +from typing import Any, cast + +import pytest + +from composer.spec.solana.model import ( + ProgramComponent, + SolanaApplication, + SolanaComponentInstance, + SolanaProgram, + SolanaProgramInstance, +) +from composer.spec.solana.null_backend import ( + NullArtifact, + NullResult, + NullSolanaArtifactStore, + NullSolanaBackend, + NullSolanaFormalizer, + NullSolanaPrepared, + SOLANA_NULL_GUIDANCE, + SolanaPhase, +) +from composer.spec.types import ProgramName, PropertyFormulation, RustIdentifier + + +def _program_instance() -> SolanaProgramInstance: + program = SolanaProgram( + name=ProgramName("Vault"), + program_identifier=RustIdentifier("vault"), + description="Holds deposits and releases them to the authority.", + instructions=[], + components=[ + ProgramComponent( + name="Custody", + description="Holding deposits and releasing them.", + instructions=[], + account_types=["Vault"], + interactions=[], + requirements=[], + ) + ], + ) + app = SolanaApplication( + application_type="Vault", + description="A single-program token vault.", + components=[program], + ) + return SolanaProgramInstance(0, app) + + +def _unit() -> SolanaComponentInstance: + """The backend's ``Unit`` — a component, not the program (``Main`` is not a ``FeatureUnit``).""" + return SolanaComponentInstance(0, _program_instance()) + + +def _props() -> list[PropertyFormulation]: + return [ + PropertyFormulation( + title="balance_conserved", sort="invariant", + description="The vault balance equals the sum of recorded deposits.", + ), + PropertyFormulation( + title="only_authority_withdraws", sort="safety_property", + description="Only the stored authority can reduce the vault balance.", + ), + ] + + +def _backend(project_root: str) -> NullSolanaBackend: + return NullSolanaBackend(NullSolanaArtifactStore(project_root)) + + +@pytest.mark.asyncio +async def test_formalize_echoes_properties_into_result(): + feat = _unit() + props = _props() + + result = await NullSolanaFormalizer().formalize( + "batch", feat, props, cast(Any, None), cast(Any, None) + ) + + assert isinstance(result, NullResult) + # Every property is echoed back verbatim as its own single-rule mapping. + assert result.property_units() == [ + ("balance_conserved", ["balance_conserved"]), + ("only_authority_withdraws", ["only_authority_withdraws"]), + ] + # Commentary records the unit and the count. + assert feat.display_name in result.commentary + assert "2 properties" in result.commentary + # artifact_text is well-formed JSON carrying the same properties; there is no output link. + parsed = json.loads(result.artifact_text) + assert parsed["properties"] == [ + ["balance_conserved", ["balance_conserved"]], + ["only_authority_withdraws", ["only_authority_withdraws"]], + ] + assert result.output_link is None + + +@pytest.mark.asyncio +async def test_formalize_with_no_properties_records_empty(): + result = await NullSolanaFormalizer().formalize( + "batch", _unit(), [], cast(Any, None), cast(Any, None) + ) + assert isinstance(result, NullResult) + assert result.property_units() == [] + assert "0 properties" in result.commentary + + +@pytest.mark.asyncio +async def test_fetch_verdicts_is_empty(): + # The null backend never verifies, so it surfaces no verdicts. + assert await NullSolanaFormalizer().fetch_verdicts(cast(Any, None)) == {} + + +@pytest.mark.asyncio +async def test_prepare_system_locates_main_and_builds_formalizer(tmp_path): + feat = _program_instance() + backend = _backend(str(tmp_path)) + run = cast(Any, SimpleNamespace(source=SimpleNamespace(contract_name="vault"))) + + prepared = await backend.prepare_system(feat.app, run) + + assert isinstance(prepared, NullSolanaPrepared) + # prepare_system routes through SOLANA.locate_main, so main is the matched program. + assert isinstance(prepared.main, SolanaProgramInstance) + assert prepared.main.program.program_identifier == "vault" + + formalizer = await prepared.prepare_formalization(cast(Any, None)) + assert isinstance(formalizer, NullSolanaFormalizer) + + +def test_to_artifact_id_uses_unit_slug(tmp_path): + feat = _unit() + artifact = _backend(str(tmp_path)).to_artifact_id(feat) + assert isinstance(artifact, NullArtifact) + assert artifact.slug == feat.slug + assert artifact.artifact_file == f"null_{feat.slug}.json" + + +def test_backend_declares_solana_front_half(tmp_path): + backend = _backend(str(tmp_path)) + assert backend.backend_guidance is SOLANA_NULL_GUIDANCE + assert backend.analysis_spec.analysis_key == "solana-analysis" + assert backend.analysis_spec.properties_key == "solana-properties" + assert {p.value for p in SolanaPhase} == { + "analysis", "extraction", "formalization", "report", + } diff --git a/tests/test_pipeline_staged_formalizer.py b/tests/test_pipeline_staged_formalizer.py new file mode 100644 index 00000000..850f02b7 --- /dev/null +++ b/tests/test_pipeline_staged_formalizer.py @@ -0,0 +1,188 @@ +"""``StagedFormalizer.begin``: called once, with every unit's properties, before any unit is +formalized — and what it *returns* is the formalizer the driver then fans out over. + +The staged type exists for backends with a *shared* artifact all units build on (Crucible's fixture; +a future CVLR backend's setup module). Such an artifact must be authored from the union of every +unit's properties and cannot be authored in ``prepare_formalization`` (which overlaps extraction, so +no properties exist yet). Doing it lazily inside ``formalize`` instead means the first unit to +arrive decides the shared artifact for all of them — harmless at one unit, silently wrong at several. +These tests pin both halves: that the driver drives the staged type in that order, and that a backend +returning a plain ``Formalizer`` is never staged at all. + +Stubs throughout — no LLM, no DB, no backend wheel. +""" + +import asyncio + +import pytest + +import composer.pipeline.core as core +from composer.pipeline.core import run_pipeline +from composer.pipeline.ecosystem import EVM +from composer.spec.types import PropertyFormulation + +pytestmark = pytest.mark.asyncio + + +class _Store: + def write_properties(self, *_a, **_kw): ... + def write_artifact(self, *_a, **_kw): return "artifact" + def write_report(self, *_a, **_kw): ... + + +class _Unit: + """The minimum ``FeatureUnit`` the driver touches.""" + + def __init__(self, name: str, index: int): + self.display_name, self.unit_index, self.slug = name, index, name + + def cache_material(self) -> str: return self.display_name + def context_tag(self) -> dict: return {} + def feature_json(self) -> dict: return {} + + +class _Result: + """A ``BackendResult``: only what the driver reads off it.""" + artifact_text = "" + unit_file = None + run_link = None + def property_units(self): return [] + + +class _Formalizer: + """Records the order of ``begin`` / ``formalize`` calls. ``calls`` is shared with the staged half + that built it, so one list holds the whole sequence.""" + + formalized_type = _Result + backend_tag = "foundry" + + def __init__(self, calls: list[tuple[str, list[str]]] | None = None): + self.calls = [] if calls is None else calls + + async def formalize(self, _label, feat, props, _ctx, _run): + # A yield point, so a driver that started the fan-out before `begin` finished would + # interleave here and be caught by the ordering assertion. + await asyncio.sleep(0) + self.calls.append((f"formalize:{feat.display_name}", [p.title for p in props])) + return _Result() + + def extra_report_inputs(self): return [] + async def fetch_verdicts(self, _inp): return {} + async def finalize(self, _outcomes, _run): return None + + +class _Staged(core.StagedFormalizer): + """The staged half. ``begin`` is the only way to obtain the formalizer, so an artifact authored + from every unit's properties cannot be skipped or raced by the fan-out.""" + + def __init__(self): + self.calls: list[tuple[str, list[str]]] = [] + + async def begin(self, jobs, _run): + self.calls.append(("begin", [p.title for j in jobs for p in j.props])) + return _Formalizer(self.calls) + + +class _Prepared: + main = "main-unit" + + def __init__(self, formalizer): self._f = formalizer + + async def prepare_formalization(self, _run): return self._f + + +class _Backend: + analysis_spec = core.SystemAnalysisSpec("analysis-key", "properties-key") + core_phases = {"analysis": 1, "extraction": 2, "formalization": 3, "report": 4} + backend_guidance = "guidance" + artifact_store = _Store() + + def __init__(self, prepared): self._prepared = prepared + + async def prepare_system(self, _analyzed, _run): return self._prepared + + def to_artifact_id(self, _c): return "artifact-id" + + +class _Cache: + async def cache_get(self, _ty): return None + async def cache_put(self, _v): return None + + +class _Ctx: + recursion_limit = 10 + + def child(self, *_a, **_kw): return self + + async def achild(self, *_a, **_kw): return _Cache() + + +class _FeatCtx: + async def child(self, *_a, **_kw): return _Cache() + + +class _Source: + contract_name = "Vault" + relative_path = "programs/vault/src/lib.rs" + + +class _Run: + source = _Source() + env = None + ctx = _Ctx() + + async def runner(self, _task_info, job): + return await job() + + +def _prop(title: str) -> PropertyFormulation: + return PropertyFormulation(title=title, sort="invariant", description="d") + + +async def _drive[F: (_Staged, _Formalizer)]( + monkeypatch, units: dict[str, list[str]], formalizer: F +) -> F: + async def fake_analysis(*_a, **_kw): return "analyzed" + + async def fake_extract_all(*_a, **_kw): + return [ + core._Batch(_Unit(name, i), [_prop(t) for t in titles], _FeatCtx()) # type: ignore[arg-type] + for i, (name, titles) in enumerate(units.items()) + ] + + async def fake_report(*_a, **_kw): return object() + + monkeypatch.setattr(core, "run_component_analysis", fake_analysis) + monkeypatch.setattr(core, "_extract_all", fake_extract_all) + monkeypatch.setattr(core, "build_report", fake_report) + await run_pipeline(_Backend(_Prepared(formalizer)), _Run(), max_bug_rounds=1, ecosystem=EVM) # type: ignore[arg-type] + return formalizer + + +async def test_begin_runs_once_before_any_unit_is_formalized(monkeypatch): + s = await _drive(monkeypatch, {"deposits": ["a"], "admin": ["b"], "farms": ["c"]}, _Staged()) + names = [c[0] for c in s.calls] + assert names[0] == "begin", f"begin must precede every formalize; got {names}" + assert names.count("begin") == 1 + assert sorted(names[1:]) == ["formalize:admin", "formalize:deposits", "formalize:farms"] + + +async def test_begin_sees_every_unit_s_properties(monkeypatch): + # The point of the staged type: the shared artifact is designed around all of them, not around + # whichever unit won the race to formalize first. + s = await _drive(monkeypatch, {"deposits": ["a", "b"], "admin": ["c"], "farms": ["d"]}, _Staged()) + assert s.calls[0] == ("begin", ["a", "b", "c", "d"]) + + +async def test_begin_still_runs_for_a_single_unit(monkeypatch): + # The K=1 case must go down the same path, or the shared artifact would be authored lazily + # again the moment a second unit appears. + s = await _drive(monkeypatch, {"whole-program": ["a", "b"]}, _Staged()) + assert [c[0] for c in s.calls] == ["begin", "formalize:whole-program"] + + +async def test_an_unstaged_formalizer_is_formalized_directly(monkeypatch): + # The other arm of the union: a backend with no shared artifact returns the formalizer itself, + # and the driver must fan out over exactly that object rather than looking for a staging step. + f = await _drive(monkeypatch, {"deposits": ["a"], "admin": ["b"]}, _Formalizer()) + assert sorted(c[0] for c in f.calls) == ["formalize:admin", "formalize:deposits"] diff --git a/tests/test_solana_components.py b/tests/test_solana_components.py new file mode 100644 index 00000000..812641db --- /dev/null +++ b/tests/test_solana_components.py @@ -0,0 +1,235 @@ +"""The Solana ecosystem's ``ProgramComponent`` model and its analysis-time validation. + +Per docs/ecosystem-abstraction.md §4: a program gains ``components`` — the Solana analog +of EVM's ``ContractComponent`` — and ``_solana_validate`` gains the rules that keep the +component→instruction mapping honest. ``units`` is still whole-program at this stage, so nothing +downstream changes; these tests cover the model and the validator in isolation. +""" + +from typing import Any + +import pytest + +from composer.pipeline.ecosystem import _solana_validate +from composer.spec.solana.model import ( + AuthorityInteraction, + InterComponentInteraction, + SolanaApplication, +) +from composer.spec.types import RustIdentifier + +VAULT_ID = RustIdentifier("vault") + + +def _raw() -> dict[str, Any]: + """A well-formed two-component vault, as the analysis agent would emit it.""" + return { + "application_type": "Vault", + "description": "A single-program lamports vault.", + "components": [ + { + "name": "Vault", + "program_identifier": VAULT_ID, + "description": "Holds per-user deposits in a PDA.", + "account_types": ["Vault"], + "instructions": [ + {"name": "initialize", "description": "create the vault PDA", "requirements": []}, + {"name": "deposit", "description": "move lamports in", "requirements": []}, + {"name": "withdraw", "description": "move lamports out", "requirements": []}, + ], + "components": [ + { + "name": "Deposits", + "description": "Creating a vault and funding it.", + "instructions": ["initialize", "deposit"], + "account_types": ["Vault"], + "interactions": [ + {"authority": "System Program", "description": "CPI transfer in"} + ], + "requirements": ["The implementation must credit the depositor."], + }, + { + "name": "Withdrawals", + "description": "Releasing funds to the recorded authority.", + "instructions": ["withdraw"], + "account_types": ["Vault"], + "interactions": [ + { + "program": "Vault", + "component": "Deposits", + "description": "reads the balance Deposits maintains", + } + ], + "requirements": ["The implementation must only pay the authority."], + }, + ], + }, + { + "name": "System Program", + "description": "Solana's native System program.", + "assumptions": ["Behaves per the Solana runtime spec."], + }, + ], + } + + +def _app(mutate=None) -> SolanaApplication: + raw = _raw() + if mutate is not None: + mutate(raw) + return SolanaApplication.model_validate(raw) + + +def _program(raw: dict[str, Any]) -> dict[str, Any]: + return raw["components"][0] + + +def _components(raw: dict[str, Any]) -> list[dict[str, Any]]: + return _program(raw)["components"] + + +# --- the model --------------------------------------------------------------------- + + +def test_components_parse_and_instructions_resolve_through_the_program(): + prog = _app().programs[0] + assert [c.name for c in prog.components] == ["Deposits", "Withdrawals"] + # A component references its instructions by name; the program stays authoritative for the + # objects, and `instructions_by_name` is the one place the names resolve. + deposits = prog.components[0] + resolved = [prog.instructions_by_name[n] for n in deposits.instructions] + assert [i.description for i in resolved] == ["create the vault PDA", "move lamports in"] + + +def test_interaction_union_discriminates_by_shape(): + prog = _app().programs[0] + assert isinstance(prog.components[0].interactions[0], AuthorityInteraction) + inter = prog.components[1].interactions[0] + assert isinstance(inter, InterComponentInteraction) + assert (inter.program, inter.component) == ("Vault", "Deposits") + + +# --- validation: the happy path and the existing rules ------------------------------- + + +def test_well_formed_application_validates(): + assert _solana_validate(_app(), VAULT_ID) is None + + +def test_expected_main_is_still_required(): + problem = _solana_validate(_app(), RustIdentifier("not_the_vault")) + assert problem is not None and "not_the_vault" in problem + + +# --- validation: component rules ----------------------------------------------------- + + +def test_duplicate_component_names_rejected(): + def dup(raw): + _components(raw)[1]["name"] = "Deposits" + + problem = _solana_validate(_app(dup), VAULT_ID) + assert problem is not None and "Duplicate component names in Vault: Deposits" in problem + + +def test_component_slug_collision_rejected(): + # "Deposits!" and "Deposits" are distinct names that slugify to the same artifact id. + def collide(raw): + _components(raw)[1]["name"] = "Deposits!" + + problem = _solana_validate(_app(collide), VAULT_ID) + assert problem is not None and "filename slug" in problem + + +def test_unknown_instruction_reference_rejected(): + def typo(raw): + _components(raw)[0]["instructions"] = ["initialize", "depsoit"] + + problem = _solana_validate(_app(typo), VAULT_ID) + assert problem is not None + assert "lists an instruction 'depsoit' that Vault does not declare" in problem + + +def test_instruction_belonging_to_no_component_rejected(): + def orphan(raw): + _components(raw)[0]["instructions"] = ["initialize"] # drops `deposit` + + problem = _solana_validate(_app(orphan), VAULT_ID) + assert problem is not None and "'deposit'" in problem and "belong to no component" in problem + + +def test_an_instruction_may_serve_two_components(): + def overlap(raw): + _components(raw)[1]["instructions"] = ["withdraw", "initialize"] + + assert _solana_validate(_app(overlap), VAULT_ID) is None + + +def test_a_program_with_no_instructions_needs_no_components(): + def empty(raw): + _program(raw)["instructions"] = [] + _program(raw)["components"] = [] + + assert _solana_validate(_app(empty), VAULT_ID) is None + + +# --- validation: interactions -------------------------------------------------------- + + +@pytest.mark.parametrize( + "interaction, expected", + [ + ({"authority": "Pyth", "description": "reads a price"}, "unknown external authority: Pyth"), + ( + {"program": "Staking", "component": None, "description": "x"}, + "an unknown program: Staking", + ), + ( + {"program": "Vault", "component": "Rewards", "description": "x"}, + "unknown component Rewards of program Vault", + ), + ], +) +def test_unresolvable_interactions_rejected(interaction, expected): + def point_nowhere(raw): + _components(raw)[0]["interactions"] = [interaction] + + problem = _solana_validate(_app(point_nowhere), VAULT_ID) + assert problem is not None and expected in problem + + +def test_a_forward_reference_between_components_is_fine(): + # Interactions are resolved in a second pass, so Deposits may name a component declared after + # it (the EVM validator does the same). + def forward(raw): + _components(raw)[0]["interactions"] = [ + {"program": "Vault", "component": "Withdrawals", "description": "hands off"} + ] + + assert _solana_validate(_app(forward), VAULT_ID) is None + + +# --- validation: the retry feedback -------------------------------------------------- + + +def test_feedback_lists_the_declared_names_for_the_retry(): + def typo(raw): + _components(raw)[0]["instructions"] = ["initialize", "depsoit"] + + problem = _solana_validate(_app(typo), VAULT_ID) + assert problem is not None + assert "For reference, the names you declared in your submission:" in problem + assert "- Declared programs: Vault" in problem + assert "- Declared external authorities: System Program" in problem + assert "- Components of Vault: Deposits, Withdrawals" in problem + + +def test_multiple_errors_are_all_reported(): + def two_problems(raw): + _components(raw)[1]["name"] = "Deposits" + _components(raw)[0]["interactions"] = [{"authority": "Pyth", "description": "x"}] + + problem = _solana_validate(_app(two_problems), VAULT_ID) + assert problem is not None + assert problem.startswith("Multiple validation errors") + assert "Duplicate component names" in problem and "Pyth" in problem