Add verification groups: agent-declared parallel prover runs with per-group summarization

composer/spec/source/agent_groups.py

@@ -0,0 +1,203 @@
+"""Agent-declared verification groups over properties.
+
+The transparent, agent-controlled splitting policy. Rather than infer a partition,
+the CVL author *declares* it: a set of groups, each naming the properties it
+verifies and the summaries it installs (per function). This
+rides the structure autoprover already has — the property -> rule mapping and its
+coverage guarantee (every non-skipped property is mapped to rules) — so a group is
+expressed in the agent's native unit (properties), and coverage composes: every
+property lands in exactly one group, every group's owned rules are verified
+(per-group completion), therefore every property is covered.
+
+Groups here are NOT opaque. The agent names them, sees their membership, and
+controls each group's summaries (`summaries`). (The substrate group also carries a
+per-group conf overlay, but the agent-facing tool does not expose it yet — a
+per-group prover-config knob is new, unvalidated, and unreviewed by the judge, so it
+is deferred to a follow-up with proper guardrails.)
+The machinery only expands properties to rules, enforces a disjoint rule partition,
+and validates coverage; the group count is capped by rejecting an over-cap declaration
+(:func:`over_cap_message`), not by merging. The per-group spec is the
+shared base spec plus a `methods{}` block of the summaries that group declared
+(:func:`composer.spec.source.verification_groups.append_summaries`); a function a
+group does not summarize is verified precise there.
+"""
+
+from pydantic import BaseModel, Field
+
+from composer.spec.cvl_generation import PropertyRuleMapping
+from composer.spec.source.verification_groups import (
+    VerificationGroup, append_summaries, cap_groups,
+)
+
+
+def validate_declared_coverage(
+    specs: list["VerificationGroupSpec"],
+    *,
+    all_properties: set[str],
+    skipped: set[str],
+) -> str | None:
+    """Whether the declared groups cover the property space exactly once.
+
+    Reuses autoprover's coverage contract: every non-skipped property must be
+    assigned to exactly one group; no unknown or skipped property may be assigned.
+    Returns None when valid, else one message enumerating every problem — the shape
+    an agent tool hands back so the author can fix its declaration."""
+    assigned: list[str] = [str(m.property_title) for s in specs for m in s.property_rules]
+    seen: set[str] = set()
+    duplicated: set[str] = set()
+    for p in assigned:
+        (duplicated if p in seen else seen).add(p)
+    required = all_properties - skipped
+    problems: list[str] = []
+    if duplicated:
+        problems.append(f"properties assigned to more than one group: {sorted(duplicated)}")
+    if missing := required - seen:
+        problems.append(f"non-skipped properties assigned to no group: {sorted(missing)}")
+    if unknown := seen - all_properties:
+        problems.append(f"unknown property titles: {sorted(unknown)}")
+    if skipped_assigned := seen & skipped:
+        problems.append(f"skipped properties should not be assigned to a group: {sorted(skipped_assigned)}")
+    return "; ".join(problems) if problems else None
+
+
+# --- Agent-facing declaration (the tool input / state shape) ----------------
+
+
+class VerificationGroupSpec(BaseModel):
+    """One verification group as the CVL author declares it — the transparent,
+    agent-controlled unit. Carries its own property->rule mapping so the rules are
+    known during authoring (the publish-time mapping is their union) and the functions
+    it keeps precise. (Per-group conf overrides are supported by the substrate but not
+    exposed here yet — see the module docstring.)"""
+    name: str = Field(description="A short, unique, human-readable name for this group (used in run/spec names).")
+    property_rules: list[PropertyRuleMapping] = Field(
+        description="The properties this group verifies and, for each, the rule/invariant names in "
+        "the spec that verify it. A group may cover multiple properties. Across all groups every "
+        "non-skipped property must appear in exactly one group."
+    )
+    summaries: dict[str, str] = Field(
+        default_factory=dict,
+        description="The summaries THIS group installs: each key a hostile function, each value the full "
+        "CVL methods{} entry to summarize it here (e.g. \"function C.f(uint) external => NONDET;\", a ghost "
+        "mirror, a model). A function absent from this map is verified as the base spec has it in this "
+        "group — precise only if the base spec (incl. its imports) does not already summarize it. The same "
+        "function may be summarized differently in different groups — choose, per group, "
+        "the weakest summary sound for that group's rules, and reuse the same entry across groups where "
+        "it is sound (consistency).",
+    )
+
+
+def owned_rules_per_group(specs: list[VerificationGroupSpec]) -> list[frozenset[str]]:
+    """Each spec's owned rules under first-declaration-wins, aligned to ``specs`` by index.
+
+    A group's owned rules are the union of its properties' rules; a rule declared by more than
+    one group is owned by the FIRST that declares it, so the partition stays disjoint — every
+    rule has exactly one owner."""
+    claimed: set[str] = set()
+    owned_per: list[frozenset[str]] = []
+    for s in specs:
+        owned = {str(r) for m in s.property_rules for r in m.rules} - claimed
+        claimed |= owned
+        owned_per.append(frozenset(owned))
+    return owned_per
+
+
+def over_cap_message(specs: list[VerificationGroupSpec], cap: int) -> str | None:
+    """A rejection message when the agent declared MORE groups than the cap, else ``None``.
+
+    Each group is a separate prover run, so the count is bounded. Rather than silently auto-merge the
+    declaration (which would undo the split the agent deliberately chose), the declaring tool rejects an
+    over-cap declaration and asks the agent to refactor — and SUGGESTS a concrete valid merge (the greedy,
+    most-agreeing-summaries merge :func:`cap_groups` computes), which the agent can adopt or improve."""
+    if len(specs) <= cap:
+        return None
+    # A lightweight sim of the partition, run through cap_groups to name one valid merge to suggest.
+    sim = [
+        VerificationGroup(name=s.name, owned_rules=owned, summaries=dict(s.summaries))
+        for s, owned in zip(specs, owned_rules_per_group(specs))
+    ]
+    suggested = "; ".join(g.name for g in cap_groups(sim, cap))
+    return (
+        f"You declared {len(specs)} verification groups but at most {cap} are allowed — each group is a "
+        f"separate prover run (raise the limit via AUTOPROVER_MAX_VERIFICATION_GROUPS). Merge groups until "
+        f"there are at most {cap}: combine the ones whose rules can share the same summaries — a merged "
+        f"group keeps a summary only where both groups agree, else that function drops to precise. One valid "
+        f"merge to adopt or improve: {suggested}."
+    )
+
+
+def groups_from_specs(
+    base_spec: str,
+    specs: list[VerificationGroupSpec],
+    *,
+    cap: int,
+) -> list[VerificationGroup]:
+    """Expand the agent's declared group specs into runnable :class:`VerificationGroup`s
+    (coverage assumed already validated with :func:`validate_declared_coverage`).
+
+    Owned rules are partitioned first-declaration-wins (:func:`owned_rules_per_group`). Each
+    group's spec installs the summaries it declared (:func:`append_summaries`); a function it
+    does not summarize is verified precise. The declaration must already be within ``cap`` — the
+    declaring tool rejects an over-cap declaration (:func:`over_cap_message`) rather than merging
+    — so this asserts the bound instead of capping."""
+    assert len(specs) <= cap, (
+        f"{len(specs)} groups exceeds cap {cap}; over-cap declarations are rejected at declare time"
+    )
+    return [
+        VerificationGroup(
+            name=s.name,
+            owned_rules=owned,
+            spec_contents=append_summaries(base_spec, s.summaries),
+            summaries=dict(s.summaries),
+            # conf_overlay left at its substrate default: not exposed to the agent.
+        )
+        for s, owned in zip(specs, owned_rules_per_group(specs))
+    ]
+
+
+def render_group_plan_for_judge(specs: list["VerificationGroupSpec"]) -> str | None:
+    """A judge-facing note describing the verification-group plan, or ``None`` when
+    no groups are declared.
+
+    The feedback judge reviews the *base* spec (``curr_spec``), which deliberately
+    leaves the hostile summaries OUT of its ``methods{}`` block — each group installs
+    its own summaries at prover time via :func:`append_summaries`. Without this note
+    the judge sees hostile functions used-but-not-summarized and false-flags them as
+    unsound/HAVOCing. The note makes each group's install concrete: its properties,
+    rules, and exactly which functions it summarizes (with the summary text) — so the
+    judge evaluates the spec as it is actually verified, not as a monolith. A function
+    a group does NOT list is verified as the base spec has it there — precise unless the
+    base spec itself summarizes it."""
+    if not specs:
+        return None
+    lines: list[str] = [
+        "// ============================================================================",
+        "// Verification-group plan (informational — NOT part of the base spec above)",
+        "// ============================================================================",
+        "// This spec is NOT verified as a monolith. It is split into parallel prover",
+        "// runs ('verification groups'), each with its OWN methods{} block installing the",
+        "// summaries listed below. A hostile function that appears un-summarized in the base",
+        "// spec above IS summarized in every group that lists it here — treat those as",
+        "// installed (not HAVOCing) when judging soundness and coverage; a function a group",
+        "// does not list is verified as the base spec above has it (precise unless the base",
+        "// spec above already summarizes it). A summary a group DOES list for a function the base",
+        "// spec above already summarizes is a more-specific override (exact beats wildcard), so that",
+        "// group verifies under the group's entry, not the base's.",
+        "//",
+    ]
+    for s in specs:
+        props = [str(m.property_title) for m in s.property_rules]
+        rules = [str(r) for m in s.property_rules for r in m.rules]
+        lines.append(f"// Group \"{s.name}\":")
+        lines.append(f"//   properties: {', '.join(props) if props else '(none)'}")
+        lines.append(f"//   rules: {', '.join(rules) if rules else '(none)'}")
+        if s.summaries:
+            lines.append("//   installs summaries:")
+            for func in sorted(s.summaries):
+                lines.append(f"//     {func}: {s.summaries[func].strip()}")
+        else:
+            lines.append("//   installs summaries: (none — all functions precise)")
+        # No per-group conf is shown (the agent-facing group carries none). If groups gain
+        # agent-set conf and the judge starts reviewing .conf files, list each group's conf diff here.
+        lines.append("//")
+    return "\n".join(lines)

composer/spec/source/author.py

@@ -26,6 +26,8 @@
     GeneratedCVL, PropertyRuleMapping, AppliedEdit, FeedbackToolBase,
 )
 from composer.prover.core import run_prover, CexHandler, ProverCallbacks, ProverReport
+from composer.spec.source.agent_groups import VerificationGroupSpec, over_cap_message, render_group_plan_for_judge
+from composer.spec.source.verification_groups import resolved_max_groups
 from composer.spec.source.live_explorer import VersionedHistory, LiveEditTools, WIPE_HISTORY
 from composer.spec.source.prover import setup_prover_config_in
 from composer.spec.context import WorkflowContext, CVLGeneration, CacheKey, SourceCode
@@ -170,6 +172,91 @@ async def run(self) -> Command | str:
         )
 
 
+@tool_display(lambda p: f"Declaring {len(p['groups'])} verification group(s)", None)
+class DeclareVerificationGroups(
+    WithAsyncDependencies[Command | str, list[PropertyTitle]],
+    WithInjectedState[SourceCVLGenerationState],
+    WithInjectedId,
+):
+    """
+    Split verification into independent, PARALLEL prover runs ("verification groups").
+
+    Use this when one combined run is (or would be) intractable — typically a timeout from
+    having to keep too much of the code precise at once. Each group verifies a subset of the
+    properties under its OWN summarization and configuration, so different groups can keep
+    DIFFERENT functions precise: a function summarized in one group can stay exact in another.
+    This breaks the "one global methods block forces the intersection of every rule's precision
+    needs" bottleneck.
+
+    A valid declaration:
+    - Every non-skipped property appears in exactly ONE group (via that group's `property_rules`).
+      Coverage is checked exactly as at publish time.
+    - Each group's `summaries` maps each function IT summarizes to the CVL methods-block entry to
+      summarize it with, HERE. A function a group omits is verified as the base spec has it — precise only
+      if the base spec (incl. its imports) does not already summarize it. The same
+      function may be summarized differently in different groups (a rule may allow `foo` monotone
+      while another needs it injective) — choose, per group, the weakest summary sound for that
+      group's rules.
+    - The base spec you put on the VFS must define any ghosts/CVL functions those entries use, and
+      must itself leave the summarized functions UNsummarized (each group's spec adds its own).
+    - Your `summaries` are APPENDED to the base spec's methods block (autosetup's imported summaries
+      included). To change how an ALREADY-base-summarized function behaves in a group, your entry must
+      be MORE SPECIFIC than the base's — an exact `Contract.f(...)` overrides a wildcard `_.f(...)`. If
+      the base already summarizes it EXACTLY for that contract you cannot override or remove it (a second
+      exact entry is a duplicate → typecheck error), and there is no way to make it precise in one group;
+      the workaround is to summarize a CALLER of that function instead (usually not base-summarized).
+
+    Note: a rule reachable from two properties in DIFFERENT groups is verified ONCE — in the FIRST
+    group that declares it — under THAT group's summaries (the run partitions rules disjointly). So
+    make the first group's summaries sound for any rule it shares with a later group, or keep that
+    rule's functions precise there.
+
+    Groups run in parallel; already-verified rules are not re-run. Call again to REPLACE the whole
+    partition; pass an empty `groups` list to revert to a single combined run. There is a cap on the
+    number of groups (each is a separate prover run); declaring more is REJECTED with the merge the run
+    would otherwise force, so you refactor the partition yourself rather than have it silently merged.
+    """
+    groups: list[VerificationGroupSpec] = Field(
+        description="The verification groups to split into. Empty list reverts to one combined run."
+    )
+
+    @override
+    async def run(self) -> Command | str:
+        specs = self.groups
+        if not specs:
+            return tool_state_update(
+                self.tool_call_id,
+                "Reverted to a single combined verification run.",
+                verification_groups=[],
+            )
+        names = [s.name for s in specs]
+        if len(set(names)) != len(names):
+            return "Group names must be unique."
+        # Coverage: the union of the groups' property->rule mappings must cover every
+        # non-skipped property — the same check applied at publish.
+        combined = [m for s in specs for m in s.property_rules]
+        with self.tool_deps() as titles:
+            if (err := validate_property_rules(combined, self.state["skipped"], titles)) is not None:
+                return err
+        # Partition: a property must not be claimed by more than one group.
+        seen: set[str] = set()
+        dup: set[str] = set()
+        for s in specs:
+            for m in s.property_rules:
+                (dup if m.property_title in seen else seen).add(m.property_title)
+        if dup:
+            return f"Each property must belong to exactly one group; these appear in more than one: {sorted(dup)}"
+        # Reject an over-cap declaration; over_cap_message suggests a valid merge to adopt.
+        if (over := over_cap_message(specs, resolved_max_groups())) is not None:
+            return over
+        return tool_state_update(
+            self.tool_call_id,
+            f"Declared {len(specs)} verification group(s): {', '.join(names)}. "
+            "Subsequent verify_spec runs split the rules across them and run in parallel.",
+            verification_groups=specs,
+        )
+
+
 _GIVE_UP_DESCRIPTION = """
     Call this tool to give up on the CVL generation for this task.
 
@@ -619,7 +706,13 @@ async def _get_feedback(
                 vfs=self.state["vfs"],
                 version_history=self.state["version_history"],
             )
-            return await judge(snap, spec, skipped, self.rebuttals, self.tool_call_id)
+            # The judge reviews the base spec, whose methods{} block deliberately omits
+            # the hostile summaries — each verification group installs its own at prover
+            # time (append_summaries). Surface that plan so the judge does not false-flag
+            # those functions as un-summarized / HAVOCing.
+            plan = render_group_plan_for_judge(self.state.get("verification_groups") or [])
+            judged_spec = spec if plan is None else f"{spec.rstrip()}\n\n{plan}\n"
+            return await judge(snap, judged_spec, skipped, self.rebuttals, self.tool_call_id)
 
     @override
     def _version_history(self) -> Sequence[str]:
@@ -864,6 +957,7 @@ async def propose(
         [prover_tool.lg_tool,
          ExpectRulePassage.as_tool("expect_rule_passage"),
          ExpectRuleFailure.as_tool("expect_rule_failure"),
+         DeclareVerificationGroups.bind(titles).as_tool("declare_verification_groups"),
          give_up_tool(name="give_up", description=_GIVE_UP_DESCRIPTION, label="CVL generation"),
          PublishResultTool.bind(titles).as_tool("result"),
          ctx.get_memory_tool()]