From a55013e742d0673394192e3df36c58778f8d8a59 Mon Sep 17 00:00:00 2001
From: Hadrien Croubois <hadrien.croubois@gmail.com>
Date: Wed, 8 Mar 2023 19:31:46 +0100
Subject: [PATCH] Add effect checks on the accesscontrol specs (#4099)

---
 certora/specs/AccessControl.spec | 85 +++++++++++++++++++-------------
 1 file changed, 50 insertions(+), 35 deletions(-)

diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec
index 170d56fd4..8e8f6ac9d 100644
--- a/certora/specs/AccessControl.spec
+++ b/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);
 }