certora: remove authorizer harness

mimic-fi · Oct 4, 2023 · f35b5f8 · f35b5f8
1 parent f088ec1
commit f35b5f8
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 41 deletions.
diff --git a/packages/authorizer/certora/conf/authorizer.conf b/packages/authorizer/certora/conf/authorizer.conf
@@ -1,9 +1,9 @@
 {
   "files": [
-    "certora/harnesses/AuthorizerHarness.sol",
+    "contracts/Authorizer.sol",
     "certora/helpers/Helpers.sol"
   ],
-  "verify": "AuthorizerHarness:certora/specs/Authorizer.spec",
+  "verify": "Authorizer:certora/specs/Authorizer.spec",
   "loop_iter": "3",
   "rule_sanity": "basic",
   "send_only": true,
@@ -19,5 +19,5 @@
   ],
   "solc_allow_path": ".",
   "process": "emv",
-  "msg": "AuthorizerHarness"
+  "msg": "Authorizer"
 }
diff --git a/packages/authorizer/certora/harnesses/AuthorizerHarness.sol b/packages/authorizer/certora/harnesses/AuthorizerHarness.sol
diff --git a/packages/authorizer/certora/specs/Authorizer.spec b/packages/authorizer/certora/specs/Authorizer.spec
@@ -256,7 +256,8 @@ rule grantingPermissionsIsLikeAuthorizing(env e, address who, address where, byt
 
     storage initStorage = lastStorage;
 
-    changePermissions(e, where, true, who, what, false, 0, to_bytes4(0));
+    IAuthorizer.PermissionChange change = buildPermissionChange(where, true, who, what, false, 0, to_bytes4(0));
+    changePermissions(e, [change]);
     storage afterChangePermissions = lastStorage;
 
     authorize(e, who, where, what, params) at initStorage;

diff --git a/packages/authorizer/contracts/Authorizer.sol b/packages/authorizer/contracts/Authorizer.sol
@@ -152,7 +152,7 @@ contract Authorizer is IAuthorizer, AuthorizedHelpers, Initializable, Reentrancy
      * @dev Executes a list of permission changes. Sender must be authorized.
      * @param changes List of permission changes to be executed
      */
-    function changePermissions(PermissionChange[] memory changes) public override {
+    function changePermissions(PermissionChange[] memory changes) external override {
         for (uint256 i = 0; i < changes.length; i++) {
             PermissionChange memory change = changes[i];
             for (uint256 j = 0; j < change.grants.length; j++) {