aave-dao · sakulstra · Oct 1, 2024 · Apr 23, 2024 · Apr 24, 2024 · Apr 24, 2024
diff --git a/.github/workflows/certora.yml → .github/workflows/certora-basic.yml b/.github/workflows/certora.yml → .github/workflows/certora-basic.yml
@@ -39,7 +39,7 @@ jobs:
         with: { java-version: "11", java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==7.0.7
+        run: pip install certora-cli==7.14.2
 
       - name: Install solc
         run: |
@@ -49,12 +49,12 @@ jobs:
 
       - name: Verify rule ${{ matrix.rule }}
         run: |
-          cd certora
+          cd certora/basic
           touch applyHarness.patch
           make munged
-          cd ..
+          cd ../..
           echo "key length" ${#CERTORAKEY}
-          certoraRun certora/conf/${{ matrix.rule }} --wait_for_results
+          certoraRun certora/basic/conf/${{ matrix.rule }} --wait_for_results
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -68,6 +68,8 @@ jobs:
           - UserConfiguration.conf
           - VariableDebtToken.conf
           - NEW-pool-no-summarizations.conf
+          - stableRemoved.conf
+          - EModeConfiguration.conf
           - NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
           - NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
           - NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"

diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml
@@ -56,8 +56,7 @@ jobs:
           # - 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 previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
           - verifyERC4626Extended.conf --rule redeemSum
           - verifyERC4626Extended.conf --rule redeemATokensSum
           - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf

diff --git a/LICENSE b/LICENSE
@@ -10,7 +10,7 @@ Parameters
 Licensor:             Aave DAO, represented by its governance smart contracts
 
 
-Licensed Work:        Aave v3.1
+Licensed Work:        Aave v3.2
                       The Licensed Work is (c) 2024 Aave DAO, represented by its governance smart contracts
 
 Additional Use Grant: You are permitted to use, copy, and modify the Licensed Work, subject to
@@ -35,7 +35,7 @@ Additional Use Grant: You are permitted to use, copy, and modify the Licensed Wo
 
 Change Date:          The earlier of:
                       - 2027-03-06
-                      - If specified, the date in the 'change-date' record on v31.aavelicense.eth
+                      - If specified, the date in the 'change-date' record on v32.aavelicense.eth
 
 Change License:       MIT
 
@@ -114,4 +114,4 @@ other recipients of the licensed work to be provided by Licensor:
 
 3. To specify a Change Date.
 
-4. Not to modify this License in any other way.
+4. Not to modify this License in any other way.
diff --git a/Makefile b/Makefile
@@ -9,31 +9,45 @@ update:; forge update
 test   :; forge test -vvv --no-match-contract DeploymentsGasLimits
 test-contract :; forge test --match-contract ${filter} -vvv
 test-watch   :; forge test --watch -vvv --no-match-contract DeploymentsGasLimits
-coverage :; forge coverage --report lcov && \
-	lcov --remove ./lcov.info -o ./lcov.info.p \
-	'scripts/*' \
-	'tests/*' \
-	'src/deployments/*' \
-	'src/periphery/contracts/v3-config-engine/*' \
-	'src/periphery/contracts/treasury/*' \
-	'src/periphery/contracts/dependencies/openzeppelin/ReentrancyGuard.sol' \
-	'src/periphery/contracts/misc/UiIncentiveDataProviderV3.sol' \
-	'src/periphery/contracts/misc/UiPoolDataProviderV3.sol' \
-	'src/periphery/contracts/misc/WalletBalanceProvider.sol' \
-	'src/periphery/contracts/mocks/*' \
-	'src/core/contracts/mocks/*' \
-	'src/core/contracts/dependencies/*' \
-	'src/core/contracts/misc/AaveProtocolDataProvider.sol' \
-	'src/core/contracts/protocol/libraries/configuration/*' \
-	'src/core/contracts/protocol/libraries/logic/GenericLogic.sol' \
-	'src/core/contracts/protocol/libraries/logic/ReserveLogic.sol' \
-	&& genhtml ./lcov.info.p -o report --branch-coverage \
-	&& coverage=$$(awk -F '[<>]' '/headerCovTableEntryHi/{print $3}' ./report/index.html | sed 's/[^0-9.]//g' | head -n 1); \
+
+# Coverage
+coverage-base :; forge coverage --report lcov --no-match-coverage "(scripts|tests|deployments|mocks)"
+coverage-clean :; lcov --rc derive_function_end_line=0 --remove ./lcov.info -o ./lcov.info.p \
+	'src/contracts/extensions/v3-config-engine/*' \
+	'src/contracts/treasury/*' \
+	'src/contracts/dependencies/openzeppelin/ReentrancyGuard.sol' \
+	'src/contracts/helpers/UiIncentiveDataProviderV3.sol' \
+	'src/contracts/helpers/UiPoolDataProviderV3.sol' \
+	'src/contracts/helpers/WalletBalanceProvider.sol' \
+	'src/contracts/dependencies/*' \
+	'src/contracts/helpers/AaveProtocolDataProvider.sol' \
+	'src/contracts/protocol/libraries/configuration/*' \
+	'src/contracts/protocol/libraries/logic/GenericLogic.sol' \
+	'src/contracts/protocol/libraries/logic/ReserveLogic.sol'
+coverage-report :; genhtml ./lcov.info.p -o report --branch-coverage --rc derive_function_end_line=0 --parallel
+coverage-badge :; coverage=$$(awk -F '[<>]' '/headerCovTableEntryHi/{print $3}' ./report/index.html | sed 's/[^0-9.]//g' | head -n 1); \
 	wget -O ./report/coverage.svg "https://img.shields.io/badge/coverage-$${coverage}%25-brightgreen"
+coverage :
+	make coverage-base
+	make coverage-clean
+	make coverage-report
+	make coverage-badge
 
 # Utilities
 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
+	@printf '%s\n%s\n%s\n' "\`\`\`diff" "$$(git diff --no-index --ignore-space-at-eol ${before} ${after})" "\`\`\`" > diffs/${out}.md
+
+# Deploy
+deploy-libs-one	:;
+	forge script scripts/misc/LibraryPreCompileOne.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --verify --slow --broadcast
+deploy-libs-two	:;
+	forge script scripts/misc/LibraryPreCompileTwo.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --verify --slow --broadcast
+
+deploy-libs :
+	make deploy-libs-one chain=${chain}
+	npx catapulta-verify -b broadcast/LibraryPreCompileOne.sol/${chainId}/run-latest.json
+	make deploy-libs-two chain=${chain}
+	npx catapulta-verify -b broadcast/LibraryPreCompileTwo.sol/${chainId}/run-latest.json
diff --git a/README.md b/README.md
@@ -1,8 +1,8 @@
-# Aave V3.1 Origin
+# Aave V3.2 Origin
 
 ![Aave v3.1 Origin_banner](./resources/v3-1-banner.jpeg)
 
-Aave v3.1 complete codebase, Foundry-based.
+Aave v3.2 complete codebase, Foundry-based.
 
 [![Coverage badge](./report/coverage.svg)](https://aave-dao.github.io/aave-v3-origin)
 <br>
@@ -42,6 +42,8 @@ bun install
 - [Aave v3 technical Paper](./docs/Aave_V3_Technical_Paper.pdf)
 - [v3 to v3.0.2 production upgrade](https://github.com/bgd-labs/proposal-3.0.2-upgrade/blob/main/README.md)
 - [Aave v3.1 features](./docs/Aave-v3.1-features.md)
+- [Aave v3.2 features](./docs/3.2/Aave-v3.2-features.md)
+- [v3.1 to v3.2.0 production upgrade](https://github.com/bgd-labs/protocol-3.2.0-upgrade/blob/main/README.md)
 - [Set Ltv to 0 on Freeze Feature State diagram](./docs/freeze-ltv0-states.png)
 
 <br>
@@ -85,7 +87,22 @@ The following are the security procedures historically applied to Aave v3.X vers
 - [MixBytes](./audits/02-05-2024_MixBytes_AaveV3.1.pdf)
 - An internal review by [SterMi](https://twitter.com/stermi) on the virtual accounting feature was conducted on an initial phase of the codebase.
 - [Cantina competition report](./audits/02-06-2024-Cantina-contest-AaveV3.1.pdf)
-- Additionally, Certora properties have been improved over time since the Aave v3 release. More details [HERE](./certora/README.md).
+- Additionally, Certora properties have been improved over time since the Aave v3 release. More details [HERE](./certora/basic/README.md).
+
+<br>
+
+**-> Aave v3.2 - September 2024**
+
+#### Stable Rate and Liquid eModes
+
+- [Certora](./audits/2024-09-10_Certora_Aave-v3.2_Stable_Rate_Removal.pdf)
+- [Enigma Dark](./audits/2024-09-30_Enigma_Aave-v3.2.pdf)
+
+#### Liquid eModes
+
+- [Certora](./audits/2024-09-19_Certora_Aave-v3.2_Liquid_eModes.pdf)
+- [Oxorio](./audits/2024-09-12_Oxorio_Aav3-v3.2.pdf)
+- [Pashov](./audits/2024-09-15_Pashov_Aave-v3.2.pdf)
 
 <br>
 

diff --git a/audits/2024-09-10_Certora_Aave-v3.2_Stable_Rate_Removal.pdf b/audits/2024-09-10_Certora_Aave-v3.2_Stable_Rate_Removal.pdf
diff --git a/audits/2024-09-12_Oxorio_Aav3-v3.2.pdf b/audits/2024-09-12_Oxorio_Aav3-v3.2.pdf
diff --git a/audits/2024-09-15_Pashov_Aave-v3.2.pdf b/audits/2024-09-15_Pashov_Aave-v3.2.pdf
diff --git a/audits/2024-09-19_Certora_Aave-v3.2_Liquid_eModes.pdf b/audits/2024-09-19_Certora_Aave-v3.2_Liquid_eModes.pdf
diff --git a/audits/2024-09-30_Enigma_Aave-v3.2.pdf b/audits/2024-09-30_Enigma_Aave-v3.2.pdf
diff --git a/certora/basic/Makefile b/certora/basic/Makefile
@@ -0,0 +1,24 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../../src/
+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 $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./src/++g' | sed 's+munged/++g' > $(PATCH)
+
+clean:
+	git clean -fdX
+	touch $(PATCH)
+
diff --git a/certora/README.md → certora/basic/README.md b/certora/README.md → certora/basic/README.md
diff --git a/certora/applyHarness.patch → certora/basic/applyHarness.patch b/certora/applyHarness.patch → certora/basic/applyHarness.patch
@@ -1,22 +1,22 @@
-diff -ruN core/contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol core/contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol
---- core/contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol	2024-03-27 12:57:15.497294747 +0200
-+++ core/contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol	2024-03-27 13:08:22.155984803 +0200
+diff -ruN contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol
+--- contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol	2024-03-27 12:57:15.497294747 +0200
++++ contracts/protocol/tokenization/base/ScaledBalanceTokenBase.sol	2024-03-27 13:08:22.155984803 +0200
 @@ -34,7 +34,7 @@
    }
- 
+
    /// @inheritdoc IScaledBalanceToken
 -  function scaledBalanceOf(address user) external view override returns (uint256) {
 +  function scaledBalanceOf(address user) public view override returns (uint256) {
      return super.balanceOf(user);
    }
- 
-diff -ruN core/instances/ATokenInstance.sol core/instances/ATokenInstance.sol
---- core/instances/ATokenInstance.sol	2024-03-27 12:57:15.497294747 +0200
-+++ core/instances/ATokenInstance.sol	2024-03-27 13:14:17.971198372 +0200
+
+diff -ruN contracts/instances/ATokenInstance.sol contracts/instances/ATokenInstance.sol
+--- contracts/instances/ATokenInstance.sol	2024-03-27 12:57:15.497294747 +0200
++++ contracts/instances/ATokenInstance.sol	2024-03-27 13:14:17.971198372 +0200
 @@ -35,15 +35,15 @@
- 
+
      _domainSeparator = _calculateDomainSeparator();
- 
+
 -    emit Initialized(
 -      underlyingAsset,
 -      address(POOL),

diff --git a/certora/basic/conf/AToken.conf b/certora/basic/conf/AToken.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/basic/harness/ATokenHarness.sol",
+    "certora/basic/harness/SimpleERC20.sol"
+  ],
+  "link": [
+    "ATokenHarness:_underlyingAsset=SimpleERC20"
+  ],
+  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic".
+  "optimistic_loop": true,
+  "process": "emv",
+  "solc": "solc8.19",
+  "verify": "ATokenHarness:certora/basic/specs/AToken.spec",
+  "build_cache": true,
+  "msg": "aToken spec"
+}
diff --git a/certora/basic/conf/EModeConfiguration.conf b/certora/basic/conf/EModeConfiguration.conf
@@ -0,0 +1,14 @@
+{
+  "files": [
+    "certora/basic/harness/EModeConfigurationHarness.sol"
+  ],
+  "msg": "EModeConfiguration",
+  "optimistic_loop": true,
+  "process": "emv",
+  //  "prover_args": [],
+  "precise_bitwise_ops": true,
+  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "EModeConfigurationHarness:certora/basic/specs/EModeConfiguration.spec"
+}
diff --git a/certora/basic/conf/NEW-pool-no-summarizations.conf b/certora/basic/conf/NEW-pool-no-summarizations.conf
@@ -0,0 +1,40 @@
+{
+  "files": [
+    "certora/basic/harness/ATokenHarness.sol",
+    "certora/basic/harness/PoolHarness.sol",
+    "certora/basic/harness/SimpleERC20.sol",
+    "src/contracts/instances/VariableDebtTokenInstance.sol",
+    "src/contracts/helpers/AaveProtocolDataProvider.sol",
+    "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
+    "src/contracts/protocol/configuration/ACLManager.sol",
+    "src/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
+    "src/contracts/misc/PriceOracleSentinel.sol",
+    "src/contracts/protocol/configuration/PoolAddressesProvider.sol",
+  ],
+  "link": [
+    "ATokenHarness:POOL=PoolHarness",
+    "ATokenHarness:_underlyingAsset=SimpleERC20",
+    "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+    "AaveProtocolDataProvider:ADDRESSES_PROVIDER=PoolAddressesProvider",
+  ],
+  "struct_link": [
+    "PoolHarness:aTokenAddress=ATokenHarness",
+    "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
+    "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
+  ],
+  "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+  "optimistic_loop": true,
+  "process": "emv",
+  "global_timeout": "7198",
+  "prover_args": ["-depth 11"], // If reachability passes and the time is ok, this number is ok, dont touch it.
+  "solc": "solc8.19",
+  "verify": "PoolHarness:certora/basic/specs/NEW-pool-no-summarizations.spec",
+  "rule": [
+    "liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
+    "depositUpdatesUserATokenSuperBalance",
+    "depositCannotChangeOthersATokenSuperBalance"
+  ],
+  "build_cache": true,
+  "parametric_contracts": ["PoolHarness"],
+  "msg": "pool-no-summarizations::partial rules",
+}
diff --git a/certora/basic/conf/NEW-pool-simple-properties.conf b/certora/basic/conf/NEW-pool-simple-properties.conf
@@ -0,0 +1,32 @@
+{
+  "files": [
+    "certora/basic/harness/ATokenHarness.sol",
+    "certora/basic/harness/PoolHarness.sol",
+    "certora/basic/harness/SimpleERC20.sol",
+    "src/contracts/instances/VariableDebtTokenInstance.sol",
+    "src/contracts/helpers/AaveProtocolDataProvider.sol",
+    "src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
+    "src/contracts/protocol/libraries/types/DataTypes.sol",
+    "src/contracts/protocol/configuration/PoolAddressesProvider.sol",
+  ],
+  "link": [
+    "ATokenHarness:POOL=PoolHarness",
+    "ATokenHarness:_underlyingAsset=SimpleERC20",
+    "PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
+  ],
+  "struct_link": [
+    "PoolHarness:aTokenAddress=ATokenHarness",
+    "PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
+    "PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
+  ],
+  "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+  "optimistic_loop": true,
+  "process": "emv",
+  "prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it.
+  "solc": "solc8.19",
+  "verify": "PoolHarness:certora/basic/specs/NEW-pool-simple-properties.spec",
+  "build_cache": true,
+  "parametric_contracts": ["PoolHarness"],
+  "smt_timeout": "6000",
+  "msg": "pool-simple-properties::ALL",
+}
diff --git a/certora/basic/conf/ReserveConfiguration.conf b/certora/basic/conf/ReserveConfiguration.conf
@@ -0,0 +1,16 @@
+{
+  "files": [
+    "certora/basic/harness/ReserveConfigurationHarness.sol"
+  ],
+  "msg": "ReserveConfiguration",
+  "optimistic_loop": true,
+  "process": "emv",
+  //  "prover_args": [
+  //  "-precise_bitwise_ops"
+  //],
+  "precise_bitwise_ops": true,
+  "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "ReserveConfigurationHarness:certora/basic/specs/ReserveConfiguration.spec"
+}
diff --git a/certora/basic/conf/UserConfiguration.conf b/certora/basic/conf/UserConfiguration.conf
@@ -0,0 +1,17 @@
+{
+  "files": [
+    "certora/basic/harness/UserConfigurationHarness.sol"
+  ],
+  // No rule sanity because a there are invariant s.t. the invariant can be proven
+  // without assuming it first. (for some of the functions.)
+  "msg": "UserConfiguration All spec",
+  "optimistic_loop": true,
+  "process": "emv",
+//  "prover_args": [
+  //  "-precise_bitwise_ops"
+  //],
+  "precise_bitwise_ops": true,
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "UserConfigurationHarness:certora/basic/specs/UserConfiguration.spec"
+}
diff --git a/certora/basic/conf/VariableDebtToken.conf b/certora/basic/conf/VariableDebtToken.conf
@@ -0,0 +1,12 @@
+{
+  "files": [
+    "certora/basic/harness/VariableDebtTokenHarness.sol"
+  ],
+  "rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
+  "msg": "variable debt token",
+  "optimistic_loop": true,
+  "process": "emv",
+  "solc": "solc8.19",
+  "build_cache": true,
+  "verify": "VariableDebtTokenHarness:certora/basic/specs/VariableDebtToken.spec"
+}