smart-vault: implement wrap and unwrap rules

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

@@ -1,8 +1,15 @@
 {
   "files": [
-    "contracts/SmartVault.sol"
+    "contracts/SmartVault.sol",
+    "../../packages/authorizer/contracts/Authorizer.sol",
+    "../../packages/helpers/contracts/mocks/WrappedNativeTokenMock.sol",
+    "certora/helpers/Helpers.sol"
   ],
   "verify": "SmartVault:certora/specs/SmartVault.spec",
+  "link": [
+    "SmartVault:authorizer=Authorizer",
+    "SmartVault:wrappedNativeToken=WrappedNativeTokenMock"
+  ],
   "loop_iter": "3",
   "rule_sanity": "basic",
   "send_only": true,

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

@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: GPL-3.0-or-later
+
+pragma solidity ^0.8.0;
+
+contract Helpers {
+    function nativeBalanceOf(address account) external view returns (uint256) {
+        return address(account).balance;
+    }
+}

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

@@ -1,56 +1,72 @@
 import "./General.spec";
 
+using Helpers as helpers;
+using WrappedNativeTokenMock as WrappedNativeTokenMock;
+using Authorizer as Authorizer;
+
+// METHODS
 methods {
+    // Helpers
+    function helpers.nativeBalanceOf(address) 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;
+
+    // Authorizer
+    function Authorizer.isAuthorized(address,address,bytes4,uint256[]) external returns (bool) envfree;
+
+    // Smart vault
     function isPaused() external returns (bool) envfree;
     function priceOracle() 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;
+    function getBalanceConnector(bytes32,address) external returns (uint256) envfree;
     function pause() external envfree;
     function unpause() external envfree;
     function setPriceOracle(address) external envfree;
-    function overrideConnectorCheck(address, bool) external envfree;
-    function updateBalanceConnector(bytes32, address, uint256, bool) external envfree;
+    function overrideConnectorCheck(address,bool) external envfree;
+    function updateBalanceConnector(bytes32,address,uint256,bool) external envfree;
 }
 
-definition INITIALIZE() returns uint8 = 0;
-definition PAUSE() returns uint8 = 1;
-definition UNPAUSE() returns uint8 = 2;
-
-definition getSelector(uint8 f) returns uint32 = (
-    f == INITIALIZE() ?
-        sig:initialize(address, address).selector : (
-    f == PAUSE() ? 
-        sig:pause().selector : (
-    f == UNPAUSE() ?
-        sig:unpause().selector : 0
-    ))
-);
-
+// DEFINITIONS
+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 WRAP() returns uint32 = sig:wrap(uint256).selector;
+definition UNWRAP() returns uint32 = sig:unwrap(uint256).selector;
+
+// RULES
 use rule sanity;
 
 use rule reentrancyGuard filtered {
     f -> 
         !f.isView
         && !f.isFallback
-        && f.selector != getSelector(INITIALIZE())
-        && f.selector != getSelector(PAUSE())
-        && f.selector != getSelector(UNPAUSE())
+        && f.selector != INITIALIZE()
+        && f.selector != PAUSE()
+        && f.selector != UNPAUSE()
 }
 
 rule canOnlyCallUnpause(env e, method f, calldataarg args)
     filtered { 
         f ->
             !f.isView
             && !f.isFallback
-            && f.selector != getSelector(INITIALIZE())
+            && f.selector != INITIALIZE()
     }
     good_description "If the smart vault is paused, then we cannot call any non-view function except for unpause"
 {
     require isPaused();
 
     f@withrevert(e, args);
 
-    assert lastReverted || f.selector == getSelector(UNPAUSE());
+    assert lastReverted || f.selector == UNPAUSE();
 }
 
 rule stillUnpaused() good_description "Calling pause and then unpause should leave the smart vault unpaused" {
@@ -67,29 +83,53 @@ rule stillPaused() good_description "Calling unpause and then pause should leave
     assert isPaused();
 }
 
-rule setPriceOracleProperly(address newPriceOracle)
-    good_description "Calling `setPriceOracle` should set the price oracle properly"
+rule setPriceOracleOnly(env e, method f, calldataarg args)
+    filtered {
+        f -> 
+            !f.isView
+            && f.selector != INITIALIZE()
+            && f.selector != EXECUTE()
+            && f.selector != SET_PRICE_ORACLE()
+    }
+    good_description "The only method that can modify `priceOracle` reference is `setPriceOracle`"
 {
-    setPriceOracle(newPriceOracle);
-    assert priceOracle() == newPriceOracle;
+    address initPriceOracle = priceOracle();
+
+    f(e, args);
+
+    assert priceOracle() == initPriceOracle;
 }
 
-rule overrideConnectorCheckProperly(address connector, bool ignored)
-    good_description "Calling `overrideConnectorCheck` should override the connector check properly"
+rule overrideConnectorCheckOnly(env e, method f, calldataarg args, address connector)
+    filtered {
+        f -> 
+            !f.isView
+            && f.selector != EXECUTE()
+            && f.selector != OVERRIDE_CONNECTOR_CHECK()
+    }
+    good_description "The only method that can modify `isConnectorCheckIgnored` values is `overrideConnectorCheck`"
 {
-    overrideConnectorCheck(connector, ignored);
-    assert isConnectorCheckIgnored(connector) == ignored;
+    bool initIgnored = isConnectorCheckIgnored(connector);
+
+    f(e, args);
+
+    assert isConnectorCheckIgnored(connector) == initIgnored;
 }
 
-rule updateBalanceConnectorProperly(bytes32 id, address token, uint256 amount, bool add)
-    good_description "Calling `updateBalanceConnector` should update the balance connector properly"
+rule updateBalanceConnectorOnly(env e, method f, calldataarg args, bytes32 id, address token)
+    filtered {
+        f -> 
+            !f.isView
+            && f.selector != EXECUTE()
+            && f.selector != UPDATE_BALANCE_CONNECTOR()
+    }
+    good_description "The only method that can modify balances connectors is `updateBalanceConnector`"
 {
     uint256 initBalanceConnector = getBalanceConnector(id, token);
 
-    updateBalanceConnector(id, token, amount, add);
+    f(e, args);
 
-    uint256 currentBalanceConnector = getBalanceConnector(id, token);
-    assert to_mathint(currentBalanceConnector) == initBalanceConnector + (add ? amount : -amount);
+   assert getBalanceConnector(id, token) == initBalanceConnector;
 }
 
 rule increaseAndDecreaseShouldNotChangeBalanceConnector(bytes32 id, address token, uint256 amount)
@@ -103,3 +143,93 @@ rule increaseAndDecreaseShouldNotChangeBalanceConnector(bytes32 id, address toke
     uint256 currentBalanceConnector = getBalanceConnector(id, token);
     assert initBalanceConnector == currentBalanceConnector;
 }
+
+rule wrapUnwrapIntegrity(env e, uint256 amount)
+    good_description "Calling `wrap` and then `unwrap` should not change the smart vault balance"
+{
+    storage initStorage = lastStorage;
+
+    wrap(e, amount);
+    unwrap(e, amount);
+
+    storage currentStorage = lastStorage;
+    assert initStorage[nativeBalances] == currentStorage[nativeBalances];
+}
+
+rule unwrapWrapIntegrity(env e, uint256 amount)
+    good_description "Calling `unwrap` and then `wrap` should not change the smart vault balance"
+{
+    storage initStorage = lastStorage;
+
+    unwrap(e, amount);
+    wrap(e, amount);
+
+    storage currentStorage = lastStorage;
+    assert initStorage[nativeBalances] == currentStorage[nativeBalances];
+}
+
+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 initWrappedBalance = WrappedNativeTokenMock.balanceOf(currentContract);
+
+    wrap(e, amount);
+
+    uint256 currentNativeBalance = helpers.nativeBalanceOf(currentContract);
+    uint256 currentWrappedBalance = WrappedNativeTokenMock.balanceOf(currentContract);
+
+    assert to_mathint(currentNativeBalance) == initNativeBalance - amount;
+    assert to_mathint(currentWrappedBalance) == initWrappedBalance + 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 initWrappedBalance = WrappedNativeTokenMock.balanceOf(currentContract);
+
+    unwrap(e, amount);
+
+    uint256 currentNativeBalance = helpers.nativeBalanceOf(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) {
+    require amountToUnwrap > 0;
+
+    uint256[] how = [amountToUnwrap];
+    require Authorizer.isAuthorized(e.msg.sender, currentContract, to_bytes4(UNWRAP()), how);
+
+    uint256 wrappedBalanceBefore = WrappedNativeTokenMock.balanceOf(currentContract);
+
+    wrap(e, amount);
+
+    uint256 wrappedBalanceAfter = WrappedNativeTokenMock.balanceOf(currentContract);
+    mathint wrappedAmount = wrappedBalanceAfter - wrappedBalanceBefore;
+
+    unwrap@withrevert(e, amountToUnwrap);
+
+    assert to_mathint(amountToUnwrap) <= wrappedAmount => !lastReverted;
+}
+
+rule wrapCannotRevertAfterUnwrap(env e, uint256 amount, uint256 amountToWrap) {
+    require amountToWrap > 0;
+
+    uint256[] how = [amountToWrap];
+    require Authorizer.isAuthorized(e.msg.sender, currentContract, to_bytes4(WRAP()), how);
+
+    uint256 wrappedBalanceBefore = WrappedNativeTokenMock.balanceOf(currentContract);
+
+    unwrap(e, amount);
+
+    uint256 wrappedBalanceAfter = WrappedNativeTokenMock.balanceOf(currentContract);
+    mathint unwrappedAmount = wrappedBalanceBefore - wrappedBalanceAfter;
+
+    wrap@withrevert(e, amountToWrap);
+
+    assert to_mathint(amountToWrap) <= unwrappedAmount => !lastReverted;
+}