From 57ce4e5419ff8d0c148a928fecb4f8e85dcb6967 Mon Sep 17 00:00:00 2001 From: lgalende Date: Mon, 25 Sep 2023 02:37:04 -0300 Subject: [PATCH] smart-vault: implement collect and withdraw rules --- .../smart-vault/certora/conf/smart-vault.conf | 2 + .../smart-vault/certora/helpers/Helpers.sol | 16 ++- .../smart-vault/certora/specs/SmartVault.spec | 128 +++++++++++++++++- 3 files changed, 137 insertions(+), 9 deletions(-) diff --git a/packages/smart-vault/certora/conf/smart-vault.conf b/packages/smart-vault/certora/conf/smart-vault.conf index b0aba212..351e16bf 100644 --- a/packages/smart-vault/certora/conf/smart-vault.conf +++ b/packages/smart-vault/certora/conf/smart-vault.conf @@ -2,12 +2,14 @@ "files": [ "contracts/SmartVault.sol", "../../packages/authorizer/contracts/Authorizer.sol", + "../../packages/fee-controller/contracts/FeeController.sol", "../../packages/helpers/contracts/mocks/WrappedNativeTokenMock.sol", "certora/helpers/Helpers.sol" ], "verify": "SmartVault:certora/specs/SmartVault.spec", "link": [ "SmartVault:authorizer=Authorizer", + "SmartVault:feeController=FeeController", "SmartVault:wrappedNativeToken=WrappedNativeTokenMock" ], "loop_iter": "3", diff --git a/packages/smart-vault/certora/helpers/Helpers.sol b/packages/smart-vault/certora/helpers/Helpers.sol index c592e728..be255096 100644 --- a/packages/smart-vault/certora/helpers/Helpers.sol +++ b/packages/smart-vault/certora/helpers/Helpers.sol @@ -2,8 +2,20 @@ pragma solidity ^0.8.0; +import '@openzeppelin/contracts/token/ERC20/IERC20.sol'; + contract Helpers { - function nativeBalanceOf(address account) external view returns (uint256) { - return address(account).balance; + address public constant NATIVE_TOKEN = 0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE; + + function balanceOf(address token, address account) external view returns (uint256) { + if (token == NATIVE_TOKEN) return address(account).balance; + else return IERC20(token).balanceOf(address(account)); + } + + function authParams(address p1, address p2, uint256 p3) external pure returns (uint256[] memory r) { + r = new uint256[](3); + r[0] = uint256(uint160(p1)); + r[1] = uint256(uint160(p2)); + r[2] = p3; } } diff --git a/packages/smart-vault/certora/specs/SmartVault.spec b/packages/smart-vault/certora/specs/SmartVault.spec index a5264c37..b2e0b336 100644 --- a/packages/smart-vault/certora/specs/SmartVault.spec +++ b/packages/smart-vault/certora/specs/SmartVault.spec @@ -3,23 +3,33 @@ import "./General.spec"; using Helpers as helpers; using WrappedNativeTokenMock as WrappedNativeTokenMock; using Authorizer as Authorizer; +using FeeController as FeeController; // METHODS methods { // Helpers - function helpers.nativeBalanceOf(address) external returns (uint256) envfree; + function helpers.NATIVE_TOKEN() external returns (address) envfree => ALWAYS(0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE); + function helpers.balanceOf(address,address) external returns (uint256) envfree; + function helpers.authParams(address,address,uint256) external returns (uint256[]) envfree; // Wrapped native token mock function WrappedNativeTokenMock.deposit() external; function WrappedNativeTokenMock.withdraw(uint256) external; function WrappedNativeTokenMock.balanceOf(address) external returns (uint256) envfree; + function _.balanceOf(address) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); // Authorizer function Authorizer.isAuthorized(address,address,bytes4,uint256[]) external returns (bool) envfree; + // Fee controller + function FeeController.getFee(address) external returns (uint256,uint256,address) envfree; + // Smart vault function isPaused() external returns (bool) envfree; function priceOracle() external returns (address) envfree; + function feeController() external returns (address) envfree; function wrappedNativeToken() external returns (address) envfree; function isConnectorCheckIgnored(address) external returns (bool) envfree; function getBalanceConnector(bytes32,address) external returns (uint256) envfree; @@ -31,6 +41,10 @@ methods { } // DEFINITIONS +// Constants +definition FIXED_POINT_ONE() returns uint256 = 10^18; + +// Signatures definition INITIALIZE() returns uint32 = sig:initialize(address, address).selector; definition PAUSE() returns uint32 = sig:pause().selector; definition UNPAUSE() returns uint32 = sig:unpause().selector; @@ -40,6 +54,19 @@ definition OVERRIDE_CONNECTOR_CHECK() returns uint32 = sig:overrideConnectorChec definition UPDATE_BALANCE_CONNECTOR() returns uint32 = sig:updateBalanceConnector(bytes32, address, uint256, bool).selector; definition WRAP() returns uint32 = sig:wrap(uint256).selector; definition UNWRAP() returns uint32 = sig:unwrap(uint256).selector; +definition COLLECT() returns uint32 = sig:collect(address, address, uint256).selector; +definition WITHDRAW() returns uint32 = sig:withdraw(address, address, uint256).selector; + +// FUNCTIONS +function requireValidFeeCollector() { + uint256 maxPct; + uint256 pct; + address collector; + maxPct, pct, collector = FeeController.getFee(currentContract); + require maxPct <= FIXED_POINT_ONE() + && pct <= maxPct + && collector != currentContract; // TODO: these might be invariants +} // RULES use rule sanity; @@ -171,12 +198,12 @@ rule unwrapWrapIntegrity(env e, uint256 amount) rule wrapProperBalances(env e, uint256 amount) good_description "After wrapping an `amount` of native tokens, the smart vault balance in wrapped and native token should respectively increase and decrease by that `amount`" { - uint256 initNativeBalance = helpers.nativeBalanceOf(currentContract); + uint256 initNativeBalance = helpers.balanceOf(helpers.NATIVE_TOKEN(), currentContract); uint256 initWrappedBalance = WrappedNativeTokenMock.balanceOf(currentContract); wrap(e, amount); - uint256 currentNativeBalance = helpers.nativeBalanceOf(currentContract); + uint256 currentNativeBalance = helpers.balanceOf(helpers.NATIVE_TOKEN(), currentContract); uint256 currentWrappedBalance = WrappedNativeTokenMock.balanceOf(currentContract); assert to_mathint(currentNativeBalance) == initNativeBalance - amount; @@ -186,19 +213,21 @@ rule wrapProperBalances(env e, uint256 amount) rule unwrapProperBalances(env e, uint256 amount) good_description "After unwrapping an `amount` of wrapped native tokens, the smart vault balance in wrapped and native token should respectively decrease and increase by that `amount`" { - uint256 initNativeBalance = helpers.nativeBalanceOf(currentContract); + uint256 initNativeBalance = helpers.balanceOf(helpers.NATIVE_TOKEN(), currentContract); uint256 initWrappedBalance = WrappedNativeTokenMock.balanceOf(currentContract); unwrap(e, amount); - uint256 currentNativeBalance = helpers.nativeBalanceOf(currentContract); + uint256 currentNativeBalance = helpers.balanceOf(helpers.NATIVE_TOKEN(), currentContract); uint256 currentWrappedBalance = WrappedNativeTokenMock.balanceOf(currentContract); assert to_mathint(currentNativeBalance) == initNativeBalance + amount; assert to_mathint(currentWrappedBalance) == initWrappedBalance - amount; } -rule unwrapCannotRevertAfterWrap(env e, uint256 amount, uint256 amountToUnwrap) { +rule unwrapCannotRevertAfterWrap(env e, uint256 amount, uint256 amountToUnwrap) + good_description "If the call to `wrap` was successful, then `unwrap` should not revert" +{ require amountToUnwrap > 0; uint256[] how = [amountToUnwrap]; @@ -216,7 +245,9 @@ rule unwrapCannotRevertAfterWrap(env e, uint256 amount, uint256 amountToUnwrap) assert to_mathint(amountToUnwrap) <= wrappedAmount => !lastReverted; } -rule wrapCannotRevertAfterUnwrap(env e, uint256 amount, uint256 amountToWrap) { +rule wrapCannotRevertAfterUnwrap(env e, uint256 amount, uint256 amountToWrap) + good_description "If the call to `unwrap` was successful, then `wrap` should not revert" +{ require amountToWrap > 0; uint256[] how = [amountToWrap]; @@ -233,3 +264,86 @@ rule wrapCannotRevertAfterUnwrap(env e, uint256 amount, uint256 amountToWrap) { assert to_mathint(amountToWrap) <= unwrappedAmount => !lastReverted; } + +rule collectWithdrawIntegrity(env e, address token, address user, uint256 amount) + good_description "Calling `collect` and then `withdraw` should not change the smart vault balance" +{ + require token != helpers.NATIVE_TOKEN(); + require user != currentContract; + requireValidFeeCollector(); + + uint256 initBalance = helpers.balanceOf(token, currentContract); + + collect(e, token, user, amount); + withdraw(e, token, user, amount); + + uint256 currentBalance = helpers.balanceOf(token, currentContract); + assert initBalance == currentBalance; +} + +rule withdrawCollectIntegrity(env e, address token, address user, uint256 amount) + good_description "Calling `withdraw` and then `collect` should not change the smart vault balance" +{ + require token != helpers.NATIVE_TOKEN(); + require user != currentContract; + requireValidFeeCollector(); + + uint256 initBalance = helpers.balanceOf(token, currentContract); + + withdraw(e, token, user, amount); + collect(e, token, user, amount); + + uint256 currentBalance = helpers.balanceOf(token, currentContract); + assert initBalance == currentBalance; +} + +rule collectProperBalances(env e, address token, address from, uint256 amount) + good_description "After collecting an `amount` of tokens, the smart vault balance should increase by that `amount`" +{ + require token != helpers.NATIVE_TOKEN(); + require from != currentContract; + + uint256 initBalance = helpers.balanceOf(token, currentContract); + + collect(e, token, from, amount); + + uint256 currentBalance = helpers.balanceOf(token, currentContract); + assert to_mathint(currentBalance) == initBalance + amount; +} + +rule withdrawProperBalances(env e, address token, address recipient, uint256 amount) + good_description "After withdrawing an `amount` of tokens, the smart vault balance should decrease by that `amount`" +{ + require recipient != currentContract; + requireValidFeeCollector(); + + uint256 initBalance = helpers.balanceOf(token, currentContract); + + withdraw(e, token, recipient, amount); + + uint256 currentBalance = helpers.balanceOf(token, currentContract); + assert to_mathint(currentBalance) == initBalance - amount; +} + +rule collectCannotRevertAfterWithdraw(env e, address token, address user, uint256 amount, uint256 amountToCollect) + good_description "If the call to `withdraw` was successful, then `collect` should not revert" +{ + require token != helpers.NATIVE_TOKEN(); + require user != currentContract && user != 0; + require amountToCollect > 0; + requireValidFeeCollector(); + + uint256[] how = [amountToCollect]; // TODO: why is this enough? + require Authorizer.isAuthorized(e.msg.sender, currentContract, to_bytes4(COLLECT()), how); + + uint256 balanceBefore = helpers.balanceOf(token, currentContract); + + withdraw(e, token, user, amount); + + uint256 balanceAfter = helpers.balanceOf(token, currentContract); + mathint withdrawnAmount = balanceAfter - balanceBefore; + + collect@withrevert(e, token, user, amountToCollect); + + assert to_mathint(amountToCollect) <= withdrawnAmount => !lastReverted; +}