Cancel the rest of a concurrent group when one member fails

[shellygr]

What

run_pipeline_inner started the pre-formalization work with a bare asyncio.create_task and did
not await it until after the whole property-extraction fan-out had finished. A fatal error inside
it was stored on the task object and sat there unobserved for as long as extraction took. In one
run that was 41 minutes and four bug-analysis agents' worth of spend on a run that could no longer
produce anything, and none of it was kept: extraction batches are only persisted downstream of the
await.

prepare_formalization's own asyncio.gather had the other half of the problem. Without
return_exceptions, gather propagates the first child's exception to its awaiter immediately and
does not cancel the remaining children. It only cancels them when the gathering future itself is
cancelled. So the sibling detached and ran to completion too. Fixing one level leaves the other,
which is why both are here.

The driver already had the right shape one step earlier. The preflight and the system analysis
share a task group, and the comment there states the policy: neither side outlives the other's
failure. This applies that policy at the concurrency points that were missing it.

How

gated_group() in composer/io/multi_job.py yields an asyncio.TaskGroup and unwraps the
resulting BaseExceptionGroup, so the caller sees the failure itself when only one member really
failed and keeps the group when two fail at once. It sits beside maybe_semaphore, and both edit
sites already import from that module, so there are no new import edges.

Five call sites use it: the preflight and analysis overlap, whose now-duplicated inline unwrap is
deleted rather than left beside the helper; the pre-formalization and extraction overlap; the
per-unit extraction fan-out; the plugin pre-inference fan-out; and the AutoSetup and invariants
pair. Task objects are held rather than completion order, so callers that depend on result order
still get it.

The unwrap re-raises outside the except block. raise exc from None would clear __cause__ and
suppress __context__, which matters for a wrapper whose message only points at the exception it
wraps.

task_logger gains a CancelledError branch, so a cancelled task's tokens are folded into the
per-phase breakdown instead of being left in the in-flight map. Cancellations appear in the
per-row status but are excluded from the failure roll-up, so one real failure in an N-unit fan-out
does not print as N failures.

Deliberately unchanged

The per-component asyncio.gather(..., return_exceptions=True) stays as it is. Per-component
failure isolation is the opposite policy on purpose.

The four bare fatal gathers in the natspec driver are the same class in a different pipeline, and
are left for a follow-up.

Known gap

A cancelled task does not fire its handler's on_error, because run_task catches Exception and
CancelledError is not one, so its row stays at RUNNING until the process exits. This predates the
change, since the first overlap already cancelled, but gating the extraction fan-out turns it from
a one-row artefact into a many-row one. Widening the handler touches three UI factories, so it is
out of scope here.

Testing

Four new test modules. tests/test_gated_group.py covers the primitive: a failure cancels a 30s
sibling and surfaces itself, a double failure keeps the group, cancelling the holder cancels the
members, and a member raised with from keeps its cause through the unwrap.
tests/test_extraction_fanout_gate.py drives the real _extract_all with only the LLM call
stubbed, covering both fan-outs inside it. tests/test_prover_prepare_formalization_gate.py covers
the AutoSetup and invariants pair in both directions. tests/test_cancelled_task_accounting.py
covers the new accounting branch and the roll-up.

tests/test_pipeline_overlap.py's module docstring and its two second-pair tests described the old
behaviour as intended, so they are rewritten to state the policy, with a non-zero delay on the
surviving side so they assert cancellation rather than winning a race. A third test covers
caller-side cancellation reaching the second pair. Those three tests waited a fixed interval before
cancelling and were flaky under parallel load; they now wait on an event the stub sets when it
starts.

Each new test was checked by putting asyncio.gather back in place of the gate and confirming it
fails.

Targeted run: 35 passed. pyright composer/ analyzer sanity_analyzer certora_autosetup: 0 errors.