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

certora_autosetup/autosetup/autosetup.py

@@ -903,6 +903,20 @@ async def run_single_contract_call_resolution(
 
             self.log(f"🔗 Running call resolution for {contract_handle.contract_name}")
             await call_resolution_phase.execute(max_iterations=10)
+
+            # Call resolution may recommend conf flags (e.g. optimistic_fallback when an
+            # unresolved low-level value transfer remains — no link/dispatcher can resolve
+            # those, and without the flag every caller can vacuously revert). The base conf
+            # was created before this phase ran, so merge into the existing conf here rather
+            # than at create_config time.
+            if call_resolution_phase.recommended_extra_flags:
+                self.log(
+                    f"Applying conf flags recommended by call resolution: "
+                    f"{call_resolution_phase.recommended_extra_flags}"
+                )
+                self.config_manager.apply_extra_flags(
+                    enhanced_config.path, call_resolution_phase.recommended_extra_flags
+                )
             return True
 
         except Exception as e:

certora_autosetup/setup/call_resolution.py

@@ -125,6 +125,25 @@ def dispatchers_added(self) -> int:
         return 0
 
 
+def is_unresolved_value_transfer(call: CallResolutionInfo) -> bool:
+    """Whether ``call`` is a low-level value transfer (``.call{value: ...}``, ``send``,
+    ``transfer``) with no resolvable target.
+
+    Such a call HAVOCs and — crucially — can always be *assumed to fail*, which makes every
+    caller able to revert on all paths (the vacuous-rule failure mode). ``optimistic_fallback``
+    assumes these calls succeed instead, hence the recommendation built from this predicate.
+
+    The selector check keeps high-level calls that merely look alike out: an unresolved
+    ERC20-style ``token.transfer(...)`` carries a resolvable selector, while native value
+    transfers have none (``[?].[?]`` in the report legend).
+    """
+    snippet = (call.call_site_snippet or "").replace(" ", "")
+    if not any(marker in snippet for marker in (".call{value", ".send(", ".transfer(")):
+        return False
+    # Cheap field check first: extract_sighash_from_callee may shell out to `cast sig`.
+    return call.selector is None and extract_sighash_from_callee(call.callee_name) is None
+
+
 class CallResolutionPhase:
     """
     Iterative call resolution:
@@ -169,6 +188,12 @@ def __init__(
         self.current_iteration = 0
         self._last_unresolved_calls: List[CallResolutionInfo] = []
 
+        # Structured conf-flag recommendation derived from the calls left unresolved when
+        # the loop finishes (currently only {"optimistic_fallback": True}, emitted when an
+        # unresolved low-level value transfer remains). The autosetup call site merges these
+        # into the emitted conf via the ConfigManager extra-flags whitelist.
+        self.recommended_extra_flags: Dict[str, Any] = {}
+
         # Report state: tracks every contract added to the scene with its provenance,
         # every proxy-detection scan result (hits and misses), and the prover job URL
         # for each iteration (None for local runs that don't produce a cloud URL).
@@ -337,6 +362,17 @@ async def execute(
                 else:
                     logger.info(f"  {call.caller_name} -> {call.callee_name}")
 
+        # Recommend optimistic_fallback when unresolved low-level value transfers remain:
+        # no link/dispatcher can ever resolve a native `.call{value: ...}`/`send`/`transfer`
+        # target, so without the flag every caller can vacuously revert.
+        value_transfers = [c for c in remaining if is_unresolved_value_transfer(c)]
+        if value_transfers:
+            self.recommended_extra_flags["optimistic_fallback"] = True
+            logger.info(
+                f"Recommending optimistic_fallback for {self.contract_name}: "
+                f"{len(value_transfers)} unresolved low-level value transfer(s) remain"
+            )
+
         # An empty `remaining` only means "all resolved" when the loop finished cleanly.
         # If a prover run failed, the loop broke before refreshing `remaining`, so the
         # spec is incomplete regardless of how many calls earlier iterations resolved.
@@ -553,6 +589,12 @@ def _generate_report(self, report_file: Path, limit_reached: bool) -> None:
                 prior_parts = [f"[{n}]({u})" if u else f"{n}" for n, u in prior]
                 headline += f"  (earlier iterations {', '.join(prior_parts)})"
             lines.append(headline)
+        if self.recommended_extra_flags:
+            lines.append(
+                f"- **Recommended conf flags:** {self.recommended_extra_flags} "
+                "(unresolved low-level value transfer(s) remain; without `optimistic_fallback` "
+                "every caller of such a call can vacuously revert)"
+            )
         lines.append("")
 
         # Section B: Proxy Detection

certora_autosetup/setup/setup_summaries.py

@@ -1668,6 +1668,33 @@ async def _analyze_method_with_llm_gated(
             await processed.put(None)
             return l
 
+    @staticmethod
+    def _nondet_ineligible(
+        recipe: Recipe,
+        method: Dict[str, Any],
+        payable_keys: Set[Tuple[str, str]],
+    ) -> bool:
+        """True when ``method`` must not be matched by a NONDET-producing recipe.
+
+        A NONDET summary erases the callee's effects; on a payable method that
+        includes its ability to accept ``msg.value``, and on any state-mutating
+        method it drops the state update — either way callers typically revert
+        on every path, so rules instantiated with them pass vacuously. This is
+        the match-time arm of the guard (defense in depth over the emit-time
+        view/pure check in ``_emit_per_contract_summaries``); it also covers
+        custom recipes, whose ``properties`` may not constrain mutability.
+
+        ``payable_keys`` is the ``(contractName, name)`` set from
+        ``MethodParser.get_payable_methods()`` — payability is the canonical
+        culprit, so it is checked explicitly rather than only via the
+        mutability fallback.
+        """
+        if recipe.summary_type.upper() != "NONDET":
+            return False
+        if (method["contractName"], method["name"]) in payable_keys:
+            return True
+        return method.get("stateMutability") not in ("view", "pure")
+
     async def analyze_with_llm(
         self,
         recipe: Recipe,
@@ -1701,6 +1728,12 @@ async def analyze_with_llm(
 
         mp = self.methods_parser
 
+        # Payable methods must never receive a NONDET summary (see _nondet_ineligible);
+        # keyed like methods_to_skip for the match-time exclusion below.
+        payable_keys: Set[Tuple[str, str]] = {
+            (m["contractName"], m["name"]) for m in mp.get_payable_methods()
+        }
+
         # Filter methods by properties and originatingContract
         all_methods = mp.get_all_methods()
         filtered_methods = []
@@ -1730,6 +1763,15 @@ async def analyze_with_llm(
                 if any(loc == "storage" for loc in method.get("location", [])):
                     continue
 
+                # Defense in depth over the emit-time view/pure check: never even propose a
+                # payable or state-mutating method for a NONDET recipe (custom recipes included).
+                if self._nondet_ineligible(recipe, method, payable_keys):
+                    self.log(
+                        f"Skipping payable/state-mutating method for NONDET recipe: "
+                        f"{method_key[0]}.{method_key[1]}"
+                    )
+                    continue
+
                 # Skip known ERC4626 exchange-rate methods for the decimal-conversion recipe:
                 # they read vault state, so the identity summary would be unsound (see constant).
                 if (
@@ -2257,7 +2299,15 @@ def _build_recipes(self, custom_recipe: Optional[str]) -> List[Recipe]:
                 Recipe(
                     recipe_type=RecipeType.INLINE_ASSEMBLY,
                     characteristic="contains inline assembly blocks with `mload` or `mstore` instructions",
-                    properties={"visibility": "internal"},
+                    # Restricted to view/pure: a NONDET summary on a state-mutating (and
+                    # especially payable) method erases its effects, which typically makes
+                    # every caller revert on all paths — rules over those callers then pass
+                    # vacuously. `_nondet_ineligible` enforces the same bound at match time
+                    # as defense in depth (covering custom recipes too).
+                    properties={
+                        "visibility": "internal",
+                        "stateMutability": ["view", "pure"],
+                    },
                     summary_type="NONDET",
                 ),
             ]

certora_autosetup/utils/enhanced_config_manager.py

@@ -123,6 +123,12 @@ class ConfigManager:
 
     DEFAULT_CONF_TEMPLATE = {"assert_autofinder_success": True, "files": []}
 
+    # Top-level conf flags an autosetup phase may *recommend* (e.g. call resolution
+    # recommending optimistic_fallback for unresolved low-level value transfers).
+    # Deliberately narrow: recommendations flow from automated analyses, so anything
+    # outside this whitelist is a bug in the recommending phase, not user input.
+    EXTRA_FLAGS_WHITELIST = frozenset({"optimistic_fallback", "contract_recursion_limit"})
+
     def __init__(
         self,
         project_root: Path,
@@ -199,6 +205,38 @@ def normalize_paths(self, handles: List[ContractHandle]) -> List[ContractHandle]
                 normalized_handles.append(handle)
         return normalized_handles
 
+    def _validated_extra_flags(self, extra_flags: Dict[str, Any]) -> Dict[str, Any]:
+        """Validate a recommended-flags dict against EXTRA_FLAGS_WHITELIST.
+
+        Raises ValueError on a non-whitelisted flag or an ill-typed value — the caller
+        is an automated phase, so a violation is a programming error, not bad user input.
+        NB: bool is a subclass of int, so the bool check precedes the int check.
+        """
+        for flag, value in extra_flags.items():
+            if flag not in self.EXTRA_FLAGS_WHITELIST:
+                raise ValueError(
+                    f"Flag {flag!r} is not in the extra-flags whitelist "
+                    f"({sorted(self.EXTRA_FLAGS_WHITELIST)})"
+                )
+            if flag == "optimistic_fallback" and not isinstance(value, bool):
+                raise ValueError(f"optimistic_fallback expects a bool, got {value!r}")
+            if flag == "contract_recursion_limit" and (
+                isinstance(value, bool) or not isinstance(value, int) or not (0 <= value <= 10)
+            ):
+                raise ValueError(f"contract_recursion_limit expects an int in 0..10, got {value!r}")
+        return dict(extra_flags)
+
+    def apply_extra_flags(self, config_file: Path, extra_flags: Dict[str, Any]) -> FileContent:
+        """Merge whitelisted recommended flags into an *existing* conf.
+
+        Companion to create_config's ``extra_flags`` parameter for recommendations that
+        arrive after the conf was created (call resolution runs against the already-created
+        base conf and mutates it in place, like its linker entries do).
+        """
+        return self.update_config_with_properties(
+            config_file, self._validated_extra_flags(extra_flags)
+        )
+
     def create_config(
         self,
         contract_name: str,
@@ -208,6 +246,7 @@ def create_config(
         conf_path: Optional[Path] = None,
         additional_args: Optional[Dict[str, str]] = None,
         properties: Optional[Dict[str, Any]] = None,
+        extra_flags: Optional[Dict[str, Any]] = None,
     ) -> FileContent:
         """
         Create initial configuration file from template.
@@ -220,6 +259,8 @@ def create_config(
             conf_path: Path to the to-be-created .conf file
             additional_args: Optional dict of additional prover arguments
             properties: Optional dict of additional config properties (including build system settings)
+            extra_flags: Optional recommended top-level flags from automated phases;
+                validated against EXTRA_FLAGS_WHITELIST (ValueError on violation)
 
         Returns:
             FileContent representing the created configuration
@@ -241,6 +282,11 @@ def create_config(
         if properties:
             conf_template.update(properties)
 
+        # Apply whitelisted recommended flags (after properties: a validated
+        # recommendation wins over a same-named entry smuggled in via properties)
+        if extra_flags:
+            conf_template.update(self._validated_extra_flags(extra_flags))
+
         # Apply additional prover args if provided
         if additional_args:
             existing_args_raw = conf_template.get("prover_args", [])

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),
     )