Improve FV specifications for AccessControlDefaultAdminRules

[Amxx]

Replaces #4222 (change for the FV workflow to run)

---

Changeset

• Rewrite defaultAdminConsistency to have a better scope, and make smaller assumptions
• Rewrite singleDefaultAdmin to have better coverage / make assumptions
• Reduce the use of require by removing superflous ones.
• Remove the pendingValueAndScheduleCoupling rule that is superfluous
  • everything it proves is already proven in a simpler form in the beginDefaultAdminTransfer and changeDefaultAdminDelay rules)
  • see discussion bellow
• replace nonZeroAccount(address) with nonzerosender(env) in helpers/helpers.spec`
• move max_uint48 and min to helpers/helpers.spec
• use definition instead of function to force inlining
• improve renounceRoleEffect
• improve pendingDefaultAdminDelayEnforced (limitations remain, see comment bellow)
• improve pendingDelayWaitEnforced (limitations remain, see comment bellow)

[changeset-bot]

⚠️ No Changeset found

Latest commit: f1a854d

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

[Amxx]

copy from #4222 (comment)

---

For the pendingValueAndScheduleCoupling, here is an example of why the assert it does are superfluous.

I'm going to focus on

  assert (
    pendingDelayScheduleBefore != pendingDelayScheduleAfter &&
    pendingDelayBefore == pendingDelayAfter
  ) => newDelay == pendingDelayBefore || pendingDelayBefore == 0, "pending delay stays the same if the new delay set is the same";

but the same logic applies to the other checks.

First, we need to observer that this rule is in the format (A && B) → (C || D).

This can be rewritten as: (C || D) || ! (A && B)
ie: C || D || ! A || !B

One interesting thing to remark here is that, since B → C is C || !B, we know that B → C is stronger than (A && B) → (C || D).
Said differently, if we have B → C, we automatically have (A && B) → (C || D) (for any A and D)

This means that if we have

(pendingDelayBefore == pendingDelayAfter) → newDelay == pendingDelayBefore

than the above rule is an immediate consequence.

If we look the rule changeDefaultAdminDelay, we can see that after a call to changeDefaultAdminDelay:

assert success => pendingDelay_(e) == newDelay

Now that we know that after a sucessfull call pendingDelayAfter == newDelay, it is clear that if pendingDelayBefore == pendingDelayAfter than newDelay == pendingDelayBefore (by transitivity of the equality).

It is now clear that changeDefaultAdminDelay proves

(pendingDelayBefore == pendingDelayAfter) → newDelay == pendingDelayBefore

and as a consequence also proves

  assert (
    pendingDelayScheduleBefore != pendingDelayScheduleAfter &&
    pendingDelayBefore == pendingDelayAfter
  ) => newDelay == pendingDelayBefore || pendingDelayBefore == 0;

making (this check of) pendingValueAndScheduleCoupling superfluous.

---

TLDR: the asserts in pendingValueAndScheduleCoupling are overly complex, and prove "less" than what is already proven in the beginDefaultAdminTransfer and changeDefaultAdminDelay rules. We can remove pendingValueAndScheduleCoupling without losing coverage.

[Amxx]

copy from #4222 (comment)

---

About pendingDefaultAdminDelayEnforced (logic also applies to pendingDelayWaitEnforced):

Technically, we would want any number of function being called between e1 and e2. Currently the rule only checks:

after a beginDefaultAdminTransfer call, a single function can only change the admin the call happens after delayBefore.

What we would want to check is that

after a beginDefaultAdminTransfer call, any sequence of calls that result in the admin changing must take at least delayBefore.

---

From the other rules we know that

• admin can only change through acceptDefaultAdminTransfer or renounceRole (rule noDefaultAdminChange)
• acceptDefaultAdminTransfer can only be called after the schedule as passed (rule acceptDefaultAdminTransfer liveness)
• renounceRole can only be called after the schedule as passed (if role is 0) (rule renounceRoleEffect liveness)
• the schedule can only be modified by beginDefaultAdminTransfer, acceptDefaultAdminTransfer or cancelDefaultAdminTransfer (rule noPendingDefaultAdminChange)
• acceptDefaultAdminTransfer sets the schedule to 0 (rule acceptDefaultAdminTransfer)
• cancelDefaultAdminTransfer sets the schedule to 0 (rule cancelDefaultAdminTransfer)
• beginDefaultAdminTransfer sets the delay further enough in the future (rule beginDefaultAdminTransfer)

IMO that is good if on top you add the rules about changing the delay...
Its hard to "compile" because the proof is spread between different rules, but the result is stronger.

We are missing the part where renounceRole only changes the admin if called with the correct role though (added to this PR)

[ernestognw]

LGTM, but considering #4230 needs discussion, we'll need to open a PR removing the comment in renounceRoleEffect

[Amxx]

Updated to reflect the last changes to ACDAR (that how I'm calling AccessControlDefaultAdminRules for short)

[ernestognw]

This comment hasn't been solved, but I'm approving to unblock it under the assumption that if we remove the renounceRole it should still work.

EDIT: Answered and solved