Skip to content

Commit 9ce1d06

Browse files
miguelmtzinfmiguelmtzinf
authored
Merge pull request #441 from Certora/certora
Certora - Addition of Gsm4626 Specs and Report
2 parents cf6ee42 + c766447 commit 9ce1d06

File tree

126 files changed

+4608
-14356
lines changed

Some content is hidden

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

126 files changed

+4608
-14356
lines changed

‎.github/workflows/certora-gho-505.yml

+5-5
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,18 @@ jobs:
1515
runs-on: ubuntu-latest
1616

1717
steps:
18-
- uses: actions/checkout@v2
18+
- name: Checkout
19+
uses: actions/checkout@v4
1920
with:
2021
submodules: recursive
2122

2223
- name: Install python
23-
uses: actions/setup-python@v2
24+
uses: actions/setup-python@v5
2425
with: { python-version: 3.9 }
2526

2627
- name: Install java
27-
uses: actions/setup-java@v1
28-
with: { java-version: '11', java-package: jre }
28+
uses: actions/setup-java@v4
29+
with: { distribution: "zulu", java-version: "11", java-package: jre }
2930

3031
- name: Install certora cli
3132
run: pip install certora-cli==5.0.5
@@ -42,7 +43,6 @@ jobs:
4243
touch applyHarness.patch
4344
make munged
4445
cd ../..
45-
echo "key length" ${#CERTORAKEY}
4646
certoraRun certora/gho/conf/${{ matrix.rule }}
4747
env:
4848
CERTORAKEY: ${{ secrets.CERTORAKEY }}

‎.github/workflows/certora-gho.yml

+5-5
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,18 @@ jobs:
1515
runs-on: ubuntu-latest
1616

1717
steps:
18-
- uses: actions/checkout@v2
18+
- name: Checkout
19+
uses: actions/checkout@v4
1920
with:
2021
submodules: recursive
2122

2223
- name: Install python
23-
uses: actions/setup-python@v2
24+
uses: actions/setup-python@v5
2425
with: { python-version: 3.9 }
2526

2627
- name: Install java
27-
uses: actions/setup-java@v1
28-
with: { java-version: '11', java-package: jre }
28+
uses: actions/setup-java@v4
29+
with: { distribution: "zulu", java-version: "11", java-package: jre }
2930

3031
- name: Install certora cli
3132
run: pip install certora-cli==4.13.1
@@ -42,7 +43,6 @@ jobs:
4243
touch applyHarness.patch
4344
make munged
4445
cd ../..
45-
echo "key length" ${#CERTORAKEY}
4646
certoraRun certora/gho/conf/${{ matrix.rule }}
4747
env:
4848
CERTORAKEY: ${{ secrets.CERTORAKEY }}

‎.github/workflows/certora-gsm-4626.yml

+73
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
name: certora-gsm-4626
2+
3+
on:
4+
push:
5+
branches:
6+
- main
7+
pull_request:
8+
branches:
9+
- main
10+
11+
workflow_dispatch:
12+
13+
jobs:
14+
verify:
15+
runs-on: ubuntu-latest
16+
17+
steps:
18+
- name: Checkout
19+
uses: actions/checkout@v4
20+
with:
21+
submodules: recursive
22+
23+
- name: Install python
24+
uses: actions/setup-python@v5
25+
with: { python-version: 3.9 }
26+
27+
- name: Install java
28+
uses: actions/setup-java@v4
29+
with: { distribution: "zulu", java-version: "11", java-package: jre }
30+
31+
- name: Install certora cli
32+
run: pip install certora-cli==7.14.2
33+
34+
- name: Install solc
35+
run: |
36+
wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux
37+
chmod +x solc-static-linux
38+
sudo mv solc-static-linux /usr/local/bin/solc8.10
39+
40+
- name: Verify rule ${{ matrix.rule }}
41+
run: |
42+
certoraRun certora/gsm/conf/gsm4626/${{ matrix.rule }}
43+
env:
44+
CERTORAKEY: ${{ secrets.CERTORAKEY }}
45+
46+
strategy:
47+
fail-fast: false
48+
max-parallel: 16
49+
matrix:
50+
rule:
51+
- gho-gsm_4626_inverse.conf --rule buySellInverse27 buySellInverse26 buySellInverse25 buySellInverse24 buySellInverse23 buySellInverse22 buySellInverse21 buySellInverse20 buySellInverse19
52+
- gho-gsm4626.conf --rule enoughULtoBackGhoNonBuySell NonZeroFeeCheckSellAsset NonZeroFeeCheckBuyAsset
53+
- balances-buy-4626.conf
54+
- balances-sell-4626.conf --rule R1_getAssetAmountForSellAsset_arg_vs_return R1a_buyGhoUpdatesGhoBalanceCorrectly1 R2_getAssetAmountForSellAsset_sellAsset_eq
55+
- balances-sell-4626.conf --rule R3a_sellAssetUpdatesAssetBalanceCorrectly
56+
- balances-sell-4626.conf --rule R4_buyGhoUpdatesGhoBalanceCorrectly R4a_buyGhoAmountGtGhoBalanceChange
57+
- fees-buy-4626.conf
58+
- fees-sell-4626.conf --rule R3a_estimatedSellFeeCanBeLowerThanActualSellFee R2_getAssetAmountForSellAssetVsActualSellFee R4a_getSellFeeVsgetAssetAmountForSellAsset R4_getSellFeeVsgetAssetAmountForSellAsset R1a_getAssetAmountForSellAssetFeeNeGetSellFee R2a_getAssetAmountForSellAssetNeActualSellFee R4b_getSellFeeVsgetAssetAmountForSellAsset R1_getAssetAmountForSellAssetFeeGeGetSellFee R3b_estimatedSellFeeEqActualSellFee
59+
- gho-gsm4626-2.conf --rule accruedFeesLEGhoBalanceOfThis accruedFeesNeverDecrease systemBalanceStabilitySell systemBalanceStabilitySell
60+
- optimality4626.conf --rule R5a_externalOptimalityOfSellAsset R6a_externalOptimalityOfBuyAsset
61+
- optimality4626.conf --rule R1_optimalityOfBuyAsset_v1
62+
- optimality4626.conf --rule R3_optimalityOfSellAsset_v1
63+
- getAmount_4626_properties.conf --rule getAssetAmountForBuyAsset_correctness_bound1 getAssetAmountForBuyAsset_correctness_bound2 getGhoAmountForBuyAsset_correctness_bound1 getAssetAmountForSellAsset_correctness getAssetAmountForBuyAsset_optimality getAssetAmountForBuyAsset_correctness
64+
- getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_optimality
65+
- getAmount_4626_properties.conf --rule getGhoAmountForBuyAsset_correctness
66+
- getAmount_4626_properties.conf --rule getAssetAmountForSellAsset_optimality getAssetAmountForBuyAsset_funcProperty
67+
- finishedRules4626.conf --rule cantBuyOrSellWhenSeized cantBuyOrSellWhenFrozen sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingAssetKeepsAccruedFees rescuingGhoKeepsAccruedFees giftingGhoDoesntAffectStorageSIMPLE correctnessOfBuyAsset giftingUnderlyingDoesntAffectStorageSIMPLE sellAssetSameAsGetGhoAmountForSellAsset correctnessOfSellAsset giftingGhoDoesntCreateExcessOrDearth backWithGhoDoesntCreateExcess getAssetAmountForSellAsset_correctness collectedSellFeeIsAtLeastAsRequired collectedBuyFeePlus2IsAtLeastAsRequired collectedBuyFeePlus1IsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired sellingDoesntExceedExposureCap whoCanChangeAccruedFees whoCanChangeExposure
68+
- finishedRules4626.conf --rule giftingUnderlyingDoesntCreateExcessOrDearth
69+
70+
71+
72+
73+

‎.github/workflows/certora-gsm.yml

+20-26
Original file line numberDiff line numberDiff line change
@@ -16,22 +16,17 @@ jobs:
1616

1717
steps:
1818
- name: Checkout
19-
uses: actions/checkout@v3
19+
uses: actions/checkout@v4
2020
with:
2121
submodules: recursive
2222

23-
- name: Check key
24-
env:
25-
CERTORAKEY: ${{ secrets.CERTORAKEY }}
26-
run: echo "key length" ${#CERTORAKEY}
27-
2823
- name: Install python
29-
uses: actions/setup-python@v2
24+
uses: actions/setup-python@v5
3025
with: { python-version: 3.9 }
3126

3227
- name: Install java
33-
uses: actions/setup-java@v1
34-
with: { java-version: '11', java-package: jre }
28+
uses: actions/setup-java@v4
29+
with: { distribution: "zulu", java-version: "11", java-package: jre }
3530

3631
- name: Install certora cli
3732
run: pip install certora-cli==6.1.3
@@ -44,8 +39,7 @@ jobs:
4439
4540
- name: Verify rule ${{ matrix.rule }}
4641
run: |
47-
echo "key length" ${#CERTORAKEY}
48-
certoraRun certora/GSM/conf/${{ matrix.rule }}
42+
certoraRun certora/gsm/conf/gsm/${{ matrix.rule }}
4943
env:
5044
CERTORAKEY: ${{ secrets.CERTORAKEY }}
5145

@@ -54,18 +48,18 @@ jobs:
5448
max-parallel: 16
5549
matrix:
5650
rule:
57-
- non-4626/Alex-gho-gsm_inverse.conf
58-
- non-4626/Alex-gho-gsm.conf
59-
- non-4626/balances-buy.conf
60-
- non-4626/balances-sell.conf
61-
- non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset
62-
- non-4626/Dominik-gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset
63-
- non-4626/Dominik-gho-fixedPriceStrategy.conf
64-
- non-4626/fees-buy.conf
65-
- non-4626/fees-sell.conf
66-
- non-4626/otakar-FixedFeeStrategy.conf
67-
- non-4626/Martin-gho-gsm.conf
68-
- non-4626/antti-optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2
69-
- non-4626/otakar-getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL
70-
- non-4626/otakar-finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees
71-
- non-4626/otakar-OracleSwapFreezer.conf
51+
- gho-gsm_inverse.conf
52+
- gho-gsm.conf
53+
- balances-buy.conf
54+
- balances-sell.conf
55+
- gho-assetToGhoInvertibility.conf --rule basicProperty_getAssetAmountForBuyAsset sellAssetInverse_all buyAssetInverse_all basicProperty_getGhoAmountForSellAsset basicProperty_getAssetAmountForSellAsset basicProperty_getGhoAmountForBuyAsset
56+
- gho-assetToGhoInvertibility.conf --rule basicProperty2_getAssetAmountForBuyAsset
57+
- gho-fixedPriceStrategy.conf
58+
- fees-buy.conf
59+
- fees-sell.conf
60+
- FixedFeeStrategy.conf
61+
- gho-gsm.conf
62+
- optimality.conf --rule R3_optimalityOfSellAsset_v1 R1_optimalityOfBuyAsset_v1 R6a_externalOptimalityOfBuyAsset R5a_externalOptimalityOfSellAsset R2_optimalityOfBuyAsset_v2
63+
- getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL
64+
- finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees
65+
- OracleSwapFreezer.conf

‎.github/workflows/certora-steward.yml

+5-5
Original file line numberDiff line numberDiff line change
@@ -15,17 +15,18 @@ jobs:
1515
runs-on: ubuntu-latest
1616

1717
steps:
18-
- uses: actions/checkout@v2
18+
- name: Checkout
19+
uses: actions/checkout@v4
1920
with:
2021
submodules: recursive
2122

2223
- name: Install python
23-
uses: actions/setup-python@v2
24+
uses: actions/setup-python@v5
2425
with: { python-version: 3.9 }
2526

2627
- name: Install java
27-
uses: actions/setup-java@v1
28-
with: { java-version: '11', java-package: jre }
28+
uses: actions/setup-java@v4
29+
with: { distribution: "zulu", java-version: "11", java-package: jre }
2930

3031
- name: Install certora cli
3132
run: pip install certora-cli
@@ -42,7 +43,6 @@ jobs:
4243
4344
- name: Verify rule ${{ matrix.rule }}
4445
run: |
45-
echo "key length" ${#CERTORAKEY}
4646
certoraRun certora/steward/conf/${{ matrix.rule }}
4747
env:
4848
CERTORAKEY: ${{ secrets.CERTORAKEY }}

‎certora/GSM/conf/non-4626/otakar-getAmount_properties.conf

-40
This file was deleted.

0 commit comments

Comments
 (0)