Drop the eager structural-invariant phase

.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_<name>.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 '<x>'` — 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)

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
 

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.
 

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 —

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:

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,17 +716,16 @@ 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,
             props=o.props,
             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,

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

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