Skip to content

Ensure that internal function summary gets applied #7

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: fix-import-paths
Choose a base branch
from
Open

Ensure that internal function summary gets applied #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion certora/confs/Solvency.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
}
53 changes: 52 additions & 1 deletion certora/confs/SolvencyInternal.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
},
}
23 changes: 11 additions & 12 deletions certora/scripts/EulerEarn.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;

Expand All @@ -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;
Expand All @@ -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);
}
}
Expand All @@ -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));

Expand All @@ -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) {
Expand All @@ -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) {
Expand Down