Skip to content

Commit 712f1c3

Browse files
nisnislevisakulstra
nisnislevi
authored and
sakulstra
committed
test: adjust certora test suite to new directory structure (#30)
1 parent 024d61f commit 712f1c3

81 files changed

Lines changed: 3622 additions & 59 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

.github/workflows/certora.yml renamed to .github/workflows/certora-basic.yml

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ jobs:
3939
with: { java-version: "11", java-package: jre }
4040

4141
- name: Install certora cli
42-
run: pip install certora-cli==7.0.7
42+
run: pip install certora-cli==7.14.2
4343

4444
- name: Install solc
4545
run: |
@@ -49,12 +49,12 @@ jobs:
4949
5050
- name: Verify rule ${{ matrix.rule }}
5151
run: |
52-
cd certora
52+
cd certora/basic
5353
touch applyHarness.patch
5454
make munged
55-
cd ..
55+
cd ../..
5656
echo "key length" ${#CERTORAKEY}
57-
certoraRun certora/conf/${{ matrix.rule }} --wait_for_results
57+
certoraRun certora/basic/conf/${{ matrix.rule }} --wait_for_results
5858
env:
5959
CERTORAKEY: ${{ secrets.CERTORAKEY }}
6060

@@ -68,6 +68,8 @@ jobs:
6868
- UserConfiguration.conf
6969
- VariableDebtToken.conf
7070
- NEW-pool-no-summarizations.conf
71+
- stableRemoved.conf
72+
- EModeConfiguration.conf
7173
- NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
7274
- NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
7375
- NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"

‎.github/workflows/certora-stata.yml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,7 @@ jobs:
5656
# - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
5757
- verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
5858
- verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
59-
- verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint
60-
- verifyERC4626Extended.conf --rule maxDepositConstant
59+
- verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
6160
- verifyERC4626Extended.conf --rule redeemSum
6261
- verifyERC4626Extended.conf --rule redeemATokensSum
6362
- verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf

‎certora/basic/Makefile‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
default: help
2+
3+
PATCH = applyHarness.patch
4+
CONTRACTS_DIR = ../../src/
5+
MUNGED_DIR = munged
6+
7+
help:
8+
@echo "usage:"
9+
@echo " make clean: remove all generated files (those ignored by git)"
10+
@echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
11+
@echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
12+
13+
munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
14+
rm -rf $@
15+
cp -r $(CONTRACTS_DIR) $@
16+
patch -p0 -d $@ < $(PATCH)
17+
18+
record:
19+
diff -ruN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+\.\./src/++g' | sed 's+munged/++g' > $(PATCH)
20+
21+
clean:
22+
git clean -fdX
23+
touch $(PATCH)
24+

certora/README.md renamed to certora/basic/README.md

File renamed without changes.

certora/applyHarness.patch renamed to certora/basic/applyHarness.patch

File renamed without changes.

‎certora/basic/conf/AToken.conf‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
{
2+
"files": [
3+
"certora/basic/harness/ATokenHarness.sol",
4+
"certora/basic/harness/SimpleERC20.sol"
5+
],
6+
"link": [
7+
"ATokenHarness:_underlyingAsset=SimpleERC20"
8+
],
9+
"rule_sanity": "basic", // from time to time, use "advanced" instead of "basic".
10+
"optimistic_loop": true,
11+
"process": "emv",
12+
"solc": "solc8.19",
13+
"verify": "ATokenHarness:certora/basic/specs/AToken.spec",
14+
"build_cache": true,
15+
"msg": "aToken spec"
16+
}

‎certora/basic/conf/EModeConfiguration.conf‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
{
2+
"files": [
3+
"certora/basic/harness/EModeConfigurationHarness.sol"
4+
],
5+
"msg": "EModeConfiguration",
6+
"optimistic_loop": true,
7+
"process": "emv",
8+
// "prover_args": [],
9+
"precise_bitwise_ops": true,
10+
"rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
11+
"solc": "solc8.19",
12+
"build_cache": true,
13+
"verify": "EModeConfigurationHarness:certora/basic/specs/EModeConfiguration.spec"
14+
}

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

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
{
2+
"files": [
3+
"certora/basic/harness/ATokenHarness.sol",
4+
"certora/basic/harness/PoolHarness.sol",
5+
"certora/basic/harness/SimpleERC20.sol",
6+
"src/contracts/instances/VariableDebtTokenInstance.sol",
7+
"src/contracts/helpers/AaveProtocolDataProvider.sol",
8+
"src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
9+
"src/contracts/protocol/configuration/ACLManager.sol",
10+
"src/contracts/misc/aave-upgradeability/InitializableImmutableAdminUpgradeabilityProxy.sol",
11+
"src/contracts/misc/PriceOracleSentinel.sol",
12+
"src/contracts/protocol/configuration/PoolAddressesProvider.sol",
13+
],
14+
"link": [
15+
"ATokenHarness:POOL=PoolHarness",
16+
"ATokenHarness:_underlyingAsset=SimpleERC20",
17+
"PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
18+
"AaveProtocolDataProvider:ADDRESSES_PROVIDER=PoolAddressesProvider",
19+
],
20+
"struct_link": [
21+
"PoolHarness:aTokenAddress=ATokenHarness",
22+
"PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
23+
"PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
24+
],
25+
"rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
26+
"optimistic_loop": true,
27+
"process": "emv",
28+
"global_timeout": "7198",
29+
"prover_args": ["-depth 11"], // If reachability passes and the time is ok, this number is ok, dont touch it.
30+
"solc": "solc8.19",
31+
"verify": "PoolHarness:certora/basic/specs/NEW-pool-no-summarizations.spec",
32+
"rule": [
33+
"liquidityIndexNonDecresingFor_cumulateToLiquidityIndex",
34+
"depositUpdatesUserATokenSuperBalance",
35+
"depositCannotChangeOthersATokenSuperBalance"
36+
],
37+
"build_cache": true,
38+
"parametric_contracts": ["PoolHarness"],
39+
"msg": "pool-no-summarizations::partial rules",
40+
}

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

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
{
2+
"files": [
3+
"certora/basic/harness/ATokenHarness.sol",
4+
"certora/basic/harness/PoolHarness.sol",
5+
"certora/basic/harness/SimpleERC20.sol",
6+
"src/contracts/instances/VariableDebtTokenInstance.sol",
7+
"src/contracts/helpers/AaveProtocolDataProvider.sol",
8+
"src/contracts/misc/DefaultReserveInterestRateStrategyV2.sol",
9+
"src/contracts/protocol/libraries/types/DataTypes.sol",
10+
"src/contracts/protocol/configuration/PoolAddressesProvider.sol",
11+
],
12+
"link": [
13+
"ATokenHarness:POOL=PoolHarness",
14+
"ATokenHarness:_underlyingAsset=SimpleERC20",
15+
"PoolHarness:ADDRESSES_PROVIDER=PoolAddressesProvider",
16+
],
17+
"struct_link": [
18+
"PoolHarness:aTokenAddress=ATokenHarness",
19+
"PoolHarness:variableDebtTokenAddress=VariableDebtTokenInstance",
20+
"PoolHarness:interestRateStrategyAddress=DefaultReserveInterestRateStrategyV2",
21+
],
22+
"rule_sanity": "basic", // from time to time, use advanced instead of basic, it gives more insight on requires, vacuity rules etc.
23+
"optimistic_loop": true,
24+
"process": "emv",
25+
"prover_args": ["-depth 12"], // If reachability passes and the time is ok, this number is ok, dont touch it.
26+
"solc": "solc8.19",
27+
"verify": "PoolHarness:certora/basic/specs/NEW-pool-simple-properties.spec",
28+
"build_cache": true,
29+
"parametric_contracts": ["PoolHarness"],
30+
"smt_timeout": "6000",
31+
"msg": "pool-simple-properties::ALL",
32+
}

‎certora/basic/conf/ReserveConfiguration.conf‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
{
2+
"files": [
3+
"certora/basic/harness/ReserveConfigurationHarness.sol"
4+
],
5+
"msg": "ReserveConfiguration",
6+
"optimistic_loop": true,
7+
"process": "emv",
8+
// "prover_args": [
9+
// "-precise_bitwise_ops"
10+
//],
11+
"precise_bitwise_ops": true,
12+
"rule_sanity": "basic", // from time to time, use "advanced" instead of "basic"
13+
"solc": "solc8.19",
14+
"build_cache": true,
15+
"verify": "ReserveConfigurationHarness:certora/basic/specs/ReserveConfiguration.spec"
16+
}

0 commit comments

Comments
 (0)