[Certora] Ensure that an Augustus can't call approve.

certora/confs/AllowancesInvariant.conf

@@ -13,7 +13,8 @@
     "lib/morpho-blue/certora/dispatch/ERC20Standard.sol",
     "lib/morpho-blue/certora/dispatch/ERC20NoRevert.sol",
     "test/helpers/mocks/ERC20Mock.sol",
-    "test/helpers/mocks/ERC20PermitMock.sol"
+    "test/helpers/mocks/ERC20PermitMock.sol",
+    "certora/dispatch/MockAugustus.sol"
   ],
   "parametric_contracts": [
     "EthereumGeneralAdapter1",

certora/dispatch/MockAugustus.sol

@@ -0,0 +1,19 @@
+import {IERC20} from "../../lib/openzeppelin-contracts/contracts/interfaces/IERC20.sol";
+
+contract MockAugustus {
+    address target;
+
+    constructor(address _target) {
+        target = _target;
+    }
+
+    fallback(bytes calldata data) external returns (bytes memory) {
+        require(bytes4(data[:4]) != IERC20.approve.selector);
+        // Here we can't perform a delegate call as it would be summarized with the default case.
+        // Nevertheless, since calls can be summarized appropiately, this can be used to show that `approve` is not
+        // callable at all.
+        (bool success, bytes memory x) = address(target).call(data);
+        require(success);
+        return x;
+    }
+}

certora/specs/AllowancesInvariant.spec

@@ -3,9 +3,12 @@
 using GeneralAdapter1 as GeneralAdapter1;
 using EthereumGeneralAdapter1 as EthereumGeneralAdapter1;
 using ParaswapAdapter as ParaswapAdapter;
+using MockAugustus as MockAugustus;
+using ERC20Mock as ERC20Mock;
 
 methods {
-    function _.approve(address token, address spender, uint256 amount) external => summaryApprove(calledContract, spender, amount) expect bool;
+    // We need to force summarization of unresolved calls, even those sumarized with an unresolved external summary (ALL).
+    function _.approve(address token, address spender, uint256 amount) external => summaryApprove(calledContract, spender, amount) expect bool ALL;
 
     // We need a summary because it does an unresolved call.
     // Sound because the data is "".
@@ -15,11 +18,18 @@ methods {
     // Sound because the selector is "reenter(bytes calldata)".
     function _.reenterBundler3(bytes calldata data) internal => CONSTANT;
 
-    unresolved external in _._ => DISPATCH [] default ASSERT_FALSE;
+    function _.isValidAugustus(address augustus) external => summaryIsValidAugustus(augustus) expect bool;
+
+    // We use the NONDET as a default summary since all approve calls modify a persistent state.
+    // Sound because using HAVOC_ALL wouldn't change the persistent ghost varaible state.
+    unresolved external in MockAugustus._ => DISPATCH(use_fallback=true) [ ERC20Mock.approve(address,uint256) ] default NONDET;
+    unresolved external in _._ => DISPATCH(use_fallback=true) [ MockAugustus._ ] default ASSERT_FALSE;
 }
 
 // Ghost variable to store changed allowances.
 // This models only direct changes in allowances.
+// The variable is persistent since the low-level call to the Augustus contract would havoc its state.
+// Sound since all unresolved calls to approve are being summarized to change this state.
 persistent ghost mapping (address => mapping (address => uint256)) changedAllowances {
     init_state axiom forall address token. forall address spender. changedAllowances[token][spender] == 0 ;
 }
@@ -30,17 +40,16 @@ function summaryApprove(address token, address spender, uint256 amount)  returns
     return true;
 }
 
+function summaryIsValidAugustus(address augustus) returns bool {
+    require augustus == MockAugustus;
+    return true;
+}
+
 definition isTrusted(address spender) returns bool =
     spender == GeneralAdapter1.MORPHO ||
     spender == EthereumGeneralAdapter1.MORPHO ||
     spender == EthereumGeneralAdapter1.MORPHO_WRAPPER ||
     spender == EthereumGeneralAdapter1.WST_ETH;
 
 invariant allowancesAreReset(address token, address spender)
-    isTrusted(spender) || changedAllowances[token][spender] == 0
-    // The invariant doesn't hold with the following functions.
-    filtered {
-      f -> f.selector != sig:ParaswapAdapter.buy(address, bytes ,address, address, uint256, ParaswapAdapter.Offsets, address).selector &&
-           f.selector != sig:ParaswapAdapter.buyMorphoDebt(address, bytes , address, ParaswapAdapter.MarketParams, ParaswapAdapter.Offsets, address, address).selector &&
-           f.selector != sig:ParaswapAdapter.sell(address, bytes, address, address, bool, ParaswapAdapter.Offsets, address).selector
-    }
+    isTrusted(spender) || changedAllowances[token][spender] == 0;