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

[jar-ben]

Summary

Adds verification groups: an authoring agent can split a spec's properties into independent,
PARALLEL prover runs, each verifying its own subset of rules under its OWN summarization. Different
groups can keep DIFFERENT functions precise — a function summarized in one group can stay exact in
another.

This breaks the core scaling bottleneck: a spec has ONE global methods{} block, so a monolithic run
verifies every rule under the intersection of what all rules need precise. One property that needs a
function exact forces EVERY rule to pay that cost, and re-running the same spec never escapes it. Groups
let each rule run under only the summarization it actually needs.

With no declaration (or a single group), this is a behavior-preserving pass-through of today's
one-spec/one-run model.

Why

Timeouts on hard specs are usually a precision problem, not a prover problem: one expensive property
drags the whole spec down because summarization is global. Verification groups make the precision
boundary per-rule, so the agent can summarize aggressively where a property allows it and stay exact
only where a property needs it — turning a monolithic timeout into several tractable runs.

How it works

Three layers, cleanly separated:

1. Substrate (verification_groups.py, policy-neutral) — the VerificationGroup model
   (owned rules + per-group spec/conf/summaries), the group-count cap and its env override, the
   cap-driven greedy merge (cap_groups, cheapest = the pair agreeing on the most summaries), result
   recombination (merge_group_results, owned-rules-only), and prune_phantom_owned_rules.
2. Policy (agent_groups.py) — the transparent, agent-declared partition. DeclareVerificationGroups
   lets the agent name groups over PROPERTIES, each with its property_rules and its summaries (per
   function). Coverage is validated exactly as at publish (every non-skipped property in exactly one
   group); rules are made a disjoint partition by first-declaration-wins. (The substrate group also
   carries a per-group conf overlay, but the agent-facing tool does not expose it in this PR — a
   per-group prover-config knob is new agent power, unvalidated, and unreviewed by the judge, so it is
   deferred to a follow-up with guardrails; see below.)
3. Execution (prover.py) — run_grouped runs the groups concurrently (asyncio.gather), each
   writing its spec/conf under a group-distinct stem so parallel writes don't collide, submitting only
   its pending (not-yet-verified) owned rules, then recombining verdicts. Completion is the AND of
   per-group completeness, evaluated from history on a VERIFIED basis and filtered per group+digest so
   groups don't truncate each other's streaks. The post-run bookkeeping (stuck-rule nagging, the
   completion stamp, the state update) is shared with the single-run path via _finalize_run.

The feedback judge is given a verification-group plan note so it evaluates the spec as it is
actually verified (each group's installed summaries) rather than as a monolith — otherwise it
false-flags a function that's used-but-not-summarized in the base spec as HAVOCing.

Soundness

• Merging only removes summarization. merge_summaries keeps a function only where two groups
  summarize it identically; any disagreement drops it to precise. Dropping a summary only adds precision,
  so a merge is always sound — this underpins the merge over_cap_message suggests for an over-cap
  declaration (the sole place a merge is computed; the cap is otherwise enforced by rejection, not by
  auto-merging). It assumes no summary-strength ordering (summaries aren't generally comparable —
  "monotone" and "injective" are incomparable).
• Owned-rules-only verdicts. A group is run with the prover's rule selector limited to its rules,
  but the prover's status map still reports some it doesn't own — always-run built-in checks (e.g.
  envfreeFuncsStaticCheck), parametric instantiations, and any rule shared with another group. Only the
  owned rules' verdicts are kept, so those extras — and a verdict computed under the wrong group's
  precision — can't leak.
• Completion from VERIFIED history, not the merged map — so a rule with no verdict stays pending,
  never falsely "done."
• Phantom-rule liveness. An owned rule the compiled spec never instantiates (an agent typo, or a
  property_rules entry naming a non-existent rule) is pruned and warned about, rather than sitting
  forever pending and wedging its group in a silent perpetual re-run.
• A rule shared across properties in different groups is verified under the FIRST group's summaries
  (documented in DeclareVerificationGroups so authors keep that group's summaries sound for it).

Config

DEFAULT_MAX_VERIFICATION_GROUPS = 6, overridable per run via AUTOPROVER_MAX_VERIFICATION_GROUPS
(mirroring the other AUTOPROVER_* prover-config knobs). The cap is enforced by a single mechanism:
declare_verification_groups rejects an over-cap declaration with guidance, suggesting one concrete valid
merge (cap_groups) the agent can adopt or improve, so the agent refactors the split itself. The run-time
builder then only asserts the bound (never silently merges).

Scope

Standalone and detector-independent: the grouping guidance in the property-generation prompt is
phrased generically (split preemptively when a single run would time out / properties have conflicting
precision needs), not tied to any static-analysis signal.

Limitations

• A group cannot override or remove a base-spec EXACT summary. A group's summaries are appended to
  the base spec's methods{} block, which includes autosetup's imported summaries, and CVL has no
  "un-summarize." Overlapping entries resolve by specificity (exact > wildcard), so a group can strengthen
  a base WILDCARD summary with a more-specific exact entry (Contract.f beats _.f). But if the base
  already summarizes a function EXACTLY for a contract, a second exact entry is a duplicate (typecheck
  error), and the agent cannot prune the base either — the authoring VFS forbids writing .spec files
  (live_explorer.py: "specs are the author's domain"), and autosetup's summaries arrive via an
  all-or-nothing import aggregator. So a function autosetup summarized exactly (e.g. its per-method
  => NONDET fallbacks) cannot be made stricter or precise in any group — which is precisely where
  grouping would otherwise add value. The agent's only workaround is to summarize a CALLER of the function
  (usually not base-summarized). A proper fix is deferred (see follow-ups).

Testing

Full unit coverage of the pure pieces — the group cap, the merge-to-precise, coverage validation,
first-declaration-wins partition, per-group pending/completion (including history interleaving and
digest isolation), result recombination, and phantom-rule pruning (test_verification_groups.py,
test_agent_groups.py, test_group_completion.py). pyright-clean.

Known follow-ups (deliberately out of scope here)

• Expose per-group conf to the agent, with guardrails. The substrate group already carries a
  conf_overlay (and run_grouped applies it), but DeclareVerificationGroups does NOT expose it
  here. Per-group prover config (loop_iter, global_timeout, prover_args, links) is new agent
  capability the author never had, it is applied unvalidated (only the forced OVERLAY_OWNED_KEYS
  win), and the judge does not see the .conf — so a group weakening loop_iter or adding an unsound
  prover_arg would go unchecked. A follow-up should whitelist safe keys (e.g. global_timeout;
  loop_iter only when raised above the base) and/or surface the conf diff to the judge.

• Per-group base-summary exclusion (unblocks the Limitation above). Let a group drop a base summary
  it wants to strengthen/make-precise: the grouping layer, which already assembles each group's spec, would
  emit a filtered copy of the summary specs for that group (omitting the chosen entries) and import those
  instead of the shared aggregator. Keeps the agent out of .spec files while removing the exact-collision
  wall. Pairs well with detecting the base-vs-group summary collision before submit (today the agent finds
  it as a typecheck error and iterates).

• Async glue test for run_grouped. The pure decision pieces are covered; the orchestration glue
  (the asyncio.gather fan-out, the hard-error abort, merge_group_results over executed groups) is
  not, because run_grouped is a nested closure. A follow-up would extract it to a testable function
  and add an async test with a stubbed prover.