diff --git a/.gitignore b/.gitignore index 72e88a7..7f8014f 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,8 @@ lcov.info broadcast/*/31337 deployments/31337.md deployments/json/31337.json + +# Certora and Gambit cache +.certora_internal +collect.json +collection_failures.txt \ No newline at end of file diff --git a/certora/confs/defaultEmissionManager_verified.conf b/certora/confs/defaultEmissionManager_verified.conf new file mode 100644 index 0000000..c7ad7ef --- /dev/null +++ b/certora/confs/defaultEmissionManager_verified.conf @@ -0,0 +1,29 @@ +{ + "files": [ + "src/PolygonMigration.sol", + "src/PolygonEcosystemToken.sol", + "certora/harnesses/PowUtilHarness.sol:PowUtilHarness", + "certora/harnesses/DefaultEmissionManagerHarness.sol:DefaultEmissionManagerHarness", + "certora/harnesses/helpers/DummyERC20.sol:DummyERC20Impl" + ], + "link": [ + "DefaultEmissionManagerHarness:token=PolygonEcosystemToken", + "DefaultEmissionManagerHarness:migration=PolygonMigration", + "PolygonMigration:matic=DummyERC20Impl", + "PolygonMigration:polygon=PolygonEcosystemToken" + + ], + "verify": + "DefaultEmissionManagerHarness:certora/specs/DefaultEmissionManager.spec", + "packages": [ + "openzeppelin-contracts=lib/openzeppelin-contracts" + ], + "prover_args": [ + "-optimisticFallback true" + ], + "multi_assert_check": true, + "optimistic_loop": true, + "loop_iter": "3", + "send_only": true, + "rule_sanity": "basic" +} \ No newline at end of file diff --git a/certora/confs/gambit/defaultEmissionManger.conf b/certora/confs/gambit/defaultEmissionManger.conf new file mode 100644 index 0000000..52ff4bd --- /dev/null +++ b/certora/confs/gambit/defaultEmissionManger.conf @@ -0,0 +1,8 @@ +{ + "filename": "../../../src/DefaultEmissionManager.sol", + "solc_remappings": [ + "openzeppelin-contracts=../../../lib/openzeppelin-contracts/", + "openzeppelin-contracts-upgradeable=../../../lib/openzeppelin-contracts-upgradeable/" + ], + "num_mutants" : 100 +} \ No newline at end of file diff --git a/certora/confs/gambit/polygonEcosystemToken.conf b/certora/confs/gambit/polygonEcosystemToken.conf new file mode 100644 index 0000000..1fff44f --- /dev/null +++ b/certora/confs/gambit/polygonEcosystemToken.conf @@ -0,0 +1,7 @@ +{ + "filename": "../../../src/PolygonEcosystemToken.sol", + "solc_remappings": [ + "openzeppelin-contracts=../../../lib/openzeppelin-contracts/" + ], + "num_mutants" : 100 +} \ No newline at end of file diff --git a/certora/confs/gambit/polygonMigration.conf b/certora/confs/gambit/polygonMigration.conf new file mode 100644 index 0000000..c208e54 --- /dev/null +++ b/certora/confs/gambit/polygonMigration.conf @@ -0,0 +1,8 @@ +{ + "filename": "../../../src/PolygonMigration.sol", + "solc_remappings": [ + "openzeppelin-contracts=../../../lib/openzeppelin-contracts/", + "openzeppelin-contracts-upgradeable=../../../lib/openzeppelin-contracts-upgradeable/" + ], + "num_mutants" : 100 +} \ No newline at end of file diff --git a/certora/confs/polygonEcosystemToken_verified.conf b/certora/confs/polygonEcosystemToken_verified.conf new file mode 100644 index 0000000..0997396 --- /dev/null +++ b/certora/confs/polygonEcosystemToken_verified.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "certora/harnesses/PolygonEcosystemTokenHarness.sol", + "certora/harnesses/DefaultEmissionManagerHarness.sol:DefaultEmissionManagerHarness" + ], + "verify": + "PolygonEcosystemTokenHarness:certora/specs/PolygonEcosystemToken.spec", + "packages": [ + "openzeppelin-contracts=lib/openzeppelin-contracts" + ], + "prover_args": [ + "-optimisticFallback true" + ], + "multi_assert_check": true, + "optimistic_loop": true, + "loop_iter": "3", + "send_only": true, + "rule_sanity": "basic" +} \ No newline at end of file diff --git a/certora/confs/polygonMigration_verified.conf b/certora/confs/polygonMigration_verified.conf new file mode 100644 index 0000000..7eb73ac --- /dev/null +++ b/certora/confs/polygonMigration_verified.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harnesses/PolygonMigrationHarness.sol:PolygonMigrationHarness", + "certora/harnesses/DefaultEmissionManagerHarness.sol:DefaultEmissionManagerHarness", + "certora/harnesses/helpers/DummyERC20.sol:DummyERC20Impl", + "src/PolygonEcosystemToken.sol:PolygonEcosystemToken" + ], + "link": [ + "PolygonMigrationHarness:polygon=PolygonEcosystemToken", + "PolygonMigrationHarness:matic=DummyERC20Impl" + ], + "verify": + "PolygonMigrationHarness:certora/specs/PolygonMigration.spec", + "packages": [ + "openzeppelin-contracts=lib/openzeppelin-contracts" + ], + "prover_args": [ + "-optimisticFallback true" + ], + "multi_assert_check": true, + "optimistic_loop": true, + "loop_iter": "3", + "send_only": true, + "rule_sanity": "basic" +} \ No newline at end of file diff --git a/certora/confs/powUtil_verified.conf b/certora/confs/powUtil_verified.conf new file mode 100644 index 0000000..e236998 --- /dev/null +++ b/certora/confs/powUtil_verified.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "certora/harnesses/PowUtilHarness.sol" + ], + "verify": + "PowUtilHarness:certora/specs/PowUtil.spec", + "prover_args": [ + "-optimisticFallback true" + ], + "multi_assert_check": true, + "optimistic_loop": true, + "loop_iter": "3", + "send_only": true, + "rule_sanity": "basic" +} \ No newline at end of file diff --git a/certora/confs/runAll.sh b/certora/confs/runAll.sh new file mode 100644 index 0000000..c3f372e --- /dev/null +++ b/certora/confs/runAll.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +# Get a list of all .conf files +CONF_FILES=$(ls certora/confs/*.conf) + +# Iterate over each .conf file +for CONF_FILE in $CONF_FILES; do + echo "Executing $CONF_FILE..." + + # Execute certoraRun with the current .conf file + certoraRun "$CONF_FILE" --msg "$CONF_FILE" + + echo "Done executing $CONF_FILE." + echo +done \ No newline at end of file diff --git a/certora/harnesses/DefaultEmissionManagerHarness.sol b/certora/harnesses/DefaultEmissionManagerHarness.sol new file mode 100644 index 0000000..a5ceb24 --- /dev/null +++ b/certora/harnesses/DefaultEmissionManagerHarness.sol @@ -0,0 +1,51 @@ +pragma solidity 0.8.21; + +import "../../src/DefaultEmissionManager.sol"; + + +contract DefaultEmissionManagerHarness is DefaultEmissionManager { + using SafeERC20 for IPolygonEcosystemToken; + + constructor( + address token_, + address migration_, + address stakeManager_, + address treasury_, + address owner_ + ) DefaultEmissionManager(migration_, stakeManager_, treasury_) + { + if ( + token_ == address(0) || + migration_ == address(0) || + stakeManager_ == address(0) || + treasury_ == address(0) || + owner_ == address(0) + ) revert InvalidAddress(); + + + token = IPolygonEcosystemToken(token_); + migration = IPolygonMigration(migration_); + stakeManager = stakeManager_; + treasury = treasury_; + startTimestamp = block.timestamp; + + assert(START_SUPPLY == token.totalSupply()); + + token.safeApprove(migration_, type(uint256).max); + // initial ownership setup bypassing 2 step ownership transfer process + _transferOwnership(owner_); + + } + + function amountToBeMinted() external view returns (uint256) { + uint256 timeElapsed = block.timestamp - startTimestamp; + uint256 supplyFactor = PowUtil.exp2((INTEREST_PER_YEAR_LOG2 * timeElapsed) / 365 days); + uint256 newSupply = (supplyFactor * START_SUPPLY) / 1e18; + + return newSupply - token.totalSupply(); + } + + function externalExp2(uint256 value) external pure returns (uint256) { + return PowUtil.exp2(value); + } +} \ No newline at end of file diff --git a/certora/harnesses/PolygonEcosystemTokenHarness.sol b/certora/harnesses/PolygonEcosystemTokenHarness.sol new file mode 100644 index 0000000..deac195 --- /dev/null +++ b/certora/harnesses/PolygonEcosystemTokenHarness.sol @@ -0,0 +1,18 @@ +pragma solidity 0.8.21; + +import "../../src/interfaces/IDefaultEmissionManager.sol"; +import "../../src/PolygonEcosystemToken.sol"; + + +contract PolygonEcosystemTokenHarness is PolygonEcosystemToken { + + address private _emissionManager; + constructor(address migration, address emissionManager, address governance, address permit2Revoker) + PolygonEcosystemToken(migration, emissionManager, governance, permit2Revoker) { + _emissionManager = emissionManager; + } + + function fetchMaxMint() external view returns (uint256) { + return (block.timestamp - lastMint) * mintPerSecondCap; + } +} \ No newline at end of file diff --git a/certora/harnesses/PolygonMigrationHarness.sol b/certora/harnesses/PolygonMigrationHarness.sol new file mode 100644 index 0000000..c205d3d --- /dev/null +++ b/certora/harnesses/PolygonMigrationHarness.sol @@ -0,0 +1,12 @@ +pragma solidity 0.8.21; + +import "../../src/PolygonMigration.sol"; + + +contract PolygonMigrationHarness is PolygonMigration { + constructor(address matic_) PolygonMigration(matic_) {} + + function dead() external pure returns (address) { + return 0x000000000000000000000000000000000000dEaD; + } +} \ No newline at end of file diff --git a/certora/harnesses/PowUtilHarness.sol b/certora/harnesses/PowUtilHarness.sol new file mode 100644 index 0000000..e7518e9 --- /dev/null +++ b/certora/harnesses/PowUtilHarness.sol @@ -0,0 +1,10 @@ +pragma solidity 0.8.21; + +import "../../src/lib/PowUtil.sol"; + +contract PowUtilHarness { + function exp2(uint256 value) external pure returns (uint256) { + return PowUtil.exp2(value); + } +} + diff --git a/certora/harnesses/helpers/DummyERC20.sol b/certora/harnesses/helpers/DummyERC20.sol new file mode 100644 index 0000000..90afbe6 --- /dev/null +++ b/certora/harnesses/helpers/DummyERC20.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity 0.8.21; + +// with mint +contract DummyERC20Impl { + uint256 t; + mapping (address => uint256) _balances; + mapping (address => mapping (address => uint256)) a; + + string public name; + string public symbol; + uint public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a +b; + require (c >= a); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a>=b); + return a-b; + } + + function totalSupply() external view returns (uint256) { + return t; + } + function balanceOf(address account) external view returns (uint256) { + return _balances[account]; + } + function transfer(address recipient, uint256 amount) external returns (bool) { + _balances[msg.sender] = sub(_balances[msg.sender], amount); + _balances[recipient] = add(_balances[recipient], amount); + return true; + } + function allowance(address owner, address spender) external view returns (uint256) { + return a[owner][spender]; + } + function approve(address spender, uint256 amount) external returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool) { + _balances[sender] = sub(_balances[sender], amount); + _balances[recipient] = add(_balances[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + return true; + } +} \ No newline at end of file diff --git a/certora/specs/DefaultEmissionManager.spec b/certora/specs/DefaultEmissionManager.spec new file mode 100644 index 0000000..b802cdf --- /dev/null +++ b/certora/specs/DefaultEmissionManager.spec @@ -0,0 +1,166 @@ +import "helpers/helpers.spec"; + +using PolygonEcosystemToken as _PolygonEcosystemToken; +using DummyERC20Impl as _Matic; +using PowUtilHarness as _PowUtil; + + +methods { + function _.exp2(uint256 value) external => fake_exp2(value) expect (uint256); + function _.exp2(uint256 value) internal => fake_exp2(value) expect (uint256); + + function startTimestamp() external returns (uint256) envfree; + function treasury() external returns (address) envfree; + function stakeManager() external returns (address) envfree; + function migration() external returns (address) envfree; + function amountToBeMinted() external returns (uint256); + + function _PolygonEcosystemToken.balanceOf(address) external returns(uint256) envfree; + function _Matic.balanceOf(address) external returns(uint256) envfree; + function _PolygonEcosystemToken.totalSupply() external returns(uint256) envfree; + function _Matic.totalSupply() external returns(uint256) envfree; + + function _.unmigrateTo(address, uint256) external => DISPATCHER(true); + function _.startTimestamp() external => DISPATCHER(true); +} + +// Assuming that exp2 gonna grow as value of value is grow +function fake_exp2(uint256 value) returns uint256 { + return require_uint256(value + 1); +} + +ghost mathint sumOfBalancesPolygon { + init_state axiom sumOfBalancesPolygon == 0; +} + +hook Sload uint256 balance _PolygonEcosystemToken._balances[KEY address addr] STORAGE { + require sumOfBalancesPolygon >= to_mathint(balance); +} + +hook Sstore _PolygonEcosystemToken._balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalancesPolygon = sumOfBalancesPolygon - oldValue + newValue; +} + +invariant totalSupplyIsSumOfBalancesPolygon() + to_mathint(_PolygonEcosystemToken.totalSupply()) == sumOfBalancesPolygon; + + +ghost mathint sumOfBalancesMatic { + init_state axiom sumOfBalancesMatic == 0; +} + +hook Sload uint256 balance _Matic._balances[KEY address addr] STORAGE { + require sumOfBalancesMatic >= to_mathint(balance); +} + +hook Sstore _Matic._balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalancesMatic = sumOfBalancesMatic - oldValue + newValue; +} + + +invariant totalSupplyIsSumOfBalancesMatic() + to_mathint(_Matic.totalSupply()) == sumOfBalancesMatic; + + + +rule correctAmountIsBeingTransferredOnMint ( + env e +) { + requireInvariant totalSupplyIsSumOfBalancesPolygon(); + requireInvariant totalSupplyIsSumOfBalancesMatic(); + + address treasury = treasury(); + address migration = migration(); + address stakeManager = stakeManager(); + address other; + + require treasury != migration && treasury != stakeManager; + require migration != stakeManager && migration != other; + require other != treasury && other != stakeManager; + + mathint treasuryBalanceBefore = _PolygonEcosystemToken.balanceOf(treasury); + mathint migrationBalanceBefore = _PolygonEcosystemToken.balanceOf(migration); + mathint migrationBalanceBeforeMatic = _Matic.balanceOf(migration); + mathint stakeManagerBalanceBefore = _PolygonEcosystemToken.balanceOf(stakeManager); + mathint stakeManagerBalanceBeforeMatic = _Matic.balanceOf(stakeManager); + + mathint otherBalanceBefore = _PolygonEcosystemToken.balanceOf(other); + mathint otherBalanceBeforeMatic = _Matic.balanceOf(other); + + mathint amountShouldbeMinted = amountToBeMinted(e); + + mint(e); + + mathint treasuryBalanceAfter = _PolygonEcosystemToken.balanceOf(treasury); + mathint migrationBalanceAfter = _PolygonEcosystemToken.balanceOf(migration); + mathint migrationBalanceAfterMatic = _Matic.balanceOf(migration); + mathint stakeManagerBalanceAfter = _PolygonEcosystemToken.balanceOf(stakeManager); + mathint stakeManagerBalanceAfterMatic = _Matic.balanceOf(stakeManager); + + mathint otherBalanceAfter = _PolygonEcosystemToken.balanceOf(other); + mathint otherBalanceAfterMatic = _Matic.balanceOf(other); + + mathint amountMintedToTreasury = treasuryBalanceAfter - treasuryBalanceBefore; + mathint amountMintedToMigration = stakeManagerBalanceAfterMatic - stakeManagerBalanceBeforeMatic; + + assert amountShouldbeMinted/3 == amountMintedToTreasury, "1.1"; + assert ((amountShouldbeMinted - amountShouldbeMinted / 3) == amountMintedToMigration) || + (amountShouldbeMinted - amountShouldbeMinted / 3 + 1)== amountMintedToMigration, "1.2"; + + assert treasuryBalanceBefore + amountMintedToTreasury == treasuryBalanceAfter, "1.3"; + assert migrationBalanceBefore + amountMintedToMigration == migrationBalanceAfter, "1.4"; + assert migrationBalanceBeforeMatic - amountMintedToMigration == migrationBalanceAfterMatic, "1.5"; + assert stakeManagerBalanceBefore == stakeManagerBalanceAfter, "1.6"; + assert stakeManagerBalanceBeforeMatic + amountMintedToMigration == stakeManagerBalanceAfterMatic, "1.7"; + assert stakeManagerBalanceBeforeMatic + amountMintedToMigration == stakeManagerBalanceAfterMatic, "1.8"; + + assert otherBalanceBefore == otherBalanceAfter, "1.9"; + assert otherBalanceBeforeMatic == otherBalanceAfterMatic, "1.10"; +} + +rule mintShoulsIncreaseContinueslyOverTime( + env e0, + env e1 + +) { + requireInvariant totalSupplyIsSumOfBalancesPolygon(); + requireInvariant totalSupplyIsSumOfBalancesMatic(); + + + address treasury = treasury(); + address migration = migration(); + address stakeManager = stakeManager(); + address other; + + require treasury != migration && treasury != stakeManager; + require migration != stakeManager && migration != other; + require other != treasury && other != stakeManager; + require e0.block.timestamp < require_uint256(e1.block.timestamp); + + mathint treasuryBalanceBefore = _PolygonEcosystemToken.balanceOf(treasury); + mathint migrationBalanceBefore = _PolygonEcosystemToken.balanceOf(migration); + + storage initialStorage = lastStorage; + mint(e0); + + + mathint treasuryBalanceAfterFirstMint = _PolygonEcosystemToken.balanceOf(treasury); + mathint migrationBalanceAfterFirstMint = _PolygonEcosystemToken.balanceOf(migration); + mint(e1) at initialStorage; + + mathint treasuryBalanceAfterSecondMint = _PolygonEcosystemToken.balanceOf(treasury); + mathint migrationBalanceAfterSecondMint = _PolygonEcosystemToken.balanceOf(migration); + + mathint amountMintedDuringFirstMint = (treasuryBalanceAfterFirstMint - treasuryBalanceBefore) + (migrationBalanceAfterFirstMint - migrationBalanceBefore); + mathint amountMintedDuringSecondMint = (treasuryBalanceAfterSecondMint - treasuryBalanceBefore) + (migrationBalanceAfterSecondMint - migrationBalanceBefore); + + assert amountMintedDuringFirstMint < amountMintedDuringSecondMint; +} + + +rule sanity_satisfy(method f) { + env e; + calldataarg args; + f(e, args); + satisfy true; +} \ No newline at end of file diff --git a/certora/specs/PolygonEcosystemToken.spec b/certora/specs/PolygonEcosystemToken.spec new file mode 100644 index 0000000..66cb3b6 --- /dev/null +++ b/certora/specs/PolygonEcosystemToken.spec @@ -0,0 +1,461 @@ +// Imported from OZ's certora tests + +import "helpers/helpers.spec"; +import "methods/AccessControl.spec"; +import "methods/IERC20.spec"; +import "methods/IERC2612.spec"; + +using DefaultEmissionManagerHarness as _DefaultEmissionManager; + +methods { + // non standard ERC20 functions + function increaseAllowance(address,uint256) external returns (bool); + function decreaseAllowance(address,uint256) external returns (bool); + + // exposed for FV + function mint(address,uint256) external; + function fetchMaxMint() external; + function updateMintCap(uint256) external; + function updatePermit2Allowance(bool) external; + function mintPerSecondCap() external returns (uint256) envfree; + function permit2Enabled() external returns (bool) envfree; + function EMISSION_ROLE() external returns (bytes32) envfree; + function CAP_MANAGER_ROLE() external returns (bytes32) envfree; + function PERMIT2_REVOKER_ROLE() external returns (bytes32) envfree; + function PERMIT2() external returns (address) envfree; +} + +rule sanity_satisfy(method f) { + env e; + calldataarg args; + f(e, args); + satisfy true; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Ghost & hooks: sum of all balances │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +ghost mathint sumOfBalances { + init_state axiom sumOfBalances == 0; +} + +hook Sload uint256 balance _balances[KEY address addr] STORAGE { + require sumOfBalances >= to_mathint(balance); +} + +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalances = sumOfBalances - oldValue + newValue; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: totalSupply is the sum of all balances │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant totalSupplyIsSumOfBalances() + to_mathint(totalSupply()) == sumOfBalances; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: balance of address(0) is 0 │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant zeroAddressNoBalance() + balanceOf(0) == 0; + +// rule zeroAddressNoBalanceAsRule( +// env e, +// method f, +// calldataarg args +// ) { +// require balanceOf(0) == 0; +// f(e, args); +// assert balanceOf(0) == 0; +// } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only mint can change total supply │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyMintShouldChangeTotalSupply(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + + method f; + calldataarg args; + + uint256 totalSupplyBefore = totalSupply(); + f(e, args); + uint256 totalSupplyAfter = totalSupply(); + + assert totalSupplyAfter > totalSupplyBefore => f.selector == sig:mint(address,uint256).selector; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only the token holder or an approved third party can reduce an account's balance │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyAuthorizedCanTransfer(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + + method f; + calldataarg args; + address account; + + uint256 allowanceBefore = allowance(account, e.msg.sender); + uint256 balanceBefore = balanceOf(account); + f(e, args); + uint256 balanceAfter = balanceOf(account); + + assert ( + balanceAfter < balanceBefore + ) => ( + e.msg.sender == account || + balanceBefore - balanceAfter <= to_mathint(allowanceBefore) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only the token holder (or a permit) can increase allowance. The spender can decrease it by using it │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyHolderOfSpenderCanChangeAllowance(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + + method f; + calldataarg args; + address holder; + address spender; + + uint256 allowanceBefore = allowance(holder, spender); + f(e, args); + uint256 allowanceAfter = allowance(holder, spender); + + assert ( + allowanceAfter > allowanceBefore + ) => ( + (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder) || + (f.selector == sig:increaseAllowance(address,uint256).selector && e.msg.sender == holder) || + (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) || + (f.selector == sig:updatePermit2Allowance(bool).selector) + ); + + assert ( + allowanceAfter < allowanceBefore + ) => ( + (f.selector == sig:transferFrom(address,address,uint256).selector && e.msg.sender == spender) || + (f.selector == sig:approve(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == sig:decreaseAllowance(address,uint256).selector && e.msg.sender == holder ) || + (f.selector == sig:permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector) || + (f.selector == sig:updatePermit2Allowance(bool).selector) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: mint behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule mint(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + + address to; + address other; + uint256 amount; + + // cache state + uint256 toBalanceBefore = balanceOf(to); + uint256 otherBalanceBefore = balanceOf(other); + uint256 totalSupplyBefore = totalSupply(); + + uint256 maxMint = fetchMaxMint(e); + + // run transaction + mint@withrevert(e, to, amount); + + // check outcome + if (lastReverted) { + assert to == 0 || totalSupplyBefore + amount > max_uint256 || amount > maxMint || !hasRole(EMISSION_ROLE(), e.msg.sender); + } else { + // updates balance and totalSupply + assert to_mathint(balanceOf(to)) == toBalanceBefore + amount; + assert to_mathint(totalSupply()) == totalSupplyBefore + amount; + + assert amount <= maxMint; + + // no other balance is modified + assert balanceOf(other) != otherBalanceBefore => other == to; + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: transfer behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transfer(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + + address holder = e.msg.sender; + address recipient; + address other; + uint256 amount; + + // cache state + uint256 holderBalanceBefore = balanceOf(holder); + uint256 recipientBalanceBefore = balanceOf(recipient); + uint256 otherBalanceBefore = balanceOf(other); + + // run transaction + transfer@withrevert(e, recipient, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || recipient == 0 || amount > holderBalanceBefore; + } else { + // balances of holder and recipient are updated + assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + + // no other balance is modified + assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: transferFrom behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferFrom(env e) { + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + + address spender = e.msg.sender; + address holder; + address recipient; + address other; + uint256 amount; + + // cache state + uint256 allowanceBefore = allowance(holder, spender); + uint256 holderBalanceBefore = balanceOf(holder); + uint256 recipientBalanceBefore = balanceOf(recipient); + uint256 otherBalanceBefore = balanceOf(other); + + // run transaction + transferFrom@withrevert(e, holder, recipient, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || recipient == 0 || spender == 0 || amount > holderBalanceBefore || amount > allowanceBefore; + } else { + // allowance is valid & updated + assert allowanceBefore >= amount; + assert to_mathint(allowance(holder, spender)) == (allowanceBefore == max_uint256 ? max_uint256 : allowanceBefore - amount); + + // balances of holder and recipient are updated + assert to_mathint(balanceOf(holder)) == holderBalanceBefore - (holder == recipient ? 0 : amount); + assert to_mathint(balanceOf(recipient)) == recipientBalanceBefore + (holder == recipient ? 0 : amount); + + // no other balance is modified + assert balanceOf(other) != otherBalanceBefore => (other == holder || other == recipient); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: approve behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule approve(env e) { + require nonpayable(e); + + address holder = e.msg.sender; + address spender; + address otherHolder; + address otherSpender; + uint256 amount; + + // cache state + uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); + + // run transaction + approve@withrevert(e, spender, amount); + bool didApproveRevert = lastReverted; + + + assert didApproveRevert <=> (holder == 0 || spender == 0); + + assert (!didApproveRevert && (spender != PERMIT2() || !permit2Enabled())) + => allowance(holder, spender) == amount; + assert (!didApproveRevert && (spender == PERMIT2() && permit2Enabled())) + => allowance(holder, spender) == max_uint256; + + // other allowances are untouched + assert (!didApproveRevert && allowance(otherHolder, otherSpender) != otherAllowanceBefore) + => (otherHolder == holder && otherSpender == spender); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: increaseAllowance behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule increaseAllowance(env e) { + require nonpayable(e); + + address holder = e.msg.sender; + address spender; + address otherHolder; + address otherSpender; + uint256 amount; + + // cache state + uint256 allowanceBefore = allowance(holder, spender); + uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); + + // run transaction + increaseAllowance@withrevert(e, spender, amount); + + // check outcome + if (lastReverted) { + assert holder == 0 || spender == 0 || allowanceBefore + amount > max_uint256; + } else { + // allowance is updated + assert to_mathint(allowance(holder, spender)) == allowanceBefore + amount; + + // other allowances are untouched + assert allowance(otherHolder, otherSpender) != otherAllowanceBefore => (otherHolder == holder && otherSpender == spender); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: decreaseAllowance behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule decreaseAllowance(env e) { + require nonpayable(e); + + address holder = e.msg.sender; + address spender; + address otherHolder; + address otherSpender; + uint256 amount; + + // cache state + uint256 allowanceBefore = allowance(holder, spender); + uint256 otherAllowanceBefore = allowance(otherHolder, otherSpender); + + // run transaction + decreaseAllowance@withrevert(e, spender, amount); + bool decreaseAllowance = lastReverted; + + // check outcome + + assert decreaseAllowance <=> holder == 0 || spender == 0 || allowanceBefore < amount; // "If reverted"; + + assert (!decreaseAllowance && (spender != PERMIT2() || permit2Enabled() == false)) + => (allowance(holder, spender)) == assert_uint256(allowanceBefore - amount); // "Allowance should change"; + + assert (!decreaseAllowance && spender == PERMIT2() && permit2Enabled() == true) + => (allowance(holder, spender)) == assert_uint256(allowanceBefore) && + (allowanceBefore == max_uint256); // "Allownce shouldn't change"; + + assert (!decreaseAllowance && allowance(otherHolder, otherSpender) != otherAllowanceBefore) + => otherHolder == holder && otherSpender == spender; // "Allownce shouldn't change"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: updateMintCap behavior │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule updatingMintCap(env e) { + require nonpayable(e); + + uint256 updatedCap; + + updateMintCap@withrevert(e, updatedCap); + bool updateMintCapReverted = lastReverted; + + assert updateMintCapReverted <=> !hasRole(CAP_MANAGER_ROLE(), e.msg.sender); + assert !updateMintCapReverted => (mintPerSecondCap() == updatedCap); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: permit2 behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule togglingPermit2(env e) { + require nonpayable(e); + + bool toggle; + + updatePermit2Allowance@withrevert(e, toggle); + bool updatePermit2AllowanceReverted = lastReverted; + + assert updatePermit2AllowanceReverted <=> !hasRole(PERMIT2_REVOKER_ROLE(), e.msg.sender); + assert !updatePermit2AllowanceReverted => (permit2Enabled() == toggle); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: permit behavior and side effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule permit(env e) { + require nonpayable(e); + + address holder; + address spender; + uint256 amount; + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + + address account1; + address account2; + address account3; + + // cache state + uint256 nonceBefore = nonces(holder); + uint256 otherNonceBefore = nonces(account1); + uint256 otherAllowanceBefore = allowance(account2, account3); + + // sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice + require nonceBefore < max_uint256; + require otherNonceBefore < max_uint256; + + // run transaction + permit@withrevert(e, holder, spender, amount, deadline, v, r, s); + + // check outcome + if (lastReverted) { + // Without formally checking the signature, we can't verify exactly the revert causes + assert true; + } else { + // allowance and nonce are updated + assert (!permit2Enabled() || spender != PERMIT2()) => allowance(holder, spender) == amount; + assert (permit2Enabled() && spender == PERMIT2()) => allowance(holder, spender) == max_uint256; + + assert to_mathint(nonces(holder)) == nonceBefore + 1; + + // deadline was respected + assert deadline >= e.block.timestamp; + + // no other allowance or nonce is modified + assert nonces(account1) != otherNonceBefore => account1 == holder; + assert allowance(account2, account3) != otherAllowanceBefore => (account2 == holder && account3 == spender); + } +} diff --git a/certora/specs/PolygonMigration.spec b/certora/specs/PolygonMigration.spec new file mode 100644 index 0000000..447b5c3 --- /dev/null +++ b/certora/specs/PolygonMigration.spec @@ -0,0 +1,327 @@ +import "helpers/helpers.spec"; + +using PolygonEcosystemToken as _PolygonEcosystemToken; +using DummyERC20Impl as _Matic; + + +methods { + // PolygonMigration functions + function migrate(uint256) external; + function unmigrate(uint256) external; + function unmigrateTo(uint256) external; + function unmigrateWithPermit(uint256) external; + function unmigrateWithPermit(uint256,uint256,uint8,bytes32,bytes32) external; + function updateUnmigrationLock(bool) external; + function burn() external; + + function matic() external returns (address) envfree; + function polygon() external returns (address) envfree; + function unmigrationLocked() external returns (bool) envfree; + function owner() external returns (address) envfree; + function dead() external returns (address) envfree; + + // Polygon Harness + function _PolygonEcosystemToken.allowance(address, address) external returns (uint256) envfree; + function _PolygonEcosystemToken.balanceOf(address) external returns (uint256) envfree; + function _PolygonEcosystemToken.totalSupply() external returns (uint256) envfree; + function _PolygonEcosystemToken.nonces(address) external returns (uint256) envfree; + function _PolygonEcosystemToken.permit2Enabled() external returns (bool) envfree; + function _PolygonEcosystemToken.PERMIT2() external returns (address) envfree; + + // Matic Harness + function _Matic.allowance(address, address) external returns (uint256) envfree; + function _Matic.balanceOf(address) external returns (uint256) envfree; + function _Matic.totalSupply() external returns (uint256) envfree; +} + +ghost mathint sumOfBalancesPolygon { + init_state axiom sumOfBalancesPolygon == 0; +} + +hook Sload uint256 balance _PolygonEcosystemToken._balances[KEY address addr] STORAGE { + require sumOfBalancesPolygon >= to_mathint(balance); +} + +hook Sstore _PolygonEcosystemToken._balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalancesPolygon = sumOfBalancesPolygon - oldValue + newValue; +} + +ghost mathint sumOfBalancesMatic { + init_state axiom sumOfBalancesMatic == 0; +} + +hook Sload uint256 balance _Matic._balances[KEY address addr] STORAGE { + require sumOfBalancesMatic >= to_mathint(balance); +} + +hook Sstore _Matic._balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + sumOfBalancesMatic = sumOfBalancesMatic - oldValue + newValue; +} + +invariant totalSupplyIsSumOfBalances() + to_mathint(_PolygonEcosystemToken.totalSupply()) == sumOfBalancesPolygon && to_mathint(_Matic.totalSupply()) == sumOfBalancesMatic + filtered { + f -> f.selector != sig:setPolygonToken(address).selector + // Filtering setPolygonToken function, because it causes vacuous error in cetrora + } + + + + +rule sanity_satisfy(method f) filtered { + f -> f.selector != sig:setPolygonToken(address).selector +} { + env e; + calldataarg args; + f(e, args); + satisfy true; +} + +rule setUpdateUnmigrationLock(env e) { + require nonpayable(e); + bool unmigrationLock; + + updateUnmigrationLock@withrevert(e, unmigrationLock); + bool didRevert = lastReverted; + + if (didRevert) { + assert e.msg.sender != owner(); + } else { + assert unmigrationLocked() == unmigrationLock; + } +} + +rule verifyUnmigrate(env e) { + uint256 amount; + + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + require nonzerosender(e); + require e.msg.sender != currentContract; + require (_PolygonEcosystemToken.allowance(e.msg.sender, currentContract)) >= amount; + + + uint256 polygonBalanceBeforeCaller = _PolygonEcosystemToken.balanceOf(e.msg.sender); + uint256 maticBalanceBeforeCaller = _Matic.balanceOf(e.msg.sender); + uint256 polygonBalanceBeforeContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceBeforeContract = _Matic.balanceOf(currentContract); + + unmigrate@withrevert(e, amount); + bool didRevert = lastReverted; + + uint256 polygonBalanceAfterCaller = _PolygonEcosystemToken.balanceOf(e.msg.sender); + uint256 maticBalanceAfterCaller = _Matic.balanceOf(e.msg.sender); + uint256 polygonBalanceAfterContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceAfterContract = _Matic.balanceOf(currentContract); + + if(didRevert) { + assert polygonBalanceBeforeCaller < amount || maticBalanceBeforeContract < amount || unmigrationLocked() == true; + assert polygonBalanceBeforeCaller == polygonBalanceAfterCaller && maticBalanceBeforeCaller == maticBalanceAfterCaller; + assert polygonBalanceBeforeContract == polygonBalanceAfterContract && maticBalanceBeforeContract == maticBalanceAfterContract; + } else { + assert require_uint256(polygonBalanceBeforeCaller - amount) == polygonBalanceAfterCaller; + assert require_uint256(maticBalanceBeforeCaller + amount) == maticBalanceAfterCaller; + assert require_uint256(polygonBalanceBeforeContract + amount) == polygonBalanceAfterContract; + assert require_uint256(maticBalanceBeforeContract - amount) == maticBalanceAfterContract; + } +} + +rule verifyUnmigrateTo(env e) { + address to; + uint256 amount; + + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + require nonzerosender(e); + require nonzeroaddress(to); + require e.msg.sender != currentContract && to != currentContract && e.msg.sender != to; + require (_PolygonEcosystemToken.allowance(e.msg.sender, currentContract)) >= amount; + + + uint256 polygonBalanceBeforeCaller = _PolygonEcosystemToken.balanceOf(e.msg.sender); + uint256 maticBalanceBeforeCaller = _Matic.balanceOf(e.msg.sender); + uint256 polygonBalanceBeforeReceiver = _PolygonEcosystemToken.balanceOf(to); + uint256 maticBalanceBeforeReceiver = _Matic.balanceOf(to); + uint256 polygonBalanceBeforeContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceBeforeContract = _Matic.balanceOf(currentContract); + + unmigrateTo@withrevert(e, to, amount); + bool didRevert = lastReverted; + + uint256 polygonBalanceAfterCaller = _PolygonEcosystemToken.balanceOf(e.msg.sender); + uint256 maticBalanceAfterCaller = _Matic.balanceOf(e.msg.sender); + uint256 polygonBalanceAfterReceiver = _PolygonEcosystemToken.balanceOf(to); + uint256 maticBalanceAfterReceiver = _Matic.balanceOf(to); + uint256 polygonBalanceAfterContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceAfterContract = _Matic.balanceOf(currentContract); + + if(didRevert) { + assert polygonBalanceBeforeCaller < amount || maticBalanceBeforeContract < amount || unmigrationLocked() == true; + assert polygonBalanceBeforeCaller == polygonBalanceAfterCaller && maticBalanceBeforeCaller == maticBalanceAfterCaller; + assert polygonBalanceBeforeReceiver == polygonBalanceAfterReceiver && maticBalanceBeforeReceiver == maticBalanceAfterReceiver; + assert polygonBalanceBeforeContract == polygonBalanceAfterContract && maticBalanceBeforeContract == maticBalanceAfterContract; + } else { + assert require_uint256(polygonBalanceBeforeCaller - amount) == polygonBalanceAfterCaller; + assert require_uint256(polygonBalanceBeforeReceiver) == polygonBalanceAfterReceiver; + assert require_uint256(maticBalanceBeforeReceiver + amount) == maticBalanceAfterReceiver; + assert require_uint256(maticBalanceBeforeCaller) == maticBalanceAfterCaller; + assert require_uint256(polygonBalanceBeforeContract + amount) == polygonBalanceAfterContract; + assert require_uint256(maticBalanceBeforeContract - amount) == maticBalanceAfterContract; + } +} + +rule unmigrateWithPermit(env e) { + require nonpayable(e); + requireInvariant totalSupplyIsSumOfBalances(); + + address holder = e.msg.sender; + address spender = currentContract; + + require(holder != spender); + + uint256 amount; + uint256 deadline; + uint8 v; + bytes32 r; + bytes32 s; + + address account1; + address account2; + address account3; + + // cache state + uint256 nonceBefore = _PolygonEcosystemToken.nonces(holder); + uint256 otherNonceBefore = _PolygonEcosystemToken.nonces(account1); + uint256 otherAllowanceBefore = _PolygonEcosystemToken.allowance(account2, account3); + + // sanity: nonce overflow, which possible in theory, is assumed to be impossible in practice + require nonceBefore < max_uint256; + require otherNonceBefore < max_uint256; + + uint256 polygonBalanceBeforeCaller = _PolygonEcosystemToken.balanceOf(holder); + uint256 maticBalanceBeforeCaller = _Matic.balanceOf(holder); + uint256 polygonBalanceBeforeContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceBeforeContract = _Matic.balanceOf(currentContract); + + + // run transaction + unmigrateWithPermit@withrevert(e, amount, deadline, v, r, s); + bool didRevert = lastReverted; + + uint256 polygonBalanceAfterCaller = _PolygonEcosystemToken.balanceOf(holder); + uint256 maticBalanceAfterCaller = _Matic.balanceOf(holder); + uint256 polygonBalanceAfterContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceAfterContract = _Matic.balanceOf(currentContract); + + uint256 callerAllowanceAfter = _PolygonEcosystemToken.allowance(holder, spender); + + // check outcome + if (didRevert) { + assert polygonBalanceBeforeCaller == polygonBalanceAfterCaller && maticBalanceBeforeCaller == maticBalanceAfterCaller; + assert polygonBalanceBeforeContract == polygonBalanceAfterContract && maticBalanceBeforeContract == maticBalanceAfterContract; + + // Without formally checking the signature, we can't verify exactly the revert causes + assert polygonBalanceBeforeCaller < amount || maticBalanceBeforeContract < amount || unmigrationLocked() == true || deadline < e.block.timestamp || true; + } else { + // allowance and nonce are updated + assert amount == max_uint256 => (max_uint256) == callerAllowanceAfter; + + assert (amount < max_uint256 && (!_PolygonEcosystemToken.permit2Enabled() || spender != _PolygonEcosystemToken.PERMIT2())) + => require_uint256(0) == callerAllowanceAfter; + + assert to_mathint(_PolygonEcosystemToken.nonces(holder)) == nonceBefore + 1; + + assert require_uint256(polygonBalanceBeforeCaller - amount) == polygonBalanceAfterCaller && + require_uint256(maticBalanceBeforeCaller + amount) == maticBalanceAfterCaller; + + assert require_uint256(polygonBalanceBeforeContract + amount) == polygonBalanceAfterContract && + require_uint256(maticBalanceBeforeContract - amount) == maticBalanceAfterContract; + + // deadline was respected + assert deadline >= e.block.timestamp; + + // no other allowance or nonce is modified + assert _PolygonEcosystemToken.nonces(account1) != otherNonceBefore => account1 == holder; + assert _PolygonEcosystemToken.allowance(account2, account3) != otherAllowanceBefore => (account2 == holder && account3 == spender); + } +} + +rule verifyMigrate(env e) { + uint256 amount; + address other; + + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + require nonzerosender(e); + require e.msg.sender != currentContract && e.msg.sender != other; + require other != currentContract; + require (_Matic.allowance(e.msg.sender, currentContract)) >= amount; + + + uint256 polygonBalanceBeforeCaller = _PolygonEcosystemToken.balanceOf(e.msg.sender); + uint256 maticBalanceBeforeCaller = _Matic.balanceOf(e.msg.sender); + uint256 polygonBalanceBeforeContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceBeforeContract = _Matic.balanceOf(currentContract); + uint256 polygonBalanceBeforeOther = _PolygonEcosystemToken.balanceOf(other); + uint256 maticBalanceBeforeOther = _Matic.balanceOf(other); + + + migrate@withrevert(e, amount); + bool didRevert = lastReverted; + + uint256 polygonBalanceAfterCaller = _PolygonEcosystemToken.balanceOf(e.msg.sender); + uint256 maticBalanceAfterCaller = _Matic.balanceOf(e.msg.sender); + uint256 polygonBalanceAfterContract = _PolygonEcosystemToken.balanceOf(currentContract); + uint256 maticBalanceAfterContract = _Matic.balanceOf(currentContract); + uint256 polygonBalanceAfterOther = _PolygonEcosystemToken.balanceOf(other); + uint256 maticBalanceAfterOther = _Matic.balanceOf(other); + + if(didRevert) { + assert maticBalanceBeforeCaller < amount || polygonBalanceBeforeContract < amount; + assert polygonBalanceBeforeCaller == polygonBalanceAfterCaller && maticBalanceBeforeCaller == maticBalanceAfterCaller; + assert polygonBalanceBeforeContract == polygonBalanceAfterContract && maticBalanceBeforeContract == maticBalanceAfterContract; + assert polygonBalanceBeforeOther == polygonBalanceAfterOther && polygonBalanceAfterOther == polygonBalanceAfterOther; + } else { + assert require_uint256(polygonBalanceBeforeCaller + amount) == polygonBalanceAfterCaller; + assert require_uint256(maticBalanceBeforeCaller - amount) == maticBalanceAfterCaller; + assert require_uint256(polygonBalanceBeforeContract - amount) == polygonBalanceAfterContract; + assert require_uint256(maticBalanceBeforeContract + amount) == maticBalanceAfterContract; + assert polygonBalanceBeforeOther == polygonBalanceAfterOther && polygonBalanceAfterOther == polygonBalanceAfterOther; + } +} + +rule shouldRevertIfUnmigrateIsLocked(env e) { + + uint256 amount; + + requireInvariant totalSupplyIsSumOfBalances(); + require nonpayable(e); + require nonzerosender(e); + require e.msg.sender != currentContract; + require (_PolygonEcosystemToken.allowance(e.msg.sender, currentContract)) >= amount; + + require (_PolygonEcosystemToken.balanceOf(e.msg.sender) >= amount); + require (_Matic.balanceOf(currentContract) >= amount); + + unmigrate@withrevert(e, amount); + + bool didUnmigrateRevert = lastReverted; + + assert didUnmigrateRevert <=> unmigrationLocked() == true; + +} + +rule shouldBurn(env e) { + require(currentContract != dead()); + uint256 amount; + + uint256 balanceBefore = _PolygonEcosystemToken.balanceOf(currentContract); + + burn(e, amount); + bool didRevert = lastReverted; + + uint256 balanceAfter = _PolygonEcosystemToken.balanceOf(currentContract); + + assert didRevert <=> (balanceBefore < amount || owner() != e.msg.sender); + assert !didRevert <=> (require_uint256(balanceAfter + amount) == balanceBefore); +} \ No newline at end of file diff --git a/certora/specs/PowUtil.spec b/certora/specs/PowUtil.spec new file mode 100644 index 0000000..940bd88 --- /dev/null +++ b/certora/specs/PowUtil.spec @@ -0,0 +1,45 @@ +// Rules are timing out, as this function doing exponential calculations + +methods { + function exp2(uint256) external returns(uint256) envfree; +} + +// Since log2 graph is steadily increasing, we can prove property that log(a) <= log(b) if a <= b +rule verifyingSteadyIncrease(env e) { + uint256 a; + uint256 b; + + require a >= 1352 * 10^6; + require b <= 28569152196770896000; + require a <= b; + + uint256 exp2A = exp2(a); + uint256 exp2B = exp2(b); + + require exp2B != 0; // cause this reverts anyway + + assert exp2A <= exp2B; +} + +rule resultShouldAlwaysbeGEThanOne(env e) { + uint256 a; + + require a >= 1352 * 10^6; + require a < 0xa688906bd8b000000; + + + mathint result = exp2(a); + + assert result >= 10 ^ 18 ; +} + +rule resultShouldNotBeZero(env e) { + uint256 a; + + require a >= 1352 * 10^6; + require a < 0xa688906bd8b000000; + + mathint result = exp2(a); + + assert result != 0; +} diff --git a/certora/specs/helpers/helpers.spec b/certora/specs/helpers/helpers.spec new file mode 100644 index 0000000..6fc5442 --- /dev/null +++ b/certora/specs/helpers/helpers.spec @@ -0,0 +1,8 @@ +// environment +definition nonpayable(env e) returns bool = e.msg.value == 0; +definition nonzerosender(env e) returns bool = e.msg.sender != 0; +definition nonzeroaddress(address addr) returns bool = addr != 0; + +// math +definition min(mathint a, mathint b) returns mathint = a < b ? a : b; +definition max(mathint a, mathint b) returns mathint = a > b ? a : b; \ No newline at end of file diff --git a/certora/specs/methods/AccessControl.spec b/certora/specs/methods/AccessControl.spec new file mode 100644 index 0000000..6697089 --- /dev/null +++ b/certora/specs/methods/AccessControl.spec @@ -0,0 +1,3 @@ +methods { + function hasRole(bytes32, address) external returns (bool) envfree; +} \ No newline at end of file diff --git a/certora/specs/methods/IERC20.spec b/certora/specs/methods/IERC20.spec new file mode 100644 index 0000000..133827a --- /dev/null +++ b/certora/specs/methods/IERC20.spec @@ -0,0 +1,13 @@ +// Imported from OZ's certora tests + +methods { + function name() external returns (string) envfree; + function symbol() external returns (string) envfree; + function decimals() external returns (uint8) envfree; + function totalSupply() external returns (uint256) envfree; + function balanceOf(address) external returns (uint256) envfree; + function allowance(address,address) external returns (uint256) envfree; + function approve(address,uint256) external returns (bool); + function transfer(address,uint256) external returns (bool); + function transferFrom(address,address,uint256) external returns (bool); +} \ No newline at end of file diff --git a/certora/specs/methods/IERC2612.spec b/certora/specs/methods/IERC2612.spec new file mode 100644 index 0000000..53304ad --- /dev/null +++ b/certora/specs/methods/IERC2612.spec @@ -0,0 +1,7 @@ +// Imported from OZ's certora tests + +methods { + function permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external; + function nonces(address) external returns (uint256) envfree; + function DOMAIN_SEPARATOR() external returns (bytes32) envfree; +} \ No newline at end of file