From 207c61fc44a0cafd94d19ee95b888b1d8b2692cd Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:11:24 +0300 Subject: [PATCH 01/13] Add vacuous-method detection over per-rule sanity results detect_vacuous_methods flags a parametric method as vacuous when its sanity check fails in >=2 rules or in 100% of the rules instantiating it; format_vacuity_alert renders the repair-ladder alert (summary fix -> mock -> optimistic_fallback -> documented filtered), and undocumented_filtered_vacuous provides the lenient spec-text check for the upcoming verify_spec filtered-vacuous guard. Co-Authored-By: Claude Fable 5 --- composer/prover/vacuity.py | 205 +++++++++++++++++++++++++++++++++++++ tests/test_vacuity.py | 169 ++++++++++++++++++++++++++++++ 2 files changed, 374 insertions(+) create mode 100644 composer/prover/vacuity.py create mode 100644 tests/test_vacuity.py diff --git a/composer/prover/vacuity.py b/composer/prover/vacuity.py new file mode 100644 index 0000000..fbd169d --- /dev/null +++ b/composer/prover/vacuity.py @@ -0,0 +1,205 @@ +"""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 at once) 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, +renders the ```` the agent sees, and provides the spec-text +checks backing the ``verify_spec`` filtered-vacuous guard. + +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. +""" + +import re +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 >= 2 rules OR in 100% of the rules that + instantiate them. + + The 100% arm catches single-rule runs; the >= 2 arm catches a method that + is vacuous across the board even when some rule's own preconditions mask + it. A sanity failure on a non-parametric rule (``path.method is None``) + is a rule-authoring problem, not method vacuity, and is ignored here. + """ + instantiating: dict[str, set[str]] = {} + sanity_failed: 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) + + flagged: dict[str, VacuityEvidence] = {} + for method, failed_rules in sanity_failed.items(): + all_rules = instantiating[method] + if len(failed_rules) < 2 and failed_rules != all_rules: + 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, exclude the method with a `filtered` block. The justification comment + next to the filter MUST name which of steps 1-3 you attempted and why each failed — an + undocumented filter of a vacuous method will not be accepted as a passing result.""" + + +def format_vacuity_alert(evidence: dict[str, VacuityEvidence]) -> str: + """Render the ```` block appended to the prover report the + agent sees. Empty string when nothing was flagged.""" + if not evidence: + return "" + lines = [ + "", + "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("") + return "\n".join(lines) + + +def format_filter_guard(blocked: list[str]) -> str: + """Render the message returned by ``verify_spec`` when it withholds the + PROVER validation stamp because vacuous methods are filtered without a + documented repair attempt.""" + method_list = "\n".join(f" - {m}" for m in sorted(blocked)) + return f"""\ + +The PROVER validation stamp was WITHHELD. The following method(s) were previously detected as +VACUOUS (they revert on every path under the current verification model) and are now excluded via +a `filtered` block with no documented repair attempt: +{method_list} + +Filtering a vacuous method 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` AddFile/AddLink, 3. `optimistic_fallback` via + `edit_config` set_flag), un-filter the method, and rerun `verify_spec`; or + * if steps 1-3 genuinely failed, add a comment next to the `filtered` block documenting which of + summary-fix / mock / optimistic_fallback you attempted and why each failed, then rerun + `verify_spec`. The feedback judge will assess the quality of that justification. +""" + + +def _bare_method_name(method: str) -> str: + """``Bank.withdraw(uint256)`` -> ``withdraw``. Prover method-instantiation + names are contract-qualified with a parameter list; filter expressions + reference the bare Solidity name (e.g. ``sig:withdraw(uint256).selector``).""" + return method.split("(", 1)[0].rsplit(".", 1)[-1] + + +def _filtered_blocks_with_context(spec: str, context_lines: int = 12) -> list[tuple[str, str]]: + """Return ``(context, body)`` for every ``filtered { ... }`` block in the + spec. ``body`` is the brace-delimited filter text; ``context`` additionally + includes the ``context_lines`` lines preceding the ``filtered`` keyword, + which is where a repair-attempt justification comment is expected to live. + + Deliberately a simple lexical scan (no CVL parser): filter bodies are + single expressions, so naive brace matching suffices, and a rare miss only + skips the guard — it can never spuriously block. + """ + blocks: list[tuple[str, str]] = [] + for match in re.finditer(r"\bfiltered\b", spec): + open_idx = spec.find("{", match.end()) + if open_idx == -1: + continue + depth = 0 + close_idx = -1 + for i in range(open_idx, len(spec)): + if spec[i] == "{": + depth += 1 + elif spec[i] == "}": + depth -= 1 + if depth == 0: + close_idx = i + break + if close_idx == -1: + continue + body = spec[open_idx : close_idx + 1] + preceding = spec[: match.start()].splitlines()[-context_lines:] + blocks.append(("\n".join(preceding) + "\n" + body, body)) + return blocks + + +# Lenient markers for "a repair-ladder step was attempted and documented". Substring match, +# case-insensitive: "summar" covers summary/summaries/summarized. Presence — not quality — is +# checked here; the feedback judge assesses whether the justification is actually convincing. +_REPAIR_ATTEMPT_MARKERS = ("summar", "mock", "optimistic_fallback") + + +def _documents_repair_attempt(context: str) -> bool: + lowered = context.lower() + return any(marker in lowered for marker in _REPAIR_ATTEMPT_MARKERS) + + +def undocumented_filtered_vacuous(spec: str, methods: Iterable[str]) -> list[str]: + """The subset of ``methods`` (prover instantiation names) that appear in a + ``filtered`` block of ``spec`` where neither the block nor the lines above + it document a repair-ladder attempt. + + A method mentioned in several filters passes if ANY of them is documented + — the false-block risk must stay low; the judge arbitrates quality. + """ + blocks = _filtered_blocks_with_context(spec) + blocked: list[str] = [] + for method in methods: + bare = _bare_method_name(method) + containing = [ctx for (ctx, body) in blocks if bare in body] + if containing and not any(_documents_repair_attempt(ctx) for ctx in containing): + blocked.append(method) + return sorted(blocked) diff --git a/tests/test_vacuity.py b/tests/test_vacuity.py new file mode 100644 index 0000000..84722bc --- /dev/null +++ b/tests/test_vacuity.py @@ -0,0 +1,169 @@ +""" +Unit tests for composer/prover/vacuity.py: vacuous-method detection over +synthetic RuleResult sets, alert rendering, and the filtered-block / +documented-repair spec-text checks backing the verify_spec guard. +""" + +from composer.prover.ptypes import RulePath, RuleResult, StatusCodes +from composer.prover.vacuity import ( + detect_vacuous_methods, + format_vacuity_alert, + instantiated_methods, + undocumented_filtered_vacuous, +) + + +def _res(rule: str, method: str | None, status: StatusCodes) -> RuleResult: + return RuleResult( + path=RulePath(rule=rule, contract="Bank", method=method), + cex_dump=None, + status=status, + ) + + +DEPOSIT = "Bank.deposit(uint256)" +WITHDRAW = "Bank.withdraw(uint256)" + + +# ========================================================================= +# detect_vacuous_methods +# ========================================================================= + + +class TestDetectVacuousMethods: + def test_vacuous_in_all_rules(self): + """Sanity-failed in 100% of the (3) instantiating rules -> flagged.""" + results = [ + _res(r, DEPOSIT, "SANITY_FAILED") for r in ("ruleA", "ruleB", "ruleC") + ] + flagged = detect_vacuous_methods(results) + assert set(flagged) == {DEPOSIT} + assert flagged[DEPOSIT].affected_rules == ["ruleA", "ruleB", "ruleC"] + assert "3 of 3" in flagged[DEPOSIT].diagnosis + + def test_vacuous_in_single_rule_run(self): + """One rule, one instantiation, sanity-failed: 100% -> flagged.""" + flagged = detect_vacuous_methods([_res("ruleA", DEPOSIT, "SANITY_FAILED")]) + assert set(flagged) == {DEPOSIT} + + def test_sanity_failed_in_one_of_many_not_flagged(self): + """Failed in 1 of 3 rules: below the >=2 threshold and not 100%.""" + results = [ + _res("ruleA", DEPOSIT, "SANITY_FAILED"), + _res("ruleB", DEPOSIT, "VERIFIED"), + _res("ruleC", DEPOSIT, "VERIFIED"), + ] + assert detect_vacuous_methods(results) == {} + + def test_two_rules_flagged_even_when_others_pass(self): + """>=2 sanity-failed rules flag the method even below 100%.""" + results = [ + _res("ruleA", DEPOSIT, "SANITY_FAILED"), + _res("ruleB", DEPOSIT, "SANITY_FAILED"), + _res("ruleC", DEPOSIT, "VERIFIED"), + ] + assert set(detect_vacuous_methods(results)) == {DEPOSIT} + + def test_mixed_methods(self): + """Only the everywhere-failing method is flagged in a mixed result set.""" + results = [ + _res("ruleA", DEPOSIT, "SANITY_FAILED"), + _res("ruleB", DEPOSIT, "SANITY_FAILED"), + _res("ruleA", WITHDRAW, "VERIFIED"), + _res("ruleB", WITHDRAW, "SANITY_FAILED"), + _res("ruleC", WITHDRAW, "VIOLATED"), + ] + assert set(detect_vacuous_methods(results)) == {DEPOSIT} + + def test_non_parametric_sanity_failure_ignored(self): + """SANITY_FAILED with no method is a rule problem, not method vacuity.""" + assert detect_vacuous_methods([_res("ruleA", None, "SANITY_FAILED")]) == {} + + def test_instantiated_methods(self): + results = [ + _res("ruleA", DEPOSIT, "VERIFIED"), + _res("ruleB", WITHDRAW, "SANITY_FAILED"), + _res("static", None, "VERIFIED"), + ] + assert instantiated_methods(results) == {DEPOSIT, WITHDRAW} + + +# ========================================================================= +# format_vacuity_alert +# ========================================================================= + + +class TestFormatVacuityAlert: + def test_empty_evidence_renders_nothing(self): + assert format_vacuity_alert({}) == "" + + def test_alert_contains_ladder_and_methods(self): + evidence = detect_vacuous_methods( + [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")] + ) + alert = format_vacuity_alert(evidence) + assert alert.startswith("") + assert alert.endswith("") + assert DEPOSIT in alert + # Repair ladder ordering: summary fix -> mock -> optimistic_fallback -> filtered. + assert ( + alert.index("Fix or replace the offending summary") + < alert.index("write_mock") + < alert.index("optimistic_fallback") + < alert.index("filtered") + ) + + +# ========================================================================= +# undocumented_filtered_vacuous +# ========================================================================= + + +_UNDOCUMENTED_SPEC = """\ +rule solvency(method f) filtered { f -> f.selector != sig:deposit(uint256).selector } { + assert true; +} +""" + +_DOCUMENTED_SPEC = """\ +// deposit is excluded: attempted to fix the NONDET summary on the payable receiver (typecheck +// rejected the replacement), then a mock under certora/mocks (compilation failed on the +// constructor), then optimistic_fallback (the revert persisted). Filtering as a last resort. +rule solvency(method f) filtered { f -> f.selector != sig:deposit(uint256).selector } { + assert true; +} +""" + +_NO_FILTER_SPEC = """\ +rule solvency(method f) { + assert true; +} +""" + + +class TestUndocumentedFilteredVacuous: + def test_undocumented_filter_blocked(self): + assert undocumented_filtered_vacuous(_UNDOCUMENTED_SPEC, [DEPOSIT]) == [DEPOSIT] + + def test_documented_filter_passes(self): + assert undocumented_filtered_vacuous(_DOCUMENTED_SPEC, [DEPOSIT]) == [] + + def test_method_not_filtered_passes(self): + assert undocumented_filtered_vacuous(_NO_FILTER_SPEC, [DEPOSIT]) == [] + + def test_other_method_in_filter_passes(self): + assert undocumented_filtered_vacuous(_UNDOCUMENTED_SPEC, [WITHDRAW]) == [] + + def test_one_documented_occurrence_suffices(self): + """A method filtered in two rules passes if either filter is documented.""" + spec = _UNDOCUMENTED_SPEC + "\n" + _DOCUMENTED_SPEC.replace("solvency", "shares") + assert undocumented_filtered_vacuous(spec, [DEPOSIT]) == [] + + def test_multiple_methods_sorted(self): + spec = """\ +rule a(method f) filtered { f -> f.selector != sig:deposit(uint256).selector + && f.selector != sig:withdraw(uint256).selector } { + assert true; +} +""" + assert undocumented_filtered_vacuous(spec, [WITHDRAW, DEPOSIT]) == [DEPOSIT, WITHDRAW] From 806e6e13ca27dace4d93118aec5de930d1c4001a Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:15:47 +0300 Subject: [PATCH 02/13] Wire vacuity alert into prover reports and guard verify_spec stamping MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit run_prover now computes the per-run vacuity view, appends the repair-ladder block to the report string on every branch (vacuous methods usually surface as trivially-passing rules), and carries vacuous/instantiated methods on ProverReport. verify_spec persists detections in new ProverStateExtra.vacuous_methods (cleared when a later run re-instantiates the method healthily) and WITHHOLDS the PROVER validation stamp when a detected-vacuous method sits in a filtered block with no documented repair attempt — the escape hatch is a lenient comment check near the filter; the judge assesses quality. Co-Authored-By: Claude Fable 5 --- composer/prover/core.py | 24 +++++ composer/spec/source/author.py | 1 + composer/spec/source/prover.py | 54 ++++++++++- tests/test_vacuity.py | 166 ++++++++++++++++++++++++++++++++- 4 files changed, 241 insertions(+), 4 deletions(-) diff --git a/composer/prover/core.py b/composer/prover/core.py index 34d9289..7c0464d 100644 --- a/composer/prover/core.py +++ b/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), ) diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index a7e8df1..ad626d9 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -404,6 +404,7 @@ async def batch_cvl_generation( input=[], required_validations=[FEEDBACK_VALIDATION_KEY, PROVER_VALIDATION_KEY], rule_skips={}, + vacuous_methods={}, skipped=[], property_rules=[], validations={}, diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index c88490a..67df14d 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -27,8 +27,9 @@ from graphcore.graph import LLM from composer.prover.core import ( - ProverOptions, ProverCallbacks, run_prover, DefaultCexHandler + ProverOptions, ProverCallbacks, ProverReport, run_prover, DefaultCexHandler ) +from composer.prover.vacuity import format_filter_guard, undocumented_filtered_vacuous from composer.prover.callbacks import ProverEventCallbacks from composer.ui.tool_display import tool_display from composer.diagnostics.stream import ( @@ -50,6 +51,11 @@ def prover_config_overlay(base_config: dict, *, main_contract: str, verify_targe Shared by the live ``verify_spec`` run and the persisted ``certora/confs`` dump so the two can't drift. ``verify_target`` is the ``:`` the run verifies. + + ``rule_sanity``/``optimistic_loop`` are set AFTER the base-config spread, so they win + over anything the agent's config edits put in ``base_config``. Vacuity detection + (``composer/prover/vacuity.py``) depends on ``rule_sanity: basic`` being forced here — + which is also why ``edit_config``'s ``SetProverFlag`` refuses those two flags. """ return { **base_config, @@ -83,6 +89,12 @@ class ProverStateExtra(TypedDict): # Link of the last prover run this generation performed (URL or local results dir). # Last-write-wins; absent until the first prover run. Read at completion onto GeneratedCVL. prover_link: NotRequired[str | None] + # Methods detected as vacuous by prior prover runs (instantiation name -> diagnosis). + # Must persist across verify_spec calls: once the agent excludes a vacuous method with a + # `filtered` block, later runs never re-instantiate it, so per-run detection alone would + # forget it. Shares the DELETE_SKIP-sentinel reducer with rule_skips — an entry is cleared + # when a later run instantiates the method without a sanity failure. + vacuous_methods: Annotated[dict[str, str], _merge_rule_skips] type ProverEvents = CEXAnalysisStart | CloudPollingEvent | ProverOutputEvent | RuleAnalysisResult | ProverRun | ProverLink | ProverResult @@ -156,6 +168,30 @@ async def on_prover_result(self, results: dict[str, RuleResult]) -> None: ) +def _vacuity_state_update( + state: ProverStateExtra, result: ProverReport +) -> tuple[dict[str, str], set[str]]: + """Fold this run's vacuity view into the persisted ``vacuous_methods`` state. + + Returns ``(update, known_vacuous)``: the reducer delta to merge into state + (newly detected methods added, previously-recorded methods that this run + instantiated *without* a sanity failure cleared via DELETE_SKIP), and the + resulting set of methods still considered vacuous — the set the filtered- + vacuous guard checks against. ``state.get`` tolerates checkpoints predating + this field. + """ + prior = state.get("vacuous_methods", {}) + update: dict[str, str] = {m: ev.diagnosis for m, ev in result.vacuous_methods.items()} + for m in prior: + if m in result.instantiated_methods and m not in result.vacuous_methods: + update[m] = DELETE_SKIP + known_vacuous = { + m for m in (set(prior) | set(result.vacuous_methods)) + if update.get(m) != DELETE_SKIP + } + return update, known_vacuous + + class VerifySpecSchema(BaseModel): """ Run the Certora prover to verify the current spec against the source code. @@ -255,6 +291,7 @@ async def verify_spec( if isinstance(result, str): return result + vacuity_update, known_vacuous = _vacuity_state_update(state, result) all_verified = True for (r, stat) in result.rule_status.items(): if r in state["rule_skips"]: @@ -263,12 +300,25 @@ async def verify_spec( all_verified = False break if rules is None and all_verified: + # HARD GUARD: a detected-vacuous method sitting inside a `filtered` block + # makes the run pass trivially. Withhold the PROVER validation stamp + # unless a repair-ladder attempt is documented near the filter (the + # escape hatch — checked leniently; the judge assesses its quality). + blocked = undocumented_filtered_vacuous(state["curr_spec"], known_vacuous) + if blocked: + return tool_state_update( + tool_call_id=tool_call_id, + content=f"{result.result_str}\n\n{format_filter_guard(blocked)}", + prover_link=result.link, vacuous_methods=vacuity_update, + ) return tool_state_update( tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link, validations=stamper(state), + vacuous_methods=vacuity_update, ) return tool_state_update( - tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link + tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link, + vacuous_methods=vacuity_update, ) return verify_spec diff --git a/tests/test_vacuity.py b/tests/test_vacuity.py index 84722bc..fd8993a 100644 --- a/tests/test_vacuity.py +++ b/tests/test_vacuity.py @@ -1,16 +1,30 @@ """ Unit tests for composer/prover/vacuity.py: vacuous-method detection over -synthetic RuleResult sets, alert rendering, and the filtered-block / -documented-repair spec-text checks backing the verify_spec guard. +synthetic RuleResult sets, alert rendering, the filtered-block / +documented-repair spec-text checks, and the verify_spec hard guard that +withholds the PROVER validation stamp for undocumented filters of +detected-vacuous methods. """ +import pytest + +from composer.prover.core import ProverReport from composer.prover.ptypes import RulePath, RuleResult, StatusCodes from composer.prover.vacuity import ( + VacuityEvidence, detect_vacuous_methods, format_vacuity_alert, instantiated_methods, undocumented_filtered_vacuous, ) +from composer.spec.cvl_generation import check_completion +from composer.spec.source.author import ExpectRuleFailure +from composer.spec.source.prover import StateWithSkips, VALIDATION_KEY + +from graphcore.testing import Scenario, tool_call_raw, ToolCallDict +from graphcore.tools.results import result_tool_generator + +from .conftest import ProverMock, ProverToolResponse def _res(rule: str, method: str | None, status: StatusCodes) -> RuleResult: @@ -167,3 +181,151 @@ def test_multiple_methods_sorted(self): } """ assert undocumented_filtered_vacuous(spec, [WITHDRAW, DEPOSIT]) == [DEPOSIT, WITHDRAW] + + +# ========================================================================= +# verify_spec filtered-vacuous hard guard (mocked prover) +# ========================================================================= + +_PROVER = "verify_spec" +_RESULT = "result" + +_result_tool = result_tool_generator( + "result", + (str, "Commentary"), + "Signal completion", + validator=(StateWithSkips, lambda st, *_: check_completion(st)), +) + + +def _verify() -> ToolCallDict: + return tool_call_raw(_PROVER, rules=None) + + +def _result(commentary: str) -> ToolCallDict: + return tool_call_raw(_RESULT, value=commentary) + + +def _vacuous_report(*, rule_status: dict[str, bool], vacuous: dict[str, VacuityEvidence] | None = None, + instantiated: set[str] | None = None) -> ProverReport: + return ProverReport( + rule_status=rule_status, + result_str="Prover report output", + link="local://test-run", + vacuous_methods=vacuous or {}, + instantiated_methods=instantiated or set(), + ) + + +_DEPOSIT_EVIDENCE = { + DEPOSIT: VacuityEvidence( + method=DEPOSIT, affected_rules=["solvency"], diagnosis="sanity-failed in 1 of 1 rule(s)", + ) +} + + +def _guard_scenario(certora_prover: ProverMock, *responses: ProverToolResponse, curr_spec: str): + prover_tool = certora_prover(responses) + return Scenario(StateWithSkips, prover_tool, ExpectRuleFailure.as_tool("expect_rule_failure"), _result_tool).init( + curr_spec=curr_spec, + skipped=[], + property_rules=[], + validations={}, + required_validations=[VALIDATION_KEY], + rule_skips={}, + vacuous_methods={}, + config={"files": ["src/Foo.sol"]}, + ) + + +def _result_accepted(st: StateWithSkips) -> bool: + return "result" in st + + +class TestVerifySpecVacuityGuard: + """Run 1 detects the vacuous method; run 2 passes because the spec filters it. + The stamp must be withheld unless the filter documents a repair attempt.""" + + @pytest.mark.asyncio + async def test_undocumented_filter_withholds_stamp(self, certora_prover: ProverMock): + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": True}), + curr_spec=_UNDOCUMENTED_SPEC, + ) + accepted = await scenario.turns( + _verify(), + _verify(), + _result("done"), + ).map_run(_result_accepted) + assert not accepted + + @pytest.mark.asyncio + async def test_guard_message_names_method_and_ladder(self, certora_prover: ProverMock): + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": True}), + curr_spec=_UNDOCUMENTED_SPEC, + ) + msg = await scenario.turn(_verify()).turn(_verify()).run_last_single_tool(_PROVER) + assert "vacuity_filter_guard" in msg + assert "WITHHELD" in msg + assert DEPOSIT in msg + + @pytest.mark.asyncio + async def test_documented_filter_grants_stamp(self, certora_prover: ProverMock): + """Escape hatch: a repair-ladder attempt documented near the filter.""" + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": True}), + curr_spec=_DOCUMENTED_SPEC, + ) + accepted = await scenario.turns( + _verify(), + _verify(), + _result("done"), + ).map_run(_result_accepted) + assert accepted + + @pytest.mark.asyncio + async def test_no_filter_no_guard(self, certora_prover: ProverMock): + """A vacuous verdict alone never blocks — only filtering it does.""" + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": True}), + curr_spec=_NO_FILTER_SPEC, + ) + accepted = await scenario.turns( + _verify(), + _verify(), + _result("done"), + ).map_run(_result_accepted) + assert accepted + + @pytest.mark.asyncio + async def test_healthy_reinstantiation_clears_verdict(self, certora_prover: ProverMock): + """Run 2 instantiates the method without a sanity failure (the setup was + repaired) — the vacuity verdict clears and the filter no longer blocks.""" + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": True}, instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": True}), + curr_spec=_UNDOCUMENTED_SPEC, + ) + accepted = await scenario.turns( + _verify(), + _verify(), + _verify(), + _result("done"), + ).map_run(_result_accepted) + assert accepted From 0c3bdb972cf795417d03ca762e5a0be491864a05 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:50:05 +0300 Subject: [PATCH 03/13] Register edit_config and write_mock repair tools for the authoring agent MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ConfigEditTool (previously dead code) joins the tool list as edit_config, with a new SetProverFlag edit whitelisting optimistic_fallback, loop_iter (1-8), global_timeout (<=7200) and contract_recursion_limit (0-10) — rule_sanity/optimistic_loop are deliberately excluded because vacuity detection depends on prover_config_overlay forcing them. write_mock writes a minimal Solidity mock to the real project tree, confined to certora/mocks (mirroring the harness generator's VFS confinement). Co-Authored-By: Claude Fable 5 --- composer/spec/source/author.py | 110 +++++++++++++++++++++++++++++++-- tests/test_config_edit.py | 87 +++++++++++++++++++++++++- tests/test_write_mock.py | 57 +++++++++++++++++ 3 files changed, 249 insertions(+), 5 deletions(-) create mode 100644 tests/test_write_mock.py diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index ad626d9..9b9085a 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -6,7 +6,8 @@ from pydantic import Field, BaseModel, Discriminator from graphcore.tools.schemas import ( - WithAsyncImplementation, WithImplementation, WithInjectedId, WithInjectedState, + WithAsyncDependencies, WithAsyncImplementation, WithImplementation, WithInjectedId, + WithInjectedState, ) from graphcore.graph import tool_state_update from graphcore.summary import SummaryConfig @@ -22,7 +23,7 @@ from composer.spec.source.prover import ProverStateExtra, DELETE_SKIP, VALIDATION_KEY as PROVER_VALIDATION_KEY from langgraph.graph import MessagesState from langgraph.runtime import get_runtime -from pathlib import Path +from pathlib import Path, PurePosixPath from composer.spec.gen_types import CVLResource, TypedTemplate, import_statement_for from composer.spec.service_host import ServiceHost from composer.workflow.services import CacheLevel @@ -245,8 +246,54 @@ class RemoveLink(BaseModel): source_contract_name : SolidityIdentifier = Field(description="The Solidity identifier of the contract whose link should be removed") link_field_name : str = Field(description="The storage field holding the link within `source_contract_name` that should be removed") -type ConfigEdit = Annotated[RemoveLink | AddLink | AddFile | RemoveFile, Discriminator("type")] +class SetProverFlag(BaseModel): + """ + Set a whitelisted top-level prover flag in the configuration: + + * `optimistic_fallback` (bool): assume unresolved low-level calls (`.call{value: ...}`, `send`, + `transfer`) succeed instead of HAVOCing and always being able to fail. Step 3 of the vacuity + repair ladder. + * `loop_iter` (int, 1-8): the number of loop unrollings the prover performs. + * `global_timeout` (int, 1-7200): the overall run timeout in seconds. + * `contract_recursion_limit` (int, 0-10): the allowed depth of recursive calls between contracts. + """ + # `rule_sanity` and `optimistic_loop` are DELIBERATELY not in this whitelist: vacuity + # detection (composer/prover/vacuity.py) depends on `rule_sanity: basic`, and + # `prover_config_overlay` sets both AFTER spreading the base config so they would win + # anyway — the whitelist keeps the agent from even trying (and from being confused by a + # silently-overridden edit). + type: Literal["set_flag"] + flag: Literal["optimistic_fallback", "loop_iter", "global_timeout", "contract_recursion_limit"] + value: bool | int = Field(description="The value to set: a bool for `optimistic_fallback`, an int for the other flags") + +def _validate_prover_flag(flag: str, value: bool | int) -> str | None: + """Per-flag validation for SetProverFlag; returns an error message or None if valid. + + NB: ``bool`` is a subclass of ``int``, so the bool checks must come before any int check. + """ + if flag == "optimistic_fallback": + if not isinstance(value, bool): + return f"optimistic_fallback expects a boolean value, got {value!r}" + return None + if isinstance(value, bool) or not isinstance(value, int): + return f"{flag} expects an integer value, got {value!r}" + match flag: + case "loop_iter": + if not (1 <= value <= 8): + return f"loop_iter must be between 1 and 8, got {value}" + case "global_timeout": + if not (1 <= value <= 7200): + return f"global_timeout must be between 1 and 7200 (seconds), got {value}" + case "contract_recursion_limit": + if not (0 <= value <= 10): + return f"contract_recursion_limit must be between 0 and 10, got {value}" + return None + +type ConfigEdit = Annotated[RemoveLink | AddLink | AddFile | RemoveFile | SetProverFlag, Discriminator("type")] +@tool_display( + lambda p: f"Editing prover configuration ({len(p['edits'])} edit(s))", None +) class ConfigEditTool(WithAsyncImplementation[Command | str], WithInjectedId, WithInjectedState[ProverStateExtra]): """ Call this tool to make a edits to the prover configuration. @@ -322,6 +369,10 @@ async def run(self) -> Command | str: if not found: return f"No existing link found that matches {src}:{fld}" curr_config["link"] = new_links + case SetProverFlag(flag=flag, value=value): + if (err := _validate_prover_flag(flag, value)) is not None: + return err + curr_config[flag] = value return tool_state_update( self.tool_call_id, @@ -330,6 +381,48 @@ async def run(self) -> Command | str: ) +# The only directory write_mock may write into, mirroring the harness generator's VFS +# confinement (`forbidden_write="^(?!certora/harnesses)"` in harness.py) — but enforced +# directly here because the authoring agent's source tools are read-only over the real +# project tree and the prover compiles from the real tree, so the mock must land on disk. +MOCKS_DIR = PurePosixPath("certora/mocks") + + +@tool_display(lambda p: f"Writing mock `{p['file_path']}`", None) +class WriteMockTool(WithAsyncDependencies[str, str]): + """ + Write a minimal Solidity mock contract under `certora/mocks` implementing an interface, so + the prover can resolve calls to an otherwise-unresolved callee (step 2 of the vacuity repair + ladder). After writing the mock, register it in the prover configuration with `edit_config` + (an `add_file` edit, plus an `add_link` edit if the callee is reached through a storage field). + + Keep the mock as small as possible: implement only the interface the caller needs, but + preserve the semantics that matter to the calling contract — in particular a `payable` + callee must remain `payable`. Writing to an existing path overwrites it, so you can iterate + on a mock in place. + """ + file_path: str = Field(description=f"Project-root-relative path for the mock, under `{MOCKS_DIR}` (e.g. `{MOCKS_DIR}/MockOracle.sol`)") + content: str = Field(description="The full Solidity source of the mock contract") + + @override + async def run(self) -> str: + rel = PurePosixPath(self.file_path) + if rel.is_absolute() or ".." in rel.parts: + return f"Invalid path `{self.file_path}`: must be a project-root-relative path without `..`" + if rel.parts[:len(MOCKS_DIR.parts)] != MOCKS_DIR.parts or len(rel.parts) <= len(MOCKS_DIR.parts): + return f"You may only write into the `{MOCKS_DIR}` directory (got `{self.file_path}`)" + if rel.suffix != ".sol": + return f"Mock must be a Solidity source file (`.sol`), got `{self.file_path}`" + with self.tool_deps() as project_root: + target = Path(project_root) / rel + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text(self.content) + return ( + f"Wrote mock to `{self.file_path}`. Remember to register it in the prover configuration " + "via `edit_config` (`add_file`, plus `add_link` if the callee is reached through a storage field)." + ) + + _PropertyGenTemplate = TypedTemplate[PropertyGenParams]("property_generation_prompt.j2") async def batch_cvl_generation( @@ -371,7 +464,16 @@ async def batch_cvl_generation( ).with_tools( static_tools() ).with_tools( - [prover_tool, ExpectRulePassage.as_tool("expect_rule_passage"), ExpectRuleFailure.as_tool("expect_rule_failure"), GiveUpTool.as_tool("give_up"), PublishResultTool.as_tool("result"), ctx.get_memory_tool()] + [ + prover_tool, ExpectRulePassage.as_tool("expect_rule_passage"), ExpectRuleFailure.as_tool("expect_rule_failure"), + GiveUpTool.as_tool("give_up"), PublishResultTool.as_tool("result"), + # Setup-repair tools for the vacuity repair ladder: edit_config covers ladder + # steps 2 (register a mock via add_file/add_link) and 3 (optimistic_fallback via + # set_flag); write_mock produces the step-2 mock itself. + ConfigEditTool.as_tool("edit_config"), + WriteMockTool.bind(source.project_root).as_tool("write_mock"), + ctx.get_memory_tool(), + ] ).with_state( SourceCVLGenerationState ).with_output_key( diff --git a/tests/test_config_edit.py b/tests/test_config_edit.py index 6f261e9..965d491 100644 --- a/tests/test_config_edit.py +++ b/tests/test_config_edit.py @@ -5,11 +5,12 @@ not just correct Command objects. """ import pytest +from pydantic import ValidationError from langgraph.graph import MessagesState from composer.spec.source.author import ( - ConfigEditTool, AddFile, RemoveFile, AddLink, RemoveLink, + ConfigEditTool, AddFile, RemoveFile, AddLink, RemoveLink, SetProverFlag, ) from composer.spec.source.prover import ProverStateExtra @@ -52,6 +53,12 @@ def _remove_link(src: str, field: str) -> dict: return RemoveLink(type="remove_link", source_contract_name=src, link_field_name=field).model_dump() +def _set_flag(flag: str, value: bool | int) -> dict: + # Raw dict (not SetProverFlag.model_dump()) so tests can exercise values the + # schema itself would reject before reaching the per-flag validation. + return {"type": "set_flag", "flag": flag, "value": value} + + def _edit(*edits: dict) -> ToolCallDict: return tool_call_raw(_EDIT, edits=list(edits)) @@ -200,6 +207,84 @@ async def test_remove_link_not_found(self): assert links == ["A:b=C"] +# ========================================================================= +# SetProverFlag +# ========================================================================= + + +class TestSetProverFlag: + async def test_set_optimistic_fallback(self): + config = await _scenario(files=[]).turn( + _edit(_set_flag("optimistic_fallback", True)), + ).map_run(_config) + assert config["optimistic_fallback"] is True + + async def test_optimistic_fallback_rejects_int(self): + config = await _scenario(files=[]).turn( + _edit(_set_flag("optimistic_fallback", 1)), + ).map_run(_config) + assert "optimistic_fallback" not in config + + async def test_set_loop_iter(self): + config = await _scenario(files=[]).turn( + _edit(_set_flag("loop_iter", 3)), + ).map_run(_config) + assert config["loop_iter"] == 3 + + async def test_loop_iter_out_of_range(self): + for bad in (0, 9): + config = await _scenario(files=[]).turn( + _edit(_set_flag("loop_iter", bad)), + ).map_run(_config) + assert "loop_iter" not in config + + async def test_loop_iter_rejects_bool(self): + """bool is an int subclass; the validator must not accept True as a loop count.""" + config = await _scenario(files=[]).turn( + _edit(_set_flag("loop_iter", True)), + ).map_run(_config) + assert "loop_iter" not in config + + async def test_set_global_timeout(self): + config = await _scenario(files=[]).turn( + _edit(_set_flag("global_timeout", 3600)), + ).map_run(_config) + assert config["global_timeout"] == 3600 + + async def test_global_timeout_too_large(self): + config = await _scenario(files=[]).turn( + _edit(_set_flag("global_timeout", 7201)), + ).map_run(_config) + assert "global_timeout" not in config + + async def test_set_contract_recursion_limit(self): + config = await _scenario(files=[]).turn( + _edit(_set_flag("contract_recursion_limit", 2)), + ).map_run(_config) + assert config["contract_recursion_limit"] == 2 + + async def test_contract_recursion_limit_too_large(self): + config = await _scenario(files=[]).turn( + _edit(_set_flag("contract_recursion_limit", 11)), + ).map_run(_config) + assert "contract_recursion_limit" not in config + + async def test_sanity_and_optimistic_loop_not_settable(self): + """The flags vacuity detection depends on (forced by prover_config_overlay) + are rejected at the schema level, not just by run-time validation.""" + for forbidden in ("rule_sanity", "optimistic_loop"): + with pytest.raises(ValidationError): + SetProverFlag(type="set_flag", flag=forbidden, value=True) # type: ignore[arg-type] + + async def test_failed_flag_aborts_batch(self): + """Atomicity: a rejected flag value rolls back the whole edit list.""" + config = await _scenario(files=[]).turn( + _edit(_set_flag("loop_iter", 3), _set_flag("global_timeout", 99999)), + ).map_run(_config) + assert "loop_iter" not in config + assert "global_timeout" not in config + + # ========================================================================= # Multiple edits # ========================================================================= diff --git a/tests/test_write_mock.py b/tests/test_write_mock.py new file mode 100644 index 0000000..f4eefec --- /dev/null +++ b/tests/test_write_mock.py @@ -0,0 +1,57 @@ +""" +Tests for the write_mock tool: real-filesystem writes confined to certora/mocks. +""" +import pytest + +from composer.spec.source.author import WriteMockTool + +pytestmark = pytest.mark.asyncio + + +_CONTENT = "// SPDX-License-Identifier: MIT\ncontract MockOracle { function price() external pure returns (uint256) { return 1; } }\n" + + +def _tool(project_root) -> object: + return WriteMockTool.bind(str(project_root)).as_tool("write_mock") + + +async def test_writes_under_mocks_dir(tmp_path): + res = await _tool(tmp_path).ainvoke( + {"file_path": "certora/mocks/MockOracle.sol", "content": _CONTENT} + ) + written = tmp_path / "certora" / "mocks" / "MockOracle.sol" + assert written.read_text() == _CONTENT + # The result must nudge the agent to register the mock in the prover config. + assert "edit_config" in res + + +async def test_overwrite_allowed(tmp_path): + tool = _tool(tmp_path) + await tool.ainvoke({"file_path": "certora/mocks/M.sol", "content": "// v1"}) + await tool.ainvoke({"file_path": "certora/mocks/M.sol", "content": "// v2"}) + assert (tmp_path / "certora" / "mocks" / "M.sol").read_text() == "// v2" + + +async def test_rejects_write_outside_mocks(tmp_path): + for bad in ( + "src/Evil.sol", + "certora/harnesses/Evil.sol", + "certora/mocks.sol", # file named like the dir, still outside it + ): + res = await _tool(tmp_path).ainvoke({"file_path": bad, "content": _CONTENT}) + assert "only write into" in res + assert not (tmp_path / "src").exists() + + +async def test_rejects_traversal_and_absolute(tmp_path): + for bad in ("certora/mocks/../../etc/Evil.sol", "/certora/mocks/Evil.sol"): + res = await _tool(tmp_path).ainvoke({"file_path": bad, "content": _CONTENT}) + assert "Invalid path" in res + + +async def test_rejects_non_solidity(tmp_path): + res = await _tool(tmp_path).ainvoke( + {"file_path": "certora/mocks/notes.txt", "content": "hi"} + ) + assert ".sol" in res + assert not (tmp_path / "certora" / "mocks" / "notes.txt").exists() From 38cad69c1045645e0c22ee5e854cfad635dbe335 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:51:50 +0300 Subject: [PATCH 04/13] Teach author and judge prompts the vacuity repair ladder The SANITY_FAILURE remediation bullet now distinguishes a rule-local require conflict from cross-rule method vacuity and prescribes the ordered repair ladder (summary fix -> write_mock + edit_config -> optimistic_fallback -> documented filtered); the filtered bullet makes undocumented filtering of a vacuous method non-terminal. Judge Criteria 5 calls out NONDET-on-payable explicitly and rejects filtered blocks that hide a repairable-summary sanity failure without a documented repair attempt. Co-Authored-By: Claude Fable 5 --- .../templates/property_generation_prompt.j2 | 34 +++++++++++++++---- composer/templates/property_judge_prompt.j2 | 9 +++++ 2 files changed, 37 insertions(+), 6 deletions(-) diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index d96585c..b5c89d7 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -75,21 +75,43 @@ feedback as soon as possible. (unknown) callee contract's state, you should use "ghost variables" to model this. + If the call was completely unresolved (no resolved selector/signature), consider using a "dispatch list" summary. Analyze the location of the unresolved call, and consider what the callee functions might be. + + If the unresolved call is a low-level `.call{value: ...}`/`send`/`transfer` with no resolvable target, + the HAVOC also lets the call *always fail*, which can make the caller revert on every path. Setting + `optimistic_fallback` via the `edit_config` tool (`set_flag`) assumes such calls succeed instead. + Do *NOT* try to mark ghost state as `persistent` to work around the HAVOC issue. + Do *NOT* apply a `NONDET` summary to a side-effecting function to make the HAVOC "go away", this makes the verification results useless. * If the counterexample appears to point to a potential issue in the code that should be reviewed by a security expert, use the "expect fail" tool to mark that the rule failure may be legitimate. +* If the property or invariant is genuinely incorrect or actually invalid you may mark the property as "skipped" and + remove your attempts to formalize it from the spec +* If the rule is failing due to a `SANITY_FAILURE`, this is due to the assertion in the rule/invariant being unreachable. + Diagnose which of two distinct root causes you are facing before acting: + + If the sanity failure is specific to a single rule, the preconditions in the rule and the logical encoding of the + implementation's code are themselves mutually unsatisfiable. In this case, you should try to identify places where + `require` statements in your rule may conflict with any assumptions/requirements in the code. + + If the *same method* sanity-fails across several rules that instantiate it (the prover report will flag this with a + `` block), the method reverts on *every* path under the current verification model, and every rule + instantiated with it passes vacuously. This is almost always a SETUP defect, not a property error — canonically a + `NONDET`/`CONSTANT` summary on a payable or side-effecting callee, an unresolved `.call{value: ...}` that HAVOCs, + or a missing `link`. Repair it 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` with the `write_mock` tool, implementing the callee's + interface, and register it in the prover config with `edit_config` (`add_file`, plus `add_link` 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, exclude the method with a `filtered` block — see below. * If you have a parametric rule or invariant that is persistently failing on a method, and that method should genuinely be excluded from the property/invariant being proven, use a `filtered` block to exclude it. + You should not use this strategy lightly; only do so when you are 95% certain that the method in question should be excluded from the property. -* If the property or invariant is genuinely incorrect or actually invalid you may mark the property as "skipped" and - remove your attempts to formalize it from the spec -* If the rule is failing due to a `SANITY_FAILURE`, this is due to the assertion in the rule/invariant being unreachable. - In other words, the preconditions in the rule and the logical encoding of the implementation's code are themselves - mutually unsatisfiable. In this case, you should try to identify places where `require` statements in your rule - may conflict with any assumptions/requirements in the code. + + NEVER use a `filtered` block to hide a *vacuous* method (one flagged in a ``): that hides a setup + defect instead of fixing it, and the prover validation stamp will be withheld. If steps 1-3 of the repair ladder + genuinely failed, you may filter the method, but the justification comment next to the filter MUST name which of + summary-fix / mock / `optimistic_fallback` you attempted and why each failed. * For any other logical errors/issues not described here, address the changes in a methodical way. Use your adaptive thinking and the cvl researcher to come to *principled* solutions. Do *NOT* try to brute force the solution by trying random changes. diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 537b2af..7ab7813 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -140,6 +140,15 @@ Consider if any of the summaries added in the spec *trivialize* the verification if the specification summarizes away an invocation of a contract function which moves balances as "NONDET", then this effectively makes any balance transfers a NO-OP, which in turn trivializes any property that reasons about balances. +A `NONDET` summary on a *payable* callee deserves explicit scrutiny: it drops the callee's ability to accept `msg.value`, which typically makes +every caller revert on all paths, so any rule instantiated with those callers holds *vacuously*. + +A `filtered` block that excludes a method whose sanity failure stems from such a repairable summary is the same trivialization in disguise: +the setup defect is hidden rather than fixed, and the property silently loses coverage of that method. Reject such filters unless their +justification documents that the root-cause repairs were attempted and why each failed (fixing/replacing the offending summary while preserving +payable semantics, providing a mock for the callee, or enabling `optimistic_fallback`). An undocumented filter of a vacuously-passing method +must be rejected. + ### Criteria 6: Manifest Errors {% if sort != "greenfield" %} From 734c5f5b3412ea884e87f46777f13559594f1c62 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 21:59:21 +0300 Subject: [PATCH 05/13] Prevent vacuity at autosetup time: payable-NONDET guard + optimistic_fallback recommendation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit NONDET recipes are bounded to view/pure both declaratively (inline- assembly recipe properties) and at match time via _nondet_ineligible, which consumes MethodParser.get_payable_methods() as defense in depth over the emit-time view/pure check — a NONDET summary on a payable or state-mutating callee erases its effects and makes callers vacuously revert. Call resolution now records a structured optimistic_fallback recommendation when unresolved low-level value transfers remain (.call{value}/send/transfer with no resolvable target), and the autosetup call site merges it into the conf through the new ConfigManager extra-flags whitelist (create_config extra_flags / apply_extra_flags). Co-Authored-By: Claude Fable 5 --- certora_autosetup/autosetup/autosetup.py | 14 ++ certora_autosetup/setup/call_resolution.py | 42 ++++ certora_autosetup/setup/setup_summaries.py | 52 ++++- .../utils/enhanced_config_manager.py | 46 +++++ tests/test_autosetup_vacuity_prevention.py | 185 ++++++++++++++++++ 5 files changed, 338 insertions(+), 1 deletion(-) create mode 100644 tests/test_autosetup_vacuity_prevention.py diff --git a/certora_autosetup/autosetup/autosetup.py b/certora_autosetup/autosetup/autosetup.py index 52bef8f..f79905f 100644 --- a/certora_autosetup/autosetup/autosetup.py +++ b/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: diff --git a/certora_autosetup/setup/call_resolution.py b/certora_autosetup/setup/call_resolution.py index 22efe5a..cace954 100644 --- a/certora_autosetup/setup/call_resolution.py +++ b/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 diff --git a/certora_autosetup/setup/setup_summaries.py b/certora_autosetup/setup/setup_summaries.py index 14cc96e..06471f2 100755 --- a/certora_autosetup/setup/setup_summaries.py +++ b/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", ), ] diff --git a/certora_autosetup/utils/enhanced_config_manager.py b/certora_autosetup/utils/enhanced_config_manager.py index 186b888..20831f5 100644 --- a/certora_autosetup/utils/enhanced_config_manager.py +++ b/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", []) diff --git a/tests/test_autosetup_vacuity_prevention.py b/tests/test_autosetup_vacuity_prevention.py new file mode 100644 index 0000000..d82d439 --- /dev/null +++ b/tests/test_autosetup_vacuity_prevention.py @@ -0,0 +1,185 @@ +""" +Tests for the autosetup-side vacuity prevention (plan Part D): + +- NONDET recipes never match payable / state-mutating methods + (``SummarySetup._nondet_ineligible`` + the recipe-level mutability bounds); +- unresolved low-level value transfers yield an ``optimistic_fallback`` + recommendation (``is_unresolved_value_transfer``); +- ``ConfigManager`` merges recommended flags only through its whitelist. +""" +import json + +import pytest + +from certora_autosetup.setup.call_resolution import is_unresolved_value_transfer +from certora_autosetup.setup.setup_summaries import Recipe, RecipeType, SummarySetup +from certora_autosetup.utils.enhanced_config_manager import ConfigManager + +from prover_output_utility.models import CallResolutionInfo + + +# --------------------------------------------------------------------------- +# NONDET recipe eligibility +# --------------------------------------------------------------------------- + + +_NONDET_RECIPE = Recipe( + recipe_type=RecipeType.CUSTOM, + characteristic="anything", + properties={}, + summary_type="NONDET", +) + + +def _method(name: str, mutability: str, contract: str = "Bank") -> dict: + return {"contractName": contract, "name": name, "stateMutability": mutability} + + +class TestNondetIneligible: + def test_payable_excluded(self): + m = _method("deposit", "payable") + assert SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, {("Bank", "deposit")}) + + def test_payable_excluded_even_without_key(self): + """The mutability fallback catches a payable method missing from the key set.""" + m = _method("deposit", "payable") + assert SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, set()) + + def test_state_mutating_excluded(self): + m = _method("withdraw", "nonpayable") + assert SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, set()) + + def test_view_and_pure_allowed(self): + for mutability in ("view", "pure"): + m = _method("peek", mutability) + assert not SummarySetup._nondet_ineligible(_NONDET_RECIPE, m, set()) + + def test_non_nondet_recipe_unaffected(self): + recipe = Recipe( + recipe_type=RecipeType.NEW_CONTRACT, + characteristic="anything", + properties={}, + summary_type="HAVOC_ALL_DELETE", + ) + m = _method("deploy", "payable") + assert not SummarySetup._nondet_ineligible(recipe, m, {("Bank", "deploy")}) + + +def test_default_nondet_recipes_bounded_to_view_pure(): + """Every default NONDET recipe must declaratively restrict stateMutability to + view/pure — the recipe-level arm of the payable-NONDET guard.""" + # Unbound call with a stub self: SummarySetup.__init__ requires prebuilt + # compilation-analysis artifacts, and _build_recipes only touches self.log + # (and only on the custom-recipe branch, unused here). + class _StubSetup: + def log(self, *args, **kwargs): + pass + + for recipe in SummarySetup._build_recipes(_StubSetup(), None): + if recipe.summary_type.upper() != "NONDET": + continue + bound = recipe.properties.get("stateMutability") + bound_values = bound if isinstance(bound, list) else [bound] + assert set(bound_values) <= {"view", "pure"}, ( + f"NONDET recipe {recipe.recipe_type} admits non-view/pure methods: {bound!r}" + ) + + +# --------------------------------------------------------------------------- +# optimistic_fallback recommendation predicate +# --------------------------------------------------------------------------- + + +def _call(snippet: str, callee: str = "[?].[?]", selector: str | None = None) -> CallResolutionInfo: + return CallResolutionInfo( + callee_name=callee, + caller_name="Bank.withdraw(uint256)", + call_site_snippet=snippet, + source_location="src/Bank.sol:42", + summary="AUTO havoc", + is_warning=True, + callee_resolution="UNRESOLVED", + selector=selector, + ) + + +class TestUnresolvedValueTransfer: + def test_call_value_flagged(self): + assert is_unresolved_value_transfer(_call('recipient.call{value: amount}("")')) + + def test_call_value_with_spaces_flagged(self): + assert is_unresolved_value_transfer(_call('recipient.call{ value : amount }("")')) + + def test_native_send_and_transfer_flagged(self): + assert is_unresolved_value_transfer(_call("payable(to).send(amount)")) + assert is_unresolved_value_transfer(_call("payable(to).transfer(amount)")) + + def test_erc20_transfer_with_selector_not_flagged(self): + """High-level token.transfer carries a resolvable selector — not a native transfer.""" + call = _call( + "token.transfer(to, amount)", + callee="[?].transfer(address,uint256)", + selector="0xa9059cbb", + ) + assert not is_unresolved_value_transfer(call) + + def test_plain_unresolved_call_not_flagged(self): + assert not is_unresolved_value_transfer( + _call("oracle.latestAnswer()", callee="[?].latestAnswer()") + ) + + +# --------------------------------------------------------------------------- +# ConfigManager extra-flags whitelist +# --------------------------------------------------------------------------- + + +@pytest.fixture +def manager(tmp_path) -> ConfigManager: + return ConfigManager(project_root=tmp_path) + + +def _create(manager, tmp_path, **kwargs): + spec = tmp_path / "certora" / "specs" / "Bank.spec" + spec.parent.mkdir(parents=True, exist_ok=True) + spec.write_text("// spec") + conf_path = tmp_path / "Bank.conf" + return manager.create_config( + "Bank", [], [], spec, conf_path=conf_path, **kwargs + ) + + +class TestExtraFlags: + def test_create_config_merges_whitelisted(self, manager, tmp_path): + created = _create( + manager, tmp_path, + extra_flags={"optimistic_fallback": True, "contract_recursion_limit": 2}, + ) + conf = json.loads(created.path.read_text()) + assert conf["optimistic_fallback"] is True + assert conf["contract_recursion_limit"] == 2 + + def test_create_config_rejects_non_whitelisted(self, manager, tmp_path): + # rule_sanity in particular: vacuity detection depends on the forced value. + for flag in ("rule_sanity", "optimistic_loop", "loop_iter"): + with pytest.raises(ValueError): + _create(manager, tmp_path, extra_flags={flag: True}) + + def test_create_config_rejects_ill_typed_values(self, manager, tmp_path): + with pytest.raises(ValueError): + _create(manager, tmp_path, extra_flags={"optimistic_fallback": 1}) + with pytest.raises(ValueError): + _create(manager, tmp_path, extra_flags={"contract_recursion_limit": True}) + with pytest.raises(ValueError): + _create(manager, tmp_path, extra_flags={"contract_recursion_limit": 99}) + + def test_apply_extra_flags_updates_existing_conf(self, manager, tmp_path): + created = _create(manager, tmp_path) + manager.apply_extra_flags(created.path, {"optimistic_fallback": True}) + conf = json.loads(created.path.read_text()) + assert conf["optimistic_fallback"] is True + + def test_apply_extra_flags_rejects_non_whitelisted(self, manager, tmp_path): + created = _create(manager, tmp_path) + with pytest.raises(ValueError): + manager.apply_extra_flags(created.path, {"rule_sanity": "none"}) From 3aa952bff9b6ea0052f527a368be2c27786625db Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 3 Jul 2026 22:19:03 +0300 Subject: [PATCH 06/13] Harden the vacuity guard: token-boundary filter matching, expect_rule_failure bypass Review fixes: - undocumented_filtered_vacuous matched the bare method name as a raw substring of the filter body, so vacuous `deposit` collided with a filter excluding only `depositAll` and could spuriously withhold the stamp. Match on a token boundary instead. - The guard was bypassable without filtering: marking each sanity-failing rule of a vacuous method "expected to fail" drops it from the all-verified check with the method never entering a filter body. New undocumented_skipped_vacuous applies the same documented-repair-attempt escape hatch to rule-skip reasons, verify_spec withholds the stamp via a message, and the author prompts forbid the shortcut explicitly. Co-Authored-By: Claude Fable 5 --- composer/prover/vacuity.py | 58 ++++++++- composer/spec/source/prover.py | 27 ++-- .../templates/property_generation_prompt.j2 | 3 + .../property_generation_system_prompt.j2 | 4 + tests/test_vacuity.py | 117 +++++++++++++++++- 5 files changed, 196 insertions(+), 13 deletions(-) diff --git a/composer/prover/vacuity.py b/composer/prover/vacuity.py index fbd169d..b99102a 100644 --- a/composer/prover/vacuity.py +++ b/composer/prover/vacuity.py @@ -6,8 +6,9 @@ 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, -renders the ```` the agent sees, and provides the spec-text -checks backing the ``verify_spec`` filtered-vacuous guard. +renders the ```` the agent sees, and provides the checks backing +the ``verify_spec`` vacuity guards (undocumented ``filtered`` exclusions and +undocumented ``expect_rule_failure`` skips of the affected rules). 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 @@ -136,6 +137,29 @@ def format_filter_guard(blocked: list[str]) -> str: """ +def format_skip_guard(blocked: list[str]) -> str: + """Render the message returned by ``verify_spec`` when it withholds the + PROVER validation stamp because the sanity-failing rules of vacuous methods + were marked "expected to fail" without a documented repair attempt.""" + method_list = "\n".join(f" - {m}" for m in sorted(blocked)) + return f"""\ + +The PROVER validation stamp was WITHHELD. The following method(s) are VACUOUS (they revert on +every path under the current verification model) and their sanity-failing rules were marked +"expected to fail" via `expect_rule_failure` with no documented repair attempt: +{method_list} + +Marking those rules as expected failures hides a setup defect just like filtering the method would. +Either: + * repair the root cause (repair ladder: 1. fix/replace the offending summary preserving payable + semantics, 2. `write_mock` + `edit_config` AddFile/AddLink, 3. `optimistic_fallback` via + `edit_config` set_flag), un-mark the rules with `expect_rule_passage`, and rerun `verify_spec`; or + * if steps 1-3 genuinely failed, re-call `expect_rule_failure` with a reason documenting which of + summary-fix / mock / optimistic_fallback you attempted and why each failed, then rerun + `verify_spec`. The feedback judge will assess the quality of that justification. +""" + + def _bare_method_name(method: str) -> str: """``Bank.withdraw(uint256)`` -> ``withdraw``. Prover method-instantiation names are contract-qualified with a parameter list; filter expressions @@ -198,8 +222,34 @@ def undocumented_filtered_vacuous(spec: str, methods: Iterable[str]) -> list[str blocks = _filtered_blocks_with_context(spec) blocked: list[str] = [] for method in methods: - bare = _bare_method_name(method) - containing = [ctx for (ctx, body) in blocks if bare in body] + # Token-boundary match, not raw substring: a filter excluding only + # `depositAll` must not count as containing the vacuous `deposit`. + name_re = re.compile(rf"\b{re.escape(_bare_method_name(method))}\b") + containing = [ctx for (ctx, body) in blocks if name_re.search(body)] if containing and not any(_documents_repair_attempt(ctx) for ctx in containing): blocked.append(method) return sorted(blocked) + + +def undocumented_skipped_vacuous( + evidence: dict[str, VacuityEvidence], rule_skips: dict[str, str] +) -> list[str]: + """The subset of this run's vacuous methods with a sanity-failing rule + excluded from the pass/fail verdict via a rule skip (``expect_rule_failure``) + whose reason does not document a repair-ladder attempt. + + Closes the other mechanical bypass of the filtered-vacuous guard: instead of + filtering the method, the agent can mark each of its sanity-failing rules + "expected to fail" — those rules then drop out of ``verify_spec``'s + all-verified check while the method never enters a filter body. Works off + the current run's evidence (not the persisted verdicts) because only it + names the affected rules; in the skip scenario the method stays + instantiated, so detection re-fires on every run. Mirrors the filter + check's leniency: one documented skip reason covering the method clears it. + """ + blocked: list[str] = [] + for method, ev in evidence.items(): + reasons = [rule_skips[r] for r in ev.affected_rules if r in rule_skips] + if reasons and not any(_documents_repair_attempt(reason) for reason in reasons): + blocked.append(method) + return sorted(blocked) diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index 67df14d..9ee0723 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -29,7 +29,10 @@ from composer.prover.core import ( ProverOptions, ProverCallbacks, ProverReport, run_prover, DefaultCexHandler ) -from composer.prover.vacuity import format_filter_guard, undocumented_filtered_vacuous +from composer.prover.vacuity import ( + format_filter_guard, format_skip_guard, + undocumented_filtered_vacuous, undocumented_skipped_vacuous, +) from composer.prover.callbacks import ProverEventCallbacks from composer.ui.tool_display import tool_display from composer.diagnostics.stream import ( @@ -301,14 +304,24 @@ async def verify_spec( break if rules is None and all_verified: # HARD GUARD: a detected-vacuous method sitting inside a `filtered` block - # makes the run pass trivially. Withhold the PROVER validation stamp - # unless a repair-ladder attempt is documented near the filter (the - # escape hatch — checked leniently; the judge assesses its quality). - blocked = undocumented_filtered_vacuous(state["curr_spec"], known_vacuous) - if blocked: + # makes the run pass trivially — and so does marking its sanity-failing + # rules "expected to fail", which drops them from the all_verified check + # above. Withhold the PROVER validation stamp in both cases unless a + # repair-ladder attempt is documented (near the filter / in the skip + # reason — the escape hatch, checked leniently; the judge assesses + # its quality). + filter_blocked = undocumented_filtered_vacuous( + state["curr_spec"], known_vacuous + ) + skip_blocked = undocumented_skipped_vacuous( + result.vacuous_methods, state["rule_skips"] + ) + if filter_blocked or skip_blocked: + guards = ([format_filter_guard(filter_blocked)] if filter_blocked else []) \ + + ([format_skip_guard(skip_blocked)] if skip_blocked else []) return tool_state_update( tool_call_id=tool_call_id, - content=f"{result.result_str}\n\n{format_filter_guard(blocked)}", + content="\n\n".join([result.result_str, *guards]), prover_link=result.link, vacuous_methods=vacuity_update, ) return tool_state_update( diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index b5c89d7..dff173d 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -112,6 +112,9 @@ feedback as soon as possible. defect instead of fixing it, and the prover validation stamp will be withheld. If steps 1-3 of the repair ladder genuinely failed, you may filter the method, but the justification comment next to the filter MUST name which of summary-fix / mock / `optimistic_fallback` you attempted and why each failed. + + The same applies to `expect_rule_failure`: marking a vacuous method's sanity-failing rules as "expected to fail" + hides the identical setup defect and likewise withholds the prover validation stamp, unless the reason you record + names which of summary-fix / mock / `optimistic_fallback` you attempted and why each failed. * For any other logical errors/issues not described here, address the changes in a methodical way. Use your adaptive thinking and the cvl researcher to come to *principled* solutions. Do *NOT* try to brute force the solution by trying random changes. diff --git a/composer/templates/property_generation_system_prompt.j2 b/composer/templates/property_generation_system_prompt.j2 index 6a3cd77..f5e9ab3 100644 --- a/composer/templates/property_generation_system_prompt.j2 +++ b/composer/templates/property_generation_system_prompt.j2 @@ -25,3 +25,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). + +A `SANITY_FAILED` rule whose method was flagged VACUOUS (in a ``) is NEVER a good reason: marking such +rules "expected to fail" hides a setup defect exactly like filtering the method would, and the prover validation stamp +will be withheld unless the recorded reason documents which repair-ladder steps you attempted and why each failed. diff --git a/tests/test_vacuity.py b/tests/test_vacuity.py index fd8993a..3844c2c 100644 --- a/tests/test_vacuity.py +++ b/tests/test_vacuity.py @@ -2,8 +2,8 @@ Unit tests for composer/prover/vacuity.py: vacuous-method detection over synthetic RuleResult sets, alert rendering, the filtered-block / documented-repair spec-text checks, and the verify_spec hard guard that -withholds the PROVER validation stamp for undocumented filters of -detected-vacuous methods. +withholds the PROVER validation stamp for undocumented filters — or +undocumented expect_rule_failure skips — of detected-vacuous methods. """ import pytest @@ -16,6 +16,7 @@ format_vacuity_alert, instantiated_methods, undocumented_filtered_vacuous, + undocumented_skipped_vacuous, ) from composer.spec.cvl_generation import check_completion from composer.spec.source.author import ExpectRuleFailure @@ -182,6 +183,55 @@ def test_multiple_methods_sorted(self): """ assert undocumented_filtered_vacuous(spec, [WITHDRAW, DEPOSIT]) == [DEPOSIT, WITHDRAW] + def test_prefix_collision_not_matched(self): + """Token-boundary matching: vacuous `deposit` must NOT count as contained + in a filter that only excludes `depositAll` (raw-substring prefix hit).""" + spec = """\ +rule a(method f) filtered { f -> f.selector != sig:depositAll().selector } { + assert true; +} +""" + assert undocumented_filtered_vacuous(spec, [DEPOSIT]) == [] + + +# ========================================================================= +# undocumented_skipped_vacuous +# ========================================================================= + + +_DOCUMENTED_SKIP_REASON = ( + "solvency sanity-fails because deposit is vacuous; attempted to fix the NONDET " + "summary on the payable receiver, then a mock under certora/mocks, then " + "optimistic_fallback — the revert persisted in all three." +) + + +class TestUndocumentedSkippedVacuous: + def test_undocumented_skip_blocked(self): + evidence = detect_vacuous_methods( + [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")] + ) + skips = {"ruleA": "flaky rule", "ruleB": "known to fail"} + assert undocumented_skipped_vacuous(evidence, skips) == [DEPOSIT] + + def test_documented_skip_passes(self): + evidence = detect_vacuous_methods( + [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")] + ) + skips = {"ruleA": _DOCUMENTED_SKIP_REASON, "ruleB": "known to fail"} + assert undocumented_skipped_vacuous(evidence, skips) == [] + + def test_unskipped_rules_pass(self): + """A vacuous verdict with no affected rule in rule_skips never blocks here + (the still-failing rules block all_verified instead).""" + evidence = detect_vacuous_methods( + [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")] + ) + assert undocumented_skipped_vacuous(evidence, {"unrelated": "expected CEX"}) == [] + + def test_empty_evidence_passes(self): + assert undocumented_skipped_vacuous({}, {"ruleA": "flaky"}) == [] + # ========================================================================= # verify_spec filtered-vacuous hard guard (mocked prover) @@ -310,6 +360,69 @@ async def test_no_filter_no_guard(self, certora_prover: ProverMock): ).map_run(_result_accepted) assert accepted + @pytest.mark.asyncio + async def test_undocumented_rule_skip_withholds_stamp(self, certora_prover: ProverMock): + """The expect_rule_failure bypass: instead of filtering the vacuous method, + the agent marks its sanity-failing rule "expected to fail". The rule drops + out of the all-verified check, but the stamp must still be withheld.""" + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + curr_spec=_NO_FILTER_SPEC, + ) + accepted = await scenario.turns( + _verify(), + tool_call_raw("expect_rule_failure", rule_name="solvency", reason="flaky rule"), + _verify(), + _result("done"), + ).map_run(_result_accepted) + assert not accepted + + @pytest.mark.asyncio + async def test_skip_guard_message_names_method_and_tools(self, certora_prover: ProverMock): + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + curr_spec=_NO_FILTER_SPEC, + ) + msg = await ( + scenario.turn(_verify()) + .turn(tool_call_raw("expect_rule_failure", rule_name="solvency", reason="flaky rule")) + .turn(_verify()) + .run_last_single_tool(_PROVER) + ) + assert "vacuity_skip_guard" in msg + assert "WITHHELD" in msg + assert DEPOSIT in msg + assert "expect_rule_passage" in msg + + @pytest.mark.asyncio + async def test_documented_rule_skip_grants_stamp(self, certora_prover: ProverMock): + """Escape hatch: the skip reason documents the attempted repair-ladder steps.""" + scenario = _guard_scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), + curr_spec=_NO_FILTER_SPEC, + ) + accepted = await scenario.turns( + _verify(), + tool_call_raw( + "expect_rule_failure", rule_name="solvency", reason=_DOCUMENTED_SKIP_REASON + ), + _verify(), + _result("done"), + ).map_run(_result_accepted) + assert accepted + @pytest.mark.asyncio async def test_healthy_reinstantiation_clears_verdict(self, certora_prover: ProverMock): """Run 2 instantiates the method without a sanity failure (the setup was From 40963ead69be3fc77180c2dc5a5b9f5acd462a58 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:45:20 +0300 Subject: [PATCH 07/13] Tighten the >=2-rules vacuity-detection arm to require no healthy instantiation A VERIFIED or VIOLATED instantiation requires actually reaching the method's code, so it disproves all-paths reversion; sanity failures alongside one stem from the failing rules' own preconditions, not method vacuity. The >=2 arm now fires only when every other instantiation is TIMEOUT/ERROR/SKIPPED (the statuses that can mask a truly vacuous method), eliminating the definitional false positives that misdirected the agent onto the setup-repair ladder. Co-Authored-By: Claude Fable 5 --- composer/prover/vacuity.py | 30 +++++++++++++++++++++--------- tests/test_vacuity.py | 27 +++++++++++++++++++++++++-- 2 files changed, 46 insertions(+), 11 deletions(-) diff --git a/composer/prover/vacuity.py b/composer/prover/vacuity.py index b99102a..69114bd 100644 --- a/composer/prover/vacuity.py +++ b/composer/prover/vacuity.py @@ -1,7 +1,8 @@ """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 at once) is *vacuous*: every path through it reverts under +(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 @@ -34,16 +35,23 @@ class VacuityEvidence(BaseModel): 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 >= 2 rules OR in 100% of the rules that - instantiate them. - - The 100% arm catches single-rule runs; the >= 2 arm catches a method that - is vacuous across the board even when some rule's own preconditions mask - it. A sanity failure on a non-parametric rule (``path.method is None``) - is a rule-authoring problem, not method vacuity, and is ignored here. + 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: @@ -51,11 +59,15 @@ def detect_vacuous_methods(results: Iterable[RuleResult]) -> dict[str, VacuityEv 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] - if len(failed_rules) < 2 and failed_rules != all_rules: + 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, diff --git a/tests/test_vacuity.py b/tests/test_vacuity.py index 3844c2c..77e6e3f 100644 --- a/tests/test_vacuity.py +++ b/tests/test_vacuity.py @@ -70,13 +70,36 @@ def test_sanity_failed_in_one_of_many_not_flagged(self): ] assert detect_vacuous_methods(results) == {} - def test_two_rules_flagged_even_when_others_pass(self): - """>=2 sanity-failed rules flag the method even below 100%.""" + def test_two_rules_with_healthy_instantiation_not_flagged(self): + """>=2 sanity failures alongside a VERIFIED instantiation are a + rule-precondition problem, not method vacuity: a passing rule reached + the method's code, disproving all-paths reversion.""" results = [ _res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED"), _res("ruleC", DEPOSIT, "VERIFIED"), ] + assert detect_vacuous_methods(results) == {} + + def test_two_rules_with_violated_instantiation_not_flagged(self): + """VIOLATED also requires reaching the method's code, so it clears + the >=2 arm just like VERIFIED.""" + results = [ + _res("ruleA", DEPOSIT, "SANITY_FAILED"), + _res("ruleB", DEPOSIT, "SANITY_FAILED"), + _res("ruleC", DEPOSIT, "VIOLATED"), + ] + assert detect_vacuous_methods(results) == {} + + def test_two_rules_flagged_when_others_timeout(self): + """TIMEOUT/ERROR can mask an all-paths-reverting method — the >=2 arm + still fires when no instantiation reached a healthy verdict.""" + results = [ + _res("ruleA", DEPOSIT, "SANITY_FAILED"), + _res("ruleB", DEPOSIT, "SANITY_FAILED"), + _res("ruleC", DEPOSIT, "TIMEOUT"), + _res("ruleD", DEPOSIT, "ERROR"), + ] assert set(detect_vacuous_methods(results)) == {DEPOSIT} def test_mixed_methods(self): From 571b7614526938366af7400d25304d130a1d505f Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:53:23 +0300 Subject: [PATCH 08/13] Replace the lexical vacuity escape hatch with a structural acknowledgment ledger MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The verify_spec stamp gate no longer scans spec text: the new acknowledge_vacuous_method tool (method, steps_attempted drawn from the repair ladder, justification) writes a structured ledger entry into graph state under the same DELETE_SKIP reducer as rule_skips, and the gate withholds the PROVER stamp exactly while `known_vacuous - acknowledged` is non-empty. Because a persisted verdict only clears when a run re-instantiates the method healthily, every hiding route (filtered block, expect_rule_failure, rule deletion) is covered uniformly — strictly more complete than the deleted regex/brace-scan guards, with no magic-word incentive. Acknowledgments clear together with their verdict, so a method that turns vacuous again needs a fresh entry. Deleted: undocumented_filtered_vacuous, undocumented_skipped_vacuous, _filtered_blocks_with_context, _bare_method_name, _REPAIR_ATTEMPT_MARKERS and the two per-route guard messages (replaced by one structural guard message). Author/judge prompts now describe the tool; the judge's Criteria 5 states the filter-legitimacy taxonomy (documented harness helper OR acknowledged-vacuous ledger entry) so it composes with the harness-augmentation judge guidance. Co-Authored-By: Claude Fable 5 --- composer/prover/vacuity.py | 176 ++-------- composer/spec/source/author.py | 72 +++- composer/spec/source/prover.py | 77 +++-- .../templates/property_generation_prompt.j2 | 17 +- .../property_generation_system_prompt.j2 | 4 +- composer/templates/property_judge_prompt.j2 | 15 +- tests/test_vacuity.py | 307 ++++++++---------- 7 files changed, 312 insertions(+), 356 deletions(-) diff --git a/composer/prover/vacuity.py b/composer/prover/vacuity.py index 69114bd..dae30e7 100644 --- a/composer/prover/vacuity.py +++ b/composer/prover/vacuity.py @@ -6,17 +6,20 @@ 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, -renders the ```` the agent sees, and provides the checks backing -the ``verify_spec`` vacuity guards (undocumented ``filtered`` exclusions and -undocumented ``expect_rule_failure`` skips of the affected rules). +``RulePath.method``); this module aggregates them into a per-method verdict and +renders the ```` 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. """ -import re from typing import Iterable from pydantic import BaseModel @@ -103,9 +106,11 @@ def instantiated_methods(results: Iterable[RuleResult]) -> set[str]: 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, exclude the method with a `filtered` block. The justification comment - next to the filter MUST name which of steps 1-3 you attempted and why each failed — an - undocumented filter of a vacuous method will not be accepted as a passing result.""" + 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: @@ -127,141 +132,32 @@ def format_vacuity_alert(evidence: dict[str, VacuityEvidence]) -> str: return "\n".join(lines) -def format_filter_guard(blocked: list[str]) -> str: +def format_vacuity_guard(blocked: dict[str, str]) -> str: """Render the message returned by ``verify_spec`` when it withholds the - PROVER validation stamp because vacuous methods are filtered without a - documented repair attempt.""" - method_list = "\n".join(f" - {m}" for m in sorted(blocked)) - return f"""\ - -The PROVER validation stamp was WITHHELD. The following method(s) were previously detected as -VACUOUS (they revert on every path under the current verification model) and are now excluded via -a `filtered` block with no documented repair attempt: -{method_list} - -Filtering a vacuous method 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` AddFile/AddLink, 3. `optimistic_fallback` via - `edit_config` set_flag), un-filter the method, and rerun `verify_spec`; or - * if steps 1-3 genuinely failed, add a comment next to the `filtered` block documenting which of - summary-fix / mock / optimistic_fallback you attempted and why each failed, then rerun - `verify_spec`. The feedback judge will assess the quality of that justification. -""" + PROVER validation stamp: ``blocked`` maps each still-outstanding vacuous + method (no healthy re-instantiation, no acknowledgment) to its diagnosis. - -def format_skip_guard(blocked: list[str]) -> str: - """Render the message returned by ``verify_spec`` when it withholds the - PROVER validation stamp because the sanity-failing rules of vacuous methods - were marked "expected to fail" without a documented repair attempt.""" - method_list = "\n".join(f" - {m}" for m in sorted(blocked)) + 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"""\ - -The PROVER validation stamp was WITHHELD. The following method(s) are VACUOUS (they revert on -every path under the current verification model) and their sanity-failing rules were marked -"expected to fail" via `expect_rule_failure` with no documented repair attempt: + +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} -Marking those rules as expected failures hides a setup defect just like filtering the method would. -Either: +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` AddFile/AddLink, 3. `optimistic_fallback` via - `edit_config` set_flag), un-mark the rules with `expect_rule_passage`, and rerun `verify_spec`; or - * if steps 1-3 genuinely failed, re-call `expect_rule_failure` with a reason documenting which of - summary-fix / mock / optimistic_fallback you attempted and why each failed, then rerun - `verify_spec`. The feedback judge will assess the quality of that justification. -""" - - -def _bare_method_name(method: str) -> str: - """``Bank.withdraw(uint256)`` -> ``withdraw``. Prover method-instantiation - names are contract-qualified with a parameter list; filter expressions - reference the bare Solidity name (e.g. ``sig:withdraw(uint256).selector``).""" - return method.split("(", 1)[0].rsplit(".", 1)[-1] - - -def _filtered_blocks_with_context(spec: str, context_lines: int = 12) -> list[tuple[str, str]]: - """Return ``(context, body)`` for every ``filtered { ... }`` block in the - spec. ``body`` is the brace-delimited filter text; ``context`` additionally - includes the ``context_lines`` lines preceding the ``filtered`` keyword, - which is where a repair-attempt justification comment is expected to live. - - Deliberately a simple lexical scan (no CVL parser): filter bodies are - single expressions, so naive brace matching suffices, and a rare miss only - skips the guard — it can never spuriously block. - """ - blocks: list[tuple[str, str]] = [] - for match in re.finditer(r"\bfiltered\b", spec): - open_idx = spec.find("{", match.end()) - if open_idx == -1: - continue - depth = 0 - close_idx = -1 - for i in range(open_idx, len(spec)): - if spec[i] == "{": - depth += 1 - elif spec[i] == "}": - depth -= 1 - if depth == 0: - close_idx = i - break - if close_idx == -1: - continue - body = spec[open_idx : close_idx + 1] - preceding = spec[: match.start()].splitlines()[-context_lines:] - blocks.append(("\n".join(preceding) + "\n" + body, body)) - return blocks - - -# Lenient markers for "a repair-ladder step was attempted and documented". Substring match, -# case-insensitive: "summar" covers summary/summaries/summarized. Presence — not quality — is -# checked here; the feedback judge assesses whether the justification is actually convincing. -_REPAIR_ATTEMPT_MARKERS = ("summar", "mock", "optimistic_fallback") - - -def _documents_repair_attempt(context: str) -> bool: - lowered = context.lower() - return any(marker in lowered for marker in _REPAIR_ATTEMPT_MARKERS) - - -def undocumented_filtered_vacuous(spec: str, methods: Iterable[str]) -> list[str]: - """The subset of ``methods`` (prover instantiation names) that appear in a - ``filtered`` block of ``spec`` where neither the block nor the lines above - it document a repair-ladder attempt. - - A method mentioned in several filters passes if ANY of them is documented - — the false-block risk must stay low; the judge arbitrates quality. - """ - blocks = _filtered_blocks_with_context(spec) - blocked: list[str] = [] - for method in methods: - # Token-boundary match, not raw substring: a filter excluding only - # `depositAll` must not count as containing the vacuous `deposit`. - name_re = re.compile(rf"\b{re.escape(_bare_method_name(method))}\b") - containing = [ctx for (ctx, body) in blocks if name_re.search(body)] - if containing and not any(_documents_repair_attempt(ctx) for ctx in containing): - blocked.append(method) - return sorted(blocked) - - -def undocumented_skipped_vacuous( - evidence: dict[str, VacuityEvidence], rule_skips: dict[str, str] -) -> list[str]: - """The subset of this run's vacuous methods with a sanity-failing rule - excluded from the pass/fail verdict via a rule skip (``expect_rule_failure``) - whose reason does not document a repair-ladder attempt. - - Closes the other mechanical bypass of the filtered-vacuous guard: instead of - filtering the method, the agent can mark each of its sanity-failing rules - "expected to fail" — those rules then drop out of ``verify_spec``'s - all-verified check while the method never enters a filter body. Works off - the current run's evidence (not the persisted verdicts) because only it - names the affected rules; in the skip scenario the method stays - instantiated, so detection re-fires on every run. Mirrors the filter - check's leniency: one documented skip reason covering the method clears it. - """ - blocked: list[str] = [] - for method, ev in evidence.items(): - reasons = [rule_skips[r] for r in ev.affected_rules if r in rule_skips] - if reasons and not any(_documents_repair_attempt(reason) for reason in reasons): - blocked.append(method) - return sorted(blocked) + 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. +""" diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index 9b9085a..ae8b117 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -68,6 +68,72 @@ async def run(self) -> Command: self.rule_name: self.reason } ) +type RepairStep = Literal["summary_fix", "mock", "optimistic_fallback"] + + +@tool_display(lambda p: f"Acknowledging vacuous method `{p['method']}`", None) +class AcknowledgeVacuousMethod( + WithImplementation[Command], WithInjectedState[ProverStateExtra], WithInjectedId, +): + """ + Formally acknowledge a method that `verify_spec` flagged as VACUOUS (in a `` / + `` block), after the repair ladder failed to fix it. This is the ONLY way to + obtain the prover validation stamp while a known-vacuous method is excluded (via `filtered`, + `expect_rule_failure`, or rule removal): an unacknowledged vacuous method always withholds + the stamp. The feedback judge audits the quality of your acknowledgment, so record honestly + which repair-ladder steps you attempted and why each failed. The acknowledgment is cleared + automatically if a later run shows the method healthy. + """ + method: str = Field( + description="The method's instantiation name exactly as flagged by the prover " + "(e.g. `Bank.deposit(uint256)`)" + ) + steps_attempted: list[RepairStep] = Field( + description="The repair-ladder steps you actually attempted before acknowledging: " + "`summary_fix` (fixing/replacing the offending summary), `mock` (a mock contract via " + "`write_mock` + `edit_config`), `optimistic_fallback` (via `edit_config` set_flag). " + "Must be non-empty." + ) + justification: str = Field( + description="Why each attempted step failed to repair the vacuity, concretely " + "(compiler/prover output, persisting sanity failure, etc.). The feedback judge " + "reads this verbatim." + ) + + @override + def run(self) -> Command: + known = self.state.get("vacuous_methods", {}) + if self.method not in known: + return tool_state_update( + self.tool_call_id, + f"Method {self.method!r} is not currently flagged as vacuous. " + + (f"Currently flagged: {', '.join(sorted(known))}." if known + else "No methods are currently flagged."), + ) + if not self.steps_attempted: + return tool_state_update( + self.tool_call_id, + "At least one attempted repair-ladder step is required: acknowledge a vacuous " + "method only after genuinely attempting to repair the setup.", + ) + if not self.justification.strip(): + return tool_state_update( + self.tool_call_id, + "A non-empty justification is required: describe why each attempted " + "repair-ladder step failed.", + ) + record = json.dumps({ + "steps_attempted": sorted(set(self.steps_attempted)), + "justification": self.justification, + }) + return tool_state_update( + self.tool_call_id, + f"Acknowledged {self.method} as vacuous. The feedback judge will audit this " + "justification; rerun `verify_spec` to obtain the validation stamp.", + acknowledged_vacuous={self.method: record}, + ) + + @tool_display( lambda p: f"Expecting rule `{p["rule_name"]}` to pass", None ) @@ -469,9 +535,12 @@ async def batch_cvl_generation( GiveUpTool.as_tool("give_up"), PublishResultTool.as_tool("result"), # Setup-repair tools for the vacuity repair ladder: edit_config covers ladder # steps 2 (register a mock via add_file/add_link) and 3 (optimistic_fallback via - # set_flag); write_mock produces the step-2 mock itself. + # set_flag); write_mock produces the step-2 mock itself; + # acknowledge_vacuous_method is the structured last-resort ledger entry the + # verify_spec stamp gate and the feedback judge consult. ConfigEditTool.as_tool("edit_config"), WriteMockTool.bind(source.project_root).as_tool("write_mock"), + AcknowledgeVacuousMethod.as_tool("acknowledge_vacuous_method"), ctx.get_memory_tool(), ] ).with_state( @@ -507,6 +576,7 @@ async def batch_cvl_generation( required_validations=[FEEDBACK_VALIDATION_KEY, PROVER_VALIDATION_KEY], rule_skips={}, vacuous_methods={}, + acknowledged_vacuous={}, skipped=[], property_rules=[], validations={}, diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index 9ee0723..c16db29 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -29,10 +29,7 @@ from composer.prover.core import ( ProverOptions, ProverCallbacks, ProverReport, run_prover, DefaultCexHandler ) -from composer.prover.vacuity import ( - format_filter_guard, format_skip_guard, - undocumented_filtered_vacuous, undocumented_skipped_vacuous, -) +from composer.prover.vacuity import format_vacuity_guard from composer.prover.callbacks import ProverEventCallbacks from composer.ui.tool_display import tool_display from composer.diagnostics.stream import ( @@ -98,6 +95,14 @@ class ProverStateExtra(TypedDict): # forget it. Shares the DELETE_SKIP-sentinel reducer with rule_skips — an entry is cleared # when a later run instantiates the method without a sanity failure. vacuous_methods: Annotated[dict[str, str], _merge_rule_skips] + # The acknowledged-vacuous ledger (instantiation name -> JSON record with + # `steps_attempted` and `justification`), written by the acknowledge_vacuous_method + # tool. The verify_spec stamp gate is `known_vacuous - acknowledged`: an acknowledged + # method no longer withholds the stamp, and the feedback judge audits the record's + # quality. An entry is cleared alongside its vacuity verdict when a run shows the + # method healthy, so a method that later turns vacuous *again* needs a fresh + # acknowledgment. + acknowledged_vacuous: Annotated[dict[str, str], _merge_rule_skips] type ProverEvents = CEXAnalysisStart | CloudPollingEvent | ProverOutputEvent | RuleAnalysisResult | ProverRun | ProverLink | ProverResult @@ -173,26 +178,32 @@ async def on_prover_result(self, results: dict[str, RuleResult]) -> None: def _vacuity_state_update( state: ProverStateExtra, result: ProverReport -) -> tuple[dict[str, str], set[str]]: +) -> tuple[dict[str, str], dict[str, str], set[str]]: """Fold this run's vacuity view into the persisted ``vacuous_methods`` state. - Returns ``(update, known_vacuous)``: the reducer delta to merge into state - (newly detected methods added, previously-recorded methods that this run - instantiated *without* a sanity failure cleared via DELETE_SKIP), and the - resulting set of methods still considered vacuous — the set the filtered- - vacuous guard checks against. ``state.get`` tolerates checkpoints predating - this field. + Returns ``(update, ack_update, known_vacuous)``: the reducer delta to merge + into ``vacuous_methods`` (newly detected methods added, previously-recorded + methods that this run instantiated *without* a sanity failure cleared via + DELETE_SKIP), the companion delta clearing ``acknowledged_vacuous`` entries + whose verdict just cleared (so a method that turns vacuous again later needs + a fresh acknowledgment), and the resulting set of methods still considered + vacuous — the set the stamp gate checks against. ``state.get`` tolerates + checkpoints predating these fields. """ prior = state.get("vacuous_methods", {}) + acks = state.get("acknowledged_vacuous", {}) update: dict[str, str] = {m: ev.diagnosis for m, ev in result.vacuous_methods.items()} for m in prior: if m in result.instantiated_methods and m not in result.vacuous_methods: update[m] = DELETE_SKIP + ack_update = { + m: DELETE_SKIP for m, v in update.items() if v == DELETE_SKIP and m in acks + } known_vacuous = { m for m in (set(prior) | set(result.vacuous_methods)) if update.get(m) != DELETE_SKIP } - return update, known_vacuous + return update, ack_update, known_vacuous class VerifySpecSchema(BaseModel): @@ -294,7 +305,7 @@ async def verify_spec( if isinstance(result, str): return result - vacuity_update, known_vacuous = _vacuity_state_update(state, result) + vacuity_update, ack_update, known_vacuous = _vacuity_state_update(state, result) all_verified = True for (r, stat) in result.rule_status.items(): if r in state["rule_skips"]: @@ -303,35 +314,37 @@ async def verify_spec( all_verified = False break if rules is None and all_verified: - # HARD GUARD: a detected-vacuous method sitting inside a `filtered` block - # makes the run pass trivially — and so does marking its sanity-failing - # rules "expected to fail", which drops them from the all_verified check - # above. Withhold the PROVER validation stamp in both cases unless a - # repair-ladder attempt is documented (near the filter / in the skip - # reason — the escape hatch, checked leniently; the judge assesses - # its quality). - filter_blocked = undocumented_filtered_vacuous( - state["curr_spec"], known_vacuous - ) - skip_blocked = undocumented_skipped_vacuous( - result.vacuous_methods, state["rule_skips"] - ) - if filter_blocked or skip_blocked: - guards = ([format_filter_guard(filter_blocked)] if filter_blocked else []) \ - + ([format_skip_guard(skip_blocked)] if skip_blocked else []) + # HARD GUARD, purely structural: a persisted vacuity verdict only clears + # when a run instantiates the method without a sanity failure, so ANY + # route that hides the method while it is still broken — a `filtered` + # block, `expect_rule_failure` on its sanity-failing rules (dropping + # them from the all_verified check above), even deleting the rule — + # leaves the verdict outstanding. Withhold the PROVER validation stamp + # while any known-vacuous method lacks an acknowledged_vacuous ledger + # entry (written by the acknowledge_vacuous_method tool; the feedback + # judge audits the entry's quality). + unacknowledged = known_vacuous - set(state.get("acknowledged_vacuous", {})) + if unacknowledged: + prior_verdicts = state.get("vacuous_methods", {}) + blocked = { + m: (result.vacuous_methods[m].diagnosis + if m in result.vacuous_methods else prior_verdicts[m]) + for m in unacknowledged + } return tool_state_update( tool_call_id=tool_call_id, - content="\n\n".join([result.result_str, *guards]), + content="\n\n".join([result.result_str, format_vacuity_guard(blocked)]), prover_link=result.link, vacuous_methods=vacuity_update, + acknowledged_vacuous=ack_update, ) return tool_state_update( tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link, validations=stamper(state), - vacuous_methods=vacuity_update, + vacuous_methods=vacuity_update, acknowledged_vacuous=ack_update, ) return tool_state_update( tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link, - vacuous_methods=vacuity_update, + vacuous_methods=vacuity_update, acknowledged_vacuous=ack_update, ) return verify_spec diff --git a/composer/templates/property_generation_prompt.j2 b/composer/templates/property_generation_prompt.j2 index dff173d..1bef0e1 100644 --- a/composer/templates/property_generation_prompt.j2 +++ b/composer/templates/property_generation_prompt.j2 @@ -103,18 +103,19 @@ feedback as soon as possible. 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, exclude the method with a `filtered` block — see below. + 4. ONLY as a last resort, acknowledge the method with the `acknowledge_vacuous_method` tool and then + exclude it with a `filtered` block — see below. * If you have a parametric rule or invariant that is persistently failing on a method, and that method should genuinely be excluded from the property/invariant being proven, use a `filtered` block to exclude it. + You should not use this strategy lightly; only do so when you are 95% certain that the method in question should be excluded from the property. - + NEVER use a `filtered` block to hide a *vacuous* method (one flagged in a ``): that hides a setup - defect instead of fixing it, and the prover validation stamp will be withheld. If steps 1-3 of the repair ladder - genuinely failed, you may filter the method, but the justification comment next to the filter MUST name which of - summary-fix / mock / `optimistic_fallback` you attempted and why each failed. - + The same applies to `expect_rule_failure`: marking a vacuous method's sanity-failing rules as "expected to fail" - hides the identical setup defect and likewise withholds the prover validation stamp, unless the reason you record - names which of summary-fix / mock / `optimistic_fallback` you attempted and why each failed. + + NEVER hide a *vacuous* method (one flagged in a ``) — whether via a `filtered` block, via + `expect_rule_failure` on its sanity-failing rules, or by deleting the rule: that hides a setup defect instead + of fixing it, and the prover validation stamp will be withheld while the vacuity verdict is outstanding. The + verdict clears only when a prover run shows the method instantiated without a sanity failure. If steps 1-3 of + the repair ladder genuinely failed, formally acknowledge the method with the `acknowledge_vacuous_method` + tool, recording which steps (`summary_fix` / `mock` / `optimistic_fallback`) you attempted and why each + failed; the feedback judge audits the quality of that acknowledgment. * For any other logical errors/issues not described here, address the changes in a methodical way. Use your adaptive thinking and the cvl researcher to come to *principled* solutions. Do *NOT* try to brute force the solution by trying random changes. diff --git a/composer/templates/property_generation_system_prompt.j2 b/composer/templates/property_generation_system_prompt.j2 index f5e9ab3..48eec58 100644 --- a/composer/templates/property_generation_system_prompt.j2 +++ b/composer/templates/property_generation_system_prompt.j2 @@ -28,4 +28,6 @@ are good reasons to use this "expect failure" functionality: A `SANITY_FAILED` rule whose method was flagged VACUOUS (in a ``) is NEVER a good reason: marking such rules "expected to fail" hides a setup defect exactly like filtering the method would, and the prover validation stamp -will be withheld unless the recorded reason documents which repair-ladder steps you attempted and why each failed. +will be withheld while the vacuity verdict is outstanding. The verdict clears only when a prover run shows the method +healthy or when you formally acknowledge it with the `acknowledge_vacuous_method` tool (recording which repair-ladder +steps you attempted and why each failed — the feedback judge audits that record). diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 7ab7813..1f555c7 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -144,10 +144,17 @@ A `NONDET` summary on a *payable* callee deserves explicit scrutiny: it drops th every caller revert on all paths, so any rule instantiated with those callers holds *vacuously*. A `filtered` block that excludes a method whose sanity failure stems from such a repairable summary is the same trivialization in disguise: -the setup defect is hidden rather than fixed, and the property silently loses coverage of that method. Reject such filters unless their -justification documents that the root-cause repairs were attempted and why each failed (fixing/replacing the offending summary while preserving -payable semantics, providing a mock for the callee, or enabling `optimistic_fallback`). An undocumented filter of a vacuously-passing method -must be rejected. +the setup defect is hidden rather than fixed, and the property silently loses coverage of that method. A method exclusion (a `filtered` +block, or an "expected to fail" marking of the affected rules) is legitimate in exactly two cases: +1. The excluded method is a *documented harness helper* — verification-only scaffolding the harness exposes, not production behavior — and + the exclusion keeps helper-only transitions out of a production-behavior property. +2. The excluded method appears in the *acknowledged-vacuous ledger* provided in your inputs (when available): the author formally + acknowledged the method as vacuous, recording which repair-ladder steps were attempted (summary fix preserving payable semantics / + mock for the callee / `optimistic_fallback`) and why each failed. Audit that record on its merits — an acknowledgment whose + justification is vague, does not match the recorded steps, or skips obviously-applicable repair steps must be rejected just like + an unacknowledged exclusion. +Any other exclusion of a vacuously-passing method must be rejected. When your inputs include vacuity verdicts and rule-skip reasons, +cross-check them: an exclusion of a method flagged vacuous with no matching ledger entry is never acceptable. ### Criteria 6: Manifest Errors diff --git a/tests/test_vacuity.py b/tests/test_vacuity.py index 77e6e3f..ba0ad3f 100644 --- a/tests/test_vacuity.py +++ b/tests/test_vacuity.py @@ -1,11 +1,13 @@ """ -Unit tests for composer/prover/vacuity.py: vacuous-method detection over -synthetic RuleResult sets, alert rendering, the filtered-block / -documented-repair spec-text checks, and the verify_spec hard guard that -withholds the PROVER validation stamp for undocumented filters — or -undocumented expect_rule_failure skips — of detected-vacuous methods. +Unit tests for composer/prover/vacuity.py and the verify_spec vacuity gate: +vacuous-method detection over synthetic RuleResult sets, alert rendering, the +acknowledge_vacuous_method ledger tool, and the purely structural hard guard +that withholds the PROVER validation stamp while any known-vacuous method is +neither shown healthy by a later run nor acknowledged in the ledger. """ +import json + import pytest from composer.prover.core import ProverReport @@ -15,11 +17,9 @@ detect_vacuous_methods, format_vacuity_alert, instantiated_methods, - undocumented_filtered_vacuous, - undocumented_skipped_vacuous, ) from composer.spec.cvl_generation import check_completion -from composer.spec.source.author import ExpectRuleFailure +from composer.spec.source.author import AcknowledgeVacuousMethod, ExpectRuleFailure from composer.spec.source.prover import StateWithSkips, VALIDATION_KEY from graphcore.testing import Scenario, tool_call_raw, ToolCallDict @@ -153,113 +153,18 @@ def test_alert_contains_ladder_and_methods(self): # ========================================================================= -# undocumented_filtered_vacuous +# verify_spec vacuity hard guard (mocked prover) # ========================================================================= - -_UNDOCUMENTED_SPEC = """\ -rule solvency(method f) filtered { f -> f.selector != sig:deposit(uint256).selector } { - assert true; -} -""" - -_DOCUMENTED_SPEC = """\ -// deposit is excluded: attempted to fix the NONDET summary on the payable receiver (typecheck -// rejected the replacement), then a mock under certora/mocks (compilation failed on the -// constructor), then optimistic_fallback (the revert persisted). Filtering as a last resort. +# The gate is purely structural (persisted verdicts minus the acknowledgment +# ledger) — the spec text is irrelevant to it, so one spec serves every case: +# it "hides" the vacuous method simply by not exercising it in run 2. +_SPEC = """\ rule solvency(method f) filtered { f -> f.selector != sig:deposit(uint256).selector } { assert true; } """ -_NO_FILTER_SPEC = """\ -rule solvency(method f) { - assert true; -} -""" - - -class TestUndocumentedFilteredVacuous: - def test_undocumented_filter_blocked(self): - assert undocumented_filtered_vacuous(_UNDOCUMENTED_SPEC, [DEPOSIT]) == [DEPOSIT] - - def test_documented_filter_passes(self): - assert undocumented_filtered_vacuous(_DOCUMENTED_SPEC, [DEPOSIT]) == [] - - def test_method_not_filtered_passes(self): - assert undocumented_filtered_vacuous(_NO_FILTER_SPEC, [DEPOSIT]) == [] - - def test_other_method_in_filter_passes(self): - assert undocumented_filtered_vacuous(_UNDOCUMENTED_SPEC, [WITHDRAW]) == [] - - def test_one_documented_occurrence_suffices(self): - """A method filtered in two rules passes if either filter is documented.""" - spec = _UNDOCUMENTED_SPEC + "\n" + _DOCUMENTED_SPEC.replace("solvency", "shares") - assert undocumented_filtered_vacuous(spec, [DEPOSIT]) == [] - - def test_multiple_methods_sorted(self): - spec = """\ -rule a(method f) filtered { f -> f.selector != sig:deposit(uint256).selector - && f.selector != sig:withdraw(uint256).selector } { - assert true; -} -""" - assert undocumented_filtered_vacuous(spec, [WITHDRAW, DEPOSIT]) == [DEPOSIT, WITHDRAW] - - def test_prefix_collision_not_matched(self): - """Token-boundary matching: vacuous `deposit` must NOT count as contained - in a filter that only excludes `depositAll` (raw-substring prefix hit).""" - spec = """\ -rule a(method f) filtered { f -> f.selector != sig:depositAll().selector } { - assert true; -} -""" - assert undocumented_filtered_vacuous(spec, [DEPOSIT]) == [] - - -# ========================================================================= -# undocumented_skipped_vacuous -# ========================================================================= - - -_DOCUMENTED_SKIP_REASON = ( - "solvency sanity-fails because deposit is vacuous; attempted to fix the NONDET " - "summary on the payable receiver, then a mock under certora/mocks, then " - "optimistic_fallback — the revert persisted in all three." -) - - -class TestUndocumentedSkippedVacuous: - def test_undocumented_skip_blocked(self): - evidence = detect_vacuous_methods( - [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")] - ) - skips = {"ruleA": "flaky rule", "ruleB": "known to fail"} - assert undocumented_skipped_vacuous(evidence, skips) == [DEPOSIT] - - def test_documented_skip_passes(self): - evidence = detect_vacuous_methods( - [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")] - ) - skips = {"ruleA": _DOCUMENTED_SKIP_REASON, "ruleB": "known to fail"} - assert undocumented_skipped_vacuous(evidence, skips) == [] - - def test_unskipped_rules_pass(self): - """A vacuous verdict with no affected rule in rule_skips never blocks here - (the still-failing rules block all_verified instead).""" - evidence = detect_vacuous_methods( - [_res("ruleA", DEPOSIT, "SANITY_FAILED"), _res("ruleB", DEPOSIT, "SANITY_FAILED")] - ) - assert undocumented_skipped_vacuous(evidence, {"unrelated": "expected CEX"}) == [] - - def test_empty_evidence_passes(self): - assert undocumented_skipped_vacuous({}, {"ruleA": "flaky"}) == [] - - -# ========================================================================= -# verify_spec filtered-vacuous hard guard (mocked prover) -# ========================================================================= - _PROVER = "verify_spec" _RESULT = "result" @@ -297,16 +202,39 @@ def _vacuous_report(*, rule_status: dict[str, bool], vacuous: dict[str, VacuityE } -def _guard_scenario(certora_prover: ProverMock, *responses: ProverToolResponse, curr_spec: str): +_ACK = "acknowledge_vacuous_method" + + +def _acknowledge( + method: str = DEPOSIT, + steps: list[str] | None = None, + justification: str = "summary fix rejected by typechecker; mock failed to compile", +) -> ToolCallDict: + return tool_call_raw( + _ACK, + method=method, + steps_attempted=steps if steps is not None else ["summary_fix", "mock"], + justification=justification, + ) + + +def _guard_scenario(certora_prover: ProverMock, *responses: ProverToolResponse): prover_tool = certora_prover(responses) - return Scenario(StateWithSkips, prover_tool, ExpectRuleFailure.as_tool("expect_rule_failure"), _result_tool).init( - curr_spec=curr_spec, + return Scenario( + StateWithSkips, + prover_tool, + ExpectRuleFailure.as_tool("expect_rule_failure"), + AcknowledgeVacuousMethod.as_tool(_ACK), + _result_tool, + ).init( + curr_spec=_SPEC, skipped=[], property_rules=[], validations={}, required_validations=[VALIDATION_KEY], rule_skips={}, vacuous_methods={}, + acknowledged_vacuous={}, config={"files": ["src/Foo.sol"]}, ) @@ -315,18 +243,65 @@ def _result_accepted(st: StateWithSkips) -> bool: return "result" in st +class TestAcknowledgeVacuousMethod: + """The ledger tool's own validation, exercised against pre-seeded state.""" + + def _scenario(self, vacuous: dict[str, str] | None = None): + return Scenario(StateWithSkips, AcknowledgeVacuousMethod.as_tool(_ACK)).init( + curr_spec=_SPEC, + skipped=[], + property_rules=[], + validations={}, + required_validations=[VALIDATION_KEY], + rule_skips={}, + vacuous_methods=vacuous if vacuous is not None else {DEPOSIT: "diagnosis"}, + acknowledged_vacuous={}, + config={}, + ) + + @pytest.mark.asyncio + async def test_acknowledgment_recorded_as_structured_ledger_entry(self): + acks = await self._scenario().turn(_acknowledge()).map_run( + lambda st: st["acknowledged_vacuous"] + ) + record = json.loads(acks[DEPOSIT]) + assert record["steps_attempted"] == ["mock", "summary_fix"] + assert "typechecker" in record["justification"] + + @pytest.mark.asyncio + async def test_unknown_method_rejected(self): + scenario = self._scenario().turn(_acknowledge(method=WITHDRAW)) + msg = await scenario.run_last_single_tool(_ACK) + assert "not currently flagged" in msg + assert DEPOSIT in msg # the response lists what IS flagged + + @pytest.mark.asyncio + async def test_empty_steps_rejected(self): + acks = await self._scenario().turn(_acknowledge(steps=[])).map_run( + lambda st: st["acknowledged_vacuous"] + ) + assert acks == {} + + @pytest.mark.asyncio + async def test_blank_justification_rejected(self): + acks = await self._scenario().turn(_acknowledge(justification=" ")).map_run( + lambda st: st["acknowledged_vacuous"] + ) + assert acks == {} + + class TestVerifySpecVacuityGuard: - """Run 1 detects the vacuous method; run 2 passes because the spec filters it. - The stamp must be withheld unless the filter documents a repair attempt.""" + """Run 1 detects the vacuous method; run 2 passes because the spec hides it + (filter / skip / rule removal — the gate cannot tell and must not care). + The stamp must be withheld until the method is acknowledged or shown healthy.""" @pytest.mark.asyncio - async def test_undocumented_filter_withholds_stamp(self, certora_prover: ProverMock): + async def test_unacknowledged_hidden_method_withholds_stamp(self, certora_prover: ProverMock): scenario = _guard_scenario( certora_prover, _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), _vacuous_report(rule_status={"solvency": True}), - curr_spec=_UNDOCUMENTED_SPEC, ) accepted = await scenario.turns( _verify(), @@ -336,132 +311,124 @@ async def test_undocumented_filter_withholds_stamp(self, certora_prover: ProverM assert not accepted @pytest.mark.asyncio - async def test_guard_message_names_method_and_ladder(self, certora_prover: ProverMock): + async def test_guard_message_names_method_ladder_and_tool(self, certora_prover: ProverMock): scenario = _guard_scenario( certora_prover, _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), _vacuous_report(rule_status={"solvency": True}), - curr_spec=_UNDOCUMENTED_SPEC, ) msg = await scenario.turn(_verify()).turn(_verify()).run_last_single_tool(_PROVER) - assert "vacuity_filter_guard" in msg + assert "vacuity_guard" in msg assert "WITHHELD" in msg assert DEPOSIT in msg + assert "acknowledge_vacuous_method" in msg + assert "write_mock" in msg # the repair ladder is restated @pytest.mark.asyncio - async def test_documented_filter_grants_stamp(self, certora_prover: ProverMock): - """Escape hatch: a repair-ladder attempt documented near the filter.""" + async def test_acknowledged_method_grants_stamp(self, certora_prover: ProverMock): + """The structured escape hatch: a ledger entry written by the tool.""" scenario = _guard_scenario( certora_prover, _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), _vacuous_report(rule_status={"solvency": True}), - curr_spec=_DOCUMENTED_SPEC, ) accepted = await scenario.turns( _verify(), + _acknowledge(), _verify(), _result("done"), ).map_run(_result_accepted) assert accepted @pytest.mark.asyncio - async def test_no_filter_no_guard(self, certora_prover: ProverMock): - """A vacuous verdict alone never blocks — only filtering it does.""" + async def test_rule_skip_bypass_still_blocked(self, certora_prover: ProverMock): + """The expect_rule_failure bypass: the sanity-failing rule drops out of + the all-verified check, but the persisted verdict still withholds the + stamp — no matter how persuasive the free-text skip reason sounds + (the old lexical hatch is gone; only the ledger clears the gate).""" scenario = _guard_scenario( certora_prover, _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), - _vacuous_report(rule_status={"solvency": True}), - curr_spec=_NO_FILTER_SPEC, + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), ) accepted = await scenario.turns( _verify(), + tool_call_raw( + "expect_rule_failure", rule_name="solvency", + reason="attempted summary fix, mock, and optimistic_fallback; all failed", + ), _verify(), _result("done"), ).map_run(_result_accepted) - assert accepted + assert not accepted @pytest.mark.asyncio - async def test_undocumented_rule_skip_withholds_stamp(self, certora_prover: ProverMock): - """The expect_rule_failure bypass: instead of filtering the vacuous method, - the agent marks its sanity-failing rule "expected to fail". The rule drops - out of the all-verified check, but the stamp must still be withheld.""" + async def test_acknowledged_rule_skip_grants_stamp(self, certora_prover: ProverMock): + """Skipping the sanity-failing rules is fine once the method itself is + acknowledged in the ledger.""" scenario = _guard_scenario( certora_prover, _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), - curr_spec=_NO_FILTER_SPEC, ) accepted = await scenario.turns( _verify(), - tool_call_raw("expect_rule_failure", rule_name="solvency", reason="flaky rule"), + tool_call_raw("expect_rule_failure", rule_name="solvency", reason="vacuous, acknowledged"), + _acknowledge(), _verify(), _result("done"), ).map_run(_result_accepted) - assert not accepted - - @pytest.mark.asyncio - async def test_skip_guard_message_names_method_and_tools(self, certora_prover: ProverMock): - scenario = _guard_scenario( - certora_prover, - _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, - instantiated={DEPOSIT}), - _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, - instantiated={DEPOSIT}), - curr_spec=_NO_FILTER_SPEC, - ) - msg = await ( - scenario.turn(_verify()) - .turn(tool_call_raw("expect_rule_failure", rule_name="solvency", reason="flaky rule")) - .turn(_verify()) - .run_last_single_tool(_PROVER) - ) - assert "vacuity_skip_guard" in msg - assert "WITHHELD" in msg - assert DEPOSIT in msg - assert "expect_rule_passage" in msg + assert accepted @pytest.mark.asyncio - async def test_documented_rule_skip_grants_stamp(self, certora_prover: ProverMock): - """Escape hatch: the skip reason documents the attempted repair-ladder steps.""" + async def test_healthy_reinstantiation_clears_verdict(self, certora_prover: ProverMock): + """Run 2 instantiates the method without a sanity failure (the setup was + repaired) — the vacuity verdict clears and nothing blocks the stamp.""" scenario = _guard_scenario( certora_prover, _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), - _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, - instantiated={DEPOSIT}), - curr_spec=_NO_FILTER_SPEC, + _vacuous_report(rule_status={"solvency": True}, instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": True}), ) accepted = await scenario.turns( _verify(), - tool_call_raw( - "expect_rule_failure", rule_name="solvency", reason=_DOCUMENTED_SKIP_REASON - ), + _verify(), _verify(), _result("done"), ).map_run(_result_accepted) assert accepted @pytest.mark.asyncio - async def test_healthy_reinstantiation_clears_verdict(self, certora_prover: ProverMock): - """Run 2 instantiates the method without a sanity failure (the setup was - repaired) — the vacuity verdict clears and the filter no longer blocks.""" + async def test_healthy_reinstantiation_clears_acknowledgment(self, certora_prover: ProverMock): + """When the verdict clears, its ledger entry clears with it: a method + that turns vacuous AGAIN later needs a fresh acknowledgment, so a stale + acknowledgment can never pre-clear a future verdict.""" scenario = _guard_scenario( certora_prover, + # Run 1: vacuous. Acknowledged. Run 2: healthy (verdict + ack clear). + # Run 3: vacuous again. Run 4: hidden again -> guard must re-fire. _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, instantiated={DEPOSIT}), _vacuous_report(rule_status={"solvency": True}, instantiated={DEPOSIT}), + _vacuous_report(rule_status={"solvency": False}, vacuous=_DEPOSIT_EVIDENCE, + instantiated={DEPOSIT}), _vacuous_report(rule_status={"solvency": True}), - curr_spec=_UNDOCUMENTED_SPEC, ) - accepted = await scenario.turns( + final = await scenario.turns( _verify(), + _acknowledge(), _verify(), _verify(), - _result("done"), - ).map_run(_result_accepted) - assert accepted + _verify(), + ).map_run(lambda st: (st["acknowledged_vacuous"], Scenario.last_single_tool(_PROVER, st))) + acks, last_prover_msg = final + assert acks == {} # cleared by the healthy run, not re-established + assert "vacuity_guard" in last_prover_msg + assert "WITHHELD" in last_prover_msg From f7abf807acc0ea1901c4546dcf6e446f1121e6ce Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 02:58:52 +0300 Subject: [PATCH 09/13] Hold write_mock output in graph state; materialize per-run and persist via the artifact store write_mock previously wrote straight into the shared project tree while batch generations run concurrently under asyncio.gather: same-named mocks from parallel batches could silently clobber each other (possibly mid-compile of a sibling's prover run), gave-up generations left stray sources behind, and cache replay reconstructed confs referencing mock files nothing persisted. Now the tool records path->content in ProverStateExtra under a per-generation namespace (certora/mocks//, following the curr_spec/tmp_spec isolation idiom); verify_spec materializes the files only for the duration of a prover run, and ProverArtifactStore.write_generated_spec persists them from the new GeneratedCVL.mocks field alongside the conf that references them, so a cache hit replays correctly from a fresh checkout. Co-Authored-By: Claude Fable 5 --- composer/spec/cvl_generation.py | 4 + composer/spec/gen_types.py | 6 + composer/spec/source/artifacts.py | 21 +++- composer/spec/source/author.py | 77 ++++++------ composer/spec/source/common_pipeline.py | 1 + composer/spec/source/pipeline.py | 1 + composer/spec/source/prover.py | 34 +++++- tests/test_write_mock.py | 154 +++++++++++++++++++----- 8 files changed, 227 insertions(+), 71 deletions(-) diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index ba8da4b..cefecd5 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -125,6 +125,10 @@ class GeneratedCVL(BaseModel): # (which skips the prover) can still reconstruct certora/confs. None for pre-existing # cache entries or runs where no config was established. config: dict | None = Field(default=None) + # The generation's mock contracts (state["mocks"]: project-root-relative path -> + # Solidity source), persisted so the conf's file references resolve on cache replay + # from a fresh checkout. Empty for pre-existing cache entries and mock-free runs. + mocks: dict[str, str] = Field(default_factory=dict) # The last prover-run link (URL or local results dir), persisted for the report and so a # cache hit retains it. None when the prover never produced a link. final_link: str | None = Field(default=None) diff --git a/composer/spec/gen_types.py b/composer/spec/gen_types.py index bf27022..013bbf4 100644 --- a/composer/spec/gen_types.py +++ b/composer/spec/gen_types.py @@ -27,6 +27,12 @@ PROPERTIES_DIR = CERTORA_DIR / PROPERTIES_SUBDIR #: AutoSetup / custom summaries live here. SUMMARIES_DIR = SPECS_DIR / "summaries" +#: Agent-written mock contracts (the `write_mock` repair-ladder tool). Mocks are +#: state-held during generation and only touch this directory when materialized +#: for a prover run or persisted by the artifact store; each generation writes +#: into its own subdirectory (``certora/mocks//``) so concurrent +#: batches never collide. +MOCKS_DIR = CERTORA_DIR / "mocks" #: The autoprove run report (report.json, the optional rendered HTML, and the #: canonical slug<->id map) lives here -- a dedicated subdir so a consumer can #: include or exclude the human-facing report independently of the specs. diff --git a/composer/spec/source/artifacts.py b/composer/spec/source/artifacts.py index ae46480..4ea0b8a 100644 --- a/composer/spec/source/artifacts.py +++ b/composer/spec/source/artifacts.py @@ -16,7 +16,7 @@ from composer.spec.context import SourceCode from composer.spec.cvl_generation import GeneratedCVL from composer.spec.gen_types import ( - AP_REPORT_DIR, AUTOPROVE_INTERNAL_DIR, CERTORA_DIR, SPECS_DIR, under_project, + AP_REPORT_DIR, AUTOPROVE_INTERNAL_DIR, CERTORA_DIR, MOCKS_DIR, SPECS_DIR, under_project, ) from composer.spec.prop import PropertyFormulation from composer.spec.source.prover import prover_config_overlay @@ -92,7 +92,8 @@ def write_generated_spec(self, spec: SpecIdentity, result: GeneratedCVL) -> Path project-root-relative path (e.g. ``certora/specs/invariants.spec``). Bundle: ``specs/{stem}.spec``, ``properties/{stem}.commentary.md``, - ``properties/{stem}.property_rules.json``, and ``confs/{stem}.conf``. + ``properties/{stem}.property_rules.json``, ``confs/{stem}.conf``, and the + generation's mock contracts (if any) at their state-held paths. """ specs_dir = ensure_dir(self._deliverable_dir() / "specs") (specs_dir / spec.spec_filename).write_text(result.cvl) @@ -101,10 +102,26 @@ def write_generated_spec(self, spec: SpecIdentity, result: GeneratedCVL) -> Path spec.stem, "property_rules", {m.property_title: m.rules for m in result.property_rules}, ) + self._write_mocks(result.mocks) spec_path = SPECS_DIR / spec.spec_filename # project-root-relative self._write_conf(spec, result.config, spec_path) return spec_path + def _write_mocks(self, mocks: dict[str, str]) -> None: + """The generation's mock contracts, at their exact state-held + (project-root-relative, per-generation-namespaced) paths — the conf's + ``files`` entries reference them there, so a cache replay from a fresh + checkout can recompile without rerunning the generation.""" + for rel, content in mocks.items(): + rel_path = Path(rel) + # Belt over the write_mock tool's validation: never write outside + # the canonical mocks directory. + assert not rel_path.is_absolute() and ".." not in rel_path.parts, rel + assert rel_path.parts[:len(MOCKS_DIR.parts)] == MOCKS_DIR.parts, rel + target = under_project(self._project_root, rel_path) + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text(content) + def _write_conf( self, spec: SpecIdentity, base_config: dict | None, spec_path: Path, ) -> None: diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index ae8b117..e531ecf 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -24,7 +24,7 @@ from langgraph.graph import MessagesState from langgraph.runtime import get_runtime from pathlib import Path, PurePosixPath -from composer.spec.gen_types import CVLResource, TypedTemplate, import_statement_for +from composer.spec.gen_types import CVLResource, MOCKS_DIR, TypedTemplate, import_statement_for from composer.spec.service_host import ServiceHost from composer.workflow.services import CacheLevel @@ -447,45 +447,45 @@ async def run(self) -> Command | str: ) -# The only directory write_mock may write into, mirroring the harness generator's VFS -# confinement (`forbidden_write="^(?!certora/harnesses)"` in harness.py) — but enforced -# directly here because the authoring agent's source tools are read-only over the real -# project tree and the prover compiles from the real tree, so the mock must land on disk. -MOCKS_DIR = PurePosixPath("certora/mocks") - - -@tool_display(lambda p: f"Writing mock `{p['file_path']}`", None) -class WriteMockTool(WithAsyncDependencies[str, str]): +@tool_display(lambda p: f"Writing mock `{p['file_name']}`", None) +class WriteMockTool(WithAsyncDependencies[Command | str, str], WithInjectedId): """ - Write a minimal Solidity mock contract under `certora/mocks` implementing an interface, so - the prover can resolve calls to an otherwise-unresolved callee (step 2 of the vacuity repair - ladder). After writing the mock, register it in the prover configuration with `edit_config` - (an `add_file` edit, plus an `add_link` edit if the callee is reached through a storage field). + Write a minimal Solidity mock contract implementing an interface, so the prover can resolve + calls to an otherwise-unresolved callee (step 2 of the vacuity repair ladder). The mock is + recorded against this generation's own `certora/mocks/` subdirectory and materialized on + disk for every prover run; the tool response names the exact project-root-relative path. + After writing the mock, register that path in the prover configuration with `edit_config` + (an `add_file` edit, plus an `add_link` edit if the callee is reached through a storage + field). Keep the mock as small as possible: implement only the interface the caller needs, but preserve the semantics that matter to the calling contract — in particular a `payable` - callee must remain `payable`. Writing to an existing path overwrites it, so you can iterate - on a mock in place. + callee must remain `payable`. Writing an existing file name overwrites it, so you can + iterate on a mock in place. """ - file_path: str = Field(description=f"Project-root-relative path for the mock, under `{MOCKS_DIR}` (e.g. `{MOCKS_DIR}/MockOracle.sol`)") + # The bound dependency is the generation's namespace (its spec stem): mocks are held in + # graph state and materialized under certora/mocks// only around prover runs, + # so concurrent batch generations never mutate shared paths in the project tree (the + # same isolation the tmp_spec idiom gives curr_spec). + file_name: str = Field(description="Bare file name for the mock, e.g. `MockOracle.sol` (no directories — the tool chooses this generation's mocks directory)") content: str = Field(description="The full Solidity source of the mock contract") @override - async def run(self) -> str: - rel = PurePosixPath(self.file_path) - if rel.is_absolute() or ".." in rel.parts: - return f"Invalid path `{self.file_path}`: must be a project-root-relative path without `..`" - if rel.parts[:len(MOCKS_DIR.parts)] != MOCKS_DIR.parts or len(rel.parts) <= len(MOCKS_DIR.parts): - return f"You may only write into the `{MOCKS_DIR}` directory (got `{self.file_path}`)" - if rel.suffix != ".sol": - return f"Mock must be a Solidity source file (`.sol`), got `{self.file_path}`" - with self.tool_deps() as project_root: - target = Path(project_root) / rel - target.parent.mkdir(parents=True, exist_ok=True) - target.write_text(self.content) - return ( - f"Wrote mock to `{self.file_path}`. Remember to register it in the prover configuration " - "via `edit_config` (`add_file`, plus `add_link` if the callee is reached through a storage field)." + async def run(self) -> Command | str: + name = PurePosixPath(self.file_name) + if len(name.parts) != 1 or name.parts[0] in (".", ".."): + return f"Invalid file name `{self.file_name}`: provide a bare file name without directories" + if name.suffix != ".sol": + return f"Mock must be a Solidity source file (`.sol`), got `{self.file_name}`" + with self.tool_deps() as namespace: + rel = PurePosixPath(MOCKS_DIR.as_posix()) / namespace / name + return tool_state_update( + self.tool_call_id, + f"Recorded mock `{rel}`; it will be materialized there for every prover run. " + "Remember to register it in the prover configuration via `edit_config` " + f"(`add_file` with `{rel}`, plus `add_link` if the callee is reached through " + "a storage field).", + mocks={str(rel): self.content}, ) @@ -502,10 +502,14 @@ async def batch_cvl_generation( description: str, source: SourceCode, spec_dir: Path, + mock_namespace: str, ) -> 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*. + # *mock_namespace* (the spec's stem) names this generation's private + # certora/mocks// subdirectory: write_mock records mocks against it, so + # concurrent batch generations can never clobber each other's mock files. resource_views: list[ResourceView] = [ { "description": r.description, @@ -539,7 +543,7 @@ async def batch_cvl_generation( # acknowledge_vacuous_method is the structured last-resort ledger entry the # verify_spec stamp gate and the feedback judge consult. ConfigEditTool.as_tool("edit_config"), - WriteMockTool.bind(source.project_root).as_tool("write_mock"), + WriteMockTool.bind(mock_namespace).as_tool("write_mock"), AcknowledgeVacuousMethod.as_tool("acknowledge_vacuous_method"), ctx.get_memory_tool(), ] @@ -577,6 +581,7 @@ async def batch_cvl_generation( rule_skips={}, vacuous_methods={}, acknowledged_vacuous={}, + mocks={}, skipped=[], property_rules=[], validations={}, @@ -590,14 +595,16 @@ async def batch_cvl_generation( return GaveUp(reason=res_state["result"]) 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 - # hit (which skips the prover) can still reconstruct certora/confs and retain the link. + # Persist the base prover config, mocks, and last run link from the final state so a + # later cache hit (which skips the prover) can still reconstruct certora/confs — and + # the mock files those confs reference — and retain the link. return GeneratedCVL( commentary=res_state["result"], cvl=d, skipped=res_state["skipped"], property_rules=res_state["property_rules"], config=res_state["config"], + mocks=res_state["mocks"], final_link=res_state.get("prover_link"), ) diff --git a/composer/spec/source/common_pipeline.py b/composer/spec/source/common_pipeline.py index dac066d..1458fa3 100644 --- a/composer/spec/source/common_pipeline.py +++ b/composer/spec/source/common_pipeline.py @@ -182,6 +182,7 @@ async def _generate_batch( description=label, source=source_input, spec_dir=SPECS_DIR, + mock_namespace=ComponentSpec(batch.feat.slugified_name).stem, ), semaphore, ) diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index 5799f16..d1c49d9 100644 --- a/composer/spec/source/pipeline.py +++ b/composer/spec/source/pipeline.py @@ -255,6 +255,7 @@ async def stream_bugs(): description="Structural invariant CVL", source=source_input, spec_dir=SPECS_DIR, + mock_namespace=InvariantSpec().stem, ), ) if isinstance(inv_cvl_result, GaveUp): diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index c16db29..ef97ec8 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -95,6 +95,13 @@ class ProverStateExtra(TypedDict): # forget it. Shares the DELETE_SKIP-sentinel reducer with rule_skips — an entry is cleared # when a later run instantiates the method without a sanity failure. vacuous_methods: Annotated[dict[str, str], _merge_rule_skips] + # Agent-written mock contracts (project-root-relative path under the generation's + # certora/mocks// namespace -> Solidity source), written by the write_mock tool. + # State-held rather than written to disk so concurrent batch generations never mutate + # the shared project tree: verify_spec materializes them for the duration of a prover + # run, and the artifact store persists them (with the conf that references them) only + # for completed generations. Shares the DELETE_SKIP reducer idiom of rule_skips. + mocks: Annotated[dict[str, str], _merge_rule_skips] # The acknowledged-vacuous ledger (instantiation name -> JSON record with # `steps_attempted` and `justification`), written by the acknowledge_vacuous_method # tool. The verify_spec stamp gate is `known_vacuous - acknowledged`: an acknowledged @@ -245,6 +252,31 @@ def tmp_spec( ) as tmp: yield tmp +@contextmanager +def materialized_mocks(root: str, mocks: dict[str, str]) -> Iterator[None]: + """Materialize the generation's state-held mock files onto the real project + tree for the duration of a prover run (the prover compiles from disk), then + remove them. + + Mock paths are namespaced per generation (``certora/mocks//``), + so concurrent batch generations write disjoint files and never observe each + other's mocks mid-compile. Removing them afterward keeps gave-up generations + from leaving stray sources behind; completed generations get their mocks + persisted by the artifact store alongside the conf that references them. + """ + written: list[Path] = [] + for rel, content in mocks.items(): + target = Path(root) / rel + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text(content) + written.append(target) + try: + yield + finally: + for target in written: + target.unlink(missing_ok=True) + + def _prover_sem(cloud: bool) -> AsyncContextManager[None]: if not cloud: return asyncio.Semaphore(1) @@ -292,7 +324,7 @@ async def verify_spec( content=json.dumps(config, indent=2), ext="conf", prefix="verify" - ) as config_path: + ) as config_path, materialized_mocks(project_root, state.get("mocks", {})): async with sem: result = await run_prover( Path(project_root), diff --git a/tests/test_write_mock.py b/tests/test_write_mock.py index f4eefec..f865a4e 100644 --- a/tests/test_write_mock.py +++ b/tests/test_write_mock.py @@ -1,57 +1,145 @@ """ -Tests for the write_mock tool: real-filesystem writes confined to certora/mocks. +Tests for the write_mock tool and the state-held mock lifecycle: mocks are +recorded in graph state under a per-generation namespace (never written to the +shared project tree during generation), materialized on disk only for the +duration of a prover run, and persisted by the artifact store for completed +generations so cache replay works from a fresh checkout. """ import pytest +from langgraph.graph import MessagesState + +from composer.prover.core import ProverOptions, ProverReport +from composer.spec.cvl_generation import GeneratedCVL +from composer.spec.source.artifacts import ComponentSpec, ProverArtifactStore from composer.spec.source.author import WriteMockTool +from composer.spec.source.prover import ProverStateExtra, get_prover_tool + +from graphcore.testing import Scenario, ToolCallDict, tool_call_raw pytestmark = pytest.mark.asyncio _CONTENT = "// SPDX-License-Identifier: MIT\ncontract MockOracle { function price() external pure returns (uint256) { return 1; } }\n" +_NAMESPACE = "autospec_oracle" +_MOCK_PATH = f"certora/mocks/{_NAMESPACE}/MockOracle.sol" + +class MockTestState(MessagesState, ProverStateExtra): + pass -def _tool(project_root) -> object: - return WriteMockTool.bind(str(project_root)).as_tool("write_mock") +_WRITE = "write_mock" -async def test_writes_under_mocks_dir(tmp_path): - res = await _tool(tmp_path).ainvoke( - {"file_path": "certora/mocks/MockOracle.sol", "content": _CONTENT} + +def _scenario(): + return Scenario(MockTestState, WriteMockTool.bind(_NAMESPACE).as_tool(_WRITE)).init( + config={}, rule_skips={}, mocks={}, ) - written = tmp_path / "certora" / "mocks" / "MockOracle.sol" - assert written.read_text() == _CONTENT - # The result must nudge the agent to register the mock in the prover config. - assert "edit_config" in res -async def test_overwrite_allowed(tmp_path): - tool = _tool(tmp_path) - await tool.ainvoke({"file_path": "certora/mocks/M.sol", "content": "// v1"}) - await tool.ainvoke({"file_path": "certora/mocks/M.sol", "content": "// v2"}) - assert (tmp_path / "certora" / "mocks" / "M.sol").read_text() == "// v2" +def _write(file_name: str, content: str = _CONTENT) -> ToolCallDict: + return tool_call_raw(_WRITE, file_name=file_name, content=content) + + +# ========================================================================= +# State updates (no disk writes during generation) +# ========================================================================= + + +async def test_records_mock_in_state_under_namespace(tmp_path, monkeypatch): + monkeypatch.chdir(tmp_path) # would expose any accidental relative-path disk write + mocks = await _scenario().turn(_write("MockOracle.sol")).map_run(lambda st: st["mocks"]) + assert mocks == {_MOCK_PATH: _CONTENT} + # Nothing lands on the shared tree at write time. + assert not (tmp_path / "certora").exists() + + +async def test_response_names_path_and_edit_config(): + msg = await _scenario().turn(_write("MockOracle.sol")).run_last_single_tool(_WRITE) + assert _MOCK_PATH in msg + assert "edit_config" in msg + +async def test_overwrite_replaces_state_entry(): + mocks = await _scenario().turns( + _write("M.sol", "// v1"), + _write("M.sol", "// v2"), + ).map_run(lambda st: st["mocks"]) + assert mocks == {f"certora/mocks/{_NAMESPACE}/M.sol": "// v2"} -async def test_rejects_write_outside_mocks(tmp_path): - for bad in ( - "src/Evil.sol", - "certora/harnesses/Evil.sol", - "certora/mocks.sol", # file named like the dir, still outside it - ): - res = await _tool(tmp_path).ainvoke({"file_path": bad, "content": _CONTENT}) - assert "only write into" in res - assert not (tmp_path / "src").exists() +async def test_rejects_directories_and_traversal(): + for bad in ("sub/Evil.sol", "../Evil.sol", "..", "/Evil.sol", "certora/mocks/Evil.sol"): + mocks = await _scenario().turn(_write(bad)).map_run(lambda st: st["mocks"]) + assert mocks == {} -async def test_rejects_traversal_and_absolute(tmp_path): - for bad in ("certora/mocks/../../etc/Evil.sol", "/certora/mocks/Evil.sol"): - res = await _tool(tmp_path).ainvoke({"file_path": bad, "content": _CONTENT}) - assert "Invalid path" in res +async def test_rejects_non_solidity(): + mocks = await _scenario().turn(_write("notes.txt", "hi")).map_run(lambda st: st["mocks"]) + assert mocks == {} -async def test_rejects_non_solidity(tmp_path): - res = await _tool(tmp_path).ainvoke( - {"file_path": "certora/mocks/notes.txt", "content": "hi"} + +# ========================================================================= +# Materialization around prover runs +# ========================================================================= + + +async def test_mocks_materialized_only_during_prover_run(tmp_path, monkeypatch, fake_llm): + """The state-held mock must exist on disk while run_prover executes (the + prover compiles from the real tree) and be gone afterwards (a gave-up + generation must not leave stray sources).""" + target = tmp_path / _MOCK_PATH + seen: list[bool] = [] + + async def observing_prover(*args, **kwargs): + seen.append(target.read_text() == _CONTENT if target.exists() else False) + return ProverReport(rule_status={"r": True}, result_str="ok", link="local://x") + + monkeypatch.setattr("composer.spec.source.prover.run_prover", observing_prover) + monkeypatch.setattr( + "composer.spec.source.prover.get_stream_writer", lambda: (lambda _: None) + ) + prover_tool = get_prover_tool( + prover_opts=ProverOptions(), llm=fake_llm, + main_contract="Dummy", project_root=str(tmp_path), ) - assert ".sol" in res - assert not (tmp_path / "certora" / "mocks" / "notes.txt").exists() + from composer.spec.source.prover import StateWithSkips + await Scenario(StateWithSkips, prover_tool).init( + curr_spec="rule r { assert true; }", + skipped=[], property_rules=[], validations={}, required_validations=[], + rule_skips={}, vacuous_methods={}, acknowledged_vacuous={}, + mocks={_MOCK_PATH: _CONTENT}, + config={"files": ["src/Foo.sol", _MOCK_PATH]}, + ).turn(tool_call_raw("verify_spec", rules=None)).map_run(lambda st: st) + assert seen == [True] + assert not target.exists() + + +# ========================================================================= +# Artifact-store persistence (cache replay from a fresh checkout) +# ========================================================================= + + +def _generated(mocks: dict[str, str]) -> GeneratedCVL: + return GeneratedCVL( + commentary="c", cvl="rule r { assert true; }", + config={"files": ["src/Foo.sol", *mocks]}, + mocks=mocks, + ) + + +async def test_artifact_store_persists_mocks(tmp_path): + store = ProverArtifactStore(str(tmp_path), "Dummy") + store.write_generated_spec(ComponentSpec("oracle"), _generated({_MOCK_PATH: _CONTENT})) + assert (tmp_path / _MOCK_PATH).read_text() == _CONTENT + # The conf referencing the mock is written alongside it. + conf = (tmp_path / "certora" / "confs" / "autospec_oracle.conf").read_text() + assert _MOCK_PATH in conf + + +async def test_artifact_store_rejects_out_of_tree_mock_paths(tmp_path): + store = ProverArtifactStore(str(tmp_path), "Dummy") + for bad in ("src/Evil.sol", "certora/mocks/../../Evil.sol", "/abs/Evil.sol"): + with pytest.raises(AssertionError): + store.write_generated_spec(ComponentSpec("oracle"), _generated({bad: "x"})) From ea436dfba672f52b196adc380fc3e18d178fda16 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:04:18 +0300 Subject: [PATCH 10/13] Cover the agent-mutable setup in the validation digest; feed vacuity evidence to the judge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Digest: _compute_digest gains config/mocks/acknowledged fields (canonical JSON, empty-contributes-nothing so natreq flows and pre-field cache entries hash identically), and the new state_digest helper reads them from the source-mode state. Both stamps use it, so a post-stamp edit_config flag flip, mock rewrite, or new acknowledgment stales the PROVER and FEEDBACK stamps and forces re-verification over the setup that actually gets published. verify_spec stamps over the post-update state since the same Command may clear ledger entries that are part of the digest. Judge evidence: property_feedback_judge's extra_inputs thunk now receives the calling generation's graph state (threaded through the feedback tool), and batch_cvl_generation wires vacuity_judge_evidence as that thunk — outstanding vacuity verdicts, the rule-skip reasons, and the acknowledged-vacuous ledger reach the judge verbatim each round, giving Criteria 5's taxonomy the evidence it audits instead of an unimplementable promise. Co-Authored-By: Claude Fable 5 --- composer/spec/cvl_generation.py | 75 ++++++++++--- composer/spec/feedback.py | 11 +- composer/spec/natspec/author.py | 6 +- composer/spec/source/author.py | 55 +++++++++- composer/spec/source/prover.py | 14 ++- tests/test_cvl_skips.py | 6 +- tests/test_vacuity.py | 184 +++++++++++++++++++++++++++++++- 7 files changed, 322 insertions(+), 29 deletions(-) diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index cefecd5..d667064 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -7,8 +7,11 @@ """ import hashlib +import json from dataclasses import dataclass -from typing import Annotated, Callable, Literal, NotRequired, override, Awaitable, Any, Protocol +from typing import ( + Annotated, Callable, Literal, Mapping, NotRequired, override, Awaitable, Any, Protocol, cast, +) from typing_extensions import TypedDict from pydantic import BaseModel, Field @@ -151,14 +154,55 @@ class CVLGenerationExtra(TypedDict): required_validations: list[str] -def _compute_digest(curr_spec: str, skipped: list[SkippedProperty]) -> str: +def _compute_digest( + curr_spec: str, + skipped: list[SkippedProperty], + *, + config: Mapping[str, Any] | None = None, + mocks: Mapping[str, str] | None = None, + acknowledged: Mapping[str, str] | None = None, +) -> str: digester = hashlib.md5() digester.update(curr_spec.encode()) for s in skipped: digester.update(f"{s.property_title}:{s.reason}".encode()) + # The agent-mutable prover setup joins the digest the empty-contributes-nothing + # way: an absent or empty value hashes identically to the pre-field digest, so + # stamps from flows without these state keys (and cache entries predating them) + # stay valid. Canonical JSON keeps the hash order-independent and unambiguous. + if config: + digester.update(json.dumps(config, sort_keys=True).encode()) + if mocks: + digester.update(json.dumps(mocks, sort_keys=True).encode()) + if acknowledged: + digester.update(json.dumps(acknowledged, sort_keys=True).encode()) return digester.hexdigest() +def state_digest(state: CVLGenerationExtra) -> str: + """Digest of everything the validation stamps attest to: the spec text, the + skip declarations, and — when the flow carries them — the agent-mutable + prover setup (``config``, ``mocks``, and the ``acknowledged_vacuous`` + ledger, layered onto this state by the source-mode ``ProverStateExtra``). + + Both the FEEDBACK and PROVER stamps use this digest, so ANY post-stamp edit + to the setup (an ``edit_config`` flag flip, a rewritten mock, a new + acknowledgment) goes stale on completion and forces a re-verify AND a + re-judge over the setup that will actually be published — the stamp's + attestation would otherwise silently cover state the prover/judge never + saw. The extra keys are read dynamically with empty defaults because flows + without them (natreq) must hash identically to before. + """ + extras = cast(Mapping[str, Any], state) + return _compute_digest( + state["curr_spec"] or "", + state["skipped"], + config=extras.get("config"), + mocks=extras.get("mocks"), + acknowledged=extras.get("acknowledged_vacuous"), + ) + + def check_completion( state: CVLGenerationExtra, ) -> str | None: @@ -166,7 +210,7 @@ def check_completion( spec = state["curr_spec"] if spec is None: return "Completion REJECTED: no spec written yet." - digest = _compute_digest(spec, state["skipped"]) + digest = state_digest(state) validations = state["validations"] required = state["required_validations"] for key in required: @@ -222,14 +266,11 @@ def validate_property_rules( def make_validation_stamper(key: str) -> Callable[[CVLGenerationExtra], dict[str, str]]: """Create a stamper for future prover tool integration. - The stamper reads curr_spec/skipped from state and returns - a dict suitable for merging into the validations state key. + The stamper reads the digest-covered state (see :func:`state_digest`) and + returns a dict suitable for merging into the validations state key. """ def stamp(state: CVLGenerationExtra) -> dict[str, str]: - return {key: _compute_digest( - state["curr_spec"] or "", - state["skipped"], - )} + return {key: state_digest(state)} return stamp @@ -249,13 +290,15 @@ class _LastAttemptCache(BaseModel): DESCRIPTION = "CVL generation" type FeedbackToolImpl = Callable[ - [str, list[SkippedProperty], list[Rebuttal], str], + [str, list[SkippedProperty], list[Rebuttal], str, Mapping[str, Any]], Awaitable[PropertyFeedbackProtocol], ] -"""``(cvl, skipped, rebuttals, within_tool) -> PropertyFeedback``. ``within_tool`` -is the calling ``_FeedbackSchema``'s ``tool_call_id``, plumbed through to the -sub-graph's ``run_to_completion`` so its UI panel anchors under the parent -tool widget.""" +"""``(cvl, skipped, rebuttals, within_tool, state) -> PropertyFeedback``. +``within_tool`` is the calling ``_FeedbackSchema``'s ``tool_call_id``, plumbed +through to the sub-graph's ``run_to_completion`` so its UI panel anchors under +the parent tool widget. ``state`` is the calling generation's full graph state, +so a judge's ``extra_inputs`` thunk can surface flow-specific evidence (e.g. +vacuity verdicts, rule skips, and acknowledgments in the source-mode flow).""" @dataclass class FeedbackToolContext: @@ -299,10 +342,10 @@ async def run(self) -> Command: if spec is None: return tool_return(self.tool_call_id, "No spec put yet") skipped = st["skipped"] - t = await feedback(spec, skipped, self.rebuttals, self.tool_call_id) + t = await feedback(spec, skipped, self.rebuttals, self.tool_call_id, st) msg = f"Good? {t.good}\nFeedback {t.feedback}" if t.good: - digest = _compute_digest(spec, skipped) + digest = state_digest(st) return tool_state_update( self.tool_call_id, msg, validations={FEEDBACK_VALIDATION_KEY: digest}, diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index 5f64d7b..1053772 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -1,5 +1,5 @@ -from typing import Callable, NotRequired, Sequence +from typing import Any, Callable, Mapping, NotRequired, Sequence from typing_extensions import TypedDict from composer.spec.service_host import Sort, ServiceHost @@ -59,9 +59,13 @@ def property_feedback_judge( prompt: InjectedTemplate[Properties] | TemplateInstantiation, props: list[PropertyFormulation], *, - extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None, + extra_inputs: list[str | dict] | Callable[[Mapping[str, Any]], list[str | dict]] | None = None, system_prompt: TemplateInstantiation | None = None, ) -> FeedbackToolContext: + # ``extra_inputs`` may be a static list, or a thunk over the calling + # generation's graph state (evaluated per feedback round, so the judge sees + # the evidence as it stands at judging time — e.g. the source-mode flow's + # vacuity verdicts, rule skips, and acknowledgments). if system_prompt is None: system_prompt = FeedbackSystemTemplate.bind({"sort": env.sort}) @@ -105,13 +109,14 @@ async def the_tool( skipped: Sequence[SkippedProperty], rebuttals: Sequence[Rebuttal], within_tool: str, + state: Mapping[str, Any], ) -> PropertyFeedback: input_parts: list[str | dict] = [] if extra_inputs: if isinstance(extra_inputs, list): input_parts.extend(extra_inputs) else: - input_parts.extend(extra_inputs()) + input_parts.extend(extra_inputs(state)) input_parts.append("The proposed CVL file is") input_parts.append(cvl) diff --git a/composer/spec/natspec/author.py b/composer/spec/natspec/author.py index abcfb5f..e1fc721 100644 --- a/composer/spec/natspec/author.py +++ b/composer/spec/natspec/author.py @@ -1,5 +1,5 @@ from dataclasses import dataclass -from typing import Callable, Literal, override, Annotated, Literal +from typing import Any, Callable, Literal, Mapping, override, Annotated, Literal from pydantic import Field, BaseModel, Discriminator from typing_extensions import TypedDict @@ -209,7 +209,9 @@ async def generate_cvl_batch( if (cached := await root_ctx.cache_get(AuthorResult)) is not None: return cached.result_wrapped - def stub_feedback_extras() -> list[str | dict]: + def stub_feedback_extras(_state: Mapping[str, Any]) -> list[str | dict]: + # The judge-evidence thunk receives the generation's graph state; the + # natreq judge's extras are state-independent, so it is unused here. return [ f"The current typechecking stub for the {contract_name} contract is", stub_reader(), diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index e531ecf..5d3f280 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -1,4 +1,4 @@ -from typing import NotRequired, override, Literal, Annotated +from typing import Any, Mapping, NotRequired, override, Literal, Annotated from typing_extensions import TypedDict import json @@ -489,6 +489,54 @@ async def run(self) -> Command | str: ) +def vacuity_judge_evidence(state: Mapping[str, Any]) -> list[str | dict]: + """The prover-side evidence the feedback judge audits (Criteria 5's + filter-legitimacy taxonomy): outstanding vacuity verdicts, the rule-skip + map with its recorded reasons, and the acknowledged-vacuous ledger, passed + verbatim from the generation's graph state. + + Wired as the ``extra_inputs`` thunk of ``property_feedback_judge`` at the + ``batch_cvl_generation`` call site — the judge cannot re-derive any of this + from the CVL text, because vacuity is a prover-run observation, not a + spec-text property. Evaluated per feedback round over the then-current + state. Empty state contributes nothing (the natreq-style silent default). + """ + parts: list[str | dict] = [] + vacuous: dict[str, str] = state.get("vacuous_methods") or {} + if vacuous: + parts.append( + "The prover flagged the following method(s) as VACUOUS (their sanity check " + "failed: every rule instantiated with them passes trivially). Verdicts clear " + "automatically once a run shows the method healthy — these are still " + "outstanding:\n" + "\n".join(f" - {m}: {d}" for m, d in sorted(vacuous.items())) + ) + rule_skips: dict[str, str] = state.get("rule_skips") or {} + if rule_skips: + parts.append( + "The author marked the following rule(s) as \"expected to fail\" (excluded " + "from the prover pass/fail verdict), with these reasons:\n" + + "\n".join(f" - {r}: {reason}" for r, reason in sorted(rule_skips.items())) + ) + acks: dict[str, str] = state.get("acknowledged_vacuous") or {} + if acks: + lines: list[str] = [] + for m, record in sorted(acks.items()): + try: + rec = json.loads(record) + lines.append( + f" - {m}: steps attempted: {', '.join(rec['steps_attempted'])}; " + f"justification: {rec['justification']}" + ) + except (ValueError, KeyError, TypeError): + lines.append(f" - {m}: {record}") + parts.append( + "The acknowledged-vacuous ledger (structured records from the " + "`acknowledge_vacuous_method` tool — audit each acknowledgment on its merits " + "per the Criteria 5 taxonomy):\n" + "\n".join(lines) + ) + return parts + + _PropertyGenTemplate = TypedTemplate[PropertyGenParams]("property_generation_prompt.j2") async def batch_cvl_generation( @@ -565,7 +613,10 @@ async def batch_cvl_generation( ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({ "sort": "existing", "context": component - }), props + }), props, + # Vacuity verdicts, rule skips, and acknowledgments reach the judge with + # every feedback round — the evidence Criteria 5's taxonomy audits. + extra_inputs=vacuity_judge_evidence, ) res_state = await run_cvl_generator( diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index ef97ec8..a09c79e 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -14,7 +14,7 @@ import time from contextlib import contextmanager from pathlib import Path -from typing import Annotated, Callable, Iterator, override, AsyncContextManager +from typing import Annotated, Callable, Iterator, cast, override, AsyncContextManager from typing_extensions import TypedDict, NotRequired from langchain_core.tools import InjectedToolCallId, tool, BaseTool @@ -369,9 +369,19 @@ async def verify_spec( prover_link=result.link, vacuous_methods=vacuity_update, acknowledged_vacuous=ack_update, ) + # Stamp over the POST-update state: this same Command may clear + # acknowledged_vacuous entries (ack_update), and the ledger is part of + # the validation digest — stamping the pre-update state would yield a + # digest check_completion can never match. + effective = cast(StateWithSkips, { + **state, + "acknowledged_vacuous": _merge_rule_skips( + state.get("acknowledged_vacuous", {}), ack_update + ), + }) return tool_state_update( tool_call_id=tool_call_id, content=result.result_str, - prover_link=result.link, validations=stamper(state), + prover_link=result.link, validations=stamper(effective), vacuous_methods=vacuity_update, acknowledged_vacuous=ack_update, ) return tool_state_update( diff --git a/tests/test_cvl_skips.py b/tests/test_cvl_skips.py index 85556bd..8d843e1 100644 --- a/tests/test_cvl_skips.py +++ b/tests/test_cvl_skips.py @@ -6,7 +6,7 @@ """ import pytest -from typing import NotRequired, override, Iterable, Callable, Protocol +from typing import Any, Mapping, NotRequired, override, Iterable, Callable, Protocol from dataclasses import dataclass @@ -103,7 +103,8 @@ async def dummy_feedback( spec: str, s: list[SkippedProperty], rebuttals: list[Rebuttal], - within_tool: str + within_tool: str, + state: Mapping[str, Any], ) -> Feedback: return Feedback(good=True, feedback="") @@ -130,6 +131,7 @@ async def impl( skipped: list[SkippedProperty], rebuttals: list[Rebuttal], within_tool: str, + state: Mapping[str, Any], ) -> Feedback: for sk in skipped: if sk.property_title not in skippable: diff --git a/tests/test_vacuity.py b/tests/test_vacuity.py index ba0ad3f..c8cd3cc 100644 --- a/tests/test_vacuity.py +++ b/tests/test_vacuity.py @@ -18,8 +18,11 @@ format_vacuity_alert, instantiated_methods, ) -from composer.spec.cvl_generation import check_completion -from composer.spec.source.author import AcknowledgeVacuousMethod, ExpectRuleFailure +from composer.spec.cvl_generation import check_completion, state_digest +from composer.spec.source.author import ( + AcknowledgeVacuousMethod, ConfigEditTool, ExpectRuleFailure, WriteMockTool, + vacuity_judge_evidence, +) from composer.spec.source.prover import StateWithSkips, VALIDATION_KEY from graphcore.testing import Scenario, tool_call_raw, ToolCallDict @@ -432,3 +435,180 @@ async def test_healthy_reinstantiation_clears_acknowledgment(self, certora_prove assert acks == {} # cleared by the healthy run, not re-established assert "vacuity_guard" in last_prover_msg assert "WITHHELD" in last_prover_msg + + +# ========================================================================= +# Digest coverage of the agent-mutable setup +# ========================================================================= + + +def _digest_state(**overrides) -> StateWithSkips: + base: dict = dict( + curr_spec="rule r { assert true; }", + skipped=[], + property_rules=[], + validations={}, + required_validations=[VALIDATION_KEY], + rule_skips={}, + vacuous_methods={}, + acknowledged_vacuous={}, + mocks={}, + config={"files": ["src/Foo.sol"]}, + ) + base.update(overrides) + return base # type: ignore[return-value] + + +class TestStateDigest: + """The validation stamps must cover everything the agent can mutate after + stamping: the prover config, the mocks, and the acknowledgment ledger.""" + + def test_config_change_changes_digest(self): + assert state_digest(_digest_state()) != state_digest( + _digest_state(config={"files": ["src/Foo.sol"], "optimistic_fallback": True}) + ) + + def test_mock_change_changes_digest(self): + assert state_digest(_digest_state()) != state_digest( + _digest_state(mocks={"certora/mocks/x/M.sol": "contract M {}"}) + ) + + def test_acknowledgment_changes_digest(self): + assert state_digest(_digest_state()) != state_digest( + _digest_state(acknowledged_vacuous={DEPOSIT: "{}"}) + ) + + def test_vacuous_verdicts_do_not_change_digest(self): + """Verdicts are prover observations, not agent edits: the stamp is + granted in the same Command that records them, so including them would + make every stamp instantly stale.""" + assert state_digest(_digest_state()) == state_digest( + _digest_state(vacuous_methods={DEPOSIT: "diagnosis"}) + ) + + def test_absent_and_empty_extras_hash_identically(self): + """Back-compat: flows without the source-mode state keys (natreq) and + checkpoints predating them must produce the pre-field digest.""" + bare = { + "curr_spec": "rule r { assert true; }", + "skipped": [], + "property_rules": [], + "validations": {}, + "required_validations": [], + } + assert state_digest(bare) == state_digest( # type: ignore[arg-type] + _digest_state(config={}, mocks={}, acknowledged_vacuous={}) + ) + + +class TestStampStalenessAfterSetupEdit: + """End-to-end: a PROVER stamp obtained before an edit_config / write_mock + call must not survive it — the persisted conf/mocks were never verified.""" + + def _scenario(self, certora_prover: ProverMock, *responses: ProverToolResponse): + prover_tool = certora_prover(responses) + return Scenario( + StateWithSkips, + prover_tool, + ConfigEditTool.as_tool("edit_config"), + WriteMockTool.bind("autospec_test").as_tool("write_mock"), + _result_tool, + ).init( + curr_spec=_SPEC, + skipped=[], + property_rules=[], + validations={}, + required_validations=[VALIDATION_KEY], + rule_skips={}, + vacuous_methods={}, + acknowledged_vacuous={}, + mocks={}, + config={"files": ["src/Foo.sol"]}, + ) + + @pytest.mark.asyncio + async def test_stamp_survives_without_edits(self, certora_prover: ProverMock): + scenario = self._scenario( + certora_prover, _vacuous_report(rule_status={"solvency": True}), + ) + accepted = await scenario.turns(_verify(), _result("done")).map_run(_result_accepted) + assert accepted + + @pytest.mark.asyncio + async def test_config_edit_invalidates_stamp(self, certora_prover: ProverMock): + scenario = self._scenario( + certora_prover, _vacuous_report(rule_status={"solvency": True}), + ) + accepted = await scenario.turns( + _verify(), + tool_call_raw("edit_config", edits=[ + {"type": "set_flag", "flag": "optimistic_fallback", "value": True}, + ]), + _result("done"), + ).map_run(_result_accepted) + assert not accepted + + @pytest.mark.asyncio + async def test_mock_write_invalidates_stamp(self, certora_prover: ProverMock): + scenario = self._scenario( + certora_prover, _vacuous_report(rule_status={"solvency": True}), + ) + accepted = await scenario.turns( + _verify(), + tool_call_raw("write_mock", file_name="M.sol", content="contract M {}"), + _result("done"), + ).map_run(_result_accepted) + assert not accepted + + @pytest.mark.asyncio + async def test_reverify_after_edit_restores_stamp(self, certora_prover: ProverMock): + scenario = self._scenario( + certora_prover, + _vacuous_report(rule_status={"solvency": True}), + _vacuous_report(rule_status={"solvency": True}), + ) + accepted = await scenario.turns( + _verify(), + tool_call_raw("edit_config", edits=[ + {"type": "set_flag", "flag": "optimistic_fallback", "value": True}, + ]), + _verify(), + _result("done"), + ).map_run(_result_accepted) + assert accepted + + +# ========================================================================= +# Judge evidence thunk +# ========================================================================= + + +class TestVacuityJudgeEvidence: + def test_empty_state_contributes_nothing(self): + assert vacuity_judge_evidence({}) == [] + assert vacuity_judge_evidence( + {"vacuous_methods": {}, "rule_skips": {}, "acknowledged_vacuous": {}} + ) == [] + + def test_all_three_sections_rendered(self): + record = json.dumps({ + "steps_attempted": ["mock", "summary_fix"], + "justification": "mock failed to compile; summary fix rejected", + }) + parts = vacuity_judge_evidence({ + "vacuous_methods": {DEPOSIT: "sanity-failed in 2 of 2 rule(s)"}, + "rule_skips": {"solvency": "expected CEX per threat model"}, + "acknowledged_vacuous": {DEPOSIT: record}, + }) + assert len(parts) == 3 + vacuous_part, skips_part, acks_part = (str(x) for x in parts) + assert "VACUOUS" in vacuous_part and DEPOSIT in vacuous_part + assert "solvency" in skips_part and "expected CEX" in skips_part + assert "acknowledge_vacuous_method" in acks_part + assert "mock, summary_fix" in acks_part + assert "failed to compile" in acks_part + + def test_malformed_ack_record_falls_back_to_raw(self): + parts = vacuity_judge_evidence({"acknowledged_vacuous": {DEPOSIT: "not json"}}) + assert len(parts) == 1 + assert "not json" in str(parts[0]) From c7580717c74e8dc56e42ed409896d9984941326d Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:06:41 +0300 Subject: [PATCH 11/13] Clamp agent-settable prover flags: 2x-default timeout, loop_iter <= 5, add-only optimistic_fallback MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Owner decision on run-cost ownership: SetProverFlag now caps global_timeout at twice the pipeline default (derived from DEFAULT_GLOBAL_TIMEOUT, the single source make_prover_options applies — no hardcoded ceiling), caps loop_iter at 5, and makes optimistic_fallback add-only — the agent may enable it (repair-ladder step 3) but can never set it false, so an autosetup-emitted recommendation cannot be reverted into the vacuity it prevents. The tool description renders the computed bounds via an explicit __doc__ so it cannot drift from the validator, and the flag name is a shared Literal alias making the validator match exhaustive. Co-Authored-By: Claude Fable 5 --- composer/spec/source/author.py | 54 ++++++++++++++++++++++++++-------- tests/test_config_edit.py | 34 +++++++++++++++++---- 2 files changed, 70 insertions(+), 18 deletions(-) diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index 5d3f280..bde724d 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -20,6 +20,7 @@ from composer.spec.context import WorkflowContext, CVLGeneration, SourceCode from composer.spec.prop import PropertyFormulation from composer.spec.system_model import ContractComponentInstance, SolidityIdentifier +from composer.prover.core import DEFAULT_GLOBAL_TIMEOUT from composer.spec.source.prover import ProverStateExtra, DELETE_SKIP, VALIDATION_KEY as PROVER_VALIDATION_KEY from langgraph.graph import MessagesState from langgraph.runtime import get_runtime @@ -312,15 +313,35 @@ class RemoveLink(BaseModel): source_contract_name : SolidityIdentifier = Field(description="The Solidity identifier of the contract whose link should be removed") link_field_name : str = Field(description="The storage field holding the link within `source_contract_name` that should be removed") +# Agent-facing cost/soundness clamps for SetProverFlag (owner decision): +# * global_timeout may be raised to at most 2x the pipeline default the prover runs +# with anyway (DEFAULT_GLOBAL_TIMEOUT, the single source `make_prover_options` +# applies) — run cost stays owner-bounded, not agent-controlled. +# * loop_iter is capped at 5 unrollings. +# * optimistic_fallback is ADD-ONLY: the agent may enable it (repair-ladder step 3) +# but may never set it false — that could revert an autosetup-emitted +# recommendation, silently re-introducing the vacuity the flag was recommended for. +_MAX_GLOBAL_TIMEOUT = 2 * int(DEFAULT_GLOBAL_TIMEOUT) +_MAX_LOOP_ITER = 5 + +type ProverFlagName = Literal[ + "optimistic_fallback", "loop_iter", "global_timeout", "contract_recursion_limit" +] + + class SetProverFlag(BaseModel): - """ + # An explicit __doc__ (rather than a docstring literal) so the tool description the + # LLM sees carries the computed clamp bounds instead of hardcoded copies of them. + __doc__ = f""" Set a whitelisted top-level prover flag in the configuration: - * `optimistic_fallback` (bool): assume unresolved low-level calls (`.call{value: ...}`, `send`, - `transfer`) succeed instead of HAVOCing and always being able to fail. Step 3 of the vacuity - repair ladder. - * `loop_iter` (int, 1-8): the number of loop unrollings the prover performs. - * `global_timeout` (int, 1-7200): the overall run timeout in seconds. + * `optimistic_fallback` (bool, add-only — may only be set to `true`): assume unresolved + low-level calls (`.call{{value: ...}}`, `send`, `transfer`) succeed instead of HAVOCing + and always being able to fail. Step 3 of the vacuity repair ladder. Setting it back to + `false` is not allowed (it could revert an autosetup recommendation). + * `loop_iter` (int, 1-{_MAX_LOOP_ITER}): the number of loop unrollings the prover performs. + * `global_timeout` (int, 1-{_MAX_GLOBAL_TIMEOUT}): the overall run timeout in seconds + (capped at twice the pipeline default). * `contract_recursion_limit` (int, 0-10): the allowed depth of recursive calls between contracts. """ # `rule_sanity` and `optimistic_loop` are DELIBERATELY not in this whitelist: vacuity @@ -329,10 +350,10 @@ class SetProverFlag(BaseModel): # anyway — the whitelist keeps the agent from even trying (and from being confused by a # silently-overridden edit). type: Literal["set_flag"] - flag: Literal["optimistic_fallback", "loop_iter", "global_timeout", "contract_recursion_limit"] + flag: ProverFlagName value: bool | int = Field(description="The value to set: a bool for `optimistic_fallback`, an int for the other flags") -def _validate_prover_flag(flag: str, value: bool | int) -> str | None: +def _validate_prover_flag(flag: ProverFlagName, value: bool | int) -> str | None: """Per-flag validation for SetProverFlag; returns an error message or None if valid. NB: ``bool`` is a subclass of ``int``, so the bool checks must come before any int check. @@ -340,16 +361,25 @@ def _validate_prover_flag(flag: str, value: bool | int) -> str | None: if flag == "optimistic_fallback": if not isinstance(value, bool): return f"optimistic_fallback expects a boolean value, got {value!r}" + if value is False: + return ( + "optimistic_fallback is add-only: it may be set to true (repair-ladder " + "step 3) but never back to false — autosetup may have recommended it, and " + "unsetting that recommendation would re-introduce the vacuity it prevents" + ) return None if isinstance(value, bool) or not isinstance(value, int): return f"{flag} expects an integer value, got {value!r}" match flag: case "loop_iter": - if not (1 <= value <= 8): - return f"loop_iter must be between 1 and 8, got {value}" + if not (1 <= value <= _MAX_LOOP_ITER): + return f"loop_iter must be between 1 and {_MAX_LOOP_ITER}, got {value}" case "global_timeout": - if not (1 <= value <= 7200): - return f"global_timeout must be between 1 and 7200 (seconds), got {value}" + if not (1 <= value <= _MAX_GLOBAL_TIMEOUT): + return ( + f"global_timeout must be between 1 and {_MAX_GLOBAL_TIMEOUT} (seconds, " + f"at most twice the pipeline default), got {value}" + ) case "contract_recursion_limit": if not (0 <= value <= 10): return f"contract_recursion_limit must be between 0 and 10, got {value}" diff --git a/tests/test_config_edit.py b/tests/test_config_edit.py index 965d491..ec97e57 100644 --- a/tests/test_config_edit.py +++ b/tests/test_config_edit.py @@ -9,8 +9,10 @@ from langgraph.graph import MessagesState +from composer.prover.core import DEFAULT_GLOBAL_TIMEOUT from composer.spec.source.author import ( ConfigEditTool, AddFile, RemoveFile, AddLink, RemoveLink, SetProverFlag, + _MAX_GLOBAL_TIMEOUT, ) from composer.spec.source.prover import ProverStateExtra @@ -225,6 +227,24 @@ async def test_optimistic_fallback_rejects_int(self): ).map_run(_config) assert "optimistic_fallback" not in config + async def test_optimistic_fallback_is_add_only(self): + """The agent may enable the flag but never disable it — setting false + could revert an autosetup-emitted recommendation.""" + config = await _scenario(files=[]).turn( + _edit(_set_flag("optimistic_fallback", False)), + ).map_run(_config) + assert "optimistic_fallback" not in config + + async def test_optimistic_fallback_cannot_unset_autosetup_recommendation(self): + """An autosetup-recommended true in the base config survives a false edit.""" + scenario = Scenario(ConfigTestState, TOOL).init( + config={"files": [], "optimistic_fallback": True}, rule_skips={}, + ) + config = await scenario.turn( + _edit(_set_flag("optimistic_fallback", False)), + ).map_run(_config) + assert config["optimistic_fallback"] is True + async def test_set_loop_iter(self): config = await _scenario(files=[]).turn( _edit(_set_flag("loop_iter", 3)), @@ -232,7 +252,7 @@ async def test_set_loop_iter(self): assert config["loop_iter"] == 3 async def test_loop_iter_out_of_range(self): - for bad in (0, 9): + for bad in (0, 6): config = await _scenario(files=[]).turn( _edit(_set_flag("loop_iter", bad)), ).map_run(_config) @@ -245,15 +265,17 @@ async def test_loop_iter_rejects_bool(self): ).map_run(_config) assert "loop_iter" not in config - async def test_set_global_timeout(self): + async def test_set_global_timeout_at_clamp(self): config = await _scenario(files=[]).turn( - _edit(_set_flag("global_timeout", 3600)), + _edit(_set_flag("global_timeout", _MAX_GLOBAL_TIMEOUT)), ).map_run(_config) - assert config["global_timeout"] == 3600 + assert config["global_timeout"] == _MAX_GLOBAL_TIMEOUT - async def test_global_timeout_too_large(self): + async def test_global_timeout_clamped_to_twice_default(self): + """The ceiling derives from the pipeline default, not a hardcoded cap.""" + assert _MAX_GLOBAL_TIMEOUT == 2 * int(DEFAULT_GLOBAL_TIMEOUT) config = await _scenario(files=[]).turn( - _edit(_set_flag("global_timeout", 7201)), + _edit(_set_flag("global_timeout", _MAX_GLOBAL_TIMEOUT + 1)), ).map_run(_config) assert "global_timeout" not in config From 16e18f68af4b8b9a847121099a56aed77eca497a Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 03:16:19 +0300 Subject: [PATCH 12/13] Remove empty mock namespace dirs after prover-run materialization materialized_mocks unlinked the mock files but left the created certora/mocks// directories behind, so gave-up generations polluted the project tree with empty dirs. Cleanup now rmdirs upward from each mock's parent to the mocks root, stopping at any non-empty dir so concurrent generations' materialized mocks are untouched. Co-Authored-By: Claude Fable 5 --- composer/spec/source/prover.py | 15 ++++++++++++++- tests/test_write_mock.py | 17 +++++++++++++++++ 2 files changed, 31 insertions(+), 1 deletion(-) diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index a09c79e..66d5d08 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -40,7 +40,7 @@ from composer.diagnostics.timing import RunSummary, get_run_summary from graphcore.graph import tool_state_update from composer.spec.util import temp_certora_file -from composer.spec.gen_types import SPECS_DIR +from composer.spec.gen_types import MOCKS_DIR, SPECS_DIR _logger = logging.getLogger("composer.prover") @@ -275,6 +275,19 @@ def materialized_mocks(root: str, mocks: dict[str, str]) -> Iterator[None]: finally: for target in written: target.unlink(missing_ok=True) + # Also drop the namespace dirs we created (up to and including the + # mocks root, never above it) so gave-up generations leave no empty + # directories behind. rmdir refuses non-empty dirs, so a concurrent + # generation's still-materialized mocks are never disturbed. + mocks_root = Path(root) / MOCKS_DIR + for target in written: + directory = target.parent + while directory == mocks_root or mocks_root in directory.parents: + try: + directory.rmdir() + except OSError: + break + directory = directory.parent def _prover_sem(cloud: bool) -> AsyncContextManager[None]: diff --git a/tests/test_write_mock.py b/tests/test_write_mock.py index f865a4e..0411f4b 100644 --- a/tests/test_write_mock.py +++ b/tests/test_write_mock.py @@ -114,6 +114,23 @@ async def observing_prover(*args, **kwargs): ).turn(tool_call_raw("verify_spec", rules=None)).map_run(lambda st: st) assert seen == [True] assert not target.exists() + # The namespace dirs created for the run are cleaned up too. + assert not (tmp_path / "certora" / "mocks").exists() + + +async def test_materialization_preserves_other_generations_dirs(tmp_path): + """Cleanup only removes the dirs this generation emptied: a concurrent + generation's still-materialized mocks (and the shared mocks root holding + them) must survive.""" + from composer.spec.source.prover import materialized_mocks + + other = tmp_path / "certora" / "mocks" / "other_ns" / "Keep.sol" + other.parent.mkdir(parents=True) + other.write_text("// keep") + with materialized_mocks(str(tmp_path), {_MOCK_PATH: _CONTENT}): + assert (tmp_path / _MOCK_PATH).read_text() == _CONTENT + assert not (tmp_path / "certora" / "mocks" / _NAMESPACE).exists() + assert other.read_text() == "// keep" # ========================================================================= From 9255055f73a03794254e32515246e5f9306d3db4 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 4 Jul 2026 19:41:20 +0300 Subject: [PATCH 13/13] Restore certora_autosetup to origin/master; autosetup work moves to its own PR The autosetup-side vacuity prevention (payable-NONDET guard, optimistic_fallback recommendation, extra_flags plumbing) was extracted and reshaped on shelly/ap-autosetup-vacuity-prevention (PR #52), so this branch drops its certora_autosetup changes. The whole certora_autosetup tree is synced to current origin/master (which includes the build_job_msg refactor) so the package stays internally consistent. Co-Authored-By: Claude Fable 5 --- certora_autosetup/autosetup/autosetup.py | 20 ------ certora_autosetup/conf_runner/callbacks.py | 2 - certora_autosetup/conf_runner/conf_runner.py | 1 - certora_autosetup/setup/call_resolution.py | 45 +------------ certora_autosetup/setup/sanity.py | 11 ---- certora_autosetup/setup/setup_summaries.py | 52 +-------------- .../utils/enhanced_config_manager.py | 65 ++++--------------- 7 files changed, 18 insertions(+), 178 deletions(-) diff --git a/certora_autosetup/autosetup/autosetup.py b/certora_autosetup/autosetup/autosetup.py index f79905f..a174db4 100644 --- a/certora_autosetup/autosetup/autosetup.py +++ b/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(): @@ -903,20 +897,6 @@ 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: diff --git a/certora_autosetup/conf_runner/callbacks.py b/certora_autosetup/conf_runner/callbacks.py index 45621a4..1d1ff15 100644 --- a/certora_autosetup/conf_runner/callbacks.py +++ b/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) diff --git a/certora_autosetup/conf_runner/conf_runner.py b/certora_autosetup/conf_runner/conf_runner.py index 21ede3f..a267cfe 100644 --- a/certora_autosetup/conf_runner/conf_runner.py +++ b/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( diff --git a/certora_autosetup/setup/call_resolution.py b/certora_autosetup/setup/call_resolution.py index cace954..92f7fc2 100644 --- a/certora_autosetup/setup/call_resolution.py +++ b/certora_autosetup/setup/call_resolution.py @@ -125,25 +125,6 @@ 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: @@ -188,12 +169,6 @@ 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). @@ -362,17 +337,6 @@ 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. @@ -509,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) @@ -589,12 +556,6 @@ 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 diff --git a/certora_autosetup/setup/sanity.py b/certora_autosetup/setup/sanity.py index 3221eae..f6d3b1b 100644 --- a/certora_autosetup/setup/sanity.py +++ b/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 : " - 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) diff --git a/certora_autosetup/setup/setup_summaries.py b/certora_autosetup/setup/setup_summaries.py index 06471f2..14cc96e 100755 --- a/certora_autosetup/setup/setup_summaries.py +++ b/certora_autosetup/setup/setup_summaries.py @@ -1668,33 +1668,6 @@ 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, @@ -1728,12 +1701,6 @@ 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 = [] @@ -1763,15 +1730,6 @@ 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 ( @@ -2299,15 +2257,7 @@ 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", - # 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"], - }, + properties={"visibility": "internal"}, summary_type="NONDET", ), ] diff --git a/certora_autosetup/utils/enhanced_config_manager.py b/certora_autosetup/utils/enhanced_config_manager.py index 20831f5..afe060b 100644 --- a/certora_autosetup/utils/enhanced_config_manager.py +++ b/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 ": ". + 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 : " + Format: ": " (with " " 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: @@ -123,12 +132,6 @@ 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, @@ -205,38 +208,6 @@ 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, @@ -246,7 +217,6 @@ 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. @@ -259,8 +229,6 @@ 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 @@ -282,11 +250,6 @@ 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", [])