diff --git a/.claude/skills/generate-tape/SKILL.md b/.claude/skills/generate-tape/SKILL.md index ce35ceca..c4802e1e 100644 --- a/.claude/skills/generate-tape/SKILL.md +++ b/.claude/skills/generate-tape/SKILL.md @@ -40,8 +40,8 @@ work for: checkpointed to any thread. Recording captures it in the right lane and position; reconstruction has to recover it separately (e.g. by logging the side-channel messages, or scraping the `verify_spec` tool output). -- **Subagent interleaving** (code_explorer / feedback / cvl_research / - invariant_feedback) — these inherit the parent phase's task_id, so recording +- **Subagent interleaving** (code_explorer / feedback / cvl_research) — these + inherit the parent phase's task_id, so recording lands them in the parent lane in exact call order; reconstruction has to stitch the separate threads back together (e.g. by matching tool calls). @@ -130,7 +130,7 @@ The recorder prints, at exit: ``` [record_tape] wrote N entries across K lane(s) to .../ui_harness_.py -[record_tape] lanes: system-analysis=.., harness=.., invariants=.., ... +[record_tape] lanes: system-analysis=.., harness=.., extract-0=.., ... ``` A `__no_task__` lane in that summary means some LLM call fired outside any @@ -205,8 +205,8 @@ again — it's an iterate-to-green loop: these); remove the trailing/empty message objects in that lane. - `no tape lane for task_id ''` — replay took a phase the recording never hit (usually a flag mismatch, or a non-deterministic branch). Match flags; if a phase - legitimately makes no LLM calls (e.g. `invariant-cvl` on a stateless contract) it - correctly has no lane. + legitimately makes no LLM calls (e.g. `summaries` on a system with no external + contracts) it correctly has no lane. - `LLM call outside any run_task scope` — a `__no_task__` lane entry; move or drop it. ## How it wires together (for debugging) diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 9e06bbca..b5f141ba 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -100,7 +100,7 @@ five steps and never inspects anything backend-specific: 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 + depends on the other, so the prover's expensive AutoSetup/summary work overlaps with per-unit property inference. Property extraction fans out one agent per *unit* — `ecosystem.units(main)` — one per **component** of the main contract/program in both ecosystems — bounded by a semaphore (`--max-concurrent`). @@ -135,7 +135,7 @@ 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 | +| `PreparedSystem` | Holds the located `Main`; builds the `Formalizer` | harness-lifted app + AutoSetup/summaries | 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 @@ -180,7 +180,7 @@ type-safe framework. ## 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: +README's Phase 0–4: - **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 @@ -194,10 +194,6 @@ README's Phase 0–5: 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. @@ -206,8 +202,11 @@ README's Phase 0–5: 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. + because…"). Where a counterexample starts from a state the contract cannot reach, the agent + states that relationship as an invariant, proves it in the same spec, and cites it with + `requireInvariant` — there is no separate invariant phase, so nothing is proven speculatively + ahead of the property that needs it. Output is a `GeneratedCVL` carrying the spec, skipped + properties with reasons, the property→rule mapping, and the final prover run link. ### Outputs and artifacts diff --git a/README.md b/README.md index fc1d4010..82ab2120 100644 --- a/README.md +++ b/README.md @@ -209,38 +209,33 @@ Runs AutoSetup to analyze compilation and classify external contracts (ERC20s, i Generates CVL summaries for ERC20 contracts and external interfaces discovered in Phase 1. Only runs if the system has external contracts that need summarizing. -### Phase 3: Structural Invariants - -Formulates and generates CVL for system-wide structural invariants (e.g. total supply consistency, balance accounting). The resulting `certora/specs/invariants.spec` is made available as a resource that later phases can import and use as preconditions. - -### Phase 4: Per-Component Property Extraction (parallel) +### Phase 3: Per-Component Property Extraction (parallel) For each component identified in Phase 0, an agent analyzes the code and formulates properties to verify. Runs in parallel, bounded by `--max-concurrent`. Produces a list of property formulations per component. -### Phase 5: Per-Component CVL Generation (parallel) +### Phase 4: Per-Component CVL Generation (parallel) -For each component's properties, an agent generates CVL specs and runs the prover to verify them. Failed specs are revised in a feedback loop. Results are written to `certora/specs/autospec_{component}.spec` with accompanying commentary files. Also bounded by `--max-concurrent`. +For each component's properties, an agent generates CVL specs and runs the prover to verify them. Failed specs are revised in a feedback loop. Where a counterexample starts from a state the contract cannot reach, the agent states that relationship as an invariant, proves it in the same spec, and cites it with `requireInvariant`. Results are written to `certora/specs/autospec_{component}.spec` with accompanying commentary files. Also bounded by `--max-concurrent`. ### Output Auto-prove writes its output into the `certora/` directory within the project root. Generated specs live under `certora/specs/` (the prover resolves CVL `import`s relative to that directory), while their run configs go to `certora/confs/`: -- `certora/specs/invariants.spec` — structural invariants (if any were formulated) - `certora/specs/autospec_{component}.spec` (e.g. `autospec_Core_Logic.spec`) — per-component specs - `certora/specs/summaries/*.spec` — AutoSetup-generated and protocol-specific summaries - `certora/confs/*.conf` — per-spec prover configs (each `verify` points at the spec's path relative to the project root) -Each spec (`invariants` and every `autospec_{component}`) is accompanied by metadata under `certora/properties/`, keyed by the spec's stem: +Each `autospec_{component}` spec is accompanied by metadata under `certora/properties/`, keyed by the spec's stem: - `certora/properties/{stem}.properties.json` — the analysis-phase property formulations (title, sort, methods, description); `title` is the cross-reference key - `certora/properties/{stem}.property_rules.json` — the property→rules mapping (`{property title: [rule names]}`) -- `certora/properties/{stem}.commentary.md` — LLM commentary explaining the generated spec (per-component specs only) +- `certora/properties/{stem}.commentary.md` — LLM commentary explaining the generated spec The pipeline returns an `AutoProveResult` with counts of components analyzed, properties generated, and any failures. ## Caching -When `--cache-ns` is provided, auto-prove caches the results of expensive phases (system analysis, property extraction, invariant CVL generation) in the LangGraph store. On subsequent runs with the same `--cache-ns`, cached results are reused if the inputs (project root, contract path, design doc content) haven't changed. +When `--cache-ns` is provided, auto-prove caches the results of expensive phases (system analysis, property extraction, per-component CVL generation) in the LangGraph store. On subsequent runs with the same `--cache-ns`, cached results are reused if the inputs (project root, contract path, design doc content) haven't changed. The cache key is derived from a SHA-256 hash of the project root, design document content, contract path, and contract name. Changing any of these invalidates the cache. diff --git a/budget_integration.md b/budget_integration.md index 5be5e6ca..2df811d6 100644 --- a/budget_integration.md +++ b/budget_integration.md @@ -60,7 +60,7 @@ The five phase names (the keys of `PhaseBudget` in `composer/pipeline/ptypes.py` |---|---| | `system_analysis` | component analysis of the contract system | | `system_preparation` | harness construction | -| `formalization_preparation` | prover pre-formalization fan-out: structural invariants, custom summaries, protocol-specific setup | +| `formalization_preparation` | prover pre-formalization: AutoSetup, then custom summaries and protocol-specific setup | | `property_extraction` | per-component property inference | | `formalization` | per-component CVL / test authoring (usually the dominant cost) | @@ -213,6 +213,10 @@ published)`. never cached, so re-running a curtailed run re-spends on exactly those components. - **Autosetup subprocess spend is invisible.** LLM calls made inside the autosetup subprocess do not flow through the meter and count toward no cap. +- **`formalization_preparation` is attribution-only.** Nothing left under it installs a + budget monitor — AutoSetup is an unmetered subprocess and the custom-summaries agent + installs none — so the cap can neither warn nor hard-stop. Spend still accrues into + the shared pool, where it goes on pressuring formalization. - **Sub-agents accrue to their parent's phase.** Judges, researchers, and other spawned helpers spend from whatever named scope their root agent runs under; there is no separate accounting knob for them. @@ -235,8 +239,9 @@ conversation used. Calibrate on the 1h bound (the authors run with the long cach Sub-agent threads fold into their root thread, matching how budget scopes accrue. `--emit-matrix DIR` writes a ready-made live-test budget matrix (a control budget -plus budgets that trip the formalization cap, the preparation cap, and the shared -pool) with a `manifest.md` of expected outcomes per test. +plus budgets that trip the formalization cap and the shared pool) with a +`manifest.md` of expected outcomes per test. There is no preparation-cap test: nothing +under that phase can trip a monitor. Phase attribution rides on **cost-center telemetry**: every logged thread records the named budget scope it ran under (`ThreadMeta.cost_center`), stamped unconditionally — diff --git a/composer/cli/cache_autoprove.py b/composer/cli/cache_autoprove.py index 349af7a1..653d38d7 100644 --- a/composer/cli/cache_autoprove.py +++ b/composer/cli/cache_autoprove.py @@ -58,11 +58,10 @@ from composer.spec.util import combine_digests from composer.spec.source.keys import ( AP_PROPERTIES_KEY_NAME, CVL_JUDGE_KEY, HARNESS_ANALYSIS_KEY, - HARNESS_GENERATION_KEY, INV_CVL_KEY, LAST_ATTEMPT_KEY, STRUCTURAL_INV_KEY, + HARNESS_GENERATION_KEY, LAST_ATTEMPT_KEY, SUMMARY_KEY, SYSTEM_SETUP_KEY, config_key, ) from composer.spec.source.summarizer import _SummaryCache -from composer.spec.source.struct_invariant import Invariants from composer.spec.prop_inference import ( _BugAnalysisCache, _AgentResult, _AgentRoundWithHistory, ) @@ -94,7 +93,6 @@ class PluginCacheRaw: | AgentSystemDescription | HarnessResult | _SummaryCache - | Invariants | GeneratedCVL | _LastAttemptCache | _BugAnalysisCache @@ -304,11 +302,6 @@ async def build_tree_inner( if config_val is not None: yield await leaf(root_ctx, SUMMARY_KEY(config_val), "summary", _SummaryCache) - yield await leaf(root_ctx, STRUCTURAL_INV_KEY, "structural-inv", Invariants) - async with node_for(root_ctx, INV_CVL_KEY, "invariant-cvl", GeneratedCVL) as inv_cvl_ctx: - async for n in _build_cvl_gen_nodes(inv_cvl_ctx.abstract(CVLGeneration)): - yield n - # Properties — per-component plugin pre-inference + bug analysis + CVL generation if sa_leaf.value is None: with section("properties (no source analysis)"): @@ -435,11 +428,6 @@ def format_value(val: AutoProveCachedValue) -> list[str]: case _SummaryCache(content=content): lines.extend(content.splitlines()) - case Invariants(inv=invs): - lines.append(f"Invariants ({len(invs)}):") - for inv in invs: - lines.append(f" {inv.description}") - case GeneratedCVL(commentary=commentary, cvl=cvl, skipped=skipped): lines.append(f"Commentary: {commentary}") if skipped: diff --git a/composer/pipeline/core.py b/composer/pipeline/core.py index 0a5f3461..e96bab42 100644 --- a/composer/pipeline/core.py +++ b/composer/pipeline/core.py @@ -22,9 +22,9 @@ The driver owns the genuinely-shared steps: system analysis, per-component property extraction, the result-type-keyed cache, and (since the report is backend-agnostic) building + persisting the -property-keyed report. Everything backend-specific — the harnessed lift, autosetup/summaries/ -invariant fan-out, the formalizer itself, per-unit verdicts — is contributed through the three -phase objects, and never inspected by the driver. +property-keyed report. Everything backend-specific — the harnessed lift, the autosetup/summaries +pre-work, the formalizer itself, per-unit verdicts — is contributed through the three phase +objects, and never inspected by the driver. """ import asyncio @@ -161,7 +161,7 @@ async def __call__[TP: PipelinePlugin[Any], **P, **I, R]( class Formalizer[FormT: BackendResult, U: FeatureUnit](ABC): """Immutable, fully constructed by whatever produced it — ``prepare_formalization``, or :meth:`StagedFormalizer.begin` for a backend with a shared artifact. Carries the prover's - config/resources/prover_tool/invariant-results (or nothing, for foundry) as constructor + config/resources/prover_tool (or nothing, for foundry) as constructor 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``, @@ -191,11 +191,6 @@ async def formalize( graph's state type and staged-state reader).""" ... - def extra_report_inputs(self) -> list[ReportComponentInput[FormT]]: - """Synthetic report inputs beyond the per-component outcomes — the prover folds in its - 'Structural Invariants' here. Default: none.""" - return [] - async def source_edits( self, outcomes: list[ComponentOutcome[FormT, U]], run: PipelineRun ) -> list[SourceEditRecord]: @@ -234,8 +229,8 @@ class StagedFormalizer[FormT: BackendResult, U: FeatureUnit](ABC): then told to work within — harmless at one unit, silently wrong at several. ``begin`` sits between the two, where extraction is done and no unit has been formalized. - Some backends need none of this and return a ``Formalizer`` directly; the prover's shared peer - (``invariants.spec``) is staged in ``prepare_formalization``.""" + Some backends need none of this and return a ``Formalizer`` directly; the prover is one of + them — its units share no authored artifact, only AutoSetup's config and summaries.""" @abstractmethod async def begin( @@ -721,9 +716,8 @@ async def _run(batch: _Batch[U]) -> ComponentOutcome[FormT, U]: await formalizer.finalize(outcomes, run) - # 6. Report (shared, backend-agnostic). The driver assembles the per-component inputs; backends - # contribute only synthetic extras (prover: structural invariants). Best-effort: a failure here - # never fails the run. + # 6. Report (shared, backend-agnostic). The driver assembles the per-component inputs. + # Best-effort: a failure here never fails the run. inputs = [ ReportComponentInput( name=o.feat.display_name, @@ -731,7 +725,7 @@ async def _run(batch: _Batch[U]) -> ComponentOutcome[FormT, U]: formalized=o.result if isinstance(o.result, (Delivered, Curtailed)) else None, ) for o in outcomes - ] + formalizer.extra_report_inputs() + ] artifact_records = [ VerificationArtifactRecord( component=o.feat.display_name, diff --git a/composer/pipeline/keys.py b/composer/pipeline/keys.py index 1f9a10c9..923f7fe7 100644 --- a/composer/pipeline/keys.py +++ b/composer/pipeline/keys.py @@ -23,8 +23,8 @@ The extraction-layer families (bug analysis, agent rounds) are declared in ``composer.spec.prop_inference`` beside their cache models and re-exported here. The prover backend's sub-chain (config / harness / -autosetup / summaries / invariants / CVL generation) has its own -registry: ``composer.spec.source.keys``. +autosetup / summaries / CVL generation) has its own registry: +``composer.spec.source.keys``. """ from typing import Any diff --git a/composer/pipeline/run_mode.py b/composer/pipeline/run_mode.py index 923f2e7b..2b8a393e 100644 --- a/composer/pipeline/run_mode.py +++ b/composer/pipeline/run_mode.py @@ -4,8 +4,8 @@ the shape the pipeline has always had. ``prioritized`` ranks the whole candidate set once, keeps the highest-contribution property plus the properties needed to support it, and spends the formalization phase on that alone. The rest of the run (analysis, -harness, autosetup, structural invariants, property inference) is identical either -way; only the batches reaching formalization differ. +harness, autosetup, property inference) is identical either way; only the batches +reaching formalization differ. The mode is settable from the environment as well as the command line so the cloud can turn it on by adding one variable to the Batch job, without a code change on diff --git a/composer/scripts/budget_math.py b/composer/scripts/budget_math.py index 26a6bf1c..962cde00 100644 --- a/composer/scripts/budget_math.py +++ b/composer/scripts/budget_math.py @@ -23,7 +23,6 @@ t1_control.json ample everything: must behave like an unbudgeted run t2_formalization_curtail.json trips the component author mid-batch - t3_preparation_curtail.json trips the invariant author; run degrades gracefully t4_pool_pressure.json trips the shared pool partway through the run (T5, the caching interplay test, reuses t2 across two runs — see the manifest) @@ -216,8 +215,7 @@ def build_matrix( phase_spend = {p: sum(r.cost() for r in roots if r.phase == p) for p in (*PHASES, UNATTRIBUTED)} # The author proxy: the priciest formalization root, falling back to the priciest - # root overall (e.g. a cache-warm source run where only invariant work ran live — - # same agent shape, stated as a proxy in the manifest). + # root overall (e.g. a fully cache-warm source run), stated as a proxy in the manifest. formalization_roots = [r for r in roots if r.phase == "formalization"] author = max(formalization_roots or roots, key=lambda r: r.cost()) author_is_proxy = not formalization_roots @@ -231,8 +229,6 @@ def build_matrix( ample_caps = {p: ample for p in PHASES} t2_cap = _cap(cap_fraction * author_cost) - prep_spend = phase_spend["formalization_preparation"] - t3_cap = _cap(theta * prep_spend) if prep_spend > 0 else None t4_total = _cap(theta * run_total) files: dict[str, dict] = { @@ -241,10 +237,6 @@ def build_matrix( "total": ample, "caps": {**ample_caps, "formalization": t2_cap}, }, } - if t3_cap is not None: - files["t3_preparation_curtail.json"] = { - "total": ample, "caps": {**ample_caps, "formalization_preparation": t3_cap}, - } files["t4_pool_pressure.json"] = {"total": t4_total, "caps": dict(ample_caps)} def headroom_note(cap: float) -> str: @@ -278,8 +270,8 @@ def headroom_note(cap: float) -> str: "", f"Author baseline: `{author.description}` — ${author_cost:.4f} over " f"{len(author.calls)} calls (max ${max_call:.4f}, late-turn mean ${late_mean:.4f})." - + (" **Proxy**: no formalization-phase thread ran live in the source run (cache-warm);" - " the invariant author is the same agent shape." if author_is_proxy else ""), + + (" **Proxy**: no formalization-phase thread ran live in the source run (cache-warm)." + if author_is_proxy else ""), ] if unobserved: lines += [ @@ -315,16 +307,6 @@ def headroom_note(cap: float) -> str: f"report appendix, exit code reflects `all_failed` for single-component scenarios. " f"{headroom_note(t2_cap)}.", ] - if t3_cap is not None: - lines += [ - "", - f"### T3 — invariant curtailment (`t3_preparation_curtail.json`: " - f"formalization_preparation cap ${t3_cap})", - f"Warn fires at ≥ ${theta * t3_cap:.2f} into preparation spend (observed " - f"${prep_spend:.2f}). Expected: `invariants.spec.unverified`, NO invariant import " - "in component specs, 'Structural Invariants' appendix entry — and the run " - f"*continues* into component formalization. {headroom_note(t3_cap)}.", - ] lines += [ "", f"### T4 — pool pressure (`t4_pool_pressure.json`: total ${t4_total}, caps ample)", @@ -356,8 +338,9 @@ def headroom_note(cap: float) -> str: "line above against `composer/llm/pricing.py` before running.", "- Calibration uses the 1h cache-write bound (authors run the long cache); the 5m " "bound runs ~20% cheaper.", - "- AutoSetup's subprocess LLM calls never pass through `CostAccumulator`: " - "`formalization_preparation` meters only in-process work (invariants, summaries).", + "- AutoSetup's subprocess LLM calls never pass through `CostAccumulator`, and the " + "custom-summaries agent installs no budget monitor, so `formalization_preparation` " + "is attribution-only: it accrues into the pool but can neither warn nor stop.", "", f"Regenerate: `uv run scripts/budget_math.py {run.run_id} --emit-matrix `", "", diff --git a/composer/spec/context.py b/composer/spec/context.py index 0ba4295e..b9552177 100644 --- a/composer/spec/context.py +++ b/composer/spec/context.py @@ -103,12 +103,6 @@ def __str__(self) -> str: # Phantom marker types for the cache hierarchy. -class InvJudge: - """Invariant formulation feedback judge step.""" - -class InvFormal: - """Grouping step for individual invariant formalization.""" - class Properties: """Grouping step for property-level analysis.""" @@ -140,7 +134,7 @@ class EditorJudge: type Marker = ( - InvJudge | InvFormal | Properties | ComponentGroup + Properties | ComponentGroup | CVLJudge | FoundryJudge | Abstraction | Contract | EditorAgent | EditorJudge ) diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index 5dba554b..dbd030dc 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -128,10 +128,14 @@ class CVLGenerationExtra(AuthoringExtra): property_rules: list[PropertyRuleMapping] -#: How the CVL author words its publish-time mapping. The prover reports no rule-name ground truth -#: (unlike forge), so ``validate_property_rules`` passes no ``ran`` set and the mapping is checked -#: for coverage only. -_CVL_MAPPING = MappingVocab(check_noun="rule", field_name="property_rules") +#: How the CVL author words its publish-time mapping. The source author supplies a ``ran`` set +#: from the typechecker's declaration list (see ``declared_rules_at``), so its mapping is checked +#: in both directions; a caller with no prover run behind it passes none and gets the +#: coverage-only check. +_CVL_MAPPING = MappingVocab( + check_noun="rule", field_name="property_rules", + ran_source="the prover's typecheck of your spec", +) def validate_property_rules( @@ -142,10 +146,13 @@ def validate_property_rules( ) -> str | None: """Validate the property->rules mapping declared at completion time. ``titles`` is the batch's full set of property titles; returns None if valid, else one message enumerating all problems.""" + # ``None`` means the caller has no ground truth (no prover run covered this state); an + # EMPTY set means the prover typechecked the spec and found nothing declared. Those are + # different answers, and collapsing them would let a publish claiming a nonexistent rule + # through on the second one. return validate_check_mapping( - [(m.property_title, m.rules) for m in property_rules], skipped, titles, _CVL_MAPPING, ran=[ - CheckName(it) for it in known_rules - ] if known_rules else None + [(m.property_title, m.rules) for m in property_rules], skipped, titles, _CVL_MAPPING, + ran=None if known_rules is None else [CheckName(it) for it in known_rules], ) diff --git a/composer/spec/gen_types.py b/composer/spec/gen_types.py index 3c5d3875..1a47ab15 100644 --- a/composer/spec/gen_types.py +++ b/composer/spec/gen_types.py @@ -10,7 +10,7 @@ # Canonical certora/ layout # # Every persisted path variable in the spec pipeline is stored **relative to the -# project root** (e.g. ``certora/specs/invariants.spec``). Conversions to other +# project root** (e.g. ``certora/specs/autospec_vault.spec``). Conversions to other # bases happen only at the edges: the ``ArtifactStore`` conf writer emits the verify # entry verbatim (the prover reads it relative to the project root), and CVL ``import`` # statements are derived with :func:`import_statement_for` (the prover reads @@ -93,7 +93,7 @@ def import_statement_for(resource_path: Path, importer_dir: Path) -> str: # --------------------------------------------------------------------------- class CVLResource(BaseModel): - path: Path = Field(description="path to the resource file, relative to the project root (e.g. `certora/specs/invariants.spec`)") + path: Path = Field(description="path to the resource file, relative to the project root (e.g. `certora/specs/summaries/Vault.spec`)") required: bool = Field(description="whether this resource *must* be used in the verification process") description: str = Field(description="A description of this resource") sort: Literal["import"] diff --git a/composer/spec/guidance.py b/composer/spec/guidance.py index 77b5193e..6f5ee939 100644 --- a/composer/spec/guidance.py +++ b/composer/spec/guidance.py @@ -22,3 +22,14 @@ class UnresolvedCallGuidance(WithImplementation[str]): @override def run(self) -> str: return load_jinja_template("unresolved_call_guidance.j2") + +@tool_display("Getting structural invariant guidance", None) +class StructuralInvariantGuidance(WithImplementation[str]): + """ +Invoke this tool to receive guidance on choosing which relationship among a contract's state +fields to state and prove as an invariant, when a counterexample starts from a state the +contract could not reach. + """ + @override + def run(self) -> str: + return load_jinja_template("structural_invariant_guidance.j2") diff --git a/composer/spec/source/artifacts.py b/composer/spec/source/artifacts.py index 6ce13ce2..76760a49 100644 --- a/composer/spec/source/artifacts.py +++ b/composer/spec/source/artifacts.py @@ -3,8 +3,8 @@ A subclass of the shared :class:`composer.spec.artifacts.ArtifactStore`. Adds the CVL-specific bundle (``specs/``, ``confs/``) and the autoprove report on top of the base's shared property / commentary / token-usage primitives. The stem / filename / -run-key conventions for a spec (``autospec_{slug}`` vs ``invariants``) are captured by -the :data:`SpecIdentity` sum type, not interpolated at call sites. +run-key conventions for a spec (``autospec_{slug}``) are captured by +:class:`ComponentSpec`, not interpolated at call sites. """ import json @@ -48,31 +48,7 @@ def artifact_file(self) -> str: return self.spec_filename -@dataclass(frozen=True) -class InvariantSpec: - """The single structural-invariants spec.""" - - @property - def stem(self) -> str: - return "invariants" - - @property - def spec_filename(self) -> str: - return f"{self.stem}.spec" - - @property - def run_key(self) -> str: - return "invariants" - - @property - def artifact_file(self) -> str: - return self.spec_filename - - -type SpecIdentity = ComponentSpec | InvariantSpec - - -class ProverArtifactStore(ArtifactStore[SpecIdentity, GeneratedCVL]): +class ProverArtifactStore(ArtifactStore[ComponentSpec, GeneratedCVL]): """Persists the autoprove pipeline's outputs under ``certora/`` (plus ``.certora_internal/autoProve/`` diagnostics).""" @@ -91,13 +67,13 @@ def _artifact_dir(self) -> Path: return under_project(self._project_root, CERTORA_DIR) @override - def write_artifact(self, i: ComponentSpec | InvariantSpec, artifact: GeneratedCVL) -> Path: + def write_artifact(self, i: ComponentSpec, artifact: GeneratedCVL) -> Path: written_spec = super().write_artifact(i, artifact) self._write_conf(i, artifact.config, written_spec) return written_spec def _write_conf( - self, spec: SpecIdentity, base_config: dict | None, spec_path: Path, + self, spec: ComponentSpec, base_config: dict | None, spec_path: Path, ) -> None: """The prover conf for the run: the generation's final ``state["config"]`` plus the fixed run overlay (shared with the live ``verify_spec`` run). No-op if no diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index 1af8fe72..3810e453 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -18,8 +18,9 @@ from graphcore.tools.vfs import VFSAccessor, VFSState from composer.authoring.judge import PropertyFeedbackProtocol -from composer.authoring.state import SkippedProperty, check_completion +from composer.authoring.state import SkippedProperty, check_completion, spec_digest from composer.authoring.tools import gated_give_up_tool, give_up_tool +from composer.spec.guidance import StructuralInvariantGuidance from composer.spec.cvl_generation import ( static_tools, property_tools, skip_tools, CVLGenerationExtra, FEEDBACK_VALIDATION_KEY, validate_property_rules, CVL_JUDGE_KEY, run_cvl_generator, @@ -36,7 +37,7 @@ from composer.spec.system_model import ContractComponentInstance, SolidityIdentifier, component_context from composer.spec.source.prover import ( OVERLAY_OWNED_KEYS, ProverStateExtra, DELETE_SKIP, VALIDATION_KEY as PROVER_VALIDATION_KEY, - materializing_project, + declared_rules_at, materializing_project, ) from langgraph.graph import MessagesState from pathlib import Path @@ -101,6 +102,9 @@ class SourceCVLGenerationState(SourceCVLGenerationExtra, MessagesState): class ExpectRuleFailure(WithAsyncImplementation[Command], WithInjectedId): """ Mark a rule name as expected to fail. + + Never mark an invariant that another rule or `preserved` block cites with `requireInvariant`: + that citation is sound only because the invariant is proved in this same spec. """ rule_name: str = Field(description="The name of the rule") reason: str = Field(description="The reason the rule is expected to fail") @@ -156,10 +160,21 @@ class PublishResultTool( @override async def run(self) -> Command | str: - if (err := check_completion(self.state, self.state["version_history"])) is not None: + st = self.state + if (err := check_completion(st, st["version_history"])) is not None: return err + spec = st["curr_spec"] + assert spec is not None, "check_completion admits no spec-less state" + # What the typechecker actually found in the published spec, so the mapping is checked + # in both directions: a supporting invariant the author proved but never tied back to a + # property would otherwise be dropped from the report as an orphan. + declared = declared_rules_at( + st["prover_history"], spec_digest(spec, st["skipped"], st["version_history"]) + ) with self.tool_deps() as titles: - if (err := validate_property_rules(self.property_rules, self.state["skipped"], titles)) is not None: + if (err := validate_property_rules( + self.property_rules, st["skipped"], titles, declared + )) is not None: return err return tool_state_update( self.tool_call_id, @@ -214,7 +229,7 @@ class ResourceView(TypedDict): @component_context class PropertyGenParams(TypedDict): sort: Literal["existing"] - context: ContractComponentInstance | None + context: ContractComponentInstance resources: list[ResourceView] properties: list[PropertyFormulation] contract_name: str @@ -224,17 +239,12 @@ class PropertyGenParams(TypedDict): focused: bool class PropertyGenerationConfig(SummaryConfig[SourceCVLGenerationState]): - def __init__(self, source_editing: bool = False): - super().__init__() - self._source_editing = source_editing - @override def get_summarization_prompt(self, state: SourceCVLGenerationState) -> str: edit_item = ( "\n7. The source edits you have applied (their edit ids and what each was for), " "any edit ids the editor produced that you chose NOT to apply, and any plans " "you had to request further edits" - if self._source_editing else "" ) return f""" You are approaching the context limit for your task. After this point, your context will be cleared @@ -263,7 +273,6 @@ def get_resume_prompt(self, state: SourceCVLGenerationState, summary: str) -> st edit_note = ( "\nAny source edits you applied remain in effect on your working copy; " f"the `{EDIT_HISTORY_LOG}` tool shows each applied edit and its diff.\n" - if self._source_editing else "" ) return f""" You are resuming this task already in progress. The current version of your spec (if any) is available via the `get_cvl` tool. @@ -563,9 +572,7 @@ def generate_edit_management_tools( class SourceEditing: """The editing-enabled generation phase's kit: the live tool suite (vfs-aware reads + versioned explorer + live doc ref, plus the write tools - the editor sub-agent uses) and the edit snapshot store. Phases whose output - must hold against the unedited source — structural invariants — run - without one.""" + the editor sub-agent uses) and the edit snapshot store.""" live: LiveEditTools store: EditStore @@ -576,8 +583,7 @@ class EditingTools: staged :class:`CVLAuthorState` proposes edits into the editing kit's store and materializes against its working copy, so a binder without an editing kit is unusable. Fusing them makes "tools provided ⟺ editing enabled" a - fact of the type rather than an assert (the structural-invariant phase - passes None: neither).""" + fact of the type rather than an assert.""" editing: SourceEditing tool_provider: ToolBinder[ContractComponentInstance] @@ -658,10 +664,7 @@ def _version_history(self) -> Sequence[str]: _PropertyGenTemplate = TypedTemplate[PropertyGenParams]("property_generation_prompt.j2") -class PropertyGenSystemParams(TypedDict): - source_editing: bool - -_PropertyGenSysTemplate = TypedTemplate[PropertyGenSystemParams]("property_generation_system_prompt.j2") +_PROPERTY_GEN_SYS_PROMPT = "property_generation_system_prompt.j2" #: The prover's tool extension: contributions come from plugins deriving #: ``CertoraProverTools``, dispatched via their ``certora_prover_tools`` hook. @@ -753,7 +756,7 @@ async def batch_cvl_generation( ctx: WorkflowContext[CVLGeneration], init_config: dict, props: list[PropertyFormulation], - component: ContractComponentInstance | None, + component: ContractComponentInstance, resources: list[CVLResource], prover_tool: ProverTool, env: ServiceHost, @@ -761,7 +764,7 @@ async def batch_cvl_generation( source: SourceCode, spec_dir: Path, spec_stem: str, - editing_tools: EditingTools | None, + editing_tools: EditingTools, focus: FocusPolicy | None = None, ) -> BatchGeneratedCVLResult: # *spec_dir* (project-root-relative) is where the caller will persist the spec @@ -769,7 +772,7 @@ async def batch_cvl_generation( # directory, so resource imports are expressed relative to *spec_dir*. # *spec_stem* is the basename it is persisted under; the prover materializes its # transient spec/conf under the same stem so on-disk names match the dump. - editing = editing_tools.editing if editing_tools is not None else None + editing = editing_tools.editing resource_views: list[ResourceView] = [ { "description": r.description, @@ -788,64 +791,61 @@ async def batch_cvl_generation( }) sys_prompt : list[RawPromptInput | type[CacheMarker]] = [ - _PropertyGenSysTemplate.bind({"source_editing": editing is not None}).render_to + lambda load: load(_PROPERTY_GEN_SYS_PROMPT) ] added_tools : list[BaseTool] = [] - if editing_tools is not None: - task_host = TaskHost() - kit = editing_tools.editing - # The same run-root strategy verify_spec uses (see ProjectDirectory): an - # empty working copy is read in-situ, a non-empty one against a temporary - # materialization whose lifetime is the contributed tool's invocation. - project_directory = materializing_project(source.project_root, kit.live.mat) - - @asynccontextmanager - async def yield_state( - plugin_id: str, - st: SourceCVLGenerationState - ) -> AsyncIterator[CVLAuthorState]: - class _PluginStore: - async def propose( - self, vfs: dict[str, str], *, executive_summary: str, why_sound: str - ) -> str: - # Snapshot completion (the EditProposer contract): the - # proposer's overlay is relative to the working copy this - # read staged, but ApplyEditTool snapshots are wholesale — - # so fold the author's own overlay back in, or applying - # the proposal would silently revert prior edits. - return await kit.store.commit( - {**(st.get("vfs") or {}), **vfs}, - executive_summary=executive_summary, - why_sound=why_sound, - attribution=PluginEditor(plugin_id) - ) - async with project_directory(st.get("vfs") or {}) as run_root: - yield CVLAuthorState( - working_dir=pathlib.Path(run_root), - curr_spec=st["curr_spec"], - prover_runner=WrappedProverRunner( - st["config"], - prover_tool.options, - source.contract_name - ).run, - host=task_host, - edit_store=_PluginStore() + task_host = TaskHost() + kit = editing_tools.editing + # The same run-root strategy verify_spec uses (see ProjectDirectory): an + # empty working copy is read in-situ, a non-empty one against a temporary + # materialization whose lifetime is the contributed tool's invocation. + project_directory = materializing_project(source.project_root, kit.live.mat) + + @asynccontextmanager + async def yield_state( + plugin_id: str, + st: SourceCVLGenerationState + ) -> AsyncIterator[CVLAuthorState]: + class _PluginStore: + async def propose( + self, vfs: dict[str, str], *, executive_summary: str, why_sound: str + ) -> str: + # Snapshot completion (the EditProposer contract): the + # proposer's overlay is relative to the working copy this + # read staged, but ApplyEditTool snapshots are wholesale — + # so fold the author's own overlay back in, or applying + # the proposal would silently revert prior edits. + return await kit.store.commit( + {**(st.get("vfs") or {}), **vfs}, + executive_summary=executive_summary, + why_sound=why_sound, + attribution=PluginEditor(plugin_id) ) + async with project_directory(st.get("vfs") or {}) as run_root: + yield CVLAuthorState( + working_dir=pathlib.Path(run_root), + curr_spec=st["curr_spec"], + prover_runner=WrappedProverRunner( + st["config"], + prover_tool.options, + source.contract_name + ).run, + host=task_host, + edit_store=_PluginStore() + ) - tools = await editing_tools.tool_provider( - _PROVER_TOOLS, yield_state, SourceCVLGenerationState - ) - if tools: - # The retrieval surface for whatever the contributed tools launch; - # dead prompt weight when no plugin contributed, so gated on a - # non-empty contribution. - added_tools.extend([ - TaskListTool.bind(task_host).as_tool(TASK_LIST), - RetrieveTask.bind(task_host).as_tool(RETRIEVE_TASK), - ]) - else: - tools = [] + tools = await editing_tools.tool_provider( + _PROVER_TOOLS, yield_state, SourceCVLGenerationState + ) + if tools: + # The retrieval surface for whatever the contributed tools launch; + # dead prompt weight when no plugin contributed, so gated on a + # non-empty contribution. + added_tools.extend([ + TaskListTool.bind(task_host).as_tool(TASK_LIST), + RetrieveTask.bind(task_host).as_tool(RETRIEVE_TASK), + ]) for inj in tools: added_tools.extend(inj.tools) @@ -859,22 +859,16 @@ async def propose( judge_prompt = FeedbackTemplate.bind({ "sort": "existing", "context": component, - "source_editing": editing is not None, + "source_editing": True, }) protected = focus.protected if focus is not None else () - if editing is None: - feedback_suite = property_tools( - property_feedback_judge(judge_ctx, env, judge_prompt, props), - protected=protected, - ) - else: - judge_impl = source_feedback_judge( - judge_ctx, _LiveJudgeHost(env, editing), judge_prompt, props - ) - feedback_suite = [ - EditorAwareFeedbackTool.bind(judge_impl).as_tool("feedback_tool"), - *skip_tools(titles, protected=protected), - ] + judge_impl = source_feedback_judge( + judge_ctx, _LiveJudgeHost(env, editing), judge_prompt, props + ) + feedback_suite = [ + EditorAwareFeedbackTool.bind(judge_impl).as_tool("feedback_tool"), + *skip_tools(titles, protected=protected), + ] # use "cache=long" to account for very long prover runs. # on anthropic (the only backend we support) a long cache is 1hr @@ -883,18 +877,19 @@ async def propose( b = env.builder_heavy(cache_level=CacheLevel.LONG).with_tools( env.rag_tools ) - if editing is not None: - b = b.with_tools( - editing.live.read_tools - ).with_tools( - [editing.live.explorer, editing.live.doc_tool] - ).with_tools( - generate_edit_management_tools(ctx, env, editing.store, editing.live) - ) - else: - b = b.with_tools(env.source_tools) + b = b.with_tools( + editing.live.read_tools + ).with_tools( + [editing.live.explorer, editing.live.doc_tool] + ).with_tools( + generate_edit_management_tools(ctx, env, editing.store, editing.live) + ) task_graph = b.with_tools( static_tools() + ).with_tools( + # Prover-only: the natspec author shares ``static_tools()`` but has no + # prover and so no counterexample to remediate. + [StructuralInvariantGuidance.as_tool("structural_invariant_guidance")] ).with_tools( feedback_suite ).with_tools( @@ -924,7 +919,7 @@ async def propose( ).with_tools( added_tools ).with_summary_config( - PropertyGenerationConfig(source_editing=editing is not None) + PropertyGenerationConfig() ).compile_async() # Crash recovery for the working copy, sibling to cvl_generation's draft @@ -935,22 +930,21 @@ async def propose( restored_vfs: dict[str, str] = {} restored_config: dict = init_config resume_note: list[str | dict] = [] - if editing is not None: - prior = await ctx.child(LAST_ATTEMPT_EDITS_KEY).cache_get(_LastAttemptEdits) - if prior is not None: - if prior.config is not None: - restored_config = prior.config - if prior.version_history: - tail = await editing.store.read(prior.version_history[-1]) - assert tail is not None, ( - f"recovered edit {prior.version_history[-1]} absent from the edit store" - ) - restored_history = prior.version_history - restored_vfs = tail.vfs - resume_note = [ - "Source edits applied during your previous attempt at this task have " - f"been restored to your working copy; use `{EDIT_HISTORY_LOG}` to review them." - ] + prior = await ctx.child(LAST_ATTEMPT_EDITS_KEY).cache_get(_LastAttemptEdits) + if prior is not None: + if prior.config is not None: + restored_config = prior.config + if prior.version_history: + tail = await editing.store.read(prior.version_history[-1]) + assert tail is not None, ( + f"recovered edit {prior.version_history[-1]} absent from the edit store" + ) + restored_history = prior.version_history + restored_vfs = tail.vfs + resume_note = [ + "Source edits applied during your previous attempt at this task have " + f"been restored to your working copy; use `{EDIT_HISTORY_LOG}` to review them." + ] try: res_state = await run_cvl_generator( @@ -978,17 +972,16 @@ async def propose( except BudgetExceeded as e: return Curtailed(None, detail=str(e)) finally: - if editing is not None: - last_state = ( - await task_graph.aget_state({"configurable": {"thread_id": ctx.thread_id}}) - ).values - hist = last_state.get("version_history") - if hist is not None: - await ctx.child(LAST_ATTEMPT_EDITS_KEY).cache_put( - _LastAttemptEdits( - version_history=list(hist), config=last_state.get("config"), - ) + last_state = ( + await task_graph.aget_state({"configurable": {"thread_id": ctx.thread_id}}) + ).values + hist = last_state.get("version_history") + if hist is not None: + await ctx.child(LAST_ATTEMPT_EDITS_KEY).cache_put( + _LastAttemptEdits( + version_history=list(hist), config=last_state.get("config"), ) + ) assert "result" in res_state assert res_state["failed"] is not None @@ -1001,15 +994,14 @@ async def propose( d = res_state["curr_spec"] assert d is not None applied_edits: list[AppliedEdit] = [] - if editing is not None: - for edit_id in res_state["version_history"]: - rec = await editing.store.read(edit_id) - assert rec is not None, f"edit {edit_id} in history but absent from the edit store" - applied_edits.append(AppliedEdit( - edit_id=edit_id, - executive_summary=rec.executive_summary, - why_sound=rec.why_sound, - )) + for edit_id in res_state["version_history"]: + rec = await editing.store.read(edit_id) + assert rec is not None, f"edit {edit_id} in history but absent from the edit store" + applied_edits.append(AppliedEdit( + edit_id=edit_id, + executive_summary=rec.executive_summary, + why_sound=rec.why_sound, + )) # Persist the base prover config and last run link from the final state so a later cache # hit (which skips the prover) can still reconstruct certora/confs and retain the link. diff --git a/composer/spec/source/keys.py b/composer/spec/source/keys.py index b1c5acd5..3ac5f44d 100644 --- a/composer/spec/source/keys.py +++ b/composer/spec/source/keys.py @@ -10,32 +10,23 @@ │ │ └── {instructions digest} HARNESS_GENERATION_KEY → HarnessResult │ └── autosetup-{app+opts digest} AUTOSETUP_KEY → SetupSuccess ├── summary-{config digest} SUMMARY_KEY → _SummaryCache - ├── structural-inv STRUCTURAL_INV_KEY → Invariants - │ └── judge INV_JUDGE_KEY → (judge memory) - ├── invariant-cvl INV_CVL_KEY → GeneratedCVL - │ ├── judge CVL_JUDGE_KEY → (judge memory) - │ └── last_attempt LAST_ATTEMPT_KEY → _LastAttemptCache └── ap-properties PROPERTIES_KEY(AP_PROPERTIES_KEY_NAME) └── … driver chain … └── {props digest} FORMALIZATION_KEY → GeneratedCVL ├── judge CVL_JUDGE_KEY └── last_attempt LAST_ATTEMPT_KEY -Families and constants are declared beside their cache models (harness, -summarizer, struct_invariant, cvl_generation) and gathered here; -consumers (the backend pipeline, ``cache-autoprove``) import from this -registry rather than spelunking the producer modules. +Every family and constant is declared beside its cache model (harness, +summarizer, cvl_generation); this module declares none of its own and only +gathers them, so consumers (the backend pipeline, ``cache-autoprove``) import +from one registry rather than spelunking the producer modules. """ -from composer.spec.context import CacheKey -from composer.spec.cvl_generation import ( - CVL_JUDGE_KEY, LAST_ATTEMPT_KEY, GeneratedCVL, -) +from composer.spec.cvl_generation import CVL_JUDGE_KEY, LAST_ATTEMPT_KEY from composer.spec.source.harness import ( AUTOSETUP_KEY, HARNESS_ANALYSIS_KEY, HARNESS_GENERATION_KEY, SYSTEM_SETUP_KEY, config_key, ) -from composer.spec.source.struct_invariant import INV_JUDGE_KEY, STRUCTURAL_INV_KEY from composer.spec.source.summarizer import SUMMARY_KEY __all__ = [ @@ -44,10 +35,7 @@ "CVL_JUDGE_KEY", "HARNESS_ANALYSIS_KEY", "HARNESS_GENERATION_KEY", - "INV_CVL_KEY", - "INV_JUDGE_KEY", "LAST_ATTEMPT_KEY", - "STRUCTURAL_INV_KEY", "SUMMARY_KEY", "SYSTEM_SETUP_KEY", "config_key", @@ -55,7 +43,3 @@ #: The prover backend's ``SystemAnalysisSpec.properties_key``. AP_PROPERTIES_KEY_NAME = "ap-properties" - -#: CVL generation for the structural invariants (the per-component peer is -#: reached via ``FORMALIZATION_KEY``). -INV_CVL_KEY = CacheKey[None, GeneratedCVL]("invariant-cvl") diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index 55a63897..b52ac0c6 100644 --- a/composer/spec/source/pipeline.py +++ b/composer/spec/source/pipeline.py @@ -7,12 +7,9 @@ * ``ProverBackend.prepare_system`` — harness creation, then the lift of the analyzed ``SourceApplication`` into a ``HarnessedApplication`` and the prover tool. Returns a ``ProverPrepared``. -* ``ProverPrepared.prepare_formalization`` — the AutoSetup ∥ custom-summaries ∥ - structural-invariant fan-out, then the staged structural-invariant CVL whose - ``invariants.spec`` is folded into the resources every per-component spec then - imports. Returns a ``ProverRunner``. -* ``ProverRunner`` — per-batch CVL generation (``batch_cvl_generation``), the - report inputs (per component + the synthetic ``Structural Invariants``), and +* ``ProverPrepared.prepare_formalization`` — AutoSetup, then the custom summaries + that build on its config. Returns a ``ProverRunner``. +* ``ProverRunner`` — per-batch CVL generation (``batch_cvl_generation``) and prover-run-backed verdicts (``make_prover_fetcher``). ``run_autoprove_pipeline`` is now a thin wrapper that builds the backend + run @@ -28,7 +25,7 @@ from composer.io.multi_job import TaskInfo from composer.spec.context import WorkflowContext, CVLGeneration -from composer.spec.types import PropertyFormulation, PropertyTitle +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, ContractInstance, SourceApplication, HarnessedApplication, @@ -42,27 +39,24 @@ lift_harnessed, ) from composer.spec.source.summarizer import setup_summaries -from composer.spec.source.struct_invariant import get_invariant_formulation -from composer.spec.source.autosetup import SetupSuccess from composer.spec.source.prover import get_prover_tool, materializing_project from composer.spec.source.plugin import CertoraProverTools from composer.spec.source.author import ( batch_cvl_generation, EditingTools, FocusPolicy, SourceEditing, ProverTool, ) -from composer.spec.source.artifacts import ProverArtifactStore, ComponentSpec, InvariantSpec +from composer.spec.source.artifacts import ProverArtifactStore, ComponentSpec from composer.spec.source.report_prover import make_prover_fetcher from composer.spec.source.report.collect import ( - Formalized, EvidenceFetcher, ReportComponentInput, RuleEvidence, Verdict, VerdictFetcher, + Formalized, EvidenceFetcher, RuleEvidence, Verdict, VerdictFetcher, ) from composer.spec.source.report.schema import ( - AppliedEditRecord, ComponentName, RuleName, SourceEditRecord, + AppliedEditRecord, RuleName, SourceEditRecord, ) from composer.spec.source.cex_capture import CexAnalysisStore from composer.spec.source.munge.vfs_diff import diff_against_baseline from composer.spec.source.task_ids import ( HARNESS_TASK_ID, AUTOSETUP_TASK_ID, SUMMARIES_TASK_ID, - INVARIANTS_TASK_ID, INVARIANT_CVL_TASK_ID, ) from composer.prover.core import ProverOptions from composer.ui.autoprove_app import AutoProvePhase @@ -74,7 +68,7 @@ from composer.pipeline.ecosystem import main_instance from composer.pipeline.run_mode import RunMode from composer.pipeline.keys import COMMON_SYSTEM_CACHE_KEY -from composer.spec.source.keys import AP_PROPERTIES_KEY_NAME, INV_CVL_KEY +from composer.spec.source.keys import AP_PROPERTIES_KEY_NAME @dataclass class _ProverPipelineDeps: @@ -86,20 +80,13 @@ class _ProverPipelineDeps: def to_prover_tool(self, tool: BaseTool) -> ProverTool: return ProverTool(lg_tool=tool, options=self.prover_options) -#: The invariant CVL's slot in the report: a real delivery (imported by every component spec) -#: or the quarantined leftovers of a budget-curtailed generation (appendix only). -type InvariantResult = Delivered[GeneratedCVL] | Curtailed[Delivered[GeneratedCVL]] - - @dataclass 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.""" + config + resource set.""" _prover_tool: BaseTool _prover_config: dict _resources: list[CVLResource] - _invariant: tuple[list[PropertyFormulation], InvariantResult] | None _fetch: VerdictFetcher[GeneratedCVL] _deps: _ProverPipelineDeps @@ -139,16 +126,6 @@ async def formalize( ), ) - @override - def extra_report_inputs(self) -> list[ReportComponentInput[GeneratedCVL]]: - # The synthetic structural-invariant entry; per-component inputs are assembled by the driver. - if self._invariant is None: - return [] - inv_props, inv = self._invariant - return [ReportComponentInput( - name=ComponentName("Structural Invariants"), props=inv_props, formalized=inv, - )] - @override async def fetch_verdicts( self, formalized: Formalized[GeneratedCVL], @@ -159,8 +136,6 @@ async def fetch_verdicts( async def source_edits( self, outcomes: list[ComponentOutcome[GeneratedCVL, ContractComponentInstance]], run: PipelineRun ) -> list[SourceEditRecord]: - # Only real component outcomes can carry edits: the structural-invariant - # phase runs without an editing kit (see SourceEditing). records: list[SourceEditRecord] = [] for o in outcomes: if not isinstance(o.result, Delivered) or not o.result.result.applied_edits: @@ -197,17 +172,14 @@ async def finalize(self, outcomes: list[ComponentOutcome[GeneratedCVL, ContractC for o in outcomes if isinstance(o.result, Delivered) and o.result.run_link } - if self._invariant is not None: - inv = self._invariant[1] - if isinstance(inv, Delivered) and inv.run_link: - runs[InvariantSpec().run_key] = inv.run_link self._deps.store.write_component_runs(runs) @dataclass 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``.""" + prover-only pre-formalization work (AutoSetup, then custom summaries) in + ``prepare_formalization``.""" _sys_desc: SystemDescriptionHarnessed _harnessed: HarnessedApplication _prover_tool: BaseTool @@ -217,91 +189,6 @@ class ProverPrepared(PreparedSystem[GeneratedCVL, ContractComponentInstance, Con @override 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( - self._autosetup(run), self._invariants(run), - ) - - invariant: tuple[list[PropertyFormulation], InvariantResult] | None = None - if invariants.inv: - inv_props = [ - PropertyFormulation( - title=PropertyTitle(inv.name), description=inv.description, sort="invariant", - ) - for inv in invariants.inv - ] - self._deps.store.write_properties(InvariantSpec(), inv_props) - - inv_cvl_ctx = run.ctx.child(INV_CVL_KEY) - cached = await inv_cvl_ctx.cache_get(GeneratedCVL) - inv_cvl: GeneratedCVL | Curtailed[GeneratedCVL] - if cached is not None: - inv_cvl = cached - else: - inv_result = await run.runner( - TaskInfo(INVARIANT_CVL_TASK_ID, "Invariant CVL", AutoProvePhase.CVL_GEN), - lambda: batch_cvl_generation( - ctx=inv_cvl_ctx.abstract(CVLGeneration), - init_config=setup_config.prover_config, - props=inv_props, - component=None, - resources=resources, - prover_tool=self._deps.to_prover_tool(self._prover_tool), - env=run.env, - description="Structural invariant CVL", - source=run.source, - spec_dir=SPECS_DIR, - spec_stem=InvariantSpec().stem, - # Invariants are assumed as preconditions by every - # downstream spec, so they must hold against the - # unedited source: no editor, frozen source tools, - # immutable-source judge — and, since the two travel - # together, no plugin tool contribution either. - editing_tools=None, - ), - ) - if isinstance(inv_result, GaveUp): - raise RuntimeError( - f"Structural invariant CVL generation gave up: {inv_result.reason}" - ) - inv_cvl = inv_result - if isinstance(inv_result, GeneratedCVL): - await inv_cvl_ctx.cache_put(inv_result) - - if isinstance(inv_cvl, Curtailed): - # The budget cut the invariant CVL short. An unreliable invariants.spec must not - # be imported into the per-component specs as assumed preconditions, so the - # partial (if any) is quarantined for inspection and the invariants surface only - # in the report's budget appendix; the run itself degrades gracefully. - partial = ( - Delivered( - inv_cvl.partial, - self._deps.store.write_quarantined(InvariantSpec(), inv_cvl.partial), - ) - if inv_cvl.partial is not None else None - ) - invariant = (inv_props, Curtailed(partial, inv_cvl.detail)) - else: - # Writes invariants.spec + bundle, returns its project-root-relative path. - inv_path = self._deps.store.write_artifact(InvariantSpec(), inv_cvl) - # All pre-formalization work has joined, so appending here is race-free; - # the per-component CVLs (run after this returns) will see invariants.spec. - resources = [*resources, CVLResource( - path=inv_path, - required=False, - description="Structural invariants that may be assumed as preconditions", - sort="import", - )] - invariant = (inv_props, Delivered(inv_cvl, inv_path)) - - return ProverRunner( - GeneratedCVL, "prover", - self._prover_tool, setup_config.prover_config, resources, invariant, - make_prover_fetcher(), self._deps - ) - - async def _autosetup(self, run: PipelineRun) -> tuple[SetupSuccess, list[CVLResource]]: setup_config = await run.runner( TaskInfo(AUTOSETUP_TASK_ID, "AutoSetup", AutoProvePhase.AUTOSETUP), lambda: run_autosetup_phase( @@ -314,6 +201,8 @@ async def _autosetup(self, run: PipelineRun) -> tuple[SetupSuccess, list[CVLReso description="AutoSetup-generated summaries", sort="import", )] + # The custom summaries build on AutoSetup's config, so they follow it rather than + # running alongside it. if self._sys_desc.erc20_contracts or self._sys_desc.external_interfaces: summary_resource = await run.runner( TaskInfo(SUMMARIES_TASK_ID, "Custom Summaries", AutoProvePhase.SUMMARIES), @@ -326,12 +215,11 @@ async def _autosetup(self, run: PipelineRun) -> tuple[SetupSuccess, list[CVLReso ), ) resources.append(summary_resource) - return setup_config, resources - async def _invariants(self, run: PipelineRun): - return await run.runner( - TaskInfo(INVARIANTS_TASK_ID, "Structural Invariants", AutoProvePhase.INVARIANTS), - lambda: get_invariant_formulation(run.ctx, run.source, run.env, self._harnessed), + return ProverRunner( + GeneratedCVL, "prover", + self._prover_tool, setup_config.prover_config, resources, + make_prover_fetcher(), self._deps ) @dataclass @@ -353,9 +241,9 @@ class ProverBackend: analysis_store: CexAnalysisStore async def preflight(self, run: PipelineRun[AutoProvePhase, None]) -> None: - """Nothing to do ahead of analysis. The prover's expensive pre-work (AutoSetup, summaries, - structural invariants) needs the *harnessed* model, so it stays in ``prepare_formalization``, - where it already overlaps property extraction.""" + """Nothing to do ahead of analysis. The prover's pre-work (AutoSetup, then the custom + summaries built on its config) needs the *harnessed* model, so it stays in + ``prepare_formalization``, where it already overlaps property extraction.""" return None async def prepare_system( diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index 4f26d2b6..6a7674d7 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -132,6 +132,21 @@ def _executed_rules( to_filt = set(r["rules"]["selector"]) return [ r_id for r_id in r["declared_rules"] if r_id not in to_filt ] +def declared_rules_at( + history: Sequence[ProverHistoryItem], state_digest: str +) -> set[str] | None: + """The rule/invariant names the typechecker found in the spec that ``state_digest`` identifies, + or None if no run covered that state. + + Every ``verify_spec`` records what the prover declared, so this is ground truth about the + published spec rather than the author's account of it. None is the honest answer under a lifted + publish gate: a budget wrap-up publishes without ever having run the prover.""" + for item in reversed(history): + if item["sort"] == "run" and item["state_digest"] == state_digest: + return set(item["declared_rules"]) + return None + + #: How many consecutive runs must end in the identical failure before the author is nagged #: about a rule. Counts the run being processed, so 3 means "this run plus the two before it". STUCK_RULE_NAG_THRESHOLD = 3 @@ -273,9 +288,8 @@ class ProverStateExtra(TypedDict): type ProverEvents = CEXAnalysisStart | CloudPollingEvent | ProverOutputEvent | RuleAnalysisResult | ProverRun | ProverLink | ProverResult # ``verify_spec`` only runs in the source pipeline, whose state always seeds -# ``version_history`` — permanently empty in phases without the edit tools -# (structural invariants, never-edited authors), in which case it contributes -# nothing to the digest. The prover's validation stamp is bound to it so a +# ``version_history`` — permanently empty for an author that never edited, in +# which case it contributes nothing to the digest. The prover's validation stamp is bound to it so a # post-run edit invalidates the stamp. class StateWithSkips(CVLGenerationState, ProverStateExtra, VersionedHistory): pass diff --git a/composer/spec/source/report/collect.py b/composer/spec/source/report/collect.py index aa23cf17..aa74fc26 100644 --- a/composer/spec/source/report/collect.py +++ b/composer/spec/source/report/collect.py @@ -1,6 +1,6 @@ """Collect the report's inputs from in-memory pipeline results + per-unit verdicts. -For each component (and the structural invariants) the report phase hands us the inferred +For each component the report phase hands us the inferred properties, the generation result (a `ReportableResult`: its skip list + property->unit mapping; a `Curtailed` wrapper when the budget cut the generation short; ``None`` if the component gave up or crashed), and a per-component run link. We split the properties into the ones a rule formalizes @@ -45,8 +45,8 @@ def output_link(self) -> str | None: class Formalized[R: ReportableResult](Protocol): """The report's view of a generation result persisted to disk: the result, the project-relative - path it was written to, the basename of the file its units live in (``autospec_.spec`` / - ``invariants.spec`` / a ``.t.sol``) — the unit-identity fallback when a verdict carries no + path it was written to, the basename of the file its units live in (``autospec_.spec`` + / a ``.t.sol``) — the unit-identity fallback when a verdict carries no source location — and the verification-run link (``None`` for backends with no run service).""" @property def result(self) -> R: ... @@ -60,7 +60,7 @@ def run_link(self) -> str | None: ... @dataclass(frozen=True) class ReportComponentInput[R: ReportableResult]: - """One unit to collect: a component or the structural invariants. ``formalized`` carries the + """One unit to collect. ``formalized`` carries the generation result and its unit file / run link; a `Curtailed` wrapper when the budget cut the generation short (its ``partial`` is the quarantined encoding, or ``None`` if nothing was published); or ``None`` when the component gave up or crashed — in which case no units were @@ -181,9 +181,9 @@ async def collect[R: ReportableResult]( """Assemble the report inputs. Returns ``(formalized_properties, rules, skipped, gave_up_components, curtailed_components, - dropped_orphan_count)``. Rules are identified by ``(unit_file, name)``: a single definition - seen through several runs (e.g. a structural invariant imported into a component spec) - collapses to one entry. Orphan units — reported by the backend but referenced by no property — + dropped_orphan_count)``. Rules are identified by ``(unit_file, name)``: a name is only unique + within a spec, so two components that independently author a rule of the same name stay + distinct, while one definition seen through several runs collapses to one entry. Orphan units — reported by the backend but referenced by no property — are dropped and counted. Verdicts are fetched concurrently via the backend `fetch_verdicts` hook, for delivered inputs only: a curtailed component's verification state is unreliable by construction, so nothing is fetched for it. diff --git a/composer/spec/source/report/schema.py b/composer/spec/source/report/schema.py index b978875b..ea70bc12 100644 --- a/composer/spec/source/report/schema.py +++ b/composer/spec/source/report/schema.py @@ -21,8 +21,9 @@ type RuleRef = tuple[str, RuleName] """A rule's identity: ``(spec_file, name)``. A name is only unique within a spec, so the defining -spec file disambiguates a rule re-stated under the same name in another spec (and collapses a single -definition — e.g. an imported structural invariant — seen through several component runs).""" +spec file disambiguates a rule re-stated under the same name in another spec — two components that +each author a supporting invariant of the same name stay distinct — while collapsing a single +definition seen through several runs.""" class Outcome(str, Enum): """Backend-agnostic per-unit (rule / test) result. Each backend's native analysis status maps @@ -332,7 +333,7 @@ class AutoProverReport(BaseModel): deprioritized: list[DeprioritizedProperty] = Field(default_factory=list) contract_name: str run_timestamp_utc: str | None = None - #: component name (or "Structural Invariants") -> prover run link/path + #: component name -> prover run link/path prover_links: dict[ComponentName, str] = Field(default_factory=dict) properties: list[FormalizedProperty] rules: list[RuleVerdict] diff --git a/composer/spec/source/struct_invariant.py b/composer/spec/source/struct_invariant.py deleted file mode 100644 index bf4742e2..00000000 --- a/composer/spec/source/struct_invariant.py +++ /dev/null @@ -1,233 +0,0 @@ -""" -Structural invariant formulation. - -Runs an LLM agent that identifies structural invariants for a contract, -with a feedback sub-agent that validates each candidate invariant. -The resulting invariants are converted to ``PropertyFormulation`` instances -and fed into ``generate_batch_cvl`` by the pipeline. -""" - -import asyncio -from typing import Literal, Annotated, NotRequired, override - -from typing_extensions import TypedDict -from pydantic import Field, BaseModel - -from langgraph.types import Command -from langgraph.graph import MessagesState -from langchain_core.messages import ToolMessage - -from graphcore.tools.schemas import WithInjectedId, WithAsyncImplementation -from graphcore.graph import FlowInput - -from composer.tools.thinking import RoughDraftState, get_rough_draft_tools -from composer.spec.graph_builder import bind_standard, run_to_completion -from composer.spec.context import WorkflowContext, SourceFields, SourceCode, CacheKey, InvJudge -from composer.spec.service_host import ServiceHost -from composer.spec.system_model import HarnessedApplication -from composer.spec.gen_types import TypedTemplate -from composer.spec.util import uniq_thread_id -from composer.ui.tool_display import tool_display - - -# --------------------------------------------------------------------------- -# Models -# --------------------------------------------------------------------------- - -class BaseInvariant(BaseModel): - """A single invariant.""" - name: str = Field(description="A unique, descriptive name of the invariant. Must not contain spaces (use snake casing if necessary)") - description: str = Field(description="A semi-formal, natural language description of the invariant to formalize.") - - -class Invariants(BaseModel): - """The structural invariants identified in the analysis.""" - inv: list[BaseInvariant] = Field(description="The invariants you identified") - - -type InvFeedbackSort = Literal[ - "GOOD", - "NOT_STRUCTURAL", - "NOT_INDUCTIVE", - "UNLIKELY_TO_HOLD", - "NOT_FORMAL", -] - - -class InvariantFeedback(BaseModel): - """Feedback on a given invariant.""" - sort: InvFeedbackSort = Field(description="Your classification on the invariant") - explanation: str = Field(description="An explanation of your finding, including any suggestions for improvement.") - - -STRUCTURAL_INV_KEY = CacheKey[None, Invariants]("structural-inv") -INV_JUDGE_KEY = CacheKey[Invariants, InvJudge]("judge") - - -# --------------------------------------------------------------------------- -# Agent -# --------------------------------------------------------------------------- - -def _merge_invariant_feedback( - left: dict[str, tuple[str, InvFeedbackSort]], - right: dict[str, tuple[str, InvFeedbackSort]], -) -> dict[str, tuple[str, InvFeedbackSort]]: - to_ret = left.copy() - for k, v in right.items(): - to_ret[k] = v - return to_ret - -class InvariantParams(TypedDict): - context: HarnessedApplication - contract_spec: SourceFields - -_typed_invariant_prompt = TypedTemplate[InvariantParams]("structural_invariant_prompt.j2") - -async def get_invariant_formulation( - ctx: WorkflowContext[None], - source: SourceCode, - env: ServiceHost, - app: HarnessedApplication -) -> Invariants: - """Run the structural invariant formulation agent. - - An LLM agent reads the contract source, proposes structural invariants, - and validates each one through a feedback sub-agent. Returns invariants - that passed all feedback criteria. - - Args: - ctx: Workflow context for threading, memory, and checkpointing. - source: Source code metadata (used for template rendering). - source_tools: Builder with fs_tools for source code reading. - - Returns: - Validated structural invariants. - """ - inv_ctx = ctx.child(STRUCTURAL_INV_KEY) - if (cached := await inv_ctx.cache_get(Invariants)) is not None: - return cached - - judge_ctx = inv_ctx.child(INV_JUDGE_KEY) - - class InvExtra(TypedDict): - invariant_data: Annotated[ - dict[str, tuple[str, InvFeedbackSort]], - _merge_invariant_feedback, - ] - - class ST(MessagesState, InvExtra): - result: NotRequired[Invariants] - - class InvInput(FlowInput, InvExtra): - pass - - def _validate_invariants(s: ST, i: Invariants) -> str | None: - all_invariant_names: set[str] = set() - for inv in i.inv: - if inv.name in all_invariant_names: - return f"Multiple definitions for {inv.name}" - all_invariant_names.add(inv.name) - feed_rec = s["invariant_data"].get(inv.name, None) - if feed_rec is None or feed_rec[0] != inv.description or feed_rec[1] != "GOOD": - return f"Invariant with name {inv.name} (with description `{inv.description}`) was never accepted by feedback judge" - return None - - # -- Feedback sub-agent -- - - class FeedbackExtra(RoughDraftState): - pass - - class FeedbackST(MessagesState, FeedbackExtra): - result: NotRequired[InvariantFeedback] - - class FeedbackInput(FlowInput, FeedbackExtra): - pass - - feedback_graph = bind_standard( - env.builder_heavy(), - FeedbackST, - ).with_sys_prompt_template( - "invariant_judge_system_prompt.j2" - ).with_initial_prompt_template( - "invariant_judge_prompt.j2", - contract_spec=source, - ).with_tools( - [judge_ctx.get_memory_tool(), *get_rough_draft_tools(FeedbackST), *env.source_tools] - ).with_input( - FeedbackInput - ).compile_async() - - sem = asyncio.Semaphore(3) - - @tool_display("Getting feedback", "Invariant feedback") - class InvariantFeedbackTool(WithInjectedId, WithAsyncImplementation[Command]): - """ - Receive feedback on one of your invariants. - - You may call this tool in parallel. - """ - inv: BaseInvariant = Field(description="The invariant to receive feedback on") - - @override - async def run(self) -> Command: - async with sem: - res = await run_to_completion( - feedback_graph, - FeedbackInput( - input=[f"The invariant is called: {self.inv.name}\nStatement: {self.inv.description}"], - memory=None, - did_read=False, - ), - thread_id=uniq_thread_id("invariant-judge"), - recursion_limit=judge_ctx.recursion_limit, - description=f"Invariant feedback: {self.inv.name}", - within_tool=self.tool_call_id, - ) - assert "result" in res - feedback: InvariantFeedback = res["result"] - return Command(update={ - "messages": [ToolMessage( - tool_call_id=self.tool_call_id, - content=f"Judgment: {feedback.sort}\nExplanation: {feedback.explanation}", - )], - "invariant_data": { - self.inv.name: (self.inv.description, feedback.sort) - }, - }) - - # -- Main formulation agent -- - - bound_template = _typed_invariant_prompt.bind({ - "context": app, - "contract_spec": source - }) - - graph = bind_standard( - env.builder_heavy(), - ST, - doc="The structural/state invariants you identified", - validator=_validate_invariants, - ).with_sys_prompt_template( - # The formulation agent only has source tools — suppress the partial's - # CVL researcher/manual guidance (those tools are not bound here). - "source_cvl_system_prompt.j2", with_cvl_tools=False - ).inject( - lambda g: bound_template.render_to(g.with_initial_prompt_template) - ).with_tools( - [inv_ctx.get_memory_tool(), InvariantFeedbackTool.as_tool("invariant_feedback"), *env.source_tools] - ).with_input( - InvInput - ).compile_async() - - st = await run_to_completion( - graph=graph, - input=InvInput(input=[], invariant_data={}), - thread_id=inv_ctx.thread_id, - recursion_limit=inv_ctx.recursion_limit, - description="Structural invariant formulation", - ) - - assert "result" in st - to_ret: Invariants = st["result"] - await inv_ctx.cache_put(to_ret) - return to_ret diff --git a/composer/spec/source/task_ids.py b/composer/spec/source/task_ids.py index 08b3331e..3a5e8a17 100644 --- a/composer/spec/source/task_ids.py +++ b/composer/spec/source/task_ids.py @@ -14,6 +14,4 @@ HARNESS_TASK_ID = "harness" AUTOSETUP_TASK_ID = "autosetup" SUMMARIES_TASK_ID = "summaries" -INVARIANTS_TASK_ID = "invariants" -INVARIANT_CVL_TASK_ID = "invariant-cvl" REPORT_TASK_ID = "report" diff --git a/composer/spec/types.py b/composer/spec/types.py index b2c84d57..b52d5735 100644 --- a/composer/spec/types.py +++ b/composer/spec/types.py @@ -19,8 +19,7 @@ # ``CheckName``: the backend's name for one check — a CVL rule, a foundry # test, a fuzz harness function. ``FormalResult.property_checks()`` maps each # property title onto the checks that verify it. -# ``ComponentName``: human name of an AIComposer component (e.g. "Increment"), -# or "Structural Invariants". +# ``ComponentName``: human name of an AIComposer component (e.g. "Increment"). # ``PropertyTitle``: a property's unique snake_case title — the key in a # component's ``property_rules`` mapping. # diff --git a/composer/templates/invariant_explanation.j2 b/composer/templates/invariant_explanation.j2 deleted file mode 100644 index 9725f3b9..00000000 --- a/composer/templates/invariant_explanation.j2 +++ /dev/null @@ -1,30 +0,0 @@ -You are assisting in the setup for a formal verification project for a Web3 application. - -These formal verification projects typically prove important safety or security properties surrounding -the Web3 application. These properties are proven using the Certora Prover, a symbolic reasoning tool -which can explore all possible inputs and potential states when determining if a property holds. - -However, these properties typically rely on "structural", "sane state", or "well formed" invariants to -rule out violations due to infeasible starting states. For example, a property might be violated because -the prover found a starting state where some user's balance of a token was significantly greater than the -total supply of that token; a clearly infeasible starting state for a well-behaved and implemented token. - -Thus, the first step of any formal verification project is to identify these "structural invariants" -and formulate them for the purpose of ruling out spurious counter examples when verifying -security and safety properties. - -These invariants must be inductive; that is, they must hold at contract creation, and must hold after -any step of the contract assuming the invariant in the prestate. - -IMPORTANT: The line between a "structural invariant" and a safety/security property is not well-defined; -it is arguably a safety property that a user's balance of tokens does not exceed the totalSupply. -There is no definite rule of thumb, however the following are some key indicators that a property is a structural invariant: -1. It is "obvious" to an informed reader of the code -2. It is more "structural" than "mathematical" - a. For example, the owner of an active auction must appear in the "approved users" mapping - b. As another example, every position slot with a non-zero "owner" field must also have non-zero "backingAsset" field -3. It is, with high probability, fundamental to *other* security properties. - -The above list is NOT exhaustive, and an invariant under consideration need not necessarily satisfy all or even any -of these criteria. For example, the total supply invariant mentioned above clearly involves math (and so appears to not meet -criteria 2) but *does* meet criteria 3 (likely to be important to other safety/security properties). diff --git a/composer/templates/invariant_judge_prompt.j2 b/composer/templates/invariant_judge_prompt.j2 deleted file mode 100644 index bbd88ea9..00000000 --- a/composer/templates/invariant_judge_prompt.j2 +++ /dev/null @@ -1,47 +0,0 @@ - -{% include "invariant_explanation.j2" %} - - - -You are tasked with reviewing a proposed invariant for the contract {{ contract_spec.contract_name }} located at {{ contract_spec.relative_path }}. - -You should evaluate the proposed invariant against several different criteria: -1. Plausibility: Is it *likely* to hold given the current implementation? -2. Formalizability: Is it *likely* that this invariant can be formalized as formal CVL specification? Invariants which are overly - broad of vague are not formalizable. -3. Inductive: Is the invariant inductive? If it is a *temporal* property (e.g., "at some point, X is no longer true" or "after X, Y is true") - then the invariant is definitely NOT inductive. -4. Structural: Is the invariant significantly structural? - -If the invariant fails any of the above criteria, then you should return feedback to this effect. However, the bar -to use when measuring the invariant against these criteria depends on the specific criterion: -1. Plausibility: Reject only if there is *overwhelmingly strong evidence* that the invariant will not hold -2. Formalizability: Reject if there are any significant issues with the formalization -3. Inductive: Reject if there are any significant concerns regarding the inductiveness -4. Structural: Reject only if there is *strong evidence* that the invariant does not qualify as structural - -In summary, the bar to reject an invariant requires *at least* 60% confidence in all cases. - -{% with draft_subject = "your feedback" %} -{% include "rough_draft_protocol.j2" %} -{% endwith %} - -If the invariant meets the above criteria, use the result tool to return "GOOD", otherwise output the reason -for your rejection and concrete suggestions. - - -You will be asked to evaluate multiple invariants, and sometimes multiple attempts at the same invariant. - -Make liberal use of your memory tool to keep any notes or conclusions you have about the Web3 application -being analyzed, along with any notes about your feedback on the proposed invariants. - -In particular, if you learn some fact "field X is always used in context Y" that is likely relevant in other contexts, -record that information to avoid having to re-analyze source code as much as possible. - -**IMPORTANT**: Do NOT give contradictory feedback in different rounds on the same invariant; your feedback -should always be "monotone". - -You may also assume that the code has not changed since you wrote the contents of your memory. That is, -if you concluded in a prior analysis that fact X about the implementation is true, you may assume that X is still true. - - diff --git a/composer/templates/invariant_judge_system_prompt.j2 b/composer/templates/invariant_judge_system_prompt.j2 deleted file mode 100644 index d7a8424c..00000000 --- a/composer/templates/invariant_judge_system_prompt.j2 +++ /dev/null @@ -1,5 +0,0 @@ -You are a methodical formal verification expert working at Certora, Inc. - -## Tools - -{% include "source_tools_system_prompt.j2" %} diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index 937ffc89..d1db802d 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -69,13 +69,23 @@ feedback as soon as possible. ### Verification Failure Remediation Strategies * If the failure is due to an *impossible starting state*: - + Consider whether the impossible starting state can be rule out using an *invariant*. If so, author that invariant, - and add a `requireInvariant` to the rule/invariant preserved block. - + If the impossible starting state cannot be ruled out using an invariant, attempt to write a "justification rule", - i.e., a rule which proves that the assumption is *valid*. You may then use a bare `require` statement in the rule - or invariant, but reference your written justification rule - + If the above two approaches fail, you may still consider adding `require` statements, but add comments - that either document the trust assumption you are making and/or arguing for its Validity + + The state is impossible because the contract's fields stand in a relationship the counterexample broke. + State that relationship as an *invariant* in this spec, prove it here alongside your rules, and cite it with + `requireInvariant` in the failing rule, or in the failing invariant's `preserved` block. This is the default + move, not the last one: an invariant is proven against the code, where a `require` is assumed without proof. + The first time you reach for one, call the `structural_invariant_guidance` tool — it describes what + makes a state relationship worth stating as an invariant, and the four ways a candidate goes wrong. + + A supporting invariant is an ordinary declaration in your spec. `verify_spec` checks it like everything else, + it must reach VERIFIED before you can deliver, and you list it in `property_rules` under the property it + supports, so a reader can see what that property's proof rests on. Never mark a supporting invariant with + `expect_rule_failure`: a `requireInvariant` citing an unproven invariant assumes exactly what you failed to prove. + + If the relationship cannot be stated as an invariant — no single method preserves it, or it quantifies over + something CVL cannot reach — write a "justification rule", i.e., a rule which proves that the assumption is + *valid*. You may then use a bare `require` statement in the failing rule, naming your justification rule in a + comment beside it. + + A bare `require` with neither an invariant nor a justification rule behind it is the last rung, and it leaves + the property proven only under an assumption nothing checks. If you take it, state in a comment what you + assumed, why the contract cannot reach a state that violates it, and what the property therefore no longer covers. * If the failure is due to a HAVOC from an unresolved call: follow the triage ladder described in section B3 of the "CVL Summarization — Knowledge Base" context document * If the counterexample appears to point to a potential issue in the code that should be reviewed by a security expert, @@ -121,7 +131,11 @@ the positive feedback result, and will necessitate "restamping". The `result` tool *also* requires a `property_rules` mapping: for every property you did NOT skip (referenced by its unique snake_case title from the batch listing above), list the name(s) of the rule(s)/invariant(s) in your -spec that verify it. Every non-skipped property must appear in this mapping with at least one rule; skipped +spec that verify it, including anything they rest on — a supporting invariant cited with `requireInvariant`, +a justification rule behind a `require`. Every rule and invariant your spec declares must be named by some +property: one that no property names is dropped from the report, so the reader would see the property's +verdict without seeing what it rests on. Every non-skipped property must appear in this mapping with at +least one rule; skipped properties must NOT appear. The result tool will be rejected if this mapping is incomplete or references a skipped or unknown property title. @@ -140,6 +154,9 @@ You therefore may not retire them. `record_skip` will refuse them, and the `give `sort='exhausted'` stop until you have actually put a spec in front of the prover several times and can enumerate what you tried. When you are stuck, the move is to make the problem smaller, not to put it down: + - State the missing fact. If the prover keeps starting the property from states the contract cannot + reach, what is missing is a fact about the state, not a smaller property. State that fact as an + invariant, prove it here, and cite it. - Decompose it. Prove a smaller statement that the property is built out of as its own rule, and work up from there. - Weaken it honestly. If the full property will not go through, formalize the strongest version of it @@ -185,7 +202,7 @@ You may also make use of the following CVL resources, available as CVL files. {% if res.required %} You MUST ensure your final specification imports this file. {% else %} - You may use this import at your discretion (e.g., it defines an invariant necessary to prove your rule/invariant). + You may use this import at your discretion (e.g., it defines a summary you need for a call your rule makes). {% endif %} {% endfor %} @@ -198,11 +215,9 @@ your current approach. Be sure to update your memory *before* calling the result -{% if context %} {% include "application_context_new.j2" %} -{% endif %} {% include "cvl_additions.j2" %} diff --git a/composer/templates/property_generation_system_prompt.j2 b/composer/templates/property_generation_system_prompt.j2 index 7c85f0df..2ff07198 100644 --- a/composer/templates/property_generation_system_prompt.j2 +++ b/composer/templates/property_generation_system_prompt.j2 @@ -23,7 +23,6 @@ With neither argument, the run executes every rule and invariant declared in the either list refer to the declarations in the current spec. `verify_spec` must be the only tool call in its turn. -{% if source_editing %} ## Editing the Source Under Verification The Solidity you are verifying is a working copy, and you have a narrow ability to have it changed @@ -48,7 +47,6 @@ Treat source edits as a last resort, reached only after spec-side approaches hav applied edit becomes part of the final deliverable, where a human auditor must read and accept it. After applying or reverting an edit, prover results and feedback verdicts obtained before the change no longer describe your working copy — re-run them before relying on them. -{% endif %} ## Authoring CVL with References @@ -68,3 +66,7 @@ are good reasons to use this "expect failure" functionality: the rule failure is the intended result. 2. Verifying the rule is hitting some limitation in the prover (including prover errors, etc.), and you have exhausted all reasonable alternative formulations to work around these prover limitations (errors, timeouts, imprecision). + +Never mark an invariant that another rule or `preserved` block cites with `requireInvariant`. That citation is +sound only because the invariant is proved in this same spec; expecting it to fail converts every rule that +cites it into an unproven assumption while leaving the run green. diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index c23ac043..5e7e0576 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -114,8 +114,8 @@ Invariants and quantifiers (Invariants and Quantifiers Guide): 9. An invariant expression that can itself revert passes vacuously; invariant expressions are kept revert-free (§4). 10. `requireInvariant` is a proven assumption only when the cited invariant is declared and proved in - this specification; citing a filtered or otherwise-compromised invariant launders an unproven - assumption through the exemption of Criteria 4 (§2). + this specification; citing a filtered, expect-fail-marked, or otherwise-compromised invariant + launders an unproven assumption through the exemption of Criteria 4 (§2). 11. Pointwise properties use invariant parameters rather than `forall`, and index parameters are declared `mathint` — an out-of-range instantiation is then vacuously true, where a `require_uint256` cast on a witness silently prunes executions (§5). @@ -176,13 +176,17 @@ Evaluate each rule for its *preconditions*. Remember that these rules/invariants to consider all possible initial states of the smart contract and its dependencies. Consider whether each rule sufficiently constrains the input space to rule out *obviously spurious* starting states (e.g., a case where a user balance is larger than the total supply). If you conclude that a rule will *LIKELY* fail due to a spurious starting state, propose what *invariants* are necessary to rule out those starting states. +The author can act on that: it may declare the invariant in this same spec, prove it here, and cite it with `requireInvariant`. Where a rule instead +reaches for a bare `require` to rule out the same starting state, that is a Criteria 4 finding — carry it there. NOTE: portions of the input state may be unconstrained/underconstrained if they don't matter for the purposes of the property being verified. ### Criteria 4: Overconstrained Inputs -You may also consider the inverse; over-constraining the input space may cause the prover to miss real bugs. In particular, any constraints in -`preserved` blocks that are *not* a `requireInvariant` statement (i.e., a *proven* assumption) should be subject to intense scrutiny. +You may also consider the inverse; over-constraining the input space may cause the prover to miss real bugs. In particular, any constraint on the +*shape of the prestate* — a relationship among the contract's own state fields — that is not a `requireInvariant` (i.e., a *proven* assumption) +should be subject to intense scrutiny, wherever it appears: a `preserved` block or a rule body. That is what an invariant is for; a bare `require` +assumes the relationship instead of establishing it. A constraint that merely bounds a rule's own free inputs is Criteria 3's business, not this one. Justification for such requirements like "X is impossible in a realistic situation/deployment/etc" should not be taken at face value; do not check that justifications a simply provided, critically evaluate the argument underpinning the justifications. @@ -296,6 +300,10 @@ Verify that the specification covers all {{ properties | length }} listed proper - If the spec neither addresses the property NOR carries an author skip: reject the spec and flag the missing property. - If the author declared a skip: evaluate it by the rules below. +A property's `property_rules` entry may also name a supporting invariant that its rules cite with +`requireInvariant`. That invariant is part of how the property is proven, not a second rule covering +it; judge coverage by the rule that checks the property itself. + #### Coverage-defeating exclusions A rule or invariant does not cover a property if it excludes the primary methods the property is diff --git a/composer/templates/structural_invariant_guidance.j2 b/composer/templates/structural_invariant_guidance.j2 new file mode 100644 index 00000000..2fa3438b --- /dev/null +++ b/composer/templates/structural_invariant_guidance.j2 @@ -0,0 +1,79 @@ + +A counterexample that starts from a state the contract could never reach means the spec is missing a +constraint that the code maintains: the contract's fields stand in some relationship, and nothing in the +spec says so. The prover explores every state the spec admits, so unless a constraint rules it out it may +start from a state where a user's token balance exceeds total supply. + +The fix is to state that relationship as an invariant and prove it. This document is about *choosing* what +to state. The mechanics — the induction shape, strengthening, lemma invariants, `preserved` blocks, +`requireInvariant`, `strong`, the soundness audit — are in the "CVL Invariants and Quantifiers" guide that +is already in your context. + +## What makes a good candidate + +The line between this kind of invariant and a safety property is not well defined; it is arguably a safety +property that a user's balance does not exceed the total supply. There is no definite rule of thumb, but +these are the key indicators: + +1. It is "obvious" to an informed reader of the code. +2. It is more structural than mathematical. For example: the owner of an active auction must appear in the + "approved users" mapping. Or: every position slot with a non-zero `owner` field must also have a + non-zero `backingAsset` field. +3. It is, with high probability, fundamental to *other* security properties. + +This list is not exhaustive, and a candidate need not satisfy all or even any of them. The total-supply +invariant above clearly involves math, so it appears to fail indicator 2 — but it meets indicator 3, and it +is a good invariant. + +## Where to look + +The contract's storage layout, its state-modifying functions, its access control patterns, and the +relationships between its data structures. + + + +## Four ways a candidate goes wrong + +Check your candidate against these before you spend a prover run on it. + +1. **Not structural.** What you have is a safety or security property rather than a relationship the code + maintains. Consider whether it can be restated as a simpler, structural relationship. + Bad example: "no user can withdraw more collateral than they deposited" + (a safety property; it is about what an actor may do, not about how the fields stand) + Good example: "every position slot with a non-zero `owner` has a non-zero `backingAsset`" + (the same concern, restated as a relationship the code maintains) +2. **Not inductive.** The statement cannot be proven by induction, usually because it references specific + functions or call sequences. Reformulate it so it holds regardless of which function was called. + Bad example: "after `settleAuction` runs, the auction's owner is in the approved-users mapping" + (names a function; this is a postcondition of that function) + Good example: "the owner of an active auction is in the approved-users mapping" + (holds in every reachable state, whichever function ran) +3. **Unlikely to hold.** The relationship probably is not maintained by this implementation. Re-read the + source before formalizing it. + Bad example: "`backingAsset` is never the zero address" + (proposed without checking; the constructor leaves it zero until the first deposit) + Good example: "`backingAsset` is non-zero for every slot whose `owner` is non-zero" + (the guard the code actually maintains) +4. **Not formal.** The statement is too vague to formalize. Make it precise enough to be a logical formula + over the contract's state. + Bad example: "the accounting is consistent" + Good example: "the sum over all holders of `balances[holder]` equals `totalSupply`" + +The bars are not symmetric. Drop a candidate on any real doubt about its inductiveness or its +formalizability. Do *not* drop one merely because it looks mathematical. + +## Naming a function is the usual mistake + +An inductive invariant holds regardless of which function was called, or in what order. If you find +yourself naming a specific function in the statement, you are describing a postcondition, not an invariant. +That is the single most common way a candidate fails, and it is what failure mode 2 above looks like in +practice. + +## Invariants that depend on each other + +Invariant i1 depends on i2 when proving i1 preserved requires assuming i2 in the prestate — that is, +without i2 the prover would consider states where i1 is spuriously violated. If i1 states "every active +position has a non-zero owner" and i2 states "the position count never exceeds the array length", then i1 +likely depends on i2: without i2 the prover can consider out-of-bounds positions that vacuously violate i1. +When that happens, prove i2 as well and cite it in i1's `preserved` block. + diff --git a/composer/templates/structural_invariant_prompt.j2 b/composer/templates/structural_invariant_prompt.j2 deleted file mode 100644 index 20b65eed..00000000 --- a/composer/templates/structural_invariant_prompt.j2 +++ /dev/null @@ -1,63 +0,0 @@ - -{% include "invariant_explanation.j2" %} - - - -This invariant formulation is being performed for {{ contract_spec.contract_name }} at {{ contract_spec.relative_path }}. - -The following is a description of the application that {{ contract_spec.contract_name }} is a part of. - -{% include "harnessed_application_context.j2" %} - - - -Follow these instructions exactly: - -## Step 1 -Read the implementation of {{ contract_spec.contract_name }} at {{ contract_spec.relative_path }} and identify -all candidate structural invariants. Examine the contract's storage layout, state-modifying functions, access control -patterns, and relationships between data structures. - -These invariants should be "obvious" to a reader of the code, and thus should be very likely to hold. -However, you do *NOT* need to have absolute certainty that a structural invariant actually holds for the implementation -to propose it. - -## Step 2 -Invoke the invariant feedback tool with the invariants generated in Step 1. The feedback tool classifies each invariant as one of: -- **GOOD**: The invariant is well-formulated and appropriate. -- **NOT_STRUCTURAL**: The property is a safety/security property, not a structural invariant. Consider whether it can be restated as a simpler, structural relationship. -- **NOT_INDUCTIVE**: The property cannot be proven inductively — it may reference specific functions or call sequences. Reformulate as a property that holds regardless of which function was called. -- **UNLIKELY_TO_HOLD**: The property probably does not hold for the implementation. Re-examine the source code to verify your assumption. -- **NOT_FORMAL**: The statement is too vague to formalize. Make it precise enough that it could be translated to a logical formula over the contract's state. - -If any invariant is not classified as "GOOD", adjust your formulation to address the feedback, or drop the invariant if it cannot be restated. - -*IMPORTANT* DO NOT proceed to step 3 until the feedback judge indicates all the invariants presented to it are GOOD. - -## Step 3 -Consider dependencies between your invariants. Invariant i1 depends on invariant i2 when proving i1 is preserved -likely requires assuming i2 in the prestate — that is, without i2, the prover would consider states where i1 is -spuriously violated. - -For example, if i1 states "every active position has a non-zero owner" and i2 states "the position count never -exceeds the array length", then i1 likely depends on i2 because without i2, the prover could consider -out-of-bounds positions that vacuously violate i1. - -## Step 4 -Output the results of your analysis using the provided tool. - - - - - Do NOT attempt to write the CVL to check these properties yourself, instead focus simply on identifying - and stating the properties in semi-formal natural language. - - - The structural invariants you identify should be inductive, i.e., proven to hold with an inductive proof. - Do NOT propose properties of the form "after calling function F, property P holds" — these are not inductive. - An inductive invariant must hold regardless of which function was called or in what order. If you find yourself - referencing a specific function in the invariant statement, you are likely describing a postcondition, not a - structural invariant. - - - diff --git a/composer/testing/record_tape.py b/composer/testing/record_tape.py index 20c4a408..e782c5f2 100644 --- a/composer/testing/record_tape.py +++ b/composer/testing/record_tape.py @@ -19,8 +19,8 @@ its ``AIMessage`` is never checkpointed to any thread. It is invisible to post-hoc reconstruction, but it flows through the *same* llm object, so recording captures it for free — in the correct lane and position. -* **Subagent interleaving** — code_explorer / feedback / cvl_research / - invariant_feedback subagents run inside the parent phase's task scope, so +* **Subagent interleaving** — code_explorer / feedback / cvl_research + subagents run inside the parent phase's task scope, so ``get_current_task_id()`` returns the parent task_id for their calls. Recording therefore lands them in the parent lane in exact call order, with no thread-stitching heuristics. diff --git a/composer/testing/ui_harness_autoprove_Answer.py b/composer/testing/ui_harness_autoprove_Answer.py index 43c32bc2..acf346c8 100644 --- a/composer/testing/ui_harness_autoprove_Answer.py +++ b/composer/testing/ui_harness_autoprove_Answer.py @@ -11,7 +11,7 @@ COMPOSER_TEST_TAPE=autoprove_Answer console-autoprove \ --max-bug-rounds 1 [--interactive] -Lanes captured: system-analysis=4, harness=4, extract-0=3, invariants=9, formalize-0=7 +Lanes captured: system-analysis=4, harness=4, extract-0=3, formalize-0=7 """ import json @@ -351,220 +351,6 @@ "invalid_tool_calls": [] } ], - "invariants": [ - { - "content": [ - "\n\nI'll start by checking my memory directory for any earlier progress, then examine the contract.", - { - "type": "tool_use", - "id": "toolu_0901ec41809341d4a66b", - "name": "get_file", - "input": { - "path": "src/Answer.sol" - } - } - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [ - { - "name": "get_file", - "args": { - "path": "src/Answer.sol" - }, - "id": "toolu_0901ec41809341d4a66b", - "type": "tool_call" - } - ], - "invalid_tool_calls": [] - }, - { - "content": [ - "This is an extremely simple contract. Let me analyze it:\n\n- **No state variables** \u2014 the contract has zero storage slots\n- **One function** \u2014 `theAnswer()` which is `pure` (no state reads or writes)\n- **No access control** \u2014 no owner, no roles\n- **No data structures** \u2014 no mappings, arrays, or structs\n\nFor a stateless contract with a single pure function, the only structural invariant one could state is about the absence of state \u2014 but that's inherent to the Solidity compilation (a contract with no state variables has nothing in storage).\n\nHowever, there is one meaningful invariant: the function always returns 42. But that's more of a functional correctness property than a structural invariant. Let me think about what could qualify as structural here...\n\nThe only thing that could serve as a structural invariant for a stateless contract is that all storage slots are zero (since no state variables are declared). Let me try this.", - { - "type": "tool_use", - "id": "toolu_0751adbf8b5f49d08f8e", - "name": "invariant_feedback", - "input": { - "inv": { - "name": "all_storage_zero", - "description": "All storage slots of the Answer contract are zero, since the contract declares no state variables and no function modifies storage." - } - } - } - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [ - { - "name": "invariant_feedback", - "args": { - "inv": { - "name": "all_storage_zero", - "description": "All storage slots of the Answer contract are zero, since the contract declares no state variables and no function modifies storage." - } - }, - "id": "toolu_0751adbf8b5f49d08f8e", - "type": "tool_call" - } - ], - "invalid_tool_calls": [] - }, - { - "content": [ - "\n\nI'll start by checking my memory for any earlier progress on this task." - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [], - "invalid_tool_calls": [] - }, - { - "content": [ - "No prior memory. Let me examine the Answer contract to understand its structure.", - { - "type": "tool_use", - "id": "toolu_ea1db844e14546759985", - "name": "get_file", - "input": { - "path": "src/Answer.sol" - } - }, - { - "type": "tool_use", - "id": "toolu_0f461818f2cb43c7ae11", - "name": "list_files", - "input": {} - } - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [ - { - "name": "get_file", - "args": { - "path": "src/Answer.sol" - }, - "id": "toolu_ea1db844e14546759985", - "type": "tool_call" - }, - { - "name": "list_files", - "args": {}, - "id": "toolu_0f461818f2cb43c7ae11", - "type": "tool_call" - } - ], - "invalid_tool_calls": [] - }, - { - "content": [ - "The contract is extremely simple - it has no state variables, no constructor that writes storage, and only a single `pure` function that returns 42. Let me save my findings and draft my feedback." - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [], - "invalid_tool_calls": [] - }, - { - "content": [ - "Now let me think more carefully about formalizability. The invariant says \"all storage slots are zero.\" In CVL, you can write invariants about specific state variables, but the contract has none. You could potentially use a `hook` on `Sstore` to track writes, but quantifying over all 2^256 storage slots is not standard CVL practice.\n\nHowever, there's a subtlety: since there are no state variables, there's literally nothing to assert about. The invariant is vacuously true but also vacuously unformalizable in a meaningful way in CVL.\n\nLet me also consider: is this really a useful structural invariant? Even if it's true, it doesn't help prove any other property since the contract has no meaningful state.", - { - "type": "tool_use", - "id": "toolu_3307214650474e15adb8", - "name": "write_rough_draft", - "input": { - "rough_draft": "The invariant \"all_storage_zero\" states that all storage slots of the Answer contract are zero since the contract declares no state variables and no function modifies storage.\n\nWhile this statement is factually correct about the contract's behavior, it has significant formalizability issues:\n\n1. **Formalizability**: The invariant quantifies over \"all storage slots,\" which means all 2^256 possible storage locations. CVL invariants typically operate on named state variables, but this contract declares none. There is no straightforward way to express \"all storage slots are zero\" as a CVL invariant. You could use a `hook Sstore` with a ghost variable to detect any storage write, but even that doesn't directly verify that pre-existing storage is zero \u2014 it only checks that no writes occur. The universal quantification over an unbounded storage space is not directly expressible in standard CVL.\n\n2. **Structural value**: While technically true, this invariant is vacuously structural. The contract has no state, so there are no other security/safety properties that would depend on this invariant. It provides no practical value as a \"structural invariant\" for ruling out infeasible starting states.\n\nRecommendation: Reject on formalizability grounds. The invariant cannot be meaningfully formalized as a CVL specification because (a) universal quantification over all 2^256 storage slots is not expressible in CVL, and (b) there are no named state variables to write an invariant about." - } - } - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [ - { - "name": "write_rough_draft", - "args": { - "rough_draft": "The invariant \"all_storage_zero\" states that all storage slots of the Answer contract are zero since the contract declares no state variables and no function modifies storage.\n\nWhile this statement is factually correct about the contract's behavior, it has significant formalizability issues:\n\n1. **Formalizability**: The invariant quantifies over \"all storage slots,\" which means all 2^256 possible storage locations. CVL invariants typically operate on named state variables, but this contract declares none. There is no straightforward way to express \"all storage slots are zero\" as a CVL invariant. You could use a `hook Sstore` with a ghost variable to detect any storage write, but even that doesn't directly verify that pre-existing storage is zero \u2014 it only checks that no writes occur. The universal quantification over an unbounded storage space is not directly expressible in standard CVL.\n\n2. **Structural value**: While technically true, this invariant is vacuously structural. The contract has no state, so there are no other security/safety properties that would depend on this invariant. It provides no practical value as a \"structural invariant\" for ruling out infeasible starting states.\n\nRecommendation: Reject on formalizability grounds. The invariant cannot be meaningfully formalized as a CVL specification because (a) universal quantification over all 2^256 storage slots is not expressible in CVL, and (b) there are no named state variables to write an invariant about." - }, - "id": "toolu_3307214650474e15adb8", - "type": "tool_call" - } - ], - "invalid_tool_calls": [] - }, - { - "content": [ - "The draft looks accurate. Let me review against the criteria once more:\n\n- **Plausibility**: It's true. \u2713\n- **Formalizability**: Universal quantification over all 2^256 storage slots is not expressible in CVL. No named state variables exist to write an invariant about. This is a significant issue. \u2717\n- **Inductive**: Trivially yes. \u2713\n- **Structural**: Vacuously true but not meaningfully structural. Borderline, but the formalizability issue alone is sufficient.\n\nThe formalizability concern is strong enough (well above 60% confidence) to reject.", - { - "type": "tool_use", - "id": "toolu_479701d7899947a78d91", - "name": "result", - "input": { - "sort": "NOT_FORMAL", - "explanation": "The invariant \"all_storage_zero\" states that all storage slots of the Answer contract are zero since the contract declares no state variables and no function modifies storage.\n\nWhile this statement is factually correct about the contract's behavior, it has significant formalizability issues:\n\n1. **Formalizability**: The invariant quantifies over \"all storage slots,\" which means all 2^256 possible storage locations. CVL invariants typically operate on named state variables, but this contract declares none. There is no straightforward way to express \"all storage slots are zero\" as a CVL invariant. You could use a `hook Sstore` with a ghost variable to detect any storage write, but even that doesn't directly verify that pre-existing storage is zero \u2014 it only checks that no writes occur. The universal quantification over an unbounded storage space is not directly expressible in standard CVL.\n\n2. **Structural value**: While technically true, this invariant is vacuously structural. The contract has no state, so there are no other security/safety properties that would depend on this invariant. It provides no practical value as a \"structural invariant\" for ruling out infeasible starting states.\n\n**Suggestion**: Since the Answer contract has no state variables and only a single `pure` function, there are no meaningful structural invariants to formulate for it. If the goal is to verify the contract's behavior, a simple rule asserting that `theAnswer()` returns 42 would be more appropriate and directly formalizable." - } - } - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [ - { - "name": "result", - "args": { - "sort": "NOT_FORMAL", - "explanation": "The invariant \"all_storage_zero\" states that all storage slots of the Answer contract are zero since the contract declares no state variables and no function modifies storage.\n\nWhile this statement is factually correct about the contract's behavior, it has significant formalizability issues:\n\n1. **Formalizability**: The invariant quantifies over \"all storage slots,\" which means all 2^256 possible storage locations. CVL invariants typically operate on named state variables, but this contract declares none. There is no straightforward way to express \"all storage slots are zero\" as a CVL invariant. You could use a `hook Sstore` with a ghost variable to detect any storage write, but even that doesn't directly verify that pre-existing storage is zero \u2014 it only checks that no writes occur. The universal quantification over an unbounded storage space is not directly expressible in standard CVL.\n\n2. **Structural value**: While technically true, this invariant is vacuously structural. The contract has no state, so there are no other security/safety properties that would depend on this invariant. It provides no practical value as a \"structural invariant\" for ruling out infeasible starting states.\n\n**Suggestion**: Since the Answer contract has no state variables and only a single `pure` function, there are no meaningful structural invariants to formulate for it. If the goal is to verify the contract's behavior, a simple rule asserting that `theAnswer()` returns 42 would be more appropriate and directly formalizable." - }, - "id": "toolu_479701d7899947a78d91", - "type": "tool_call" - } - ], - "invalid_tool_calls": [] - }, - { - "content": [ - "The feedback confirms what I suspected \u2014 this contract is so trivial that there are no meaningful structural invariants to formulate. It has no state variables, no storage, and only a pure function.\n\nLet me save my analysis and submit the result." - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [], - "invalid_tool_calls": [] - }, - { - "content": [ - "Given that the Answer contract is completely stateless with a single pure function, there are genuinely no structural invariants to identify. Structural invariants relate to relationships between state variables, storage layout consistency, and data structure well-formedness \u2014 none of which exist in this contract.\n\nI'll submit an empty invariant set, as this is the correct answer for a stateless contract.", - { - "type": "tool_use", - "id": "toolu_3f7b5c8d6cd24106a7cb", - "name": "result", - "input": { - "inv": [] - } - } - ], - "additional_kwargs": {}, - "response_metadata": {}, - "type": "ai", - "tool_calls": [ - { - "name": "result", - "args": { - "inv": [] - }, - "id": "toolu_3f7b5c8d6cd24106a7cb", - "type": "tool_call" - } - ], - "invalid_tool_calls": [] - } - ], "formalize-0": [ { "content": [ diff --git a/composer/testing/ui_harness_autoprove_Counter.py b/composer/testing/ui_harness_autoprove_Counter.py index 61c98b78..105f3398 100644 --- a/composer/testing/ui_harness_autoprove_Counter.py +++ b/composer/testing/ui_harness_autoprove_Counter.py @@ -15,9 +15,9 @@ The scenario is deliberately constrained to one contract with one component so that the per-component ``asyncio.gather`` fan-outs in the extraction and -CVL phases collapse to a single lane each. Multiple invariants and multiple -properties are still authored per-phase — a single authoring agent services -them sequentially, so each lane stays linear. +CVL phases collapse to a single lane each. Multiple properties are still +authored per-phase — a single authoring agent services them sequentially, so +each lane stays linear. ``AutoProveTaskHandler.format_hitl_prompt`` raises ``NotImplementedError`` — there is no Textual-side HITL prompt in this pipeline. The interactive @@ -38,23 +38,20 @@ is no single global call order any more. ``HarnessFakeLLM`` routes each call to a per-phase *lane* keyed by the ``run_task`` task_id (read from the ``get_current_task_id`` ContextVar that ``run_task`` sets). Within a lane the -calls happen in the order authored below; sub-agents (invariant_feedback, CEX -analyzer, cvl_research, code_explorer) inherit their parent phase's task_id, -so their responses live in the parent's lane. +calls happen in the order authored below; sub-agents (CEX analyzer, +cvl_research, code_explorer) inherit their parent phase's task_id, so their +responses live in the parent's lane. system-analysis : run_component_analysis (+ code_explorer sub-agent) harness : run_harness_creation / classifier_agent autosetup : run_autosetup_phase — a subprocess, makes NO LLM calls, so it has no lane ── after harness creation, these lanes run concurrently ── - invariants : get_invariant_formulation (+ invariant_feedback ×3) extract-0 : run_property_inference (+ refinement when --interactive) - ── staged CVL join, after the concurrent branch completes ── - invariant-cvl : batch_cvl_generation, component=None - (+ cvl_research, code_explorer, feedback ×2, CEX ×1) + ── formalization, after the pre-formalization setup joins ── formalize-0 : batch_cvl_generation, component= - (+ feedback ×1, CEX ×1 — surfaces the real - ``incrementOther`` implementation bug) + (+ cvl_research, code_explorer, feedback ×2, CEX ×1 — + surfaces the real ``incrementOther`` implementation bug) ── final, best-effort report phase ── report : build_report → call_grouping_llm (one structured-output call partitioning the formalized properties into groups) @@ -70,8 +67,7 @@ from composer.spec.source.prover import STUCK_RULE_NAG_THRESHOLD from composer.spec.source.task_ids import ( DESIGN_DOC_DISCOVERY_TASK_ID, - SYSTEM_ANALYSIS_TASK_ID, HARNESS_TASK_ID, INVARIANTS_TASK_ID, - INVARIANT_CVL_TASK_ID, REPORT_TASK_ID, + SYSTEM_ANALYSIS_TASK_ID, HARNESS_TASK_ID, REPORT_TASK_ID, ) from composer.pipeline.core import extract_task_id, formalize_task_id @@ -110,64 +106,49 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # # The Solidity source is staged on disk in # ``composer/testing/scenarios/autoprove_counter/src/Counter.sol``. These CVL -# strings are emitted as ``put_cvl_raw`` arguments during the invariant-CVL -# and component-CVL phases. Real tools validate them: +# strings are emitted as ``put_cvl_raw`` arguments during the component-CVL +# phase. Real tools validate them: # # - Typechecker.jar — gatekeeps ``put_cvl_raw`` (rejects parse errors). # - Certora prover — gatekeeps ``verify_spec`` (proves or CEXes). # Intentionally malformed surface-syntax CVL. Triggers the Typechecker.jar -# rejection path on the first ``put_cvl_raw`` of the invariant-CVL phase; +# rejection path on the first ``put_cvl_raw`` of the component-CVL phase; # the tape's next turn resubmits valid CVL. BROKEN_PARSE_CVL = """\ invariant not_valid_cvl() this is definitely not valid CVL syntax; """ -# Typechecks but the invariant is obviously false: after ``increment()`` runs, -# ``count`` is 1, so ``count == 0`` no longer holds. Used as the first -# (easy-to-catch) semantic-error candidate — the feedback judge rejects this -# on first pass without involving the prover at all. -BAD_INV_CVL = """\ -invariant increments_sum_is_count() currentContract.count == 0; -""" - -# Typechecks and declares the two ostensibly-correct invariant names, but the -# ``increments_sum_is_count`` is subtly wrong; without an init state axiom, the -# prover can choose an initial value of incrementsSum that violates the base case. -# The feedback judge approves by name-coverage; the prover catches it on the -# base case (initial state has ``count == 0``, violating ``count > 0``). -# This is the artifact that drives the verify_spec → analyze_cex_raw round-trip -# in the tape — exactly one failing rule (``count_nonneg``), so exactly one -# CEX LLM call is consumed. -SUBTLE_INV_CVL = """\ -ghost uint256 incrementsSum; - -hook Sstore currentContract.increments[KEY address who] uint256 newValue (uint256 oldValue) { - incrementsSum = require_uint256(incrementsSum + (newValue - oldValue)); +# The author's first draft: the two increment() rules, but nothing for +# ``other_increments_by_one``. Typechecks (it is COMPONENT_CVL minus its last rule), +# so it is the feedback judge rather than the Typechecker that rejects it, on +# coverage. Drives the good=False -> revise -> good=True round of the tape. +PARTIAL_COMPONENT_CVL = """\ +methods { + function count() external returns (uint256) envfree; + function increments(address) external returns (uint256) envfree; + function increment() external; + function incrementOther(address) external; } -invariant zero_address_is_zero() currentContract.increments[0] == 0; - -invariant increments_sum_is_count() currentContract.count == incrementsSum; -""" - -# Two trivially-true invariants over the Counter state. Both should verify -# against Counter.sol on first try, so verify_spec stamps the prover digest -# and the author can call `result` to terminate the invariant-CVL author graph. -GOOD_INV_CVL = """\ -ghost uint256 incrementsSum { - init_state axiom incrementsSum == 0; +rule increment_increases_count { + env e; + mathint before = count(); + increment(e); + assert to_mathint(count()) == before + 1, + "increment() must increase count by exactly 1"; } -hook Sstore currentContract.increments[KEY address who] uint256 newValue (uint256 oldValue) { - incrementsSum = require_uint256(incrementsSum + (newValue - oldValue)); +rule increment_increases_sender_tally { + env e; + address s = e.msg.sender; + mathint before = increments(s); + increment(e); + assert to_mathint(increments(s)) == before + 1, + "increment() must increase increments[msg.sender] by exactly 1"; } - -invariant zero_address_is_zero() currentContract.increments[0] == 0; - -invariant increments_sum_is_count() currentContract.count == incrementsSum; """ # Component-CVL spec: three rules covering all three extracted properties. @@ -531,220 +512,99 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: ), # ─────────────────────────────────────────────────────────────────── - # P3. Structural invariant formulation (get_invariant_formulation) + # P3. Bug analysis (run_bug_analysis, 1 component) # ─────────────────────────────────────────────────────────────────── - # Main-agent tools: memory, source_tools, invariant_feedback, result. - # Feedback sub-agent tools: memory, rough_draft, source_tools, result - # (schema: InvariantFeedback{sort, explanation}). - # Validator `_validate_invariants`: every inv in the final result must - # appear in state["invariant_data"] with (description, "GOOD") matching - # exactly. The state dict merges on name, so resubmitting the same - # name with a different description overwrites the prior entry. + # Tools available: rough_draft (via get_rough_draft_tools), + # bug_analysis_tools (= source_tools), result. + # Validator: standard bind_standard (output_key). Result schema is + # (list[PropertyFormulation], "The security properties ..."), so args + # are {"value": [...]}. # - # The tape uses 3 invariant_feedback rounds (1 bad + 2 good) to exercise - # the NOT_INDUCTIVE → resubmit recovery path, and delivers 2 invariants - # in the final result. + # `refinement` is None from the pipeline, so there is NO refinement-loop + # conversation after this — once `result` fires, the phase ends. ] -_INVARIANTS_TAPE: list[BaseMessage] = [ - - # P3.1 — exercise source_tools in the main invariant agent. - _ai( - "Reading Counter.sol to understand the state shape.", - _tc("get_file", path="src/Counter.sol"), - ), - - # P3.2 — first invariant_feedback call: candidate "count_zero" (count is - # always 0) — intentionally bad. This spawns F1.{1-3}. - _ai( - "Proposing count_zero as a structural candidate.", - _tc( - "invariant_feedback", - inv={ - "name": "count_zero", - "description": "The global count is always zero.", - }, - ), - ), +_BUG_TAPE: list[BaseMessage] = [ - # F1.1 — invariant feedback judge, first invocation, turn 1. Judge tools: - # memory, rough_draft, source_tools, result. Validator on this sub-agent - # is the standard `bind_standard` without custom checks — the only - # implicit requirement is providing `result` to set output_key. + # P3.1 — exercise source_tools + rough_draft. No did_read requirement, + # kept for coverage. _ai( - "Judge: inspecting the source + drafting a verdict.", + "Bug analysis: inspecting the entry point source.", _tc("get_file", path="src/Counter.sol"), _tc( "write_rough_draft", rough_draft=( - "count_zero claims count is always 0, but increment() " - "mutates count upward. The post-state of any increment() " - "call already violates this claim. Verdict: NOT_INDUCTIVE." - ), - ), - ), - - # F1.2 — judge: read the draft before emitting result. - _ai( - "Judge: re-reading the draft.", - _tc("read_rough_draft"), - ), - - # F1.3 — judge: NOT_INDUCTIVE verdict. This stores - # state["invariant_data"]["count_zero"] = ("The global count is always - # zero.", "NOT_INDUCTIVE"). The main agent sees the ToolMessage and can - # try a different candidate. - _ai( - "Judge: delivering NOT_INDUCTIVE verdict.", - _tc( - "result", - sort="NOT_INDUCTIVE", - explanation=( - "The claim fails immediately after any call to increment(): " - "count transitions from k to k+1 and the invariant does not " - "hold in the post-state. Consider a non-negativity " - "invariant (count >= 0) or a correlation between count and " - "the increments mapping instead." + "increment() unconditionally adds 1 to count and 1 to " + "increments[msg.sender]. incrementOther(other) is meant " + "to credit increments[other] but the implementation looks " + "off — flag a property over its intended behavior. Three " + "safety properties total: (a) increment() bumps count " + "by 1, (b) increment() bumps increments[msg.sender] by 1, " + "(c) incrementOther(other) bumps increments[other] by 1." ), ), ), - # P3.3 — main agent resubmits with a stronger invariant name: - # "count_nonneg" (trivially true on uint256). Spawns F2.{1-3}. - _ai( - "Addressing the feedback — proposing count_nonneg instead.", - _tc( - "invariant_feedback", - inv={ - "name": "increments_sum_is_count", - "description": ( - "`count` is the sum of all values in the `increments` map" - ), - }, - ), - ), - - # F2.1 — judge, second invocation, turn 1. + # P3.2 — read draft before emitting result. _ai( - "Judge: evaluating count_nonneg.", - _tc( - "write_rough_draft", - rough_draft=( - "Sums can be reasoned about in CVL. Formal and inductive. Verdict: GOOD." - ), - ), - ), - _ai( - "Judge: reading the draft.", + "Bug analysis: re-reading the draft.", _tc("read_rough_draft"), ), - # F2.3 — GOOD verdict. Stamps state["invariant_data"]["count_nonneg"]. - _ai( - "Judge: GOOD verdict on increments_sum_is_count.", - _tc( - "result", - sort="GOOD", - explanation=( - "The invariant is inductive and formalizable." - ), - ), - ), - # P3.4 — main agent proposes second invariant. Spawns F3.{1-3}. - _ai( - "Proposing the second invariant.", - _tc( - "invariant_feedback", - inv={ - "name": "zero_address_is_zero", - "description": ( - "The zero address' `increments` value is always 0." - ), - }, - ), - ), - - # F3.1 — judge, third invocation. - _ai( - "Judge: evaluating zero_address_is_zero.", - _tc( - "write_rough_draft", - rough_draft=( - "Trivially implied by the implementation, " - "but formal and inductive. Verdict: GOOD." - ), - ), - ), - _ai( - "Judge: reading the draft.", - _tc("read_rough_draft"), - ), + # P3.3 — emit all three properties in one result call. Schema is the + # ``_AgentRoundResult`` BaseModel (composer/spec/bug.py): ``items`` is the + # property list and ``reasoning`` is a required narrative field — there + # is no ``value`` wrapper here, unlike the tuple-shaped result tools. _ai( - "Judge: GOOD verdict on zero_address_is_zero.", + "Delivering the three extracted properties.", _tc( "result", - sort="GOOD", - explanation=( - "The invariant is trivially true" + items=_BUG_ANALYSIS_PROPS, + reasoning=( + "increment() unconditionally mutates two storage slots: it " + "adds 1 to `count` and 1 to `increments[msg.sender]`. " + "incrementOther(other) is documented to credit " + "`increments[other]` by 1; whether the implementation " + "actually does that is a question for the prover. The " + "three pre/post equalities on those slots are the obvious " + "safety properties; nothing else in the contract surface " + "is worth formalizing at this stage." ), ), ), - # P3.5 — main agent delivers both invariants. Descriptions must match - # the ones in state["invariant_data"] verbatim (merged on name). - _ai( - "Delivering the validated invariants.", - _tc( - "result", - inv=[ - { - "name": "increments_sum_is_count", - "description": ( - "`count` is the sum of all values in the `increments` map" - ), - }, - { - "name": "zero_address_is_zero", - "description": ( - "The zero address' `increments` value is always 0." - ), - }, - ], - ), - ), # ─────────────────────────────────────────────────────────────────── - # P4. Invariant CVL generation (batch_cvl_generation, component=None) + # P4. Component CVL generation (batch_cvl_generation, component=) # ─────────────────────────────────────────────────────────────────── - # Author-agent tools: - # - cvl_authorship_tools (source_tools + rag_tools): list_files, - # get_file, grep_files, code_explorer, code_document_ref, - # cvl_manual_search, cvl_keyword_search, get_cvl_manual_section, - # get_cvl_recipe, cvl_research, cvl_document_ref. - # - static_tools: put_cvl, put_cvl_raw, feedback_tool, record_skip, - # unskip_property, get_cvl, erc20_guidance, unresolved_call_guidance. - # - prover_tool: verify_spec. - # - ExpectRuleFailure.as_tool("expect_rule_failure"), - # ExpectRulePassage.as_tool("expect_rule_passage"). - # - result (str commentary), memory. + # The only authoring lane, so it carries the file's whole tool coverage + # (research, guidance, skip/unskip, expect-fail/passage, the Typechecker + # rejection path) as well as the judge good=False -> revise -> good=True + # round and the surface-a-real-bug path. # - # Result digest: validations[feedback] AND validations[prover] must - # both equal digest(curr_spec, skipped) before `result` is accepted. - # feedback_tool (good=True) stamps feedback; verify_spec (rules=None, - # all_verified) stamps prover. Any put_cvl_raw / record_skip / - # unskip_property invalidates both stamps. + # 3 refined properties from P3b. # - # 2 invariants — record_skip / unskip_property accept the property titles - # `increments_sum_is_count` and `zero_address_is_zero`. + # The spec contains three rules: two that hold against the + # implementation and one (``incrementOther_credits_target_when_distinct``) + # that CEXes because ``Counter.incrementOther`` has a real bug — it + # credits ``msg.sender`` instead of ``other``. The author marks that + # rule as expected-to-fail with a reason explaining the surfaced bug, + # then re-runs the prover with the rule excluded so + # ``validations[prover]`` can be stamped. ] -_INVARIANT_CVL_TAPE: list[BaseMessage] = [ +_CVL_TAPE: list[BaseMessage] = [ + + # ── Tool coverage (Q1-Q9) ────────────────────────────────────────── + # These turns exist to exercise tool dispatch, not to advance the spec. + # They ran in the structural-invariant CVL lane until that phase was + # removed; this is now the only authoring lane, so they live here. # Q1 — exercise the similarity + keyword search paths. _ai( - "Surveying the CVL manual for invariant patterns.", + "Surveying the CVL manual for rule and invariant patterns.", _tc( "cvl_manual_search", question=( @@ -765,14 +625,15 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: _tc("get_cvl_recipe", id="R1"), ), - # Q3 — exercise the recipe miss path + both guidance tools + memory view. - # The recipe id is expected to miss — the harness only cares - # about exercising the tool dispatch, not the result value. + # Q3 — exercise the recipe miss path + all three guidance tools + memory + # view. The recipe id is expected to miss — the harness only cares about + # exercising the tool dispatch, not the result value. _ai( "Checking for a recipe and pulling guidance.", _tc("get_cvl_recipe", id="R99"), _tc("erc20_guidance"), _tc("unresolved_call_guidance"), + _tc("structural_invariant_guidance"), _tc("memory", command="view", path="/memories"), ), @@ -841,26 +702,17 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # Typechecker.jar rejects the parse and the tool returns the error text # without mutating curr_spec. _ai( - "Attempting an initial draft.", + "Drafting the component spec.", _tc("put_cvl_raw", cvl_file=BROKEN_PARSE_CVL), ), - # Q6 — put the BAD_INV_CVL. Typechecks fine — the bug is semantic - # (the invariant is false), not syntactic. Mutates state["curr_spec"] - # and resets did_read. - _ai( - "Putting an initial count_zero-style invariant.", - _tc("put_cvl_raw", cvl_file=BAD_INV_CVL), - ), - - # Q7 — exercise get_cvl + record_skip. The two invariant titles are - # `increments_sum_is_count` (1st) and `zero_address_is_zero` (2nd). + # Q6 — exercise get_cvl + record_skip against a real batch title. _ai( "Reading back the draft + recording a tentative skip.", _tc("get_cvl"), _tc( "record_skip", - property_title="increments_sum_is_count", + property_title="other_increments_by_one", reason=( "Tentative — will be undone on the next turn to exercise " "unskip_property." @@ -868,17 +720,18 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: ), ), - # Q8 — exercise unskip_property. Empty-reason sentinel in merge_skips + # Q7 — exercise unskip_property. Empty-reason sentinel in merge_skips # filters the entry out, so state["skipped"] returns to []. _ai( "Undoing the tentative skip.", - _tc("unskip_property", property_title="increments_sum_is_count"), + _tc("unskip_property", property_title="other_increments_by_one"), ), - # Q9 — exercise expect_rule_failure + expect_rule_passage. The rule - # name here needn't match any actual rule in curr_spec — both tools just - # record a rule_skips entry. `expect_rule_passage` then removes it with - # the DELETE_SKIP sentinel, so state["rule_skips"] returns to {}. + # Q8 — exercise expect_rule_failure + expect_rule_passage as a pair. The + # rule name needn't match anything in curr_spec — both tools just record a + # rule_skips entry. `expect_rule_passage` removes it with the DELETE_SKIP + # sentinel, so state["rule_skips"] returns to {} before R1 puts the real + # spec. (The load-bearing expect_rule_failure is R4, further down.) _ai( "Marking a rule expected-to-fail...", _tc( @@ -895,87 +748,31 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: _tc("expect_rule_passage", rule_name="count_zero"), ), - # Q10 — first feedback_tool invocation against BAD_INV_CVL. Spawns the - # feedback judge sub-agent (J1.{1-3}). The judge returns good=False so - # validations["feedback"] is NOT stamped. - _ai( - "Seeking judge feedback on the current (bad) draft.", - _tc("feedback_tool"), - ), - - # J1.1 — feedback judge, first invocation, turn 1. Tools: memory, - # rough_draft, get_cvl, feedback_tools (= cvl_authorship_tools), result - # (PropertyFeedback). Validator `did_rough_draft_read` rejects result - # until did_read=True. - _ai( - "Judge: gathering the spec + drafting a verdict.", - _tc("memory", command="view", path="/memories"), - _tc("get_cvl"), - _tc( - "write_rough_draft", - rough_draft=( - "First-pass: the current spec encodes `count == 0` as an " - "invariant, which directly contradicts the property that " - "increment() increases count by 1. Verdict: BAD — spec does " - "not faithfully express the two target invariants " - "(increments_sum_is_count, zero_address_is_zero)." - ), - ), - ), - - # J1.2 — judge: read the draft. - _ai( - "Judge: reading the draft before verdict.", - _tc("read_rough_draft"), - ), - - # J1.3 — judge: good=False verdict. Does NOT stamp the feedback digest. - _ai( - "Judge: delivering the first (rejecting) verdict.", - _tc( - "result", - good=False, - feedback=( - "The submitted spec states `count == 0` as an invariant " - "but the properties to formalize are `count_nonneg` and " - "`zero_address_is_zero`. Please replace the spec with " - "invariants that match the approved property list." - ), - ), - ), + # ── The component spec proper ────────────────────────────────────── - # Q11 — author addresses the feedback by replacing the spec with - # SUBTLE_INV_CVL (has the two expected invariant names but `count_nonneg` - # is subtly wrong — body says ``count > 0`` instead of ``>= 0``). - # Mutates curr_spec, resets did_read. The feedback digest stamped for - # BAD_INV_CVL (if any — here J1 returned good=False so there was no - # stamp) is now stale regardless. + # R1 — put the incomplete first draft. Typechecks, so it reaches the judge. _ai( - "Addressing the judge feedback with the two named invariants.", - _tc("put_cvl_raw", cvl_file=SUBTLE_INV_CVL), + "Writing a first pass at the component spec.", + _tc("put_cvl_raw", cvl_file=PARTIAL_COMPONENT_CVL), ), - # Q12 — second feedback_tool invocation against SUBTLE_INV_CVL. Spawns - # J2.{1-3}. The judge approves by name-coverage (both expected names - # present, both trivially typecheck) — missing the subtle `count > 0` - # semantic bug in the first invariant. good=True stamps - # validations["feedback"] = digest(SUBTLE_INV_CVL, skipped=[]). + # R2 — request feedback. Spawns J1.{1-3}. The judge returns good=False, so + # validations["feedback"] is NOT stamped and the author must revise. _ai( - "Re-running the judge on the updated draft.", + "Requesting judge feedback on the first draft.", _tc("feedback_tool"), ), - # J2.1 — feedback judge, second invocation, turn 1. + # J1.1 — feedback judge, first invocation, turn 1. _ai( - "Judge: re-evaluating the updated spec.", + "Judge: inspecting the draft.", _tc("get_cvl"), _tc( "write_rough_draft", rough_draft=( - "Second pass: the spec declares both increments_sum_is_count and " - "zero_address_is_zero as separate invariants matching the " - "approved property list. Coverage looks complete. " - "Verdict: GOOD." + "Two rules, both about increment(). Nothing addresses " + "other_increments_by_one, and it carries no skip " + "declaration. Coverage is incomplete. Verdict: NOT GOOD." ), ), ), @@ -983,220 +780,36 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: "Judge: reading the draft.", _tc("read_rough_draft"), ), - # J2.3 — good=True verdict. Stamps validations["feedback"] = - # digest(SUBTLE_INV_CVL, []). Judge did not catch the `count > 0` - # typo; the prover will. + # J1.3 — good=False. No digest stamped; the author has to come back. _ai( - "Judge: approving the spec.", + "Judge: rejecting the draft on coverage.", _tc( "result", - good=True, - feedback="", - ), - ), - - # Q13 — run verify_spec against SUBTLE_INV_CVL. The base-case check - # for `count_nonneg` fires on the initial state (count == 0), where - # the body `count > 0` is false. One rule violated → one - # ``analyze_cex_raw`` LLM call fires INSIDE verify_spec (between this - # tape entry and the next author turn). ``all_verified=False`` so - # the tool returns the raw report string; validations[prover] is NOT - # stamped. - _ai( - "Running the prover on the updated draft.", - _tc("verify_spec", rules=None), - ), - - # CEX.1 — inline counter-example analysis. ``analyze_cex_raw`` in - # ``composer/prover/analysis.py`` calls ``llm.ainvoke(messages)`` (via - # ``acached_invoke``) with a human-framed instruction template. It - # expects a plain-text AIMessage back — NO tool_calls, because the - # call bypasses the LangGraph agent loop entirely. - # - # Placement is critical: ``FakeMessagesListChatModel`` has a single - # global cursor, so this entry must sit between the verify_spec turn - # (Q13) and the next author turn (Q14). If the author reorders or - # verify_spec is invoked twice without an intervening CEX, the tape - # will drift. - _ai( - "Counter-example analysis for rule ``increments_sum_is_count``:\n\n" - "The prover found a spurious starting state where incrementsSum is initialized to be" - " non-zero in the invariant base case (constructor) which causes a trivial failure.\n\n" - "Suggested fix: add an init_state axiom to constrain the value of the ghost in the base case." - - ), - - # Q14 — author responds to the CEX by replacing SUBTLE_INV_CVL with - # GOOD_INV_CVL (uses ``>=`` instead of ``>``). Mutates curr_spec, - # invalidates validations["feedback"] (digest changes). - _ai( - "Fixing the count_nonneg operator as the CEX suggests.", - _tc("put_cvl_raw", cvl_file=GOOD_INV_CVL), - ), - - # Q15 — third feedback_tool invocation. Spawns J3.{1-3}. Digest stale - # since curr_spec changed; re-stamping is required before result. - _ai( - "Re-running the judge to re-stamp the feedback digest.", - _tc("feedback_tool"), - ), - - # J3.1 — feedback judge, third invocation, turn 1. - _ai( - "Judge: re-evaluating with the operator fix applied.", - _tc("get_cvl"), - _tc( - "write_rough_draft", - rough_draft=( - "The init state axiom is well justified given that the sum of increments is 0 on creation." - " Verdict: GOOD." - ), - ), - ), - _ai( - "Judge: reading the draft.", - _tc("read_rough_draft"), - ), - # J3.3 — good=True. Stamps validations["feedback"] = - # digest(GOOD_INV_CVL, []). - _ai( - "Judge: approving the fixed spec.", - _tc("result", good=True, feedback=""), - ), - - # Q16 — run verify_spec on GOOD_INV_CVL. Both invariants reduce to - # uint256 non-negativity and hold trivially. all_verified=True with - # rules=None → validations["prover"] stamped with - # digest(GOOD_INV_CVL, []) — same digest as feedback. - _ai( - "Running the prover on the fixed invariants.", - _tc("verify_spec", rules=None), - ), - - # Q17 — final result. Both validations current, curr_spec unchanged - # since Q14 / J3. PublishResultTool requires `commentary` plus a - # `property_rules` mapping covering every (non-skipped) batch title — - # here the two invariant titles, each verified by the invariant of the - # same name in GOOD_INV_CVL. - _ai( - "Finalizing the invariant CVL.", - _tc( - "result", - commentary=( - "Formalized the two structural invariants (increments_sum_is_count, " - "zero_address_is_zero)." - ), - property_rules=[ - {"property_title": "increments_sum_is_count", "rules": ["increments_sum_is_count"]}, - {"property_title": "zero_address_is_zero", "rules": ["zero_address_is_zero"]}, - ], - ), - ), - - # ─────────────────────────────────────────────────────────────────── - # P5. Bug analysis (run_bug_analysis, 1 component) - # ─────────────────────────────────────────────────────────────────── - # Tools available: rough_draft (via get_rough_draft_tools), - # bug_analysis_tools (= source_tools), result. - # Validator: standard bind_standard (output_key). Result schema is - # (list[PropertyFormulation], "The security properties ..."), so args - # are {"value": [...]}. - # - # `refinement` is None from the pipeline, so there is NO refinement-loop - # conversation after this — once `result` fires, the phase ends. - -] - -_BUG_TAPE: list[BaseMessage] = [ - - # P5.1 — exercise source_tools + rough_draft. No did_read requirement, - # kept for coverage. - _ai( - "Bug analysis: inspecting the entry point source.", - _tc("get_file", path="src/Counter.sol"), - _tc( - "write_rough_draft", - rough_draft=( - "increment() unconditionally adds 1 to count and 1 to " - "increments[msg.sender]. incrementOther(other) is meant " - "to credit increments[other] but the implementation looks " - "off — flag a property over its intended behavior. Three " - "safety properties total: (a) increment() bumps count " - "by 1, (b) increment() bumps increments[msg.sender] by 1, " - "(c) incrementOther(other) bumps increments[other] by 1." - ), - ), - ), - - # P5.2 — read draft before emitting result. - _ai( - "Bug analysis: re-reading the draft.", - _tc("read_rough_draft"), - ), - - # P5.3 — emit all three properties in one result call. Schema is the - # ``_AgentRoundResult`` BaseModel (composer/spec/bug.py): ``items`` is the - # property list and ``reasoning`` is a required narrative field — there - # is no ``value`` wrapper here, unlike the tuple-shaped result tools. - _ai( - "Delivering the three extracted properties.", - _tc( - "result", - items=_BUG_ANALYSIS_PROPS, - reasoning=( - "increment() unconditionally mutates two storage slots: it " - "adds 1 to `count` and 1 to `increments[msg.sender]`. " - "incrementOther(other) is documented to credit " - "`increments[other]` by 1; whether the implementation " - "actually does that is a question for the prover. The " - "three pre/post equalities on those slots are the obvious " - "safety properties; nothing else in the contract surface " - "is worth formalizing at this stage." + good=False, + feedback=( + "The property other_increments_by_one is neither formalized " + "nor skipped. Add a rule for incrementOther(address), or " + "record a skip with a justification." ), ), ), - - # ─────────────────────────────────────────────────────────────────── - # P6. Component CVL generation (batch_cvl_generation, component=) - # ─────────────────────────────────────────────────────────────────── - # Same author-agent shape as P4 but streamlined — we do not re-exercise - # every tool. Tool coverage is satisfied by P4; P6 covers the - # surface-a-real-bug path. - # - # 3 refined properties from P5b — record_skip would accept their titles, - # but the tape doesn't exercise record_skip in this phase. - # - # The spec contains three rules: two that hold against the - # implementation and one (``incrementOther_credits_target_when_distinct``) - # that CEXes because ``Counter.incrementOther`` has a real bug — it - # credits ``msg.sender`` instead of ``other``. The author marks that - # rule as expected-to-fail with a reason explaining the surfaced bug, - # then re-runs the prover with the rule excluded so - # ``validations[prover]`` can be stamped. - -] - -_CVL_TAPE: list[BaseMessage] = [ - - # R1 — put the three-rule component spec. Typechecks; covers all three - # refined props. + # R3 — author addresses the feedback with the full three-rule spec. + # Mutates curr_spec, so any prior stamp would be stale regardless. _ai( - "Writing the component spec covering all three properties.", + "Adding the missing incrementOther rule.", _tc("put_cvl_raw", cvl_file=COMPONENT_CVL), ), - # R2 — request feedback. Spawns J3.{1-3}. Judge returns good=True on - # first pass (the spec faithfully encodes all three properties; whether - # the rules pass against the implementation is the prover's question). + # R4 — second feedback round. Spawns J2.{1-3}, which approves. _ai( - "Requesting judge feedback on the component spec.", + "Requesting judge feedback on the revised spec.", _tc("feedback_tool"), ), - # J3.1 — feedback judge, single pass, turn 1. + # J2.1 — feedback judge, second invocation, turn 1. _ai( - "Judge: inspecting the component spec.", + "Judge: inspecting the revised spec.", _tc("get_cvl"), _tc( "write_rough_draft", @@ -1212,7 +825,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: "Judge: reading the draft.", _tc("read_rough_draft"), ), - # J3.3 — good=True verdict. Stamps validations["feedback"] with + # J2.3 — good=True verdict. Stamps validations["feedback"] with # digest(COMPONENT_CVL, skipped=[]). rule_skips is NOT part of the # digest, so the later expect_rule_failure won't invalidate this # stamp. @@ -1221,7 +834,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: _tc("result", good=True, feedback=""), ), - # R3 — first prover run. The two increment() rules verify; the + # R5 — first prover run. The two increment() rules verify; the # incrementOther rule CEXes (msg.sender credited instead of other). # all_verified=False → validations[prover] NOT stamped, tool returns # raw report string. Exactly ONE failing rule → exactly ONE @@ -1233,7 +846,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # CEX.2 — inline analysis of the incrementOther CEX. Plain AIMessage, # no tool_calls, mirrors the CEX.1 entry in the invariant-CVL phase. - # Critical placement: between R3 and R4 in the global tape cursor. + # Critical placement: between R5 and R6 in the global tape cursor. _ai( "Counter-example analysis for rule " "``incrementOther_credits_target_when_distinct``:\n\n" @@ -1250,7 +863,7 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: "so a human can fix the Solidity." ), - # R4 — author responds to the surfaced bug by marking the rule as + # R6 — author responds to the surfaced bug by marking the rule as # expected-to-fail. ``expect_rule_failure`` writes into ``rule_skips`` # via a Command. ``rule_skips`` is NOT part of the digest used by # validation stamps, so the prior feedback stamp remains valid. @@ -1273,11 +886,11 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: ), ), - # R5 — re-run prover. With the buggy rule in rule_skips, the + # R7 — re-run prover. With the buggy rule in rule_skips, the # all_verified loop in verify_spec ignores it; the two increment() # rules pass, so all_verified=True and rules=None → stamps # validations[prover] at digest(COMPONENT_CVL, skipped=[]), which - # matches the feedback stamp from J3.3. + # matches the feedback stamp from J2.3. _ai( "Re-running the prover with the buggy rule excluded.", _tc("verify_spec", rules=None), @@ -1298,8 +911,8 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: "so a human can fix the Solidity." ), - # R6 — final result. Both stamps current, curr_spec unchanged since - # R1. Commentary documents the surfaced bug so the downstream + # R8 — final result. Both stamps current, curr_spec unchanged since + # R3. Commentary documents the surfaced bug so the downstream # ``natspec_report`` / file-on-disk autospec output flags it for the # human reviewer. _ai( @@ -1326,19 +939,18 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # ─────────────────────────────────────────────────────────────────────────── -# P7. Report grouping (build_report → call_grouping_llm) +# P5. Report grouping (build_report → call_grouping_llm) # ─────────────────────────────────────────────────────────────────────────── # The final, best-effort phase. ``call_grouping_llm`` makes ONE structured-output # call (``llm.with_structured_output(GroupingResult)``), so this lane has exactly # one entry: an AIMessage whose ``GroupingResult`` tool call (the tool name is the # pydantic model's class name) partitions every formalized property into groups. # -# The five formalized properties this run produces (component, title): +# The three formalized properties this run produces (component, title): # ("Increment", count_increments_by_one / sender_increments_by_one / -# other_increments_by_one) + ("Structural Invariants", -# increments_sum_is_count / zero_address_is_zero). -# ``coverage.validate`` requires each appear in exactly one group, so the two -# groups below must cover all five with no overlap or omission. Without this lane +# other_increments_by_one). +# ``coverage.validate`` requires each appear in exactly one group, so the group +# below must cover all three with no overlap or omission. Without this lane # the call raised ``no tape lane``, which ``build_report`` swallows into its # fallback single-bucket grouping — so the report path ran but the grouping step # was never actually exercised. @@ -1362,18 +974,6 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: ["Increment", "other_increments_by_one"], ], }, - { - "slug": "counter-structural-invariants", - "title": "Counter state respects its structural invariants", - "description": ( - "The global counter stays consistent with the sum of the per-address " - "tallies and the zero address is never credited." - ), - "members": [ - ["Structural Invariants", "increments_sum_is_count"], - ["Structural Invariants", "zero_address_is_zero"], - ], - }, ], ), ), @@ -1383,46 +983,18 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: # ─────────────────────────────────────────────────────────────────────────── # Budget-curtailment variant lanes # ─────────────────────────────────────────────────────────────────────────── -# Alternate invariant-CVL / formalize-0 lanes for the curtailment integration -# test, which runs the pipeline with the ``formalization_preparation`` and -# ``formalization`` caps at 0.0: the budget monitor's wrap-up alert fires on the -# first tool-result tick (0 >= 0.8 * 0), lifting the validation gates and -# stamping ``budget_curtailed`` — while the hard stop never fires (taped runs -# accrue no cost, and 0 > 0 is false). Each lane therefore: puts a typechecking -# draft, skips one property "for budget", and publishes WITHOUT ever consulting -# the feedback judge or the prover — the lifted gates accept it. No judge or -# CEX entries, and no live prover run, are consumed. - -_CURTAILED_INVARIANT_CVL_TAPE: list[BaseMessage] = [ - # V1 — put a valid draft (real Typechecker.jar gatekeeps this put). - _ai( - "Drafting the structural invariants.", - _tc("put_cvl_raw", cvl_file=GOOD_INV_CVL), - ), - # The wrap-up alert lands before this turn: skip what isn't finished. - _ai( - "Budget pressure — skipping the remaining invariant and wrapping up.", - _tc( - "record_skip", - property_title="zero_address_is_zero", - reason="Budget exhausted before this invariant could be validated.", - ), - ), - # V3 — publish the partial under the lifted gates (no feedback/prover stamps). - _ai( - "Publishing the partial invariant spec.", - _tc( - "result", - commentary=( - "Budget-curtailed partial: increments_sum_is_count is drafted but " - "unverified; zero_address_is_zero was skipped." - ), - property_rules=[ - {"property_title": "increments_sum_is_count", "rules": ["increments_sum_is_count"]}, - ], - ), - ), -] +# Alternate formalize-0 lane for the curtailment integration test, which runs the +# pipeline with the ``formalization`` cap at 0.0: the budget monitor's wrap-up +# alert fires on the first tool-result tick (0 >= 0.8 * 0), lifting the +# validation gates and stamping ``budget_curtailed`` — while the hard stop never +# fires (taped runs accrue no cost, and 0 > 0 is false). The lane therefore puts +# a typechecking draft, skips one property "for budget", and publishes WITHOUT +# ever consulting the feedback judge or the prover — the lifted gates accept it. +# No judge or CEX entries, and no live prover run, are consumed. +# +# Only formalization is curtailable now: nothing under +# ``formalization_preparation`` makes an LLM call, so that cap can no longer +# trip a monitor. _CURTAILED_CVL_TAPE: list[BaseMessage] = [ # W1 — put the full three-rule draft (typechecks; never sent to the prover). @@ -1525,59 +1097,6 @@ def _ai(text: str = "", *tool_calls: ToolCall) -> AIMessage: """ -# Minimal happy-path invariant lane: the nag test doesn't re-pay the -# broken-parse / bad-draft / CEX detours the main tape covers — one judge -# round, one (passing) prover run, publish. -_NAG_INVARIANT_CVL_TAPE: list[BaseMessage] = [ - _ai( - "Drafting the structural invariants.", - _tc("put_cvl_raw", cvl_file=GOOD_INV_CVL), - ), - _ai( - "Requesting judge feedback.", - _tc("feedback_tool"), - ), - _ai( - "Judge: inspecting the spec.", - _tc("get_cvl"), - _tc( - "write_rough_draft", - rough_draft=( - "Both approved invariants (increments_sum_is_count, " - "zero_address_is_zero) are faithfully encoded, with the ghost " - "seeded by an init_state axiom. Verdict: GOOD." - ), - ), - ), - _ai( - "Judge: reading the draft.", - _tc("read_rough_draft"), - ), - _ai( - "Judge: approving the spec.", - _tc("result", good=True, feedback=""), - ), - _ai( - "Running the prover on the invariants.", - _tc("verify_spec", rules=None), - ), - _ai( - "Finalizing the invariant CVL.", - _tc( - "result", - commentary=( - "Formalized the two structural invariants " - "(increments_sum_is_count, zero_address_is_zero)." - ), - property_rules=[ - {"property_title": "increments_sum_is_count", "rules": ["increments_sum_is_count"]}, - {"property_title": "zero_address_is_zero", "rules": ["zero_address_is_zero"]}, - ], - ), - ), -] - - def _nag_attempt_spec(i: int) -> str: """The spec for streak attempt ``i`` (0-based). Attempts differ only by a trailing comment: the streak detector keys on (rule, status), so the nudge @@ -1739,8 +1258,6 @@ def _nag_streak_turns() -> list[BaseMessage]: DESIGN_DOC_DISCOVERY_TASK_ID: _DESIGN_DOC_TAPE, SYSTEM_ANALYSIS_TASK_ID: _SYSTEM_ANALYSIS_TAPE, HARNESS_TASK_ID: _HARNESS_TAPE, - INVARIANTS_TASK_ID: _INVARIANTS_TAPE, - INVARIANT_CVL_TASK_ID: _INVARIANT_CVL_TAPE, extract_task_id(0): _BUG_TAPE, formalize_task_id(0): _CVL_TAPE, REPORT_TASK_ID: _REPORT_TAPE, @@ -1755,8 +1272,6 @@ def _nag_streak_turns() -> list[BaseMessage]: DESIGN_DOC_DISCOVERY_TASK_ID: _DESIGN_DOC_TAPE, SYSTEM_ANALYSIS_TASK_ID: _SYSTEM_ANALYSIS_TAPE, HARNESS_TASK_ID: _HARNESS_TAPE, - INVARIANTS_TASK_ID: _INVARIANTS_TAPE, - INVARIANT_CVL_TASK_ID: _CURTAILED_INVARIANT_CVL_TAPE, extract_task_id(0): _BUG_TAPE, formalize_task_id(0): _CURTAILED_CVL_TAPE, } @@ -1769,8 +1284,6 @@ def _nag_streak_turns() -> list[BaseMessage]: DESIGN_DOC_DISCOVERY_TASK_ID: _DESIGN_DOC_TAPE, SYSTEM_ANALYSIS_TASK_ID: _SYSTEM_ANALYSIS_TAPE, HARNESS_TASK_ID: _HARNESS_TAPE, - INVARIANTS_TASK_ID: _INVARIANTS_TAPE, - INVARIANT_CVL_TASK_ID: _NAG_INVARIANT_CVL_TAPE, extract_task_id(0): _BUG_TAPE, formalize_task_id(0): _NAG_CVL_TAPE, REPORT_TASK_ID: _REPORT_TAPE, @@ -1846,13 +1359,11 @@ def install_nag_tape( __all__ = [ - "BAD_INV_CVL", "BROKEN_PARSE_CVL", "COMPONENT_CVL", - "GOOD_INV_CVL", + "PARTIAL_COMPONENT_CVL", "NAG_COMPONENT_CVL", "NAG_STUCK_RULE", - "SUBTLE_INV_CVL", "autoprove_nag_lanes", "get_autoprove_Counter_llm", "get_autoprove_Counter_curtailment_llm", @@ -1863,7 +1374,7 @@ def install_nag_tape( # --------------------------------------------------------------------------- -# Operator notes for the interactive refinement conversation (P5b) +# Operator notes for the interactive refinement conversation (P3b) # --------------------------------------------------------------------------- # # The refinement conversation kicks in only when the auto-prove pipeline is @@ -1875,7 +1386,7 @@ def install_nag_tape( # property 3 — I want to make sure it's right. # # (Or any prompt that asks the AI to discuss the properties; the AI's -# scripted P5b.1 response presupposes a question along those lines.) +# scripted P3b.1 response presupposes a question along those lines.) # # Subsequent human turns have ``[TAPE EXPECTATION: respond '...']`` markers # embedded in the preceding AI message — type those verbatim to advance the diff --git a/composer/ui/autoprove_app.py b/composer/ui/autoprove_app.py index 5adae686..d42bca45 100644 --- a/composer/ui/autoprove_app.py +++ b/composer/ui/autoprove_app.py @@ -40,7 +40,6 @@ class AutoProvePhase(enum.Enum): DISCOVER_DESIGN_DOC = "discover_design_doc" HARNESS = "harness" AUTOSETUP = "autosetup" - INVARIANTS = "invariants" SUMMARIES = "summaries" COMPONENT_ANALYSIS = "component_analysis" BUG_ANALYSIS = "bug_analysis" @@ -52,7 +51,6 @@ class AutoProvePhase(enum.Enum): AutoProvePhase.DISCOVER_DESIGN_DOC: "Design Doc Discovery", AutoProvePhase.HARNESS: "Harness Creation", AutoProvePhase.AUTOSETUP: "AutoSetup", - AutoProvePhase.INVARIANTS: "Structural Invariants", AutoProvePhase.SUMMARIES: "Summaries", AutoProvePhase.COMPONENT_ANALYSIS: "Component Analysis", AutoProvePhase.BUG_ANALYSIS: "Property Extraction", @@ -64,7 +62,6 @@ class AutoProvePhase(enum.Enum): "Design Doc Discovery", "Harness Creation", "AutoSetup", - "Structural Invariants", "Summaries", "Component Analysis", "Property Extraction", diff --git a/composer/ui/autoprove_live.py b/composer/ui/autoprove_live.py index bb80ad34..658318ac 100644 --- a/composer/ui/autoprove_live.py +++ b/composer/ui/autoprove_live.py @@ -167,9 +167,9 @@ async def make_handler( self, info: TaskInfo[AutoProvePhase] ) -> TaskHandle[None]: # ``run_task`` fires ``on_start`` / ``on_done`` per-task, not - # per-phase — a single phase like CVL_GEN spawns one - # "Invariant CVL" task plus one per-component batch, all - # sharing the same ``AutoProvePhase``. Use ``_phases_seen`` to + # per-phase — a single phase like CVL_GEN spawns one task per + # component batch, all sharing the same ``AutoProvePhase``. + # Use ``_phases_seen`` to # collapse the per-task callback into a single phase header # emitted the first time any task of that phase actually starts # work. Subsequent tasks in the same phase don't repeat it. diff --git a/docs/application-abstraction.md b/docs/application-abstraction.md index 816d108c..aa1135a6 100644 --- a/docs/application-abstraction.md +++ b/docs/application-abstraction.md @@ -147,7 +147,6 @@ class AutoProvePhase(enum.Enum): DISCOVER_DESIGN_DOC = "discover_design_doc" HARNESS = "harness" AUTOSETUP = "autosetup" - INVARIANTS = "invariants" SUMMARIES = "summaries" COMPONENT_ANALYSIS = "component_analysis" BUG_ANALYSIS = "bug_analysis" @@ -187,14 +186,15 @@ The phase serves two roles: ] ``` - A phase may be absent from the labels (foundry's `REPORT` is): the label map drives *sections*, - so an unlabelled phase simply gets no section of its own. + A phase must be labelled: `MultiJobApp` looks the label up by subscript, so an unlabelled phase + raises `KeyError` when its first task starts. (Foundry's `REPORT` has no label — a latent bug in + the foundry TUI, not a supported way to hide a section. Delete a phase and its label together.) - **The driver ↔ backend contract.** The shared driver tags four *core* phases; the backend maps its own enum onto them via `CorePhases[P]` (see §6). Note the two enums - above differ in granularity: foundry has five phases, autoprove has nine — the - prover contributes several extra prep phases (harness, autosetup, summaries, - invariants) that the driver never knows about. The enum is the application's own + above differ in granularity: foundry has five phases, autoprove has eight — the + prover contributes several extra prep phases (harness, autosetup, summaries) + that the driver never knows about. The enum is the application's own vocabulary; only the four core slots are shared. --- @@ -356,7 +356,7 @@ of the contrast: | `FormT` | `GeneratedCVL` | `GeneratedFoundryTest` | | `preflight` | none | none (a building backend — Crucible — puts its build here, overlapping analysis) | | `prepare_system` | harness lift + build prover tool | identity (`main_instance` only) | -| `prepare_formalization` | AutoSetup ∥ summaries ∥ invariants fan-out | trivial (formalizer already built) | +| `prepare_formalization` | AutoSetup, then custom summaries | trivial (formalizer already built) | | `formalize` | author CVL, run prover, revise on CEX | author `.t.sol`, run `forge test` | | `backend_guidance` | `CERTORA_BACKEND_GUIDANCE` | `FOUNDRY_BACKEND_GUIDANCE` | diff --git a/docs/formalization-abstraction.md b/docs/formalization-abstraction.md index 385c8751..1eb70759 100644 --- a/docs/formalization-abstraction.md +++ b/docs/formalization-abstraction.md @@ -91,7 +91,7 @@ report = await build_report(..., fetch_verdicts=formalizer.fetch_verdicts) The key structural point is the two overlaps, and both fall out of the driver generically. For the CVL backend, launching `prepare_formalization` before awaiting extraction is what overlaps the slow -AutoSetup / summary / structural-invariant work with per-component property inference — so Foundry +AutoSetup / summary work with per-component property inference — so Foundry gets the same overlap with zero extra code. `preflight` is the earlier peer, for pre-work that needs *nothing at all* from the run: Crucible @@ -149,7 +149,6 @@ class Formalizer[FormT: BackendResult, U: FeatureUnit](ABC): @abstractmethod async def fetch_verdicts(self, inp: ReportComponentInput[FormT]) -> dict[RuleName, Verdict]: ... - def extra_report_inputs(self) -> list[ReportComponentInput[FormT]]: return [] # synthetic report rows; default none async def finalize(self, outcomes, run) -> None: @@ -198,8 +197,9 @@ class StagedFormalizer[FormT: BackendResult, U: FeatureUnit](ABC): Which of the two a backend returns is its own declared signature, so a backend with no shared artifact never mentions staging at all. The prover is one of those: its shared peer -(`invariants.spec`) is produced inside `prepare_formalization` (§4.2), because the invariants are -formulated from the *model*, not from the extracted properties. +The prover is not one of those backends: its units share only AutoSetup's config and summaries, +which are not authored from anyone's properties. The one `StagedFormalizer` in the tree is +Rust/Crucible's. ### 3.4 The outcome types the driver produces @@ -284,61 +284,39 @@ the shared `verify_spec` prover tool once, and packages everything the next phas an immutable `ProverPrepared`. (Foundry's `prepare_system` is an identity transform — no harness, no tool.) -### 4.2 `prepare_formalization` — the concurrent setup fan-out +### 4.2 `prepare_formalization` — the pre-formalization setup -This is where the CVL backend does its expensive pre-work, and it is the richest method in -the abstraction. From `ProverPrepared` in [pipeline.py](../composer/spec/source/pipeline.py): +This is where the CVL backend does its pre-work. From `ProverPrepared` in +[pipeline.py](../composer/spec/source/pipeline.py): ```python async def prepare_formalization(self, run) -> 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( - self._autosetup(run), self._invariants(run), - ) - - invariant = None - if invariants.inv: - inv_props = [PropertyFormulation(title=inv.name, description=inv.description, sort="invariant") - for inv in invariants.inv] - self._store.write_properties(InvariantSpec(), inv_props) - - # Generate invariants.spec ONCE, with cache short-circuit - inv_cvl_ctx = run.ctx.child(INV_CVL_KEY) - cached = await inv_cvl_ctx.cache_get(GeneratedCVL) - if cached is not None: - inv_cvl = cached - else: - inv_result = await run.runner(TaskInfo(INVARIANT_CVL_TASK_ID, ...), - lambda: batch_cvl_generation(inv_cvl_ctx.abstract(CVLGeneration), - setup_config.prover_config, inv_props, None, resources, self._prover_tool, ...)) - if isinstance(inv_result, GaveUp): - raise RuntimeError(f"Structural invariant CVL generation gave up: {inv_result.reason}") - inv_cvl = inv_result - await inv_cvl_ctx.cache_put(inv_cvl) - - inv_path = self._store.write_artifact(InvariantSpec(), inv_cvl) - # Append invariants.spec to the resource set so EVERY per-component spec imports it. - resources = [*resources, CVLResource(path=inv_path, required=False, - description="Structural invariants that may be assumed as preconditions", sort="import")] - invariant = (inv_props, Delivered(inv_cvl, inv_path)) - - return ProverRunner(GeneratedCVL, "prover", self._store, self._prover_tool, - setup_config.prover_config, resources, invariant, make_prover_fetcher()) + setup_config = await run.runner(TaskInfo(AUTOSETUP_TASK_ID, ...), + lambda: run_autosetup_phase(run.ctx, run.source, self._sys_desc, self._analyzed, ...)) + resources = [CVLResource(path=certora_relative_to_project(setup_config.summaries_path), + required=True, description="AutoSetup-generated summaries", sort="import")] + + # The custom summaries build on AutoSetup's config, so they follow it rather than + # running alongside it. + if self._sys_desc.erc20_contracts or self._sys_desc.external_interfaces: + resources.append(await run.runner(TaskInfo(SUMMARIES_TASK_ID, ...), + lambda: setup_summaries(ctx=run.ctx, app=self._harnessed, ...))) + + return ProverRunner(GeneratedCVL, "prover", self._prover_tool, + setup_config.prover_config, resources, make_prover_fetcher(), self._deps) ``` -Three things worth calling out: +Two things worth calling out: -- **Concurrency inside the method.** AutoSetup+summaries and invariant *formulation* are - independent, so they `gather`. This nests under the driver-level overlap (this whole - method already runs concurrently with property extraction). -- **Structural invariants are formalized eagerly, here, not per-component.** They are - generated once into `invariants.spec`, then injected into `resources` so every later - per-component spec can `import` them as preconditions. The invariant CVL goes through the - exact same `batch_cvl_generation` path that components do (with `component=None`). -- **The returned `ProverRunner` is fully loaded.** Its config, resource set (now including - `invariants.spec`), prover tool, and the in-memory invariant result are all constructor - fields. `formalize` adds nothing — it only *reads* them. +- **No authoring agent runs here.** This method is joined at a barrier before any component is + formalized, so everything in it delays every property in the run. It used to also formulate + structural invariants and prove them into a shared `invariants.spec` — a full + `batch_cvl_generation` with real prover jobs ahead of the barrier, which on a real contract + was hours. An invariant is now authored by the component that needs one, in that component's + own spec, and proven in the same `verify_spec` run as the rule citing it. The barrier itself + stays: `batch_cvl_generation` is constructed with AutoSetup's `prover_config`. +- **The returned `ProverRunner` is fully loaded.** Its config, resource set and prover tool are + all constructor fields. `formalize` adds nothing — it only *reads* them. ### 4.3 `formalize` — per-component authoring + verification loop @@ -441,23 +419,6 @@ point — `batch_cvl_generation`, `batch_foundry_test_generation`, [`run_session`](../composer/rustapp/session.py). They differ in exactly the parameters the core takes, so collapsing them into one function would buy nothing. -### 4.4 `extra_report_inputs` — folding in the invariants - -Per-component outcomes are assembled by the driver. The structural invariants are a -*synthetic* component the backend contributes ([pipeline.py](../composer/spec/source/pipeline.py)): - -```python -def extra_report_inputs(self) -> list[ReportComponentInput[GeneratedCVL]]: - if self._invariant is None: - return [] - inv_props, inv = self._invariant - return [ReportComponentInput(name="Structural Invariants", props=inv_props, formalized=inv)] -``` - -This is the report-side payoff of formalizing invariants in `prepare_formalization`: the -in-memory `Delivered[GeneratedCVL]` is replayed straight into the report with no special -casing in the driver. - ### 4.5 `fetch_verdicts` — pass/fail per rule ```python @@ -468,7 +429,7 @@ async def fetch_verdicts(self, inp) -> dict[RuleName, Verdict]: The fetcher resolves each spec's prover run (via `inp.formalized.run_link`) and rolls per-rule outcomes into `Verdict`s. The `collect` step ([report/collect.py](../composer/spec/source/report/collect.py)) then keys rules by -`(unit_file, name)` so a structural invariant imported into several component specs collapses +`(unit_file, name)` so one definition seen through several runs collapses to one entry, and uses `Verdict.merge` (priority `BAD > ERROR > TIMEOUT > UNKNOWN > GOOD`) to roll up multiple results for one rule. Foundry's fetcher instead reads pass/fail straight off the result with no run service — same protocol, different source. @@ -479,8 +440,6 @@ the result with no run service — same protocol, different source. async def finalize(self, outcomes, run) -> None: runs = {ComponentSpec(o.feat.slugified_name).run_key: o.result.run_link for o in outcomes if isinstance(o.result, Delivered) and o.result.run_link} - if self._invariant and self._invariant[1].run_link: - runs[InvariantSpec().run_key] = self._invariant[1].run_link self._store.write_component_runs(runs) # → components_to_prover_runs.json ``` @@ -560,11 +519,6 @@ class ComponentSpec: # autospec_.spec def stem(self): return f"autospec_{self.slug}" @property def run_key(self): return self.slug - -@dataclass(frozen=True) -class InvariantSpec: # invariants.spec - @property - def stem(self): return "invariants" ``` `ProverBackend.to_artifact_id(component)` maps a component instance to its `ComponentSpec`; @@ -574,7 +528,6 @@ The resulting on-disk layout (all under the project's `certora/`): ``` certora/specs/autospec_.spec # per-component CVL -certora/specs/invariants.spec # structural invariants (imported by the above) certora/confs/.conf # prover config per spec certora/properties/.properties.json # inferred properties certora/properties/.property_rules.json # property → [rule names] @@ -610,8 +563,7 @@ The cache key is the hash of the *property batch* (`_batch_cache_key`), under th context, under the `properties` context — the hierarchical scheme described in [ARCHITECTURE.md §7](../ARCHITECTURE.md). Because the result type carries `config` and `final_link`, a cache hit can rebuild the `.conf` and keep the run link without touching the -prover. The structural-invariant CVL has its own cache short-circuit inside -`prepare_formalization` (`INV_CVL_KEY`, §4.2) for the same reason. +prover. --- @@ -623,12 +575,11 @@ The abstraction encodes three distinct failure modes, each handled differently: |---|---|---| | Agent declines a component | `formalize` returns `GaveUp(reason)` | recorded as a `ComponentOutcome`, surfaced in `failures`, rendered in report as a gap; **not cached** | | Component crashes | `formalize` raises | `asyncio.gather(..., return_exceptions=True)` captures it into `ComponentOutcome.result` | -| Invariant CVL gives up | `prepare_formalization` raises `RuntimeError` | **fatal** — invariants are a shared precondition, so the whole run aborts | | Report build fails | exception in `build_report` | best-effort: logged, run still succeeds — unless `report_build.RERAISE_REPORT_FAILURES` is set, which tests flip to make a silent report failure fail loudly | -The asymmetry is intentional: a single component giving up is a normal, reportable outcome, -but the shared invariant spec failing would silently weaken every downstream component, so it -fails loud. +A component giving up is a normal, reportable outcome. The one remaining way +`prepare_formalization` kills a run is AutoSetup itself failing — without a `prover_config` +there is nothing for any component to verify against. --- @@ -644,11 +595,10 @@ system analysis, property extraction, caching, and the report, and contributes o | `FormT` | `GeneratedCVL` | `GeneratedFoundryTest` | | `preflight` | none (its pre-work needs the harnessed model) | none (`forge` builds the project already) | | `prepare_system` | harness lift + prover tool | identity | -| `prepare_formalization` | AutoSetup ∥ summaries ∥ invariants | trivial (pre-built formalizer) | -| shared artifact (`StagedFormalizer`) | none — `invariants.spec` is built from the model, in `prepare_formalization` | none | +| `prepare_formalization` | AutoSetup, then custom summaries | trivial (pre-built formalizer) | +| shared artifact (`StagedFormalizer`) | none — units share only AutoSetup's config and summaries | none | | `formalize` | authoring session, gated by `verify_spec` | authoring session, gated by `forge_test` | | `fetch_verdicts` | query prover output off-thread | read ran/expected tests off the result | -| `extra_report_inputs` | synthetic "Structural Invariants" | none | | `finalize` | `components_to_prover_runs.json` | none | | artifact bundle | `.spec` + `.conf` | `.t.sol` + metadata | @@ -666,8 +616,7 @@ A backend author's checklist: 4. Implement `PreparedSystem.prepare_formalization` returning a fully-constructed `Formalizer` — or, if every unit builds on one shared artifact, a `StagedFormalizer` whose `begin` authors it from the union of all units' properties (§3.3). -5. Implement `Formalizer.formalize` + `fetch_verdicts`; override `extra_report_inputs` / - `finalize` only if needed. `formalize` should assemble the shared authoring session (§4.3.1) +5. Implement `Formalizer.formalize` + `fetch_verdicts`; override `finalize` only if needed. `formalize` should assemble the shared authoring session (§4.3.1) rather than grow its own loop — what it supplies is the gate tools, the prompts, and its own noun for a check. @@ -688,10 +637,9 @@ _entry_point → cli_pipeline → cont(env, ProverBackend, EVM) get_prover_tool ─▶ verify_spec tool ▶ ProverPrepared(main=located main contract, ...) 3. ┌ create_task: ProverPrepared.prepare_formalization - │ gather( _autosetup → (config, [summaries]) , _invariants → [BaseInvariant] ) - │ batch_cvl_generation(component=None) ─▶ invariants.spec (cached under INV_CVL_KEY) - │ resources += invariants.spec - │ ▶ ProverRunner(config, resources, invariant, fetch) + │ run_autosetup_phase → (config, [summaries resource]) + │ setup_summaries (only when the system has erc20s/external interfaces) + │ ▶ ProverRunner(config, resources, fetch) └ _extract_all ─▶ [ _Batch(component, props) , ... ] # runs concurrently with the above 4. for each batch (parallel, semaphore-bounded): write_properties(ComponentSpec(slug), props) @@ -705,7 +653,7 @@ _entry_point → cli_pipeline → cont(env, ProverBackend, EVM) write_artifact ─▶ autospec_.spec (+ .conf) ⇒ Delivered(result, path) ─▶ ComponentOutcome ProverRunner.finalize(outcomes) ─▶ components_to_prover_runs.json - 5. build_report( per-component inputs + extra_report_inputs(), + 5. build_report( per-component inputs, fetch_verdicts=ProverRunner.fetch_verdicts ) ─▶ certora/ap_report/report.json ``` diff --git a/source_edits_integration.md b/source_edits_integration.md index 28cc07f4..5534ec6e 100644 --- a/source_edits_integration.md +++ b/source_edits_integration.md @@ -51,10 +51,11 @@ The new top-level field: Record semantics: - A component appears **iff it delivered a result and at least one edit was - applied**. Un-edited components, gave-up components, and the synthetic - "Structural Invariants" entry never appear — the structural-invariant phase runs - with editing denied by design, so its outcomes are always about the on-disk - source. Foundry-backend reports never carry entries. + applied**. Un-edited and gave-up components never appear. Foundry-backend reports + never carry entries. +- An invariant a component authored to support one of its own properties is covered by + that component's edit record, so it is established against exactly the source that + component's rules were proven against. - `applied_edits` lists every edit that survived to the final working copy, in the order they were applied. `executive_summary` and `why_sound` are free prose from the editor; the reference renderer treats both as markdown. diff --git a/template_manifest.json b/template_manifest.json index a3570e41..9b11e4f1 100644 --- a/template_manifest.json +++ b/template_manifest.json @@ -149,12 +149,6 @@ "template_name": "property_generation_prompt.j2", "ty_sort": "TypedTemplate" }, - "composer.spec.source.author:_PropertyGenSysTemplate": { - "module": "composer.spec.source.author", - "qualname": "_PropertyGenSysTemplate", - "template_name": "property_generation_system_prompt.j2", - "ty_sort": "TypedTemplate" - }, "composer.spec.source.design_doc_finder:_FINDER_PROMPT": { "module": "composer.spec.source.design_doc_finder", "qualname": "_FINDER_PROMPT", @@ -191,12 +185,6 @@ "template_name": "autoprove_report.html.j2", "ty_sort": "TypedTemplate" }, - "composer.spec.source.struct_invariant:_typed_invariant_prompt": { - "module": "composer.spec.source.struct_invariant", - "qualname": "_typed_invariant_prompt", - "template_name": "structural_invariant_prompt.j2", - "ty_sort": "TypedTemplate" - }, "composer.spec.source.summarizer:_SummarizationTemplate": { "module": "composer.spec.source.summarizer", "qualname": "_SummarizationTemplate", diff --git a/test_scenarios/autoprove_counter/src/Counter.sol b/test_scenarios/autoprove_counter/src/Counter.sol index 8a449004..e68a589e 100644 --- a/test_scenarios/autoprove_counter/src/Counter.sol +++ b/test_scenarios/autoprove_counter/src/Counter.sol @@ -15,9 +15,8 @@ contract Counter { /// global ``count`` and the per-address tally for the *target* address. /// /// BUG: the implementation credits ``msg.sender`` instead of ``other``. - /// The structural invariant ``count == sum(increments)`` still holds - /// (both sides grow by exactly 1) and ``increments[address(0)]`` is - /// never written, so the structural-invariant phase still verifies. + /// The relationship ``count == sum(increments)`` still holds (both sides + /// grow by exactly 1) and ``increments[address(0)]`` is never written. /// The per-method correctness rule for ``incrementOther`` is what /// surfaces this bug. function incrementOther(address other) external { diff --git a/tests/test_autoprove_report.py b/tests/test_autoprove_report.py index 542a9d49..833c92c3 100644 --- a/tests/test_autoprove_report.py +++ b/tests/test_autoprove_report.py @@ -299,21 +299,27 @@ async def test_collect_falls_back_to_input_spec_when_verdict_has_no_source(): @pytest.mark.asyncio -async def test_collect_shared_rule_dedupes_and_is_referenced_by_both(): - """An invariant imported into a component spec reports the same source file from - both runs, so it collapses to one rule that both components' properties reference.""" - comp = _input("Increment", "autospec_Increment.spec", [_prop("c", "component view", sort="invariant")], - _gen({"c": ["countEqualsSum"]}, link="Lc")) - inv = _input("Structural Invariants", "invariants.spec", [_prop("i", "structural", sort="invariant")], - _gen({"i": ["countEqualsSum"]}, link="Li")) - fetch = _fetcher({ - "Lc": [_fake_check("countEqualsSum", NodeStatus.VERIFIED, file="invariants.spec")], - "Li": [_fake_check("countEqualsSum", NodeStatus.VERIFIED, file="invariants.spec")], - }) - properties, rules, *_ = await collect([comp, inv], fetch_verdicts=fetch) - ces = [r for r in rules if r.name == "countEqualsSum"] - assert len(ces) == 1 and ces[0].spec_file == "invariants.spec" - assert all(p.rule_refs == [("invariants.spec", "countEqualsSum")] for p in properties) +async def test_collect_keeps_a_supporting_invariant_the_property_names(): + """An author that needs an invariant proves it in its own component spec and names it in + ``property_rules`` alongside the rule it supports. Both must survive collection: ``collect`` + keeps only rules some property references and counts the rest as orphans, so an unnamed + invariant would be proved and then silently dropped from the report.""" + comp = _input( + "Increment", "autospec_Increment.spec", [_prop("c", "count tracks the tally")], + _gen({"c": ["increment_increases_count", "countEqualsSum"]}, link="Lc"), + ) + fetch = _fetcher({"Lc": [ + _fake_check("increment_increases_count", NodeStatus.VERIFIED), + _fake_check("countEqualsSum", NodeStatus.VERIFIED), + ]}) + properties, rules, *rest = await collect([comp], fetch_verdicts=fetch) + dropped_orphans = rest[-1] + assert {r.name for r in rules} == {"increment_increases_count", "countEqualsSum"} + assert properties[0].rule_refs == [ + ("autospec_Increment.spec", "increment_increases_count"), + ("autospec_Increment.spec", "countEqualsSum"), + ] + assert dropped_orphans == 0 @pytest.mark.asyncio diff --git a/tests/test_focus_exits.py b/tests/test_focus_exits.py index 7daba0b9..d09a899d 100644 --- a/tests/test_focus_exits.py +++ b/tests/test_focus_exits.py @@ -65,14 +65,15 @@ async def _skip(scope: SkipScope, title: str, *, curtailed: bool = False) -> str def _direct(protected): - """The editing branch builds the pair with ``skip_tools`` (spec/source/author.py).""" + """The CVL author builds the pair with ``skip_tools`` (spec/source/author.py).""" return skip_tools(TITLES, skip_description="d", skip_reason="r", protected=protected) def _via_property_tools(protected): - """The non-editing branch reaches the same pair through ``property_tools`` - (spec/cvl_generation.py). Both must honour the protection, or the ban depends on which - branch happened to build the suite.""" + """The natspec author reaches the same pair through ``property_tools`` + (spec/cvl_generation.py). It passes no ``protected`` today — a focus is a prover-run + concept — but the two routes must not diverge on whether they honour one, or a + protection wired into a single route is silently bypassable from the other.""" from composer.spec.cvl_generation import property_tools class _Services: diff --git a/tests/test_pipeline_staged_formalizer.py b/tests/test_pipeline_staged_formalizer.py index c9c42161..89d82e81 100644 --- a/tests/test_pipeline_staged_formalizer.py +++ b/tests/test_pipeline_staged_formalizer.py @@ -70,7 +70,6 @@ async def formalize(self, _label, feat, props, _ctx, _run, _extra_tools): self.calls.append((f"formalize:{feat.display_name}", [p.title for p in props])) return _Result() - def extra_report_inputs(self): return [] def findings_evidence(self): return None async def fetch_verdicts(self, _inp): return {} async def finalize(self, _outcomes, _run): return None @@ -329,8 +328,8 @@ def test_an_unmapped_focus_property_does_not_satisfy_the_focus(): async def test_ranking_does_not_wait_for_pre_formalization(monkeypatch): """The ranking reads nothing ``prepare_formalization`` produces, so it must not queue - behind it. On a real contract that setup is hours of autosetup and invariant proving, and - the focus is knowable the moment extraction lands.""" + behind it. On a real contract that setup is a full AutoSetup build, and the focus is + knowable the moment extraction lands.""" order: list[str] = [] started = asyncio.Event() release = asyncio.Event() diff --git a/tests/test_prover_nag_integration.py b/tests/test_prover_nag_integration.py index f9ad68d0..ced5280c 100644 --- a/tests/test_prover_nag_integration.py +++ b/tests/test_prover_nag_integration.py @@ -75,8 +75,8 @@ async def _fake_run_prover( calls through (the same seam the ``certora_prover`` conftest fixture patches). Parses the conf the tool just wrote, reads the spec it verifies, and reports every declared rule/invariant VERIFIED except the permanently - stuck ``NAG_STUCK_RULE`` → SANITY_FAILED. Content-derived, so both - authoring lanes are served without ordering assumptions.""" + stuck ``NAG_STUCK_RULE`` → SANITY_FAILED. Content-derived, so the + authoring lane is served without ordering assumptions.""" conf = conf_of_prover_call(folder, args) spec_text = spec_of_prover_conf(folder, conf) statuses: dict[RulePath, StatusCodes] = { diff --git a/tests/test_prover_prepare_formalization.py b/tests/test_prover_prepare_formalization.py new file mode 100644 index 00000000..258a5d84 --- /dev/null +++ b/tests/test_prover_prepare_formalization.py @@ -0,0 +1,111 @@ +"""The prover backend's pre-formalization step: what it runs, and what it does NOT. + +``prepare_formalization`` is spawned as a bare task and joined at the barrier in +``composer/pipeline/core.py`` before any component is formalized, so whatever runs inside it +delays every property in the run. It is AutoSetup, then the custom summaries built on AutoSetup's +config — and nothing else. In particular no authoring agent runs here: structural invariants used +to be formulated and proven at this point, which put a full ``batch_cvl_generation`` (real prover +jobs) ahead of the barrier. Invariants are now written by the component author that needs one. + +Stubs throughout — no LLM, no prover, no subprocess. +""" + +from dataclasses import dataclass +from types import SimpleNamespace + +import pytest + +import composer.spec.source.pipeline as pipeline +from composer.io.multi_job import TaskInfo +from composer.spec.source.autosetup import SetupSuccess +from composer.spec.source.task_ids import AUTOSETUP_TASK_ID, SUMMARIES_TASK_ID +from composer.spec.gen_types import CVLResource +from composer.ui.autoprove_app import AutoProvePhase + +pytestmark = pytest.mark.asyncio + +SUMMARIES_PATH = "specs/summaries/Counter.spec" + +SETUP = SetupSuccess( + prover_config={"files": ["src/Counter.sol"]}, + summaries_path=SUMMARIES_PATH, + user_types=[], +) + + +@dataclass +class _Run: + """Just enough ``PipelineRun``: a runner that awaits the thunk inline and records the + ``TaskInfo`` it was handed.""" + seen: list[TaskInfo] + + ctx = None + env = None + source = SimpleNamespace(contract_name="Counter", project_root="/tmp/proj") + + async def runner(self, task_info, job=None): + self.seen.append(task_info) + return await (job or task_info)() + + +def _prepared(*, erc20s: bool) -> pipeline.ProverPrepared: + sys_desc = SimpleNamespace( + erc20_contracts=["Token"] if erc20s else [], + external_interfaces=[], + ) + return pipeline.ProverPrepared( + main=None, + _sys_desc=sys_desc, + _harnessed=None, + _prover_tool=None, + _analyzed=None, + _deps=pipeline._ProverPipelineDeps( + prover_options=None, store=None, analysis_store=None, editing=None, + ), + ) + + +@pytest.fixture +def stub_setup(monkeypatch): + async def _autosetup(*_a, **_kw): + return SETUP + + async def _summaries(**_kw): + return CVLResource( + path="certora/specs/custom_summaries.spec", required=True, + description="Custom summaries", sort="import", + ) + + monkeypatch.setattr(pipeline, "run_autosetup_phase", _autosetup) + monkeypatch.setattr(pipeline, "setup_summaries", _summaries) + # ContractSetup validates a real SystemDescriptionHarnessed; it only carries config + # through to the (stubbed) summaries agent, and this test is about task ordering. + monkeypatch.setattr(pipeline, "ContractSetup", lambda **kw: SimpleNamespace(**kw)) + + +async def test_only_autosetup_runs_before_the_barrier(stub_setup): + run = _Run(seen=[]) + await _prepared(erc20s=False).prepare_formalization(run) + assert [t.task_id for t in run.seen] == [AUTOSETUP_TASK_ID] + + +async def test_custom_summaries_follow_autosetup_when_the_system_needs_them(stub_setup): + run = _Run(seen=[]) + await _prepared(erc20s=True).prepare_formalization(run) + # Summaries are second, not concurrent: they consume AutoSetup's config. + assert [t.task_id for t in run.seen] == [AUTOSETUP_TASK_ID, SUMMARIES_TASK_ID] + + +async def test_no_authoring_agent_runs_before_the_barrier(stub_setup): + """The point of the change. A CVL_GEN task here is one every component waits behind.""" + run = _Run(seen=[]) + await _prepared(erc20s=True).prepare_formalization(run) + assert not [t for t in run.seen if t.phase is AutoProvePhase.CVL_GEN] + + +async def test_the_formalizer_carries_only_the_setup_resources(stub_setup): + """No ``invariants.spec`` is folded into the resource set any more, so nothing a component + spec imports depends on work done ahead of it.""" + formalizer = await _prepared(erc20s=False).prepare_formalization(_Run(seen=[])) + assert [str(r.path) for r in formalizer._resources] == [f"certora/{SUMMARIES_PATH}"] + assert formalizer._prover_config == SETUP.prover_config diff --git a/tests/test_publish_mapping_gate.py b/tests/test_publish_mapping_gate.py new file mode 100644 index 00000000..6c770289 --- /dev/null +++ b/tests/test_publish_mapping_gate.py @@ -0,0 +1,104 @@ +"""``PublishResultTool``'s mapping gate, driven through the tool itself. + +The report keeps only rules that some property's ``property_rules`` names and counts the rest as +orphans (``report/collect.py``). So an invariant the author proved to support one of its own rules +is invisible in the report unless the author maps it. The gate closes that: the tool reads what the +typechecker declared out of the run that satisfied the publish stamp, and checks the mapping +against it in both directions. + +The state is assembled by hand rather than by running the author graph — these tests are about the +gate's decision, not about how the state got there. +""" + +import pytest + +from composer.authoring.state import spec_digest +from composer.spec.source.author import PublishResultTool +from composer.spec.cvl_generation import PropertyRuleMapping +from composer.spec.types import PropertyTitle +from composer.spec.source.report.schema import RuleName + +pytestmark = pytest.mark.asyncio + +SPEC = "rule a() { assert true; }\ninvariant b() true;\n" +TITLES = [PropertyTitle("p1")] + + +def _state(declared: list[str] | None, *, spec: str = SPEC) -> dict: + """An authoring state whose publish gate is already satisfied. ``declared`` None means no + prover run covered this spec — the shape a budget wrap-up publishes in, since it lifts the + prover requirement.""" + history = [] + if declared is not None: + history.append({ + "sort": "run", + "tool_call_id": "t0", + "prover_results": [], + "spec_digest": "irrelevant-here", + "rules": None, + "declared_rules": declared, + "state_digest": spec_digest(spec, [], []), + }) + return { + "curr_spec": spec, + "skipped": [], + "validations": {}, + "required_validations": [], # the stamp check is not what these tests exercise + "version_history": [], + "prover_history": history, + # The rest of SourceCVLGenerationState, which the injected-state validator requires. + "messages": [], + "config": {}, + "rule_skips": {}, + "property_rules": [], + "reminders_channel": [], + "budget_curtailed": False, + "failed": None, + } + + +async def _publish(declared: list[str] | None, *mapped: str) -> str: + inst = PublishResultTool( + commentary="done", + property_rules=[PropertyRuleMapping( + property_title=PropertyTitle("p1"), rules=[RuleName(m) for m in mapped], + )], + state=_state(declared), + tool_call_id="t", + ) + tok = PublishResultTool._dep_ctx.set(TITLES) + try: + out = await inst.run() + finally: + PublishResultTool._dep_ctx.reset(tok) + # A rejection is a plain string; an accepted publish writes state. + return out if isinstance(out, str) else "ACCEPTED" + + +async def test_a_mapped_supporting_invariant_publishes(): + assert await _publish(["a", "b"], "a", "b") == "ACCEPTED" + + +async def test_an_unmapped_proved_invariant_is_refused(): + """The case the gate exists for: `b` verified but no property names it, so the report would + drop it as an orphan.""" + out = await _publish(["a", "b"], "a") + assert out != "ACCEPTED" and "b" in out + + +async def test_a_claim_on_a_rule_that_was_never_declared_is_refused(): + out = await _publish(["a"], "a", "imaginary") + assert out != "ACCEPTED" and "imaginary" in out + + +async def test_no_prover_run_leaves_the_names_uncross_checked(): + """Nothing to check against, so the gate falls back to coverage only rather than refusing a + wrap-up publish it has no ground truth for.""" + assert await _publish(None, "anything_goes") == "ACCEPTED" + + +async def test_an_empty_declaration_is_not_the_same_as_no_declaration(): + """A run that declared nothing is ground truth, not absence of it. Treating the empty set as + "unknown" would accept a mapping naming rules that do not exist.""" + out = await _publish([], "ghost_rule") + assert out != "ACCEPTED" and "ghost_rule" in out diff --git a/tests/test_rules_striping.py b/tests/test_rules_striping.py index 969c3848..28db82cb 100644 --- a/tests/test_rules_striping.py +++ b/tests/test_rules_striping.py @@ -606,3 +606,12 @@ def test_without_known_rules_names_arent_cross_checked(self): assert validate_property_rules( [_mapping("p1", "anything_goes")], [], [PropertyTitle("p1")], ) is None + + def test_without_known_rules_names_arent_cross_checked_but_empty_is_not_unknown(self): + # None means "no ground truth available"; an empty set means "the prover typechecked + # the spec and found nothing declared". Conflating them lets a claim on a nonexistent + # rule through. + assert validate_property_rules( + [_mapping("p1", "declared_nowhere")], [], [PropertyTitle("p1")], + known_rules=set(), + ) is not None