Put a curated summary's companion contracts in the scene

[shellygr]

OZ_BitMaps.spec summarizes BitMaps by rerouting its calls to a companion library of its own, OZ_BitMaps. CVL can only name a contract that is in the scene, and the scene is the files the conf lists. copy_summaries_folder copies the companion beside the spec and stops there, so nothing ever puts it in a conf.

The result is that any project whose methods match the bitmaps entry fails its warmup typecheck:

Found errors in certora/specs/summaries/OpenZeppelin/OZ_BitMaps.spec:
Error in spec file (OZ_BitMaps.spec:6:9): Variable `OZ_BitMaps` has not been declared.
...
RuntimeError: Cache warmup failed - stopping orchestration

bitmaps is the only entry in function_summaries.json that declares additional_contracts, and it has not changed since the package was imported from the AutoSetup repo, so I believe this has never worked. I hit it on a dev run whose main contract calls BitMaps.get/set/unset/setTo.

The base conf now carries an entry per top-level definition in each matched entry's additional_contracts. Per definition, not per file: a conf entry naming only the file puts just the stem-named contract in scene.

Two things worth a reviewer's attention:

• curated_scene_contracts lives in summary_resolver.py rather than next to its caller in setup_summaries.py, because that module calls sys.exit(1) at import time when there is no ANTHROPIC_API_KEY or .env, so a unit test cannot import it at all.
• A companion that was matched but not copied logs a warning and is skipped, matching what copy_summaries_folder already does for a missing bundled file. Happy to make it fatal instead.

Tests in Certora/Autosetup#TBD (six cases: the conf entry, multiple definitions per file, a summary with no companion, nothing matched, an unknown key, and the uncopied-companion warning).

🤖 Generated with Claude Code

---

Folded in (was #219): make the reroute actually attach.

Putting the companion in the scene was necessary but not sufficient. Two more things stopped OZ_BitMaps from doing anything:

• Parameter matching compares canonicalId, which is "<file resolved under .certora_sources>|<qualified name>". A bundled companion declares its own copy of BitMaps.BitMap, and that is a different type from the project's however identical it looks. The companion is now generated per project from a template, importing the project's own copy of the library.
• The bodies were require(false) tripwires. A body that always reverts leaves the summary nothing to attach to, so every call through it reverts and every rule over it passes vacuously. That reads as a green run. The bodies are neutral now.

Two smaller ones, both fixed here: the host functions have to be external, since DetectRerouteSummaries only sees external library functions, and the summary entries have to survive the prune pass, which drops entries naming a contract that is not in the scene index. That index comes from the project's own compilation, which happens before the companion exists.

Checked on a small project that uses BitMaps: every rule verifies under rule_sanity basic, and one of them is a bare satisfy, so a vacuous pass fails instead of looking like success. Tests are in the Autosetup PR.

[shellygr]

Tests are in Certora/Autosetup#148.