From bece7172a87551e6943a52b08c9a0117eb02c6c3 Mon Sep 17 00:00:00 2001 From: kasperpawlowski Date: Tue, 14 Oct 2025 19:22:54 +0200 Subject: [PATCH 01/10] fix: absolute import paths --- remappings.txt | 1 + src/EulerEarn.sol | 14 +++++++------- src/EulerEarnFactory.sol | 4 ++-- src/PublicAllocator.sol | 4 ++-- src/interfaces/IEulerEarn.sol | 4 ++-- src/interfaces/IPublicAllocator.sol | 2 +- src/libraries/ErrorsLib.sol | 2 +- src/libraries/EventsLib.sol | 2 +- src/libraries/SafeERC20Permit2Lib.sol | 4 ++-- test/ERC4626Test.sol | 2 +- 10 files changed, 20 insertions(+), 19 deletions(-) diff --git a/remappings.txt b/remappings.txt index b6b08e5..f9e164d 100644 --- a/remappings.txt +++ b/remappings.txt @@ -1 +1,2 @@ +openzeppelin-contracts/=lib/openzeppelin-contracts/contracts/ ethereum-vault-connector/=lib/ethereum-vault-connector/src/ \ No newline at end of file diff --git a/src/EulerEarn.sol b/src/EulerEarn.sol index 4635a89..27c1873 100644 --- a/src/EulerEarn.sol +++ b/src/EulerEarn.sol @@ -17,12 +17,12 @@ 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, @@ -30,8 +30,8 @@ import { 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. diff --git a/src/EulerEarnFactory.sol b/src/EulerEarnFactory.sol index 758185e..e7fd335 100644 --- a/src/EulerEarnFactory.sol +++ b/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. diff --git a/src/PublicAllocator.sol b/src/PublicAllocator.sol index f71306c..9527976 100644 --- a/src/PublicAllocator.sol +++ b/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. diff --git a/src/interfaces/IEulerEarn.sol b/src/interfaces/IEulerEarn.sol index 27334f2..ed18e7e 100644 --- a/src/interfaces/IEulerEarn.sol +++ b/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"; diff --git a/src/interfaces/IPublicAllocator.sol b/src/interfaces/IPublicAllocator.sol index b222ce3..4a9067b 100644 --- a/src/interfaces/IPublicAllocator.sol +++ b/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. diff --git a/src/libraries/ErrorsLib.sol b/src/libraries/ErrorsLib.sol index 300bb22..da0feca 100644 --- a/src/libraries/ErrorsLib.sol +++ b/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. diff --git a/src/libraries/EventsLib.sol b/src/libraries/EventsLib.sol index f9dc967..862b344 100644 --- a/src/libraries/EventsLib.sol +++ b/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"; diff --git a/src/libraries/SafeERC20Permit2Lib.sol b/src/libraries/SafeERC20Permit2Lib.sol index 59603da..0e633eb 100644 --- a/src/libraries/SafeERC20Permit2Lib.sol +++ b/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 security@euler.xyz diff --git a/test/ERC4626Test.sol b/test/ERC4626Test.sol index d1a5576..bbc3929 100644 --- a/test/ERC4626Test.sol +++ b/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); From eab4f77553a00168e3ce50432c21d22b553f4ac0 Mon Sep 17 00:00:00 2001 From: kasperpawlowski Date: Tue, 14 Oct 2025 19:35:03 +0200 Subject: [PATCH 02/10] fix: import paths --- certora/harnesses/ERC20Helper.sol | 2 +- certora/mocks/Token0.sol | 2 +- certora/mocks/VaultMock0.sol | 2 +- certora/mocks/VaultMock1.sol | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/harnesses/ERC20Helper.sol b/certora/harnesses/ERC20Helper.sol index 0f8e5e2..d4f0dc8 100644 --- a/certora/harnesses/ERC20Helper.sol +++ b/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; diff --git a/certora/mocks/Token0.sol b/certora/mocks/Token0.sol index bbe2679..ab760ef 100644 --- a/certora/mocks/Token0.sol +++ b/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") {} diff --git a/certora/mocks/VaultMock0.sol b/certora/mocks/VaultMock0.sol index 604c182..49705cb 100644 --- a/certora/mocks/VaultMock0.sol +++ b/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") {} diff --git a/certora/mocks/VaultMock1.sol b/certora/mocks/VaultMock1.sol index 119de7c..0cbfc46 100644 --- a/certora/mocks/VaultMock1.sol +++ b/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") {} From 62c71fdcbf441095c0b5a8d4d3a5f4893a374ee5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Antti=20Hyv=C3=A4rinen?= Date: Wed, 15 Oct 2025 10:50:40 +0200 Subject: [PATCH 03/10] Remove packages key from certora confs --- .github/workflows/certora-prover.yml | 4 ++++ certora/confs/BaseConfForInheritance.conf | 6 ------ 2 files changed, 4 insertions(+), 6 deletions(-) diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml index 8f381bd..a2eb3e8 100644 --- a/.github/workflows/certora-prover.yml +++ b/.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 diff --git a/certora/confs/BaseConfForInheritance.conf b/certora/confs/BaseConfForInheritance.conf index 0b35728..27ba6b8 100644 --- a/certora/confs/BaseConfForInheritance.conf +++ b/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", From aeef1e459351735d2e18cf1f6217d3144567e5a0 Mon Sep 17 00:00:00 2001 From: raz-certora Date: Sun, 19 Oct 2025 19:14:30 +0300 Subject: [PATCH 04/10] patch change - hope to resolve summary error. --- certora/scripts/EulerEarn.patch | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/certora/scripts/EulerEarn.patch b/certora/scripts/EulerEarn.patch index 7fe001a..84be2d7 100644 --- a/certora/scripts/EulerEarn.patch +++ b/certora/scripts/EulerEarn.patch @@ -1,8 +1,8 @@ diff --git a/src/EulerEarn.sol b/src/EulerEarn.sol -index 4635a89..ae0869b 100644 +index 27c1873..9e0c019 100644 --- a/src/EulerEarn.sol +++ b/src/EulerEarn.sol -@@ -106,6 +106,18 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -106,6 +106,23 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar /// @dev "Overrides" the ERC20's storage variable to be able to modify it. string private _symbol; @@ -15,13 +15,18 @@ index 4635a89..ae0869b 100644 + mapping(address => uint256) public deletedAt; + + // hooks for cvl assertions -+ function HOOK_after_accrueInterest() internal {} -+ function HOOK_after_withdrawStrategy(uint256) internal {} ++ bool _for_hooks; ++ function HOOK_after_accrueInterest() internal { ++ _for_hooks = true; ++ } ++ function HOOK_after_withdrawStrategy(uint256) internal { ++ _for_hooks = true; ++ } + /* CONSTRUCTOR */ /// @dev Initializes the contract. -@@ -353,6 +365,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -353,6 +370,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar seen[prevIndex] = true; newWithdrawQueue[i] = id; @@ -31,7 +36,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 +389,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar revert ErrorsLib.InvalidMarketRemovalTimelockNotElapsed(id); } } @@ -41,7 +46,7 @@ index 4635a89..ae0869b 100644 delete config[id]; } -@@ -559,6 +577,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -559,6 +582,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar /// @inheritdoc IERC4626 function deposit(uint256 assets, address receiver) public override nonReentrant returns (uint256 shares) { _accrueInterest(); @@ -49,7 +54,7 @@ index 4635a89..ae0869b 100644 shares = _convertToSharesWithTotals(assets, totalSupply(), lastTotalAssets, Math.Rounding.Floor); -@@ -570,6 +589,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -570,6 +594,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar /// @inheritdoc IERC4626 function mint(uint256 shares, address receiver) public override nonReentrant returns (uint256 assets) { _accrueInterest(); @@ -57,7 +62,7 @@ index 4635a89..ae0869b 100644 assets = _convertToAssetsWithTotals(shares, totalSupply(), lastTotalAssets, Math.Rounding.Ceil); -@@ -584,6 +604,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -584,6 +609,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar returns (uint256 shares) { _accrueInterest(); @@ -65,7 +70,7 @@ index 4635a89..ae0869b 100644 // Do not call expensive `maxWithdraw` and optimistically withdraw assets. -@@ -600,6 +621,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -600,6 +626,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar returns (uint256 assets) { _accrueInterest(); @@ -73,7 +78,7 @@ index 4635a89..ae0869b 100644 // Do not call expensive `maxRedeem` and optimistically redeem shares. -@@ -729,7 +751,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -729,7 +756,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 +88,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 +809,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar IERC20(asset()).forceApproveMaxWithPermit2(address(id), permit2); if (!marketConfig.enabled) { @@ -93,7 +98,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 +869,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) { From 1d66e84c46248a6d09d06152677efc9b47269429 Mon Sep 17 00:00:00 2001 From: raz-certora Date: Sun, 19 Oct 2025 19:55:32 +0300 Subject: [PATCH 05/10] different attempt to fix summary problem, with assembly code. --- certora/scripts/EulerEarn.patch | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/certora/scripts/EulerEarn.patch b/certora/scripts/EulerEarn.patch index 84be2d7..a4ba55a 100644 --- a/certora/scripts/EulerEarn.patch +++ b/certora/scripts/EulerEarn.patch @@ -1,8 +1,8 @@ diff --git a/src/EulerEarn.sol b/src/EulerEarn.sol -index 27c1873..9e0c019 100644 +index 27c1873..482c657 100644 --- a/src/EulerEarn.sol +++ b/src/EulerEarn.sol -@@ -106,6 +106,23 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -106,6 +106,25 @@ 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,19 +14,21 @@ index 27c1873..9e0c019 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 -+ bool _for_hooks; + function HOOK_after_accrueInterest() internal { -+ _for_hooks = true; ++ assembly { ++ let temp := timestamp() ++ } + } + function HOOK_after_withdrawStrategy(uint256) internal { -+ _for_hooks = true; ++ assembly { ++ let temp := timestamp() ++ } + } + /* CONSTRUCTOR */ /// @dev Initializes the contract. -@@ -353,6 +370,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -353,6 +372,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar seen[prevIndex] = true; newWithdrawQueue[i] = id; @@ -36,7 +38,7 @@ index 27c1873..9e0c019 100644 } for (uint256 i; i < currLength; ++i) { -@@ -369,6 +389,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -369,6 +391,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar revert ErrorsLib.InvalidMarketRemovalTimelockNotElapsed(id); } } @@ -46,7 +48,7 @@ index 27c1873..9e0c019 100644 delete config[id]; } -@@ -559,6 +582,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -559,6 +584,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar /// @inheritdoc IERC4626 function deposit(uint256 assets, address receiver) public override nonReentrant returns (uint256 shares) { _accrueInterest(); @@ -54,7 +56,7 @@ index 27c1873..9e0c019 100644 shares = _convertToSharesWithTotals(assets, totalSupply(), lastTotalAssets, Math.Rounding.Floor); -@@ -570,6 +594,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -570,6 +596,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar /// @inheritdoc IERC4626 function mint(uint256 shares, address receiver) public override nonReentrant returns (uint256 assets) { _accrueInterest(); @@ -62,7 +64,7 @@ index 27c1873..9e0c019 100644 assets = _convertToAssetsWithTotals(shares, totalSupply(), lastTotalAssets, Math.Rounding.Ceil); -@@ -584,6 +609,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -584,6 +611,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar returns (uint256 shares) { _accrueInterest(); @@ -70,7 +72,7 @@ index 27c1873..9e0c019 100644 // Do not call expensive `maxWithdraw` and optimistically withdraw assets. -@@ -600,6 +626,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -600,6 +628,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar returns (uint256 assets) { _accrueInterest(); @@ -78,7 +80,7 @@ index 27c1873..9e0c019 100644 // Do not call expensive `maxRedeem` and optimistically redeem shares. -@@ -729,7 +756,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -729,7 +758,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)); @@ -88,7 +90,7 @@ index 27c1873..9e0c019 100644 super._withdraw(caller, receiver, owner, assets, shares); } -@@ -780,6 +809,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -780,6 +811,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar IERC20(asset()).forceApproveMaxWithPermit2(address(id), permit2); if (!marketConfig.enabled) { @@ -98,7 +100,7 @@ index 27c1873..9e0c019 100644 withdrawQueue.push(id); if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded(); -@@ -837,6 +869,9 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar +@@ -837,6 +871,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) { From 1afa464363438c4545fc3cd2193ff82bd7199e58 Mon Sep 17 00:00:00 2001 From: raz-certora Date: Sun, 19 Oct 2025 20:44:23 +0300 Subject: [PATCH 06/10] different fix for summary issue: change back the patch to functions that don't do anything, but change conf arguments solc_via_ir_map --- certora/confs/BaseConfForInheritance.conf | 13 ++++++++- certora/scripts/EulerEarn.patch | 34 +++++++++-------------- 2 files changed, 25 insertions(+), 22 deletions(-) diff --git a/certora/confs/BaseConfForInheritance.conf b/certora/confs/BaseConfForInheritance.conf index 27ba6b8..bcc2d7a 100644 --- a/certora/confs/BaseConfForInheritance.conf +++ b/certora/confs/BaseConfForInheritance.conf @@ -36,7 +36,18 @@ "ERC20Helper": "solc-0.8.26" }, "solc_optimize": "200", - "solc_via_ir": true, + "solc_via_ir_map": { + "ERC20Helper": false, + "EthereumVaultConnector": false, + "EulerEarnFactory": false, + "EulerEarnHarness": false, + "IRMLinearKink": false, + "Permit2": true, + "PerspectiveMock": false, + "Token0": false, + "VaultMock0": false, + "VaultMock1": false + }, "assert_autofinder_success": true, "contract_recursion_limit": "1", "process": "emv", diff --git a/certora/scripts/EulerEarn.patch b/certora/scripts/EulerEarn.patch index a4ba55a..a8a934e 100644 --- a/certora/scripts/EulerEarn.patch +++ b/certora/scripts/EulerEarn.patch @@ -1,8 +1,8 @@ diff --git a/src/EulerEarn.sol b/src/EulerEarn.sol -index 27c1873..482c657 100644 +index 27c1873..1efc278 100644 --- a/src/EulerEarn.sol +++ b/src/EulerEarn.sol -@@ -106,6 +106,25 @@ 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,21 +14,13 @@ index 27c1873..482c657 100644 + // The last index at which a market identifier has been removed from the withdraw queue. + mapping(address => uint256) public deletedAt; + -+ function HOOK_after_accrueInterest() internal { -+ assembly { -+ let temp := timestamp() -+ } -+ } -+ function HOOK_after_withdrawStrategy(uint256) internal { -+ assembly { -+ let temp := timestamp() -+ } -+ } ++ function HOOK_after_accrueInterest() internal {} ++ function HOOK_after_withdrawStrategy(uint256) internal {} + /* CONSTRUCTOR */ /// @dev Initializes the contract. -@@ -353,6 +372,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; @@ -38,7 +30,7 @@ index 27c1873..482c657 100644 } for (uint256 i; i < currLength; ++i) { -@@ -369,6 +391,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); } } @@ -48,7 +40,7 @@ index 27c1873..482c657 100644 delete config[id]; } -@@ -559,6 +584,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(); @@ -56,7 +48,7 @@ index 27c1873..482c657 100644 shares = _convertToSharesWithTotals(assets, totalSupply(), lastTotalAssets, Math.Rounding.Floor); -@@ -570,6 +596,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(); @@ -64,7 +56,7 @@ index 27c1873..482c657 100644 assets = _convertToAssetsWithTotals(shares, totalSupply(), lastTotalAssets, Math.Rounding.Ceil); -@@ -584,6 +611,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(); @@ -72,7 +64,7 @@ index 27c1873..482c657 100644 // Do not call expensive `maxWithdraw` and optimistically withdraw assets. -@@ -600,6 +628,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(); @@ -80,7 +72,7 @@ index 27c1873..482c657 100644 // Do not call expensive `maxRedeem` and optimistically redeem shares. -@@ -729,7 +758,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)); @@ -90,7 +82,7 @@ index 27c1873..482c657 100644 super._withdraw(caller, receiver, owner, assets, shares); } -@@ -780,6 +811,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) { @@ -100,7 +92,7 @@ index 27c1873..482c657 100644 withdrawQueue.push(id); if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded(); -@@ -837,6 +871,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) { From 377b14f3fcb410b0cd29336f31cd06dc44da1b4c Mon Sep 17 00:00:00 2001 From: raz-certora Date: Sun, 19 Oct 2025 20:58:07 +0300 Subject: [PATCH 07/10] remove assert_auto_finder_success --- certora/confs/BaseConfForInheritance.conf | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/confs/BaseConfForInheritance.conf b/certora/confs/BaseConfForInheritance.conf index bcc2d7a..c1a21b6 100644 --- a/certora/confs/BaseConfForInheritance.conf +++ b/certora/confs/BaseConfForInheritance.conf @@ -48,7 +48,6 @@ "VaultMock0": false, "VaultMock1": false }, - "assert_autofinder_success": true, "contract_recursion_limit": "1", "process": "emv", "prover_args": [ From dafb63b4ca6ea8ce886523e5f3cd05bf30945757 Mon Sep 17 00:00:00 2001 From: raz-certora Date: Sun, 19 Oct 2025 21:37:55 +0300 Subject: [PATCH 08/10] revert change to BaseConf, and specific conf for SolvencyInternal. --- certora/confs/BaseConfForInheritance.conf | 14 +----- certora/confs/SolvencyInternal.conf | 53 ++++++++++++++++++++++- 2 files changed, 54 insertions(+), 13 deletions(-) diff --git a/certora/confs/BaseConfForInheritance.conf b/certora/confs/BaseConfForInheritance.conf index c1a21b6..27ba6b8 100644 --- a/certora/confs/BaseConfForInheritance.conf +++ b/certora/confs/BaseConfForInheritance.conf @@ -36,18 +36,8 @@ "ERC20Helper": "solc-0.8.26" }, "solc_optimize": "200", - "solc_via_ir_map": { - "ERC20Helper": false, - "EthereumVaultConnector": false, - "EulerEarnFactory": false, - "EulerEarnHarness": false, - "IRMLinearKink": false, - "Permit2": true, - "PerspectiveMock": false, - "Token0": false, - "VaultMock0": false, - "VaultMock1": false - }, + "solc_via_ir": true, + "assert_autofinder_success": true, "contract_recursion_limit": "1", "process": "emv", "prover_args": [ diff --git a/certora/confs/SolvencyInternal.conf b/certora/confs/SolvencyInternal.conf index 359aeb1..79f7de8 100644 --- a/certora/confs/SolvencyInternal.conf +++ b/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 + }, } From 3ee6ecc6d1ba1bac60987b6809873520c6fe57de Mon Sep 17 00:00:00 2001 From: raz-certora Date: Mon, 20 Oct 2025 11:09:39 +0300 Subject: [PATCH 09/10] A removed optimization in Solvency.conf to prevent the initial case bug. --- certora/confs/Solvency.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/Solvency.conf b/certora/confs/Solvency.conf index e2d1f48..20334f1 100644 --- a/certora/confs/Solvency.conf +++ b/certora/confs/Solvency.conf @@ -12,5 +12,6 @@ "-cvlFunctionRevert true", "-depth 0" ], + "-disabledTransformations OPTIMIZE_INFEASIBLE_PATHS", "override_base_config": "certora/confs/BaseConfForInheritance.conf" } From 5a0283526c110c82ad676a1e6d83274e71dfde83 Mon Sep 17 00:00:00 2001 From: raz-certora Date: Mon, 20 Oct 2025 11:35:45 +0300 Subject: [PATCH 10/10] fix conf --- certora/confs/Solvency.conf | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/certora/confs/Solvency.conf b/certora/confs/Solvency.conf index 20334f1..f117e91 100644 --- a/certora/confs/Solvency.conf +++ b/certora/confs/Solvency.conf @@ -10,8 +10,8 @@ "process": "emv", "prover_args": [ "-cvlFunctionRevert true", - "-depth 0" + "-depth 0", + "-disabledTransformations OPTIMIZE_INFEASIBLE_PATHS", ], - "-disabledTransformations OPTIMIZE_INFEASIBLE_PATHS", "override_base_config": "certora/confs/BaseConfForInheritance.conf" }