feat: stata token v2 (#52)

* feat: Add rescuable to static a token (#29)

* feat: Add rescuable to static a token

* Update src/periphery/contracts/static-a-token/StaticATokenLM.sol

---------

Co-authored-by: Lukas <[email protected]>

* fix: combine interface (#33)

* Update METADEPOSIT_TYPEHASH (#44)

* Update METADEPOSIT_TYPEHASH

* cleanup of MetaDepositParams

* feat: pausability (#45)

* feat: expose latest answer on static a token (#3)

* fix: add readme

* docs: note on upgrade

* fix: move around tests

* feat: use openzeppelin & remove meta txns (for now) (#5)

* fix: remove deprecation gap

* fix: migrate to oz

* oz: use erc20pausableupgradable

* fix: move 4626 to oz as well

* fix: cleanup

* feat: add failing rewards test

* fix: use oz

* fix: cleanup tests

* fix: remove deprecated interfaces

* fix: lint

* fix: remove unused revision

* fix: address comments

* fix: alter function ordering a bit

* feat: move logic to oz and rework all tests (#7)

* fix: remove deprecation gap

* fix: migrate to oz

* oz: use erc20pausableupgradable

* fix: move 4626 to oz as well

* fix: cleanup

* feat: add failing rewards test

* fix: use oz

* fix: cleanup tests

* fix: remove deprecated interfaces

* fix: lint

* fix: remove unused revision

* fix: address comments

* fix: alter function ordering a bit

* More OZ logic on stata

* add missing virtual

* Separate Stata4626 (#8)

* Separate Stata4626

* change to erc7201

* regenerated storage location

* change latestAnswer calculation logic

* DRAFT: Refactoring in extensions style

* add initializer

* remove unused params at __Stata4626_init

* remove RayMathExplicitRounding

* regenerated ERC20AaveLMStorageLocation

* add RAY constant

* remove IInitializableStata4626LM

* depositWithPermit

* disclamer on _update overload

* some descriptions cleanup

* change require to revert

* add comment to latestAnswer calc

* add comment to latestAnswer calc -1

* make ERC20AaveLMUpgradable abstract

* update license

* rename merger and 4626 contracts

* change Upgradable to Upgradeable

* move _disableInitializers into StataTokenV2

* rename IStata4626 to IERC4626StataToken

* rename init on ERC4626StataToken

* Changes on stata initializations, to follow more strict guidelines

* Changes to make stata more consistent with using ERC20 extensions

* Fix on function called on initialize of stata

* feat: improved tests

* fix: update test

* feat: add erc4626 tests

* fix: migrate some more tests

* fix: improve tests

* refactor: move to dedicated files

* feat: improve tests

* fix typo

* feat: add permit tests

* fix: linting

* feat: improved docs

* fix: typos

* fix: use internal function

---------

Co-authored-by: eboado <[email protected]>
Co-authored-by: sakulstra <[email protected]>

---------

Co-authored-by: sakulstra <[email protected]>
Co-authored-by: eboado <[email protected]>

* fix: cleanup imports

refactor: cleanup some things
(cherry picked from commit dd7166d0640e1a5bb9ad7afa03d9a21c6eb938ee)

* test: prevent mint to address(0)

* docs: add a bit more docs

* fix: lint on save

* docs: add comment about libraries

* Update tests/periphery/static-a-token/ERC20AaveLMUpgradable.t.sol

Co-authored-by: Ernesto Boado <[email protected]>

* Update tests/periphery/static-a-token/ERC4626StataTokenUpgradeable.t.sol

Co-authored-by: Ernesto Boado <[email protected]>

* refactor: rename factory + add inheritance graph (#13)

* docs: add inheritance image

* refactor: rename factory

* docs: add some more docs on readm

* fix: address certora feedback (#14)

* fix: address certora feedback

* fix: leftover

* fix: one more leftover

* fix: properly resolve conflict

* fix: total assets (#17)

* fix: calculate totalAssets

* test: add test to ensure doesn't revert on zero

* feat: use permissionless rescuable (#20)

* refactor: interface inheritance (#21)

* refactor: interface inheritance

* refactor: inherit permit

* fix: add inheritdoc

* Certora adaptation to stata (#18)

* fix: calculate totalAssets

* Certora adaptation to stata

---------

Co-authored-by: sakulstra <[email protected]>

* fix: lint certora files

* Update README.md

---------

Co-authored-by: sendra <[email protected]>
Co-authored-by: Andrey <[email protected]>
Co-authored-by: eboado <[email protected]>
Co-authored-by: Michael Morami <[email protected]>

.github/workflows/certora-stata.yml

@@ -0,0 +1,79 @@
+name: certora-stata
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v2
+        with: { python-version: 3.9 }
+
+      - name: Install java
+        uses: actions/setup-java@v1
+        with: { java-version: "11", java-package: jre }
+
+      - name: Install certora cli
+        run: pip install certora-cli==7.14.2
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.20
+
+      - name: Verify rule ${{ matrix.rule }}
+        run: |
+          cd certora/stata
+          touch applyHarness.patch
+          make munged
+          cd ../..
+          certoraRun certora/stata/conf/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
+          - verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
+          # Timeout
+          # - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
+          - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
+          - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
+          - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint
+          - verifyERC4626Extended.conf --rule maxDepositConstant
+          - verifyERC4626Extended.conf --rule redeemSum
+          - verifyERC4626Extended.conf --rule redeemATokensSum
+          - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
+          - verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
+          - verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
+          - verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
+          - verifyStataToken.conf --rule totalClaimableRewards_stable
+          - verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
+          - verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
+          - verifyStataToken.conf --rule singleAssetAccruedRewards
+          - verifyStataToken.conf --rule totalAssets_stable
+          - verifyStataToken.conf --rule getClaimableRewards_stable
+          - verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
+          - verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
+          - verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
+          - verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
+          - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
+          - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient

Makefile

@@ -35,4 +35,5 @@ coverage :; forge coverage --report lcov && \
 download :; cast etherscan-source --chain ${chain} -d src/etherscan/${chain}_${address} ${address}
 git-diff :
 	@mkdir -p diffs
+	@npx prettier ${before} ${after} --write
 	@printf '%s\n%s\n%s\n' "\`\`\`diff" "$$(git diff --no-index --diff-algorithm=patience --ignore-space-at-eol ${before} ${after})" "\`\`\`" > diffs/${out}.md

certora/conf/AToken.conf

@@ -11,5 +11,6 @@
   "process": "emv",
   "solc": "solc8.19",
   "verify": "ATokenHarness:certora/specs/AToken.spec",
+//  "build_cache": true,
   "msg": "aToken spec"
 }

certora/conf/NEW-pool-no-summarizations.conf

@@ -36,6 +36,7 @@
     "depositUpdatesUserATokenSuperBalance",
     "depositCannotChangeOthersATokenSuperBalance"
   ],
+//  "build_cache": true,
   "parametric_contracts": ["PoolHarness"],
   "msg": "pool-no-summarizations::partial rules",
 }

certora/conf/NEW-pool-simple-properties.conf

@@ -38,6 +38,7 @@
     "cannotBorrowOnReserveDisabledForBorrowing",
     "cannotBorrowOnFrozenReserve"
   ],
+//  "build_cache": true,
   "parametric_contracts": ["PoolHarness"],
   "msg": "pool-simple-properties::ALL",
 }

certora/conf/ReserveConfiguration.conf

@@ -10,5 +10,6 @@
   ],
   "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
   "solc": "solc8.19",
+//  "build_cache": true,
   "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec"
 }

certora/conf/StableDebtToken.conf

@@ -14,5 +14,6 @@
   "optimistic_loop": true,
   "process": "emv",
   "solc": "solc8.19",
+//  "build_cache": true,
   "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec"
 }

certora/conf/UserConfiguration.conf

@@ -11,5 +11,6 @@
     "-useBitVectorTheory"
   ],
   "solc": "solc8.19",
+//  "build_cache": true,
   "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec"
 }

certora/conf/VariableDebtToken.conf

@@ -7,5 +7,6 @@
   "optimistic_loop": true,
   "process": "emv",
   "solc": "solc8.19",
+//  "build_cache": true,
   "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec"
 }

certora/scripts/run-all.sh

@@ -1,4 +1,4 @@
-CMN=""
+#CMN="--compilation_steps_only"
 
 
 

certora/specs/NEW-pool-base.spec

@@ -30,19 +30,19 @@ methods {
   function _.transfer(address, uint256) external => DISPATCHER(true);
   function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
   function _.approve(address, uint256) external => DISPATCHER(true);
-  function _.mint(address, uint256) external => DISPATCHER(true);
-  function _.burn(uint256) external => DISPATCHER(true);
+  //function _.mint(address, uint256) external => DISPATCHER(true);
+  //function _.burn(uint256) external => DISPATCHER(true);
   function _.balanceOf(address) external => DISPATCHER(true);
 
   function _.totalSupply() external => DISPATCHER(true);
 
   // ATOKEN
-  function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true);
-  function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true);
+  //function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true);
+  //function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true);
   function _.mintToTreasury(uint256 amount, uint256 index) external => DISPATCHER(true);
   function _.transferOnLiquidation(address from, address to, uint256 value) external => DISPATCHER(true);
   function _.transferUnderlyingTo(address user, uint256 amount) external => DISPATCHER(true);
-  function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true);
+  //  function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true);
   function _.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) external => DISPATCHER(true);
   function _.ATokenBalanceOf(address user) external => DISPATCHER(true);
 
@@ -62,7 +62,7 @@ methods {
   function _.getReserveNormalizedIncome(address asset) external => DISPATCHER(true);
   function _.getReserveNormalizedVariableDebt(address asset) external => DISPATCHER(true);
   function _.getACLManager() external  => DISPATCHER(true);
-  function _.isBridge(address) external => DISPATCHER(true);
+  //function _.isBridge(address) external => DISPATCHER(true);
 
   // StableDebt
   function _.mint(address user, address onBehalfOf, uint256 amount, uint256 rate) external => DISPATCHER(true);

certora/specs/NEW-pool-no-summarizations.spec

@@ -9,7 +9,7 @@ methods {
   function _.symbol() external => DISPATCHER(true);
   function _.isFlashBorrower(address a) external => DISPATCHER(true);
 
-  function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true);
+  //  function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true);
 
   function _.getAverageStableRate() external => DISPATCHER(true);
   function _.isPoolAdmin(address a) external => DISPATCHER(true);

certora/stata/Makefile

@@ -0,0 +1,33 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../../src
+LIBS_DIR = ../../lib
+MUNGED_SRC    = munged/src
+MUNGED_LIB    = munged/lib
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	mkdir $@
+	cp -r ../../lib $@
+	cp -r ../../src $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	mkdir tmp
+	cp -r ../../lib tmp
+	cp -r ../../src tmp
+	diff -ruN tmp $(MUNGED_DIR) | sed 's+tmp/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH)
+	rm -rf tmp
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+

certora/stata/applyHarness.patch

@@ -0,0 +1,48 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1970-01-01 02:00:00
++++ .gitignore	2024-09-04 13:59:46
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+\ No newline at end of file
+diff -ruN src/core/instances/ATokenInstance.sol src/core/instances/ATokenInstance.sol
+--- src/core/instances/ATokenInstance.sol	2024-09-05 19:01:54
++++ src/core/instances/ATokenInstance.sol	2024-09-05 11:33:23
+@@ -35,15 +35,15 @@
+
+     _domainSeparator = _calculateDomainSeparator();
+
+-    emit Initialized(
+-      underlyingAsset,
+-      address(POOL),
+-      treasury,
+-      address(incentivesController),
+-      aTokenDecimals,
+-      aTokenName,
+-      aTokenSymbol,
+-      params
+-    );
++    // emit Initialized(
++    //   underlyingAsset,
++    //   address(POOL),
++    //   treasury,
++    //   address(incentivesController),
++    //   aTokenDecimals,
++    //   aTokenName,
++    //   aTokenSymbol,
++    //   params
++    // );
+   }
+ }
+diff -ruN src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol
+--- src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol	2024-09-05 19:01:54
++++ src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol	2024-09-05 13:48:31
+@@ -147,7 +147,7 @@
+   }
+
+   ///@inheritdoc IERC20AaveLM
+-  function rewardTokens() external view returns (address[] memory) {
++  function rewardTokens() public view returns (address[] memory) {
+     ERC20AaveLMStorage storage $ = _getERC20AaveLMStorage();
+     return $._rewardTokens;
+   }

certora/stata/conf/verifyAToken.conf

@@ -0,0 +1,40 @@
+{
+  "files": [
+    "certora/stata/harness/StataTokenV2Harness.sol",
+    "certora/stata/harness/pool/SymbolicLendingPool.sol",
+    "certora/stata/harness/rewards/RewardsControllerHarness.sol",
+    "certora/stata/harness/rewards/TransferStrategyHarness.sol",
+    "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+    "certora/stata/harness/tokens/DummyERC20_rewardToken.sol",
+    "certora/stata/munged/src/core/instances/ATokenInstance.sol",
+  ],
+  "link": [
+    "SymbolicLendingPool:aToken=ATokenInstance",
+    "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying",
+    "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "TransferStrategyHarness:REWARD=DummyERC20_rewardToken",
+    "ATokenInstance:POOL=SymbolicLendingPool",
+    "ATokenInstance:_incentivesController=RewardsControllerHarness",
+    "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying",
+    "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StataTokenV2Harness:POOL=SymbolicLendingPool",
+    "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=certora/stata/munged/src/core",
+     "aave-v3-periphery/=certora/stata/munged/src/periphery",
+     "solidity-utils/=certora/stata/munged/lib/solidity-utils/src",
+     "forge-std/=certora/stata/munged/lib/forge-std/src",
+     "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable",
+     "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
+     "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
+  ],
+  "loop_iter": "1",
+  "msg": "aToken properties",
+  "optimistic_hashing": true,
+  "optimistic_loop": true,
+  "solc": "solc8.20",
+  "smt_timeout": "1400",
+  "verify": "StataTokenV2Harness:certora/stata/specs/StataToken/aTokenProperties.spec",
+  "build_cache": true,
+}

certora/stata/conf/verifyDoubleClaim.conf

@@ -0,0 +1,40 @@
+{
+  "files": [
+    "certora/stata/harness/StataTokenV2Harness.sol",
+    "certora/stata/harness/pool/SymbolicLendingPool.sol",
+    "certora/stata/harness/rewards/RewardsControllerHarness.sol",
+    "certora/stata/harness/rewards/TransferStrategyHarness.sol",
+    "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+    "certora/stata/harness/tokens/DummyERC20_rewardToken.sol",
+    "certora/stata/munged/src/core/instances/ATokenInstance.sol",
+  ],
+  "link": [
+    "SymbolicLendingPool:aToken=ATokenInstance",
+    "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying",
+    "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "TransferStrategyHarness:REWARD=DummyERC20_rewardToken",
+    "ATokenInstance:POOL=SymbolicLendingPool",
+    "ATokenInstance:_incentivesController=RewardsControllerHarness",
+    "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying",
+    "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StataTokenV2Harness:POOL=SymbolicLendingPool",
+    "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=certora/stata/munged/src/core",
+     "aave-v3-periphery/=certora/stata/munged/src/periphery",
+     "solidity-utils/=certora/stata/munged/lib/solidity-utils/src",
+     "forge-std/=certora/stata/munged/lib/forge-std/src",
+     "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable",
+     "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
+     "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
+],
+  "verify":"StataTokenV2Harness:certora/stata/specs/StataToken/double_claim.spec",
+  "solc": "solc8.20",
+  "msg": "Multi rewards - double claim properties",
+  "optimistic_loop": true,
+  "smt_timeout": "2000",
+  "loop_iter": "2",
+  "optimistic_hashing": true,
+  "build_cache": true,
+}

certora/stata/conf/verifyERC4626.conf

@@ -0,0 +1,40 @@
+{
+  "files": [
+    "certora/stata/harness/StataTokenV2Harness.sol",
+    "certora/stata/harness/pool/SymbolicLendingPool.sol",
+    "certora/stata/harness/rewards/RewardsControllerHarness.sol",
+    "certora/stata/harness/rewards/TransferStrategyHarness.sol",
+    "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol",
+    "certora/stata/harness/tokens/DummyERC20_rewardToken.sol",
+    "certora/stata/munged/src/core/instances/ATokenInstance.sol",
+  ],
+  "link": [
+    "SymbolicLendingPool:aToken=ATokenInstance",
+    "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying",
+    "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "TransferStrategyHarness:REWARD=DummyERC20_rewardToken",
+    "ATokenInstance:POOL=SymbolicLendingPool",
+    "ATokenInstance:_incentivesController=RewardsControllerHarness",
+    "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying",
+    "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StataTokenV2Harness:POOL=SymbolicLendingPool",
+    "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=certora/stata/munged/src/core",
+     "aave-v3-periphery/=certora/stata/munged/src/periphery",
+     "solidity-utils/=certora/stata/munged/lib/solidity-utils/src",
+     "forge-std/=certora/stata/munged/lib/forge-std/src",
+     "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable",
+     "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
+     "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
+],
+  "verify":"StataTokenV2Harness:certora/stata/specs/erc4626/erc4626.spec",
+  "solc": "solc8.20",
+  "msg": "ERC4626 properties",
+  "optimistic_loop": true,
+  "smt_timeout": "3600",
+  "loop_iter": "1",
+  "optimistic_hashing": true,
+  "build_cache": true,
+}