Treat an unimplemented contract as a terminal compilation failure

[shellygr]

Problem

When a contract in the compilation input inherits functions it never implements, solc rejects it outright (Contract "X" should be marked as abstract.). Nothing in the conf can change that — it is a defect in the contract's source.

The retry loop cannot tell, so it treats the failure like any other: the specific detectors miss, the use_relpaths_for_solc_json catch-all fires, and the run spends further certoraRun passes plus the import-patch pass before reporting a generic "compilation analysis failed" that names neither the contract nor the reason. In a dev run this cost four compilations and the import patch, all reaching the identical error, and the log's only actionable content was the raw solc output buried in a warning dump.

The contracts most exposed to this are the generated harnesses: they are written against their target's own file, so a function the target inherits from an interface and leaves to a sibling mixin is invisible at the point the harness is written.

Change

Detect the diagnostic in the retry loop, immediately after the existing _detect_abstract_main_contract check, and raise UnimplementedContractError naming the contract and the file that declares it. Like that check it runs before any workaround is applied, so the loop stops at the compilation that reported the error rather than after exhausting the catch-all.

Detection normalizes whitespace first (_normalize_ws), as the other multi-line detectors in this module do — solc hard-wraps its diagnostics, and the wrap can fall inside this sentence. The contract name is quoted by solc so it survives the fold; the source location that follows is optional, since only the diagnostic itself is guaranteed to be present.

Consistent with AbstractMainContractError, the raise unwinds to run_compilation_analysis's handler, which logs the message and fails the phase.

Validation

• uv run --no-sync python -m pytest tests/ -m "not expensive" -q → 507 passed; pyright → 0 errors
• new tests: detection with and without a source location, a negative case, and a loop-level test asserting exactly one certoraRun before the raise
• ran the detector over the verbatim output of the real run that motivated this: it returns the contract and its file

Note on approach

The detector is a regex over compiler text, which is the established mechanism in this module (every existing detector works that way) — the structured --json diagnostics are not available on this path, since what is being parsed is certoraRun's output rather than solc's.

Possible extension

The message currently reaches the log but not the run's user-facing failure, which stays the generic "Compilation analysis failed" — same as for AbstractMainContractError today. Propagating either one as the reported reason is a separate change.

Companions

Two independent PRs address the same failure earlier in the pipeline: a compile gate on generated harnesses, and prompt guidance against extending a non-deployable contract.

Companion PRs: #129 #130. They are independent — any order, any subset.