import the static(stata) rules

Certora · Aug 26, 2024 · 759909d · 759909d
1 parent f7213cd
commit 759909d
Show file tree

Hide file tree

Showing 31 changed files with 3,602 additions and 0 deletions.
diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml
@@ -0,0 +1,89 @@
+name: certora-stata
+
+on:
+  push:
+    branches:
+      - main certora
+  pull_request:
+    branches:
+      - main certora
+
+  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.10.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
+          touch applyHarness.patch
+          make munged
+          cd ..
+          certoraRun certora/conf/${{ matrix.rule }}
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+    strategy:
+      fail-fast: false
+      max-parallel: 16
+      matrix:
+        rule:
+          - verifyERC4626.conf --rule previewMintIndependentOfAllowance previewRedeemIndependentOfBalance  previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawIndependentOfMaxWithdraw previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert  previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
+          - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
+          #The following seem to be incorrect:
+          #  verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert
+          #   # Timeout
+          # - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1
+          - verifyERC4626DepositSummarization.conf --rule depositCheckIndexERayAssert1
+          - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint
+          #The following seem to be incorrect:
+          # verifyERC4626Extended.conf --rule maxDepositConstant
+          - verifyERC4626Extended.conf --rule redeemSum
+          - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
+          - verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
+          - verifyStaticATokenLM.conf --rule rewardsConsistencyWhenSufficientRewardsExist
+          - verifyStaticATokenLM.conf --rule rewardsConsistencyWhenInsufficientRewards
+          - verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim
+          - verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim_timedout_methods
+          - verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim_redeem_methods
+          - verifyStaticATokenLM.conf --rule solvency_positive_total_supply_only_if_positive_asset
+          - verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply
+          - verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply_CASE_SPLIT_redeem
+          - verifyStaticATokenLM.conf --rule singleAssetAccruedRewards
+          - verifyStaticATokenLM.conf --rule totalAssets_stable
+          - verifyStaticATokenLM.conf --rule totalAssets_stable_after_collectAndUpdateRewards
+          - verifyStaticATokenLM.conf --rule reward_balance_stable_after_collectAndUpdateRewards
+          - verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT
+          # - verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT_redeem
+          #   # Timeout
+          - verifyStaticATokenLM.conf --rule getClaimableRewards_stable
+          - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_deposit
+          - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_redeem 
+          - verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT_deposit
+          - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
+          - verifyStaticATokenLM.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
+          - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
+          - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient
diff --git a/certora/stata/Makefile b/certora/stata/Makefile
@@ -0,0 +1,32 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../src
+LIBS_DIR = ../lib
+MUNGED_SRC    = munged/src
+MUNGED_LIB    = munged/lib
+
+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)
+
diff --git a/certora/stata/applyHarness.patch b/certora/stata/applyHarness.patch
@@ -0,0 +1,7 @@
+diff -ruN .gitignore .gitignore
+--- .gitignore	1970-01-01 02:00:00
++++ .gitignore	2023-04-01 01:24:40
+@@ -0,0 +1,2 @@
++*
++!.gitignore
+\ No newline at end of file
diff --git a/certora/stata/conf/verifyAToken.conf b/certora/stata/conf/verifyAToken.conf
@@ -0,0 +1,39 @@
+{
+  "files": [
+    "certora/stata/harness/StaticATokenLMHarness.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",
+    "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",
+    "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StaticATokenLMHarness:POOL=SymbolicLendingPool",
+    "StaticATokenLMHarness:_aToken=ATokenInstance",
+    "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying",
+    "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "loop_iter": "1",
+  "msg": "aToken properties",
+  "optimistic_hashing": true,
+  "optimistic_loop": true,
+  "packages": [
+     "aave-v3-core/=src/core",
+     "aave-v3-periphery/=src/periphery",
+     "solidity-utils/=lib/solidity-utils/src",
+     "forge-std/=lib/forge-std/src",
+  ],
+  "solc": "solc8.20",
+  "smt_timeout": "1400",
+  "verify": "StaticATokenLMHarness:certora/stata/specs/staticATokenLM/aTokenProperties.spec",
+  "build_cache": true,
+}
diff --git a/certora/stata/conf/verifyDoubleClaim.conf b/certora/stata/conf/verifyDoubleClaim.conf
@@ -0,0 +1,39 @@
+{
+  "files": [
+    "certora/stata/harness/StaticATokenLMHarness.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",
+    "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",
+    "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StaticATokenLMHarness:POOL=SymbolicLendingPool",
+    "StaticATokenLMHarness:_aToken=ATokenInstance",
+    "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying",
+    "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=src/core",
+     "aave-v3-periphery/=src/periphery",
+     "solidity-utils/=lib/solidity-utils/src",
+     "forge-std/=lib/forge-std/src",
+  ],
+  "verify":"StaticATokenLMHarness:certora/stata/specs/staticATokenLM/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,
+}
diff --git a/certora/stata/conf/verifyERC4626.conf b/certora/stata/conf/verifyERC4626.conf
@@ -0,0 +1,39 @@
+{
+  "files": [
+    "certora/stata/harness/StaticATokenLMHarness.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",
+    "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",
+    "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StaticATokenLMHarness:POOL=SymbolicLendingPool",
+    "StaticATokenLMHarness:_aToken=ATokenInstance",
+    "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying",
+    "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=src/core",
+     "aave-v3-periphery/=src/periphery",
+     "solidity-utils/=lib/solidity-utils/src",
+     "forge-std/=lib/forge-std/src",
+  ],
+  "verify":"StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626.spec",
+  "solc": "solc8.20",
+  "msg": "ERC4626 properties",
+  "optimistic_loop": true,
+  "smt_timeout": "1000",
+  "loop_iter": "1",
+  "optimistic_hashing": true,
+  "build_cache": true,
+}
diff --git a/certora/stata/conf/verifyERC4626DepositSummarization.conf b/certora/stata/conf/verifyERC4626DepositSummarization.conf
@@ -0,0 +1,39 @@
+{
+  "files": [
+    "certora/stata/harness/StaticATokenLMHarness.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",
+    "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",
+    "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StaticATokenLMHarness:POOL=SymbolicLendingPool",
+    "StaticATokenLMHarness:_aToken=ATokenInstance",
+    "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying",
+    "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=src/core",
+     "aave-v3-periphery/=src/periphery",
+     "solidity-utils/=lib/solidity-utils/src",
+     "forge-std/=lib/forge-std/src",
+  ],
+  "verify": "StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626DepositSummarization.spec",
+  "solc": "solc8.20",
+  "msg": "ERC4626 summarized properties depositCheckIndexGRayAssert1",
+  "optimistic_loop": true,
+  "loop_iter": "1",
+  "optimistic_hashing": true,
+  "build_cache": true,
+//  "rule":["depositCheckIndexGRayAssert1"],
+}
diff --git a/certora/stata/conf/verifyERC4626Extended.conf b/certora/stata/conf/verifyERC4626Extended.conf
@@ -0,0 +1,39 @@
+{
+  "files": [
+    "certora/stata/harness/StaticATokenLMHarness.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",
+    "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",
+    "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StaticATokenLMHarness:POOL=SymbolicLendingPool",
+    "StaticATokenLMHarness:_aToken=ATokenInstance",
+    "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying",
+    "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=src/core",
+     "aave-v3-periphery/=src/periphery",
+     "solidity-utils/=lib/solidity-utils/src",
+     "forge-std/=lib/forge-std/src",
+  ],
+  "verify":"StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626Extended.spec",
+  "solc": "solc8.20",
+  "msg": "ERC4626 Extended properties",
+  "optimistic_loop": true,
+  "smt_timeout": "1000",
+  "loop_iter": "1",
+  "optimistic_hashing": true,
+  "build_cache": true,
+}
diff --git a/certora/stata/conf/verifyERC4626MintDepositSummarization.conf b/certora/stata/conf/verifyERC4626MintDepositSummarization.conf
@@ -0,0 +1,40 @@
+{
+  "files": [
+    "certora/stata/harness/StaticATokenLMHarness.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",
+    "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",
+    "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
+    "StaticATokenLMHarness:POOL=SymbolicLendingPool",
+    "StaticATokenLMHarness:_aToken=ATokenInstance",
+    "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying",
+    "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken"
+  ],
+  "packages": [
+     "aave-v3-core/=src/core",
+     "aave-v3-periphery/=src/periphery",
+     "solidity-utils/=lib/solidity-utils/src",
+     "forge-std/=lib/forge-std/src",
+  ],
+  "verify":
+    "StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626MintDepositSummarization.spec",
+  "solc": "solc8.20",
+  "msg": "ERC4626 Summarized no transferFrom properties",
+  "optimistic_loop": true,
+  "smt_timeout": "5000",
+  "loop_iter": "1",
+  "optimistic_hashing": true,
+  "build_cache": true,
+}