Skip to content

Commit

Permalink
Merge pull request #6 from Certora/munging
Browse files Browse the repository at this point in the history
final adaptation of FV specs to stata
  • Loading branch information
MichaelMorami authored Sep 8, 2024
2 parents 843f6e4 + 64a0ffd commit 7c61ef4
Show file tree
Hide file tree
Showing 37 changed files with 1,463 additions and 1,739 deletions.
50 changes: 20 additions & 30 deletions .github/workflows/certora-stata.yml
Original file line number Diff line number Diff line change
Expand Up @@ -51,39 +51,29 @@ jobs:
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
- 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
#The following seem to be incorrect:
# verifyERC4626Extended.conf --rule maxDepositConstant
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
- 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
- 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
13 changes: 7 additions & 6 deletions certora/stata/Makefile
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
default: help

PATCH = applyHarness.patch
CONTRACTS_DIR = ../src
LIBS_DIR = ../lib
CONTRACTS_DIR = ../../src
LIBS_DIR = ../../lib
MUNGED_SRC = munged/src
MUNGED_LIB = munged/lib
MUNGED_DIR = munged

help:
@echo "usage:"
Expand All @@ -15,14 +16,14 @@ help:
munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
rm -rf $@
mkdir $@
cp -r ../lib $@
cp -r ../src $@
cp -r ../../lib $@
cp -r ../../src $@
patch -p0 -d $@ < $(PATCH)

record:
mkdir tmp
cp -r ../lib tmp
cp -r ../src 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

Expand Down
45 changes: 43 additions & 2 deletions certora/stata/applyHarness.patch
Original file line number Diff line number Diff line change
@@ -1,7 +1,48 @@
diff -ruN .gitignore .gitignore
--- .gitignore 1970-01-01 02:00:00
+++ .gitignore 2023-04-01 01:24:40
+++ .gitignore 2024-09-04 13:59:46
@@ -0,0 +1,2 @@
+*
+!.gitignore
\ No newline at end of file
\ 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;
}
29 changes: 15 additions & 14 deletions certora/stata/conf/verifyAToken.conf
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
{
"files": [
"certora/stata/harness/StaticATokenLMHarness.sol",
"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",
"src/core/instances/ATokenInstance.sol",
"certora/stata/munged/src/core/instances/ATokenInstance.sol",
],
"link": [
"SymbolicLendingPool:aToken=ATokenInstance",
Expand All @@ -16,24 +16,25 @@
"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"
"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,
"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",
"verify": "StataTokenV2Harness:certora/stata/specs/staticATokenLM/aTokenProperties.spec",
"build_cache": true,
}
27 changes: 14 additions & 13 deletions certora/stata/conf/verifyDoubleClaim.conf
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
{
"files": [
"certora/stata/harness/StaticATokenLMHarness.sol",
"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",
"src/core/instances/ATokenInstance.sol",
"certora/stata/munged/src/core/instances/ATokenInstance.sol",
],
"link": [
"SymbolicLendingPool:aToken=ATokenInstance",
Expand All @@ -16,19 +16,20 @@
"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"
"StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
"StataTokenV2Harness:POOL=SymbolicLendingPool",
"StataTokenV2Harness:_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",
"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/staticATokenLM/double_claim.spec",
"solc": "solc8.20",
"msg": "Multi rewards - double claim properties",
"optimistic_loop": true,
Expand Down
29 changes: 9 additions & 20 deletions certora/stata/conf/verifyERC4626.conf
Original file line number Diff line number Diff line change
@@ -1,15 +1,12 @@
{
"files": [
"certora/stata/harness/StataTokenV2Harness.sol",
"certora/stata/harness/ERC4626StataTokenStorage_Harness.sol",
"certora/stata/harness/ERC4626Storage_Harness.sol",
// "certora/stata/harness/ERC20AaveLMStorage_Harness.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",
"certora/stata/munged/src/core/instances/ATokenInstance.sol",
],
"link": [
"SymbolicLendingPool:aToken=ATokenInstance",
Expand All @@ -21,30 +18,22 @@
"ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying",
"StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
"StataTokenV2Harness:POOL=SymbolicLendingPool",
"ERC4626StataTokenStorage_Harness:_aToken=ATokenInstance",
"ERC4626Storage_Harness:_asset=DummyERC20_aTokenUnderlying",
// "ERC4626Storage_Harness:the_storage._asset=DummyERC20_aTokenUnderlying",
"StataTokenV2Harness:_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",
"openzeppelin-contracts-upgradeable/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable",
"openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
"@openzeppelin/contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",

//lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/
//@openzeppelin/contracts/=lib/openzeppelin-contracts/contracts/

"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":"StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626.spec",
"verify":"StataTokenV2Harness:certora/stata/specs/erc4626/erc4626.spec",
"solc": "solc8.20",
"msg": "ERC4626 properties",
"optimistic_loop": true,
"smt_timeout": "1000",
"smt_timeout": "3600",
"loop_iter": "1",
"optimistic_hashing": true,
"build_cache": true,
Expand Down
30 changes: 15 additions & 15 deletions certora/stata/conf/verifyERC4626DepositSummarization.conf
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
{
"files": [
"certora/stata/harness/StaticATokenLMHarness.sol",
"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",
"src/core/instances/ATokenInstance.sol",
"certora/stata/munged/src/core/instances/ATokenInstance.sol",
],
"link": [
"SymbolicLendingPool:aToken=ATokenInstance",
Expand All @@ -16,24 +16,24 @@
"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"
"StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness",
"StataTokenV2Harness:POOL=SymbolicLendingPool",
"StataTokenV2Harness:_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",
"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/erc4626DepositSummarization.spec",
"solc": "solc8.20",
"msg": "ERC4626 summarized properties depositCheckIndexGRayAssert1",
"msg": "ERC4626 Deposit summarized",
"optimistic_loop": true,
"loop_iter": "1",
"optimistic_hashing": true,
"build_cache": true,
// "rule":["depositCheckIndexGRayAssert1"],
}
Loading

0 comments on commit 7c61ef4

Please sign in to comment.