From 789adb40d4d4b5d96f603fe296240e830a794a67 Mon Sep 17 00:00:00 2001 From: sunbreak1211 Date: Fri, 25 Oct 2024 16:56:04 -0300 Subject: [PATCH] Add Certora specs --- .github/workflows/certora.yml | 45 ++++ .gitignore | 3 + Makefile | 3 + certora/L1FarmProxy.conf | 30 +++ certora/L1FarmProxy.spec | 332 ++++++++++++++++++++++++++++++ certora/L2FarmProxy.conf | 22 ++ certora/L2FarmProxy.spec | 208 +++++++++++++++++++ certora/harness/Auxiliar.sol | 28 +++ test/mocks/FarmMock.sol | 3 + test/mocks/L1TokenGatewayMock.sol | 28 ++- 10 files changed, 697 insertions(+), 5 deletions(-) create mode 100644 .github/workflows/certora.yml create mode 100644 Makefile create mode 100644 certora/L1FarmProxy.conf create mode 100644 certora/L1FarmProxy.spec create mode 100644 certora/L2FarmProxy.conf create mode 100644 certora/L2FarmProxy.spec create mode 100644 certora/harness/Auxiliar.sol diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..0dca91e --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,45 @@ +name: Certora + +on: [push, pull_request] + +jobs: + certora: + name: Certora + runs-on: ubuntu-latest + strategy: + fail-fast: false + matrix: + arbitrum-farms: + - l1-farm-proxy + - l2-farm-proxy + + steps: + - name: Checkout + uses: actions/checkout@v3 + with: + submodules: recursive + + - uses: actions/setup-java@v2 + with: + distribution: 'zulu' + java-version: '11' + java-package: jre + + - name: Set up Python 3.8 + uses: actions/setup-python@v3 + with: + python-version: 3.8 + + - name: Install solc-select + run: pip3 install solc-select + + - name: Solc Select 0.8.21 + run: solc-select install 0.8.21 + + - name: Install Certora + run: pip3 install certora-cli-beta + + - name: Verify ${{ matrix.arbitrum-farms }} + run: make certora-${{ matrix.arbitrum-farms }} results=1 + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/.gitignore b/.gitignore index 87132a9..94e0926 100644 --- a/.gitignore +++ b/.gitignore @@ -12,3 +12,6 @@ docs/ .env deployed-[0-9]*.json + +# Certora +.certora_internal diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..8e30c4e --- /dev/null +++ b/Makefile @@ -0,0 +1,3 @@ +PATH := ~/.solc-select/artifacts/:~/.solc-select/artifacts/solc-0.8.21:$(PATH) +certora-l1-farm-proxy :; PATH=${PATH} certoraRun certora/L1FarmProxy.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) +certora-l2-farm-proxy :; PATH=${PATH} certoraRun certora/L2FarmProxy.conf$(if $(rule), --rule $(rule),)$(if $(results), --wait_for_results all,) diff --git a/certora/L1FarmProxy.conf b/certora/L1FarmProxy.conf new file mode 100644 index 0000000..5bf1501 --- /dev/null +++ b/certora/L1FarmProxy.conf @@ -0,0 +1,30 @@ +{ + "files": [ + "src/L1FarmProxy.sol", + "certora/harness/Auxiliar.sol", + "test/mocks/L1TokenGatewayMock.sol", + "test/mocks/InboxMock.sol", + "test/mocks/GemMock.sol", + ], + "solc": "solc-0.8.21", + "solc_optimize_map": { + "L1FarmProxy": "200", + "Auxiliar": "0", + "L1TokenGatewayMock": "0", + "InboxMock": "0", + "GemMock": "0" + }, + "link": [ + "L1FarmProxy:l1Gateway=L1TokenGatewayMock", + "L1FarmProxy:inbox=InboxMock" + ], + "verify": "L1FarmProxy:certora/L1FarmProxy.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "parametric_contracts": ["L1FarmProxy"], + "build_cache": true, + "optimistic_hashing": true, + "optimistic_fallback": true, + "hashing_length_bound": "512", + "msg": "L1FarmProxy" +} diff --git a/certora/L1FarmProxy.spec b/certora/L1FarmProxy.spec new file mode 100644 index 0000000..46d63d7 --- /dev/null +++ b/certora/L1FarmProxy.spec @@ -0,0 +1,332 @@ +// L1FarmProxy.spec + +using GemMock as gem; +using Auxiliar as aux; +using L1TokenGatewayMock as l1Gateway; + +methods { + // storage variables + function wards(address) external returns (uint256) envfree; + function maxGas() external returns (uint64) envfree; + function gasPriceBid() external returns (uint64) envfree; + function rewardThreshold() external returns (uint128) envfree; + // immutables + function rewardsToken() external returns (address) envfree; + function l2Proxy() external returns (address) envfree; + function feeRecipient() external returns (address) envfree; + function l1Gateway() external returns (address) envfree; + // + function aux.getDataHash(uint256) external returns (bytes32) envfree; + function gem.allowance(address,address) external returns (uint256) envfree; + function gem.totalSupply() external returns (uint256) envfree; + function gem.balanceOf(address) external returns (uint256) envfree; + function l1Gateway.escrow() external returns (address) envfree; + function l1Gateway.lastL1Token() external returns (address) envfree; + function l1Gateway.lastRefundTo() external returns (address) envfree; + function l1Gateway.lastTo() external returns (address) envfree; + function l1Gateway.lastAmount() external returns (uint256) envfree; + function l1Gateway.lastMaxGas() external returns (uint256) envfree; + function l1Gateway.lastGasPriceBid() external returns (uint256) envfree; + function l1Gateway.lastDataHash() external returns (bytes32) envfree; + function l1Gateway.lastValue() external returns (uint256) envfree; + // + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); +} + +persistent ghost bool success; +hook CALL(uint256 g, address addr, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc { + success = rc != 0; +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + + mathint wardsBefore = wards(anyAddr); + mathint maxGasBefore = maxGas(); + mathint gasPriceBidBefore = gasPriceBid(); + mathint rewardThresholdBefore = rewardThreshold(); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + mathint maxGasAfter = maxGas(); + mathint gasPriceBidAfter = gasPriceBid(); + mathint rewardThresholdAfter = rewardThreshold(); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1"; + assert maxGasAfter != maxGasBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 2"; + assert gasPriceBidAfter != gasPriceBidBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 3"; + assert rewardThresholdAfter != rewardThresholdBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 4"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 1, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on rely +rule rely_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + rely@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting deny +rule deny(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + deny(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 0, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on deny +rule deny_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + deny@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting file +rule file(bytes32 what, uint256 data) { + env e; + + mathint maxGasBefore = maxGas(); + mathint gasPriceBidBefore = gasPriceBid(); + mathint rewardThresholdBefore = rewardThreshold(); + + file(e, what, data); + + mathint maxGasAfter = maxGas(); + mathint gasPriceBidAfter = gasPriceBid(); + mathint rewardThresholdAfter = rewardThreshold(); + + assert what == to_bytes32(0x6d61784761730000000000000000000000000000000000000000000000000000) => maxGasAfter == data % (max_uint64 + 1), "Assert 1"; + assert what != to_bytes32(0x6d61784761730000000000000000000000000000000000000000000000000000) => maxGasAfter == maxGasBefore, "Assert 2"; + assert what == to_bytes32(0x6761735072696365426964000000000000000000000000000000000000000000) => gasPriceBidAfter == data % (max_uint64 + 1), "Assert 3"; + assert what != to_bytes32(0x6761735072696365426964000000000000000000000000000000000000000000) => gasPriceBidAfter == gasPriceBidBefore, "Assert 4"; + assert what == to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000) => rewardThresholdAfter == data % (max_uint128 + 1), "Assert 5"; + assert what != to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000) => rewardThresholdAfter == rewardThresholdBefore, "Assert 6"; +} + +// Verify revert rules on file +rule file_revert(bytes32 what, uint256 data) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + file@withrevert(e, what, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = what != to_bytes32(0x6d61784761730000000000000000000000000000000000000000000000000000) && + what != to_bytes32(0x6761735072696365426964000000000000000000000000000000000000000000) && + what != to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000); + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting reclaim +rule reclaim(address receiver, uint256 amount) { + env e; + + // require receiver == rec; + + mathint balanceProxyBefore = nativeBalances[currentContract]; + mathint balanceReceiverBefore = nativeBalances[receiver]; + // ERC20 assumption + require gem.totalSupply() >= balanceProxyBefore + balanceReceiverBefore; + + reclaim(e, receiver, amount); + + mathint balanceProxyAfter = nativeBalances[currentContract]; + mathint balanceReceiverAfter = nativeBalances[receiver]; + + assert currentContract != receiver => balanceProxyAfter == balanceProxyBefore - amount, "Assert 1"; + assert currentContract != receiver => balanceReceiverAfter == balanceReceiverBefore + amount, "Assert 2"; + assert currentContract == receiver => balanceProxyAfter == balanceProxyBefore, "Assert 3"; +} + +// Verify revert rules on reclaim +rule reclaim_revert(address receiver, uint256 amount) { + env e; + + mathint balanceProxy = nativeBalances[currentContract]; + // Practical assumption + require nativeBalances[receiver] + amount <= max_uint256; + + mathint wardsSender = wards(e.msg.sender); + + reclaim@withrevert(e, receiver, amount); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = balanceProxy < amount; + bool revert4 = !success; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting recover +rule recover(address token, address receiver, uint256 amount) { + env e; + + require token == gem; + + mathint tokenBalanceOfProxyBefore = gem.balanceOf(currentContract); + mathint tokenBalanceOfReceiverBefore = gem.balanceOf(receiver); + // ERC20 assumption + require gem.totalSupply() >= tokenBalanceOfProxyBefore + tokenBalanceOfReceiverBefore; + + recover(e, token, receiver, amount); + + mathint tokenBalanceOfProxyAfter = gem.balanceOf(currentContract); + mathint tokenBalanceOfReceiverAfter = gem.balanceOf(receiver); + + assert currentContract != receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore - amount, "Assert 1"; + assert currentContract != receiver => tokenBalanceOfReceiverAfter == tokenBalanceOfReceiverBefore + amount, "Assert 2"; + assert currentContract == receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore, "Assert 3"; +} + +// Verify revert rules on recover +rule recover_revert(address token, address receiver, uint256 amount) { + env e; + + mathint tokenBalanceOfProxy = gem.balanceOf(currentContract); + // ERC20 assumption + require gem.totalSupply() >= tokenBalanceOfProxy + gem.balanceOf(receiver); + + mathint wardsSender = wards(e.msg.sender); + + recover@withrevert(e, token, receiver, amount); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = tokenBalanceOfProxy < amount; + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct estimateDepositCost getter behavior +rule estimateDepositCost(uint256 l1BaseFee, uint256 _maxGas, uint256 _gasPriceBid) { + env e; + + mathint maxSubmissionCost = (1400 + 6 * 324) * (l1BaseFee == 0 ? 30 * 10^9 : l1BaseFee); + mathint l1CallValue = maxSubmissionCost + (_maxGas > 0 ? _maxGas : maxGas()) * (_gasPriceBid > 0 ? _gasPriceBid : gasPriceBid()); + + mathint l1CallValueRet; mathint maxSubmissionCostRet; + l1CallValueRet, maxSubmissionCostRet = estimateDepositCost(e, l1BaseFee, _maxGas, _gasPriceBid); + + assert l1CallValueRet == l1CallValue, "Assert 1"; + assert maxSubmissionCostRet == maxSubmissionCost, "Assert 2"; +} + +// Verify correct storage changes for non reverting notifyRewardAmount +rule notifyRewardAmount(uint256 reward) { + env e; + + address rewardsToken = rewardsToken(); + address l2Proxy = l2Proxy(); + address feeRecipient = feeRecipient(); + mathint maxGas = maxGas(); + mathint gasPriceBid = gasPriceBid(); + uint256 maxSubmissionCost = (1400 + 6 * 324) * 30*10^9; + bytes32 dataHash = aux.getDataHash(maxSubmissionCost); + mathint l1CallValue = maxSubmissionCost + maxGas * gasPriceBid; + + notifyRewardAmount(e, reward); + + address lastL1TokenAfter = l1Gateway.lastL1Token(); + address lastRefundToAfter = l1Gateway.lastRefundTo(); + address lastToAfter = l1Gateway.lastTo(); + mathint lastAmountAfter = l1Gateway.lastAmount(); + mathint lastMaxGasAfter = l1Gateway.lastMaxGas(); + mathint lastGasPriceBidAfter = l1Gateway.lastGasPriceBid(); + bytes32 lastDataHashAfter = l1Gateway.lastDataHash(); + mathint lastValueAfter = l1Gateway.lastValue(); + + assert lastL1TokenAfter == rewardsToken, "Assert 1"; + assert lastRefundToAfter == feeRecipient, "Assert 2"; + assert lastToAfter == l2Proxy, "Assert 3"; + assert lastAmountAfter == to_mathint(reward), "Assert 4"; + assert lastMaxGasAfter == maxGas, "Assert 5"; + assert lastGasPriceBidAfter == gasPriceBid, "Assert 6"; + assert lastDataHashAfter == dataHash, "Assert 7"; + assert lastValueAfter == l1CallValue, "Assert 8"; +} + +// Verify revert rules on notifyRewardAmount +rule notifyRewardAmount_revert(uint256 reward) { + env e; + + require rewardsToken() == gem; + + mathint maxGas = maxGas(); + mathint gasPriceBid = gasPriceBid(); + mathint rewardThreshold = rewardThreshold(); + mathint rewardsTokenBalanceOfProxy = gem.balanceOf(currentContract); + address escrow = l1Gateway.escrow(); + mathint rewardsTokenBalanceOfEscrow = gem.balanceOf(escrow); + // ERC20 assumption + require gem.totalSupply() >= rewardsTokenBalanceOfProxy + rewardsTokenBalanceOfEscrow; + // Happening in constructor + require gem.allowance(currentContract, l1Gateway) == max_uint256; + + mathint balanceProxy = nativeBalances[currentContract]; + uint256 maxSubmissionCost = (1400 + 6 * 324) * 30*10^9; + mathint l1CallValue = maxSubmissionCost + maxGas * gasPriceBid; + // Practical assumption + require nativeBalances[l1Gateway] + l1CallValue <= max_uint256; + + notifyRewardAmount@withrevert(e, reward); + + bool revert1 = e.msg.value > 0; + bool revert2 = reward <= rewardThreshold; + bool revert3 = balanceProxy < l1CallValue; + bool revert4 = rewardsTokenBalanceOfProxy < reward; + + assert lastReverted <=> revert1 || revert2 || revert3 || + revert4, "Revert rules failed"; +} diff --git a/certora/L2FarmProxy.conf b/certora/L2FarmProxy.conf new file mode 100644 index 0000000..e45537f --- /dev/null +++ b/certora/L2FarmProxy.conf @@ -0,0 +1,22 @@ +{ + "files": [ + "src/L2FarmProxy.sol", + "test/mocks/GemMock.sol", + "test/mocks/FarmMock.sol" + ], + "solc": "solc-0.8.21", + "solc_optimize_map": { + "L2FarmProxy": "200", + "GemMock": "0", + "FarmMock": "0" + }, + "link": [ + "L2FarmProxy:farm=FarmMock" + ], + "verify": "L2FarmProxy:certora/L2FarmProxy.spec", + "rule_sanity": "basic", + "multi_assert_check": true, + "parametric_contracts": ["L2FarmProxy"], + "build_cache": true, + "msg": "L2FarmProxy" +} diff --git a/certora/L2FarmProxy.spec b/certora/L2FarmProxy.spec new file mode 100644 index 0000000..dd062d1 --- /dev/null +++ b/certora/L2FarmProxy.spec @@ -0,0 +1,208 @@ +// L2FarmProxy.spec + +using GemMock as gem; +using FarmMock as farm; + +methods { + // storage variables + function wards(address) external returns (uint256) envfree; + function rewardThreshold() external returns (uint256) envfree; + // immutables + function rewardsToken() external returns (address) envfree; + function farm() external returns (address) envfree; + // + function gem.totalSupply() external returns (uint256) envfree; + function gem.balanceOf(address) external returns (uint256) envfree; + function farm.lastReward() external returns (uint256) envfree; + // + function _.balanceOf(address) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); +} + +// Verify that each storage layout is only modified in the corresponding functions +rule storageAffected(method f) { + env e; + + address anyAddr; + + mathint wardsBefore = wards(anyAddr); + mathint rewardThresholdBefore = rewardThreshold(); + + calldataarg args; + f(e, args); + + mathint wardsAfter = wards(anyAddr); + mathint rewardThresholdAfter = rewardThreshold(); + + assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "Assert 1"; + assert rewardThresholdAfter != rewardThresholdBefore => f.selector == sig:file(bytes32,uint256).selector, "Assert 2"; +} + +// Verify correct storage changes for non reverting rely +rule rely(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + rely(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 1, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on rely +rule rely_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + rely@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting deny +rule deny(address usr) { + env e; + + address other; + require other != usr; + + mathint wardsOtherBefore = wards(other); + + deny(e, usr); + + mathint wardsUsrAfter = wards(usr); + mathint wardsOtherAfter = wards(other); + + assert wardsUsrAfter == 0, "Assert 1"; + assert wardsOtherAfter == wardsOtherBefore, "Assert 2"; +} + +// Verify revert rules on deny +rule deny_revert(address usr) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + deny@withrevert(e, usr); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting file +rule file(bytes32 what, uint256 data) { + env e; + + file(e, what, data); + + mathint rewardThresholdAfter = rewardThreshold(); + + assert rewardThresholdAfter == data, "Assert 1"; +} + +// Verify revert rules on file +rule file_revert(bytes32 what, uint256 data) { + env e; + + mathint wardsSender = wards(e.msg.sender); + + file@withrevert(e, what, data); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = what != to_bytes32(0x7265776172645468726573686f6c640000000000000000000000000000000000); + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting recover +rule recover(address token, address receiver, uint256 amount) { + env e; + + require token == gem; + + mathint tokenBalanceOfProxyBefore = gem.balanceOf(currentContract); + mathint tokenBalanceOfReceiverBefore = gem.balanceOf(receiver); + // ERC20 assumption + require gem.totalSupply() >= tokenBalanceOfProxyBefore + tokenBalanceOfReceiverBefore; + + recover(e, token, receiver, amount); + + mathint tokenBalanceOfProxyAfter = gem.balanceOf(currentContract); + mathint tokenBalanceOfReceiverAfter = gem.balanceOf(receiver); + + assert currentContract != receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore - amount, "Assert 1"; + assert currentContract != receiver => tokenBalanceOfReceiverAfter == tokenBalanceOfReceiverBefore + amount, "Assert 2"; + assert currentContract == receiver => tokenBalanceOfProxyAfter == tokenBalanceOfProxyBefore, "Assert 3"; +} + +// Verify revert rules on recover +rule recover_revert(address token, address receiver, uint256 amount) { + env e; + + mathint tokenBalanceOfProxy = gem.balanceOf(currentContract); + // ERC20 assumption + require gem.totalSupply() >= tokenBalanceOfProxy + gem.balanceOf(receiver); + + mathint wardsSender = wards(e.msg.sender); + + recover@withrevert(e, token, receiver, amount); + + bool revert1 = e.msg.value > 0; + bool revert2 = wardsSender != 1; + bool revert3 = tokenBalanceOfProxy < amount; + + assert lastReverted <=> revert1 || revert2 || revert3, "Revert rules failed"; +} + +// Verify correct storage changes for non reverting forwardReward +rule forwardReward() { + env e; + + require rewardsToken() == gem; + + mathint rewardsTokenBalanceOfProxyBefore = gem.balanceOf(currentContract); + mathint rewardsTokenBalanceOfFarmBefore = gem.balanceOf(farm); + // ERC20 assumption + require gem.totalSupply() >= rewardsTokenBalanceOfProxyBefore + rewardsTokenBalanceOfFarmBefore; + + forwardReward(e); + + mathint rewardsTokenBalanceOfProxyAfter = gem.balanceOf(currentContract); + mathint rewardsTokenBalanceOfFarmAfter = gem.balanceOf(farm); + mathint farmLastRewardAfter = farm.lastReward(); + + assert rewardsTokenBalanceOfProxyAfter == 0, "Assert 1"; + assert rewardsTokenBalanceOfFarmAfter == rewardsTokenBalanceOfFarmBefore + rewardsTokenBalanceOfProxyBefore, "Assert 2"; + assert farmLastRewardAfter == rewardsTokenBalanceOfProxyBefore, "Assert 3"; +} + +// Verify revert rules on forwardReward +rule forwardReward_revert() { + env e; + + mathint rewardThreshold = rewardThreshold(); + mathint rewardsTokenBalanceOfProxy = gem.balanceOf(currentContract); + // ERC20 assumption + require gem.totalSupply() >= gem.balanceOf(currentContract) + gem.balanceOf(farm); + + forwardReward@withrevert(e); + + bool revert1 = e.msg.value > 0; + bool revert2 = rewardsTokenBalanceOfProxy <= rewardThreshold; + + assert lastReverted <=> revert1 || revert2, "Revert rules failed"; +} diff --git a/certora/harness/Auxiliar.sol b/certora/harness/Auxiliar.sol new file mode 100644 index 0000000..b4ec010 --- /dev/null +++ b/certora/harness/Auxiliar.sol @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later + +// Copyright (C) 2024 Dai Foundation +// +// This program is free software: you can redistribute it and/or modify +// it under the terms of the GNU Affero General Public License as published by +// the Free Software Foundation, either version 3 of the License, or +// (at your option) any later version. +// +// This program is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU Affero General Public License for more details. +// +// You should have received a copy of the GNU Affero General Public License +// along with this program. If not, see . + +pragma solidity ^0.8.21; + +contract Auxiliar { + function getDataHash(uint256 maxSubmissionCost) public view returns (bytes32) { + return this.getDataHash(maxSubmissionCost, ""); + } + + function getDataHash(uint256 maxSubmissionCost, bytes calldata data) public pure returns (bytes32) { + return keccak256(abi.encode(maxSubmissionCost, data)); + } +} diff --git a/test/mocks/FarmMock.sol b/test/mocks/FarmMock.sol index 151c89e..d68fc4a 100644 --- a/test/mocks/FarmMock.sol +++ b/test/mocks/FarmMock.sol @@ -21,6 +21,8 @@ contract FarmMock { address public immutable rewardsToken; address public immutable stakingToken; + uint256 public lastReward; + event OwnerNominated(address newOwner); event PauseChanged(bool isPaused); event RewardAdded(uint256 rewards); @@ -42,6 +44,7 @@ contract FarmMock { } function notifyRewardAmount(uint256 reward) external { + lastReward = reward; emit RewardAdded(reward); } diff --git a/test/mocks/L1TokenGatewayMock.sol b/test/mocks/L1TokenGatewayMock.sol index 6181bdc..7d7a889 100644 --- a/test/mocks/L1TokenGatewayMock.sol +++ b/test/mocks/L1TokenGatewayMock.sol @@ -25,6 +25,15 @@ contract L1TokenGatewayMock { address public immutable inbox; address public immutable escrow; + address public lastL1Token; + address public lastRefundTo; + address public lastTo; + uint256 public lastAmount; + uint256 public lastMaxGas; + uint256 public lastGasPriceBid; + bytes32 public lastDataHash; + uint256 public lastValue; + constructor( address _inbox, address _escrow @@ -35,13 +44,22 @@ contract L1TokenGatewayMock { function outboundTransferCustomRefund( address l1Token, - address /* refundTo */, - address /* to */, + address refundTo, + address to, uint256 amount, - uint256 /* maxGas */, - uint256 /* gasPriceBid */, - bytes calldata /* data */ + uint256 maxGas, + uint256 gasPriceBid, + bytes calldata data ) public payable returns (bytes memory res) { + lastL1Token = l1Token; + lastRefundTo = refundTo; + lastTo = to; + lastAmount = amount; + lastMaxGas = maxGas; + lastGasPriceBid = gasPriceBid; + lastDataHash = keccak256(data); + lastValue = msg.value; + TokenLike(l1Token).transferFrom(msg.sender, escrow, amount); res = abi.encode(0); }