Main-contract augmentation harness: unstructured-storage getters, helper decomposition, verify-target threading

composer/spec/feedback.py

@@ -41,6 +41,9 @@ class FeedbackInherentParams(TypedDict):
     #   ``existing``   — pre-existing codebase being verified as-is; target
     #                    has real immutable source.
     sort: Sort
+    # One-liners describing the main-contract augmentation harness API. Only the
+    # source-mode (autoprove) flow supplies this; the other flows have no harness.
+    harness_api: NotRequired[list[str] | None]
 
 FeedbackTemplate = TypedTemplate[FeedbackInherentParams]("property_judge_prompt.j2")
 
@@ -53,18 +56,37 @@ class JudgeSystemParams(TypedDict):
 # ``sort == "existing"``, the only mode that wires those tools).
 FeedbackSystemTemplate = TypedTemplate[JudgeSystemParams]("property_judge_system_prompt.j2")
 
+
+def _bind_harness_augmentation(
+    prompt: TemplateInstantiation, harness_augmentation: bool
+) -> TemplateInstantiation:
+    """Inject the ``harness_augmentation`` flag into an already-instantiated template bind.
+
+    Both judge templates gate their harness-skip policy on this variable; injecting it
+    from the single ``property_feedback_judge`` parameter into BOTH binds is what keeps
+    the system prompt and Criteria 7 in agreement. The templates' ``default(false)`` is
+    a render fail-safe only, never the mechanism that decides the value.
+    """
+    return TemplateInstantiation(
+        prompt.template,
+        {**prompt.args, "harness_augmentation": harness_augmentation},
+    )
+
+
 def property_feedback_judge(
     ctx: WorkflowContext[CVLJudge],
     env: ServiceHost,
     prompt: InjectedTemplate[Properties] | TemplateInstantiation,
     props: list[PropertyFormulation],
     *,
+    harness_augmentation: bool = False,
     extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None,
     system_prompt: TemplateInstantiation | None = None,
 ) -> FeedbackToolContext:
 
     if system_prompt is None:
         system_prompt = FeedbackSystemTemplate.bind({"sort": env.sort})
+    system_prompt = _bind_harness_augmentation(system_prompt, harness_augmentation)
 
     builder = env.builder_heavy().with_tools(
         env.all_tools
@@ -88,7 +110,10 @@ def did_rough_draft_read(s: ST, _) -> str | None:
 
     mem = ctx.get_memory_tool()
 
-    final_prompt = prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props})
+    final_prompt = _bind_harness_augmentation(
+        prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props}),
+        harness_augmentation,
+    )
 
     workflow = bind_standard(
         builder, ST, validator=did_rough_draft_read

composer/spec/source/artifacts.py

@@ -69,9 +69,13 @@ class ProverArtifactStore(ArtifactStore):
     """Persists the autoprove pipeline's outputs under ``certora/`` (plus
     ``.certora_internal/autoProve/`` diagnostics)."""
 
-    def __init__(self, project_root: str, main_contract: str):
+    def __init__(self, project_root: str, main_contract: str, verify_contract: str | None = None):
         super().__init__(project_root)
-        self._main_contract = main_contract
+        # The contract identifier the prover verifies: the main-harness identifier
+        # when the run verifies through an augmentation harness, otherwise the main
+        # contract itself. ``main_contract`` (the protocol name) only serves as that
+        # default — the store's outputs (conf dumps) all name the verify target.
+        self._verify_contract = verify_contract or main_contract
 
     def _deliverable_dir(self) -> Path:
         return under_project(self._project_root, CERTORA_DIR)
@@ -116,8 +120,8 @@ def _write_conf(
             return
         conf = prover_config_overlay(
             base_config,
-            main_contract=self._main_contract,
-            verify_target=f"{self._main_contract}:{spec_path}",
+            main_contract=self._verify_contract,
+            verify_target=f"{self._verify_contract}:{spec_path}",
         )
         confs_dir = ensure_dir(self._deliverable_dir() / "confs")
         (confs_dir / f"{spec.stem}.conf").write_text(json.dumps(conf, indent=2))
@@ -138,11 +142,19 @@ def write_report(self, report: AutoProverReport) -> None:
         _log.info("autoprove report: wrote %s", out)
 
 
+@dataclass
 class ProverSourceCode(SourceCode):
     """``SourceCode`` that exposes the prover artifact store. Construct this in the
     autoprove entry point; analysis / property-inference passes keep taking plain
     ``SourceCode`` since the store is irrelevant to them."""
 
+    # The contract identifier the prover verifies. Defaults to ``contract_name``;
+    # the staged pipeline overrides it (via ``dataclasses.replace``) when a
+    # main-contract augmentation harness is the verify target.
+    verify_contract: str | None = None
+
     @property
     def artifact_store(self) -> ProverArtifactStore:
-        return ProverArtifactStore(self.project_root, self.contract_name)
+        return ProverArtifactStore(
+            self.project_root, self.contract_name, verify_contract=self.verify_contract,
+        )

composer/spec/source/author.py

@@ -33,8 +33,12 @@
 
 from graphcore.graph import FlowInput
 
+type GiveUpSort = Literal["env_issue", "needs_harness", "prover_limit", "other"]
+
 class SourceAuthorExtra(TypedDict):
     failed: bool | None
+    # Classification recorded by the give_up tool; None until (unless) it is called.
+    give_up_sort: GiveUpSort | None
 
 class SourceCVLGenerationExtra(CVLGenerationExtra, ProverStateExtra, SourceAuthorExtra):
     pass
@@ -47,6 +51,8 @@ class SourceCVLGenerationState(SourceCVLGenerationExtra, MessagesState):
 
 class GaveUp(BaseModel):
     reason: str
+    # Default keeps pre-change cached results deserializing.
+    sort: GiveUpSort = "other"
 
 type BatchGeneratedCVLResult = GeneratedCVL | GaveUp
 
@@ -135,6 +141,16 @@ class GiveUpTool(WithImplementation[Command], WithInjectedId):
     mechanisms to complete your task.
     """
     reason: str = Field(description="The reason for giving up on your task")
+    sort: GiveUpSort = Field(
+        default="other",
+        description=(
+            "Classification of the give-up: `env_issue` when a toolchain/environment "
+            "component is missing or broken; `needs_harness` when the properties require "
+            "observing state or entry points that the contract's external interface (and "
+            "any verification harness) does not expose; `prover_limit` when prover "
+            "timeouts/resource limits defeat every reformulation; `other` for anything else."
+        ),
+    )
 
     @override
     def run(self) -> Command:
@@ -143,6 +159,7 @@ def run(self) -> Command:
             "Accepted",
             failed=True,
             result=self.reason,
+            give_up_sort=self.sort,
         )
 
 class ResourceView(TypedDict):
@@ -157,6 +174,9 @@ class PropertyGenParams(TypedDict):
     resources: list[ResourceView]
     properties: list[PropertyFormulation]
     contract_name: str
+    # One-liners describing the main-contract augmentation harness API
+    # (getters/helpers); None when the run has no main harness.
+    harness_api: list[str] | None
 
 class PropertyGenerationConfig(SummaryConfig[SourceCVLGenerationState]):
     def __init__(self):
@@ -343,10 +363,13 @@ async def batch_cvl_generation(
     description: str,
     source: SourceCode,
     spec_dir: Path,
+    harness_api: list[str] | None = None,
 ) -> BatchGeneratedCVLResult:
     # *spec_dir* (project-root-relative) is where the caller will persist the spec
     # authored here. The prover resolves the spec's CVL imports relative to its own
     # directory, so resource imports are expressed relative to *spec_dir*.
+    # *harness_api* is the main-contract augmentation harness API (if any); it is
+    # surfaced to both the author and the feedback judge.
     resource_views: list[ResourceView] = [
         {
             "description": r.description,
@@ -359,7 +382,8 @@ async def batch_cvl_generation(
         "resources": resource_views,
         "context": component,
         "properties": props,
-        "contract_name": source.contract_name
+        "contract_name": source.contract_name,
+        "harness_api": harness_api
     })
 
     # use "cache=long" to account for very long prover runs.
@@ -389,8 +413,10 @@ async def batch_cvl_generation(
     feedback_env = property_feedback_judge(
         ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({
             "sort": "existing",
-            "context": component
-        }), props
+            "context": component,
+            "harness_api": harness_api
+        }), props,
+        harness_augmentation=harness_api is not None,
     )
 
     res_state = await run_cvl_generator(
@@ -408,13 +434,17 @@ async def batch_cvl_generation(
             property_rules=[],
             validations={},
             failed=None,
+            give_up_sort=None,
         )
     )
 
     assert "result" in res_state
     assert res_state["failed"] is not None
     if res_state["failed"]:
-        return GaveUp(reason=res_state["result"])
+        return GaveUp(
+            reason=res_state["result"],
+            sort=res_state.get("give_up_sort") or "other",
+        )
     d = res_state["curr_spec"]
     assert d is not None
     # Persist the base prover config and last run link from the final state so a later cache

composer/spec/source/common_pipeline.py

@@ -31,6 +31,7 @@
 from composer.spec.source.report import build as report_build
 from composer.spec.source.report.build import build_report
 from composer.spec.source.report.collect import ReportComponentInput
+from composer.spec.source.report.schema import HarnessDisclosure
 from composer.spec.source.report_prover import make_prover_fetcher
 
 _log = logging.getLogger(__name__)
@@ -147,13 +148,20 @@ async def generate_all_component_cvl(
     resources: list[CVLResource],
     semaphore: asyncio.Semaphore,
     invariant_result: tuple[list[PropertyFormulation], GeneratedCVL] | None = None,
+    harness_api: list[str] | None = None,
+    main_harness: HarnessDisclosure | None = None,
+    main_harness_fallback: str | None = None,
 ) -> AutoProveResult:
     """Phase 6 — per-component CVL generation.
 
     Generates and writes a spec for each extracted batch in parallel
     (semaphore-bounded). ``resources`` is consumed read-only; callers that want
     the structural invariants assumed as preconditions must include
-    ``invariants.spec`` in ``resources`` before calling.
+    ``invariants.spec`` in ``resources`` before calling. ``harness_api`` is the
+    main-contract augmentation harness API (if any), surfaced to the authors
+    and the feedback judge. ``main_harness`` / ``main_harness_fallback`` are the
+    report's harness disclosure: the augmentation harness verification ran
+    against, or the reason the run fell back to the raw contract.
     """
     async def _generate_batch(
         task_id: str,
@@ -182,6 +190,7 @@ async def _generate_batch(
                 description=label,
                 source=source_input,
                 spec_dir=SPECS_DIR,
+                harness_api=harness_api,
             ),
             semaphore,
         )
@@ -234,6 +243,7 @@ async def _generate_and_write_batch(
                 props=batch.props,
                 result=result if isinstance(result, GeneratedCVL) else None,
                 run_link=component_runs.get(spec.run_key),
+                gave_up_sort=result.sort if isinstance(result, GaveUp) else None,
             ))
         if invariant_result is not None:
             inv_props, inv_cvl = invariant_result
@@ -254,6 +264,8 @@ async def _generate_and_write_batch(
                 components=report_components,
                 llm=env.llm_lite(),
                 fetch_verdicts=make_prover_fetcher(),
+                main_harness=main_harness,
+                main_harness_fallback=main_harness_fallback,
             ),
         )
         if report is not None:
@@ -270,7 +282,7 @@ async def _generate_and_write_batch(
         if isinstance(result, BaseException):
             failures.append(f"{batch.feat.component.name}: {result}")
         elif isinstance(result, GaveUp):
-            failures.append(f"{batch.feat.component.name}: GAVE_UP: {result.reason}")
+            failures.append(f"{batch.feat.component.name}: GAVE_UP[{result.sort}]: {result.reason}")
 
     return AutoProveResult(
         n_components=len(component_batches),