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.

[shellygr]

Codex review:

1. [P2] Companion can import the wrong BitMaps library. _project_library_file (worktrees/AutoProver/curated-summary-scene/certora_autosetup/setup/setup_summaries.py:830) selects the
   first matching library anywhere on disk. With multiple vendored OpenZeppelin copies, that can differ from the compiled contract’s dependency, recreating the canonical-type
   mismatch this PR fixes. Resolve the source from compilation metadata.

2. [P2] Companions discovered during call resolution never enter the config. Companion injection (worktrees/AutoProver/curated-summary-scene/certora_autosetup/autosetup/
   autosetup.py:844) happens before call resolution. If a newly linked contract introduces BitMaps, _on_contracts_added generates and imports its summary but only adds the original
   library to files. The next typecheck encounters an undeclared OZ_BitMaps. Update the config after each summary batch.

3. [P2] Failed companion generation leaves its summary enabled. This continue (worktrees/AutoProver/curated-summary-scene/certora_autosetup/setup/setup_summaries.py:797) skips
   generating the companion, but retains bitmaps in matched_functions and imports its reroute spec. A library excluded from discovery, or without a pragma, therefore produces a
   broken summary instead of the documented fallback. Drop the dependent summary or fail explicitly.

[shellygr]

Claude answers:

1. Done. The library file now comes from all_methods.json, which records the originalFile the compiler read for each method, filtered to the compilation units in the scene, with the main contract's unit breaking a tie between two copies. find_libraries_used_by picked its file from the same kind of filesystem search and had the same hole, so it resolves the same way now and build_library_name_index is gone.

2. Done. _on_contracts_added adds the companions to the conf after each summary batch. add_files_to_config dedupes and fills the compiler maps, so re-adding on every batch costs nothing.

3. Done, dropped rather than fatal. copy_summaries_folder generates the companions before it copies anything and returns the keys that failed; the caller takes them out of matched_functions and the aggregator, and their spec is never copied. An unresolvable library, an ambiguous one, or one with no pragma now leaves the library unsummarized, which is the documented fallback.

Tests are on the matching branch of the tests repo: which copy wins, the drop all the way through to the aggregator, and the conf entry after a late batch. The BitMaps e2e passes locally against a project whose tree carries a second copy of the library.