From 0d2fa193da138766ca8e46ab0be8a11a7ef44f75 Mon Sep 17 00:00:00 2001 From: raz-certora Date: Sun, 19 Oct 2025 19:14:30 +0300 Subject: [PATCH 1/2] Ensure that internal function summary gets applied --- certora/confs/Solvency.conf | 3 +- certora/confs/SolvencyInternal.conf | 53 ++++++++++++++++++++++++++++- certora/scripts/EulerEarn.patch | 23 ++++++------- 3 files changed, 65 insertions(+), 14 deletions(-) diff --git a/certora/confs/Solvency.conf b/certora/confs/Solvency.conf index e2d1f48..f117e91 100644 --- a/certora/confs/Solvency.conf +++ b/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" } 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 + }, } diff --git a/certora/scripts/EulerEarn.patch b/certora/scripts/EulerEarn.patch index 7fe001a..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 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,7 +40,7 @@ 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(); @@ -49,7 +48,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 +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(); @@ -57,7 +56,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 +603,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar returns (uint256 shares) { _accrueInterest(); @@ -65,7 +64,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 +620,7 @@ contract EulerEarn is ReentrancyGuard, ERC4626, Ownable2Step, EVCUtil, IEulerEar returns (uint256 assets) { _accrueInterest(); @@ -73,7 +72,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 +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) { From 0231eabcdf922f31a4dc0e53d62b2799a0afa5c8 Mon Sep 17 00:00:00 2001 From: raz-certora Date: Mon, 17 Nov 2025 17:30:22 +0200 Subject: [PATCH 2/2] fix of rules for CERT-9671 change. Currently this does not affect the run on the current prover version. but it will prevent spurious violations after the changes in CERT-9671 are pushed. --- certora/confs/BaseConfForInheritance.conf | 1 + certora/confs/constructor_tests.conf | 10 ++++++++++ certora/specs/ConsistentState.spec | 14 ++++++++++++++ certora/specs/EulerEarnERC4626.spec | 13 ++++++++++++- 4 files changed, 37 insertions(+), 1 deletion(-) create mode 100644 certora/confs/constructor_tests.conf diff --git a/certora/confs/BaseConfForInheritance.conf b/certora/confs/BaseConfForInheritance.conf index 27ba6b8..5237abc 100644 --- a/certora/confs/BaseConfForInheritance.conf +++ b/certora/confs/BaseConfForInheritance.conf @@ -1,4 +1,5 @@ { + "prover_version": "johannes/CERT-9671", "optimistic_loop": true, "global_timeout": "7200", "parametric_contracts": "EulerEarnHarness", diff --git a/certora/confs/constructor_tests.conf b/certora/confs/constructor_tests.conf new file mode 100644 index 0000000..3715928 --- /dev/null +++ b/certora/confs/constructor_tests.conf @@ -0,0 +1,10 @@ +{ + "verify": "EulerEarnHarness:certora/specs/EulerEarnERC4626.spec", + "msg": "ERC4626-style properties and helper properties", + "rule": [ + "noAssetsOnEuler", + ], + "loop_iter": "1", + "optimistic_summary_recursion": true, + "override_base_config": "certora/confs/BaseConfForInheritance.conf" +} diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index ee2f0a6..f59b2de 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -13,6 +13,8 @@ methods { function curator() external returns(address) envfree; function isAllocator(address target) external returns(bool) envfree; function permit2Address() external returns address envfree; + function Token0.balanceOf(address) external returns uint256 envfree; + function Token0.allowance(address, address) external returns uint256 envfree; } function hasCuratorRole(address user) returns bool { @@ -98,9 +100,18 @@ rule newSupplyQueueEnsuresPositiveCap(env e, address[] newSupplyQueue) //The following two rules are from TokenApproval.spec in Silo and caught bugs in Silo. +function constructor_token_assumptions(address user) { + require Token0.balanceOf(currentContract)==0, "at initialization the contract address doesn't have a balance in Token0"; + require Token0.allowance(currentContract,user)==0, "at initialization the contract address hasn't given an allowance in Token0"; + require Token0.allowance(user,currentContract)==0, "at initialization the contract address hasn't received an allowance in Token0"; +} + invariant noCapThenNoApproval(address market) config_(market).cap == 0 => ERC20Helper.allowance(asset(), currentContract, market) == 0 { + preserved constructor() with (env e) { + constructor_token_assumptions(market); + } preserved acceptCap(address id) with (env e) { // not sure all of these assumptions are necessary but all are legitimate. require market != permit2Address(); @@ -134,6 +145,9 @@ invariant noCapThenNoApproval(address market) invariant notInWithdrawQThenNoApproval(address market) withdrawRank(market) == 0 => ERC20Helper.allowance(asset(), currentContract, market) == 0 { + preserved constructor() with (env e) { + constructor_token_assumptions(market); + } preserved with (env e) { require market != permit2Address(); require msgSender(e) != currentContract; diff --git a/certora/specs/EulerEarnERC4626.spec b/certora/specs/EulerEarnERC4626.spec index 2cc1409..467186c 100644 --- a/certora/specs/EulerEarnERC4626.spec +++ b/certora/specs/EulerEarnERC4626.spec @@ -103,6 +103,11 @@ hook Sload uint256 val _balances[KEY address addy] { invariant totalSupplyIsSumOfBalances() totalSupply() == sumOfBalances; +function constructor_token_assumptions(address user) { + require Token0.balanceOf(currentContract)==0, "at initialization the contract address doesn't have a balance in Token0"; + require Token0.allowance(currentContract,user)==0, "at initialization the contract address hasn't given an allowance in Token0"; + require Token0.allowance(user,currentContract)==0, "at initialization the contract address hasn't received an allowance in Token0"; +} // Verified invariant noAssetsOnEuler() @@ -118,6 +123,9 @@ invariant noAssetsOnEuler() require owner != currentContract; safeAssumptions(e); } + preserved constructor() with (env e) { + constructor_token_assumptions(currentContract); + } preserved with (env e) { safeAssumptions(e); } @@ -201,8 +209,11 @@ rule redeemingAllValidity() { // Verified https://prover.certora.com/output/5771024/fdeec6302e9b429bb0b725f3d9fd22fe invariant zeroAllowanceOnAssets(address user) - // no alloownaces from current contract. + // no allowances from current contract. Token0.allowance(currentContract, user) == 0 && currentContract.allowance(currentContract, user) == 0 { + preserved constructor() with (env e) { + constructor_token_assumptions(user); + } preserved with(env e) { require msgSender(e) != currentContract; safeAssumptions(e);