Files
openzeppelin-contracts/certora/specs/methods/IAccessManager.spec
Hadrien Croubois aca4030e4a Formal verification of AccessManager (#4611)
Co-authored-by: Ernesto García <ernestognw@gmail.com>
Co-authored-by: Francisco Giordano <fg@frang.io>
2023-10-04 21:17:15 +02:00

34 lines
2.5 KiB
RPMSpec

methods {
function ADMIN_ROLE() external returns (uint64) envfree;
function PUBLIC_ROLE() external returns (uint64) envfree;
function canCall(address,address,bytes4) external returns (bool,uint32);
function expiration() external returns (uint32) envfree;
function minSetback() external returns (uint32) envfree;
function isTargetClosed(address) external returns (bool) envfree;
function getTargetFunctionRole(address,bytes4) external returns (uint64) envfree;
function getTargetAdminDelay(address) external returns (uint32);
function getRoleAdmin(uint64) external returns (uint64) envfree;
function getRoleGuardian(uint64) external returns (uint64) envfree;
function getRoleGrantDelay(uint64) external returns (uint32);
function getAccess(uint64,address) external returns (uint48,uint32,uint32,uint48);
function hasRole(uint64,address) external returns (bool,uint32);
function labelRole(uint64,string) external;
function grantRole(uint64,address,uint32) external;
function revokeRole(uint64,address) external;
function renounceRole(uint64,address) external;
function setRoleAdmin(uint64,uint64) external;
function setRoleGuardian(uint64,uint64) external;
function setGrantDelay(uint64,uint32) external;
function setTargetFunctionRole(address,bytes4[],uint64) external;
function setTargetAdminDelay(address,uint32) external;
function setTargetClosed(address,bool) external;
function hashOperation(address,address,bytes) external returns (bytes32) envfree;
function getNonce(bytes32) external returns (uint32) envfree;
function getSchedule(bytes32) external returns (uint48);
function schedule(address,bytes,uint48) external returns (bytes32,uint32);
function execute(address,bytes) external returns (uint32);
function cancel(address,address,bytes) external returns (uint32);
function consumeScheduledOp(address,bytes) external;
function updateAuthority(address,address) external;
}