autosetup: curate Solady SafeTransferLib and AuthorityUtils.canCallWithDelay

[jar-ben]

Two additions to the curated summary catalogue.

Solady SafeTransferLib — scoping fix, no new CVL. OZ_SafeERC20.spec
already summarises through a wildcard receiver, and Solady's safeTransfer /
safeTransferFrom carry the same signatures and the same revert-on-failure
contract (checked against Solady's source: it raises TransferFailed() where
OpenZeppelin raises SafeERC20FailedOperation). The entry never matched because
library_names listed only SafeERC20, and _library_matches gates on the
method's defining/originating contract. Both libraries stay on one
summary_file: a project can use both, and two copies of the same wildcard
summary imported into one scene would be a duplicate declaration.

AuthorityUtils.canCallWithDelay — new spec. It is the gate behind
OpenZeppelin AccessManager's restricted modifier, so it sits on the entry path
of every access-controlled function in an AccessManaged contract, and its body is
a hand-written staticcall into an IAuthority the Prover cannot resolve. The
new spec keys an unconstrained ghost pair on all four arguments — authority,
caller, target, selector. That is the sound abstraction of a genuine external
call: the ghosts can take any value, including the (false, 0) the real library
returns when the staticcall fails or returns short data. Keying on fewer
arguments forces a single answer across call sites a real authority can answer
differently, which removes reachable behaviour and can make an access-control
rule pass vacuously.

SafeERC20.forceApprove — deliberately excluded. Its whole purpose is the
recovery path: when approve(value) fails it retries approve(0) then
approve(value). A single dispatched approve prunes the case the library
exists to handle, and a ghost allowance model assumes approve never reverts and
writes to a ghost rather than the token in scene. Either way an approximation
lands inside autosetup, which the precision boundary exists to prevent.

Validation

Ran autosetup end-to-end against a Solady-using project, with the same invocation
the pipeline uses: the generated <Main>_base_summaries.spec gains
import "OpenZeppelin/OZ_SafeERC20.spec";. Not merely imported —
summary_resolver reported dropped entries for the other imported specs and
none for this one, so both wildcard summaries resolved against the scene and
were kept.

OZ_AuthorityUtils.spec typechecks (certoraRun --compilation_steps_only) but
is not exercised end-to-end; the project used for validation does not use
AccessManager.

Tests

4 added to tests/test_curated_library_scene_matching.py (4 -> 8, all pass),
including an end-to-end match through the shipped registry and a check that every
registry entry names a spec file that exists.
pytest tests/ -k "summar or curated or autosetup or registry": 44 passed.

Risk and follow-ups

Widens where an existing wildcard summary is imported; the CVL is unchanged.
Scenes using Solady's SafeTransferLib now dispatch token calls to the real token
instead of leaving unresolved raw calls.

Two things found and not fixed here:

• safeApprove, safeIncreaseAllowance and safeDecreaseAllowance are registry
  entries pointing at OZ_SafeERC20.spec, which does not define them — they
  match and then import a file that summarises nothing. The new file-existence
  test does not catch this (the file exists, the function does not); closing it
  needs a check of entries against the summaries their spec actually declares.
• The OZ SafeERC20 entry can fail to match on projects that do use it, leaving
  the curated summary unapplied. Separate from this change.

Note for the next curated entry: a wildcard method entry may not declare return
types in its signature — the result type goes in expect. The first draft of the
new spec failed to typecheck on exactly that.