smart-vault: implement execute and call rules

packages/smart-vault/certora/conf/smart-vault.conf

@@ -4,11 +4,13 @@
     "../../packages/authorizer/contracts/Authorizer.sol",
     "../../packages/fee-controller/contracts/FeeController.sol",
     "../../packages/helpers/contracts/mocks/WrappedNativeTokenMock.sol",
+    "../../packages/registry/contracts/Registry.sol",
     "certora/helpers/Helpers.sol"
   ],
   "verify": "SmartVault:certora/specs/SmartVault.spec",
   "link": [
     "SmartVault:authorizer=Authorizer",
+    "SmartVault:registry=Registry",
     "SmartVault:feeController=FeeController",
     "SmartVault:wrappedNativeToken=WrappedNativeTokenMock"
   ],
@@ -27,7 +29,8 @@
     "@mimic-fi/v3-helpers=../../node_modules/@mimic-fi/v3-helpers",
     "@mimic-fi/v3-price-oracle=../../node_modules/@mimic-fi/v3-price-oracle",
     "@mimic-fi/v3-registry=../../node_modules/@mimic-fi/v3-registry",
-    "@openzeppelin=../../node_modules/@openzeppelin"
+    "@openzeppelin=../../node_modules/@openzeppelin",
+    "solmate=../../node_modules/solmate"
   ],
   "solc_allow_path": ".",
   "process": "emv",

packages/smart-vault/certora/helpers/Helpers.sol

@@ -18,4 +18,9 @@ contract Helpers {
         r[1] = uint256(uint160(p2));
         r[2] = p3;
     }
+
+    function authParams(address p1) external pure returns (uint256[] memory r) {
+        r = new uint256[](1);
+        r[0] = uint256(uint160(p1));
+    }
 }

packages/smart-vault/certora/specs/SmartVault.spec

@@ -4,12 +4,14 @@ using Helpers as helpers;
 using WrappedNativeTokenMock as WrappedNativeTokenMock;
 using Authorizer as Authorizer;
 using FeeController as FeeController;
+using Registry as Registry;
 
 // METHODS
 methods {
     // Helpers
     function helpers.NATIVE_TOKEN() external returns (address) envfree => ALWAYS(0xEeeeeEeeeEeEeeEeEeEeeEEEeeeeEeeeeeeeEEeE);
     function helpers.balanceOf(address,address) external returns (uint256) envfree;
+    function helpers.authParams(address) external returns (uint256[]) envfree;
     function helpers.authParams(address,address,uint256) external returns (uint256[]) envfree;
 
     // Wrapped native token mock
@@ -26,6 +28,11 @@ methods {
     // Fee controller
     function FeeController.getFee(address) external returns (uint256,uint256,address) envfree;
 
+    // Registry
+    function Registry.isRegistered(address) external returns (bool) envfree;
+    function Registry.isStateless(address) external returns (bool) envfree;
+    function Registry.isDeprecated(address) external returns (bool) envfree;
+
     // Smart vault
     function isPaused() external returns (bool) envfree;
     function priceOracle() external returns (address) envfree;
@@ -43,15 +50,17 @@ methods {
 // DEFINITIONS
 // Constants
 definition FIXED_POINT_ONE() returns uint256 = 10^18;
+definition MAX_UINT256() returns mathint = 2^256 - 1;
 
 // Signatures
 definition INITIALIZE() returns uint32 = sig:initialize(address, address).selector;
 definition PAUSE() returns uint32 = sig:pause().selector;
 definition UNPAUSE() returns uint32 = sig:unpause().selector;
-definition EXECUTE() returns uint32 = sig:execute(address, bytes).selector;
 definition SET_PRICE_ORACLE() returns uint32 = sig:setPriceOracle(address).selector;
 definition OVERRIDE_CONNECTOR_CHECK() returns uint32 = sig:overrideConnectorCheck(address, bool).selector;
 definition UPDATE_BALANCE_CONNECTOR() returns uint32 = sig:updateBalanceConnector(bytes32, address, uint256, bool).selector;
+definition EXECUTE() returns uint32 = sig:execute(address, bytes).selector;
+definition CALL_SIG() returns uint32 = sig:call(address, bytes, uint256).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;
@@ -68,6 +77,26 @@ function requireValidFeeCollector() {
         && collector != currentContract; // TODO: these might be invariants
 }
 
+function requireValidFeeCollector2(uint256 amount, address token) {
+    uint256 maxPct;
+    uint256 pct;
+    address collector;
+    maxPct, pct, collector = FeeController.getFee(currentContract);
+    require maxPct <= FIXED_POINT_ONE()
+        && pct <= maxPct
+        && amount * pct <= MAX_UINT256()
+        && collector != currentContract;
+
+    uint256 collectorBalance = helpers.balanceOf(token, collector);
+    require collectorBalance + amount <= MAX_UINT256();
+}
+
+function isValidConnector(address connector) returns bool {
+    return Registry.isRegistered(connector)
+        && Registry.isStateless(connector)
+        && !Registry.isDeprecated(connector);
+}
+
 // RULES
 use rule sanity;
 
@@ -325,6 +354,29 @@ rule withdrawProperBalances(env e, address token, address recipient, uint256 amo
     assert to_mathint(currentBalance) == initBalance - amount;
 }
 
+rule withdrawCannotRevertAfterCollect(env e, address token, address user, uint256 amount, uint256 amountToWithdraw)
+    good_description "If the call to `collect` was successful, then `withdraw` should not revert"
+{
+    require token != helpers.NATIVE_TOKEN();
+    require user != currentContract && user != 0;
+    require amountToWithdraw > 0;
+    requireValidFeeCollector2(amountToWithdraw, token);
+
+    uint256[] how = helpers.authParams(token, user, amountToWithdraw);
+    require Authorizer.isAuthorized(e.msg.sender, currentContract, to_bytes4(WITHDRAW()), how);
+
+    uint256 balanceBefore = helpers.balanceOf(token, currentContract);
+
+    collect(e, token, user, amount);
+
+    uint256 balanceAfter = helpers.balanceOf(token, currentContract);
+    mathint collectedAmount = balanceAfter - balanceBefore;
+
+    withdraw@withrevert(e, token, user, amountToWithdraw);
+
+    assert to_mathint(amountToWithdraw) <= collectedAmount => !lastReverted;
+}
+
 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"
 {
@@ -347,3 +399,35 @@ rule collectCannotRevertAfterWithdraw(env e, address token, address user, uint25
 
     assert to_mathint(amountToCollect) <= withdrawnAmount => !lastReverted;
 }
+
+rule executeValidConnector(env e, address connector, bytes data)
+    good_description "If the call to `execute` does not revert, then the connector is valid or overridden"
+{
+    bool isOverridden = isConnectorCheckIgnored(connector);
+
+    execute(e, connector, data);
+
+    assert isOverridden || isValidConnector(connector);
+}
+
+rule executeSenderMustBeAuthorized(env e, address connector, bytes data)
+    good_description "If the call to `execute` does not revert, then the sender must be authorized"
+{
+    uint256[] how = helpers.authParams(connector);
+    bool isAuthorized = Authorizer.isAuthorized(e.msg.sender, currentContract, to_bytes4(EXECUTE()), how);
+
+    execute(e, connector, data);
+
+    assert isAuthorized;
+}
+
+rule callSenderMustBeAuthorized(env e, address target, bytes data, uint256 value)
+    good_description "If the call to `call` does not revert, then the sender must be authorized"
+{
+    uint256[] how = helpers.authParams(target);
+    bool isAuthorized = Authorizer.isAuthorized(e.msg.sender, currentContract, to_bytes4(CALL_SIG()), how);
+
+    call(e, target, data, value);
+
+    assert isAuthorized;
+}