Vacuity detection + repair ladder: fix setup root causes instead of filtering methods

certora_autosetup/autosetup/autosetup.py

@@ -215,10 +215,6 @@ def _summarized_library_names(self) -> set[str]:
         llm = set(setup._methods_per_contract.keys()) & self._library_names
         return curated | llm
 
-    def _build_job_msg(self, contract_name: str, conf_file: Path) -> str:
-        """Build the msg string for a prover job."""
-        return ProverJobSpec.build_job_msg(self.config.orchestration_timestamp, contract_name, conf_file)
-
     def run(self, main_contract_handle: ContractHandle, skip_warmup: bool = False) -> AutosetupResult:
         """Execute the full autosetup pipeline.
 
@@ -811,7 +807,6 @@ async def prepare_contract_warmup() -> Optional[ProverJobSpec[Any]]:
                     contract_name=contract_name,
                     phase=f"Sanity Test Run - {contract_name}",
                     extra_args=autosetup.config.extra_args,
-                    msg=autosetup._build_job_msg(contract_name, test_config.path),
                 ))
 
                 if skip_warmup:
@@ -831,7 +826,6 @@ async def prepare_contract_warmup() -> Optional[ProverJobSpec[Any]]:
                     contract_name=contract_name,
                     phase="Sanity Warmup - warmup",
                     extra_args=autosetup.config.extra_args,
-                    msg=autosetup._build_job_msg(contract_name, warmup_config.path),
                 )
 
             async def prepare_and_run_warmup():

certora_autosetup/conf_runner/callbacks.py

@@ -191,7 +191,6 @@ def _create_multi_assert_jobs_if_needed(self, result: ProverResult) -> List[Prov
                     phase=f"{result.job_spec.phase}_{rule_name}_multi_assert",
                     extra_args=result.job_spec.extra_args,
                     context=result.job_spec.context,
-                    msg=ProverJobSpec.build_job_msg(self.orchestration_timestamp, contract_name, new_config_path),
                 )
                 new_jobs.append(new_job_spec)
 
@@ -294,7 +293,6 @@ def _create_difficult_retry_jobs_if_needed(
                     phase=f"{result.job_spec.phase}_{rule_name}_difficult_retry",
                     extra_args=result.job_spec.extra_args,
                     context=result.job_spec.context,
-                    msg=ProverJobSpec.build_job_msg(self.orchestration_timestamp, contract_name, new_config_path),
                 )
                 new_jobs.append(new_job_spec)
 

certora_autosetup/conf_runner/conf_runner.py

@@ -137,7 +137,6 @@ def _run_all_configs(
                     contract_name=contract_name,
                     phase=f"{tool_name}-{config_name}",
                     extra_args=self.config.extra_args,
-                    msg=ProverJobSpec.build_job_msg(self.orchestration_timestamp, contract_name, config_file),
                 )
                 job_specs.append(job_spec)
                 self.log(

certora_autosetup/setup/call_resolution.py

@@ -473,6 +473,9 @@ async def _run_prover_and_parse_calls(self) -> Optional[List[CallResolutionInfo]
             phase="call_resolution",
             config_file=config_content,
             extra_args=self.extra_args,
+            msg=ProverJobSpec.build_job_msg(
+                self.contract_name, self.config_file, suffix=f"(iteration {self.current_iteration})"
+            ),
         )
 
         prover_result = await self.prover_runner.check_with_prover(job_spec)

certora_autosetup/setup/sanity.py

@@ -364,14 +364,6 @@ def _internal_confs_dir(self) -> Path:
         """Directory for transient conf copies, kept out of the user-facing certora/confs/ tree."""
         return self.prover_runner.project_root / DIR_INTERNAL_CONFS
 
-    def _build_job_msg(self, conf_file: Path) -> Optional[str]:
-        """Build the msg string for a prover job.
-
-        Format: "ProverLite <timestamp> <ContractName>: <conf_name>"
-        Returns None if no orchestration_timestamp is set.
-        """
-        return ProverJobSpec.build_job_msg(self.orchestration_timestamp, self.contract_name, conf_file)
-
     def log(self, level: str, message: str):
         """Simple contract logging utility."""
         log_with_contract("Sanity", level, self.contract_name, message)
@@ -598,7 +590,6 @@ async def _run_sanity_coverage_rerun(self, failing_methods: List[str], completio
                 phase=f"Sanity Coverage Rerun - {self.contract_name} - {method}",
                 config_file=coverage_config,
                 extra_args=self.extra_args,
-                msg=self._build_job_msg(coverage_config.path),
             ))
         return await self.prover_runner.submit_and_wait_for_jobs(job_specs, completion_callback=completion_callback)
 
@@ -728,7 +719,6 @@ async def _detect_optimal_hashing_bounds(self) -> Optional[int]:
                 phase="hashing_bound_detection",
                 config_file=bound_detection_config,
                 extra_args=self.extra_args,
-                msg=self._build_job_msg(bound_detection_config.path),
             )
 
             result = await self.prover_runner.check_with_prover(job_spec)
@@ -904,7 +894,6 @@ async def _test_configurations(
                 config_file=test_config,
                 extra_args=self.extra_args,
                 context=config,  # Store BoundConfiguration as context
-                msg=self._build_job_msg(test_config.path),
             )
             job_specs.append(job_spec)
 

certora_autosetup/utils/enhanced_config_manager.py

@@ -75,6 +75,11 @@ class ProverJobSpec(Generic[ContextT]):
     context: Optional[ContextT] = None
     msg: Optional[str] = None  # Message for --msg argument
 
+    def __post_init__(self) -> None:
+        # When no msg is given, default it to "<Contract>: <conf_name>".
+        if self.msg is None:
+            self.msg = self.build_job_msg(self.contract_name, self.config_file.path)
+
     def get_cache_key(self, config_manager: "ConfigManager") -> str:
         """
         Generate cache key from config + all referenced files + extra_args.
@@ -100,20 +105,24 @@ def get_cache_key(self, config_manager: "ConfigManager") -> str:
         return cache_key
 
     @staticmethod
-    def build_job_msg(orchestration_timestamp: str, contract_name: str, conf_file: Path) -> str:
+    def build_job_msg(contract_name: str, conf_file: Path, suffix: Optional[str] = None) -> str:
         """Build the msg string for a prover job.
 
-        Format: "Certora <timestamp> <ContractName>: <conf_name>"
+        Format: "<ContractName>: <conf_name>" (with " <suffix>" appended if provided).
 
         Args:
-            orchestration_timestamp: Timestamp string from orchestration start
             contract_name: Name of the contract being verified
             conf_file: Path to the configuration file
+            suffix: Optional trailing text to disambiguate jobs that reuse the same
+                conf (e.g. an iteration marker); the caller decides its content
 
         Returns:
-            Formatted message string or None if no timestamp
+            Formatted message string
         """
-        return f"Certora {orchestration_timestamp} {contract_name}: {conf_file.stem}"
+        msg = f"{contract_name}: {conf_file.stem}"
+        if suffix:
+            msg += f" {suffix}"
+        return msg
 
 
 class ConfigManager:

composer/prover/core.py

@@ -45,6 +45,9 @@
 from composer.prover.cloud import CloudJobError, cloud_results
 from composer.prover.ptypes import RuleResult
 from composer.prover.results import read_and_format_run_result
+from composer.prover.vacuity import (
+    VacuityEvidence, detect_vacuous_methods, format_vacuity_alert, instantiated_methods,
+)
 from composer.templates.loader import load_jinja_template
 from composer.prover.prover_protocol import ProverResult
 
@@ -97,10 +100,18 @@ class ProverReport:
     them through the return value.
 
     ``link`` is the prover run's URL (cloud) or local results directory.
+
+    ``vacuous_methods`` / ``instantiated_methods`` carry the per-run vacuity
+    view (see ``composer/prover/vacuity.py``): the methods detected as vacuous
+    in this run, and every method this run instantiated at all. The latter
+    lets the caller clear a previously-recorded vacuity verdict once a run
+    shows the method instantiated and healthy.
     """
     rule_status: dict[str, bool]
     result_str: str
     link: str
+    vacuous_methods: dict[str, VacuityEvidence] = field(default_factory=dict)
+    instantiated_methods: set[str] = field(default_factory=set)
 
     @property
     def all_verified(self) -> bool:
@@ -481,6 +492,11 @@ async def run_prover(
 
             all_results = list(parsed.values())
 
+            # Vacuity view of this run: methods whose sanity check failed across
+            # their instantiating rules. Computed here (rather than in callers)
+            # so every prover consumer sees the same alert in its report string.
+            vacuous = detect_vacuous_methods(all_results)
+
             # 10. Hand off to the handler when anything failed. It owns the
             # analysis approach, per-rule UI events, rendering, summarization
             # (if any), and storage of any keyed records (e.g. report_keys
@@ -498,6 +514,12 @@ async def run_prover(
                     rule_entries=[(r, None) for r in all_results],
                     diagnoses=[],
                 )
+
+            # Append the vacuity alert to whatever the handler/template rendered:
+            # a vacuous method most often surfaces as a *passing* (trivially
+            # verified) rule, so the alert must reach the agent on both branches.
+            if vacuous:
+                result_str = f"{result_str}\n\n{format_vacuity_alert(vacuous)}"
     except CloudJobError as exc:
         return f"Prover cloud job did not produce results (status {exc.status.value})."
 
@@ -512,4 +534,6 @@ async def run_prover(
         rule_status=prover_report,
         result_str=result_str,
         link=run_result["link"],
+        vacuous_methods=vacuous,
+        instantiated_methods=instantiated_methods(all_results),
     )

composer/prover/vacuity.py

@@ -0,0 +1,163 @@
+"""Vacuous-method detection over per-rule prover results.
+
+A parametric method whose sanity check fails in every rule that instantiates it
+(or in several rules while every other instantiation timed out or errored) is
+*vacuous*: every path through it reverts under
+the current verification model, so any rule instantiated with it passes
+trivially. Per-rule ``SANITY_FAILED`` results already reach the verify loop
+(``composer/prover/results.py`` attaches the ``METHOD_INSTANTIATION`` name to
+``RulePath.method``); this module aggregates them into a per-method verdict and
+renders the ``<vacuity_alert>`` the agent sees plus the ``verify_spec`` guard
+message. The guard itself is purely structural (no spec-text scanning): a
+verdict persists in graph state until a run re-instantiates the method
+healthily, so *any* route that hides the method (a ``filtered`` block, marking
+its rules "expected to fail", deleting the rule) leaves the verdict
+outstanding, and the PROVER stamp is withheld unless the agent formally
+acknowledges the method via the ``acknowledge_vacuous_method`` tool.
+
+The near-universal root cause is a setup defect — canonically a NONDET summary
+on a payable or side-effecting callee — so the alert prescribes a *repair
+ladder* that puts root-cause fixes first and ``filtered`` exclusion last.
+"""
+
+from typing import Iterable
+
+from pydantic import BaseModel
+
+from composer.prover.ptypes import RuleResult
+
+
+class VacuityEvidence(BaseModel):
+    """Why a method was flagged as vacuous: the rules whose sanity check it
+    failed, and a one-line diagnosis suitable for reports and agent state."""
+
+    method: str
+    affected_rules: list[str]
+    diagnosis: str
+
+
+def detect_vacuous_methods(results: Iterable[RuleResult]) -> dict[str, VacuityEvidence]:
+    """Group ``SANITY_FAILED`` results by instantiated method and flag the
+    methods that are sanity-failed in 100% of the rules that instantiate them,
+    OR in >= 2 rules while no instantiation reached a healthy verdict.
+
+    The 100% arm catches single-rule runs. The >= 2 arm catches a method that
+    is vacuous across the board when the remaining instantiations are
+    TIMEOUT/ERROR/SKIPPED — statuses that can *mask* an all-paths-reverting
+    method. A VERIFIED or VIOLATED instantiation, by contrast, requires
+    actually reaching the method's code, so it *disproves* all-paths
+    reversion: sanity failures alongside a healthy instantiation stem from
+    the failing rules' own preconditions (a rule-authoring problem), not
+    method vacuity, and must not be flagged here. A sanity failure on a
+    non-parametric rule (``path.method is None``) is likewise a
+    rule-authoring problem and is ignored.
+    """
+    instantiating: dict[str, set[str]] = {}
+    sanity_failed: dict[str, set[str]] = {}
+    healthy: dict[str, set[str]] = {}
+    for r in results:
+        method = r.path.method
+        if method is None:
+            continue
+        instantiating.setdefault(method, set()).add(r.path.rule)
+        if r.status == "SANITY_FAILED":
+            sanity_failed.setdefault(method, set()).add(r.path.rule)
+        elif r.status in ("VERIFIED", "VIOLATED"):
+            healthy.setdefault(method, set()).add(r.path.rule)
+
+    flagged: dict[str, VacuityEvidence] = {}
+    for method, failed_rules in sanity_failed.items():
+        all_rules = instantiating[method]
+        everywhere = failed_rules == all_rules
+        masked_majority = len(failed_rules) >= 2 and not healthy.get(method)
+        if not (everywhere or masked_majority):
+            continue
+        flagged[method] = VacuityEvidence(
+            method=method,
+            affected_rules=sorted(failed_rules),
+            diagnosis=(
+                f"sanity-failed in {len(failed_rules)} of {len(all_rules)} rule(s) "
+                "that instantiate it: the method reverts on every path under the "
+                "current verification model, so rules over it pass vacuously"
+            ),
+        )
+    return flagged
+
+
+def instantiated_methods(results: Iterable[RuleResult]) -> set[str]:
+    """Every method name instantiated in this result set (any status). Used to
+    clear a stale vacuity verdict once a later run shows the method healthy."""
+    return {r.path.method for r in results if r.path.method is not None}
+
+
+_REPAIR_LADDER = """\
+This is almost always a SETUP defect, not a property error. The canonical culprits are:
+  * a NONDET/CONSTANT summary applied to a payable or side-effecting callee (the summary drops
+    the callee's effects — e.g. its ability to accept msg.value — making the caller's success
+    path infeasible),
+  * an unresolved low-level `.call{value: ...}` that HAVOCs and can always be assumed to fail,
+  * a missing `link`, leaving a callee address unresolved.
+
+Repair in this order (the "repair ladder"); do NOT jump to a later step without attempting the earlier ones:
+  1. Fix or replace the offending summary so it preserves the callee's semantics — in particular
+     payable-ness: a payable callee must be able to accept the transferred value.
+  2. Write a minimal mock contract under `certora/mocks` (the `write_mock` tool) implementing the
+     callee's interface, and register it in the prover config with `edit_config` (AddFile, plus
+     AddLink if the callee is reached through a storage field).
+  3. Set `optimistic_fallback` to true via `edit_config` (set_flag) so unresolved calls are assumed
+     to succeed instead of always being able to revert.
+  4. ONLY as a last resort, formally acknowledge the method with the `acknowledge_vacuous_method`
+     tool, recording which of steps 1-3 you attempted and why each failed, and then exclude it
+     with a `filtered` block. Hiding a vacuous method (filtering it, marking its rules "expected
+     to fail", or deleting the rule) without that acknowledgment will not be accepted as a
+     passing result."""
+
+
+def format_vacuity_alert(evidence: dict[str, VacuityEvidence]) -> str:
+    """Render the ``<vacuity_alert>`` block appended to the prover report the
+    agent sees. Empty string when nothing was flagged."""
+    if not evidence:
+        return ""
+    lines = [
+        "<vacuity_alert>",
+        "The following method(s) are VACUOUS — every rule instantiated with them holds trivially",
+        "because their assertions are unreachable:",
+    ]
+    for method in sorted(evidence):
+        ev = evidence[method]
+        lines.append(f"  - {method}: {ev.diagnosis} (rules: {', '.join(ev.affected_rules)})")
+    lines.append("")
+    lines.append(_REPAIR_LADDER)
+    lines.append("</vacuity_alert>")
+    return "\n".join(lines)
+
+
+def format_vacuity_guard(blocked: dict[str, str]) -> str:
+    """Render the message returned by ``verify_spec`` when it withholds the
+    PROVER validation stamp: ``blocked`` maps each still-outstanding vacuous
+    method (no healthy re-instantiation, no acknowledgment) to its diagnosis.
+
+    The gate feeding this is purely structural — set membership over the
+    persisted verdicts and the acknowledgment ledger, never spec-text scanning
+    — so the message covers every hiding route (``filtered`` blocks,
+    ``expect_rule_failure`` skips, rule deletion) uniformly.
+    """
+    method_list = "\n".join(f"  - {m}: {d}" for m, d in sorted(blocked.items()))
+    return f"""\
+<vacuity_guard>
+The PROVER validation stamp was WITHHELD. The following method(s) were detected as VACUOUS
+(they revert on every path under the current verification model), and no later run has shown
+them healthy, nor have they been acknowledged:
+{method_list}
+
+A run where every rule passes while a known-vacuous method is hidden (via a `filtered` block,
+`expect_rule_failure` on its sanity-failing rules, or removing the rule) hides a setup defect
+instead of fixing it. Either:
+  * repair the root cause (repair ladder: 1. fix/replace the offending summary preserving payable
+    semantics, 2. `write_mock` + `edit_config` add_file/add_link, 3. `optimistic_fallback` via
+    `edit_config` set_flag), re-include the method, and rerun `verify_spec` — a run that
+    instantiates the method without a sanity failure clears its verdict automatically; or
+  * if steps 1-3 genuinely failed, call `acknowledge_vacuous_method` for the method, recording
+    which steps you attempted and why each failed, then rerun `verify_spec`. The feedback judge
+    will audit the quality of that acknowledgment.
+</vacuity_guard>"""