Finish Pausable and AccessControl

certora/diff/access_AccessControl.sol.patch

@@ -0,0 +1,11 @@
+--- access/AccessControl.sol	2023-08-10 22:02:18
++++ access/AccessControl.sol	2023-08-10 22:11:07
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControl.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {IAccessControl} from "./IAccessControl.sol";
+ import {Context} from "../utils/Context.sol";

certora/diff/access_IAccessControl.sol.patch

@@ -0,0 +1,11 @@
+--- access/IAccessControl.sol	2023-08-10 22:02:20
++++ access/IAccessControl.sol	2023-08-10 22:11:07
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts v4.4.1 (access/IAccessControl.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ /**
+  * @dev External interface of AccessControl declared to support ERC165 detection.

certora/diff/security_Pausable.sol.patch

@@ -0,0 +1,11 @@
+--- security/Pausable.sol	2023-08-10 21:54:54
++++ security/Pausable.sol	2023-08-10 22:11:07
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts (last updated v4.7.0) (security/Pausable.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {Context} from "../utils/Context.sol";
+ 

certora/diff/token_ERC721_ERC721.sol.patch

@@ -1,6 +1,6 @@
---- token/ERC721/ERC721.sol	2023-03-07 10:48:47.736822221 +0100
-+++ token/ERC721/ERC721.sol	2023-03-09 19:49:39.669338673 +0100
-@@ -199,6 +199,11 @@
+--- token/ERC721/ERC721.sol	2023-08-10 16:45:36
++++ token/ERC721/ERC721.sol	2023-08-10 22:11:07
+@@ -208,6 +208,11 @@
          return _owners[tokenId];
      }
  

certora/diff/utils_Context.sol.patch

@@ -0,0 +1,11 @@
+--- utils/Context.sol	2023-08-10 21:54:56
++++ utils/Context.sol	2023-08-10 22:11:07
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts v4.4.1 (utils/Context.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ /**
+  * @dev Provides information about the current execution context, including the

certora/diff/utils_introspection_ERC165.sol.patch

@@ -0,0 +1,11 @@
+--- utils/introspection/ERC165.sol	2023-08-10 22:02:24
++++ utils/introspection/ERC165.sol	2023-08-10 22:11:07
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts v4.4.1 (utils/introspection/ERC165.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ import {IERC165} from "./IERC165.sol";
+ 

certora/diff/utils_introspection_IERC165.sol.patch

@@ -0,0 +1,11 @@
+--- utils/introspection/IERC165.sol	2023-08-09 11:45:05
++++ utils/introspection/IERC165.sol	2023-08-10 22:11:07
+@@ -1,7 +1,7 @@
+ // SPDX-License-Identifier: MIT
+ // OpenZeppelin Contracts v4.4.1 (utils/introspection/IERC165.sol)
+ 
+-pragma solidity ^0.8.20;
++pragma solidity ^0.8.19;
+ 
+ /**
+  * @dev Interface of the ERC165 standard, as defined in the

certora/harnesses/AccessControlHarness.sol

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: MIT
 
-pragma solidity ^0.8.20;
+pragma solidity ^0.8.19;
 
-import "../patched/access/AccessControl.sol";
+import {AccessControl} from "../patched/access/AccessControl.sol";
 
 contract AccessControlHarness is AccessControl {}

certora/harnesses/PausableHarness.sol

@@ -1,8 +1,8 @@
 // SPDX-License-Identifier: MIT
 
-pragma solidity ^0.8.20;
+pragma solidity ^0.8.19;
 
-import "../patched/security/Pausable.sol";
+import {Pausable} from "../patched/security/Pausable.sol";
 
 contract PausableHarness is Pausable {
     function pause() external {

certora/specs/AccessControl.spec

@@ -1,126 +1,119 @@
-import "helpers/helpers.spec"
-import "methods/IAccessControl.spec"
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Definitions                                                                                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-definition DEFAULT_ADMIN_ROLE() returns bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000;
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions                             │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) {
-    calldataarg args;
-
-    bool hasRoleBefore = hasRole(role, account);
-    f(e, args);
-    bool hasRoleAfter = hasRole(role, account);
-
-    assert (
-        !hasRoleBefore &&
-        hasRoleAfter
-    ) => (
-        f.selector == grantRole(bytes32, address).selector
-    );
-
-    assert (
-        hasRoleBefore &&
-        !hasRoleAfter
-    ) => (
-        f.selector == revokeRole(bytes32, address).selector ||
-        f.selector == renounceRole(bytes32, address).selector
-    );
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: grantRole only affects the specified user/role combo                                          │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule grantRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
-    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-
-    grantRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-
-    // liveness
-    assert success <=> isCallerAdmin;
-
-    // effect
-    assert success => hasRole(role, account);
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: revokeRole only affects the specified user/role combo                                         │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule revokeRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
-    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-
-    revokeRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-
-    // liveness
-    assert success <=> isCallerAdmin;
-
-    // effect
-    assert success => !hasRole(role, account);
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: renounceRole only affects the specified user/role combo                                       │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule renounceRoleEffect(env e, bytes32 role) {
-    require nonpayable(e);
-
-    bytes32 otherRole;
-    address account;
-    address otherAccount;
-
-    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
-
-    renounceRole@withrevert(e, role, account);
-    bool success = !lastReverted;
-
-    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
-
-    // liveness
-    assert success <=> account == e.msg.sender;
-
-    // effect
-    assert success => !hasRole(role, account);
-
-    // no side effect
-    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
-}
+import "helpers/helpers.spec";
+import "methods/IAccessControl.spec";
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions                             │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) {
+    calldataarg args;
+
+    bool hasRoleBefore = hasRole(role, account);
+    f(e, args);
+    bool hasRoleAfter = hasRole(role, account);
+
+    assert (
+        !hasRoleBefore &&
+        hasRoleAfter
+    ) => (
+        f.selector == sig:grantRole(bytes32, address).selector
+    );
+
+    assert (
+        hasRoleBefore &&
+        !hasRoleAfter
+    ) => (
+        f.selector == sig:revokeRole(bytes32, address).selector ||
+        f.selector == sig:renounceRole(bytes32, address).selector
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: grantRole only affects the specified user/role combo                                          │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule grantRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    grantRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: revokeRole only affects the specified user/role combo                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule revokeRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    revokeRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: renounceRole only affects the specified user/role combo                                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule renounceRoleEffect(env e, bytes32 role) {
+    require nonpayable(e);
+
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
+
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
+
+    renounceRole@withrevert(e, role, account);
+    bool success = !lastReverted;
+
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
+
+    // liveness
+    assert success <=> account == e.msg.sender;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
+}

certora/specs/Pausable.spec

@@ -1,96 +1,96 @@
-import "helpers/helpers.spec"
-
-methods {
-    paused() returns (bool) envfree
-    pause()
-    unpause()
-    onlyWhenPaused()
-    onlyWhenNotPaused()
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: _pause pauses the contract                                                                    │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule pause(env e) {
-    require nonpayable(e);
-
-    bool pausedBefore = paused();
-
-    pause@withrevert(e);
-    bool success = !lastReverted;
-
-    bool pausedAfter = paused();
-
-    // liveness
-    assert success <=> !pausedBefore, "works if and only if the contract was not paused before";
-
-    // effect
-    assert success => pausedAfter, "contract must be paused after a successful call";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: _unpause unpauses the contract                                                                │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule unpause(env e) {
-    require nonpayable(e);
-
-    bool pausedBefore = paused();
-
-    unpause@withrevert(e);
-    bool success = !lastReverted;
-
-    bool pausedAfter = paused();
-
-    // liveness
-    assert success <=> pausedBefore, "works if and only if the contract was paused before";
-
-    // effect
-    assert success => !pausedAfter, "contract must be unpaused after a successful call";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: whenPaused modifier can only be called if the contract is paused                              │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule whenPaused(env e) {
-    require nonpayable(e);
-
-    onlyWhenPaused@withrevert(e);
-    assert !lastReverted <=> paused(), "works if and only if the contract is paused";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused                       │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule whenNotPaused(env e) {
-    require nonpayable(e);
-
-    onlyWhenNotPaused@withrevert(e);
-    assert !lastReverted <=> !paused(), "works if and only if the contract is not paused";
-}
-
-/*
-┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
-│ Rules: only _pause and _unpause can change paused status                                                            │
-└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
-*/
-rule noPauseChange(env e) {
-    method f;
-    calldataarg args;
-
-    bool pausedBefore = paused();
-    f(e, args);
-    bool pausedAfter = paused();
-
-    assert pausedBefore != pausedAfter => (
-        (!pausedAfter && f.selector == unpause().selector) ||
-        (pausedAfter && f.selector == pause().selector)
-    ), "contract's paused status can only be changed by _pause() or _unpause()";
-}
+import "helpers/helpers.spec";
+
+methods {
+    function paused() external returns (bool) envfree;
+    function pause() external;
+    function unpause() external;
+    function onlyWhenPaused() external;
+    function onlyWhenNotPaused() external;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: _pause pauses the contract                                                                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule pause(env e) {
+    require nonpayable(e);
+
+    bool pausedBefore = paused();
+
+    pause@withrevert(e);
+    bool success = !lastReverted;
+
+    bool pausedAfter = paused();
+
+    // liveness
+    assert success <=> !pausedBefore, "works if and only if the contract was not paused before";
+
+    // effect
+    assert success => pausedAfter, "contract must be paused after a successful call";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: _unpause unpauses the contract                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule unpause(env e) {
+    require nonpayable(e);
+
+    bool pausedBefore = paused();
+
+    unpause@withrevert(e);
+    bool success = !lastReverted;
+
+    bool pausedAfter = paused();
+
+    // liveness
+    assert success <=> pausedBefore, "works if and only if the contract was paused before";
+
+    // effect
+    assert success => !pausedAfter, "contract must be unpaused after a successful call";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: whenPaused modifier can only be called if the contract is paused                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule whenPaused(env e) {
+    require nonpayable(e);
+
+    onlyWhenPaused@withrevert(e);
+    assert !lastReverted <=> paused(), "works if and only if the contract is paused";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused                       │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule whenNotPaused(env e) {
+    require nonpayable(e);
+
+    onlyWhenNotPaused@withrevert(e);
+    assert !lastReverted <=> !paused(), "works if and only if the contract is not paused";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rules: only _pause and _unpause can change paused status                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule noPauseChange(env e) {
+    method f;
+    calldataarg args;
+
+    bool pausedBefore = paused();
+    f(e, args);
+    bool pausedAfter = paused();
+
+    assert pausedBefore != pausedAfter => (
+        (!pausedAfter && f.selector == sig:unpause().selector) ||
+        (pausedAfter && f.selector == sig:pause().selector)
+    ), "contract's paused status can only be changed by _pause() or _unpause()";
+}

certora/specs/methods/IAccessControl.spec

@@ -1,7 +1,7 @@
 methods {
-    hasRole(bytes32, address) returns(bool) envfree
-    getRoleAdmin(bytes32) returns(bytes32) envfree
-    grantRole(bytes32, address)
-    revokeRole(bytes32, address)
-    renounceRole(bytes32, address)
+    function hasRole(bytes32, address) external returns(bool) envfree;
+    function getRoleAdmin(bytes32) external returns(bytes32) envfree;
+    function grantRole(bytes32, address) external;
+    function revokeRole(bytes32, address) external;
+    function renounceRole(bytes32, address) external;
 }