Generate the BitMaps summary's reroute host from the project's own library

certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_BitMaps.spec

@@ -1,5 +1,13 @@
-// SG: We cannot use BitMaps.BitMap as a key in a ghost mapping.
-// Solution: reroute to OZ_BitMaps.sol, add it to scene, and summarize its methods.
+// BitMaps.BitMap cannot be a ghost mapping key, so the library's calls are rerouted to
+// OZ_BitMaps (added to the scene alongside this spec) and the ghost is keyed on the storage
+// slot instead. The reroute host is generated per project from OZ_BitMaps.template.sol,
+// because its parameter type has to come from the project's own BitMaps.sol.
+//
+// The model replaces the BitMap's storage with a ghost and nothing ties the two together:
+// reading bitmap._data directly, deleting the struct, a raw sstore, or copying the struct all
+// diverge from it silently. The slot key is also only as sound as distinct BitMaps having
+// distinct slots — true for a plain field, but a BitMap reached through a mapping has a
+// hashed pointer, so a collision would alias two of them.
 methods {
     // rerouting
     function BitMaps.get(BitMaps.BitMap storage bitmap, uint256 index) internal returns bool => 
@@ -16,16 +24,16 @@ methods {
 
     // actual summaries
     function OZ_BitMaps.get(uint256 bitmap, uint256 index) internal returns bool => 
-        ghost_bitmap_get[currentContract][bitmap][index];
+        ghost_bitmap_get[calledContract][bitmap][index];
 
     function OZ_BitMaps.set(uint256 bitmap, uint256 index) internal => 
-        ghost_bitmap_set(currentContract, bitmap, index);
+        ghost_bitmap_set(calledContract, bitmap, index);
 
     function OZ_BitMaps.unset(uint256 bitmap, uint256 index) internal => 
-        ghost_bitmap_unset(currentContract, bitmap, index);
+        ghost_bitmap_unset(calledContract, bitmap, index);
 
     function OZ_BitMaps.setTo(uint256 bitmap, uint256 index, bool value) internal => 
-        ghost_bitmap_setTo(currentContract, bitmap, index, value);
+        ghost_bitmap_setTo(calledContract, bitmap, index, value);
 }
 
 // Ghost variable to track bitmap state per contract and index

certora_autosetup/certora/specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.template.sol

@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: MIT
+$PRAGMA$
+
+// BitMaps.BitMap cannot be a ghost mapping key, so OZ_BitMaps.spec reroutes the library's
+// calls here and summarizes these functions instead, keying the ghost on the storage slot.
+//
+// The import is what makes the reroute resolve. A reroute host's parameter must carry the
+// same canonicalId as the summarized function's, and canonicalId is
+// "<file resolved under .certora_sources>|<qualified name>" — so BitMaps.BitMap has to come
+// from the very BitMaps.sol the project compiles. A copy of the struct is a different type,
+// however identical it looks. That path differs per project, which is why this is a template.
+import {BitMaps} from "$BITMAPS_IMPORT$";
+
+library OZ_BitMaps {
+    // Reroute targets, and external for a reason: the Prover keeps a candidate only when its
+    // evmExternalMethodInfo reports a library function, and that is populated for EXTERNAL
+    // visibility alone. External is also the only place a storage parameter can be bound.
+    function get(BitMaps.BitMap storage bitmap, uint256 index) external view returns (bool) {
+        return get(slotOf(bitmap), index);
+    }
+
+    function set(BitMaps.BitMap storage bitmap, uint256 index) external {
+        set(slotOf(bitmap), index);
+    }
+
+    function unset(BitMaps.BitMap storage bitmap, uint256 index) external {
+        unset(slotOf(bitmap), index);
+    }
+
+    function setTo(BitMaps.BitMap storage bitmap, uint256 index, bool value) external {
+        setTo(slotOf(bitmap), index, value);
+    }
+
+    // The summarized functions. CVL replaces each body with a ghost read or write, so what is
+    // written here only runs if a summary failed to attach.
+    //
+    // These were `require(false)` tripwires, meant to make that failure loud. They made it
+    // certain instead: a body that unconditionally reverts leaves nothing for the summary to
+    // attach to, so every call reverted and every rule over it passed vacuously. The tripwire
+    // caused the failure it was meant to announce.
+    //
+    // Neutral bodies invert that. An unattached summary now means `set` stores nothing and
+    // `get` reads false, so a rule that sets a bit and reads it back fails outright. A
+    // violated rule is a far better failure than a green vacuous one, and `rule_sanity`
+    // catches what is left.
+    function get(uint256 bitmap, uint256 index) internal view returns (bool) {
+        return false;
+    }
+
+    function set(uint256 bitmap, uint256 index) internal {}
+
+    function unset(uint256 bitmap, uint256 index) internal {}
+
+    function setTo(uint256 bitmap, uint256 index, bool value) internal {}
+
+    // The ghost is keyed on the slot, which is what stands in for the BitMap identity.
+    function slotOf(BitMaps.BitMap storage bitmap) internal pure returns (uint256 ret) {
+        assembly { ret := bitmap.slot }
+    }
+}

certora_autosetup/setup/function_summaries.json

@@ -105,7 +105,7 @@
     "library_names": ["BitMaps"],
     "summary_file": "specs/summaries/OpenZeppelin/OZ_BitMaps.spec",
     "description": "OpenZeppelin BitMaps operations",
-    "additional_contracts": ["specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.sol"]
+    "additional_contracts": ["specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.template.sol"]
   },
   "oz_arrays_unsafeMemoryAccess": {
     "names": ["unsafeMemoryAccess"],

certora_autosetup/setup/setup_summaries.py

@@ -52,12 +52,14 @@
     is_local_backend,
 )
 
-from certora_autosetup.setup.solidity_utils import DEPENDENCIES, find_all_library_files as util_find_all_library_files
+from certora_autosetup.setup.solidity_utils import DEPENDENCIES, find_all_library_files_and_names
+from certora_autosetup.setup.solidity_utils import find_all_library_files as util_find_all_library_files
 from certora_autosetup.setup.solidity_utils import find_all_solidity_files as util_find_all_solidity_files
 from certora_autosetup.setup.solidity_utils import walk_files_by_suffix
 
 # Import method parser
 from certora_autosetup.parsers.method_parser import MethodParser
+from certora_autosetup.utils.solc_version_resolver import read_pragma_from_source_file
 from certora_autosetup.parsers.spec_imports import parse_imports_from_spec
 from certora_autosetup.setup.summary_resolver import curated_scene_contracts, resolve_summary_specs
 from certora_autosetup.setup.signature_types import InheritanceGraph
@@ -775,7 +777,7 @@ def copy_summaries_folder(self, matched_function_keys: Iterable[str]) -> Path:
 
         copied = 0
         for rel in sorted(closure):
-            # Templates are read from the package source by _materialize_template;
+            # Spec templates are read from the package source by _materialize_template;
             # never copy them to the user's dir.
             if str(rel).endswith(".template.spec"):
                 continue
@@ -785,12 +787,97 @@ def copy_summaries_folder(self, matched_function_keys: Iterable[str]) -> Path:
                 self.log(f"Bundled summary file missing: {src}", "WARNING")
                 continue
             dst.parent.mkdir(parents=True, exist_ok=True)
-            shutil.copyfile(src, dst)
+            if str(rel).endswith(".template.sol"):
+                # A companion contract the summary reroutes through cannot be shipped ready to
+                # use: its parameter types have to come from the project's own copy of the
+                # library, so the import is filled in here.
+                if not self._materialize_companion(rel, src, self._untemplated(dst)):
+                    continue
+            else:
+                shutil.copyfile(src, dst)
             copied += 1
 
         self.log(f"Copied {copied} curated summary file(s) to {target_summaries}")
         return target_summaries
 
+    @staticmethod
+    def _untemplated(path: Path) -> Path:
+        """``X.template.sol`` -> ``X.sol``; anything else unchanged.
+
+        Deliberately not ``_versioned_template_relpath``: that one is ``.spec``-shaped and
+        appends the main contract's name, while a companion's content depends only on the
+        project, so two main contracts in one project share a single companion.
+        """
+        name = path.name
+        return path.with_name(name.replace(".template.", ".", 1)) if ".template." in name else path
+
+    def _library_for_companion(self, rel: Path) -> Optional[str]:
+        """The library name a companion template belongs to, from the registry.
+
+        Read from the entry that declares the companion rather than parsed out of its
+        filename, so the two cannot drift apart.
+        """
+        wanted = (SUMMARIES_SUBDIR / rel).as_posix()
+        for info in self.function_summaries.values():
+            if wanted in info.get("additional_contracts", []):
+                names = info.get("library_names") or []
+                return names[0] if names else None
+        return None
+
+    def _project_library_file(self, library_name: str) -> Optional[Path]:
+        """The project's own file declaring ``library <library_name>``."""
+        found = find_all_library_files_and_names(
+            include_test_files=False, include_dependencies=True, log_func=self.log
+        )
+        for file_path, names in found.items():
+            if library_name in names:
+                return Path(file_path)
+        return None
+
+    def _materialize_companion(self, rel: Path, template: Path, destination: Path) -> bool:
+        """Fill a companion template in from the project and write it. False if we cannot.
+
+        Returns False rather than raising so the caller can drop the key: a summary whose
+        companion never materialized is worse than no summary, because the reroute would send
+        the library's calls to a contract that is not in the scene.
+        """
+        library_name = self._library_for_companion(rel)
+        if library_name is None:
+            self.log(f"No registry entry claims companion {rel}", "WARNING")
+            return False
+
+        library_file = self._project_library_file(library_name)
+        if library_file is None:
+            self.log(
+                f"Cannot generate {destination.name}: the project has no library "
+                f"{library_name} to take its types from",
+                "WARNING",
+            )
+            return False
+
+        # The library's own spec, so the companion can never fall outside the range the
+        # library itself compiles under.
+        pragma_spec = read_pragma_from_source_file(library_file, Path.cwd())
+        if not pragma_spec:
+            self.log(
+                f"Cannot generate {destination.name}: {library_file} declares no pragma",
+                "WARNING",
+            )
+            return False
+
+        # Relative, because the emitted file sits under certora/ while the library can be
+        # anywhere; an absolute path would also bake the build machine's layout into a source
+        # file that gets uploaded with the run.
+        import_path = os.path.relpath(library_file.resolve(), destination.parent.resolve())
+        content = (
+            template.read_text()
+            .replace("$PRAGMA$", f"pragma solidity {pragma_spec};")
+            .replace("$BITMAPS_IMPORT$", import_path)
+        )
+        destination.write_text(content)
+        self.log(f"Generated {destination.name} against {library_file}")
+        return True
+
     def process_template_in_place(
         self,
         template_file: Path,
@@ -1022,7 +1109,13 @@ def _add(p: Path) -> None:
         # Then any other emitted spec (LLM per-contract, call resolution) — lower dedup precedence.
         for spec in walk_files_by_suffix(self.user_summaries_dir, ".spec"):
             _add(spec)
-        resolve_summary_specs(ordered_specs, PATH_ALL_METHODS_JSON, log=self.log)
+        # The companions are in the conf but not in the index, which is built from the
+        # project's own compilation; without this their summaries would be pruned as out of
+        # scene and the reroute would land on the companion's unsummarized bodies.
+        companions = {entry.split(":")[-1] for entry in self.curated_scene_contracts()}
+        resolve_summary_specs(
+            ordered_specs, PATH_ALL_METHODS_JSON, exempt_receivers=companions, log=self.log
+        )
 
     def should_process_file(self, file_path: str) -> bool:
         """Check if a file should be processed (not a dependency or internal file).