Skip to content

Commit 02fe2dc

Browse files
nisnislevinisnislevi
authored
test: update certora suite for 3.4 and addition of aTokenWithDelegation
1 parent 74412e2 commit 02fe2dc

File tree

66 files changed

+4741
-266
lines changed

Some content is hidden

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

66 files changed

+4741
-266
lines changed

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

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
name: certora-ATokenWithDelegation
2+
3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
7+
on:
8+
pull_request:
9+
branches:
10+
- main
11+
- certora
12+
push:
13+
branches:
14+
- main
15+
16+
workflow_dispatch:
17+
18+
jobs:
19+
verify:
20+
runs-on: ubuntu-latest
21+
if:
22+
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
23+
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
28+
steps:
29+
- uses: actions/checkout@v4
30+
with:
31+
submodules: recursive
32+
33+
- name: Munged
34+
run: |
35+
cd certora/atoken-with-delegation
36+
touch applyHarness.patch
37+
make munged
38+
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.28.0
42+
configurations: |-
43+
certora/atoken-with-delegation/conf/AToken.conf
44+
certora/atoken-with-delegation/conf/AToken-problematic-rules.conf --rule totalSupplyEqualsSumAllBalance additiveBurn additiveTransfer
45+
certora/atoken-with-delegation/conf/token-v3-general.conf
46+
certora/atoken-with-delegation/conf/token-v3-erc20.conf
47+
certora/atoken-with-delegation/conf/token-v3-delegate-basic.conf
48+
certora/atoken-with-delegation/conf/token-v3-delegate-invariants.conf --rule mirror_votingDelegatee_correct mirror_propositionDelegatee_correct mirror_delegationMode_correct mirror_balance_correct --rule_sanity "none"
49+
certora/atoken-with-delegation/conf/token-v3-delegate-invariants.conf --exclude_rule mirror_votingDelegatee_correct mirror_propositionDelegatee_correct mirror_delegationMode_correct mirror_balance_correct
50+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule vp_change_in_balance_affect_power_DELEGATEE
51+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule vp_change_of_balance_affect_power_NON_DELEGATEE
52+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_in_balance_affect_power_DELEGATEE
53+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_of_balance_affect_power_NON_DELEGATEE
54+
certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule no_function_changes_both_balance_and_delegation_state
55+
solc-versions: 0.8.27
56+
comment-fail-only: false
57+
solc-remove-version-prefix: "0."
58+
job-name: "Certora Prover Run"
59+
certora-key: ${{ secrets.CERTORAKEY }}
60+
install-java: true
61+
env:
62+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
63+
64+
65+
66+
67+
68+
69+
70+

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

Lines changed: 39 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ concurrency:
77
on:
88
pull_request:
99
branches:
10-
- certora
1110
- main
11+
- certora
1212
push:
1313
branches:
1414
- main
@@ -21,56 +21,50 @@ jobs:
2121
if:
2222
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
2323
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
24-
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
2528
steps:
2629
- uses: actions/checkout@v4
30+
with:
31+
submodules: recursive
2732

28-
- name: Install python
29-
uses: actions/setup-python@v5
30-
with: { python-version: 3.9 }
31-
32-
- name: Install java
33-
uses: actions/setup-java@v4
34-
with: { distribution: "zulu", java-version: "11", java-package: jre }
35-
36-
- name: Install certora cli
37-
run: pip install certora-cli==7.20.3
38-
39-
- name: Install solc
40-
run: |
41-
wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
42-
chmod +x solc-static-linux
43-
sudo mv solc-static-linux /usr/local/bin/solc8.19
44-
45-
- name: Verify rule ${{ matrix.rule }}
33+
- name: Munged
4634
run: |
4735
cd certora/basic
4836
touch applyHarness.patch
4937
make munged
50-
cd ../..
51-
echo "key length" ${#CERTORAKEY}
52-
certoraRun certora/basic/conf/${{ matrix.rule }} --wait_for_results
38+
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.28.0
42+
configurations: |-
43+
certora/basic/conf/AToken.conf
44+
certora/basic/conf/ReserveConfiguration.conf
45+
certora/basic/conf/UserConfiguration.conf
46+
certora/basic/conf/VariableDebtToken.conf
47+
certora/basic/conf/stableRemoved.conf
48+
certora/basic/conf/EModeConfiguration.conf
49+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve
50+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve
51+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount
52+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount
53+
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve
54+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount
55+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve
56+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing
57+
certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve
58+
solc-versions: 0.8.27
59+
comment-fail-only: false
60+
solc-remove-version-prefix: "0."
61+
job-name: "Certora Prover Run"
62+
certora-key: ${{ secrets.CERTORAKEY }}
63+
install-java: true
5364
env:
54-
CERTORAKEY: ${{ secrets.CERTORAKEY }}
65+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
66+
67+
68+
# Put back the following rule after ticket 8889 is closed
69+
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
5570

56-
strategy:
57-
fail-fast: false
58-
max-parallel: 16
59-
matrix:
60-
rule:
61-
- AToken.conf
62-
- ReserveConfiguration.conf
63-
- UserConfiguration.conf
64-
- VariableDebtToken.conf
65-
- NEW-pool-no-summarizations.conf
66-
- stableRemoved.conf
67-
- EModeConfiguration.conf
68-
- NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
69-
- NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
70-
- NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"
71-
- NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount --msg "cannotWithdrawZeroAmount"
72-
- NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve --msg "cannotWithdrawFromInactiveReserve"
73-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount"
74-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve"
75-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing"
76-
- NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve"

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

Lines changed: 48 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,15 @@
11
name: certora-stata
22

3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
37
on:
4-
push:
8+
pull_request:
59
branches:
610
- main
7-
pull_request:
11+
- certora
12+
push:
813
branches:
914
- main
1015

@@ -16,65 +21,55 @@ jobs:
1621
if:
1722
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
1823
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
19-
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
2028
steps:
2129
- uses: actions/checkout@v4
2230
with:
2331
submodules: recursive
2432

25-
- name: Install python
26-
uses: actions/setup-python@v5
27-
with: { python-version: 3.9 }
28-
29-
- name: Install java
30-
uses: actions/setup-java@v4
31-
with: { distribution: "zulu", java-version: "11", java-package: jre }
32-
33-
- name: Install certora cli
34-
run: pip install certora-cli==7.20.3
35-
- name: Install solc
36-
run: |
37-
wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
38-
chmod +x solc-static-linux
39-
sudo mv solc-static-linux /usr/local/bin/solc8.20
40-
41-
- name: Verify rule ${{ matrix.rule }}
33+
- name: Munged
4234
run: |
4335
cd certora/stata
4436
touch applyHarness.patch
4537
make munged
46-
cd ../..
47-
certoraRun certora/stata/conf/${{ matrix.rule }}
38+
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.28.0
42+
configurations: |-
43+
certora/stata/conf/verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance previewMintIndependentOfAllowance
44+
certora/stata/conf/verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
45+
certora/stata/conf/verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
46+
certora/stata/conf/verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
47+
certora/stata/conf/verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
48+
certora/stata/conf/verifyERC4626Extended.conf --rule redeemSum
49+
certora/stata/conf/verifyERC4626Extended.conf --rule redeemATokensSum
50+
certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
51+
certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
52+
certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
53+
certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
54+
certora/stata/conf/verifyStataToken.conf --rule totalClaimableRewards_stable
55+
certora/stata/conf/verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
56+
certora/stata/conf/verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
57+
certora/stata/conf/verifyStataToken.conf --rule singleAssetAccruedRewards
58+
certora/stata/conf/verifyStataToken.conf --rule totalAssets_stable
59+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable
60+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
61+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
62+
certora/stata/conf/verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
63+
certora/stata/conf/verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
64+
certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
65+
certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient
66+
solc-versions: 0.8.27
67+
comment-fail-only: false
68+
solc-remove-version-prefix: "0."
69+
job-name: "Certora Prover Run"
70+
certora-key: ${{ secrets.CERTORAKEY }}
71+
install-java: true
4872
env:
49-
CERTORAKEY: ${{ secrets.CERTORAKEY }}
73+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
74+
5075

51-
strategy:
52-
fail-fast: false
53-
max-parallel: 16
54-
matrix:
55-
rule:
56-
- verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance previewMintIndependentOfAllowance
57-
- verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
58-
# Timeout
59-
# - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
60-
- verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
61-
- verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
62-
- verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
63-
- verifyERC4626Extended.conf --rule redeemSum
64-
- verifyERC4626Extended.conf --rule redeemATokensSum
65-
- verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
66-
- verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
67-
- verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
68-
- verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
69-
- verifyStataToken.conf --rule totalClaimableRewards_stable
70-
- verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
71-
- verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
72-
- verifyStataToken.conf --rule singleAssetAccruedRewards
73-
- verifyStataToken.conf --rule totalAssets_stable
74-
- verifyStataToken.conf --rule getClaimableRewards_stable
75-
- verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
76-
- verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
77-
- verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
78-
- verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
79-
- verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
80-
- verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient

‎certora/atoken-with-delegation/Makefile‎

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

0 commit comments

Comments
 (0)