Fix AccessManager FV spec for setAuthority admin delay

[Amxx]

This updates the canCall rule in fv/specs/AccessManager.spec to account for the special-case handling of IAccessManaged.setAuthority(address) in AccessManager.canCall.

For the setAuthority selector, the contract bypasses normal function-role management: only the ADMIN_ROLE can perform the call, and the effective delay is the maximum of the caller's admin execution delay and the target's admin delay (getTargetAdminDelay). The formal verification spec did not model this and was out of sync with the implementation.

This is a behavior change introduced in #6388 ("Fix bypassing target admin delay using execute") that the FV spec was not updated for.

Changes:

• Special-case the setAuthority(address) selector (0x7a9e5e4b), using ADMIN_ROLE as roleId.
• Compute currentDelay as max(memberDelay, targetAdminDelay) for setAuthority, matching Math.max(executionDelay, adminDelay) in the contract.
• Promote currentDelay to mathint and adjust the delay assertion accordingly.

Spec-only change; no changeset needed.

---

Link to certora run for the updated specs: https://prover.certora.com/output/71959/8f88b37ebae64e8e829d206bb0c123d7?anonymousKey=53a555805307674afbfb1afea80bf5fa2a0a3378

[changeset-bot]

⚠️ No Changeset found

Latest commit: 45c0f61

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Repository UI

Review profile: CHILL

Plan: Pro

Run ID: 3f5f76dc-b0cd-48b1-9164-38264e6d6659

📥 Commits

Reviewing files that changed from the base of the PR and between db06a6e and 863c01e.

📒 Files selected for processing (1)

• fv/specs/AccessManager.spec

---

Walkthrough

Updated the canCall rule to detect setAuthority(address) calls, assign them ADMIN_ROLE(), and compute their delay using the maximum of the caller’s role delay and target admin delay. Non-setAuthority calls retain the existing delay logic. Delayed-call validation now compares to_mathint(delay) with the computed delay.

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly and concisely summarizes the spec update for setAuthority admin delay handling.
Description check	✅ Passed	The description accurately explains the AccessManager spec changes and is directly related to the changeset.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fv/access-manager-setauthority-delay

---

_{Comment @coderabbitai help to get the list of available commands.}