Generate the BitMaps summary's reroute host from the project's own library - #219
Merged
shellygr merged 5 commits intoSep 6, 2026
Merged
Conversation
The bundled OZ_BitMaps companion could never work. A reroute target must be an external library function, and every function in it was internal; and even made external, it declared its own copy of `struct BitMap`, which is a different type from the project's however identical it looks — parameter matching compares canonicalId, which names the file the type came from. So the companion is now a template, filled in per project with the project's own BitMaps.sol as the import and that library's pragma. Verified by hand first: with the companion internal the typechecker gives exactly the production error, and with it external and importing the project's own library it exits clean. Two adjacent gaps this uncovered, both general rather than BitMaps-specific: a file added to `files` needs its compiler_map entry or certoraRun rejects the conf as unmatched, and a companion shipped as a template is emitted under its untemplated name, which is the name the scene has to look for. The spec's ghosts now key on calledContract rather than currentContract, which is bound to the primary contract and so let two contracts holding a BitMap at the same slot alias each other's bits. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Every other entry in a conf is relative to the project root, and an absolute one bakes the build machine's layout into a file that travels with the run. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The prune pass drops an internal-method entry whose receiver is absent from the scene index, and that index is built from the project's own compilation — which happens before a curated companion joins the conf. So every OZ_BitMaps entry was commented out as "not in scene", leaving the reroute pointing at a companion whose bodies revert on every call: a green run that proved nothing, which is worse than the loud failure it replaced. The exemption is per receiver and covers only contracts that are genuinely in the conf and cannot be in an index that predates them. A receiver that is absent for the ordinary reason is still dropped. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The four `require(false)` bodies were a tripwire for "summarization failed". They guaranteed it instead: an unconditionally reverting body leaves nothing for the summary to attach to, so every BitMaps call reverted, and rules over a reverting call pass vacuously. The tripwire caused the failure it announced, and made it silent. Measured on a project that uses BitMaps, one variable changed: anchors callsAreReachable the four behavioural rules require(false) VIOLATED all SANITY_FAILED neutral VERIFIED all VERIFIED, none vacuous setThenGetIsTrue verifying non-vacuously is what settles it: with neutral bodies and no working summary, set stores nothing and get reads false, so that rule fails. It passes, so the ghost is doing the work. Neutral bodies also invert the failure mode. An unattached summary now shows up as a violated rule rather than a green vacuous one, and rule_sanity catches the rest. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #216, which puts a curated summary's companion contracts in the scene. The diff here is against that branch.
The
OZ_BitMapssummary reroutesBitMaps.get/set/unset/setToonto a companion contract. It could not attach, for two reasons:canonicalId, which is"<file resolved under .certora_sources>|<qualified name>". A bundled companion declares its own copy ofBitMaps.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.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 things the reroute needs, both fixed here: the host functions have to be
external, sinceDetectRerouteSummariesonly 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_sanitybasic, and one of them is a baresatisfy, so a vacuous pass fails instead of looking like success. The tests live in the Autosetup PR.