mirror of
https://github.com/vacp2p/staking-reward-streamer.git
synced 2026-01-09 23:37:58 -05:00
1304846f2c
This commit introduces `AccessControl` capabilities to Karma. The reason this is done so that there can be multiple actors in the system with different privileges. The main changes done here are: - Introduce internal functions for most of the `Karma` specific logic (this is necessary to allow properly extending the contract's functionality via modifiers) later on - Inherit AccessControlUpgradeable contract - Introduce OPERATOR_ROLE next to the already provided DEFAULT_ADMIN_ROLE This is an alternative solution to the PR in #209. Instead of providing an upgrade version, this commit is a breaking change as it introduces a storage layout conflict. BREAKING CHANGE This commit introduces a storage layout conflict. Redeployment required. Closes #207
105 lines
3.2 KiB
Ruby
105 lines
3.2 KiB
Ruby
using Karma as karma;
|
|
|
|
methods {
|
|
function totalDistributorAllocation() external returns (uint256) envfree;
|
|
function totalSupply() external returns (uint256) envfree;
|
|
function externalSupply() external returns (uint256) envfree;
|
|
function _.setReward(uint256, uint256) external => DISPATCHER(true);
|
|
function hasRole(bytes32, address) external returns (bool) envfree;
|
|
function DEFAULT_ADMIN_ROLE() external returns (bytes32) envfree;
|
|
function OPERATOR_ROLE() external returns (bytes32) envfree;
|
|
}
|
|
|
|
persistent ghost mathint sumOfDistributorAllocations {
|
|
init_state axiom sumOfDistributorAllocations == 0;
|
|
}
|
|
|
|
hook Sstore rewardDistributorAllocations[KEY address addr] uint256 newValue (uint256 oldValue) {
|
|
sumOfDistributorAllocations = sumOfDistributorAllocations - oldValue + newValue;
|
|
}
|
|
|
|
invariant totalDistributorAllocationIsSumOfDistributorAllocations()
|
|
to_mathint(totalDistributorAllocation()) == sumOfDistributorAllocations
|
|
filtered {
|
|
f -> !isUpgradeFunction(f)
|
|
}
|
|
|
|
rule externalSupplyIsLessOrEqThanTotalDistributorAllocation() {
|
|
assert externalSupply() <= totalDistributorAllocation();
|
|
}
|
|
|
|
|
|
definition isUpgradeFunction(method f) returns bool = (
|
|
f.selector == sig:karma.upgradeToAndCall(address, bytes).selector ||
|
|
f.selector == sig:karma.upgradeTo(address).selector
|
|
);
|
|
|
|
definition isERC20TransferFunction(method f) returns bool = (
|
|
f.selector == sig:karma.transfer(address, uint256).selector
|
|
|| f.selector == sig:karma.transferFrom(address, address, uint256).selector
|
|
|| f.selector == sig:karma.approve(address, uint256).selector
|
|
);
|
|
|
|
definition isAdminFunction(method f) returns bool = (
|
|
f.selector == sig:karma.addRewardDistributor(address).selector
|
|
|| f.selector == sig:karma.removeRewardDistributor(address).selector
|
|
|
|
);
|
|
|
|
definition isOperatorFunction(method f) returns bool = (
|
|
f.selector == sig:karma.setReward(address, uint256, uint256).selector
|
|
|| f.selector == sig:karma.mint(address, uint256).selector
|
|
);
|
|
|
|
rule erc20TransferIsDisabled(method f) {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
f@withrevert(e, args);
|
|
bool isReverted = lastReverted;
|
|
|
|
assert isERC20TransferFunction(f) => isReverted;
|
|
}
|
|
|
|
rule adminFuncsOnlyCallableByAdmin(method f) {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
bool isOwner = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender);
|
|
|
|
f@withrevert(e, args);
|
|
bool isReverted = lastReverted;
|
|
|
|
assert isAdminFunction(f) && !isOwner => isReverted;
|
|
}
|
|
|
|
rule operatorFuncsCallableByAdminAndOperators(method f) {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
bool isOwner = hasRole(DEFAULT_ADMIN_ROLE(), e.msg.sender);
|
|
bool isOperator = hasRole(OPERATOR_ROLE(), e.msg.sender);
|
|
|
|
f@withrevert(e, args);
|
|
bool isReverted = lastReverted;
|
|
|
|
assert isOperatorFunction(f) && !isOwner && !isOperator => isReverted;
|
|
}
|
|
|
|
rule totalDistributorAllocationCanOnlyIncrease(method f) filtered { f ->
|
|
!isUpgradeFunction(f)
|
|
&& !isERC20TransferFunction(f)
|
|
} {
|
|
env e;
|
|
calldataarg args;
|
|
|
|
|
|
uint256 totalDistributorAllocationBefore = totalDistributorAllocation();
|
|
|
|
f(e, args);
|
|
|
|
uint256 totalDistributorAllocationAfter = totalDistributorAllocation();
|
|
|
|
assert totalDistributorAllocationAfter >= totalDistributorAllocationBefore;
|
|
}
|