diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md new file mode 100644 index 00000000..6aa336e4 --- /dev/null +++ b/ARCHITECTURE.md @@ -0,0 +1,316 @@ +# 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. +- **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)` (EVM yields one per contract component; a whole-program ecosystem + like Solana yields a single unit that is the program) — 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 its own whole-program types. 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 whole-program `units()` (one + unit per program rather than per component). 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..e662afc0 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,29 @@ +# 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. + +## 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/foundry/pipeline.py b/composer/foundry/pipeline.py index ef7c323e..918de59b 100644 --- a/composer/foundry/pipeline.py +++ b/composer/foundry/pipeline.py @@ -78,7 +78,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 +106,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 +138,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 +166,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..45cb65db 100644 --- a/composer/pipeline/cli.py +++ b/composer/pipeline/cli.py @@ -20,6 +20,7 @@ CorePipelineResult ) from composer.spec.artifacts import ArtifactIdentifier +from composer.spec.system_model import FeatureUnit from composer.spec.service_host import ModelProvider from composer.spec.system_analysis import SolidityIdentifier from .core import PipelineBackend, run_pipeline @@ -113,10 +114,10 @@ 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]( self, env: ServiceHost, - backend: PipelineBackend[P, FormT, H, A] + backend: PipelineBackend[P, FormT, H, A, U, Main] ) -> CorePipelineResult[FormT]: ... @@ -249,9 +250,9 @@ 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]( env: ServiceHost, - backend: PipelineBackend[P, FormT, H, A] + backend: PipelineBackend[P, FormT, H, A, U, Main] ) -> CorePipelineResult[FormT]: full_ctx = WorkflowContext.create( services=conns.memory, diff --git a/composer/pipeline/core.py b/composer/pipeline/core.py index 3c92a585..5f42ae9d 100644 --- a/composer/pipeline/core.py +++ b/composer/pipeline/core.py @@ -17,10 +17,9 @@ import enum import logging from dataclasses import dataclass -from typing import Protocol +from typing import Protocol, Any, cast from abc import ABC, abstractmethod -from pydantic import BaseModel from composer.io.multi_job import TaskInfo from composer.spec.artifacts import ArtifactStore @@ -28,7 +27,7 @@ WorkflowContext, CacheKey, Properties, ComponentGroup, SourceCode ) from composer.spec.system_model import ( - SourceApplication, ContractInstance, ContractComponentInstance, AnyApplication + SourceApplication, FeatureUnit ) from composer.spec.types import PropertyFormulation, ArtifactIdentifier from composer.spec.system_analysis import run_component_analysis @@ -40,6 +39,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 +# The ecosystem seam supplies the domain-specific front half (analyzed model type, prompts, +# analysis validation, unit enumeration). ``main_instance`` moved here too and is re-exported +# so existing EVM backends keep doing ``from composer.pipeline.core import main_instance``. +from composer.pipeline.ecosystem import Ecosystem, EVM, main_instance from .ptypes import ( BackendJob, BackendResult, ComponentOutcome, CorePhases, CorePipelineResult, Delivered, GaveUp, PipelineRun, SystemAnalysisSpec ) @@ -49,18 +52,22 @@ _log = logging.getLogger(__name__) @dataclass -class Formalizer[FormT: BackendResult](ABC): +class Formalizer[FormT: BackendResult, U: FeatureUnit](ABC): """Immutable, fully constructed by prepare_formalization. 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 +84,26 @@ 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 @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]: ... -class PipelineBackend[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentifier](Protocol): +class PipelineBackend[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentifier, U: FeatureUnit, Main](Protocol): @property def backend_guidance(self) -> str: ... @@ -106,9 +119,9 @@ def artifact_store(self) -> ArtifactStore[A, FormT]: ... async def prepare_system( self, analyzed: SourceApplication, 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 +129,25 @@ 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 _batch_cache_key[FormT: BaseModel](props: list[PropertyFormulation]) -> CacheKey[ComponentGroup, FormT]: +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: BackendResult]( + props: list[PropertyFormulation], result_type: type[FormT] +) -> CacheKey[ComponentGroup, FormT]: + # The cache VALUE type can't be inferred from ``props`` (they don't carry the backend's + # result type), and ``CacheKey``/``WorkflowContext`` are invariant — so a bare bound + # (``CacheKey[ComponentGroup, BackendResult]``) won't assign to the caller's + # ``WorkflowContext[FormT]``, and a return-only TypeVar trips ``reportInvalidTypeVarUse``. + # Take the concrete ``result_type`` (the formalizer's ``formalized_type``) as a witness so + # ``FormT`` is inferred from an argument: the key is typed to exactly the caller's result. return CacheKey(string_hash("|".join(p.model_dump_json() for p in props))) @@ -147,28 +159,45 @@ 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]( + backend: PipelineBackend[P, FormT, H, A, U, Main], run: PipelineRun[P, H], *, interactive: bool = False, threat_model: Document | None = None, max_bug_rounds: int = 3, + ecosystem: Ecosystem[Any, Any, Any] = EVM, ) -> CorePipelineResult[FormT]: + # ``ecosystem`` supplies the domain-specific front half; it defaults to ``EVM``, which + # reproduces the previous hardcoded Solidity behavior exactly, so EVM callers (and cli.py) + # need pass nothing. Non-EVM backends (e.g. the Rust/Crucible backend) pass ``ecosystem=SOLANA``. + # + # Its ``[App, Main, Unit]`` params are deliberately erased to ``Any``, not tied to the + # backend's — ``Ecosystem`` is INVARIANT (it holds callables that both consume and produce + # those types), so ``Ecosystem[SolanaApplication, …]`` and ``Ecosystem[SourceApplication, …]`` + # are unrelated. At this generic boundary the backend (hence its ``Main``) is itself a free + # var, and — by invariance — a concretely-typed argument (the ``EVM`` default, or an explicit + # ``SOLANA``) can't unify with a tied ``Main``; the only type accepting both is ``Any``. The + # coupling is loose besides: ``prepare_system`` fixes ``analyzed: SourceApplication`` (so a + # non-EVM ``App`` can't be tied without making it generic), and the backend's ``U`` isn't the + # ecosystem's ``Unit`` (the null backend uses ``FeatureUnit``; whole-program extraction yields + # one program-level unit) — which is why the unit list is ``cast`` below, not inferred. + # So the backend↔ecosystem pairing is a runtime contract; the caller is trusted to pair them. spec, phases = backend.analysis_spec, backend.core_phases source = run.source - # 1. System analysis (shared primitive, backend-parameterized; always yields SourceApplication). + # 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: @@ -181,30 +210,36 @@ async def run_pipeline[P: enum.Enum, FormT: BackendResult, H, A: ArtifactIdentif # this preserves the prover's autosetup ∥ bug-analysis overlap, generically. formalizer_task = asyncio.create_task(prepared.prepare_formalization(run)) - batches = await _extract_all( - backend.analysis_spec.properties_key, - prepared.main, backend.backend_guidance, run, - phases["extraction"], interactive, threat_model, max_bug_rounds + # Extraction yields ``FeatureUnit`` batches (the ecosystem is invariant in its unit type and + # callers pass a concrete chain, so it can't be tied to the backend's ``U`` at the signature). + # The paired backend guarantees these units are its ``U``; widen once, here, honestly. + batches: list[_Batch[U]] = cast( + "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, ecosystem), ) formalizer = await formalizer_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]: + 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, formalizer.formalized_type), + {"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), @@ -232,7 +267,7 @@ async def _run(batch: _Batch) -> ComponentOutcome[FormT]: # 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, ) @@ -256,32 +291,41 @@ async def _run(batch: _Batch) -> ComponentOutcome[FormT]: async def _extract_all[P: enum.Enum, H]( prop_key: str, - main: ContractInstance, backend_guidance: str, run: PipelineRun[P, H], + # ``main`` stays untyped here: this internal helper drives the type-erased + # ``Ecosystem[Any, Any, Any]`` (see run_pipeline), so there is nothing to tie it to. + main: Any, backend_guidance: str, run: PipelineRun[P, H], phase: P, interactive: bool, threat_model: Document | None, max_rounds: int, -) -> list[_Batch]: + ecosystem: Ecosystem[Any, Any, Any], +) -> list[_Batch[FeatureUnit]]: 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: FeatureUnit) -> _Batch[FeatureUnit] | 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..23a57d9d --- /dev/null +++ b/composer/pipeline/ecosystem.py @@ -0,0 +1,292 @@ +"""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_connectivity``, +``main_instance``, and unit enumeration into the seam; ``SOLANA = RUST ⊕ solana`` binds the +Solana model + prompts and reuses the shared ``RUST`` language facet. The driver defaults to +``EVM``, so Solidity applications pass no ecosystem. See ``docs/ecosystem-abstraction.md``. +""" + +from dataclasses import dataclass +from typing import Any, Callable, Literal + +from composer.spec.context import SourceCode +from composer.spec.code_explorer import CODE_EXPLORER_SYS_PROMPT +from composer.spec.system_analysis import _validate_connectivity +from composer.spec.system_model import ( + AnyApplication, + BaseApplication, + ContractComponentInstance, + ContractInstance, + FeatureUnit, + SolidityIdentifier, + SourceApplication, +) +from composer.spec.solana.model import ( + SolanaApplication, + SolanaProgramInstance, +) +from composer.spec.util import FS_FORBIDDEN_READ + +LanguageTag = Literal["solidity", "rust"] +ChainTag = Literal["evm", "solana", "soroban"] + + +@dataclass(frozen=True) +class PromptPair: + """A (system prompt, initial prompt) template-name pair for one agent.""" + + system: str + initial: str + + +@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). + + This is emphatically **not** the language the AutoProver backend is *implemented* in: a + backend implemented as a Rust wheel (:mod:`composer.rustapp`) may analyze Solidity + (``echoprover`` → EVM) or Rust (Crucible → Solana). The implementation language is not + associated with the ecosystem; only the analyzed-source language is. + + Its members are captured here for the seam; consumers (the entry point's ``forbidden_read``, + the ``code_explorer`` prompt) are rewired to read from it in a later phase, when a + non-Solidity analyzed language first needs them.""" + + name: LanguageTag + default_forbidden_read: str + code_explorer_prompt: str + # The j2 partial with this language's failure modes (overflow, panics, …). Reserved for + # the prompt-fragment split; unused while prompts are still monolithic. + failure_modes_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 + #: Prompts for the per-component property-inference agent. + property_prompts: PromptPair + #: Connectivity/shape validation of the analyzed model (retry feedback on failure). + #: Typed over ``BaseApplication`` (not ``App``): the validator receives the produced model + #: and narrows internally (as ``_validate_connectivity`` does), and this keeps it assignable + #: to ``run_component_analysis``'s ``validate`` parameter without a contravariance clash. + validate_analysis: Callable[[BaseApplication, SolidityIdentifier | 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. EVM + #: returns one per component; a whole-program ecosystem (Solana) returns a singleton ``[main]``, + #: so all its invariants are inferred + formalized in a single harness + run + #: (docs/crucible-unit-granularity.md §3). + 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]] + + +# --------------------------------------------------------------------------- +# 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 become language-neutral. +# 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: 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_connectivity, + locate_main=main_instance, + 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, + failure_modes_partial="rust/_failure_modes.j2", +) + + +# --------------------------------------------------------------------------- +# The Solana chain (RUST ⊕ solana) +# --------------------------------------------------------------------------- + + +def _solana_validate(app: BaseApplication, expected_main: SolidityIdentifier | None) -> str | None: + """Connectivity/shape validation for a ``SolanaApplication`` (retry feedback on failure). + Mirrors the EVM ``_validate_connectivity`` structure: unique program identifiers, unique + instruction slugs within a program, the expected main program present, CPI targets known.""" + if not isinstance(app, SolanaApplication): + return None + errors: list[str] = [] + known_programs: set[str] = set() + for prog in app.programs: + if prog.program_identifier in known_programs: + errors.append(f"Duplicate program identifier: {prog.program_identifier}") + known_programs.add(prog.program_identifier) + slug_origin: dict[str, str] = {} + from composer.spec.util import slugify_filename + + 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 + # CPI targets may be well-known external programs (SPL Token, System, …) + # that are not declared in the model; we do not flag those. A future + # policy can require known_programs | known_authorities | an allowlist. + if expected_main is not None and expected_main not in known_programs: + errors.append( + f"Expected a program with identifier {expected_main!r}; declared programs: " + f"{sorted(known_programs) or '(none)'}." + ) + if not errors: + return None + if len(errors) == 1: + return errors[0] + return "Multiple validation errors; fix all before resubmitting:\n" + "\n".join(f"- {e}" for e in errors) + + +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[SolanaProgramInstance]: + # Whole-program mode: a single unit that IS the program — so all invariants are inferred and + # formalized in one harness + run (docs/crucible-unit-granularity.md §3). SolanaProgramInstance + # is itself a FeatureUnit, so the driver reads it directly to propose whole-program invariants. + return [main] + + +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." + ] + + +# Whole-program mode: ``units`` returns a singleton ``[main]`` (the ``Unit`` type param is +# ``SolanaProgramInstance``, same as ``Main``). We may support finer-grained units in the future. +SOLANA: Ecosystem[SolanaApplication, SolanaProgramInstance, SolanaProgramInstance] = 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, + units=_solana_units, + analysis_extra_input=_solana_analysis_extra_input, +) + + +#: Registry of available ecosystems, keyed by chain tag. Heterogeneous in ``App``/``Main``/``Unit`` +#: (each chain has its own model), hence ``Ecosystem[Any, Any, Any]``. +ECOSYSTEMS: dict[ChainTag, Ecosystem[Any, Any, Any]] = {"evm": EVM, "solana": SOLANA} diff --git a/composer/pipeline/ptypes.py b/composer/pipeline/ptypes.py index e665c790..43f65fda 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 @@ -71,8 +71,12 @@ class SystemAnalysisSpec: @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 +98,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/prop_inference.py b/composer/spec/prop_inference.py index 3edc92c0..635137ab 100644 --- a/composer/spec/prop_inference.py +++ b/composer/spec/prop_inference.py @@ -21,7 +21,7 @@ from composer.spec.context import WorkflowContext, CacheKey, ComponentGroup 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 @@ -101,13 +101,14 @@ class RefinementState(MessagesState): def _get_initial_prompt( - context: ContractComponentInstance, + context: FeatureUnit, sort: Sort, prev_results: list[_AgentRoundResult], backend_guidance: str, + template: str = "property_analysis_prompt.j2", ) -> str: return load_jinja_template( - "property_analysis_prompt.j2", + template, context=context, backend_guidance=backend_guidance, sort=sort, @@ -279,12 +280,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: str = "property_analysis_system_prompt.j2", + initial_template: str = "property_analysis_prompt.j2", ) -> _AgentRoundWithHistory: round_ctx = ctx.child(agent_round_key(round)) if (cached := await round_ctx.cache_get(_AgentRoundWithHistory)) is not None: @@ -305,13 +308,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 + system_template, sort=env.sort ).compile_async() flow_input: BugAnalysisInput = BugAnalysisInput( @@ -341,11 +344,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: str = "property_analysis_system_prompt.j2", + initial_template: str = "property_analysis_prompt.j2", ) -> _AgentResult: if (cached := await agent_component_analysis.cache_get(_AgentResult)) is not None: return cached @@ -367,7 +372,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,12 +394,15 @@ 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, + *, + system_template: str = "property_analysis_system_prompt.j2", + initial_template: str = "property_analysis_prompt.j2", ) -> list[PropertyFormulation]: """ Extract security properties for a component. @@ -419,6 +427,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..63f53c3d --- /dev/null +++ b/composer/spec/solana/__init__.py @@ -0,0 +1,9 @@ +"""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``) and the index-wrapper instances the driver iterates +(``SolanaProgramInstance`` / ``SolanaInstructionInstance``, 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..13b70c91 --- /dev/null +++ b/composer/spec/solana/model.py @@ -0,0 +1,274 @@ +"""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. + +``SolanaApplication`` is what the shared analysis phase produces (it is a ``BaseApplication`` +so ``run_component_analysis`` accepts it). ``SolanaProgramInstance`` / ``SolanaInstructionInstance`` +are the driver's ``Main`` / ``Unit``: thin index wrappers over the model, with the instruction +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 PropertyFormulation +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 SolanaProgram(BaseModel): + """A concrete on-chain program in the system.""" + + name: str = Field( + description="A short conceptual name for the program, used to refer to it across the system." + ) + program_identifier: str = 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.", + ) + + +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``. + + Also serves as the **whole-program extraction unit** (satisfies + ``composer.spec.system_model.FeatureUnit``): under the global extraction strategy + (docs/crucible-unit-granularity.md) it is the context the property phase reads to + propose whole-program invariants, before those invariants fan out into + :class:`SolanaInvariantUnit`\\ s.""" + + ind: int + app: SolanaApplication + + @property + def program(self) -> SolanaProgram: + return self.app.programs[self.ind] + + # -- FeatureUnit protocol (whole-program extraction context) ------------------------ + @property + def display_name(self) -> str: + return self.program.name + + @property + def slug(self) -> str: + return slugify_filename(self.program.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), "program"]) + + def context_tag(self) -> dict[str, object]: + return {"program": self.program.model_dump()} + + def feature_json(self) -> dict[str, object]: + return { + "program": self.program.name, + "instructions": [i.model_dump(mode="json") for i in self.program.instructions], + } + + +@dataclass +class SolanaInvariantUnit: + """One whole-program invariant — a ``Unit`` for the global extraction strategy. + + Produced by fanning the invariants out of a single whole-program extraction, so each + invariant gets its own harness fn + fuzz run + report row (satisfies + ``composer.spec.system_model.FeatureUnit``). The invariant travels in the formalize + batch's ``props``; ``feature_json`` carries the whole-program API so the test author + can drive any ``action_*`` in the sequence it asserts over.""" + + ind: int + _program: SolanaProgramInstance + invariant: PropertyFormulation + + @property + def app(self) -> SolanaApplication: + return self._program.app + + @property + def program(self) -> SolanaProgram: + return self._program.program + + # -- FeatureUnit protocol ----------------------------------------------------------- + @property + def display_name(self) -> str: + return self.invariant.title + + @property + def slug(self) -> str: + return slugify_filename(self.invariant.title) + + @property + def unit_index(self) -> int: + return self.ind + + def cache_material(self) -> str: + return "|".join( + [self.app.model_dump_json(), str(self._program.ind), str(self.ind), self.invariant.title] + ) + + def context_tag(self) -> dict[str, object]: + return {"invariant": self.invariant.model_dump(mode="json"), "program": self.program.name} + + def feature_json(self) -> dict[str, object]: + return { + "program": self.program.name, + "instructions": [i.model_dump(mode="json") for i in self.program.instructions], + } + + +@dataclass +class SolanaInstructionInstance: + """One instruction of the target program — the ecosystem's ``Unit`` (satisfies + ``composer.spec.system_model.FeatureUnit``).""" + + ind: int + _program: SolanaProgramInstance + + @property + def app(self) -> SolanaApplication: + return self._program.app + + @property + def program(self) -> SolanaProgram: + return self._program.program + + @property + def instruction(self) -> SolanaInstruction: + return self.program.instructions[self.ind] + + # -- FeatureUnit protocol ----------------------------------------------------------- + @property + def display_name(self) -> str: + return self.instruction.name + + @property + def slug(self) -> str: + return slugify_filename(self.instruction.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 {"instruction": self.instruction.model_dump()} + + def feature_json(self) -> dict[str, object]: + # The unit's semantic content for a backend marshalling it across a boundary: + # the instruction, tagged with its program (a Solana backend needs both). + return { + "program": self.program.name, + "instruction": self.instruction.model_dump(mode="json"), + } diff --git a/composer/spec/solana/null_backend.py b/composer/spec/solana/null_backend.py new file mode 100644 index 00000000..5f7e3e1d --- /dev/null +++ b/composer/spec/solana/null_backend.py @@ -0,0 +1,175 @@ +"""A null Solana backend — records extracted properties without verifying them. + +It satisfies the full ``PipelineBackend`` contract over the Solana ecosystem's +``(SolanaApplication, SolanaProgramInstance, SolanaInstructionInstance)`` 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 cast, 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, + SolanaInstructionInstance, + SolanaProgramInstance, +) +from composer.spec.source.report.collect import ReportComponentInput, Verdict +from composer.spec.source.report.schema import ReportBackend, RuleName +from composer.spec.system_model import FeatureUnit +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, FeatureUnit]): + def __init__(self) -> None: + # Reuses the ``"crucible"`` report backend (the real Solana verifier this null backend + # models); its results are all-UNKNOWN, so the label choice is provenance only. + # Intermediate (PR1): report/schema.py's ReportBackend literal is still master's + # {prover, foundry}; cast the tag until PR3 closes the literal to include "crucible". + super().__init__(NullResult, cast(ReportBackend, "crucible")) + + @override + async def formalize( + self, + label: str, + feat: FeatureUnit, + 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, FeatureUnit, SolanaProgramInstance]): + form: NullSolanaFormalizer + + @override + async def prepare_formalization( + self, run: PipelineRun + ) -> Formalizer[NullResult, FeatureUnit]: + return self.form + + +@dataclass +class NullSolanaBackend: + """``PipelineBackend[SolanaPhase, NullResult, None, NullArtifact, FeatureUnit, + SolanaProgramInstance]`` (P, FormT, H, A, Unit, Main) — 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, FeatureUnit, 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: FeatureUnit) -> NullArtifact: + return NullArtifact(c.slug) diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index c6ac5120..5218666c 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, ) @@ -98,7 +98,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 +149,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 +164,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 +175,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 +272,8 @@ async def _invariants(self, run: PipelineRun): @dataclass class ProverBackend: - """PipelineBackend[AutoProvePhase, GeneratedCVL, None, ComponentSpec].""" + """PipelineBackend[AutoProvePhase, GeneratedCVL, None, ComponentSpec, + ContractComponentInstance, ContractInstance] (P, FormT, H, A, Unit, Main).""" backend_guidance = CERTORA_BACKEND_GUIDANCE core_phases = CorePhases({ "analysis": AutoProvePhase.COMPONENT_ANALYSIS, @@ -287,7 +288,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..a5661f3d 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 from graphcore.graph import MessagesState, FlowInput @@ -95,8 +95,16 @@ async def run_component_analysis[T: BaseApplication]( env: ServiceHost, extra_input: list[str | dict], expected_main_id: SolidityIdentifier | None = None, + *, + system_template: str = "application_analysis_system.j2", + initial_template: str = "application_analysis_prompt.j2", + validate: Callable[[BaseApplication, SolidityIdentifier | None], str | None] = _validate_connectivity, ) -> T | None: - """Analyze application components from a system doc and optionally source code.""" + """Analyze application components from a system doc and optionally source code. + + The prompt templates and connectivity ``validate`` are parameters so the ecosystem + (``composer.pipeline.ecosystem``) can supply domain-specific ones; the defaults are the + EVM/Solidity values, so existing callers are unaffected.""" if (cached := await child_ctxt.cache_get(ty)) is not None: return cached @@ -114,7 +122,7 @@ class AnalysisInput(RoughDraftState, FlowInput): def _validation_wrapper( _: Any, app: BaseApplication ) -> str | None: - return _validate_connectivity(app, expected_main_id) + return validate(app, expected_main_id) b = bind_standard( builder=env.builder_lite(), @@ -123,13 +131,13 @@ def _validation_wrapper( ).with_input( AnalysisInput ).with_sys_prompt_template( - "application_analysis_system.j2", + system_template, sort=env.sort, has_doc=input is not None ).with_tools( [memory, *get_rough_draft_tools(AnalysisState), *env.analysis_tools] ).with_initial_prompt_template( - "application_analysis_prompt.j2", + initial_template, sort=env.sort, has_doc=input is not None ) diff --git a/composer/spec/system_model.py b/composer/spec/system_model.py index 7bdb4059..0b31a824 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") @@ -234,6 +275,28 @@ def slugified_name(self) -> str: ``_validate_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/templates/application_analysis_prompt.j2 b/composer/templates/application_analysis_prompt.j2 index 7a303af6..26e308bb 100644 --- a/composer/templates/application_analysis_prompt.j2 +++ b/composer/templates/application_analysis_prompt.j2 @@ -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..4b6a6ea8 100644 --- a/composer/templates/application_analysis_system.j2 +++ b/composer/templates/application_analysis_system.j2 @@ -3,19 +3,7 @@ You are an experienced system architect who is also well-versed in Web3 (blockch 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/_failure_modes.j2 b/composer/templates/rust/_failure_modes.j2 new file mode 100644 index 00000000..99d71091 --- /dev/null +++ b/composer/templates/rust/_failure_modes.j2 @@ -0,0 +1,15 @@ +Rust language-level failure modes (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_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/_failure_modes.j2 b/composer/templates/solana/_failure_modes.j2 new file mode 100644 index 00000000..0da21b80 --- /dev/null +++ b/composer/templates/solana/_failure_modes.j2 @@ -0,0 +1,30 @@ +Solana platform failure modes (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..b02d3447 --- /dev/null +++ b/composer/templates/solana/analysis_prompt.j2 @@ -0,0 +1,70 @@ +# Background + +{% if sort == "greenfield" %} +You have been provided a system/design document describing a Solana application. No +implementation exists yet, and the document may vary in technical rigor. +{% else %} +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. +{% endif %} + +# Task + +Analyze this design document {% if sort != "greenfield" %}and implementation {% endif %}and extract a holistic, structured model of the +application. Your model describes the **programs** {% if sort == "greenfield" %}that need to be written{% else %}present in the implementation{% endif %}, 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. + +#### 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 ..."). + +## 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..b2878760 --- /dev/null +++ b/composer/templates/solana/analysis_system.j2 @@ -0,0 +1,17 @@ +You are an experienced system architect well-versed in Solana on-chain programs (native and +Anchor). You are analyzing a Solana application's design document {% if sort != "greenfield" %}and its Rust implementation {% endif %}to extract a +structured model of its behavior. This model guides the {% if sort != "greenfield" %}verification{% else %}implementation{% endif %} of the application. + +{% include "shared/architect_behavior_tools.j2" %} +{% with draft_subject = "your response" %} +{% include "rough_draft_protocol.j2" %} +{% endwith %} +{% if sort != "greenfield" %} +{% 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. +{% endif %} diff --git a/composer/templates/solana/instruction_context.j2 b/composer/templates/solana/instruction_context.j2 new file mode 100644 index 00000000..19e7fb36 --- /dev/null +++ b/composer/templates/solana/instruction_context.j2 @@ -0,0 +1,52 @@ +This task targets the security properties of the instruction `{{ context.instruction.name }}` +of the program `{{ context.program.name }}` (`{{ context.program.program_identifier }}`). + +This instruction is described as: + +{{ context.instruction.description }} + +The requirements for this instruction are: +{% for req in context.instruction.requirements %} +* {{ req }} +{% endfor %} +{% if context.instruction.args %} + +Non-account arguments: {% for a in context.instruction.args %}`{{ a }}`{% if not loop.last %}, {% endif %}{% endfor %}. +{% endif %} + +Accounts this instruction takes, and the checks the program is responsible for enforcing on each: +{% for acc in context.instruction.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 context.instruction.signers %} + +Accounts that must sign: {{ context.instruction.signers | join(", ") }}. +{% endif %} +{% if context.instruction.cpis %} + +Cross-program invocations this instruction performs: +{% for cpi in context.instruction.cpis %} +* → `{{ cpi.target_program }}`: {{ cpi.description }} +{% endfor %} +{% endif %} + +The `{{ context.program.name }}` program is part of a `{{ context.app.application_type }}` application. +{% if context.program.account_types %} +It owns / derives these account (state) types: {{ context.program.account_types | join(", ") }}. +{% endif %} + +{% set siblings = [] %} +{% for p in context.app.programs %}{% if p.program_identifier != context.program.program_identifier %}{% set _ = siblings.append(p) %}{% endif %}{% endfor %} +{% if siblings %} +Other programs in the application: +{% for p in siblings %} +* `{{ 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 %} diff --git a/composer/templates/solana/program_context.j2 b/composer/templates/solana/program_context.j2 new file mode 100644 index 00000000..03cb993d --- /dev/null +++ b/composer/templates/solana/program_context.j2 @@ -0,0 +1,21 @@ +This task targets whole-program security invariants of the program `{{ context.program.name }}` +(`{{ context.program.program_identifier }}`), part of a `{{ context.app.application_type }}` application. + +{% if context.program.account_types %} +The program owns / derives these account (state) types: {{ context.program.account_types | join(", ") }}. +{% endif %} + +The program exposes these instructions (the actions a fuzzer will drive in random sequences): +{% for ins in context.program.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 (and the checks the program must enforce): +{% for acc in ins.accounts %} - `{{ acc.name }}` — {{ acc.account_type }}{% if acc.roles %} [{{ acc.roles | join(", ") }}]{% endif %}{% if acc.constraints %}; constraints: {{ acc.constraints | join("; ") }}{% endif %}. +{% endfor %}{% if ins.signers %}Must sign: {{ ins.signers | join(", ") }}. +{% endif %}{% if ins.cpis %}CPIs: {% for cpi in ins.cpis %}→ `{{ cpi.target_program }}` ({{ cpi.description }}){% if not loop.last %}; {% endif %}{% endfor %}. +{% endif %} +{% endfor %} diff --git a/composer/templates/solana/property_prompt.j2 b/composer/templates/solana/property_prompt.j2 new file mode 100644 index 00000000..a645c41b --- /dev/null +++ b/composer/templates/solana/property_prompt.j2 @@ -0,0 +1,92 @@ + +You are performing a security review of a Solana program as a whole, to produce **program-level +invariants** for a coverage-guided fuzzer. The fuzzer drives *random sequences* of the program's +instructions and checks each property after every action — so the properties you write must hold +across ANY reachable sequence of actions, not only within a single instruction. + + + +{% include "solana/program_context.j2" %} + + +{% with unit_noun = "program" %}{% include "shared/prior_properties.j2" %}{% endwith %} + + +Input: {% if sort != "greenfield" %}the Rust/Anchor implementation of a Solana program{% else %}a design document for a Solana program{% endif %}, and a description of its instructions. +Output: a list of whole-program "security properties" a fuzzer can check after every action. + +Follow these steps exactly: + +## Step 1 + +Analyze the provided {% if sort != "greenfield" %}implementation{% else %}design{% endif %} and formulate a set of security +properties that are PLAUSIBLE for this program. Prefer **cross-instruction** properties — ones a +random sequence of actions could violate (conservation, monotonicity, access control that must hold +no matter what came before) — over ones local to a single call. Each description must be precise and +concise, and phrased as something checkable against on-chain state after any action. + +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, + over any action sequence. + 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 {% if sort != "greenfield" %}implementation{% else %}design{% endif %}. + 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 failure modes: + +{% include "rust/_failure_modes.j2" %} + +{% include "solana/_failure_modes.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 as a whole-program invariant. Drop anything +you cannot defend. + +## Step 4 +Output the results using the result tool. + + + + {% if sort != "greenfield" %} + + Derive invariants and safety properties from first principles — what the program SHOULD + guarantee — relying as little as possible on what the code CURRENTLY does. + + {% endif %} + + 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 {% if sort != "greenfield" %}implementation{% else %}design{% endif %}. + + diff --git a/composer/templates/solana/property_system.j2 b/composer/templates/solana/property_system.j2 new file mode 100644 index 00000000..80c659bc --- /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 whole-program *security properties* (invariants a coverage-guided +fuzzer checks after every action in a random instruction sequence). 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 = "program" %}{% 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`. + +{% if sort != "greenfield" %} +## 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. +{% endif %} diff --git a/docs/ecosystem-abstraction.md b/docs/ecosystem-abstraction.md new file mode 100644 index 00000000..9b58b305 --- /dev/null +++ b/docs/ecosystem-abstraction.md @@ -0,0 +1,240 @@ +# 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") + failure_modes_partial: str | None = None # j2 partial of language-level failure modes + +@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, SolidityIdentifier | 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_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" + failure_modes_partial="rust/_failure_modes.j2", # overflow/underflow, panic!/unwrap/expect, ownership +) + +SOLANA: Ecosystem[SolanaApplication, SolanaProgramInstance, SolanaProgramInstance] = 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, # whole-program: a singleton [main] + 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` / + `SolanaInstructionInstance` are the index-wrapper instances (the latter satisfies + `FeatureUnit`). +- **Whole-program units.** `units` returns a singleton `[main]` — the `Unit` type is + `SolanaProgramInstance`, the same as `Main`. All of a program's invariants are inferred over + the whole program in a single extraction rather than fanned out per instruction. +- **Validation** — `_solana_validate` mirrors `_validate_connectivity`'s structure over + `SolanaApplication`: unique program identifiers, unique instruction slugs within a program, + the expected main program present. + +### Prompt composition — the shared Rust fragment + +The `RUST` language facet is chain-independent, so its source conventions and failure-mode +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/_failure_modes.j2" %} {# shared: overflow, panics, unwrap, lossy casts #} +{% include "solana/_failure_modes.j2" %} {# chain-specific: signer/owner/PDA/CPI checks #} +``` + +`rust/_failure_modes.j2` (the language facet) states language-level failure modes — integer +overflow/underflow, `panic!`/`unwrap`/`expect` aborts, lossy conversions, unchecked results — +independent of any chain; `solana/_failure_modes.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 defaults to `EVM`, so Solidity backends pass +nothing; a non-EVM backend passes its ecosystem (e.g. `ecosystem=SOLANA`). + +```python +async def run_pipeline[..., U, Main]( + backend: PipelineBackend[P, FormT, H, A, U, Main], + run: PipelineRun[P, H], + *, ..., + ecosystem: Ecosystem[Any, Any, Any] = EVM, +): + analyzed = await run_component_analysis( + ty=ecosystem.system_model, + prompts=ecosystem.analysis_prompts, + 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 accepts the prompt pair + validation function; the ecosystem + supplies all three. +- **`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`); the "failure modes in this domain" axis is the + ecosystem's prompt. +- **`_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/_failure_modes.j2` | +| fs-exclusion default (EVM) | [composer/spec/util.py](../composer/spec/util.py) | diff --git a/tests/test_null_solana_backend.py b/tests/test_null_solana_backend.py new file mode 100644 index 00000000..d5647e29 --- /dev/null +++ b/tests/test_null_solana_backend.py @@ -0,0 +1,140 @@ +"""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 ( + SolanaApplication, + SolanaProgram, + SolanaProgramInstance, +) +from composer.spec.solana.null_backend import ( + NullArtifact, + NullResult, + NullSolanaArtifactStore, + NullSolanaBackend, + NullSolanaFormalizer, + NullSolanaPrepared, + SOLANA_NULL_GUIDANCE, + SolanaPhase, +) +from composer.spec.types import PropertyFormulation + + +def _program_instance() -> SolanaProgramInstance: + program = SolanaProgram( + name="Vault", + program_identifier="vault", + description="Holds deposits and releases them to the authority.", + instructions=[], + ) + app = SolanaApplication( + application_type="Vault", + description="A single-program token vault.", + components=[program], + ) + return SolanaProgramInstance(0, app) + + +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 = _program_instance() + 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", _program_instance(), [], 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 = _program_instance() + 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", + }