Ensure that internal function summary gets applied

certora/confs/BaseConfForInheritance.conf

@@ -1,4 +1,5 @@
 {
+    "prover_version": "johannes/CERT-9671",
     "optimistic_loop": true,
     "global_timeout": "7200",
     "parametric_contracts": "EulerEarnHarness",

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/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"
+}

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) {

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; 

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);