vacp2p/staking-reward-streamer
1
0
Fork 0
mirror of https://github.com/vacp2p/staking-reward-streamer.git synced 2026-01-08 20:48:00 -05:00
Code Issues Packages Projects Releases Wiki Activity

test(certora): Karma.totalDistributorAllocation can only increase (#166)

Browse Source
This commit is contained in:
Andrea Franz
2025-03-11 08:24:57 +01:00
committed by GitHub
parent fed4446749
commit 26926c1d5e
1 changed files with 18 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
certora/specs/Karma.spec
View File

@@ -2,10 +2,10 @@ using Karma as karma;
methods {
function owner() external returns (address) envfree;
function totalDistributorAllocation() external returns (uint256) envfree;
}
// TODO:
// totalDistributorAllocation can only increase
// totalDistributorAllocation == sum of all distributor allocations
// sum of external supply <= total supply
@@ -44,3 +44,20 @@ rule ownableFuncsOnlyCallableByOwner(method f) {
assert isOwnableFunction(f) && !isOwner => isReverted;
}
rule totalDistributorAllocationCanOnlyIncrease(method f) filtered { f ->
f.selector != sig:karma.upgradeToAndCall(address, bytes).selector
&& !isERC20TransferFunction(f)
} {
env e;
calldataarg args;
uint256 totalDistributorAllocationBefore = totalDistributorAllocation();
f(e, args);
uint256 totalDistributorAllocationAfter = totalDistributorAllocation();
assert totalDistributorAllocationAfter >= totalDistributorAllocationBefore;
}