Add effect checks on the accesscontrol specs (#4099)

certora/specs/AccessControl.spec

@@ -44,22 +44,27 @@ rule onlyGrantCanGrant(env e, bytes32 role, address account) {
 rule grantRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    grantRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> isCallerAdmin;
+    grantRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == true && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
 
 /*
@@ -70,22 +75,27 @@ rule grantRoleEffect(env e) {
 rule revokeRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    revokeRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> isCallerAdmin;
+    revokeRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == false && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
 
 /*
@@ -96,19 +106,24 @@ rule revokeRoleEffect(env e) {
 rule renounceRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    renounceRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> account2 == e.msg.sender;
+    renounceRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == false && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> account == e.msg.sender;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }