Absolute import paths

.github/workflows/certora-prover.yml

@@ -28,6 +28,10 @@ jobs:
         with:
           submodules: recursive
 
+      # Install foundry, needed for prover path resolution
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
       # Run Certora munge script
       - name: Certora munge
         run: ./certora/scripts/patch.sh

certora/confs/BaseConfForInheritance.conf

@@ -23,12 +23,6 @@
         "VaultMock1:_asset=Token0",
         "EulerEarnHarness:_asset=Token0"
     ],
-    "packages": [
-        "ethereum-vault-connector=lib/ethereum-vault-connector/src",
-        "euler-vault-kit=lib/euler-vault-kit/src",
-        "forge-std=lib/forge-std/src",
-        "solmate=lib/euler-vault-kit/lib/permit2/lib/solmate"
-    ],
     "compiler_map": {
         "EulerEarnHarness": "solc-0.8.26",
         "EthereumVaultConnector": "solc-0.8.26",

certora/confs/Solvency.conf

@@ -10,7 +10,8 @@
     "process": "emv",
     "prover_args": [
         "-cvlFunctionRevert true",
-        "-depth 0"
+        "-depth 0",
+        "-disabledTransformations OPTIMIZE_INFEASIBLE_PATHS",
     ],
     "override_base_config": "certora/confs/BaseConfForInheritance.conf"
 }

certora/confs/SolvencyInternal.conf

@@ -9,5 +9,56 @@
         "-cvlFunctionRevert true",
         "-depth 0"
     ],
-    "override_base_config": "certora/confs/BaseConfForInheritance.conf"
+    "optimistic_loop": true,
+    "global_timeout": "7200",
+    "parametric_contracts": "EulerEarnHarness",
+    "rule_sanity": "basic",
+    "files": [
+        "certora/harnesses/EulerEarnHarness.sol",
+        "lib/ethereum-vault-connector/src/EthereumVaultConnector.sol",
+        "lib/euler-vault-kit/lib/permit2/src/Permit2.sol",
+        "src/EulerEarnFactory.sol",
+        "test/mocks/PerspectiveMock.sol",
+        "certora/mocks/VaultMock0.sol",
+        "certora/mocks/VaultMock1.sol",
+        "certora/mocks/Token0.sol",
+        "certora/harnesses/ERC20Helper.sol"
+    ],
+    "link": [
+        "EulerEarnHarness:evc=EthereumVaultConnector",
+        "EulerEarnHarness:permit2Address=Permit2",
+        "EulerEarnFactory:permit2Address=Permit2",
+        "EulerEarnFactory:perspective=PerspectiveMock",
+        "VaultMock0:_asset=Token0",
+        "VaultMock1:_asset=Token0",
+        "EulerEarnHarness:_asset=Token0"
+    ],
+    "compiler_map": {
+        "EulerEarnHarness": "solc-0.8.26",
+        "EthereumVaultConnector": "solc-0.8.26",
+        "Permit2": "solc-0.8.17",
+        "EulerEarnFactory": "solc-0.8.26",
+        "PerspectiveMock": "solc-0.8.26",
+        "IRMLinearKink": "solc-0.8.26",
+        "VaultMock0": "solc-0.8.26",
+        "VaultMock1": "solc-0.8.26",
+        "Token0": "solc-0.8.26",
+        "ERC20Helper": "solc-0.8.26"
+    },
+    "solc_optimize": "200",
+    "process": "emv",
+    "build_cache": true,
+    "smt_timeout": "6000",
+    "solc_via_ir_map": {
+		"ERC20Helper": false,
+		"EthereumVaultConnector": false,
+		"EulerEarnFactory": false,
+		"EulerEarnHarness": false,
+		"IRMLinearKink": false,
+		"Permit2": true,
+		"PerspectiveMock": false,
+		"Token0": false,
+		"VaultMock0": false,
+		"VaultMock1": false
+	},
 }

certora/harnesses/ERC20Helper.sol

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity 0.8.26;
 
-import {SafeERC20, IERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/utils/SafeERC20.sol";
+import {SafeERC20, IERC20} from "openzeppelin-contracts/token/ERC20/utils/SafeERC20.sol";
 
 contract ERC20Helper {
     using SafeERC20 for IERC20;

certora/mocks/Token0.sol

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: MIT
 pragma solidity >=0.8.21;
 
-import {ERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol";
+import {ERC20} from "openzeppelin-contracts/token/ERC20/ERC20.sol";
 
 contract Token0 is ERC20 {
    constructor() ERC20("Token0", "TOK0") {}

certora/mocks/VaultMock0.sol

@@ -7,7 +7,7 @@ import {
     ERC20,
     ERC4626,
     Math
-} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC4626.sol";
+} from "openzeppelin-contracts/token/ERC20/extensions/ERC4626.sol";
 
 contract VaultMock0 is ERC4626 {
    constructor(IERC20 asset) ERC4626(asset) ERC20("VaultMock0", "V0") {}

certora/mocks/VaultMock1.sol

@@ -7,7 +7,7 @@ import {
     ERC20,
     ERC4626,
     Math
-} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC4626.sol";
+} from "openzeppelin-contracts/token/ERC20/extensions/ERC4626.sol";
 
 contract VaultMock1 is ERC4626 {
    constructor(IERC20 asset) ERC4626(asset) ERC20("VaultMock1", "V1") {}

certora/scripts/EulerEarn.patch

@@ -1,8 +1,8 @@
 diff --git a/src/EulerEarn.sol b/src/EulerEarn.sol
-index 4635a89..ae0869b 100644
+index 27c1873..1efc278 100644
 --- a/src/EulerEarn.sol
 +++ b/src/EulerEarn.sol
-@@ -106,6 +106,18 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -106,6 +106,17 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
      /// @dev "Overrides" the ERC20's storage variable to be able to modify it.
      string private _symbol;
 
@@ -14,14 +14,13 @@ index 4635a89..ae0869b 100644
 +    // The last index at which a market identifier has been removed from the withdraw queue.
 +    mapping(address => uint256) public deletedAt;
 +
-+    // hooks for cvl assertions
 +    function HOOK_after_accrueInterest() internal {}
 +    function HOOK_after_withdrawStrategy(uint256) internal {}
 +
      /* CONSTRUCTOR */
 
      /// @dev Initializes the contract.
-@@ -353,6 +365,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -353,6 +364,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
              seen[prevIndex] = true;
 
              newWithdrawQueue[i] = id;
@@ -31,7 +30,7 @@ index 4635a89..ae0869b 100644
          }
 
          for (uint256 i; i < currLength; ++i) {
-@@ -369,6 +384,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -369,6 +383,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
                          revert ErrorsLib.InvalidMarketRemovalTimelockNotElapsed(id);
                      }
                  }
@@ -41,39 +40,39 @@ index 4635a89..ae0869b 100644
 
                  delete config[id];
              }
-@@ -559,6 +577,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -559,6 +576,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
      /// @inheritdoc IERC4626
      function deposit(uint256 assets, address receiver) public override nonReentrant returns (uint256 shares) {
          _accrueInterest();
 +        HOOK_after_accrueInterest();
 
          shares = _convertToSharesWithTotals(assets, totalSupply(), lastTotalAssets, Math.Rounding.Floor);
 
-@@ -570,6 +589,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -570,6 +588,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
      /// @inheritdoc IERC4626
      function mint(uint256 shares, address receiver) public override nonReentrant returns (uint256 assets) {
          _accrueInterest();
 +        HOOK_after_accrueInterest();
 
          assets = _convertToAssetsWithTotals(shares, totalSupply(), lastTotalAssets, Math.Rounding.Ceil);
 
-@@ -584,6 +604,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -584,6 +603,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
          returns (uint256 shares)
      {
          _accrueInterest();
 +        HOOK_after_accrueInterest();
 
          // Do not call expensive `maxWithdraw` and optimistically withdraw assets.
 
-@@ -600,6 +621,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -600,6 +620,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
          returns (uint256 assets)
      {
          _accrueInterest();
 +        HOOK_after_accrueInterest();
 
          // Do not call expensive `maxRedeem` and optimistically redeem shares.
 
-@@ -729,7 +751,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -729,7 +750,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
          // clamp at 0 so the error raised is the more informative NotEnoughLiquidity.
          _updateLastTotalAssets(lastTotalAssets.zeroFloorSub(assets));
 
@@ -83,7 +82,7 @@ index 4635a89..ae0869b 100644
 
          super._withdraw(caller, receiver, owner, assets, shares);
      }
-@@ -780,6 +804,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -780,6 +803,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
              IERC20(asset()).forceApproveMaxWithPermit2(address(id), permit2);
 
              if (!marketConfig.enabled) {
@@ -93,7 +92,7 @@ index 4635a89..ae0869b 100644
                  withdrawQueue.push(id);
 
                  if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded();
-@@ -837,6 +864,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
+@@ -837,6 +863,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar
      /// @dev Withdraws `assets` from the strategy vaults.
      function _withdrawStrategy(uint256 assets) internal {
          for (uint256 i; i < withdrawQueue.length; ++i) {

remappings.txt

@@ -1 +1,2 @@
+openzeppelin-contracts/=lib/openzeppelin-contracts/contracts/
 ethereum-vault-connector/=lib/ethereum-vault-connector/src/

src/EulerEarn.sol

@@ -17,21 +17,21 @@ import {ErrorsLib} from "./libraries/ErrorsLib.sol";
 import {EventsLib} from "./libraries/EventsLib.sol";
 import {SafeERC20Permit2Lib} from "./libraries/SafeERC20Permit2Lib.sol";
 import {UtilsLib, WAD} from "./libraries/UtilsLib.sol";
-import {SafeCast} from "../lib/openzeppelin-contracts/contracts/utils/math/SafeCast.sol";
-import {IERC20Metadata} from "../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Metadata.sol";
+import {SafeCast} from "openzeppelin-contracts/utils/math/SafeCast.sol";
+import {IERC20Metadata} from "openzeppelin-contracts/token/ERC20/extensions/IERC20Metadata.sol";
 
-import {Context} from "../lib/openzeppelin-contracts/contracts/utils/Context.sol";
-import {ReentrancyGuard} from "../lib/openzeppelin-contracts/contracts/utils/ReentrancyGuard.sol";
-import {Ownable2Step, Ownable} from "../lib/openzeppelin-contracts/contracts/access/Ownable2Step.sol";
+import {Context} from "openzeppelin-contracts/utils/Context.sol";
+import {ReentrancyGuard} from "openzeppelin-contracts/utils/ReentrancyGuard.sol";
+import {Ownable2Step, Ownable} from "openzeppelin-contracts/access/Ownable2Step.sol";
 import {
     IERC20,
     IERC4626,
     ERC20,
     ERC4626,
     Math,
     SafeERC20
-} from "../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/ERC4626.sol";
-import {EVCUtil} from "../lib/ethereum-vault-connector/src/utils/EVCUtil.sol";
+} from "openzeppelin-contracts/token/ERC20/extensions/ERC4626.sol";
+import {EVCUtil} from "ethereum-vault-connector/utils/EVCUtil.sol";
 
 /// @title EulerEarn
 /// @author Forked with gratitude from Morpho Labs. Inspired by Silo Labs.

src/EulerEarnFactory.sol

@@ -10,8 +10,8 @@ import {ErrorsLib} from "./libraries/ErrorsLib.sol";
 
 import {EulerEarn} from "./EulerEarn.sol";
 
-import {Ownable, Context} from "../lib/openzeppelin-contracts/contracts/access/Ownable.sol";
-import {EVCUtil} from "../lib/ethereum-vault-connector/src/utils/EVCUtil.sol";
+import {Ownable, Context} from "openzeppelin-contracts/access/Ownable.sol";
+import {EVCUtil} from "ethereum-vault-connector/utils/EVCUtil.sol";
 
 /// @title EulerEarnFactory
 /// @author Forked with gratitude from Morpho Labs. Inspired by Silo Labs.

src/PublicAllocator.sol

@@ -14,8 +14,8 @@ import {IEulerEarn, MarketAllocation} from "./interfaces/IEulerEarn.sol";
 import {ErrorsLib} from "./libraries/ErrorsLib.sol";
 import {EventsLib} from "./libraries/EventsLib.sol";
 
-import {IERC4626} from "../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
-import {EVCUtil} from "../lib/ethereum-vault-connector/src/utils/EVCUtil.sol";
+import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol";
+import {EVCUtil} from "ethereum-vault-connector/utils/EVCUtil.sol";
 
 /// @title PublicAllocator
 /// @author Forked with gratitude from Morpho Labs. Inspired by Silo Labs.

src/interfaces/IEulerEarn.sol

@@ -3,8 +3,8 @@ pragma solidity >=0.5.0;
 
 import {IEulerEarnFactory} from "./IEulerEarnFactory.sol";
 
-import {IERC4626} from "../../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
-import {IERC20Permit} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/extensions/IERC20Permit.sol";
+import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol";
+import {IERC20Permit} from "openzeppelin-contracts/token/ERC20/extensions/IERC20Permit.sol";
 
 import {MarketConfig, PendingUint136, PendingAddress} from "../libraries/PendingLib.sol";
 

src/interfaces/IPublicAllocator.sol

@@ -3,7 +3,7 @@ pragma solidity >=0.5.0;
 
 import {MarketAllocation} from "./IEulerEarn.sol";
 
-import {IERC4626} from "../../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
+import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol";
 
 /// @dev Max settable flow cap, such that caps can always be stored on 128 bits.
 /// @dev The actual max possible flow cap is type(uint128).max-1.

src/libraries/ErrorsLib.sol

@@ -1,7 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 pragma solidity ^0.8.0;
 
-import {IERC4626} from "../../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
+import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol";
 
 /// @title ErrorsLib
 /// @author Forked with gratitude from Morpho Labs. Inspired by Silo Labs.

src/libraries/EventsLib.sol

@@ -3,7 +3,7 @@ pragma solidity ^0.8.0;
 
 import {FlowCapsConfig} from "../interfaces/IPublicAllocator.sol";
 
-import {IERC4626} from "../../lib/openzeppelin-contracts/contracts/interfaces/IERC4626.sol";
+import {IERC4626} from "openzeppelin-contracts/interfaces/IERC4626.sol";
 
 import {PendingAddress} from "./PendingLib.sol";
 

src/libraries/SafeERC20Permit2Lib.sol

@@ -3,8 +3,8 @@
 pragma solidity ^0.8.0;
 
 import {IAllowanceTransfer} from "../interfaces/IAllowanceTransfer.sol";
-import {IERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol";
-import {SafeERC20} from "../../lib/openzeppelin-contracts/contracts/token/ERC20/utils/SafeERC20.sol";
+import {IERC20} from "openzeppelin-contracts/token/ERC20/ERC20.sol";
+import {SafeERC20} from "openzeppelin-contracts/token/ERC20/utils/SafeERC20.sol";
 
 /// @title SafeERC20Permit2Lib Library
 /// @custom:security-contact [email protected]

test/ERC4626Test.sol

@@ -531,7 +531,7 @@ contract ERC4626Test is IntegrationTest {
 
         // max deposit is 0
         assertEq(vault.maxDeposit(SUPPLIER), 0);
-        // although cap still allows 1 wei 
+        // although cap still allows 1 wei
         assertEq(vault.totalAssets(), cap - 1);
         // because depositing 1 wei would throw zero shares
         vm.prank(SUPPLIER);