Add curated CVL summaries for Solady SafeTransferLib, CREATE3, LibClone#51
Open
shellygr wants to merge 4 commits into
Open
Add curated CVL summaries for Solady SafeTransferLib, CREATE3, LibClone#51shellygr wants to merge 4 commits into
shellygr wants to merge 4 commits into
Conversation
Reroutes SafeTransferLib's assembly-based safe wrappers (safeTransfer, safeTransferFrom, safeApprove/safeApproveWithRetry, balanceOf) to direct token calls with require-success, mirroring the OpenZeppelin SafeERC20 summary. The library's inline assembly is what breaks the prover's pointer analysis; the semantics are plain ERC20 calls, so a reroute is sound. Uses an explicit `SafeTransferLib.` receiver (not the wildcard `_.` SafeERC20 uses) so the two summaries coexist without a redeclaration conflict when a project imports both, and so each entry is covered by the summary_resolver prune pass. ETH helpers, the balance-derived transfer-all variants, and the Permit2 helpers are left unsummarized (documented in the spec header). Registered via four function_summaries.json entries gated on library_names = ["SafeTransferLib"]. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Summarizes CREATE3's deterministic-deployment functions as NONDET (arbitrary address, no modeled side effects) — the raw create/create2 assembly is opaque to the prover, so this is the sound over-approximation setups already apply by hand to factory clone/predict calls. Documented limitation in the spec header: exact-address and duplicate-salt-revert properties can't be verified under it. deployDeterministic's argument order differs across Solady versions, so both (initCode, salt) and (salt, initCode) orders are listed. A project has only one; the summary_resolver prune pass keeps by (receiver, name, arity) and the TypecheckerLoop backstop auto-disables the overload not present in the code, so listing both is safe. predictDeterministicAddress signatures are version-stable. Registered via two function_summaries.json entries gated on library_names = ["CREATE3"]. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Internal library summaries must spell reference-type params with their data location (see the bundled ConsenSys BytesLib summary, `bytes memory b`). The deployDeterministic entries used bare `bytes`, which would fail to match the compiled signature and be auto-disabled by the TypecheckerLoop, leaving the function unsummarized. predictDeterministicAddress was unaffected (value types). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Summarizes LibClone's minimal-proxy / ERC-1967 clone factory functions as NONDET (arbitrary address / (bool,address) / bytes32 code hash, no modeled side effects) — the raw create/create2/extcodecopy assembly is opaque to the prover, so this is the sound over-approximation setups apply by hand to a proxy factory's deployDeterministicERC1967 / predictDeterministicAddress calls. Documented limitation: exact-address and duplicate-salt-revert properties can't be verified. Scope: the address-returning families (clone*, deploy*/create*ERC1967*, predict*, implementationOf, erc1967Bootstrap) and the bytes32 initCodeHash* family (91 overloads). Excludes the immutable-arg readers (argsOnClone/argsOnERC1967*/argLoad) and initCode* builders: those read a proxy's immutable args from its bytecode and need per-project ghosts to stay correlated, so they're left to hand-written specs. Signatures generated from a real Solady LibClone compilation. Overloads absent from a project's Solady version are dropped by the prune pass (name/arity) or auto-disabled by the TypecheckerLoop (type mismatch), so listing the full set is safe. Registered via one function_summaries.json entry gated on ["LibClone"]. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
shellygr
commented
Jul 4, 2026
| @@ -0,0 +1,116 @@ | |||
| // Summarization of Solady's LibClone (minimal-proxy / ERC-1967 clone factory library). | |||
Contributor
Author
There was a problem hiding this comment.
these are quite aggressive. double check with previous projects
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.
Curated CVL summaries for three Solady libraries whose inline assembly breaks the prover:
Gated by library name in
function_summaries.json. Version/overload variants are handled by the existing prune pass (name/arity) + TypecheckerLoop backstop, so overloads absent from a project go inert.🤖 Generated with Claude Code